src/HOL/Library/Zorn.thy
changeset 13551 b7f64ee8da84
child 13652 172600c40793
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Zorn.thy	Sat Aug 31 14:03:49 2002 +0200
     1.3 @@ -0,0 +1,263 @@
     1.4 +(*  Title       \<in> Zorn.thy
     1.5 +    ID          \<in> $Id$
     1.6 +    Author      \<in> Jacques D. Fleuriot
     1.7 +    Copyright   \<in> 1998  University of Cambridge
     1.8 +    Description \<in> Zorn's Lemma -- See Larry Paulson's Zorn.thy in ZF
     1.9 +*) 
    1.10 +
    1.11 +header {*Zorn's Lemma*}
    1.12 +
    1.13 +theory Zorn = Main:
    1.14 +
    1.15 +text{*The lemma and section numbers refer to an unpublished article ``Towards
    1.16 +the Mechanization of the Proofs of Some Classical Theorems of Set Theory,'' by
    1.17 +Abrial and Laffitte.  *}
    1.18 +
    1.19 +constdefs
    1.20 +  chain     ::  "'a::ord set => 'a set set"
    1.21 +    "chain S  == {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}" 
    1.22 +
    1.23 +  super     ::  "['a::ord set,'a set] => 'a set set"
    1.24 +    "super S c == {d. d \<in> chain(S) & c < d}"
    1.25 +
    1.26 +  maxchain  ::  "'a::ord set => 'a set set"
    1.27 +    "maxchain S == {c. c \<in> chain S & super S c = {}}"
    1.28 +
    1.29 +  succ      ::  "['a::ord set,'a set] => 'a set"
    1.30 +    "succ S c == if (c \<notin> chain S| c \<in> maxchain S) 
    1.31 +                 then c else (@c'. c': (super S c))" 
    1.32 +
    1.33 +consts 
    1.34 +  "TFin" ::  "'a::ord set => 'a set set"
    1.35 +
    1.36 +inductive "TFin(S)"
    1.37 +  intros
    1.38 +    succI:        "x \<in> TFin S ==> succ S x \<in> TFin S"
    1.39 +    Pow_UnionI:   "Y \<in> Pow(TFin S) ==> Union(Y) \<in> TFin S"
    1.40 +           
    1.41 +  monos          Pow_mono
    1.42 +
    1.43 +
    1.44 +subsection{*Mathematical Preamble*}
    1.45 +
    1.46 +lemma Union_lemma0: "(\<forall>x \<in> C. x \<subseteq> A | B \<subseteq> x) ==> Union(C)<=A | B \<subseteq> Union(C)"
    1.47 +by blast
    1.48 +
    1.49 +
    1.50 +text{*This is theorem @{text increasingD2} of ZF/Zorn.thy*}
    1.51 +lemma Abrial_axiom1: "x \<subseteq> succ S x"
    1.52 +apply (unfold succ_def)
    1.53 +apply (rule split_if [THEN iffD2])
    1.54 +apply (auto simp add: super_def maxchain_def psubset_def)
    1.55 +apply (rule swap, assumption)
    1.56 +apply (rule someI2, blast+)
    1.57 +done
    1.58 +
    1.59 +lemmas TFin_UnionI = TFin.Pow_UnionI [OF PowI]
    1.60 +
    1.61 +lemma TFin_induct: 
    1.62 +          "[| n \<in> TFin S;  
    1.63 +             !!x. [| x \<in> TFin S; P(x) |] ==> P(succ S x);  
    1.64 +             !!Y. [| Y \<subseteq> TFin S; Ball Y P |] ==> P(Union Y) |]  
    1.65 +          ==> P(n)"
    1.66 +apply (erule TFin.induct, blast+)
    1.67 +done
    1.68 +
    1.69 +lemma succ_trans: "x \<subseteq> y ==> x \<subseteq> succ S y"
    1.70 +apply (erule subset_trans) 
    1.71 +apply (rule Abrial_axiom1) 
    1.72 +done
    1.73 +
    1.74 +text{*Lemma 1 of section 3.1*}
    1.75 +lemma TFin_linear_lemma1:
    1.76 +     "[| n \<in> TFin S;  m \<in> TFin S;   
    1.77 +         \<forall>x \<in> TFin S. x \<subseteq> m --> x = m | succ S x \<subseteq> m  
    1.78 +      |] ==> n \<subseteq> m | succ S m \<subseteq> n"
    1.79 +apply (erule TFin_induct)
    1.80 +apply (erule_tac [2] Union_lemma0) txt{*or just Blast_tac*}
    1.81 +apply (blast del: subsetI intro: succ_trans)
    1.82 +done
    1.83 +
    1.84 +text{* Lemma 2 of section 3.2 *}
    1.85 +lemma TFin_linear_lemma2:
    1.86 +     "m \<in> TFin S ==> \<forall>n \<in> TFin S. n \<subseteq> m --> n=m | succ S n \<subseteq> m"
    1.87 +apply (erule TFin_induct)
    1.88 +apply (rule impI [THEN ballI])
    1.89 +txt{*case split using TFin_linear_lemma1*}
    1.90 +apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE], 
    1.91 +       assumption+)
    1.92 +apply (drule_tac x = n in bspec, assumption)
    1.93 +apply (blast del: subsetI intro: succ_trans, blast) 
    1.94 +txt{*second induction step*}
    1.95 +apply (rule impI [THEN ballI])
    1.96 +apply (rule Union_lemma0 [THEN disjE])
    1.97 +apply (rule_tac [3] disjI2)
    1.98 + prefer 2 apply blast 
    1.99 +apply (rule ballI)
   1.100 +apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE], 
   1.101 +       assumption+, auto) 
   1.102 +apply (blast intro!: Abrial_axiom1 [THEN subsetD])  
   1.103 +done
   1.104 +
   1.105 +text{*Re-ordering the premises of Lemma 2*}
   1.106 +lemma TFin_subsetD:
   1.107 +     "[| n \<subseteq> m;  m \<in> TFin S;  n \<in> TFin S |] ==> n=m | succ S n \<subseteq> m"
   1.108 +apply (rule TFin_linear_lemma2 [rule_format])
   1.109 +apply (assumption+)
   1.110 +done
   1.111 +
   1.112 +text{*Consequences from section 3.3 -- Property 3.2, the ordering is total*}
   1.113 +lemma TFin_subset_linear: "[| m \<in> TFin S;  n \<in> TFin S|] ==> n \<subseteq> m | m \<subseteq> n"
   1.114 +apply (rule disjE) 
   1.115 +apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2])
   1.116 +apply (assumption+, erule disjI2)
   1.117 +apply (blast del: subsetI 
   1.118 +             intro: subsetI Abrial_axiom1 [THEN subset_trans])
   1.119 +done
   1.120 +
   1.121 +text{*Lemma 3 of section 3.3*}
   1.122 +lemma eq_succ_upper: "[| n \<in> TFin S;  m \<in> TFin S;  m = succ S m |] ==> n \<subseteq> m"
   1.123 +apply (erule TFin_induct)
   1.124 +apply (drule TFin_subsetD)
   1.125 +apply (assumption+, force, blast)
   1.126 +done
   1.127 +
   1.128 +text{*Property 3.3 of section 3.3*}
   1.129 +lemma equal_succ_Union: "m \<in> TFin S ==> (m = succ S m) = (m = Union(TFin S))"
   1.130 +apply (rule iffI)
   1.131 +apply (rule Union_upper [THEN equalityI])
   1.132 +apply (rule_tac [2] eq_succ_upper [THEN Union_least])
   1.133 +apply (assumption+)
   1.134 +apply (erule ssubst)
   1.135 +apply (rule Abrial_axiom1 [THEN equalityI])
   1.136 +apply (blast del: subsetI
   1.137 +	     intro: subsetI TFin_UnionI TFin.succI)
   1.138 +done
   1.139 +
   1.140 +subsection{*Hausdorff's Theorem: Every Set Contains a Maximal Chain.*}
   1.141 +
   1.142 +text{*NB: We assume the partial ordering is @{text "\<subseteq>"}, 
   1.143 + the subset relation!*}
   1.144 +
   1.145 +lemma empty_set_mem_chain: "({} :: 'a set set) \<in> chain S"
   1.146 +by (unfold chain_def, auto)
   1.147 +
   1.148 +lemma super_subset_chain: "super S c \<subseteq> chain S"
   1.149 +by (unfold super_def, fast)
   1.150 +
   1.151 +lemma maxchain_subset_chain: "maxchain S \<subseteq> chain S"
   1.152 +by (unfold maxchain_def, fast)
   1.153 +
   1.154 +lemma mem_super_Ex: "c \<in> chain S - maxchain S ==> ? d. d \<in> super S c"
   1.155 +by (unfold super_def maxchain_def, auto)
   1.156 +
   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 +                          (@c'. c': super S c) \<noteq> c"
   1.165 +apply (rule notI)
   1.166 +apply (drule select_super)
   1.167 +apply (simp add: super_def psubset_def)
   1.168 +done
   1.169 +
   1.170 +lemma succI3: "c \<in> chain S - maxchain S ==> succ S c = (@c'. c': super S c)"
   1.171 +apply (unfold succ_def)
   1.172 +apply (fast intro!: if_not_P)
   1.173 +done
   1.174 +
   1.175 +lemma succ_not_equals: "c \<in> chain S - maxchain S ==> succ S c \<noteq> c"
   1.176 +apply (frule succI3)
   1.177 +apply (simp (no_asm_simp))
   1.178 +apply (rule select_not_equals, assumption)
   1.179 +done
   1.180 +
   1.181 +lemma TFin_chain_lemma4: "c \<in> TFin S ==> (c :: 'a set set): chain S"
   1.182 +apply (erule TFin_induct)
   1.183 +apply (simp add: succ_def select_super [THEN super_subset_chain[THEN subsetD]])
   1.184 +apply (unfold chain_def)
   1.185 +apply (rule CollectI, safe)
   1.186 +apply (drule bspec, assumption)
   1.187 +apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE], 
   1.188 +       blast+)
   1.189 +done
   1.190 + 
   1.191 +theorem Hausdorff: "\<exists>c. (c :: 'a set set): maxchain S"
   1.192 +apply (rule_tac x = "Union (TFin S) " in exI)
   1.193 +apply (rule classical)
   1.194 +apply (subgoal_tac "succ S (Union (TFin S)) = Union (TFin S) ")
   1.195 + prefer 2
   1.196 + apply (blast intro!: TFin_UnionI equal_succ_Union [THEN iffD2, symmetric]) 
   1.197 +apply (cut_tac subset_refl [THEN TFin_UnionI, THEN TFin_chain_lemma4])
   1.198 +apply (drule DiffI [THEN succ_not_equals], blast+)
   1.199 +done
   1.200 +
   1.201 +
   1.202 +subsection{*Zorn's Lemma: If All Chains Have Upper Bounds Then 
   1.203 +                               There Is  a Maximal Element*}
   1.204 +
   1.205 +lemma chain_extend: 
   1.206 +    "[| c \<in> chain S; z \<in> S;  
   1.207 +        \<forall>x \<in> c. x<=(z:: 'a set) |] ==> {z} Un c \<in> chain S"
   1.208 +by (unfold chain_def, blast)
   1.209 +
   1.210 +lemma chain_Union_upper: "[| c \<in> chain S; x \<in> c |] ==> x \<subseteq> Union(c)"
   1.211 +by (unfold chain_def, auto)
   1.212 +
   1.213 +lemma chain_ball_Union_upper: "c \<in> chain S ==> \<forall>x \<in> c. x \<subseteq> Union(c)"
   1.214 +by (unfold chain_def, auto)
   1.215 +
   1.216 +lemma maxchain_Zorn:
   1.217 +     "[| c \<in> maxchain S; u \<in> S; Union(c) \<subseteq> u |] ==> Union(c) = u"
   1.218 +apply (rule ccontr)
   1.219 +apply (simp add: maxchain_def)
   1.220 +apply (erule conjE)
   1.221 +apply (subgoal_tac " ({u} Un c) \<in> super S c")
   1.222 +apply simp
   1.223 +apply (unfold super_def psubset_def)
   1.224 +apply (blast intro: chain_extend dest: chain_Union_upper)
   1.225 +done
   1.226 +
   1.227 +theorem Zorn_Lemma:
   1.228 +     "\<forall>c \<in> chain S. Union(c): S ==> \<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z --> y = z"
   1.229 +apply (cut_tac Hausdorff maxchain_subset_chain)
   1.230 +apply (erule exE)
   1.231 +apply (drule subsetD, assumption)
   1.232 +apply (drule bspec, assumption)
   1.233 +apply (rule_tac x = "Union (c) " in bexI)
   1.234 +apply (rule ballI, rule impI)
   1.235 +apply (blast dest!: maxchain_Zorn, assumption)
   1.236 +done
   1.237 +
   1.238 +subsection{*Alternative version of Zorn's Lemma*}
   1.239 +
   1.240 +lemma Zorn_Lemma2:
   1.241 +     "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>x \<in> c. x \<subseteq> y
   1.242 +      ==> \<exists>y \<in> S. \<forall>x \<in> S. (y :: 'a set) \<subseteq> x --> y = x"
   1.243 +apply (cut_tac Hausdorff maxchain_subset_chain)
   1.244 +apply (erule exE) 
   1.245 +apply (drule subsetD, assumption) 
   1.246 +apply (drule bspec, assumption, erule bexE) 
   1.247 +apply (rule_tac x = y in bexI)
   1.248 + prefer 2 apply assumption
   1.249 +apply clarify 
   1.250 +apply (rule ccontr) 
   1.251 +apply (frule_tac z = x in chain_extend)
   1.252 +apply (assumption, blast)
   1.253 +apply (unfold maxchain_def super_def psubset_def) 
   1.254 +apply (blast elim!: equalityCE)
   1.255 +done
   1.256 +
   1.257 +text{*Various other lemmas*}
   1.258 +
   1.259 +lemma chainD: "[| c \<in> chain S; x \<in> c; y \<in> c |] ==> x \<subseteq> y | y \<subseteq> x"
   1.260 +by (unfold chain_def, blast)
   1.261 +
   1.262 +lemma chainD2: "!!(c :: 'a set set). c \<in> chain S ==> c \<subseteq> S"
   1.263 +by (unfold chain_def, blast)
   1.264 +
   1.265 +end
   1.266 +