7917

1 
(* Title: HOL/Real/HahnBanach/ZornLemma.thy


2 
ID: $Id$


3 
Author: Gertrud Bauer, TU Munich


4 
*)


5 

9035

6 
header {* Zorn's Lemma *}

7917

7 

9035

8 
theory ZornLemma = Aux + Zorn:

7917

9 

8104

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


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


14 
for all elements of the chain, the conditions of Zorn's lemma can be


15 
modified: if $S$ is nonempty, it suffices to show that for every

9035

16 
nonempty chain $c$ in $S$ the union of $c$ also lies in $S$. *}

7917

17 


18 
theorem Zorn's_Lemma:

8104

19 
"(!!c. c: chain S ==> EX x. x:c ==> Union c : S) ==> a:S

9035

20 
==> EX y: S. ALL z: S. y <= z > y = z"


21 
proof (rule Zorn_Lemma2)

8104

22 
txt_raw {* \footnote{See

9035

23 
\url{http://isabelle.in.tum.de/library/HOL/HOLReal/Zorn.html}} \isanewline *}


24 
assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S"


25 
assume aS: "a:S"


26 
show "ALL c:chain S. EX y:S. ALL z:c. z <= y"


27 
proof


28 
fix c assume "c:chain S"


29 
show "EX y:S. ALL z:c. z <= y"


30 
proof cases

7917

31 


32 
txt{* If $c$ is an empty chain, then every element

9035

33 
in $S$ is an upper bound of $c$. *}

7917

34 

9035

35 
assume "c={}"


36 
with aS show ?thesis by fast

7917

37 

7927

38 
txt{* If $c$ is nonempty, then $\Union c$

9035

39 
is an upper bound of $c$, lying in $S$. *}

7917

40 

9035

41 
next


42 
assume c: "c~={}"


43 
show ?thesis


44 
proof


45 
show "ALL z:c. z <= Union c" by fast


46 
show "Union c : S"


47 
proof (rule r)


48 
from c show "EX x. x:c" by fast


49 
qed


50 
qed


51 
qed


52 
qed


53 
qed

7917

54 

9035

55 
end 