src/HOL/Real/HahnBanach/ZornLemma.thy
author wenzelm
Fri Oct 22 20:14:31 1999 +0200 (1999-10-22)
changeset 7917 5e5b9813cce7
child 7927 b50446a33c16
permissions -rw-r--r--
HahnBanach update by Gertrud Bauer;
wenzelm@7917
     1
(*  Title:      HOL/Real/HahnBanach/ZornLemma.thy
wenzelm@7917
     2
    ID:         $Id$
wenzelm@7917
     3
    Author:     Gertrud Bauer, TU Munich
wenzelm@7917
     4
*)
wenzelm@7917
     5
wenzelm@7917
     6
header {* Zorn's Lemma *};
wenzelm@7917
     7
wenzelm@7917
     8
theory ZornLemma = Aux + Zorn:;
wenzelm@7917
     9
wenzelm@7917
    10
text{* 
wenzelm@7917
    11
Zorn's Lemmas says: if every linear ordered subset of an ordered set 
wenzelm@7917
    12
$S$ has an upper bound in $S$, then there exists a maximal element in $S$.
wenzelm@7917
    13
In our application $S$ is a set of sets, ordered by set inclusion. Since 
wenzelm@7917
    14
the union of a chain of sets is an upperbound for all elements of the 
wenzelm@7917
    15
chain, the conditions of Zorn's lemma can be modified:
wenzelm@7917
    16
If $S$ is non-empty, it suffices to show that for every non-empty 
wenzelm@7917
    17
chain $c$ in $S$ the union of $c$ also lies in $S$:
wenzelm@7917
    18
*};
wenzelm@7917
    19
wenzelm@7917
    20
theorem Zorn's_Lemma: 
wenzelm@7917
    21
  "a:S ==> (!!c. c: chain S ==> EX x. x:c ==> Union c : S) 
wenzelm@7917
    22
  ==>  EX y: S. ALL z: S. y <= z --> y = z";
wenzelm@7917
    23
proof (rule Zorn_Lemma2);
wenzelm@7917
    24
  assume aS: "a:S";
wenzelm@7917
    25
  assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S";
wenzelm@7917
    26
  show "ALL c:chain S. EX y:S. ALL z:c. z <= y";
wenzelm@7917
    27
  proof;
wenzelm@7917
    28
    fix c; assume "c:chain S"; 
wenzelm@7917
    29
    show "EX y:S. ALL z:c. z <= y";
wenzelm@7917
    30
    proof (rule case_split);
wenzelm@7917
    31
 
wenzelm@7917
    32
      txt{* If $c$ is an empty chain, then every element
wenzelm@7917
    33
      in $S$ is an upperbound of $c$. *};
wenzelm@7917
    34
wenzelm@7917
    35
      assume "c={}"; 
wenzelm@7917
    36
      with aS; show ?thesis; by fast;
wenzelm@7917
    37
wenzelm@7917
    38
      txt{* If $c$ is non-empty, then $\cup\; c$ 
wenzelm@7917
    39
      is an upperbound of $c$, that lies in $S$. *};
wenzelm@7917
    40
wenzelm@7917
    41
    next;
wenzelm@7917
    42
      assume c: "c~={}";
wenzelm@7917
    43
      show ?thesis; 
wenzelm@7917
    44
      proof; 
wenzelm@7917
    45
        show "ALL z:c. z <= Union c"; by fast;
wenzelm@7917
    46
        show "Union c : S"; 
wenzelm@7917
    47
        proof (rule r);
wenzelm@7917
    48
          from c; show "EX x. x:c"; by fast;  
wenzelm@7917
    49
        qed;
wenzelm@7917
    50
      qed;
wenzelm@7917
    51
    qed;
wenzelm@7917
    52
  qed;
wenzelm@7917
    53
qed;
wenzelm@7917
    54
wenzelm@7917
    55
end;