Addition of Hyperreal theories Zorn and Filter
authorpaulson
Fri Nov 27 11:24:27 1998 +0100 (1998-11-27)
changeset 597911cbf236ca16
parent 5978 fa2c2dd74f8c
child 5980 2e9314c07146
Addition of Hyperreal theories Zorn and Filter
src/HOL/Real/Hyperreal/Filter.ML
src/HOL/Real/Hyperreal/Filter.thy
src/HOL/Real/Hyperreal/README.html
src/HOL/Real/Hyperreal/ROOT.ML
src/HOL/Real/Hyperreal/Zorn.ML
src/HOL/Real/Hyperreal/Zorn.thy
src/HOL/Real/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Real/Hyperreal/Filter.ML	Fri Nov 27 11:24:27 1998 +0100
     1.3 @@ -0,0 +1,557 @@
     1.4 +(*  Title       : Filter.ML
     1.5 +    Author      : Jacques D. Fleuriot
     1.6 +    Copyright   : 1998  University of Cambridge
     1.7 +    Description : Filters and Ultrafilter
     1.8 +*) 
     1.9 +
    1.10 +open Filter;
    1.11 +
    1.12 +
    1.13 +(*------------------------------------------------------------------
    1.14 +      Properties of Filters and Freefilters - 
    1.15 +      rules for intro, destruction etc.
    1.16 + ------------------------------------------------------------------*)
    1.17 +
    1.18 +Goalw [is_Filter_def] "is_Filter X S ==> X <= Pow(S)";
    1.19 +by (Blast_tac 1);
    1.20 +qed "is_FilterD1";
    1.21 +
    1.22 +Goalw [is_Filter_def] "is_Filter X S ==> X ~= {}";
    1.23 +by (Blast_tac 1);
    1.24 +qed "is_FilterD2";
    1.25 +
    1.26 +Goalw [is_Filter_def] "is_Filter X S ==> {} ~: X";
    1.27 +by (Blast_tac 1);
    1.28 +qed "is_FilterD3";
    1.29 +
    1.30 +Goalw [Filter_def] "is_Filter X S ==> X : Filter S";
    1.31 +by (Blast_tac 1);
    1.32 +qed "mem_FiltersetI";
    1.33 +
    1.34 +Goalw [Filter_def] "X : Filter S ==> is_Filter X S";
    1.35 +by (Blast_tac 1);
    1.36 +qed "mem_FiltersetD";
    1.37 +
    1.38 +Goal "X : Filter S ==> {} ~: X";
    1.39 +by (etac (mem_FiltersetD RS is_FilterD3) 1);
    1.40 +qed "Filter_empty_not_mem";
    1.41 +
    1.42 +bind_thm ("Filter_empty_not_memE",(Filter_empty_not_mem RS notE));
    1.43 +
    1.44 +Goalw [Filter_def,is_Filter_def] 
    1.45 +      "[| X: Filter S; A: X; B: X |] ==> A Int B : X";
    1.46 +by (Blast_tac 1);
    1.47 +qed "mem_FiltersetD1";
    1.48 +
    1.49 +Goalw [Filter_def,is_Filter_def] 
    1.50 +      "[| X: Filter S; A: X; A <= B; B <= S|] ==> B : X";
    1.51 +by (Blast_tac 1);
    1.52 +qed "mem_FiltersetD2";
    1.53 +
    1.54 +Goalw [Filter_def,is_Filter_def] 
    1.55 +      "[| X: Filter S; A: X |] ==> A : Pow S";
    1.56 +by (Blast_tac 1);
    1.57 +qed "mem_FiltersetD3";
    1.58 +
    1.59 +Goalw [Filter_def,is_Filter_def] 
    1.60 +      "X: Filter S  ==> S : X";
    1.61 +by (Blast_tac 1);
    1.62 +qed "mem_FiltersetD4";
    1.63 +
    1.64 +Goalw [is_Filter_def] 
    1.65 +      "[| X <= Pow(S);\
    1.66 +\              S : X; \
    1.67 +\              X ~= {}; \
    1.68 +\              {} ~: X; \
    1.69 +\              ALL u: X. ALL v: X. u Int v : X; \
    1.70 +\              ALL u v. u: X & u<=v & v<=S --> v: X \
    1.71 +\           |] ==> is_Filter X S";
    1.72 +by (Blast_tac 1); 
    1.73 +qed "is_FilterI";
    1.74 +
    1.75 +Goal "[| X <= Pow(S);\
    1.76 +\              S : X; \
    1.77 +\              X ~= {}; \
    1.78 +\              {} ~: X; \
    1.79 +\              ALL u: X. ALL v: X. u Int v : X; \
    1.80 +\              ALL u v. u: X & u<=v & v<=S --> v: X \
    1.81 +\           |] ==> X: Filter S";
    1.82 +by (blast_tac (claset() addIs [mem_FiltersetI,is_FilterI]) 1);
    1.83 +qed "mem_FiltersetI2";
    1.84 +
    1.85 +Goalw [is_Filter_def]
    1.86 +      "is_Filter X S ==> X <= Pow(S) & \
    1.87 +\                          S : X & \
    1.88 +\                          X ~= {} & \
    1.89 +\                          {} ~: X  & \
    1.90 +\                          (ALL u: X. ALL v: X. u Int v : X) & \
    1.91 +\                          (ALL u v. u: X & u <= v & v<=S --> v: X)";
    1.92 +by (Fast_tac 1);
    1.93 +qed "is_FilterE_lemma";
    1.94 +
    1.95 +Goalw [is_Filter_def]
    1.96 +      "X : Filter S ==> X <= Pow(S) &\
    1.97 +\                          S : X & \
    1.98 +\                          X ~= {} & \
    1.99 +\                          {} ~: X  & \
   1.100 +\                          (ALL u: X. ALL v: X. u Int v : X) & \
   1.101 +\                          (ALL u v. u: X & u <= v & v<=S --> v: X)";
   1.102 +by (etac (mem_FiltersetD RS is_FilterE_lemma) 1);
   1.103 +qed "memFiltersetE_lemma";
   1.104 +
   1.105 +Goalw [Filter_def,Freefilter_def] 
   1.106 +      "X: Freefilter S ==> X: Filter S";
   1.107 +by (Fast_tac 1);
   1.108 +qed "Freefilter_Filter";
   1.109 +
   1.110 +Goalw [Freefilter_def] 
   1.111 +      "X: Freefilter S ==> ALL y: X. ~finite(y)";
   1.112 +by (Blast_tac 1);
   1.113 +qed "mem_Freefilter_not_finite";
   1.114 +
   1.115 +Goal "[| X: Freefilter S; x: X |] ==> ~ finite x";
   1.116 +by (blast_tac (claset() addSDs [mem_Freefilter_not_finite]) 1);
   1.117 +qed "mem_FreefiltersetD1";
   1.118 +
   1.119 +bind_thm ("mem_FreefiltersetE1", (mem_FreefiltersetD1 RS notE));
   1.120 +
   1.121 +Goal "[| X: Freefilter S; finite x|] ==> x ~: X";
   1.122 +by (blast_tac (claset() addSDs [mem_Freefilter_not_finite]) 1);
   1.123 +qed "mem_FreefiltersetD2";
   1.124 +
   1.125 +Goalw [Freefilter_def] 
   1.126 +      "[| X: Filter S; ALL x. ~(x: X & finite x) |] ==> X: Freefilter S";
   1.127 +by (Blast_tac 1);
   1.128 +qed "mem_FreefiltersetI1";
   1.129 +
   1.130 +Goalw [Freefilter_def]
   1.131 +      "[| X: Filter S; ALL x. (x ~: X | ~ finite x) |] ==> X: Freefilter S";
   1.132 +by (Blast_tac 1);
   1.133 +qed "mem_FreefiltersetI2";
   1.134 +
   1.135 +Goal "[| X: Filter S; A: X; B: X |] ==> A Int B ~= {}";
   1.136 +by (forw_inst_tac [("A","A"),("B","B")] mem_FiltersetD1 1);
   1.137 +by (auto_tac (claset() addSDs [Filter_empty_not_mem],simpset()));
   1.138 +qed "Filter_Int_not_empty";
   1.139 +
   1.140 +bind_thm ("Filter_Int_not_emptyE",(Filter_Int_not_empty RS notE));
   1.141 +
   1.142 +(*----------------------------------------------------------------------------------
   1.143 +              Ultrafilters and Free ultrafilters
   1.144 + ----------------------------------------------------------------------------------*)
   1.145 +
   1.146 +Goalw [Ultrafilter_def] "X : Ultrafilter S ==> X: Filter S";
   1.147 +by (Blast_tac 1);
   1.148 +qed "Ultrafilter_Filter";
   1.149 +
   1.150 +Goalw [Ultrafilter_def] 
   1.151 +      "X : Ultrafilter S ==> !A: Pow(S). A : X | S - A: X";
   1.152 +by (Blast_tac 1);
   1.153 +qed "mem_UltrafiltersetD2";
   1.154 +
   1.155 +Goalw [Ultrafilter_def] 
   1.156 +      "[|X : Ultrafilter S; A <= S; A ~: X |] ==> S - A: X";
   1.157 +by (Blast_tac 1);
   1.158 +qed "mem_UltrafiltersetD3";
   1.159 +
   1.160 +Goalw [Ultrafilter_def] 
   1.161 +      "[|X : Ultrafilter S; A <= S; S - A ~: X |] ==> A: X";
   1.162 +by (Blast_tac 1);
   1.163 +qed "mem_UltrafiltersetD4";
   1.164 +
   1.165 +Goalw [Ultrafilter_def]
   1.166 +     "[| X: Filter S; \
   1.167 +\             ALL A: Pow(S). A: X | S - A : X |] ==> X: Ultrafilter S";
   1.168 +by (Blast_tac 1);
   1.169 +qed "mem_UltrafiltersetI";
   1.170 +
   1.171 +Goalw [Ultrafilter_def,FreeUltrafilter_def]
   1.172 +     "X: FreeUltrafilter S ==> X: Ultrafilter S";
   1.173 +by (Blast_tac 1);
   1.174 +qed "FreeUltrafilter_Ultrafilter";
   1.175 +
   1.176 +Goalw [FreeUltrafilter_def]
   1.177 +     "X: FreeUltrafilter S ==> ALL y: X. ~finite(y)";
   1.178 +by (Blast_tac 1);
   1.179 +qed "mem_FreeUltrafilter_not_finite";
   1.180 +
   1.181 +Goal "[| X: FreeUltrafilter S; x: X |] ==> ~ finite x";
   1.182 +by (blast_tac (claset() addSDs [mem_FreeUltrafilter_not_finite]) 1);
   1.183 +qed "mem_FreeUltrafiltersetD1";
   1.184 +
   1.185 +bind_thm ("mem_FreeUltrafiltersetE1", (mem_FreeUltrafiltersetD1 RS notE));
   1.186 +
   1.187 +Goal "[| X: FreeUltrafilter S; finite x|] ==> x ~: X";
   1.188 +by (blast_tac (claset() addSDs [mem_FreeUltrafilter_not_finite]) 1);
   1.189 +qed "mem_FreeUltrafiltersetD2";
   1.190 +
   1.191 +Goalw [FreeUltrafilter_def] 
   1.192 +      "[| X: Ultrafilter S; \
   1.193 +\              ALL x. ~(x: X & finite x) |] ==> X: FreeUltrafilter S";
   1.194 +by (Blast_tac 1);
   1.195 +qed "mem_FreeUltrafiltersetI1";
   1.196 +
   1.197 +Goalw [FreeUltrafilter_def]
   1.198 +      "[| X: Ultrafilter S; \
   1.199 +\              ALL x. (x ~: X | ~ finite x) |] ==> X: FreeUltrafilter S";
   1.200 +by (Blast_tac 1);
   1.201 +qed "mem_FreeUltrafiltersetI2";
   1.202 +
   1.203 +Goalw [FreeUltrafilter_def,Freefilter_def,Ultrafilter_def]
   1.204 +     "(X: FreeUltrafilter S) = (X: Freefilter S & (ALL x:Pow(S). x: X | S - x: X))";
   1.205 +by (Blast_tac 1);
   1.206 +qed "FreeUltrafilter_iff";
   1.207 +
   1.208 +(*-------------------------------------------------------------------
   1.209 +   A Filter F on S is an ultrafilter iff it is a maximal filter 
   1.210 +   i.e. whenever G is a filter on I and F <= F then F = G
   1.211 + --------------------------------------------------------------------*)
   1.212 +(*---------------------------------------------------------------------
   1.213 +  lemmas that shows existence of an extension to what was assumed to
   1.214 +  be a maximal filter. Will be used to derive contradiction in proof of
   1.215 +  property of ultrafilter 
   1.216 + ---------------------------------------------------------------------*)
   1.217 +Goal "[| F ~= {}; A <= S |] ==> \
   1.218 +\        EX x. x: {X. X <= S & (EX f:F. A Int f <= X)}";
   1.219 +by (Blast_tac 1);
   1.220 +qed "lemma_set_extend";
   1.221 +
   1.222 +Goal "a: X ==> X ~= {}";
   1.223 +by (Step_tac 1);
   1.224 +qed "lemma_set_not_empty";
   1.225 +
   1.226 +Goal "x Int F <= {} ==> F <= - x";
   1.227 +by (Blast_tac 1);
   1.228 +qed "lemma_empty_Int_subset_Compl";
   1.229 +
   1.230 +Goalw [Filter_def,is_Filter_def]
   1.231 +      "[| F: Filter S; A ~: F; A <= S|] \
   1.232 +\          ==> ALL B. B ~: F | ~ B <= A";
   1.233 +by (Blast_tac 1);
   1.234 +qed "mem_Filterset_disjI";
   1.235 +
   1.236 +Goal "F : Ultrafilter S ==> \
   1.237 +\         (F: Filter S & (ALL G: Filter S. F <= G --> F = G))";
   1.238 +by (auto_tac (claset(),simpset() addsimps [Ultrafilter_def]));
   1.239 +by (dres_inst_tac [("x","x")] bspec 1);
   1.240 +by (etac mem_FiltersetD3 1 THEN assume_tac 1);
   1.241 +by (Step_tac 1);
   1.242 +by (dtac subsetD 1 THEN assume_tac 1);
   1.243 +by (blast_tac (claset() addSDs [Filter_Int_not_empty]) 1);
   1.244 +qed "Ultrafilter_max_Filter";
   1.245 +
   1.246 +
   1.247 +(*--------------------------------------------------------------------------------
   1.248 +     This is a very long and tedious proof; need to break it into parts.
   1.249 +     Have proof that {X. X <= S & (EX f: F. A Int f <= X)} is a filter as 
   1.250 +     a lemma
   1.251 +--------------------------------------------------------------------------------*)
   1.252 +Goalw [Ultrafilter_def] 
   1.253 +      "[| F: Filter S; \
   1.254 +\              ALL G: Filter S. F <= G --> F = G |] ==> F : Ultrafilter S";
   1.255 +by (Step_tac 1);
   1.256 +by (rtac ccontr 1);
   1.257 +by (forward_tac [mem_FiltersetD RS is_FilterD2] 1);
   1.258 +by (forw_inst_tac [("x","{X. X <= S & (EX f: F. A Int f <= X)}")] bspec 1);
   1.259 +by (EVERY1[rtac mem_FiltersetI2, Blast_tac, Asm_full_simp_tac]);
   1.260 +by (blast_tac (claset() addDs [mem_FiltersetD3]) 1);
   1.261 +by (etac (lemma_set_extend RS exE) 1);
   1.262 +by (assume_tac 1 THEN etac lemma_set_not_empty 1);
   1.263 +by (REPEAT(rtac ballI 2) THEN Asm_full_simp_tac 2);
   1.264 +by (rtac conjI 2 THEN Blast_tac 2);
   1.265 +by (REPEAT(etac conjE 2) THEN REPEAT(etac bexE 2));
   1.266 +by (res_inst_tac [("x","f Int fa")] bexI 2);
   1.267 +by (etac mem_FiltersetD1 3);
   1.268 +by (assume_tac 3 THEN assume_tac 3);
   1.269 +by (Fast_tac 2);
   1.270 +by (EVERY[REPEAT(rtac allI 2), rtac impI 2,Asm_full_simp_tac 2]);
   1.271 +by (EVERY[REPEAT(etac conjE 2), etac bexE 2]);
   1.272 +by (res_inst_tac [("x","f")] bexI 2);
   1.273 +by (rtac subsetI 2);
   1.274 +by (Fast_tac 2 THEN assume_tac 2);
   1.275 +by (Step_tac 2);
   1.276 +by (Blast_tac 3);
   1.277 +by (eres_inst_tac [("c","A")] equalityCE 3);
   1.278 +by (REPEAT(Blast_tac 3));
   1.279 +by (dres_inst_tac [("A","xa")] mem_FiltersetD3 2 THEN assume_tac 2);
   1.280 +by (Blast_tac 2);
   1.281 +by (dtac lemma_empty_Int_subset_Compl 1);
   1.282 +by (EVERY1[forward_tac [mem_Filterset_disjI], assume_tac, Fast_tac]);
   1.283 +by (dtac mem_FiltersetD3 1 THEN assume_tac 1);
   1.284 +by (dres_inst_tac [("x","f")] spec 1);
   1.285 +by (Blast_tac 1);
   1.286 +qed "max_Filter_Ultrafilter";
   1.287 +
   1.288 +Goal "(F : Ultrafilter S) = (F: Filter S & (ALL G: Filter S. F <= G --> F = G))";
   1.289 +by (blast_tac (claset() addSIs [Ultrafilter_max_Filter,max_Filter_Ultrafilter]) 1);
   1.290 +qed "Ultrafilter_iff";
   1.291 +
   1.292 +(*--------------------------------------------------------------------
   1.293 +             A few properties of freefilters
   1.294 + -------------------------------------------------------------------*)
   1.295 +
   1.296 +Goal "F1 Int F2 = ((F1 Int Y) Int F2) Un ((F2 Int - Y) Int F1)";
   1.297 +by (Auto_tac);
   1.298 +qed "lemma_Compl_cancel_eq";
   1.299 +
   1.300 +Goal "finite X ==> finite (X Int Y)";
   1.301 +by (etac (Int_lower1 RS finite_subset) 1);
   1.302 +qed "finite_IntI1";
   1.303 +
   1.304 +Goal "finite Y ==> finite (X Int Y)";
   1.305 +by (etac (Int_lower2 RS finite_subset) 1);
   1.306 +qed "finite_IntI2";
   1.307 +
   1.308 +Goal "[| finite (F1 Int Y); \
   1.309 +\                 finite (F2 Int - Y) \
   1.310 +\              |] ==> finite (F1 Int F2)";
   1.311 +by (res_inst_tac [("Y1","Y")] (lemma_Compl_cancel_eq RS ssubst) 1);
   1.312 +by (rtac finite_UnI 1);
   1.313 +by (auto_tac (claset() addSIs [finite_IntI1,finite_IntI2],simpset()));
   1.314 +qed "finite_Int_Compl_cancel";
   1.315 +
   1.316 +Goal "U: Freefilter S  ==> \
   1.317 +\         ~ (EX f1: U. EX f2: U. finite (f1 Int x) \
   1.318 +\                            & finite (f2 Int (- x)))";
   1.319 +by (Step_tac 1);
   1.320 +by (forw_inst_tac [("A","f1"),("B","f2")] 
   1.321 +    (Freefilter_Filter RS mem_FiltersetD1) 1);
   1.322 +by (dres_inst_tac [("x","f1 Int f2")] mem_FreefiltersetD1 3);
   1.323 +by (dtac finite_Int_Compl_cancel 4);
   1.324 +by (Auto_tac);
   1.325 +qed "Freefilter_lemma_not_finite";
   1.326 +
   1.327 +(* the lemmas below follow *)
   1.328 +Goal "U: Freefilter S ==> \
   1.329 +\          ALL f: U. ~ finite (f Int x) | ~finite (f Int (- x))";
   1.330 +by (blast_tac (claset() addSDs [Freefilter_lemma_not_finite,bspec]) 1);
   1.331 +qed "Freefilter_Compl_not_finite_disjI";
   1.332 +
   1.333 +Goal "U: Freefilter S ==> \
   1.334 +\          (ALL f: U. ~ finite (f Int x)) | (ALL f:U. ~finite (f Int (- x)))";
   1.335 +by (blast_tac (claset() addSDs [Freefilter_lemma_not_finite,bspec]) 1);
   1.336 +qed "Freefilter_Compl_not_finite_disjI2";
   1.337 +
   1.338 +Goal "- UNIV = {}";
   1.339 +by (Auto_tac );
   1.340 +qed "Compl_UNIV_eq";
   1.341 +
   1.342 +Addsimps [Compl_UNIV_eq];
   1.343 +
   1.344 +Goal "- {} = UNIV";
   1.345 +by (Auto_tac );
   1.346 +qed "Compl_empty_eq";
   1.347 +
   1.348 +Addsimps [Compl_empty_eq];
   1.349 +
   1.350 +val [prem] = goal thy "~ finite (UNIV:: 'a set) ==> \
   1.351 +\            {A:: 'a set. finite (- A)} : Filter UNIV";
   1.352 +by (cut_facts_tac [prem] 1);
   1.353 +by (rtac mem_FiltersetI2 1);
   1.354 +by (auto_tac (claset(),simpset() addsimps [Compl_Int]));
   1.355 +by (eres_inst_tac [("c","UNIV")] equalityCE 1);
   1.356 +by (Auto_tac);
   1.357 +by (etac (Compl_anti_mono RS finite_subset) 1);
   1.358 +by (assume_tac 1);
   1.359 +qed "cofinite_Filter";
   1.360 +
   1.361 +Goal "~finite(UNIV :: 'a set) ==> ~finite (X :: 'a set) | ~finite (- X)";
   1.362 +by (dres_inst_tac [("A1","X")] (Compl_partition RS ssubst) 1);
   1.363 +by (Asm_full_simp_tac 1); 
   1.364 +qed "not_finite_UNIV_disjI";
   1.365 +
   1.366 +Goal "[| ~finite(UNIV :: 'a set); \
   1.367 +\                 finite (X :: 'a set) \
   1.368 +\              |] ==>  ~finite (- X)";
   1.369 +by (dres_inst_tac [("X","X")] not_finite_UNIV_disjI 1);
   1.370 +by (Blast_tac 1);
   1.371 +qed "not_finite_UNIV_Compl";
   1.372 +
   1.373 +val [prem] = goal thy "~ finite (UNIV:: 'a set) ==> \
   1.374 +\            !X: {A:: 'a set. finite (- A)}. ~ finite X";
   1.375 +by (cut_facts_tac [prem] 1);
   1.376 +by (auto_tac (claset() addDs [not_finite_UNIV_disjI],simpset()));
   1.377 +qed "mem_cofinite_Filter_not_finite";
   1.378 +
   1.379 +val [prem] = goal thy "~ finite (UNIV:: 'a set) ==> \
   1.380 +\            {A:: 'a set. finite (- A)} : Freefilter UNIV";
   1.381 +by (cut_facts_tac [prem] 1);
   1.382 +by (rtac mem_FreefiltersetI2 1);
   1.383 +by (rtac cofinite_Filter 1 THEN assume_tac 1);
   1.384 +by (blast_tac (claset() addSDs [mem_cofinite_Filter_not_finite]) 1);
   1.385 +qed "cofinite_Freefilter";
   1.386 +
   1.387 +Goal "UNIV - x = - x";
   1.388 +by (Auto_tac);
   1.389 +qed "UNIV_diff_Compl";
   1.390 +Addsimps [UNIV_diff_Compl];
   1.391 +
   1.392 +Goalw [Ultrafilter_def,FreeUltrafilter_def]
   1.393 +     "[| ~finite(UNIV :: 'a set); (U :: 'a set set): FreeUltrafilter UNIV\
   1.394 +\         |] ==> {X. finite(- X)} <= U";
   1.395 +by (forward_tac [cofinite_Filter] 1);
   1.396 +by (Step_tac 1);
   1.397 +by (forw_inst_tac [("X","- x :: 'a set")] not_finite_UNIV_Compl 1);
   1.398 +by (assume_tac 1);
   1.399 +by (Step_tac 1 THEN Fast_tac 1);
   1.400 +by (dres_inst_tac [("x","x")] bspec 1);
   1.401 +by (Blast_tac 1);
   1.402 +by (asm_full_simp_tac (simpset() addsimps [UNIV_diff_Compl]) 1);
   1.403 +qed "FreeUltrafilter_contains_cofinite_set";
   1.404 +
   1.405 +(*--------------------------------------------------------------------
   1.406 +   We prove: 1. Existence of maximal filter i.e. ultrafilter
   1.407 +             2. Freeness property i.e ultrafilter is free
   1.408 +             Use a locale to prove various lemmas and then 
   1.409 +             export main result- The Ultrafilter Theorem
   1.410 + -------------------------------------------------------------------*)
   1.411 +Open_locale "UFT"; 
   1.412 +
   1.413 +Goalw [chain_def, thm "superfrechet_def", thm "frechet_def"]
   1.414 +   "!!(c :: 'a set set set). c : chain (superfrechet S) ==>  Union c <= Pow S";
   1.415 +by (Step_tac 1);
   1.416 +by (dtac subsetD 1 THEN assume_tac 1);
   1.417 +by (Step_tac 1);
   1.418 +by (dres_inst_tac [("X","X")] mem_FiltersetD3 1);
   1.419 +by (Auto_tac);
   1.420 +qed "chain_Un_subset_Pow";
   1.421 +
   1.422 +Goalw [chain_def,Filter_def,is_Filter_def,
   1.423 +           thm "superfrechet_def", thm "frechet_def"] 
   1.424 +          "!!(c :: 'a set set set). c: chain (superfrechet S) \
   1.425 +\         ==> !x: c. {} < x";
   1.426 +by (blast_tac (claset() addSIs [psubsetI]) 1);
   1.427 +qed "mem_chain_psubset_empty";
   1.428 +
   1.429 +Goal "!!(c :: 'a set set set). \
   1.430 +\            [| c: chain (superfrechet S);\
   1.431 +\               c ~= {} \
   1.432 +\            |]\
   1.433 +\            ==> Union(c) ~= {}";
   1.434 +by (dtac mem_chain_psubset_empty 1);
   1.435 +by (Step_tac 1);
   1.436 +by (dtac bspec 1 THEN assume_tac 1);
   1.437 +by (auto_tac (claset() addDs [Union_upper,bspec],
   1.438 +    simpset() addsimps [psubset_def]));
   1.439 +qed "chain_Un_not_empty";
   1.440 +
   1.441 +Goalw [is_Filter_def,Filter_def,chain_def,thm "superfrechet_def"] 
   1.442 +           "!!(c :: 'a set set set). \
   1.443 +\           c : chain (superfrechet S)  \
   1.444 +\           ==> {} ~: Union(c)";
   1.445 +by (Blast_tac 1);
   1.446 +qed "Filter_empty_not_mem_Un";
   1.447 +
   1.448 +Goal "c: chain (superfrechet S) \
   1.449 +\         ==> ALL u : Union(c). ALL v: Union(c). u Int v : Union(c)";
   1.450 +by (Step_tac 1);
   1.451 +by (forw_inst_tac [("x","X"),("y","Xa")] chainD 1);
   1.452 +by (REPEAT(assume_tac 1));
   1.453 +by (dtac chainD2 1);
   1.454 +by (etac disjE 1);
   1.455 +by (res_inst_tac [("X","Xa")] UnionI 1 THEN assume_tac 1);
   1.456 +by (dres_inst_tac [("A","X")] subsetD 1 THEN assume_tac 1);
   1.457 +by (dres_inst_tac [("c","Xa")] subsetD 1 THEN assume_tac 1);
   1.458 +by (res_inst_tac [("X","X")] UnionI 2 THEN assume_tac 2);
   1.459 +by (dres_inst_tac [("A","Xa")] subsetD 2 THEN assume_tac 2);
   1.460 +by (dres_inst_tac [("c","X")] subsetD 2 THEN assume_tac 2);
   1.461 +by (auto_tac (claset() addIs [mem_FiltersetD1], 
   1.462 +     simpset() addsimps [thm "superfrechet_def"]));
   1.463 +qed "Filter_Un_Int";
   1.464 +
   1.465 +Goal "c: chain (superfrechet S) \
   1.466 +\         ==> ALL u v. u: Union(c) & \
   1.467 +\                 (u :: 'a set) <= v & v <= S --> v: Union(c)";
   1.468 +by (Step_tac 1);
   1.469 +by (dtac chainD2 1);
   1.470 +by (dtac subsetD 1 THEN assume_tac 1);
   1.471 +by (rtac UnionI 1 THEN assume_tac 1);
   1.472 +by (auto_tac (claset() addIs [mem_FiltersetD2], 
   1.473 +     simpset() addsimps [thm "superfrechet_def"]));
   1.474 +qed "Filter_Un_subset";
   1.475 +
   1.476 +Goalw [chain_def,thm "superfrechet_def"]
   1.477 +      "!!(c :: 'a set set set). \
   1.478 +\            [| c: chain (superfrechet S);\
   1.479 +\               x: c \
   1.480 +\            |] ==> x : Filter S";
   1.481 +by (Blast_tac 1);
   1.482 +qed "lemma_mem_chain_Filter";
   1.483 +
   1.484 +Goalw [chain_def,thm "superfrechet_def"]
   1.485 +     "!!(c :: 'a set set set). \
   1.486 +\            [| c: chain (superfrechet S);\
   1.487 +\               x: c \
   1.488 +\            |] ==> frechet S <= x";
   1.489 +by (Blast_tac 1);
   1.490 +qed "lemma_mem_chain_frechet_subset";
   1.491 +
   1.492 +Goal "!!(c :: 'a set set set). \
   1.493 +\         [| c ~= {}; \
   1.494 +\            c : chain (superfrechet (UNIV :: 'a set))\
   1.495 +\         |] ==> Union c : superfrechet (UNIV)";
   1.496 +by (simp_tac (simpset() addsimps 
   1.497 +    [thm "superfrechet_def",thm "frechet_def"]) 1);
   1.498 +by (Step_tac 1);
   1.499 +by (rtac mem_FiltersetI2 1);
   1.500 +by (etac chain_Un_subset_Pow 1);
   1.501 +by (rtac UnionI 1 THEN assume_tac 1);
   1.502 +by (etac (lemma_mem_chain_Filter RS mem_FiltersetD4) 1 THEN assume_tac 1);
   1.503 +by (etac chain_Un_not_empty 1);
   1.504 +by (etac Filter_empty_not_mem_Un 2);
   1.505 +by (etac Filter_Un_Int 2);
   1.506 +by (etac Filter_Un_subset 2);
   1.507 +by (subgoal_tac "xa : frechet (UNIV)" 2);
   1.508 +by (rtac UnionI 2 THEN assume_tac 2);
   1.509 +by (rtac (lemma_mem_chain_frechet_subset RS subsetD) 2);
   1.510 +by (auto_tac (claset(),simpset() addsimps [thm "frechet_def"]));
   1.511 +qed "Un_chain_mem_cofinite_Filter_set";
   1.512 +
   1.513 +Goal "EX U: superfrechet (UNIV). \
   1.514 +\               ALL G: superfrechet (UNIV). U <= G --> U = G";
   1.515 +by (rtac Zorn_Lemma2 1);
   1.516 +by (cut_facts_tac [thm "not_finite_UNIV" RS cofinite_Filter] 1);
   1.517 +by (Step_tac 1);
   1.518 +by (res_inst_tac [("Q","c={}")] (excluded_middle RS disjE) 1);
   1.519 +by (res_inst_tac [("x","Union c")] bexI 1 THEN Blast_tac 1);
   1.520 +by (rtac Un_chain_mem_cofinite_Filter_set 1 THEN REPEAT(assume_tac 1));
   1.521 +by (res_inst_tac [("x","frechet (UNIV)")] bexI 1 THEN Blast_tac 1);
   1.522 +by (auto_tac (claset(),simpset() addsimps 
   1.523 +        [thm "superfrechet_def", thm "frechet_def"]));
   1.524 +qed "max_cofinite_Filter_Ex";
   1.525 +
   1.526 +Goal "EX U: superfrechet UNIV. (\
   1.527 +\               ALL G: superfrechet UNIV. U <= G --> U = G) \ 
   1.528 +\                             & (ALL x: U. ~finite x)";
   1.529 +by (cut_facts_tac [thm "not_finite_UNIV" RS 
   1.530 +         (export max_cofinite_Filter_Ex)] 1);
   1.531 +by (Step_tac 1);
   1.532 +by (res_inst_tac [("x","U")] bexI 1);
   1.533 +by (auto_tac (claset(),simpset() addsimps 
   1.534 +        [thm "superfrechet_def", thm "frechet_def"]));
   1.535 +by (dres_inst_tac [("c","- x")] subsetD 1);
   1.536 +by (Asm_simp_tac 1);
   1.537 +by (forw_inst_tac [("A","x"),("B","- x")] mem_FiltersetD1 1);
   1.538 +by (dtac Filter_empty_not_mem 3);
   1.539 +by (ALLGOALS(Asm_full_simp_tac ));
   1.540 +qed "max_cofinite_Freefilter_Ex";
   1.541 +
   1.542 +(*--------------------------------------------------------------------------------
   1.543 +               There exists a free ultrafilter on any infinite set
   1.544 + --------------------------------------------------------------------------------*)
   1.545 +
   1.546 +Goalw [FreeUltrafilter_def] "EX U. U: FreeUltrafilter (UNIV :: 'a set)";
   1.547 +by (cut_facts_tac [thm "not_finite_UNIV" RS (export max_cofinite_Freefilter_Ex)] 1);
   1.548 +by (asm_full_simp_tac (simpset() addsimps 
   1.549 +    [thm "superfrechet_def", Ultrafilter_iff, thm "frechet_def"]) 1);
   1.550 +by (Step_tac 1);
   1.551 +by (res_inst_tac [("x","U")] exI 1);
   1.552 +by (Step_tac 1);
   1.553 +by (Blast_tac 1);
   1.554 +qed "FreeUltrafilter_ex";
   1.555 +
   1.556 +val FreeUltrafilter_Ex  = export FreeUltrafilter_ex;
   1.557 +
   1.558 +Close_locale();
   1.559 +
   1.560 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Real/Hyperreal/Filter.thy	Fri Nov 27 11:24:27 1998 +0100
     2.3 @@ -0,0 +1,44 @@
     2.4 +(*  Title       : Filter.thy
     2.5 +    Author      : Jacques D. Fleuriot
     2.6 +    Copyright   : 1998  University of Cambridge
     2.7 +    Description : Filters and Ultrafilters
     2.8 +*) 
     2.9 +
    2.10 +Filter = Zorn + 
    2.11 +
    2.12 +constdefs
    2.13 +
    2.14 +  is_Filter       :: ['a set set,'a set] => bool
    2.15 +  "is_Filter F S == (F <= Pow(S) & S : F & {} ~: F &
    2.16 +                   (ALL u: F. ALL v: F. u Int v : F) &
    2.17 +                   (ALL u v. u: F & u <= v & v <= S --> v: F))" 
    2.18 +
    2.19 +  Filter          :: 'a set => 'a set set set
    2.20 +  "Filter S == {X. is_Filter X S}"
    2.21 + 
    2.22 +  (* free filter does not contain any finite set *)
    2.23 +
    2.24 +  Freefilter      :: 'a set => 'a set set set
    2.25 +  "Freefilter S == {X. X: Filter S & (ALL x: X. ~ finite x)}"
    2.26 +
    2.27 +  Ultrafilter     :: 'a set => 'a set set set
    2.28 +  "Ultrafilter S == {X. X: Filter S & (ALL A: Pow(S). A: X | S - A : X)}"
    2.29 +
    2.30 +  FreeUltrafilter :: 'a set => 'a set set set
    2.31 +  "FreeUltrafilter S == {X. X: Ultrafilter S & (ALL x: X. ~ finite x)}" 
    2.32 +
    2.33 +  (* A locale makes proof of Ultrafilter Theorem more modular *)
    2.34 +locale UFT = 
    2.35 +       fixes     frechet :: "'a set => 'a set set"
    2.36 +                 superfrechet :: "'a set => 'a set set set"
    2.37 +
    2.38 +       assumes   not_finite_UNIV "~finite (UNIV :: 'a set)"
    2.39 +
    2.40 +       defines   frechet_def "frechet S == {A. finite (S - A)}"
    2.41 +                 superfrechet_def "superfrechet S == 
    2.42 +                                   {G.  G: Filter S & frechet S <= G}"
    2.43 +end
    2.44 +
    2.45 +
    2.46 +
    2.47 +
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Real/Hyperreal/README.html	Fri Nov 27 11:24:27 1998 +0100
     3.3 @@ -0,0 +1,23 @@
     3.4 +<!-- $Id$ -->
     3.5 +<HTML><HEAD><TITLE>HOL/Real/README</TITLE></HEAD><BODY>
     3.6 +
     3.7 +<H2>Hyperreal--Ultrafilter Construction of the Non-Standard Reals</H2>
     3.8 +
     3.9 +<UL>
    3.10 +<LI><A HREF="Zorn.html">Zorn</A>
    3.11 +Zorn's Lemma: proof based on the <A HREF="../../ZF/Zorn.html">ZF version</A>
    3.12 +
    3.13 +<LI><A HREF="Filter.html">Filter</A>
    3.14 +Theory of Filters and Ultrafilters.
    3.15 +Main result is a version of the Ultrafilter Theorem proved using Zorn's Lemma.
    3.16 +</UL>
    3.17 +
    3.18 +<P>Last modified on $Date$
    3.19 +
    3.20 +<HR>
    3.21 +
    3.22 +<ADDRESS>
    3.23 +<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
    3.24 +</ADDRESS>
    3.25 +</BODY></HTML>
    3.26 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Real/Hyperreal/ROOT.ML	Fri Nov 27 11:24:27 1998 +0100
     4.3 @@ -0,0 +1,14 @@
     4.4 +(*  Title:      HOL/Hyperreal/ROOT
     4.5 +    ID:         $Id$
     4.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 +    Copyright   1998  University of Cambridge
     4.8 +
     4.9 +Construction of the Hyperreals using ultrafilters, by Jacques Fleuriot
    4.10 +*)
    4.11 +
    4.12 +HOL_build_completed;    (*Make examples fail if HOL did*)
    4.13 +
    4.14 +writeln"Root file for HOL/Hyperreal";
    4.15 +
    4.16 +set proof_timing;
    4.17 +time_use_thy "Filter";
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Real/Hyperreal/Zorn.ML	Fri Nov 27 11:24:27 1998 +0100
     5.3 @@ -0,0 +1,293 @@
     5.4 +(*  Title       : Zorn.ML
     5.5 +    Author      : Jacques D. Fleuriot
     5.6 +    Copyright   : 1998  University of Cambridge
     5.7 +    Description : Zorn's Lemma -- adapted proofs from lcp's ZF/Zorn.ML
     5.8 +*) 
     5.9 +
    5.10 +open Zorn;
    5.11 +
    5.12 +(*---------------------------------------------------------------
    5.13 +      Section 1.  Mathematical Preamble 
    5.14 + ---------------------------------------------------------------*)
    5.15 +
    5.16 +Goal "(ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
    5.17 +by (Blast_tac 1);
    5.18 +qed "Union_lemma0";
    5.19 +
    5.20 +(*-- similar to subset_cs in ZF/subset.thy --*)
    5.21 +val thissubset_SIs =
    5.22 +    [subset_refl,Union_least, UN_least, Un_least, 
    5.23 +     Inter_greatest, Int_greatest,
    5.24 +     Un_upper1, Un_upper2, Int_lower1, Int_lower2];
    5.25 +
    5.26 +
    5.27 +(*A claset for subset reasoning*)
    5.28 +val thissubset_cs = claset() 
    5.29 +    delrules [subsetI, subsetCE]
    5.30 +    addSIs thissubset_SIs
    5.31 +    addIs  [Union_upper, Inter_lower];
    5.32 +
    5.33 +(* increasingD2 of ZF/Zorn.ML *) 
    5.34 +Goalw [succ_def] "x <= succ S x";
    5.35 +by (rtac (expand_if RS iffD2) 1);
    5.36 +by (auto_tac (claset(),simpset() addsimps [super_def,
    5.37 +               maxchain_def,psubset_def]));
    5.38 +by (rtac swap 1 THEN assume_tac 1);
    5.39 +by (rtac selectI2 1);
    5.40 +by (ALLGOALS(Blast_tac));
    5.41 +qed "Abrial_axiom1";
    5.42 +
    5.43 +val [TFin_succI, Pow_TFin_UnionI] = TFin.intrs;
    5.44 +val TFin_UnionI = PowI RS Pow_TFin_UnionI;
    5.45 +
    5.46 +val major::prems = Goal  
    5.47 +          "[| n : TFin S; \
    5.48 +\            !!x. [| x: TFin S; P(x) |] ==> P(succ S x); \
    5.49 +\            !!Y. [| Y <= TFin S; Ball Y P |] ==> P(Union Y) |] \
    5.50 +\         ==> P(n)";
    5.51 +by (rtac (major RS TFin.induct) 1);
    5.52 +by (ALLGOALS (fast_tac (claset() addIs prems)));
    5.53 +qed "TFin_induct";
    5.54 +
    5.55 +(*Perform induction on n, then prove the major premise using prems. *)
    5.56 +fun TFin_ind_tac a prems i = 
    5.57 +    EVERY [res_inst_tac [("n",a)] TFin_induct i,
    5.58 +           rename_last_tac a ["1"] (i+1),
    5.59 +           rename_last_tac a ["2"] (i+2),
    5.60 +           ares_tac prems i];
    5.61 +
    5.62 +Goal "x <= y ==> x <= succ S y";
    5.63 +by (etac (Abrial_axiom1 RSN (2,subset_trans)) 1);
    5.64 +qed "succ_trans";
    5.65 +
    5.66 +(*Lemma 1 of section 3.1*)
    5.67 +Goal "[| n: TFin S;  m: TFin S;  \
    5.68 +\        ALL x: TFin S. x <= m --> x = m | succ S x <= m \
    5.69 +\     |] ==> n <= m | succ S m <= n";
    5.70 +by (etac TFin_induct 1);
    5.71 +by (etac Union_lemma0 2);               (*or just Blast_tac*)
    5.72 +by (blast_tac (thissubset_cs addIs [succ_trans]) 1);
    5.73 +qed "TFin_linear_lemma1";
    5.74 +
    5.75 +(* Lemma 2 of section 3.2 *)
    5.76 +Goal "m: TFin S ==> ALL n: TFin S. n<=m --> n=m | succ S n<=m";
    5.77 +by (etac TFin_induct 1);
    5.78 +by (rtac (impI RS ballI) 1);
    5.79 +(*case split using TFin_linear_lemma1*)
    5.80 +by (res_inst_tac [("n1","n"), ("m1","x")] 
    5.81 +    (TFin_linear_lemma1 RS disjE) 1  THEN  REPEAT (assume_tac 1));
    5.82 +by (dres_inst_tac [("x","n")] bspec 1 THEN assume_tac 1);
    5.83 +by (blast_tac (thissubset_cs addIs [succ_trans]) 1);
    5.84 +by (REPEAT (ares_tac [disjI1,equalityI] 1));
    5.85 +(*second induction step*)
    5.86 +by (rtac (impI RS ballI) 1);
    5.87 +by (rtac (Union_lemma0 RS disjE) 1);
    5.88 +by (rtac disjI2 3);
    5.89 +by (REPEAT (ares_tac [disjI1,equalityI] 2));
    5.90 +by (rtac ballI 1);
    5.91 +by (ball_tac 1);
    5.92 +by (set_mp_tac 1);
    5.93 +by (res_inst_tac [("n1","n"), ("m1","x")] 
    5.94 +    (TFin_linear_lemma1 RS disjE) 1  THEN  REPEAT (assume_tac 1));
    5.95 +by (blast_tac thissubset_cs 1);
    5.96 +by (rtac (Abrial_axiom1 RS subset_trans RS disjI1) 1);
    5.97 +by (assume_tac 1);
    5.98 +qed "TFin_linear_lemma2";
    5.99 +
   5.100 +(*a more convenient form for Lemma 2*)
   5.101 +Goal "[| n<=m;  m: TFin S;  n: TFin S |] ==> n=m | succ S n<=m";
   5.102 +by (rtac (TFin_linear_lemma2 RS bspec RS mp) 1);
   5.103 +by (REPEAT (assume_tac 1));
   5.104 +qed "TFin_subsetD";
   5.105 +
   5.106 +(*Consequences from section 3.3 -- Property 3.2, the ordering is total*)
   5.107 +Goal "[| m: TFin S;  n: TFin S|] ==> n<=m | m<=n";
   5.108 +by (rtac (TFin_linear_lemma2 RSN (3,TFin_linear_lemma1) RS disjE) 1);
   5.109 +by (REPEAT (assume_tac 1) THEN etac disjI2 1);
   5.110 +by (blast_tac (thissubset_cs addIs [Abrial_axiom1 RS subset_trans]) 1);
   5.111 +qed "TFin_subset_linear";
   5.112 +
   5.113 +(*Lemma 3 of section 3.3*)
   5.114 +Goal "[| n: TFin S;  m: TFin S;  m = succ S m |] ==> n<=m";
   5.115 +by (etac TFin_induct 1);
   5.116 +by (dtac TFin_subsetD 1);
   5.117 +by (REPEAT (assume_tac 1));
   5.118 +by (fast_tac (claset() addEs [ssubst]) 1);
   5.119 +by (blast_tac (thissubset_cs) 1);
   5.120 +qed "eq_succ_upper";
   5.121 +
   5.122 +(*Property 3.3 of section 3.3*)
   5.123 +Goal "m: TFin S ==> (m = succ S m) = (m = Union(TFin S))";
   5.124 +by (rtac iffI 1);
   5.125 +by (rtac (Union_upper RS equalityI) 1);
   5.126 +by (rtac (eq_succ_upper RS Union_least) 2);
   5.127 +by (REPEAT (assume_tac 1));
   5.128 +by (etac ssubst 1);
   5.129 +by (rtac (Abrial_axiom1 RS equalityI) 1);
   5.130 +by (blast_tac (thissubset_cs addIs [TFin_UnionI, TFin_succI]) 1);
   5.131 +qed "equal_succ_Union";
   5.132 +
   5.133 +(*-------------------------------------------------------------------------
   5.134 +    Section 4.  Hausdorff's Theorem: every set contains a maximal chain 
   5.135 +    NB: We assume the partial ordering is <=, the subset relation! 
   5.136 + -------------------------------------------------------------------------*)
   5.137 +
   5.138 +Goalw [chain_def] "({} :: 'a set set) : chain S";
   5.139 +by (Auto_tac);
   5.140 +qed "empty_set_mem_chain";
   5.141 +
   5.142 +Goalw [super_def] "super S c <= chain S";
   5.143 +by (Fast_tac 1);
   5.144 +qed "super_subset_chain";
   5.145 +
   5.146 +Goalw [maxchain_def] "maxchain S <= chain S";
   5.147 +by (Fast_tac 1);
   5.148 +qed "maxchain_subset_chain";
   5.149 +
   5.150 +Goalw [succ_def] "c ~: chain S ==> succ S c = c";
   5.151 +by (fast_tac (claset() addSIs [if_P]) 1);
   5.152 +qed "succI1";
   5.153 +
   5.154 +Goalw [succ_def] "c: maxchain S ==> succ S c = c";
   5.155 +by (fast_tac (claset() addSIs [if_P]) 1);
   5.156 +qed "succI2";
   5.157 +
   5.158 +Goalw [succ_def] "c: chain S - maxchain S ==> \
   5.159 +\                         succ S c = (@c'. c': super S c)";
   5.160 +by (fast_tac (claset() addSIs [if_not_P]) 1);
   5.161 +qed "succI3";
   5.162 +
   5.163 +Goal "c: chain S - maxchain S ==> ? d. d: super S c";
   5.164 +by (rewrite_goals_tac [super_def,maxchain_def]);
   5.165 +by (Auto_tac);
   5.166 +qed "mem_super_Ex";
   5.167 +
   5.168 +Goal "c: chain S - maxchain S ==> \
   5.169 +\                         (@c'. c': super S c): super S c";
   5.170 +by (etac (mem_super_Ex RS exE) 1);
   5.171 +by (rtac selectI2 1);
   5.172 +by (Auto_tac);
   5.173 +qed "select_super";
   5.174 +
   5.175 +Goal "c: chain S - maxchain S ==> \
   5.176 +\                         (@c'. c': super S c) ~= c";
   5.177 +by (rtac notI 1);
   5.178 +by (dtac select_super 1);
   5.179 +by (asm_full_simp_tac (simpset() addsimps [super_def,psubset_def]) 1);
   5.180 +qed "select_not_equals";
   5.181 +
   5.182 +Goal "c: chain S - maxchain S ==> \
   5.183 +\                         succ S c ~= c";
   5.184 +by (forward_tac [succI3] 1);
   5.185 +by (Asm_simp_tac 1);
   5.186 +by (rtac select_not_equals 1);
   5.187 +by (assume_tac 1);
   5.188 +qed "succ_not_equals";
   5.189 +
   5.190 +Goal "c: TFin S ==> (c :: 'a set set): chain S";
   5.191 +by (etac TFin_induct 1);
   5.192 +by (asm_simp_tac (simpset() addsimps [succ_def,
   5.193 +    select_super RS (super_subset_chain RS subsetD)]
   5.194 +                   setloop split_tac [expand_if]) 1);
   5.195 +by (rewtac chain_def);
   5.196 +by (rtac CollectI 1);
   5.197 +by (safe_tac(claset()));
   5.198 +by (dtac bspec 1 THEN assume_tac 1);
   5.199 +by (res_inst_tac  [("m1","Xa"), ("n1","X")] (TFin_subset_linear RS disjE) 2);
   5.200 +by (ALLGOALS(Blast_tac));
   5.201 +qed "TFin_chain_lemm4";
   5.202 + 
   5.203 +Goal "EX c. (c :: 'a set set): maxchain S";
   5.204 +by (res_inst_tac [("x", "Union(TFin S)")] exI 1);
   5.205 +by (rtac classical 1);
   5.206 +by (subgoal_tac "succ S (Union(TFin S)) = Union(TFin S)" 1);
   5.207 +by (resolve_tac [equal_succ_Union RS iffD2 RS sym] 2);
   5.208 +by (resolve_tac [subset_refl RS TFin_UnionI] 2);
   5.209 +by (rtac refl 2);
   5.210 +by (cut_facts_tac [subset_refl RS TFin_UnionI RS TFin_chain_lemm4] 1);
   5.211 +by (dtac (DiffI RS succ_not_equals) 1);
   5.212 +by (ALLGOALS(Blast_tac));
   5.213 +qed "Hausdorff";
   5.214 +
   5.215 +
   5.216 +(*---------------------------------------------------------------
   5.217 +  Section 5.  Zorn's Lemma: if all chains have upper bounds 
   5.218 +                               there is  a maximal element 
   5.219 + ----------------------------------------------------------------*)
   5.220 +Goalw [chain_def]
   5.221 +    "[| c: chain S; z: S; \
   5.222 +\             ALL x:c. x<=(z:: 'a set) |] ==> {z} Un c : chain S";
   5.223 +by (Blast_tac 1);
   5.224 +qed "chain_extend";
   5.225 +
   5.226 +Goalw [chain_def] "[| c: chain S; x: c |] ==> x <= Union(c)";
   5.227 +by (Auto_tac);
   5.228 +qed "chain_Union_upper";
   5.229 +
   5.230 +Goalw [chain_def] "c: chain S ==> ! x: c. x <= Union(c)";
   5.231 +by (Auto_tac);
   5.232 +qed "chain_ball_Union_upper";
   5.233 +
   5.234 +Goal "[| c: maxchain S; u: S; Union(c) <= u |] ==> Union(c) = u";
   5.235 +by (rtac ccontr 1);
   5.236 +by (asm_full_simp_tac (simpset() addsimps [maxchain_def]) 1);
   5.237 +by (etac conjE 1);
   5.238 +by (subgoal_tac "({u} Un c): super S c" 1);
   5.239 +by (Asm_full_simp_tac 1);
   5.240 +by (rewrite_tac [super_def,psubset_def]);
   5.241 +by (safe_tac (claset()));
   5.242 +by (fast_tac (claset() addEs [chain_extend]) 1);
   5.243 +by (subgoal_tac "u ~: c" 1);
   5.244 +by (blast_tac (claset() addEs [equalityE]) 1);
   5.245 +by (blast_tac (claset() addDs [chain_Union_upper]) 1);
   5.246 +qed "maxchain_Zorn";
   5.247 +
   5.248 +Goal "ALL c: chain S. Union(c): S ==> \
   5.249 +\     EX y: S. ALL z: S. y <= z --> y = z";
   5.250 +by (cut_facts_tac [Hausdorff,maxchain_subset_chain] 1);
   5.251 +by (etac exE 1);
   5.252 +by (dtac subsetD 1 THEN assume_tac 1);
   5.253 +by (dtac bspec 1 THEN assume_tac 1);
   5.254 +by (res_inst_tac [("x","Union(c)")] bexI 1);
   5.255 +by (rtac ballI 1 THEN rtac impI 1);
   5.256 +by (blast_tac (claset() addSDs [maxchain_Zorn]) 1);
   5.257 +by (assume_tac 1);
   5.258 +qed "Zorn_Lemma";
   5.259 +
   5.260 +(*-------------------------------------------------------------
   5.261 +             Alternative version of Zorn's Lemma
   5.262 + --------------------------------------------------------------*)
   5.263 +Goal "ALL (c:: 'a set set): chain S. EX y : S. ALL x : c. x <= y ==> \
   5.264 +\     EX y : S. ALL x : S. (y :: 'a set) <= x --> y = x";
   5.265 +by (cut_facts_tac [Hausdorff,maxchain_subset_chain] 1);
   5.266 +by (EVERY1[etac exE, dtac subsetD, assume_tac]);
   5.267 +by (EVERY1[dtac bspec, assume_tac, etac bexE]);
   5.268 +by (res_inst_tac [("x","y")] bexI 1);
   5.269 +by (assume_tac 2);
   5.270 +by (EVERY1[rtac ballI, rtac impI, rtac ccontr]);
   5.271 +by (forw_inst_tac [("z","x")]  chain_extend 1);
   5.272 +by (assume_tac 1 THEN Blast_tac 1);
   5.273 +by (rewrite_tac [maxchain_def,super_def,psubset_def]);
   5.274 +by (Step_tac 1);
   5.275 +by (eres_inst_tac [("c","{x} Un c")] equalityCE 1);
   5.276 +by (Step_tac 1);
   5.277 +by (subgoal_tac "x ~: c" 1);
   5.278 +by (blast_tac (claset() addEs [equalityE]) 1);
   5.279 +by (Blast_tac 1);
   5.280 +qed "Zorn_Lemma2";
   5.281 +
   5.282 +(** misc. lemmas **)
   5.283 +
   5.284 +Goalw [chain_def] "[| c : chain S; x: c; y: c |] ==> x <= y | y <= x";
   5.285 +by (Blast_tac 1);
   5.286 +qed "chainD";
   5.287 +
   5.288 +Goalw [chain_def] "!!(c :: 'a set set). c: chain S ==> c <= S";
   5.289 +by (Blast_tac 1);
   5.290 +qed "chainD2";
   5.291 +
   5.292 +(* proved elsewhere? *) 
   5.293 +Goal "x : Union(c) ==> EX m:c. x:m";
   5.294 +by (Blast_tac 1);
   5.295 +qed "mem_UnionD";
   5.296 +
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Real/Hyperreal/Zorn.thy	Fri Nov 27 11:24:27 1998 +0100
     6.3 @@ -0,0 +1,33 @@
     6.4 +(*  Title       : Zorn.thy
     6.5 +    Author      : Jacques D. Fleuriot
     6.6 +    Copyright   : 1998  University of Cambridge
     6.7 +    Description : Zorn's Lemma -- See lcp's Zorn.thy in ZF
     6.8 +*) 
     6.9 +
    6.10 +Zorn = Finite +  
    6.11 +
    6.12 +constdefs
    6.13 +  chain     ::  'a set => 'a set set
    6.14 +    "chain S  == {F. F <= S & (ALL x: F. ALL y: F. x <= y | y <= x)}" 
    6.15 +
    6.16 +  super     ::  ['a set,'a set] => (('a set) set) 
    6.17 +    "super S c == {d. d: chain(S) & c < d}"
    6.18 +
    6.19 +  maxchain  ::  'a set => 'a set set
    6.20 +    "maxchain S == {c. c: chain S & super S c = {}}"
    6.21 +
    6.22 +  succ      ::  ['a set,'a set] => 'a set
    6.23 +    "succ S c == if (c ~: chain S| c: maxchain S) 
    6.24 +                 then c else (@c'. c': (super S c))" 
    6.25 +
    6.26 +consts 
    6.27 +  "TFin" :: 'a set => 'a set set
    6.28 +
    6.29 +inductive "TFin(S)"
    6.30 +  intrs
    6.31 +    succI        "x : TFin S ==> succ S x : TFin S"
    6.32 +    Pow_UnionI   "Y : Pow(TFin S) ==> Union(Y) : TFin S"
    6.33 +           
    6.34 +  monos          Pow_mono
    6.35 +end
    6.36 +
     7.1 --- a/src/HOL/Real/ROOT.ML	Fri Nov 27 10:40:29 1998 +0100
     7.2 +++ b/src/HOL/Real/ROOT.ML	Fri Nov 27 11:24:27 1998 +0100
     7.3 @@ -15,3 +15,5 @@
     7.4  use          "simproc";
     7.5  time_use_thy "RealAbs";
     7.6  time_use_thy "RComplete";
     7.7 +
     7.8 +use_dir "Hyperreal";