author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46953  2b6e55924af3 
child 58871  c399ae4b836f 
permissions  rwrr 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

1 
header{*Theory Main: Everything Except AC*} 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

2 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

3 
theory Main_ZF imports List_ZF IntDiv_ZF CardinalArith begin 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

4 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

5 
(*The theory of "iterates" logically belongs to Nat, but can't go there because 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

6 
primrec isn't available into after Datatype.*) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

7 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

8 
subsection{* Iteration of the function @{term F} *} 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

9 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

10 
consts iterates :: "[i=>i,i,i] => i" ("(_^_ '(_'))" [60,1000,1000] 60) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

11 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

12 
primrec 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

13 
"F^0 (x) = x" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

14 
"F^(succ(n)) (x) = F(F^n (x))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

15 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

16 
definition 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

17 
iterates_omega :: "[i=>i,i] => i" where 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

18 
"iterates_omega(F,x) == \<Union>n\<in>nat. F^n (x)" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

19 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

20 
notation (xsymbols) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

21 
iterates_omega ("(_^\<omega> '(_'))" [60,1000] 60) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

22 
notation (HTML output) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

23 
iterates_omega ("(_^\<omega> '(_'))" [60,1000] 60) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

24 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

25 
lemma iterates_triv: 
46953  26 
"[ n\<in>nat; F(x) = x ] ==> F^n (x) = x" 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

27 
by (induct n rule: nat_induct, simp_all) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

28 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

29 
lemma iterates_type [TC]: 
46953  30 
"[ n \<in> nat; a \<in> A; !!x. x \<in> A ==> F(x) \<in> A ] 
31 
==> F^n (a) \<in> A" 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

32 
by (induct n rule: nat_induct, simp_all) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

33 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

34 
lemma iterates_omega_triv: 
46953  35 
"F(x) = x ==> F^\<omega> (x) = x" 
36 
by (simp add: iterates_omega_def iterates_triv) 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

37 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

38 
lemma Ord_iterates [simp]: 
46953  39 
"[ n\<in>nat; !!i. Ord(i) ==> Ord(F(i)); Ord(x) ] 
40 
==> Ord(F^n (x))" 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

41 
by (induct n rule: nat_induct, simp_all) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

42 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

43 
lemma iterates_commute: "n \<in> nat ==> F(F^n (x)) = F^n (F(x))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

44 
by (induct_tac n, simp_all) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

45 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

46 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

47 
subsection{* Transfinite Recursion *} 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

48 

46953  49 
text{*Transfinite recursion for definitions based on the 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

50 
three cases of ordinals*} 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

51 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

52 
definition 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

53 
transrec3 :: "[i, i, [i,i]=>i, [i,i]=>i] =>i" where 
46953  54 
"transrec3(k, a, b, c) == 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

55 
transrec(k, \<lambda>x r. 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

56 
if x=0 then a 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

57 
else if Limit(x) then c(x, \<lambda>y\<in>x. r`y) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

58 
else b(Arith.pred(x), r ` Arith.pred(x)))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

59 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

60 
lemma transrec3_0 [simp]: "transrec3(0,a,b,c) = a" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

61 
by (rule transrec3_def [THEN def_transrec, THEN trans], simp) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

62 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

63 
lemma transrec3_succ [simp]: 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

64 
"transrec3(succ(i),a,b,c) = b(i, transrec3(i,a,b,c))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

65 
by (rule transrec3_def [THEN def_transrec, THEN trans], simp) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

66 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

67 
lemma transrec3_Limit: 
46953  68 
"Limit(i) ==> 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

69 
transrec3(i,a,b,c) = c(i, \<lambda>j\<in>i. transrec3(j,a,b,c))" 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

70 
by (rule transrec3_def [THEN def_transrec, THEN trans], force) 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

71 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

72 

26339  73 
declaration {* fn _ => 
45625
750c5a47400b
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
36543
diff
changeset

74 
Simplifier.map_ss (Simplifier.set_mksimps (K (map mk_eq o Ord_atomize o gen_all))) 
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

75 
*} 
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

76 

6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset

77 
end 