# Theory ZF

section‹Main ZF Theory: Everything Except AC›

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‹Iteration of the function termF

consts  iterates :: "[ii,i,i]  i"   ((_^_ '(_')) [60,1000,1000] 60)

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

definition
iterates_omega :: "[ii,i]  i" ((_ '(_')) [60,1000] 60) where
"F (x)  nnat. F^n (x)"

lemma iterates_triv:
"nnat;  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)  A"
by (induct n rule: nat_induct, simp_all)

lemma iterates_omega_triv:
"F(x) = x  F (x) = x"

lemma Ord_iterates [simp]:
"nnat;  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‹Transfinite Recursion›

text‹Transfinite recursion for definitions based on the
three cases of ordinals›

definition
transrec3 :: "[i, i, [i,i]i, [i,i]i] i" where
"transrec3(k, a, b, c)
transrec(k, λx r.
if x=0 then a
else if Limit(x) then c(x, λyx. 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, λji. transrec3(j,a,b,c))"
by (rule transrec3_def [THEN def_transrec, THEN trans], force)

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

end