equal
deleted
inserted
replaced
1 section{*Theory Main: Everything Except AC*} |
1 section\<open>Theory Main: Everything Except AC\<close> |
2 |
2 |
3 theory Main_ZF imports List_ZF IntDiv_ZF CardinalArith begin |
3 theory Main_ZF imports List_ZF IntDiv_ZF CardinalArith begin |
4 |
4 |
5 (*The theory of "iterates" logically belongs to Nat, but can't go there because |
5 (*The theory of "iterates" logically belongs to Nat, but can't go there because |
6 primrec isn't available into after Datatype.*) |
6 primrec isn't available into after Datatype.*) |
7 |
7 |
8 subsection{* Iteration of the function @{term F} *} |
8 subsection\<open>Iteration of the function @{term F}\<close> |
9 |
9 |
10 consts iterates :: "[i=>i,i,i] => i" ("(_^_ '(_'))" [60,1000,1000] 60) |
10 consts iterates :: "[i=>i,i,i] => i" ("(_^_ '(_'))" [60,1000,1000] 60) |
11 |
11 |
12 primrec |
12 primrec |
13 "F^0 (x) = x" |
13 "F^0 (x) = x" |
42 |
42 |
43 lemma iterates_commute: "n \<in> nat ==> F(F^n (x)) = F^n (F(x))" |
43 lemma iterates_commute: "n \<in> nat ==> F(F^n (x)) = F^n (F(x))" |
44 by (induct_tac n, simp_all) |
44 by (induct_tac n, simp_all) |
45 |
45 |
46 |
46 |
47 subsection{* Transfinite Recursion *} |
47 subsection\<open>Transfinite Recursion\<close> |
48 |
48 |
49 text{*Transfinite recursion for definitions based on the |
49 text\<open>Transfinite recursion for definitions based on the |
50 three cases of ordinals*} |
50 three cases of ordinals\<close> |
51 |
51 |
52 definition |
52 definition |
53 transrec3 :: "[i, i, [i,i]=>i, [i,i]=>i] =>i" where |
53 transrec3 :: "[i, i, [i,i]=>i, [i,i]=>i] =>i" where |
54 "transrec3(k, a, b, c) == |
54 "transrec3(k, a, b, c) == |
55 transrec(k, \<lambda>x r. |
55 transrec(k, \<lambda>x r. |
68 "Limit(i) ==> |
68 "Limit(i) ==> |
69 transrec3(i,a,b,c) = c(i, \<lambda>j\<in>i. transrec3(j,a,b,c))" |
69 transrec3(i,a,b,c) = c(i, \<lambda>j\<in>i. transrec3(j,a,b,c))" |
70 by (rule transrec3_def [THEN def_transrec, THEN trans], force) |
70 by (rule transrec3_def [THEN def_transrec, THEN trans], force) |
71 |
71 |
72 |
72 |
73 declaration {* fn _ => |
73 declaration \<open>fn _ => |
74 Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt => |
74 Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt => |
75 map mk_eq o Ord_atomize o Drule.gen_all (Variable.maxidx_of ctxt))) |
75 map mk_eq o Ord_atomize o Drule.gen_all (Variable.maxidx_of ctxt))) |
76 *} |
76 \<close> |
77 |
77 |
78 end |
78 end |