src/ZF/Main_ZF.thy
 author wenzelm Sun Nov 09 17:04:14 2014 +0100 (2014-11-09) changeset 58957 c9e744ea8a38 parent 58871 c399ae4b836f child 59647 c6f413b660cf permissions -rw-r--r--
proper context for match_tac etc.;
 wenzelm@58871 ` 1` ```section{*Theory Main: Everything Except AC*} ``` krauss@26056 ` 2` krauss@26056 ` 3` ```theory Main_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` krauss@26056 ` 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 ``` krauss@26056 ` 17` ``` iterates_omega :: "[i=>i,i] => i" where ``` krauss@26056 ` 18` ``` "iterates_omega(F,x) == \n\nat. F^n (x)" ``` krauss@26056 ` 19` krauss@26056 ` 20` ```notation (xsymbols) ``` krauss@26056 ` 21` ``` iterates_omega ("(_^\ '(_'))" [60,1000] 60) ``` krauss@26056 ` 22` ```notation (HTML output) ``` krauss@26056 ` 23` ``` iterates_omega ("(_^\ '(_'))" [60,1000] 60) ``` krauss@26056 ` 24` krauss@26056 ` 25` ```lemma iterates_triv: ``` paulson@46953 ` 26` ``` "[| n\nat; F(x) = x |] ==> F^n (x) = x" ``` krauss@26056 ` 27` ```by (induct n rule: nat_induct, simp_all) ``` krauss@26056 ` 28` krauss@26056 ` 29` ```lemma iterates_type [TC]: ``` paulson@46953 ` 30` ``` "[| n \ nat; a \ A; !!x. x \ A ==> F(x) \ A |] ``` paulson@46953 ` 31` ``` ==> F^n (a) \ A" ``` krauss@26056 ` 32` ```by (induct n rule: nat_induct, simp_all) ``` krauss@26056 ` 33` krauss@26056 ` 34` ```lemma iterates_omega_triv: ``` paulson@46953 ` 35` ``` "F(x) = x ==> F^\ (x) = x" ``` paulson@46953 ` 36` ```by (simp add: iterates_omega_def iterates_triv) ``` krauss@26056 ` 37` krauss@26056 ` 38` ```lemma Ord_iterates [simp]: ``` paulson@46953 ` 39` ``` "[| n\nat; !!i. Ord(i) ==> Ord(F(i)); Ord(x) |] ``` paulson@46953 ` 40` ``` ==> Ord(F^n (x))" ``` krauss@26056 ` 41` ```by (induct n rule: nat_induct, simp_all) ``` krauss@26056 ` 42` krauss@26056 ` 43` ```lemma iterates_commute: "n \ nat ==> F(F^n (x)) = F^n (F(x))" ``` krauss@26056 ` 44` ```by (induct_tac n, simp_all) ``` krauss@26056 ` 45` krauss@26056 ` 46` krauss@26056 ` 47` ```subsection{* Transfinite Recursion *} ``` krauss@26056 ` 48` paulson@46953 ` 49` ```text{*Transfinite recursion for definitions based on the ``` krauss@26056 ` 50` ``` three cases of ordinals*} ``` krauss@26056 ` 51` krauss@26056 ` 52` ```definition ``` krauss@26056 ` 53` ``` transrec3 :: "[i, i, [i,i]=>i, [i,i]=>i] =>i" where ``` paulson@46953 ` 54` ``` "transrec3(k, a, b, c) == ``` krauss@26056 ` 55` ``` transrec(k, \x r. ``` krauss@26056 ` 56` ``` if x=0 then a ``` krauss@26056 ` 57` ``` else if Limit(x) then c(x, \y\x. r`y) ``` krauss@26056 ` 58` ``` else b(Arith.pred(x), r ` Arith.pred(x)))" ``` krauss@26056 ` 59` krauss@26056 ` 60` ```lemma transrec3_0 [simp]: "transrec3(0,a,b,c) = a" ``` krauss@26056 ` 61` ```by (rule transrec3_def [THEN def_transrec, THEN trans], simp) ``` krauss@26056 ` 62` krauss@26056 ` 63` ```lemma transrec3_succ [simp]: ``` krauss@26056 ` 64` ``` "transrec3(succ(i),a,b,c) = b(i, transrec3(i,a,b,c))" ``` krauss@26056 ` 65` ```by (rule transrec3_def [THEN def_transrec, THEN trans], simp) ``` krauss@26056 ` 66` krauss@26056 ` 67` ```lemma transrec3_Limit: ``` paulson@46953 ` 68` ``` "Limit(i) ==> ``` krauss@26056 ` 69` ``` transrec3(i,a,b,c) = c(i, \j\i. transrec3(j,a,b,c))" ``` krauss@26056 ` 70` ```by (rule transrec3_def [THEN def_transrec, THEN trans], force) ``` krauss@26056 ` 71` krauss@26056 ` 72` wenzelm@26339 ` 73` ```declaration {* fn _ => ``` wenzelm@45625 ` 74` ``` Simplifier.map_ss (Simplifier.set_mksimps (K (map mk_eq o Ord_atomize o gen_all))) ``` krauss@26056 ` 75` ```*} ``` krauss@26056 ` 76` krauss@26056 ` 77` ```end ```