7917

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


2 
ID: $Id$


3 
Author: Gertrud Bauer, TU Munich


4 
*)


5 


6 
header {* Zorn's Lemma *};


7 


8 
theory ZornLemma = Aux + Zorn:;


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


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

7917

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


21 
proof (rule Zorn_Lemma2);

8104

22 
txt_raw {* \footnote{See

7978

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

8104

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

7917

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 (rule case_split);


31 


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

7978

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

7917

34 


35 
assume "c={}";


36 
with aS; show ?thesis; by fast;


37 

7927

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

7978

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

7917

40 


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;


54 


55 
end;
