21 iterates_omega ("(_^\<omega> '(_'))" [60,1000] 60) |
21 iterates_omega ("(_^\<omega> '(_'))" [60,1000] 60) |
22 notation (HTML output) |
22 notation (HTML output) |
23 iterates_omega ("(_^\<omega> '(_'))" [60,1000] 60) |
23 iterates_omega ("(_^\<omega> '(_'))" [60,1000] 60) |
24 |
24 |
25 lemma iterates_triv: |
25 lemma iterates_triv: |
26 "[| n\<in>nat; F(x) = x |] ==> F^n (x) = x" |
26 "[| n\<in>nat; F(x) = x |] ==> F^n (x) = x" |
27 by (induct n rule: nat_induct, simp_all) |
27 by (induct n rule: nat_induct, simp_all) |
28 |
28 |
29 lemma iterates_type [TC]: |
29 lemma iterates_type [TC]: |
30 "[| n:nat; a: A; !!x. x:A ==> F(x) \<in> A |] |
30 "[| n \<in> nat; a \<in> A; !!x. x \<in> A ==> F(x) \<in> A |] |
31 ==> F^n (a) \<in> A" |
31 ==> F^n (a) \<in> A" |
32 by (induct n rule: nat_induct, simp_all) |
32 by (induct n rule: nat_induct, simp_all) |
33 |
33 |
34 lemma iterates_omega_triv: |
34 lemma iterates_omega_triv: |
35 "F(x) = x ==> F^\<omega> (x) = x" |
35 "F(x) = x ==> F^\<omega> (x) = x" |
36 by (simp add: iterates_omega_def iterates_triv) |
36 by (simp add: iterates_omega_def iterates_triv) |
37 |
37 |
38 lemma Ord_iterates [simp]: |
38 lemma Ord_iterates [simp]: |
39 "[| n\<in>nat; !!i. Ord(i) ==> Ord(F(i)); Ord(x) |] |
39 "[| n\<in>nat; !!i. Ord(i) ==> Ord(F(i)); Ord(x) |] |
40 ==> Ord(F^n (x))" |
40 ==> Ord(F^n (x))" |
41 by (induct n rule: nat_induct, simp_all) |
41 by (induct n rule: nat_induct, simp_all) |
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{* Transfinite Recursion *} |
48 |
48 |
49 text{*Transfinite recursion for definitions based on the |
49 text{*Transfinite recursion for definitions based on the |
50 three cases of ordinals*} |
50 three cases of ordinals*} |
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. |
56 if x=0 then a |
56 if x=0 then a |
57 else if Limit(x) then c(x, \<lambda>y\<in>x. r`y) |
57 else if Limit(x) then c(x, \<lambda>y\<in>x. r`y) |
58 else b(Arith.pred(x), r ` Arith.pred(x)))" |
58 else b(Arith.pred(x), r ` Arith.pred(x)))" |
59 |
59 |
63 lemma transrec3_succ [simp]: |
63 lemma transrec3_succ [simp]: |
64 "transrec3(succ(i),a,b,c) = b(i, transrec3(i,a,b,c))" |
64 "transrec3(succ(i),a,b,c) = b(i, transrec3(i,a,b,c))" |
65 by (rule transrec3_def [THEN def_transrec, THEN trans], simp) |
65 by (rule transrec3_def [THEN def_transrec, THEN trans], simp) |
66 |
66 |
67 lemma transrec3_Limit: |
67 lemma transrec3_Limit: |
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 {* fn _ => |