src/HOL/Real/HahnBanach/ZornLemma.thy
author wenzelm
Tue Jul 15 19:39:37 2008 +0200 (2008-07-15)
changeset 27612 d3eb431db035
parent 23378 1d138d6bb461
child 29234 60f7fb56f8cd
permissions -rw-r--r--
modernized specifications and proofs;
tuned document;
     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
     9 imports Zorn
    10 begin
    11 
    12 text {*
    13   Zorn's Lemmas states: if every linear ordered subset of an ordered
    14   set @{text S} has an upper bound in @{text S}, then there exists a
    15   maximal element in @{text S}.  In our application, @{text S} is a
    16   set of sets ordered by set inclusion. Since the union of a chain of
    17   sets is an upper bound for all elements of the chain, the conditions
    18   of Zorn's lemma can be modified: if @{text S} is non-empty, it
    19   suffices to show that for every non-empty chain @{text c} in @{text
    20   S} the union of @{text c} also lies in @{text S}.
    21 *}
    22 
    23 theorem Zorn's_Lemma:
    24   assumes r: "\<And>c. c \<in> chain S \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> \<Union>c \<in> S"
    25     and aS: "a \<in> S"
    26   shows "\<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z \<longrightarrow> y = z"
    27 proof (rule Zorn_Lemma2)
    28   show "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
    29   proof
    30     fix c assume "c \<in> chain S"
    31     show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
    32     proof cases
    33 
    34       txt {* If @{text c} is an empty chain, then every element in
    35 	@{text S} is an upper bound of @{text c}. *}
    36 
    37       assume "c = {}"
    38       with aS show ?thesis by fast
    39 
    40       txt {* If @{text c} is non-empty, then @{text "\<Union>c"} is an upper
    41 	bound of @{text c}, lying in @{text S}. *}
    42 
    43     next
    44       assume "c \<noteq> {}"
    45       show ?thesis
    46       proof
    47         show "\<forall>z \<in> c. z \<subseteq> \<Union>c" by fast
    48         show "\<Union>c \<in> S"
    49         proof (rule r)
    50           from `c \<noteq> {}` show "\<exists>x. x \<in> c" by fast
    51 	  show "c \<in> chain S" by fact
    52         qed
    53       qed
    54     qed
    55   qed
    56 qed
    57 
    58 end