Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: ZF.thy Sprache: Isabelle

Original von: Isabelle^©

section\<open>Main ZF Theory: Everything Except AC\<close>

theory ZF imports List IntDiv CardinalArith begin

(*The theory of "iterates" logically belongs to Nat, but can't go there because
  primrec isn't available into after Datatype.*)

subsection\<open>Iteration of the function \<^term>\<open>F\<close>\<close>

consts  iterates :: "[i=>i,i,i] => i"   (\<open>(_^_ '(_'))\<close> [60,1000,1000] 60)

primrec
    "F^0 (x) = x"
    "F^(succ(n)) (x) = F(F^n (x))"

definition
  iterates_omega :: "[i=>i,i] => i" (\<open>(_^\<omega> '(_'))\<close> [60,1000] 60) where
    "F^\ (x) == \n\nat. F^n (x)"

lemma iterates_triv:
     "[| n\nat; F(x) = x |] ==> F^n (x) = x"
by (induct n rule: nat_induct, simp_all)

lemma iterates_type [TC]:
     "[| n \ nat; a \ A; !!x. x \ A ==> F(x) \ A |]
      ==> F^n (a) \<in> A"
by (induct n rule: nat_induct, simp_all)

lemma iterates_omega_triv:
    "F(x) = x ==> F^\ (x) = x"
by (simp add: iterates_omega_def iterates_triv)

lemma Ord_iterates [simp]:
     "[| n\nat; !!i. Ord(i) ==> Ord(F(i)); Ord(x) |]
      ==> Ord(F^n (x))"
by (induct n rule: nat_induct, simp_all)

lemma iterates_commute: "n \ nat ==> F(F^n (x)) = F^n (F(x))"
by (induct_tac n, simp_all)

subsection\<open>Transfinite Recursion\<close>

text\<open>Transfinite recursion for definitions based on the
    three cases of ordinals\<close>

definition
  transrec3 :: "[i, i, [i,i]=>i, [i,i]=>i] =>i" where
    "transrec3(k, a, b, c) ==
       transrec(k, \<lambda>x r.
         if x=0 then a
         else if Limit(x) then c(x, \<lambda>y\<in>x. r`y)
         else b(Arith.pred(x), r ` Arith.pred(x)))"

lemma transrec3_0 [simp]: "transrec3(0,a,b,c) = a"
by (rule transrec3_def [THEN def_transrec, THEN trans], simp)

lemma transrec3_succ [simp]:
     "transrec3(succ(i),a,b,c) = b(i, transrec3(i,a,b,c))"
by (rule transrec3_def [THEN def_transrec, THEN trans], simp)

lemma transrec3_Limit:
     "Limit(i) ==>
      transrec3(i,a,b,c) = c(i, \<lambda>j\<in>i. transrec3(j,a,b,c))"
by (rule transrec3_def [THEN def_transrec, THEN trans], force)

declaration \<open>fn _ =>
  Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt =>
    map mk_eq o Ord_atomize o Variable.gen_all ctxt))
\<close>

end

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.