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