1.1 --- a/src/HOL/HahnBanach/ZornLemma.thy Wed Jun 24 21:28:02 2009 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,57 +0,0 @@
1.4 -(* Title: HOL/Real/HahnBanach/ZornLemma.thy
1.5 - Author: Gertrud Bauer, TU Munich
1.6 -*)
1.7 -
1.8 -header {* Zorn's Lemma *}
1.9 -
1.10 -theory ZornLemma
1.11 -imports Zorn
1.12 -begin
1.13 -
1.14 -text {*
1.15 - Zorn's Lemmas states: if every linear ordered subset of an ordered
1.16 - set @{text S} has an upper bound in @{text S}, then there exists a
1.17 - maximal element in @{text S}. In our application, @{text S} is a
1.18 - set of sets ordered by set inclusion. Since the union of a chain of
1.19 - sets is an upper bound for all elements of the chain, the conditions
1.20 - of Zorn's lemma can be modified: if @{text S} is non-empty, it
1.21 - suffices to show that for every non-empty chain @{text c} in @{text
1.22 - S} the union of @{text c} also lies in @{text S}.
1.23 -*}
1.24 -
1.25 -theorem Zorn's_Lemma:
1.26 - assumes r: "\<And>c. c \<in> chain S \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> \<Union>c \<in> S"
1.27 - and aS: "a \<in> S"
1.28 - shows "\<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z \<longrightarrow> y = z"
1.29 -proof (rule Zorn_Lemma2)
1.30 - show "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
1.31 - proof
1.32 - fix c assume "c \<in> chain S"
1.33 - show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
1.34 - proof cases
1.35 -
1.36 - txt {* If @{text c} is an empty chain, then every element in
1.37 - @{text S} is an upper bound of @{text c}. *}
1.38 -
1.39 - assume "c = {}"
1.40 - with aS show ?thesis by fast
1.41 -
1.42 - txt {* If @{text c} is non-empty, then @{text "\<Union>c"} is an upper
1.43 - bound of @{text c}, lying in @{text S}. *}
1.44 -
1.45 - next
1.46 - assume "c \<noteq> {}"
1.47 - show ?thesis
1.48 - proof
1.49 - show "\<forall>z \<in> c. z \<subseteq> \<Union>c" by fast
1.50 - show "\<Union>c \<in> S"
1.51 - proof (rule r)
1.52 - from `c \<noteq> {}` show "\<exists>x. x \<in> c" by fast
1.53 - show "c \<in> chain S" by fact
1.54 - qed
1.55 - qed
1.56 - qed
1.57 - qed
1.58 -qed
1.59 -
1.60 -end