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\ \<Longrightarrow> 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)\ \<Longrightarrow> 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.16 Sekunden
(vorverarbeitet)
¤
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.
