Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Eigene Datei ansehen e.g. http://myserver.net/mysource.java Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/ints/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 45 kB

Quellcode-Bibliothek Diagonal_Subsequence.thy Sprache: Isabelle

(* Author: Fabian Immler, TUM *)

section \<open>Sequence of Properties on Subsequences\<close>

theory Diagonal_Subsequence
imports Complex_Main
begin

locale subseqs =
  fixes P::"nat\(nat\nat)\bool"
  assumes ex_subseq: "\n s. strict_mono (s::nat\nat) \ \r'. strict_mono r' \ P n (s \ r')"
begin

definition reduce where "reduce s n = (SOME r'::nat\nat. strict_mono r' \ P n (s \ r'))"

lemma subseq_reduce[intro, simp]:
  "strict_mono s \ strict_mono (reduce s n)"
  unfolding reduce_def by (rule someI2_ex[OF ex_subseq]) auto

lemma reduce_holds:
  "strict_mono s \ P n (s \ reduce s n)"
  unfolding reduce_def by (rule someI2_ex[OF ex_subseq]) (auto simp: o_def)

primrec seqseq :: "nat \ nat \ nat" where
  "seqseq 0 = id"
| "seqseq (Suc n) = seqseq n \ reduce (seqseq n) n"

lemma subseq_seqseq[intro, simp]: "strict_mono (seqseq n)"
proof (induct n)
  case 0 thus ?case by (simp add: strict_mono_def)
next
  case (Suc n) thus ?case by (subst seqseq.simps) (auto intro!: strict_mono_o)
qed

lemma seqseq_holds:
  "P n (seqseq (Suc n))"
proof -
  have "P n (seqseq n \ reduce (seqseq n) n)"
    by (intro reduce_holds subseq_seqseq)
  thus ?thesis by simp
qed

definition diagseq :: "nat \ nat" where "diagseq i = seqseq i i"

lemma diagseq_mono: "diagseq n < diagseq (Suc n)"
proof -
  have "diagseq n < seqseq n (Suc n)"
    using subseq_seqseq[of n] by (simp add: diagseq_def strict_mono_def)
  also have "\ \ seqseq n (reduce (seqseq n) n (Suc n))"
    using strict_mono_less_eq seq_suble by blast
  also have "\ = diagseq (Suc n)" by (simp add: diagseq_def)
  finally show ?thesis .
qed

lemma subseq_diagseq: "strict_mono diagseq"
  using diagseq_mono by (simp add: strict_mono_Suc_iff diagseq_def)

primrec fold_reduce where
  "fold_reduce n 0 = id"
| "fold_reduce n (Suc k) = fold_reduce n k \ reduce (seqseq (n + k)) (n + k)"

lemma subseq_fold_reduce[intro, simp]: "strict_mono (fold_reduce n k)"
proof (induct k)
  case (Suc k) from strict_mono_o[OF this subseq_reduce] show ?case by (simp add: o_def)
qed (simp add: strict_mono_def)

lemma ex_subseq_reduce_index: "seqseq (n + k) = seqseq n \ fold_reduce n k"
  by (induct k) simp_all

lemma seqseq_fold_reduce: "seqseq n = fold_reduce 0 n"
  by (induct n) (simp_all)

lemma diagseq_fold_reduce: "diagseq n = fold_reduce 0 n n"
  using seqseq_fold_reduce by (simp add: diagseq_def)

lemma fold_reduce_add: "fold_reduce 0 (m + n) = fold_reduce 0 m \ fold_reduce m n"
  by (induct n) simp_all

lemma diagseq_add: "diagseq (k + n) = (seqseq k \ (fold_reduce k n)) (k + n)"
proof -
  have "diagseq (k + n) = fold_reduce 0 (k + n) (k + n)"
    by (simp add: diagseq_fold_reduce)
  also have "\ = (seqseq k \ fold_reduce k n) (k + n)"
    unfolding fold_reduce_add seqseq_fold_reduce ..
  finally show ?thesis .
qed

lemma diagseq_sub:
  assumes "m \ n" shows "diagseq n = (seqseq m \ (fold_reduce m (n - m))) n"
  using diagseq_add[of m "n - m"] assms by simp

lemma subseq_diagonal_rest: "strict_mono (\x. fold_reduce k x (k + x))"
  unfolding strict_mono_Suc_iff fold_reduce.simps o_def
proof
  fix n
  have "fold_reduce k n (k + n) < fold_reduce k n (k + Suc n)" (is "?lhs < _")
    by (auto intro: strict_monoD)
  also have "\ \ fold_reduce k n (reduce (seqseq (k + n)) (k + n) (k + Suc n))"
    by (auto intro: less_mono_imp_le_mono seq_suble strict_monoD)
  finally show "?lhs < \" .
qed

lemma diagseq_seqseq: "diagseq \ ((+) k) = (seqseq k \ (\x. fold_reduce k x (k + x)))"
  by (auto simp: o_def diagseq_add)

lemma diagseq_holds:
  assumes subseq_stable: "\r s n. strict_mono r \ P n s \ P n (s \ r)"
  shows "P k (diagseq \ ((+) (Suc k)))"
  unfolding diagseq_seqseq by (intro subseq_stable subseq_diagonal_rest seqseq_holds)

end

end

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.13Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.