equal
deleted
inserted
replaced
|
1 (* Title: HOL/Real/HahnBanach/Zorn_Lemma.thy |
|
2 ID: $Id$ |
|
3 Author: Gertrud Bauer, TU Munich |
|
4 *) |
1 |
5 |
2 theory Zorn_Lemma = Zorn:; |
6 theory Zorn_Lemma = Aux + Zorn:; |
3 |
7 |
4 |
8 |
5 lemma Zorn's_Lemma: "a:S ==> (!!c. c: chain S ==> EX x. x:c ==> Union c : S) ==> |
9 lemma Zorn's_Lemma: "a:S ==> (!!c. c: chain S ==> EX x. x:c ==> Union c : S) ==> |
6 EX y: S. ALL z: S. y <= z --> y = z"; |
10 EX y: S. ALL z: S. y <= z --> y = z"; |
7 proof (rule Zorn_Lemma2); |
11 proof (rule Zorn_Lemma2); |
13 have s: "EX x. x:c ==> Union c : S"; |
17 have s: "EX x. x:c ==> Union c : S"; |
14 by (rule r); |
18 by (rule r); |
15 show "EX y:S. ALL z:c. z <= y"; |
19 show "EX y:S. ALL z:c. z <= y"; |
16 proof (rule case [of "c={}"]); |
20 proof (rule case [of "c={}"]); |
17 assume "c={}"; |
21 assume "c={}"; |
18 show ?thesis; by fast; |
22 show ?thesis; by (fast!); |
19 next; |
23 next; |
20 assume "c~={}"; |
24 assume "c~={}"; |
21 show ?thesis; |
25 show ?thesis; |
22 proof; |
26 proof; |
23 have "EX x. x:c"; by fast; |
27 have "EX x. x:c"; by (fast!); |
24 thus "Union c : S"; by (rule s); |
28 thus "Union c : S"; by (rule s); |
25 show "ALL z:c. z <= Union c"; by fast; |
29 show "ALL z:c. z <= Union c"; by fast; |
26 qed; |
30 qed; |
27 qed; |
31 qed; |
28 qed; |
32 qed; |