|
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.6 Sekunden
(vorverarbeitet)
¤
|
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.
|
