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