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