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 


10 
text{*

7978

11 
Zorn's Lemmas states: if every linear ordered subset of an ordered set

7917

12 
$S$ has an upper bound in $S$, then there exists a maximal element in $S$.

7978

13 
In our application, $S$ is a set of sets ordered by set inclusion. Since


14 
the union of a chain of sets is an upper bound for all elements of the

7917

15 
chain, the conditions of Zorn's lemma can be modified:

7927

16 
if $S$ is nonempty, it suffices to show that for every nonempty


17 
chain $c$ in $S$ the union of $c$ also lies in $S$.

7917

18 
*};


19 


20 
theorem Zorn's_Lemma:


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


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


23 
proof (rule Zorn_Lemma2);

7978

24 
txt_raw{* \footnote{See


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

7917

26 
assume aS: "a:S";


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


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


29 
proof;


30 
fix c; assume "c:chain S";


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


32 
proof (rule case_split);


33 


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

7978

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

7917

36 


37 
assume "c={}";


38 
with aS; show ?thesis; by fast;


39 

7927

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

7978

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

7917

42 


43 
next;


44 
assume c: "c~={}";


45 
show ?thesis;


46 
proof;


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


48 
show "Union c : S";


49 
proof (rule r);


50 
from c; show "EX x. x:c"; by fast;


51 
qed;


52 
qed;


53 
qed;


54 
qed;


55 
qed;


56 


57 
end;
