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