3 Author : Jacques D. Fleuriot |
3 Author : Jacques D. Fleuriot |
4 Copyright : 1998 University of Cambridge |
4 Copyright : 1998 University of Cambridge |
5 Description : Zorn's Lemma -- See lcp's Zorn.thy in ZF |
5 Description : Zorn's Lemma -- See lcp's Zorn.thy in ZF |
6 *) |
6 *) |
7 |
7 |
8 Zorn = Main + |
8 Zorn = Main + |
9 |
9 |
10 constdefs |
10 constdefs |
11 chain :: 'a set => 'a set set |
11 chain :: 'a::ord set => 'a set set |
12 "chain S == {F. F <= S & (ALL x: F. ALL y: F. x <= y | y <= x)}" |
12 "chain S == {F. F <= S & (ALL x: F. ALL y: F. x <= y | y <= x)}" |
13 |
13 |
14 super :: ['a set,'a set] => (('a set) set) |
14 super :: ['a::ord set,'a set] => 'a set set |
15 "super S c == {d. d: chain(S) & c < d}" |
15 "super S c == {d. d: chain(S) & c < d}" |
16 |
16 |
17 maxchain :: 'a set => 'a set set |
17 maxchain :: 'a::ord set => 'a set set |
18 "maxchain S == {c. c: chain S & super S c = {}}" |
18 "maxchain S == {c. c: chain S & super S c = {}}" |
19 |
19 |
20 succ :: ['a set,'a set] => 'a set |
20 succ :: ['a::ord set,'a set] => 'a set |
21 "succ S c == if (c ~: chain S| c: maxchain S) |
21 "succ S c == if (c ~: chain S| c: maxchain S) |
22 then c else (@c'. c': (super S c))" |
22 then c else (@c'. c': (super S c))" |
23 |
23 |
24 consts |
24 consts |
25 "TFin" :: 'a set => 'a set set |
25 "TFin" :: 'a::ord set => 'a set set |
26 |
26 |
27 inductive "TFin(S)" |
27 inductive "TFin(S)" |
28 intrs |
28 intrs |
29 succI "x : TFin S ==> succ S x : TFin S" |
29 succI "x : TFin S ==> succ S x : TFin S" |
30 Pow_UnionI "Y : Pow(TFin S) ==> Union(Y) : TFin S" |
30 Pow_UnionI "Y : Pow(TFin S) ==> Union(Y) : TFin S" |