src/ZF/ZF.thy
 author wenzelm Sat Nov 04 19:17:19 2017 +0100 (21 months ago) changeset 67006 b1278ed3cd46 parent 65464 f3cd78ba687c child 68490 eb53f944c8cd permissions -rw-r--r--
prefer main entry points of HOL;
 wenzelm@65453 ` 1` ```section\Main ZF Theory: Everything Except AC\ ``` krauss@26056 ` 2` wenzelm@65449 ` 3` ```theory ZF imports List_ZF IntDiv_ZF CardinalArith begin ``` krauss@26056 ` 4` krauss@26056 ` 5` ```(*The theory of "iterates" logically belongs to Nat, but can't go there because ``` krauss@26056 ` 6` ``` primrec isn't available into after Datatype.*) ``` krauss@26056 ` 7` wenzelm@60770 ` 8` ```subsection\Iteration of the function @{term F}\ ``` krauss@26056 ` 9` krauss@26056 ` 10` ```consts iterates :: "[i=>i,i,i] => i" ("(_^_ '(_'))" [60,1000,1000] 60) ``` krauss@26056 ` 11` krauss@26056 ` 12` ```primrec ``` krauss@26056 ` 13` ``` "F^0 (x) = x" ``` krauss@26056 ` 14` ``` "F^(succ(n)) (x) = F(F^n (x))" ``` krauss@26056 ` 15` krauss@26056 ` 16` ```definition ``` wenzelm@61397 ` 17` ``` iterates_omega :: "[i=>i,i] => i" ("(_^\ '(_'))" [60,1000] 60) where ``` wenzelm@61397 ` 18` ``` "F^\ (x) == \n\nat. F^n (x)" ``` krauss@26056 ` 19` krauss@26056 ` 20` ```lemma iterates_triv: ``` paulson@46953 ` 21` ``` "[| n\nat; F(x) = x |] ==> F^n (x) = x" ``` krauss@26056 ` 22` ```by (induct n rule: nat_induct, simp_all) ``` krauss@26056 ` 23` krauss@26056 ` 24` ```lemma iterates_type [TC]: ``` paulson@46953 ` 25` ``` "[| n \ nat; a \ A; !!x. x \ A ==> F(x) \ A |] ``` paulson@46953 ` 26` ``` ==> F^n (a) \ A" ``` krauss@26056 ` 27` ```by (induct n rule: nat_induct, simp_all) ``` krauss@26056 ` 28` krauss@26056 ` 29` ```lemma iterates_omega_triv: ``` paulson@46953 ` 30` ``` "F(x) = x ==> F^\ (x) = x" ``` paulson@46953 ` 31` ```by (simp add: iterates_omega_def iterates_triv) ``` krauss@26056 ` 32` krauss@26056 ` 33` ```lemma Ord_iterates [simp]: ``` paulson@46953 ` 34` ``` "[| n\nat; !!i. Ord(i) ==> Ord(F(i)); Ord(x) |] ``` paulson@46953 ` 35` ``` ==> Ord(F^n (x))" ``` krauss@26056 ` 36` ```by (induct n rule: nat_induct, simp_all) ``` krauss@26056 ` 37` krauss@26056 ` 38` ```lemma iterates_commute: "n \ nat ==> F(F^n (x)) = F^n (F(x))" ``` krauss@26056 ` 39` ```by (induct_tac n, simp_all) ``` krauss@26056 ` 40` krauss@26056 ` 41` wenzelm@60770 ` 42` ```subsection\Transfinite Recursion\ ``` krauss@26056 ` 43` wenzelm@60770 ` 44` ```text\Transfinite recursion for definitions based on the ``` wenzelm@60770 ` 45` ``` three cases of ordinals\ ``` krauss@26056 ` 46` krauss@26056 ` 47` ```definition ``` krauss@26056 ` 48` ``` transrec3 :: "[i, i, [i,i]=>i, [i,i]=>i] =>i" where ``` paulson@46953 ` 49` ``` "transrec3(k, a, b, c) == ``` krauss@26056 ` 50` ``` transrec(k, \x r. ``` krauss@26056 ` 51` ``` if x=0 then a ``` krauss@26056 ` 52` ``` else if Limit(x) then c(x, \y\x. r`y) ``` krauss@26056 ` 53` ``` else b(Arith.pred(x), r ` Arith.pred(x)))" ``` krauss@26056 ` 54` krauss@26056 ` 55` ```lemma transrec3_0 [simp]: "transrec3(0,a,b,c) = a" ``` krauss@26056 ` 56` ```by (rule transrec3_def [THEN def_transrec, THEN trans], simp) ``` krauss@26056 ` 57` krauss@26056 ` 58` ```lemma transrec3_succ [simp]: ``` krauss@26056 ` 59` ``` "transrec3(succ(i),a,b,c) = b(i, transrec3(i,a,b,c))" ``` krauss@26056 ` 60` ```by (rule transrec3_def [THEN def_transrec, THEN trans], simp) ``` krauss@26056 ` 61` krauss@26056 ` 62` ```lemma transrec3_Limit: ``` paulson@46953 ` 63` ``` "Limit(i) ==> ``` krauss@26056 ` 64` ``` transrec3(i,a,b,c) = c(i, \j\i. transrec3(j,a,b,c))" ``` krauss@26056 ` 65` ```by (rule transrec3_def [THEN def_transrec, THEN trans], force) ``` krauss@26056 ` 66` krauss@26056 ` 67` wenzelm@60770 ` 68` ```declaration \fn _ => ``` wenzelm@59647 ` 69` ``` Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt => ``` wenzelm@60822 ` 70` ``` map mk_eq o Ord_atomize o Variable.gen_all ctxt)) ``` wenzelm@60770 ` 71` ```\ ``` krauss@26056 ` 72` krauss@26056 ` 73` ```end ```