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{*


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


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


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 upperbound for all elements of the


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


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$:


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);


24 
assume aS: "a:S";


25 
assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : 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


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


34 


35 
assume "c={}";


36 
with aS; show ?thesis; by fast;


37 


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


39 
is an upperbound of $c$, that lies in $S$. *};


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;
