1 (* Title: HOL/Real/HahnBanach/ZornLemma.thy |
1 (* Title: HOL/Real/HahnBanach/ZornLemma.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Gertrud Bauer, TU Munich |
3 Author: Gertrud Bauer, TU Munich |
4 *) |
4 *) |
5 |
5 |
6 header {* Zorn's Lemma *}; |
6 header {* Zorn's Lemma *} |
7 |
7 |
8 theory ZornLemma = Aux + Zorn:; |
8 theory ZornLemma = Aux + Zorn: |
9 |
9 |
10 text {* Zorn's Lemmas states: if every linear ordered subset of an |
10 text {* Zorn's Lemmas states: if every linear ordered subset of an |
11 ordered set $S$ has an upper bound in $S$, then there exists a maximal |
11 ordered set $S$ has an upper bound in $S$, then there exists a maximal |
12 element in $S$. In our application, $S$ is a set of sets ordered by |
12 element in $S$. In our application, $S$ is a set of sets ordered by |
13 set inclusion. Since the union of a chain of sets is an upper bound |
13 set inclusion. Since the union of a chain of sets is an upper bound |
14 for all elements of the chain, the conditions of Zorn's lemma can be |
14 for all elements of the chain, the conditions of Zorn's lemma can be |
15 modified: if $S$ is non-empty, it suffices to show that for every |
15 modified: if $S$ is non-empty, it suffices to show that for every |
16 non-empty chain $c$ in $S$ the union of $c$ also lies in $S$. *}; |
16 non-empty chain $c$ in $S$ the union of $c$ also lies in $S$. *} |
17 |
17 |
18 theorem Zorn's_Lemma: |
18 theorem Zorn's_Lemma: |
19 "(!!c. c: chain S ==> EX x. x:c ==> Union c : S) ==> a:S |
19 "(!!c. c: chain S ==> EX x. x:c ==> Union c : S) ==> a:S |
20 ==> EX y: S. ALL z: S. y <= z --> y = z"; |
20 ==> EX y: S. ALL z: S. y <= z --> y = z" |
21 proof (rule Zorn_Lemma2); |
21 proof (rule Zorn_Lemma2) |
22 txt_raw {* \footnote{See |
22 txt_raw {* \footnote{See |
23 \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Zorn.html}} \isanewline *}; |
23 \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Zorn.html}} \isanewline *} |
24 assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S"; |
24 assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S" |
25 assume aS: "a:S"; |
25 assume aS: "a:S" |
26 show "ALL c:chain S. EX y:S. ALL z:c. z <= y"; |
26 show "ALL c:chain S. EX y:S. ALL z:c. z <= y" |
27 proof; |
27 proof |
28 fix c; assume "c:chain S"; |
28 fix c assume "c:chain S" |
29 show "EX y:S. ALL z:c. z <= y"; |
29 show "EX y:S. ALL z:c. z <= y" |
30 proof cases; |
30 proof cases |
31 |
31 |
32 txt{* If $c$ is an empty chain, then every element |
32 txt{* If $c$ is an empty chain, then every element |
33 in $S$ is an upper bound of $c$. *}; |
33 in $S$ is an upper bound of $c$. *} |
34 |
34 |
35 assume "c={}"; |
35 assume "c={}" |
36 with aS; show ?thesis; by fast; |
36 with aS show ?thesis by fast |
37 |
37 |
38 txt{* If $c$ is non-empty, then $\Union c$ |
38 txt{* If $c$ is non-empty, then $\Union c$ |
39 is an upper bound of $c$, lying in $S$. *}; |
39 is an upper bound of $c$, lying in $S$. *} |
40 |
40 |
41 next; |
41 next |
42 assume c: "c~={}"; |
42 assume c: "c~={}" |
43 show ?thesis; |
43 show ?thesis |
44 proof; |
44 proof |
45 show "ALL z:c. z <= Union c"; by fast; |
45 show "ALL z:c. z <= Union c" by fast |
46 show "Union c : S"; |
46 show "Union c : S" |
47 proof (rule r); |
47 proof (rule r) |
48 from c; show "EX x. x:c"; by fast; |
48 from c show "EX x. x:c" by fast |
49 qed; |
49 qed |
50 qed; |
50 qed |
51 qed; |
51 qed |
52 qed; |
52 qed |
53 qed; |
53 qed |
54 |
54 |
55 end; |
55 end |