src/HOL/Library/Zorn.thy
changeset 14706 71590b7733b7
parent 13652 172600c40793
child 15131 c69542757a4d
     1.1 --- a/src/HOL/Library/Zorn.thy	Thu May 06 12:43:00 2004 +0200
     1.2 +++ b/src/HOL/Library/Zorn.thy	Thu May 06 14:14:18 2004 +0200
     1.3 @@ -1,39 +1,40 @@
     1.4 -(*  Title       : Zorn.thy
     1.5 +(*  Title       : HOL/Library/Zorn.thy
     1.6      ID          : $Id$
     1.7      Author      : Jacques D. Fleuriot
     1.8 -    Description : Zorn's Lemma -- See Larry Paulson's Zorn.thy in ZF
     1.9 -*) 
    1.10 +    Description : Zorn's Lemma -- see Larry Paulson's Zorn.thy in ZF
    1.11 +*)
    1.12  
    1.13 -header {*Zorn's Lemma*}
    1.14 +header {* Zorn's Lemma *}
    1.15  
    1.16  theory Zorn = Main:
    1.17  
    1.18 -text{*The lemma and section numbers refer to an unpublished article ``Towards
    1.19 -the Mechanization of the Proofs of Some Classical Theorems of Set Theory,'' by
    1.20 -Abrial and Laffitte.  *}
    1.21 +text{*
    1.22 +  The lemma and section numbers refer to an unpublished article
    1.23 +  \cite{Abrial-Laffitte}.
    1.24 +*}
    1.25  
    1.26  constdefs
    1.27    chain     ::  "'a set set => 'a set set set"
    1.28 -    "chain S  == {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}" 
    1.29 +  "chain S  == {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}"
    1.30  
    1.31    super     ::  "['a set set,'a set set] => 'a set set set"
    1.32 -    "super S c == {d. d \<in> chain(S) & c < d}"
    1.33 +  "super S c == {d. d \<in> chain S & c \<subset> d}"
    1.34  
    1.35    maxchain  ::  "'a set set => 'a set set set"
    1.36 -    "maxchain S == {c. c \<in> chain S & super S c = {}}"
    1.37 +  "maxchain S == {c. c \<in> chain S & super S c = {}}"
    1.38  
    1.39    succ      ::  "['a set set,'a set set] => 'a set set"
    1.40 -    "succ S c == if (c \<notin> chain S| c \<in> maxchain S) 
    1.41 -                 then c else (@c'. c': (super S c))" 
    1.42 +  "succ S c ==
    1.43 +    if c \<notin> chain S | c \<in> maxchain S
    1.44 +    then c else SOME c'. c' \<in> super S c"
    1.45  
    1.46 -consts 
    1.47 -  "TFin" ::  "'a set set => 'a set set set"
    1.48 +consts
    1.49 +  TFin :: "'a set set => 'a set set set"
    1.50  
    1.51 -inductive "TFin(S)"
    1.52 +inductive "TFin S"
    1.53    intros
    1.54      succI:        "x \<in> TFin S ==> succ S x \<in> TFin S"
    1.55      Pow_UnionI:   "Y \<in> Pow(TFin S) ==> Union(Y) \<in> TFin S"
    1.56 -           
    1.57    monos          Pow_mono
    1.58  
    1.59  
    1.60 @@ -54,26 +55,26 @@
    1.61  
    1.62  lemmas TFin_UnionI = TFin.Pow_UnionI [OF PowI]
    1.63  
    1.64 -lemma TFin_induct: 
    1.65 -          "[| n \<in> TFin S;  
    1.66 -             !!x. [| x \<in> TFin S; P(x) |] ==> P(succ S x);  
    1.67 -             !!Y. [| Y \<subseteq> TFin S; Ball Y P |] ==> P(Union Y) |]  
    1.68 +lemma TFin_induct:
    1.69 +          "[| n \<in> TFin S;
    1.70 +             !!x. [| x \<in> TFin S; P(x) |] ==> P(succ S x);
    1.71 +             !!Y. [| Y \<subseteq> TFin S; Ball Y P |] ==> P(Union Y) |]
    1.72            ==> P(n)"
    1.73  apply (erule TFin.induct, blast+)
    1.74  done
    1.75  
    1.76  lemma succ_trans: "x \<subseteq> y ==> x \<subseteq> succ S y"
    1.77 -apply (erule subset_trans) 
    1.78 -apply (rule Abrial_axiom1) 
    1.79 +apply (erule subset_trans)
    1.80 +apply (rule Abrial_axiom1)
    1.81  done
    1.82  
    1.83  text{*Lemma 1 of section 3.1*}
    1.84  lemma TFin_linear_lemma1:
    1.85 -     "[| n \<in> TFin S;  m \<in> TFin S;   
    1.86 -         \<forall>x \<in> TFin S. x \<subseteq> m --> x = m | succ S x \<subseteq> m  
    1.87 +     "[| n \<in> TFin S;  m \<in> TFin S;
    1.88 +         \<forall>x \<in> TFin S. x \<subseteq> m --> x = m | succ S x \<subseteq> m
    1.89        |] ==> n \<subseteq> m | succ S m \<subseteq> n"
    1.90  apply (erule TFin_induct)
    1.91 -apply (erule_tac [2] Union_lemma0) txt{*or just Blast_tac*}
    1.92 +apply (erule_tac [2] Union_lemma0) (*or just blast*)
    1.93  apply (blast del: subsetI intro: succ_trans)
    1.94  done
    1.95  
    1.96 @@ -82,20 +83,20 @@
    1.97       "m \<in> TFin S ==> \<forall>n \<in> TFin S. n \<subseteq> m --> n=m | succ S n \<subseteq> m"
    1.98  apply (erule TFin_induct)
    1.99  apply (rule impI [THEN ballI])
   1.100 -txt{*case split using TFin_linear_lemma1*}
   1.101 -apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE], 
   1.102 +txt{*case split using @{text TFin_linear_lemma1}*}
   1.103 +apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
   1.104         assumption+)
   1.105  apply (drule_tac x = n in bspec, assumption)
   1.106 -apply (blast del: subsetI intro: succ_trans, blast) 
   1.107 +apply (blast del: subsetI intro: succ_trans, blast)
   1.108  txt{*second induction step*}
   1.109  apply (rule impI [THEN ballI])
   1.110  apply (rule Union_lemma0 [THEN disjE])
   1.111  apply (rule_tac [3] disjI2)
   1.112 - prefer 2 apply blast 
   1.113 + prefer 2 apply blast
   1.114  apply (rule ballI)
   1.115 -apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE], 
   1.116 -       assumption+, auto) 
   1.117 -apply (blast intro!: Abrial_axiom1 [THEN subsetD])  
   1.118 +apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
   1.119 +       assumption+, auto)
   1.120 +apply (blast intro!: Abrial_axiom1 [THEN subsetD])
   1.121  done
   1.122  
   1.123  text{*Re-ordering the premises of Lemma 2*}
   1.124 @@ -107,10 +108,10 @@
   1.125  
   1.126  text{*Consequences from section 3.3 -- Property 3.2, the ordering is total*}
   1.127  lemma TFin_subset_linear: "[| m \<in> TFin S;  n \<in> TFin S|] ==> n \<subseteq> m | m \<subseteq> n"
   1.128 -apply (rule disjE) 
   1.129 +apply (rule disjE)
   1.130  apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2])
   1.131  apply (assumption+, erule disjI2)
   1.132 -apply (blast del: subsetI 
   1.133 +apply (blast del: subsetI
   1.134               intro: subsetI Abrial_axiom1 [THEN subset_trans])
   1.135  done
   1.136  
   1.137 @@ -130,12 +131,12 @@
   1.138  apply (erule ssubst)
   1.139  apply (rule Abrial_axiom1 [THEN equalityI])
   1.140  apply (blast del: subsetI
   1.141 -	     intro: subsetI TFin_UnionI TFin.succI)
   1.142 +             intro: subsetI TFin_UnionI TFin.succI)
   1.143  done
   1.144  
   1.145  subsection{*Hausdorff's Theorem: Every Set Contains a Maximal Chain.*}
   1.146  
   1.147 -text{*NB: We assume the partial ordering is @{text "\<subseteq>"}, 
   1.148 +text{*NB: We assume the partial ordering is @{text "\<subseteq>"},
   1.149   the subset relation!*}
   1.150  
   1.151  lemma empty_set_mem_chain: "({} :: 'a set set) \<in> chain S"
   1.152 @@ -150,13 +151,13 @@
   1.153  lemma mem_super_Ex: "c \<in> chain S - maxchain S ==> ? d. d \<in> super S c"
   1.154  by (unfold super_def maxchain_def, auto)
   1.155  
   1.156 -lemma select_super: "c \<in> chain S - maxchain S ==>  
   1.157 +lemma select_super: "c \<in> chain S - maxchain S ==>
   1.158                            (@c'. c': super S c): super S c"
   1.159  apply (erule mem_super_Ex [THEN exE])
   1.160  apply (rule someI2, auto)
   1.161  done
   1.162  
   1.163 -lemma select_not_equals: "c \<in> chain S - maxchain S ==>  
   1.164 +lemma select_not_equals: "c \<in> chain S - maxchain S ==>
   1.165                            (@c'. c': super S c) \<noteq> c"
   1.166  apply (rule notI)
   1.167  apply (drule select_super)
   1.168 @@ -180,26 +181,26 @@
   1.169  apply (unfold chain_def)
   1.170  apply (rule CollectI, safe)
   1.171  apply (drule bspec, assumption)
   1.172 -apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE], 
   1.173 +apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE],
   1.174         blast+)
   1.175  done
   1.176 - 
   1.177 +
   1.178  theorem Hausdorff: "\<exists>c. (c :: 'a set set): maxchain S"
   1.179  apply (rule_tac x = "Union (TFin S) " in exI)
   1.180  apply (rule classical)
   1.181  apply (subgoal_tac "succ S (Union (TFin S)) = Union (TFin S) ")
   1.182   prefer 2
   1.183 - apply (blast intro!: TFin_UnionI equal_succ_Union [THEN iffD2, symmetric]) 
   1.184 + apply (blast intro!: TFin_UnionI equal_succ_Union [THEN iffD2, symmetric])
   1.185  apply (cut_tac subset_refl [THEN TFin_UnionI, THEN TFin_chain_lemma4])
   1.186  apply (drule DiffI [THEN succ_not_equals], blast+)
   1.187  done
   1.188  
   1.189  
   1.190 -subsection{*Zorn's Lemma: If All Chains Have Upper Bounds Then 
   1.191 +subsection{*Zorn's Lemma: If All Chains Have Upper Bounds Then
   1.192                                 There Is  a Maximal Element*}
   1.193  
   1.194 -lemma chain_extend: 
   1.195 -    "[| c \<in> chain S; z \<in> S;  
   1.196 +lemma chain_extend:
   1.197 +    "[| c \<in> chain S; z \<in> S;
   1.198          \<forall>x \<in> c. x<=(z:: 'a set) |] ==> {z} Un c \<in> chain S"
   1.199  by (unfold chain_def, blast)
   1.200  
   1.201 @@ -237,16 +238,16 @@
   1.202       "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>x \<in> c. x \<subseteq> y
   1.203        ==> \<exists>y \<in> S. \<forall>x \<in> S. (y :: 'a set) \<subseteq> x --> y = x"
   1.204  apply (cut_tac Hausdorff maxchain_subset_chain)
   1.205 -apply (erule exE) 
   1.206 -apply (drule subsetD, assumption) 
   1.207 -apply (drule bspec, assumption, erule bexE) 
   1.208 +apply (erule exE)
   1.209 +apply (drule subsetD, assumption)
   1.210 +apply (drule bspec, assumption, erule bexE)
   1.211  apply (rule_tac x = y in bexI)
   1.212   prefer 2 apply assumption
   1.213 -apply clarify 
   1.214 -apply (rule ccontr) 
   1.215 +apply clarify
   1.216 +apply (rule ccontr)
   1.217  apply (frule_tac z = x in chain_extend)
   1.218  apply (assumption, blast)
   1.219 -apply (unfold maxchain_def super_def psubset_def) 
   1.220 +apply (unfold maxchain_def super_def psubset_def)
   1.221  apply (blast elim!: equalityCE)
   1.222  done
   1.223  
   1.224 @@ -259,4 +260,3 @@
   1.225  by (unfold chain_def, blast)
   1.226  
   1.227  end
   1.228 -