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