src/HOL/Real/Hyperreal/Filter.ML
author paulson
Fri Dec 11 10:41:53 1998 +0100 (1998-12-11)
changeset 6024 cb87f103d114
parent 5979 11cbf236ca16
child 7127 48e235179ffb
permissions -rw-r--r--
new Close_locale synatx
     1 (*  Title       : Filter.ML
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 1998  University of Cambridge
     4     Description : Filters and Ultrafilter
     5 *) 
     6 
     7 open Filter;
     8 
     9 
    10 (*------------------------------------------------------------------
    11       Properties of Filters and Freefilters - 
    12       rules for intro, destruction etc.
    13  ------------------------------------------------------------------*)
    14 
    15 Goalw [is_Filter_def] "is_Filter X S ==> X <= Pow(S)";
    16 by (Blast_tac 1);
    17 qed "is_FilterD1";
    18 
    19 Goalw [is_Filter_def] "is_Filter X S ==> X ~= {}";
    20 by (Blast_tac 1);
    21 qed "is_FilterD2";
    22 
    23 Goalw [is_Filter_def] "is_Filter X S ==> {} ~: X";
    24 by (Blast_tac 1);
    25 qed "is_FilterD3";
    26 
    27 Goalw [Filter_def] "is_Filter X S ==> X : Filter S";
    28 by (Blast_tac 1);
    29 qed "mem_FiltersetI";
    30 
    31 Goalw [Filter_def] "X : Filter S ==> is_Filter X S";
    32 by (Blast_tac 1);
    33 qed "mem_FiltersetD";
    34 
    35 Goal "X : Filter S ==> {} ~: X";
    36 by (etac (mem_FiltersetD RS is_FilterD3) 1);
    37 qed "Filter_empty_not_mem";
    38 
    39 bind_thm ("Filter_empty_not_memE",(Filter_empty_not_mem RS notE));
    40 
    41 Goalw [Filter_def,is_Filter_def] 
    42       "[| X: Filter S; A: X; B: X |] ==> A Int B : X";
    43 by (Blast_tac 1);
    44 qed "mem_FiltersetD1";
    45 
    46 Goalw [Filter_def,is_Filter_def] 
    47       "[| X: Filter S; A: X; A <= B; B <= S|] ==> B : X";
    48 by (Blast_tac 1);
    49 qed "mem_FiltersetD2";
    50 
    51 Goalw [Filter_def,is_Filter_def] 
    52       "[| X: Filter S; A: X |] ==> A : Pow S";
    53 by (Blast_tac 1);
    54 qed "mem_FiltersetD3";
    55 
    56 Goalw [Filter_def,is_Filter_def] 
    57       "X: Filter S  ==> S : X";
    58 by (Blast_tac 1);
    59 qed "mem_FiltersetD4";
    60 
    61 Goalw [is_Filter_def] 
    62       "[| X <= Pow(S);\
    63 \              S : X; \
    64 \              X ~= {}; \
    65 \              {} ~: X; \
    66 \              ALL u: X. ALL v: X. u Int v : X; \
    67 \              ALL u v. u: X & u<=v & v<=S --> v: X \
    68 \           |] ==> is_Filter X S";
    69 by (Blast_tac 1); 
    70 qed "is_FilterI";
    71 
    72 Goal "[| X <= Pow(S);\
    73 \              S : X; \
    74 \              X ~= {}; \
    75 \              {} ~: X; \
    76 \              ALL u: X. ALL v: X. u Int v : X; \
    77 \              ALL u v. u: X & u<=v & v<=S --> v: X \
    78 \           |] ==> X: Filter S";
    79 by (blast_tac (claset() addIs [mem_FiltersetI,is_FilterI]) 1);
    80 qed "mem_FiltersetI2";
    81 
    82 Goalw [is_Filter_def]
    83       "is_Filter X S ==> X <= Pow(S) & \
    84 \                          S : X & \
    85 \                          X ~= {} & \
    86 \                          {} ~: X  & \
    87 \                          (ALL u: X. ALL v: X. u Int v : X) & \
    88 \                          (ALL u v. u: X & u <= v & v<=S --> v: X)";
    89 by (Fast_tac 1);
    90 qed "is_FilterE_lemma";
    91 
    92 Goalw [is_Filter_def]
    93       "X : Filter S ==> X <= Pow(S) &\
    94 \                          S : X & \
    95 \                          X ~= {} & \
    96 \                          {} ~: X  & \
    97 \                          (ALL u: X. ALL v: X. u Int v : X) & \
    98 \                          (ALL u v. u: X & u <= v & v<=S --> v: X)";
    99 by (etac (mem_FiltersetD RS is_FilterE_lemma) 1);
   100 qed "memFiltersetE_lemma";
   101 
   102 Goalw [Filter_def,Freefilter_def] 
   103       "X: Freefilter S ==> X: Filter S";
   104 by (Fast_tac 1);
   105 qed "Freefilter_Filter";
   106 
   107 Goalw [Freefilter_def] 
   108       "X: Freefilter S ==> ALL y: X. ~finite(y)";
   109 by (Blast_tac 1);
   110 qed "mem_Freefilter_not_finite";
   111 
   112 Goal "[| X: Freefilter S; x: X |] ==> ~ finite x";
   113 by (blast_tac (claset() addSDs [mem_Freefilter_not_finite]) 1);
   114 qed "mem_FreefiltersetD1";
   115 
   116 bind_thm ("mem_FreefiltersetE1", (mem_FreefiltersetD1 RS notE));
   117 
   118 Goal "[| X: Freefilter S; finite x|] ==> x ~: X";
   119 by (blast_tac (claset() addSDs [mem_Freefilter_not_finite]) 1);
   120 qed "mem_FreefiltersetD2";
   121 
   122 Goalw [Freefilter_def] 
   123       "[| X: Filter S; ALL x. ~(x: X & finite x) |] ==> X: Freefilter S";
   124 by (Blast_tac 1);
   125 qed "mem_FreefiltersetI1";
   126 
   127 Goalw [Freefilter_def]
   128       "[| X: Filter S; ALL x. (x ~: X | ~ finite x) |] ==> X: Freefilter S";
   129 by (Blast_tac 1);
   130 qed "mem_FreefiltersetI2";
   131 
   132 Goal "[| X: Filter S; A: X; B: X |] ==> A Int B ~= {}";
   133 by (forw_inst_tac [("A","A"),("B","B")] mem_FiltersetD1 1);
   134 by (auto_tac (claset() addSDs [Filter_empty_not_mem],simpset()));
   135 qed "Filter_Int_not_empty";
   136 
   137 bind_thm ("Filter_Int_not_emptyE",(Filter_Int_not_empty RS notE));
   138 
   139 (*----------------------------------------------------------------------------------
   140               Ultrafilters and Free ultrafilters
   141  ----------------------------------------------------------------------------------*)
   142 
   143 Goalw [Ultrafilter_def] "X : Ultrafilter S ==> X: Filter S";
   144 by (Blast_tac 1);
   145 qed "Ultrafilter_Filter";
   146 
   147 Goalw [Ultrafilter_def] 
   148       "X : Ultrafilter S ==> !A: Pow(S). A : X | S - A: X";
   149 by (Blast_tac 1);
   150 qed "mem_UltrafiltersetD2";
   151 
   152 Goalw [Ultrafilter_def] 
   153       "[|X : Ultrafilter S; A <= S; A ~: X |] ==> S - A: X";
   154 by (Blast_tac 1);
   155 qed "mem_UltrafiltersetD3";
   156 
   157 Goalw [Ultrafilter_def] 
   158       "[|X : Ultrafilter S; A <= S; S - A ~: X |] ==> A: X";
   159 by (Blast_tac 1);
   160 qed "mem_UltrafiltersetD4";
   161 
   162 Goalw [Ultrafilter_def]
   163      "[| X: Filter S; \
   164 \             ALL A: Pow(S). A: X | S - A : X |] ==> X: Ultrafilter S";
   165 by (Blast_tac 1);
   166 qed "mem_UltrafiltersetI";
   167 
   168 Goalw [Ultrafilter_def,FreeUltrafilter_def]
   169      "X: FreeUltrafilter S ==> X: Ultrafilter S";
   170 by (Blast_tac 1);
   171 qed "FreeUltrafilter_Ultrafilter";
   172 
   173 Goalw [FreeUltrafilter_def]
   174      "X: FreeUltrafilter S ==> ALL y: X. ~finite(y)";
   175 by (Blast_tac 1);
   176 qed "mem_FreeUltrafilter_not_finite";
   177 
   178 Goal "[| X: FreeUltrafilter S; x: X |] ==> ~ finite x";
   179 by (blast_tac (claset() addSDs [mem_FreeUltrafilter_not_finite]) 1);
   180 qed "mem_FreeUltrafiltersetD1";
   181 
   182 bind_thm ("mem_FreeUltrafiltersetE1", (mem_FreeUltrafiltersetD1 RS notE));
   183 
   184 Goal "[| X: FreeUltrafilter S; finite x|] ==> x ~: X";
   185 by (blast_tac (claset() addSDs [mem_FreeUltrafilter_not_finite]) 1);
   186 qed "mem_FreeUltrafiltersetD2";
   187 
   188 Goalw [FreeUltrafilter_def] 
   189       "[| X: Ultrafilter S; \
   190 \              ALL x. ~(x: X & finite x) |] ==> X: FreeUltrafilter S";
   191 by (Blast_tac 1);
   192 qed "mem_FreeUltrafiltersetI1";
   193 
   194 Goalw [FreeUltrafilter_def]
   195       "[| X: Ultrafilter S; \
   196 \              ALL x. (x ~: X | ~ finite x) |] ==> X: FreeUltrafilter S";
   197 by (Blast_tac 1);
   198 qed "mem_FreeUltrafiltersetI2";
   199 
   200 Goalw [FreeUltrafilter_def,Freefilter_def,Ultrafilter_def]
   201      "(X: FreeUltrafilter S) = (X: Freefilter S & (ALL x:Pow(S). x: X | S - x: X))";
   202 by (Blast_tac 1);
   203 qed "FreeUltrafilter_iff";
   204 
   205 (*-------------------------------------------------------------------
   206    A Filter F on S is an ultrafilter iff it is a maximal filter 
   207    i.e. whenever G is a filter on I and F <= F then F = G
   208  --------------------------------------------------------------------*)
   209 (*---------------------------------------------------------------------
   210   lemmas that shows existence of an extension to what was assumed to
   211   be a maximal filter. Will be used to derive contradiction in proof of
   212   property of ultrafilter 
   213  ---------------------------------------------------------------------*)
   214 Goal "[| F ~= {}; A <= S |] ==> \
   215 \        EX x. x: {X. X <= S & (EX f:F. A Int f <= X)}";
   216 by (Blast_tac 1);
   217 qed "lemma_set_extend";
   218 
   219 Goal "a: X ==> X ~= {}";
   220 by (Step_tac 1);
   221 qed "lemma_set_not_empty";
   222 
   223 Goal "x Int F <= {} ==> F <= - x";
   224 by (Blast_tac 1);
   225 qed "lemma_empty_Int_subset_Compl";
   226 
   227 Goalw [Filter_def,is_Filter_def]
   228       "[| F: Filter S; A ~: F; A <= S|] \
   229 \          ==> ALL B. B ~: F | ~ B <= A";
   230 by (Blast_tac 1);
   231 qed "mem_Filterset_disjI";
   232 
   233 Goal "F : Ultrafilter S ==> \
   234 \         (F: Filter S & (ALL G: Filter S. F <= G --> F = G))";
   235 by (auto_tac (claset(),simpset() addsimps [Ultrafilter_def]));
   236 by (dres_inst_tac [("x","x")] bspec 1);
   237 by (etac mem_FiltersetD3 1 THEN assume_tac 1);
   238 by (Step_tac 1);
   239 by (dtac subsetD 1 THEN assume_tac 1);
   240 by (blast_tac (claset() addSDs [Filter_Int_not_empty]) 1);
   241 qed "Ultrafilter_max_Filter";
   242 
   243 
   244 (*--------------------------------------------------------------------------------
   245      This is a very long and tedious proof; need to break it into parts.
   246      Have proof that {X. X <= S & (EX f: F. A Int f <= X)} is a filter as 
   247      a lemma
   248 --------------------------------------------------------------------------------*)
   249 Goalw [Ultrafilter_def] 
   250       "[| F: Filter S; \
   251 \              ALL G: Filter S. F <= G --> F = G |] ==> F : Ultrafilter S";
   252 by (Step_tac 1);
   253 by (rtac ccontr 1);
   254 by (forward_tac [mem_FiltersetD RS is_FilterD2] 1);
   255 by (forw_inst_tac [("x","{X. X <= S & (EX f: F. A Int f <= X)}")] bspec 1);
   256 by (EVERY1[rtac mem_FiltersetI2, Blast_tac, Asm_full_simp_tac]);
   257 by (blast_tac (claset() addDs [mem_FiltersetD3]) 1);
   258 by (etac (lemma_set_extend RS exE) 1);
   259 by (assume_tac 1 THEN etac lemma_set_not_empty 1);
   260 by (REPEAT(rtac ballI 2) THEN Asm_full_simp_tac 2);
   261 by (rtac conjI 2 THEN Blast_tac 2);
   262 by (REPEAT(etac conjE 2) THEN REPEAT(etac bexE 2));
   263 by (res_inst_tac [("x","f Int fa")] bexI 2);
   264 by (etac mem_FiltersetD1 3);
   265 by (assume_tac 3 THEN assume_tac 3);
   266 by (Fast_tac 2);
   267 by (EVERY[REPEAT(rtac allI 2), rtac impI 2,Asm_full_simp_tac 2]);
   268 by (EVERY[REPEAT(etac conjE 2), etac bexE 2]);
   269 by (res_inst_tac [("x","f")] bexI 2);
   270 by (rtac subsetI 2);
   271 by (Fast_tac 2 THEN assume_tac 2);
   272 by (Step_tac 2);
   273 by (Blast_tac 3);
   274 by (eres_inst_tac [("c","A")] equalityCE 3);
   275 by (REPEAT(Blast_tac 3));
   276 by (dres_inst_tac [("A","xa")] mem_FiltersetD3 2 THEN assume_tac 2);
   277 by (Blast_tac 2);
   278 by (dtac lemma_empty_Int_subset_Compl 1);
   279 by (EVERY1[forward_tac [mem_Filterset_disjI], assume_tac, Fast_tac]);
   280 by (dtac mem_FiltersetD3 1 THEN assume_tac 1);
   281 by (dres_inst_tac [("x","f")] spec 1);
   282 by (Blast_tac 1);
   283 qed "max_Filter_Ultrafilter";
   284 
   285 Goal "(F : Ultrafilter S) = (F: Filter S & (ALL G: Filter S. F <= G --> F = G))";
   286 by (blast_tac (claset() addSIs [Ultrafilter_max_Filter,max_Filter_Ultrafilter]) 1);
   287 qed "Ultrafilter_iff";
   288 
   289 (*--------------------------------------------------------------------
   290              A few properties of freefilters
   291  -------------------------------------------------------------------*)
   292 
   293 Goal "F1 Int F2 = ((F1 Int Y) Int F2) Un ((F2 Int - Y) Int F1)";
   294 by (Auto_tac);
   295 qed "lemma_Compl_cancel_eq";
   296 
   297 Goal "finite X ==> finite (X Int Y)";
   298 by (etac (Int_lower1 RS finite_subset) 1);
   299 qed "finite_IntI1";
   300 
   301 Goal "finite Y ==> finite (X Int Y)";
   302 by (etac (Int_lower2 RS finite_subset) 1);
   303 qed "finite_IntI2";
   304 
   305 Goal "[| finite (F1 Int Y); \
   306 \                 finite (F2 Int - Y) \
   307 \              |] ==> finite (F1 Int F2)";
   308 by (res_inst_tac [("Y1","Y")] (lemma_Compl_cancel_eq RS ssubst) 1);
   309 by (rtac finite_UnI 1);
   310 by (auto_tac (claset() addSIs [finite_IntI1,finite_IntI2],simpset()));
   311 qed "finite_Int_Compl_cancel";
   312 
   313 Goal "U: Freefilter S  ==> \
   314 \         ~ (EX f1: U. EX f2: U. finite (f1 Int x) \
   315 \                            & finite (f2 Int (- x)))";
   316 by (Step_tac 1);
   317 by (forw_inst_tac [("A","f1"),("B","f2")] 
   318     (Freefilter_Filter RS mem_FiltersetD1) 1);
   319 by (dres_inst_tac [("x","f1 Int f2")] mem_FreefiltersetD1 3);
   320 by (dtac finite_Int_Compl_cancel 4);
   321 by (Auto_tac);
   322 qed "Freefilter_lemma_not_finite";
   323 
   324 (* the lemmas below follow *)
   325 Goal "U: Freefilter S ==> \
   326 \          ALL f: U. ~ finite (f Int x) | ~finite (f Int (- x))";
   327 by (blast_tac (claset() addSDs [Freefilter_lemma_not_finite,bspec]) 1);
   328 qed "Freefilter_Compl_not_finite_disjI";
   329 
   330 Goal "U: Freefilter S ==> \
   331 \          (ALL f: U. ~ finite (f Int x)) | (ALL f:U. ~finite (f Int (- x)))";
   332 by (blast_tac (claset() addSDs [Freefilter_lemma_not_finite,bspec]) 1);
   333 qed "Freefilter_Compl_not_finite_disjI2";
   334 
   335 Goal "- UNIV = {}";
   336 by (Auto_tac );
   337 qed "Compl_UNIV_eq";
   338 
   339 Addsimps [Compl_UNIV_eq];
   340 
   341 Goal "- {} = UNIV";
   342 by (Auto_tac );
   343 qed "Compl_empty_eq";
   344 
   345 Addsimps [Compl_empty_eq];
   346 
   347 val [prem] = goal thy "~ finite (UNIV:: 'a set) ==> \
   348 \            {A:: 'a set. finite (- A)} : Filter UNIV";
   349 by (cut_facts_tac [prem] 1);
   350 by (rtac mem_FiltersetI2 1);
   351 by (auto_tac (claset(),simpset() addsimps [Compl_Int]));
   352 by (eres_inst_tac [("c","UNIV")] equalityCE 1);
   353 by (Auto_tac);
   354 by (etac (Compl_anti_mono RS finite_subset) 1);
   355 by (assume_tac 1);
   356 qed "cofinite_Filter";
   357 
   358 Goal "~finite(UNIV :: 'a set) ==> ~finite (X :: 'a set) | ~finite (- X)";
   359 by (dres_inst_tac [("A1","X")] (Compl_partition RS ssubst) 1);
   360 by (Asm_full_simp_tac 1); 
   361 qed "not_finite_UNIV_disjI";
   362 
   363 Goal "[| ~finite(UNIV :: 'a set); \
   364 \                 finite (X :: 'a set) \
   365 \              |] ==>  ~finite (- X)";
   366 by (dres_inst_tac [("X","X")] not_finite_UNIV_disjI 1);
   367 by (Blast_tac 1);
   368 qed "not_finite_UNIV_Compl";
   369 
   370 val [prem] = goal thy "~ finite (UNIV:: 'a set) ==> \
   371 \            !X: {A:: 'a set. finite (- A)}. ~ finite X";
   372 by (cut_facts_tac [prem] 1);
   373 by (auto_tac (claset() addDs [not_finite_UNIV_disjI],simpset()));
   374 qed "mem_cofinite_Filter_not_finite";
   375 
   376 val [prem] = goal thy "~ finite (UNIV:: 'a set) ==> \
   377 \            {A:: 'a set. finite (- A)} : Freefilter UNIV";
   378 by (cut_facts_tac [prem] 1);
   379 by (rtac mem_FreefiltersetI2 1);
   380 by (rtac cofinite_Filter 1 THEN assume_tac 1);
   381 by (blast_tac (claset() addSDs [mem_cofinite_Filter_not_finite]) 1);
   382 qed "cofinite_Freefilter";
   383 
   384 Goal "UNIV - x = - x";
   385 by (Auto_tac);
   386 qed "UNIV_diff_Compl";
   387 Addsimps [UNIV_diff_Compl];
   388 
   389 Goalw [Ultrafilter_def,FreeUltrafilter_def]
   390      "[| ~finite(UNIV :: 'a set); (U :: 'a set set): FreeUltrafilter UNIV\
   391 \         |] ==> {X. finite(- X)} <= U";
   392 by (forward_tac [cofinite_Filter] 1);
   393 by (Step_tac 1);
   394 by (forw_inst_tac [("X","- x :: 'a set")] not_finite_UNIV_Compl 1);
   395 by (assume_tac 1);
   396 by (Step_tac 1 THEN Fast_tac 1);
   397 by (dres_inst_tac [("x","x")] bspec 1);
   398 by (Blast_tac 1);
   399 by (asm_full_simp_tac (simpset() addsimps [UNIV_diff_Compl]) 1);
   400 qed "FreeUltrafilter_contains_cofinite_set";
   401 
   402 (*--------------------------------------------------------------------
   403    We prove: 1. Existence of maximal filter i.e. ultrafilter
   404              2. Freeness property i.e ultrafilter is free
   405              Use a locale to prove various lemmas and then 
   406              export main result- The Ultrafilter Theorem
   407  -------------------------------------------------------------------*)
   408 Open_locale "UFT"; 
   409 
   410 Goalw [chain_def, thm "superfrechet_def", thm "frechet_def"]
   411    "!!(c :: 'a set set set). c : chain (superfrechet S) ==>  Union c <= Pow S";
   412 by (Step_tac 1);
   413 by (dtac subsetD 1 THEN assume_tac 1);
   414 by (Step_tac 1);
   415 by (dres_inst_tac [("X","X")] mem_FiltersetD3 1);
   416 by (Auto_tac);
   417 qed "chain_Un_subset_Pow";
   418 
   419 Goalw [chain_def,Filter_def,is_Filter_def,
   420            thm "superfrechet_def", thm "frechet_def"] 
   421           "!!(c :: 'a set set set). c: chain (superfrechet S) \
   422 \         ==> !x: c. {} < x";
   423 by (blast_tac (claset() addSIs [psubsetI]) 1);
   424 qed "mem_chain_psubset_empty";
   425 
   426 Goal "!!(c :: 'a set set set). \
   427 \            [| c: chain (superfrechet S);\
   428 \               c ~= {} \
   429 \            |]\
   430 \            ==> Union(c) ~= {}";
   431 by (dtac mem_chain_psubset_empty 1);
   432 by (Step_tac 1);
   433 by (dtac bspec 1 THEN assume_tac 1);
   434 by (auto_tac (claset() addDs [Union_upper,bspec],
   435     simpset() addsimps [psubset_def]));
   436 qed "chain_Un_not_empty";
   437 
   438 Goalw [is_Filter_def,Filter_def,chain_def,thm "superfrechet_def"] 
   439            "!!(c :: 'a set set set). \
   440 \           c : chain (superfrechet S)  \
   441 \           ==> {} ~: Union(c)";
   442 by (Blast_tac 1);
   443 qed "Filter_empty_not_mem_Un";
   444 
   445 Goal "c: chain (superfrechet S) \
   446 \         ==> ALL u : Union(c). ALL v: Union(c). u Int v : Union(c)";
   447 by (Step_tac 1);
   448 by (forw_inst_tac [("x","X"),("y","Xa")] chainD 1);
   449 by (REPEAT(assume_tac 1));
   450 by (dtac chainD2 1);
   451 by (etac disjE 1);
   452 by (res_inst_tac [("X","Xa")] UnionI 1 THEN assume_tac 1);
   453 by (dres_inst_tac [("A","X")] subsetD 1 THEN assume_tac 1);
   454 by (dres_inst_tac [("c","Xa")] subsetD 1 THEN assume_tac 1);
   455 by (res_inst_tac [("X","X")] UnionI 2 THEN assume_tac 2);
   456 by (dres_inst_tac [("A","Xa")] subsetD 2 THEN assume_tac 2);
   457 by (dres_inst_tac [("c","X")] subsetD 2 THEN assume_tac 2);
   458 by (auto_tac (claset() addIs [mem_FiltersetD1], 
   459      simpset() addsimps [thm "superfrechet_def"]));
   460 qed "Filter_Un_Int";
   461 
   462 Goal "c: chain (superfrechet S) \
   463 \         ==> ALL u v. u: Union(c) & \
   464 \                 (u :: 'a set) <= v & v <= S --> v: Union(c)";
   465 by (Step_tac 1);
   466 by (dtac chainD2 1);
   467 by (dtac subsetD 1 THEN assume_tac 1);
   468 by (rtac UnionI 1 THEN assume_tac 1);
   469 by (auto_tac (claset() addIs [mem_FiltersetD2], 
   470      simpset() addsimps [thm "superfrechet_def"]));
   471 qed "Filter_Un_subset";
   472 
   473 Goalw [chain_def,thm "superfrechet_def"]
   474       "!!(c :: 'a set set set). \
   475 \            [| c: chain (superfrechet S);\
   476 \               x: c \
   477 \            |] ==> x : Filter S";
   478 by (Blast_tac 1);
   479 qed "lemma_mem_chain_Filter";
   480 
   481 Goalw [chain_def,thm "superfrechet_def"]
   482      "!!(c :: 'a set set set). \
   483 \            [| c: chain (superfrechet S);\
   484 \               x: c \
   485 \            |] ==> frechet S <= x";
   486 by (Blast_tac 1);
   487 qed "lemma_mem_chain_frechet_subset";
   488 
   489 Goal "!!(c :: 'a set set set). \
   490 \         [| c ~= {}; \
   491 \            c : chain (superfrechet (UNIV :: 'a set))\
   492 \         |] ==> Union c : superfrechet (UNIV)";
   493 by (simp_tac (simpset() addsimps 
   494     [thm "superfrechet_def",thm "frechet_def"]) 1);
   495 by (Step_tac 1);
   496 by (rtac mem_FiltersetI2 1);
   497 by (etac chain_Un_subset_Pow 1);
   498 by (rtac UnionI 1 THEN assume_tac 1);
   499 by (etac (lemma_mem_chain_Filter RS mem_FiltersetD4) 1 THEN assume_tac 1);
   500 by (etac chain_Un_not_empty 1);
   501 by (etac Filter_empty_not_mem_Un 2);
   502 by (etac Filter_Un_Int 2);
   503 by (etac Filter_Un_subset 2);
   504 by (subgoal_tac "xa : frechet (UNIV)" 2);
   505 by (rtac UnionI 2 THEN assume_tac 2);
   506 by (rtac (lemma_mem_chain_frechet_subset RS subsetD) 2);
   507 by (auto_tac (claset(),simpset() addsimps [thm "frechet_def"]));
   508 qed "Un_chain_mem_cofinite_Filter_set";
   509 
   510 Goal "EX U: superfrechet (UNIV). \
   511 \               ALL G: superfrechet (UNIV). U <= G --> U = G";
   512 by (rtac Zorn_Lemma2 1);
   513 by (cut_facts_tac [thm "not_finite_UNIV" RS cofinite_Filter] 1);
   514 by (Step_tac 1);
   515 by (res_inst_tac [("Q","c={}")] (excluded_middle RS disjE) 1);
   516 by (res_inst_tac [("x","Union c")] bexI 1 THEN Blast_tac 1);
   517 by (rtac Un_chain_mem_cofinite_Filter_set 1 THEN REPEAT(assume_tac 1));
   518 by (res_inst_tac [("x","frechet (UNIV)")] bexI 1 THEN Blast_tac 1);
   519 by (auto_tac (claset(),simpset() addsimps 
   520         [thm "superfrechet_def", thm "frechet_def"]));
   521 qed "max_cofinite_Filter_Ex";
   522 
   523 Goal "EX U: superfrechet UNIV. (\
   524 \               ALL G: superfrechet UNIV. U <= G --> U = G) \ 
   525 \                             & (ALL x: U. ~finite x)";
   526 by (cut_facts_tac [thm "not_finite_UNIV" RS 
   527          (export max_cofinite_Filter_Ex)] 1);
   528 by (Step_tac 1);
   529 by (res_inst_tac [("x","U")] bexI 1);
   530 by (auto_tac (claset(),simpset() addsimps 
   531         [thm "superfrechet_def", thm "frechet_def"]));
   532 by (dres_inst_tac [("c","- x")] subsetD 1);
   533 by (Asm_simp_tac 1);
   534 by (forw_inst_tac [("A","x"),("B","- x")] mem_FiltersetD1 1);
   535 by (dtac Filter_empty_not_mem 3);
   536 by (ALLGOALS(Asm_full_simp_tac ));
   537 qed "max_cofinite_Freefilter_Ex";
   538 
   539 (*--------------------------------------------------------------------------------
   540                There exists a free ultrafilter on any infinite set
   541  --------------------------------------------------------------------------------*)
   542 
   543 Goalw [FreeUltrafilter_def] "EX U. U: FreeUltrafilter (UNIV :: 'a set)";
   544 by (cut_facts_tac [thm "not_finite_UNIV" RS (export max_cofinite_Freefilter_Ex)] 1);
   545 by (asm_full_simp_tac (simpset() addsimps 
   546     [thm "superfrechet_def", Ultrafilter_iff, thm "frechet_def"]) 1);
   547 by (Step_tac 1);
   548 by (res_inst_tac [("x","U")] exI 1);
   549 by (Step_tac 1);
   550 by (Blast_tac 1);
   551 qed "FreeUltrafilter_ex";
   552 
   553 val FreeUltrafilter_Ex  = export FreeUltrafilter_ex;
   554 
   555 Close_locale "UFT";
   556 
   557