author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 44887  7ca82df6e951 
child 52183  667961fa6a60 
permissions  rwrr 
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29252
diff
changeset

1 
(* Title: HOL/Hahn_Banach/Zorn_Lemma.thy 
7917  2 
Author: Gertrud Bauer, TU Munich 
3 
*) 

4 

9035  5 
header {* Zorn's Lemma *} 
7917  6 

31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29252
diff
changeset

7 
theory Zorn_Lemma 
44887  8 
imports "~~/src/HOL/Library/Zorn" 
27612  9 
begin 
7917  10 

10687  11 
text {* 
12 
Zorn's Lemmas states: if every linear ordered subset of an ordered 

13 
set @{text S} has an upper bound in @{text S}, then there exists a 

14 
maximal element in @{text S}. In our application, @{text S} is a 

15 
set of sets ordered by set inclusion. Since the union of a chain of 

16 
sets is an upper bound for all elements of the chain, the conditions 

17 
of Zorn's lemma can be modified: if @{text S} is nonempty, it 

18 
suffices to show that for every nonempty chain @{text c} in @{text 

19 
S} the union of @{text c} also lies in @{text S}. 

20 
*} 

7917  21 

10687  22 
theorem Zorn's_Lemma: 
13515  23 
assumes r: "\<And>c. c \<in> chain S \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> \<Union>c \<in> S" 
24 
and aS: "a \<in> S" 

25 
shows "\<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z \<longrightarrow> y = z" 

9035  26 
proof (rule Zorn_Lemma2) 
10687  27 
show "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y" 
9035  28 
proof 
10687  29 
fix c assume "c \<in> chain S" 
30 
show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y" 

9035  31 
proof cases 
13515  32 

10687  33 
txt {* If @{text c} is an empty chain, then every element in 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

34 
@{text S} is an upper bound of @{text c}. *} 
7917  35 

13515  36 
assume "c = {}" 
9035  37 
with aS show ?thesis by fast 
7917  38 

10687  39 
txt {* If @{text c} is nonempty, then @{text "\<Union>c"} is an upper 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

40 
bound of @{text c}, lying in @{text S}. *} 
7917  41 

9035  42 
next 
27612  43 
assume "c \<noteq> {}" 
13515  44 
show ?thesis 
45 
proof 

10687  46 
show "\<forall>z \<in> c. z \<subseteq> \<Union>c" by fast 
13515  47 
show "\<Union>c \<in> S" 
9035  48 
proof (rule r) 
27612  49 
from `c \<noteq> {}` show "\<exists>x. x \<in> c" by fast 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

50 
show "c \<in> chain S" by fact 
9035  51 
qed 
52 
qed 

53 
qed 

54 
qed 

55 
qed 

7917  56 

10687  57 
end 