author | wenzelm |
Sat, 02 Sep 2000 21:51:14 +0200 | |
changeset 9805 | 10b617bdd028 |
parent 5314 | c061e6f9d546 |
child 11317 | 7f9e4c389318 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/AC/AC16_WO4.thy |
1196 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Krzysztof Grabczewski |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
4 |
|
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
5 |
Tidied using locales by LCP |
1196 | 6 |
*) |
7 |
||
8 |
AC16_WO4 = OrderType + AC16_lemmas + Cardinal_aux + |
|
9 |
||
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
10 |
locale AC16 = |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
11 |
fixes |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
12 |
x :: i |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
13 |
y :: i |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
14 |
k :: i |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
15 |
l :: i |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
16 |
m :: i |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
17 |
t_n :: i |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
18 |
R :: i |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
19 |
MM :: i |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
20 |
LL :: i |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
21 |
GG :: i |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
22 |
s :: i=>i |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
23 |
assumes |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
24 |
all_ex "ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
25 |
EX! w. w:t_n & z <= w " |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
26 |
disjoint "x Int y = 0" |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
27 |
includes "t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}" |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
28 |
WO_R "well_ord(y,R)" |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
29 |
lnat "l:nat" |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
30 |
mnat "m:nat" |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
31 |
mpos "0<m" |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
32 |
Infinite "~ Finite(y)" |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
33 |
noLepoll "~ y lepoll {v:Pow(x). v eqpoll m}" |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
1478
diff
changeset
|
34 |
defines |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
35 |
k_def "k == succ(l)" |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
36 |
MM_def "MM == {v:t_n. succ(k) lepoll v Int y}" |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
37 |
LL_def "LL == {v Int y. v:MM}" |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
38 |
GG_def "GG == lam v:LL. (THE w. w:MM & v <= w) - v" |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
39 |
s_def "s(u) == {v:t_n. u:v & k lepoll v Int y}" |
1196 | 40 |
|
41 |
end |