conversion of Hyperreal/Filter to Isar scripts
authorpaulson
Mon Aug 02 11:20:37 2004 +0200 (2004-08-02)
changeset 15100dfb4e23923e0
parent 15099 6d8619440ea0
child 15101 d027515e2aa6
conversion of Hyperreal/Filter to Isar scripts
src/HOL/Hyperreal/Filter.ML
     1.1 --- a/src/HOL/Hyperreal/Filter.ML	Mon Aug 02 10:16:58 2004 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,560 +0,0 @@
     1.4 -(*  Title       : Filter.ML
     1.5 -    ID          : $Id$
     1.6 -    Author      : Jacques D. Fleuriot
     1.7 -    Copyright   : 1998  University of Cambridge
     1.8 -    Description : Filters and Ultrafilter
     1.9 -*) 
    1.10 -
    1.11 -(*ML bindings for Library/Zorn theorems*)
    1.12 -val chain_def = thm "chain_def";
    1.13 -val chainD = thm "chainD";
    1.14 -val chainD2 = thm "chainD2";
    1.15 -val Zorn_Lemma2 = thm "Zorn_Lemma2";
    1.16 -
    1.17 -(*------------------------------------------------------------------
    1.18 -      Properties of Filters and Freefilters - 
    1.19 -      rules for intro, destruction etc.
    1.20 - ------------------------------------------------------------------*)
    1.21 -
    1.22 -Goalw [is_Filter_def] "is_Filter X S ==> X <= Pow(S)";
    1.23 -by (Blast_tac 1);
    1.24 -qed "is_FilterD1";
    1.25 -
    1.26 -Goalw [is_Filter_def] "is_Filter X S ==> X ~= {}";
    1.27 -by (Blast_tac 1);
    1.28 -qed "is_FilterD2";
    1.29 -
    1.30 -Goalw [is_Filter_def] "is_Filter X S ==> {} ~: X";
    1.31 -by (Blast_tac 1);
    1.32 -qed "is_FilterD3";
    1.33 -
    1.34 -Goalw [Filter_def] "is_Filter X S ==> X : Filter S";
    1.35 -by (Blast_tac 1);
    1.36 -qed "mem_FiltersetI";
    1.37 -
    1.38 -Goalw [Filter_def] "X : Filter S ==> is_Filter X S";
    1.39 -by (Blast_tac 1);
    1.40 -qed "mem_FiltersetD";
    1.41 -
    1.42 -Goal "X : Filter S ==> {} ~: X";
    1.43 -by (etac (mem_FiltersetD RS is_FilterD3) 1);
    1.44 -qed "Filter_empty_not_mem";
    1.45 -
    1.46 -bind_thm ("Filter_empty_not_memE",(Filter_empty_not_mem RS notE));
    1.47 -
    1.48 -Goalw [Filter_def,is_Filter_def] 
    1.49 -      "[| X: Filter S; A: X; B: X |] ==> A Int B : X";
    1.50 -by (Blast_tac 1);
    1.51 -qed "mem_FiltersetD1";
    1.52 -
    1.53 -Goalw [Filter_def,is_Filter_def] 
    1.54 -      "[| X: Filter S; A: X; A <= B; B <= S|] ==> B : X";
    1.55 -by (Blast_tac 1);
    1.56 -qed "mem_FiltersetD2";
    1.57 -
    1.58 -Goalw [Filter_def,is_Filter_def] 
    1.59 -      "[| X: Filter S; A: X |] ==> A : Pow S";
    1.60 -by (Blast_tac 1);
    1.61 -qed "mem_FiltersetD3";
    1.62 -
    1.63 -Goalw [Filter_def,is_Filter_def] 
    1.64 -      "X: Filter S  ==> S : X";
    1.65 -by (Blast_tac 1);
    1.66 -qed "mem_FiltersetD4";
    1.67 -
    1.68 -Goalw [is_Filter_def] 
    1.69 -      "[| X <= Pow(S);\
    1.70 -\              S : X; \
    1.71 -\              X ~= {}; \
    1.72 -\              {} ~: X; \
    1.73 -\              ALL u: X. ALL v: X. u Int v : X; \
    1.74 -\              ALL u v. u: X & u<=v & v<=S --> v: X \
    1.75 -\           |] ==> is_Filter X S";
    1.76 -by (Blast_tac 1); 
    1.77 -qed "is_FilterI";
    1.78 -
    1.79 -Goal "[| X <= Pow(S);\
    1.80 -\              S : X; \
    1.81 -\              X ~= {}; \
    1.82 -\              {} ~: X; \
    1.83 -\              ALL u: X. ALL v: X. u Int v : X; \
    1.84 -\              ALL u v. u: X & u<=v & v<=S --> v: X \
    1.85 -\           |] ==> X: Filter S";
    1.86 -by (blast_tac (claset() addIs [mem_FiltersetI,is_FilterI]) 1);
    1.87 -qed "mem_FiltersetI2";
    1.88 -
    1.89 -Goalw [is_Filter_def]
    1.90 -      "is_Filter X S ==> X <= Pow(S) & \
    1.91 -\                          S : X & \
    1.92 -\                          X ~= {} & \
    1.93 -\                          {} ~: X  & \
    1.94 -\                          (ALL u: X. ALL v: X. u Int v : X) & \
    1.95 -\                          (ALL u v. u: X & u <= v & v<=S --> v: X)";
    1.96 -by (Fast_tac 1);
    1.97 -qed "is_FilterE_lemma";
    1.98 -
    1.99 -Goalw [is_Filter_def]
   1.100 -      "X : Filter S ==> X <= Pow(S) &\
   1.101 -\                          S : X & \
   1.102 -\                          X ~= {} & \
   1.103 -\                          {} ~: X  & \
   1.104 -\                          (ALL u: X. ALL v: X. u Int v : X) & \
   1.105 -\                          (ALL u v. u: X & u <= v & v<=S --> v: X)";
   1.106 -by (etac (mem_FiltersetD RS is_FilterE_lemma) 1);
   1.107 -qed "memFiltersetE_lemma";
   1.108 -
   1.109 -Goalw [Filter_def,Freefilter_def] 
   1.110 -      "X: Freefilter S ==> X: Filter S";
   1.111 -by (Fast_tac 1);
   1.112 -qed "Freefilter_Filter";
   1.113 -
   1.114 -Goalw [Freefilter_def] 
   1.115 -      "X: Freefilter S ==> ALL y: X. ~finite(y)";
   1.116 -by (Blast_tac 1);
   1.117 -qed "mem_Freefilter_not_finite";
   1.118 -
   1.119 -Goal "[| X: Freefilter S; x: X |] ==> ~ finite x";
   1.120 -by (blast_tac (claset() addSDs [mem_Freefilter_not_finite]) 1);
   1.121 -qed "mem_FreefiltersetD1";
   1.122 -
   1.123 -bind_thm ("mem_FreefiltersetE1", (mem_FreefiltersetD1 RS notE));
   1.124 -
   1.125 -Goal "[| X: Freefilter S; finite x|] ==> x ~: X";
   1.126 -by (blast_tac (claset() addSDs [mem_Freefilter_not_finite]) 1);
   1.127 -qed "mem_FreefiltersetD2";
   1.128 -
   1.129 -Goalw [Freefilter_def] 
   1.130 -      "[| X: Filter S; ALL x. ~(x: X & finite x) |] ==> X: Freefilter S";
   1.131 -by (Blast_tac 1);
   1.132 -qed "mem_FreefiltersetI1";
   1.133 -
   1.134 -Goalw [Freefilter_def]
   1.135 -      "[| X: Filter S; ALL x. (x ~: X | ~ finite x) |] ==> X: Freefilter S";
   1.136 -by (Blast_tac 1);
   1.137 -qed "mem_FreefiltersetI2";
   1.138 -
   1.139 -Goal "[| X: Filter S; A: X; B: X |] ==> A Int B ~= {}";
   1.140 -by (forw_inst_tac [("A","A"),("B","B")] mem_FiltersetD1 1);
   1.141 -by (auto_tac (claset() addSDs [Filter_empty_not_mem],simpset()));
   1.142 -qed "Filter_Int_not_empty";
   1.143 -
   1.144 -bind_thm ("Filter_Int_not_emptyE",(Filter_Int_not_empty RS notE));
   1.145 -
   1.146 -(*----------------------------------------------------------------------------------
   1.147 -              Ultrafilters and Free ultrafilters
   1.148 - ----------------------------------------------------------------------------------*)
   1.149 -
   1.150 -Goalw [Ultrafilter_def] "X : Ultrafilter S ==> X: Filter S";
   1.151 -by (Blast_tac 1);
   1.152 -qed "Ultrafilter_Filter";
   1.153 -
   1.154 -Goalw [Ultrafilter_def] 
   1.155 -      "X : Ultrafilter S ==> !A: Pow(S). A : X | S - A: X";
   1.156 -by (Blast_tac 1);
   1.157 -qed "mem_UltrafiltersetD2";
   1.158 -
   1.159 -Goalw [Ultrafilter_def] 
   1.160 -      "[|X : Ultrafilter S; A <= S; A ~: X |] ==> S - A: X";
   1.161 -by (Blast_tac 1);
   1.162 -qed "mem_UltrafiltersetD3";
   1.163 -
   1.164 -Goalw [Ultrafilter_def] 
   1.165 -      "[|X : Ultrafilter S; A <= S; S - A ~: X |] ==> A: X";
   1.166 -by (Blast_tac 1);
   1.167 -qed "mem_UltrafiltersetD4";
   1.168 -
   1.169 -Goalw [Ultrafilter_def]
   1.170 -     "[| X: Filter S; \
   1.171 -\             ALL A: Pow(S). A: X | S - A : X |] ==> X: Ultrafilter S";
   1.172 -by (Blast_tac 1);
   1.173 -qed "mem_UltrafiltersetI";
   1.174 -
   1.175 -Goalw [Ultrafilter_def,FreeUltrafilter_def]
   1.176 -     "X: FreeUltrafilter S ==> X: Ultrafilter S";
   1.177 -by (Blast_tac 1);
   1.178 -qed "FreeUltrafilter_Ultrafilter";
   1.179 -
   1.180 -Goalw [FreeUltrafilter_def]
   1.181 -     "X: FreeUltrafilter S ==> ALL y: X. ~finite(y)";
   1.182 -by (Blast_tac 1);
   1.183 -qed "mem_FreeUltrafilter_not_finite";
   1.184 -
   1.185 -Goal "[| X: FreeUltrafilter S; x: X |] ==> ~ finite x";
   1.186 -by (blast_tac (claset() addSDs [mem_FreeUltrafilter_not_finite]) 1);
   1.187 -qed "mem_FreeUltrafiltersetD1";
   1.188 -
   1.189 -bind_thm ("mem_FreeUltrafiltersetE1", (mem_FreeUltrafiltersetD1 RS notE));
   1.190 -
   1.191 -Goal "[| X: FreeUltrafilter S; finite x|] ==> x ~: X";
   1.192 -by (blast_tac (claset() addSDs [mem_FreeUltrafilter_not_finite]) 1);
   1.193 -qed "mem_FreeUltrafiltersetD2";
   1.194 -
   1.195 -Goalw [FreeUltrafilter_def] 
   1.196 -      "[| X: Ultrafilter S; \
   1.197 -\              ALL x. ~(x: X & finite x) |] ==> X: FreeUltrafilter S";
   1.198 -by (Blast_tac 1);
   1.199 -qed "mem_FreeUltrafiltersetI1";
   1.200 -
   1.201 -Goalw [FreeUltrafilter_def]
   1.202 -      "[| X: Ultrafilter S; \
   1.203 -\              ALL x. (x ~: X | ~ finite x) |] ==> X: FreeUltrafilter S";
   1.204 -by (Blast_tac 1);
   1.205 -qed "mem_FreeUltrafiltersetI2";
   1.206 -
   1.207 -Goalw [FreeUltrafilter_def,Freefilter_def,Ultrafilter_def]
   1.208 -     "(X: FreeUltrafilter S) = (X: Freefilter S & (ALL x:Pow(S). x: X | S - x: X))";
   1.209 -by (Blast_tac 1);
   1.210 -qed "FreeUltrafilter_iff";
   1.211 -
   1.212 -(*-------------------------------------------------------------------
   1.213 -   A Filter F on S is an ultrafilter iff it is a maximal filter 
   1.214 -   i.e. whenever G is a filter on I and F <= F then F = G
   1.215 - --------------------------------------------------------------------*)
   1.216 -(*---------------------------------------------------------------------
   1.217 -  lemmas that shows existence of an extension to what was assumed to
   1.218 -  be a maximal filter. Will be used to derive contradiction in proof of
   1.219 -  property of ultrafilter 
   1.220 - ---------------------------------------------------------------------*)
   1.221 -Goal "[| F ~= {}; A <= S |] ==> \
   1.222 -\        EX x. x: {X. X <= S & (EX f:F. A Int f <= X)}";
   1.223 -by (Blast_tac 1);
   1.224 -qed "lemma_set_extend";
   1.225 -
   1.226 -Goal "a: X ==> X ~= {}";
   1.227 -by (Step_tac 1);
   1.228 -qed "lemma_set_not_empty";
   1.229 -
   1.230 -Goal "x Int F <= {} ==> F <= - x";
   1.231 -by (Blast_tac 1);
   1.232 -qed "lemma_empty_Int_subset_Compl";
   1.233 -
   1.234 -Goalw [Filter_def,is_Filter_def]
   1.235 -      "[| F: Filter S; A ~: F; A <= S|] \
   1.236 -\          ==> ALL B. B ~: F | ~ B <= A";
   1.237 -by (Blast_tac 1);
   1.238 -qed "mem_Filterset_disjI";
   1.239 -
   1.240 -Goal "F : Ultrafilter S ==> \
   1.241 -\         (F: Filter S & (ALL G: Filter S. F <= G --> F = G))";
   1.242 -by (auto_tac (claset(),simpset() addsimps [Ultrafilter_def]));
   1.243 -by (dres_inst_tac [("x","x")] bspec 1);
   1.244 -by (etac mem_FiltersetD3 1 THEN assume_tac 1);
   1.245 -by (Step_tac 1);
   1.246 -by (dtac subsetD 1 THEN assume_tac 1);
   1.247 -by (blast_tac (claset() addSDs [Filter_Int_not_empty]) 1);
   1.248 -qed "Ultrafilter_max_Filter";
   1.249 -
   1.250 -
   1.251 -(*--------------------------------------------------------------------------------
   1.252 -     This is a very long and tedious proof; need to break it into parts.
   1.253 -     Have proof that {X. X <= S & (EX f: F. A Int f <= X)} is a filter as 
   1.254 -     a lemma
   1.255 ---------------------------------------------------------------------------------*)
   1.256 -Goalw [Ultrafilter_def] 
   1.257 -      "[| F: Filter S; \
   1.258 -\              ALL G: Filter S. F <= G --> F = G |] ==> F : Ultrafilter S";
   1.259 -by (Step_tac 1);
   1.260 -by (rtac ccontr 1);
   1.261 -by (forward_tac [mem_FiltersetD RS is_FilterD2] 1);
   1.262 -by (forw_inst_tac [("x","{X. X <= S & (EX f: F. A Int f <= X)}")] bspec 1);
   1.263 -by (EVERY1[rtac mem_FiltersetI2, Blast_tac, Asm_full_simp_tac]);
   1.264 -by (blast_tac (claset() addDs [mem_FiltersetD3]) 1);
   1.265 -by (etac (lemma_set_extend RS exE) 1);
   1.266 -by (assume_tac 1 THEN etac lemma_set_not_empty 1);
   1.267 -by (REPEAT(rtac ballI 2) THEN Asm_full_simp_tac 2);
   1.268 -by (rtac conjI 2 THEN Blast_tac 2);
   1.269 -by (REPEAT(etac conjE 2) THEN REPEAT(etac bexE 2));
   1.270 -by (res_inst_tac [("x","f Int fa")] bexI 2);
   1.271 -by (etac mem_FiltersetD1 3);
   1.272 -by (assume_tac 3 THEN assume_tac 3);
   1.273 -by (Fast_tac 2);
   1.274 -by (EVERY[REPEAT(rtac allI 2), rtac impI 2,Asm_full_simp_tac 2]);
   1.275 -by (EVERY[REPEAT(etac conjE 2), etac bexE 2]);
   1.276 -by (res_inst_tac [("x","f")] bexI 2);
   1.277 -by (rtac subsetI 2);
   1.278 -by (Fast_tac 2 THEN assume_tac 2);
   1.279 -by (Step_tac 2);
   1.280 -by (Blast_tac 3);
   1.281 -by (eres_inst_tac [("c","A")] equalityCE 3);
   1.282 -by (REPEAT(Blast_tac 3));
   1.283 -by (dres_inst_tac [("A","xa")] mem_FiltersetD3 2 THEN assume_tac 2);
   1.284 -by (Blast_tac 2);
   1.285 -by (dtac lemma_empty_Int_subset_Compl 1);
   1.286 -by (EVERY1[ftac mem_Filterset_disjI , assume_tac, Fast_tac]);
   1.287 -by (dtac mem_FiltersetD3 1 THEN assume_tac 1);
   1.288 -by (dres_inst_tac [("x","f")] spec 1);
   1.289 -by (Blast_tac 1);
   1.290 -qed "max_Filter_Ultrafilter";
   1.291 -
   1.292 -Goal "(F : Ultrafilter S) = (F: Filter S & (ALL G: Filter S. F <= G --> F = G))";
   1.293 -by (blast_tac (claset() addSIs [Ultrafilter_max_Filter,max_Filter_Ultrafilter]) 1);
   1.294 -qed "Ultrafilter_iff";
   1.295 -
   1.296 -(*--------------------------------------------------------------------
   1.297 -             A few properties of freefilters
   1.298 - -------------------------------------------------------------------*)
   1.299 -
   1.300 -Goal "F1 Int F2 = ((F1 Int Y) Int F2) Un ((F2 Int (- Y)) Int F1)";
   1.301 -by (Auto_tac);
   1.302 -qed "lemma_Compl_cancel_eq";
   1.303 -
   1.304 -Goal "finite X ==> finite (X Int Y)";
   1.305 -by (etac (Int_lower1 RS finite_subset) 1);
   1.306 -qed "finite_IntI1";
   1.307 -
   1.308 -Goal "finite Y ==> finite (X Int Y)";
   1.309 -by (etac (Int_lower2 RS finite_subset) 1);
   1.310 -qed "finite_IntI2";
   1.311 -
   1.312 -Goal "[| finite (F1 Int Y); \
   1.313 -\                 finite (F2 Int (- Y)) \
   1.314 -\              |] ==> finite (F1 Int F2)";
   1.315 -by (res_inst_tac [("Y1","Y")] (lemma_Compl_cancel_eq RS ssubst) 1);
   1.316 -by (rtac finite_UnI 1);
   1.317 -by (auto_tac (claset() addSIs [finite_IntI1,finite_IntI2],simpset()));
   1.318 -qed "finite_Int_Compl_cancel";
   1.319 -
   1.320 -Goal "U: Freefilter S  ==> \
   1.321 -\         ~ (EX f1: U. EX f2: U. finite (f1 Int x) \
   1.322 -\                            & finite (f2 Int (- x)))";
   1.323 -by (Step_tac 1);
   1.324 -by (forw_inst_tac [("A","f1"),("B","f2")] 
   1.325 -    (Freefilter_Filter RS mem_FiltersetD1) 1);
   1.326 -by (dres_inst_tac [("x","f1 Int f2")] mem_FreefiltersetD1 3);
   1.327 -by (dtac finite_Int_Compl_cancel 4);
   1.328 -by (Auto_tac);
   1.329 -qed "Freefilter_lemma_not_finite";
   1.330 -
   1.331 -(* the lemmas below follow *)
   1.332 -Goal "U: Freefilter S ==> \
   1.333 -\          ALL f: U. ~ finite (f Int x) | ~finite (f Int (- x))";
   1.334 -by (blast_tac (claset() addSDs [Freefilter_lemma_not_finite,bspec]) 1);
   1.335 -qed "Freefilter_Compl_not_finite_disjI";
   1.336 -
   1.337 -Goal "U: Freefilter S ==> \
   1.338 -\          (ALL f: U. ~ finite (f Int x)) | (ALL f:U. ~finite (f Int (- x)))";
   1.339 -by (blast_tac (claset() addSDs [Freefilter_lemma_not_finite,bspec]) 1);
   1.340 -qed "Freefilter_Compl_not_finite_disjI2";
   1.341 -
   1.342 -Goal "- UNIV = {}";
   1.343 -by (Auto_tac );
   1.344 -qed "Compl_UNIV_eq";
   1.345 -
   1.346 -Addsimps [Compl_UNIV_eq];
   1.347 -
   1.348 -Goal "- {} = UNIV";
   1.349 -by (Auto_tac );
   1.350 -qed "Compl_empty_eq";
   1.351 -
   1.352 -Addsimps [Compl_empty_eq];
   1.353 -
   1.354 -val [prem] = goal (the_context ()) "~ finite (UNIV:: 'a set) ==> \
   1.355 -\            {A:: 'a set. finite (- A)} : Filter UNIV";
   1.356 -by (cut_facts_tac [prem] 1);
   1.357 -by (rtac mem_FiltersetI2 1);
   1.358 -by (auto_tac (claset(), simpset() delsimps [Collect_empty_eq]));
   1.359 -by (eres_inst_tac [("c","UNIV")] equalityCE 1);
   1.360 -by (Auto_tac);
   1.361 -by (etac (Compl_anti_mono RS finite_subset) 1);
   1.362 -by (assume_tac 1);
   1.363 -qed "cofinite_Filter";
   1.364 -
   1.365 -Goal "~finite(UNIV :: 'a set) ==> ~finite (X :: 'a set) | ~finite (- X)";
   1.366 -by (dres_inst_tac [("A1","X")] (Compl_partition RS ssubst) 1);
   1.367 -by (Asm_full_simp_tac 1); 
   1.368 -qed "not_finite_UNIV_disjI";
   1.369 -
   1.370 -Goal "[| ~finite(UNIV :: 'a set); \
   1.371 -\                 finite (X :: 'a set) \
   1.372 -\              |] ==>  ~finite (- X)";
   1.373 -by (dres_inst_tac [("X","X")] not_finite_UNIV_disjI 1);
   1.374 -by (Blast_tac 1);
   1.375 -qed "not_finite_UNIV_Compl";
   1.376 -
   1.377 -val [prem] = goal (the_context ()) "~ finite (UNIV:: 'a set) ==> \
   1.378 -\            !X: {A:: 'a set. finite (- A)}. ~ finite X";
   1.379 -by (cut_facts_tac [prem] 1);
   1.380 -by (auto_tac (claset() addDs [not_finite_UNIV_disjI],simpset()));
   1.381 -qed "mem_cofinite_Filter_not_finite";
   1.382 -
   1.383 -val [prem] = goal (the_context ()) "~ finite (UNIV:: 'a set) ==> \
   1.384 -\            {A:: 'a set. finite (- A)} : Freefilter UNIV";
   1.385 -by (cut_facts_tac [prem] 1);
   1.386 -by (rtac mem_FreefiltersetI2 1);
   1.387 -by (rtac cofinite_Filter 1 THEN assume_tac 1);
   1.388 -by (blast_tac (claset() addSDs [mem_cofinite_Filter_not_finite]) 1);
   1.389 -qed "cofinite_Freefilter";
   1.390 -
   1.391 -Goal "UNIV - x = - x";
   1.392 -by (Auto_tac);
   1.393 -qed "UNIV_diff_Compl";
   1.394 -Addsimps [UNIV_diff_Compl];
   1.395 -
   1.396 -Goalw [Ultrafilter_def,FreeUltrafilter_def]
   1.397 -     "[| ~finite(UNIV :: 'a set); (U :: 'a set set): FreeUltrafilter UNIV\
   1.398 -\         |] ==> {X. finite(- X)} <= U";
   1.399 -by (ftac cofinite_Filter 1);
   1.400 -by (Step_tac 1);
   1.401 -by (forw_inst_tac [("X","- x :: 'a set")] not_finite_UNIV_Compl 1);
   1.402 -by (assume_tac 1);
   1.403 -by (Step_tac 1 THEN Fast_tac 1);
   1.404 -by (dres_inst_tac [("x","x")] bspec 1);
   1.405 -by (Blast_tac 1);
   1.406 -by (asm_full_simp_tac (simpset() addsimps [UNIV_diff_Compl]) 1);
   1.407 -qed "FreeUltrafilter_contains_cofinite_set";
   1.408 -
   1.409 -(*--------------------------------------------------------------------
   1.410 -   We prove: 1. Existence of maximal filter i.e. ultrafilter
   1.411 -             2. Freeness property i.e ultrafilter is free
   1.412 -             Use a locale to prove various lemmas and then 
   1.413 -             export main result: The Ultrafilter Theorem
   1.414 - -------------------------------------------------------------------*)
   1.415 -Open_locale "UFT"; 
   1.416 -
   1.417 -Goalw [chain_def, thm "superfrechet_def", thm "frechet_def"]
   1.418 -   "!!(c :: 'a set set set). c : chain (superfrechet S) ==>  Union c <= Pow S";
   1.419 -by (Step_tac 1);
   1.420 -by (dtac subsetD 1 THEN assume_tac 1);
   1.421 -by (Step_tac 1);
   1.422 -by (dres_inst_tac [("X","X")] mem_FiltersetD3 1);
   1.423 -by (Auto_tac);
   1.424 -qed "chain_Un_subset_Pow";
   1.425 -
   1.426 -Goalw [chain_def,Filter_def,is_Filter_def,
   1.427 -           thm "superfrechet_def", thm "frechet_def"] 
   1.428 -          "!!(c :: 'a set set set). c: chain (superfrechet S) \
   1.429 -\         ==> !x: c. {} < x";
   1.430 -by (blast_tac (claset() addSIs [psubsetI]) 1);
   1.431 -qed "mem_chain_psubset_empty";
   1.432 -
   1.433 -Goal "!!(c :: 'a set set set). \
   1.434 -\            [| c: chain (superfrechet S);\
   1.435 -\               c ~= {} \
   1.436 -\            |]\
   1.437 -\            ==> Union(c) ~= {}";
   1.438 -by (dtac mem_chain_psubset_empty 1);
   1.439 -by (Step_tac 1);
   1.440 -by (dtac bspec 1 THEN assume_tac 1);
   1.441 -by (auto_tac (claset() addDs [Union_upper,bspec],
   1.442 -    simpset() addsimps [psubset_def]));
   1.443 -qed "chain_Un_not_empty";
   1.444 -
   1.445 -Goalw [is_Filter_def,Filter_def,chain_def,thm "superfrechet_def"] 
   1.446 -           "!!(c :: 'a set set set). \
   1.447 -\           c : chain (superfrechet S)  \
   1.448 -\           ==> {} ~: Union(c)";
   1.449 -by (Blast_tac 1);
   1.450 -qed "Filter_empty_not_mem_Un";
   1.451 -
   1.452 -Goal "c: chain (superfrechet S) \
   1.453 -\         ==> ALL u : Union(c). ALL v: Union(c). u Int v : Union(c)";
   1.454 -by (Step_tac 1);
   1.455 -by (forw_inst_tac [("x","X"),("y","Xa")] chainD 1);
   1.456 -by (REPEAT(assume_tac 1));
   1.457 -by (dtac chainD2 1);
   1.458 -by (etac disjE 1);
   1.459 -by (res_inst_tac [("X","Xa")] UnionI 1 THEN assume_tac 1);
   1.460 -by (dres_inst_tac [("A","X")] subsetD 1 THEN assume_tac 1);
   1.461 -by (dres_inst_tac [("c","Xa")] subsetD 1 THEN assume_tac 1);
   1.462 -by (res_inst_tac [("X","X")] UnionI 2 THEN assume_tac 2);
   1.463 -by (dres_inst_tac [("A","Xa")] subsetD 2 THEN assume_tac 2);
   1.464 -by (dres_inst_tac [("c","X")] subsetD 2 THEN assume_tac 2);
   1.465 -by (auto_tac (claset() addIs [mem_FiltersetD1], 
   1.466 -     simpset() addsimps [thm "superfrechet_def"]));
   1.467 -qed "Filter_Un_Int";
   1.468 -
   1.469 -Goal "c: chain (superfrechet S) \
   1.470 -\         ==> ALL u v. u: Union(c) & \
   1.471 -\                 (u :: 'a set) <= v & v <= S --> v: Union(c)";
   1.472 -by (Step_tac 1);
   1.473 -by (dtac chainD2 1);
   1.474 -by (dtac subsetD 1 THEN assume_tac 1);
   1.475 -by (rtac UnionI 1 THEN assume_tac 1);
   1.476 -by (auto_tac (claset() addIs [mem_FiltersetD2], 
   1.477 -     simpset() addsimps [thm "superfrechet_def"]));
   1.478 -qed "Filter_Un_subset";
   1.479 -
   1.480 -Goalw [chain_def,thm "superfrechet_def"]
   1.481 -      "!!(c :: 'a set set set). \
   1.482 -\            [| c: chain (superfrechet S);\
   1.483 -\               x: c \
   1.484 -\            |] ==> x : Filter S";
   1.485 -by (Blast_tac 1);
   1.486 -qed "lemma_mem_chain_Filter";
   1.487 -
   1.488 -Goalw [chain_def,thm "superfrechet_def"]
   1.489 -     "!!(c :: 'a set set set). \
   1.490 -\            [| c: chain (superfrechet S);\
   1.491 -\               x: c \
   1.492 -\            |] ==> frechet S <= x";
   1.493 -by (Blast_tac 1);
   1.494 -qed "lemma_mem_chain_frechet_subset";
   1.495 -
   1.496 -Goal "!!(c :: 'a set set set). \
   1.497 -\         [| c ~= {}; \
   1.498 -\            c : chain (superfrechet (UNIV :: 'a set))\
   1.499 -\         |] ==> Union c : superfrechet (UNIV)";
   1.500 -by (simp_tac (simpset() addsimps 
   1.501 -    [thm "superfrechet_def",thm "frechet_def"]) 1);
   1.502 -by (Step_tac 1);
   1.503 -by (rtac mem_FiltersetI2 1);
   1.504 -by (etac chain_Un_subset_Pow 1);
   1.505 -by (rtac UnionI 1 THEN assume_tac 1);
   1.506 -by (etac (lemma_mem_chain_Filter RS mem_FiltersetD4) 1 THEN assume_tac 1);
   1.507 -by (etac chain_Un_not_empty 1);
   1.508 -by (etac Filter_empty_not_mem_Un 2);
   1.509 -by (etac Filter_Un_Int 2);
   1.510 -by (etac Filter_Un_subset 2);
   1.511 -by (subgoal_tac "xa : frechet (UNIV)" 2);
   1.512 -by (rtac UnionI 2 THEN assume_tac 2);
   1.513 -by (rtac (lemma_mem_chain_frechet_subset RS subsetD) 2);
   1.514 -by (auto_tac (claset(),simpset() addsimps [thm "frechet_def"]));
   1.515 -qed "Un_chain_mem_cofinite_Filter_set";
   1.516 -
   1.517 -Goal "EX U: superfrechet (UNIV). \
   1.518 -\               ALL G: superfrechet (UNIV). U <= G --> U = G";
   1.519 -by (rtac Zorn_Lemma2 1);
   1.520 -by (cut_facts_tac [thm "not_finite_UNIV" RS cofinite_Filter] 1);
   1.521 -by (Step_tac 1);
   1.522 -by (res_inst_tac [("Q","c={}")] (excluded_middle RS disjE) 1);
   1.523 -by (res_inst_tac [("x","Union c")] bexI 1 THEN Blast_tac 1);
   1.524 -by (rtac Un_chain_mem_cofinite_Filter_set 1 THEN REPEAT(assume_tac 1));
   1.525 -by (res_inst_tac [("x","frechet (UNIV)")] bexI 1 THEN Blast_tac 1);
   1.526 -by (auto_tac (claset(),
   1.527 -	      simpset() addsimps 
   1.528 -	      [thm "superfrechet_def", thm "frechet_def"]));
   1.529 -qed "max_cofinite_Filter_Ex";
   1.530 -
   1.531 -Goal "EX U: superfrechet UNIV. (\
   1.532 -\               ALL G: superfrechet UNIV. U <= G --> U = G) \ 
   1.533 -\                             & (ALL x: U. ~finite x)";
   1.534 -by (cut_facts_tac [thm "not_finite_UNIV" RS 
   1.535 -         (export max_cofinite_Filter_Ex)] 1);
   1.536 -by (Step_tac 1);
   1.537 -by (res_inst_tac [("x","U")] bexI 1);
   1.538 -by (auto_tac (claset(),simpset() addsimps 
   1.539 -        [thm "superfrechet_def", thm "frechet_def"]));
   1.540 -by (dres_inst_tac [("c","- x")] subsetD 1);
   1.541 -by (Asm_simp_tac 1);
   1.542 -by (forw_inst_tac [("A","x"),("B","- x")] mem_FiltersetD1 1);
   1.543 -by (dtac Filter_empty_not_mem 3);
   1.544 -by (ALLGOALS(Asm_full_simp_tac ));
   1.545 -qed "max_cofinite_Freefilter_Ex";
   1.546 -
   1.547 -(*--------------------------------------------------------------------------------
   1.548 -               There exists a free ultrafilter on any infinite set
   1.549 - --------------------------------------------------------------------------------*)
   1.550 -
   1.551 -Goalw [FreeUltrafilter_def] "EX U. U: FreeUltrafilter (UNIV :: 'a set)";
   1.552 -by (cut_facts_tac [thm "not_finite_UNIV" RS (export max_cofinite_Freefilter_Ex)] 1);
   1.553 -by (asm_full_simp_tac (simpset() addsimps 
   1.554 -    [thm "superfrechet_def", Ultrafilter_iff, thm "frechet_def"]) 1);
   1.555 -by (Step_tac 1);
   1.556 -by (res_inst_tac [("x","U")] exI 1);
   1.557 -by (Step_tac 1);
   1.558 -by (Blast_tac 1);
   1.559 -qed "FreeUltrafilter_ex";
   1.560 -
   1.561 -bind_thm ("FreeUltrafilter_Ex", export FreeUltrafilter_ex);
   1.562 -
   1.563 -Close_locale "UFT";