author | paulson |
Fri, 19 Jul 2002 13:28:19 +0200 | |
changeset 13396 | 11219ca224ab |
parent 13356 | c9cfe1638bf2 |
child 13694 | be3e2fa01b0f |
permissions | -rw-r--r-- |
13356 | 1 |
(*$Id$*) |
12426 | 2 |
|
13356 | 3 |
header{*Theory Main: Everything Except AC*} |
12426 | 4 |
|
13356 | 5 |
theory Main = List + IntDiv + CardinalArith: |
13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
6 |
|
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13162
diff
changeset
|
7 |
(*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
|
8 |
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
|
9 |
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
|
10 |
subsection{* Iteration of the function @{term F} *} |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
11 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
12 |
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
|
13 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
14 |
primrec |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
15 |
"F^0 (x) = x" |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
16 |
"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
|
17 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
18 |
constdefs |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
19 |
iterates_omega :: "[i=>i,i] => i" |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
20 |
"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
|
21 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
22 |
syntax (xsymbols) |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
23 |
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
|
24 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
25 |
lemma iterates_triv: |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
26 |
"[| 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
|
27 |
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
|
28 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
29 |
lemma iterates_type [TC]: |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
30 |
"[| 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
|
31 |
==> F^n (a) : A" |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
32 |
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
|
33 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
34 |
lemma iterates_omega_triv: |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
35 |
"F(x) = x ==> F^\<omega> (x) = x" |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
36 |
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
|
37 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
38 |
lemma Ord_iterates [simp]: |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
39 |
"[| 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
|
40 |
==> Ord(F^n (x))" |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
41 |
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
|
42 |
|
13396 | 43 |
lemma iterates_commute: "n \<in> nat ==> F(F^n (x)) = F^n (F(x))" |
44 |
by (induct_tac n, simp_all) |
|
45 |
||
13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
12820
diff
changeset
|
46 |
|
12426 | 47 |
(* belongs to theory IntDiv *) |
48 |
lemmas posDivAlg_induct = posDivAlg_induct [consumes 2] |
|
49 |
and negDivAlg_induct = negDivAlg_induct [consumes 2] |
|
50 |
||
12620 | 51 |
|
12426 | 52 |
end |