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