author | paulson |
Tue, 18 Jun 2002 10:52:08 +0200 | |
changeset 13218 | 3732064ccbd1 |
parent 13203 | fac77a839aa2 |
child 13356 | c9cfe1638bf2 |
permissions | -rw-r--r-- |
12552
d2d2ab3f1f37
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
paulson
parents:
12426
diff
changeset
|
1 |
(*$Id$ |
d2d2ab3f1f37
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
paulson
parents:
12426
diff
changeset
|
2 |
theory Main includes everything except AC*) |
5157 | 3 |
|
12552
d2d2ab3f1f37
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
paulson
parents:
12426
diff
changeset
|
4 |
theory Main = Update + List + EquivClass + IntDiv + CardinalArith: |
12426 | 5 |
|
6 |
(* belongs to theory Trancl *) |
|
7 |
lemmas rtrancl_induct = rtrancl_induct [case_names initial step, induct set: rtrancl] |
|
8 |
and trancl_induct = trancl_induct [case_names initial step, induct set: trancl] |
|
9 |
and converse_trancl_induct = converse_trancl_induct [case_names initial step, consumes 1] |
|
10 |
and rtrancl_full_induct = rtrancl_full_induct [case_names initial step, consumes 1] |
|
11 |
||
12 |
||
13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
13 |
|
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13162
diff
changeset
|
14 |
(*The theory of "iterates" logically belongs to Nat, but can't go there because |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13162
diff
changeset
|
15 |
primrec isn't available into after Datatype. The only theories defined |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13162
diff
changeset
|
16 |
after Datatype are List and the Integ theories.*) |
13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
17 |
subsection{* Iteration of the function @{term F} *} |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
18 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
19 |
consts iterates :: "[i=>i,i,i] => i" ("(_^_ '(_'))" [60,1000,1000] 60) |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
20 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
21 |
primrec |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
22 |
"F^0 (x) = x" |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
23 |
"F^(succ(n)) (x) = F(F^n (x))" |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
24 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
25 |
constdefs |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
26 |
iterates_omega :: "[i=>i,i] => i" |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
27 |
"iterates_omega(F,x) == \<Union>n\<in>nat. F^n (x)" |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
28 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
29 |
syntax (xsymbols) |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
30 |
iterates_omega :: "[i=>i,i] => i" ("(_^\<omega> '(_'))" [60,1000] 60) |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
31 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
32 |
lemma iterates_triv: |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
33 |
"[| n\<in>nat; F(x) = x |] ==> F^n (x) = x" |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
34 |
by (induct n rule: nat_induct, simp_all) |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
35 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
36 |
lemma iterates_type [TC]: |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
37 |
"[| n:nat; a: A; !!x. x:A ==> F(x) : A |] |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
38 |
==> F^n (a) : A" |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
39 |
by (induct n rule: nat_induct, simp_all) |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
40 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
41 |
lemma iterates_omega_triv: |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
42 |
"F(x) = x ==> F^\<omega> (x) = x" |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
43 |
by (simp add: iterates_omega_def iterates_triv) |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
44 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
45 |
lemma Ord_iterates [simp]: |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
46 |
"[| n\<in>nat; !!i. Ord(i) ==> Ord(F(i)); Ord(x) |] |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
47 |
==> Ord(F^n (x))" |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
48 |
by (induct n rule: nat_induct, simp_all) |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
49 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
50 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
51 |
(* belongs to theory Cardinal *) |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
52 |
declare Ord_Least [intro,simp,TC] |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
53 |
|
12426 | 54 |
|
55 |
(* belongs to theory List *) |
|
56 |
lemmas list_append_induct = list_append_induct [case_names Nil snoc, consumes 1] |
|
57 |
||
58 |
(* belongs to theory IntDiv *) |
|
59 |
lemmas posDivAlg_induct = posDivAlg_induct [consumes 2] |
|
60 |
and negDivAlg_induct = negDivAlg_induct [consumes 2] |
|
61 |
||
12620 | 62 |
|
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13162
diff
changeset
|
63 |
(* belongs to theory CardinalArith *) |
12620 | 64 |
|
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13162
diff
changeset
|
65 |
lemmas Finite_induct = Finite_induct [case_names 0 cons, induct set: Finite] |
12776 | 66 |
|
13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
67 |
lemma InfCard_square_eqpoll: "InfCard(K) ==> K \<times> K \<approx> K" |
12820 | 68 |
apply (rule well_ord_InfCard_square_eq) |
69 |
apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN well_ord_Memrel]) |
|
70 |
apply (simp add: InfCard_is_Card [THEN Card_cardinal_eq]) |
|
12776 | 71 |
done |
72 |
||
73 |
lemma Inf_Card_is_InfCard: "[| ~Finite(i); Card(i) |] ==> InfCard(i)" |
|
74 |
by (simp add: InfCard_def Card_is_Ord [THEN nat_le_infinite_Ord]) |
|
75 |
||
12426 | 76 |
end |