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