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