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
```