author | wenzelm |
Sun, 21 Mar 2010 19:28:25 +0100 | |
changeset 35852 | 4e3fe0b8687b |
parent 29580 | 117b88da143c |
child 36543 | 0e7fc5bf38de |
permissions | -rw-r--r-- |
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: |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
26 |
"[| n\<in>nat; F(x) = x |] ==> F^n (x) = x" |
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]: |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
30 |
"[| n:nat; a: A; !!x. x:A ==> F(x) : A |] |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
31 |
==> F^n (a) : A" |
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: |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
35 |
"F(x) = x ==> F^\<omega> (x) = x" |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
36 |
by (simp add: iterates_omega_def iterates_triv) |
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]: |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
39 |
"[| n\<in>nat; !!i. Ord(i) ==> Ord(F(i)); Ord(x) |] |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
40 |
==> Ord(F^n (x))" |
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 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
49 |
text{*Transfinite recursion for definitions based on the |
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 |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
54 |
"transrec3(k, a, b, c) == |
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: |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
68 |
"Limit(i) ==> |
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 _ => |
74 |
Simplifier.map_ss (fn ss => ss setmksimps (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 |