src/HOL/NSA/Free_Ultrafilter.thy
changeset 60041 6c86d58ab0ca
parent 60036 218fcc645d22
child 61975 b4b11391c676
     1.1 --- a/src/HOL/NSA/Free_Ultrafilter.thy	Sun Apr 12 11:34:09 2015 +0200
     1.2 +++ b/src/HOL/NSA/Free_Ultrafilter.thy	Sun Apr 12 11:34:16 2015 +0200
     1.3 @@ -12,115 +12,37 @@
     1.4  
     1.5  subsection {* Definitions and basic properties *}
     1.6  
     1.7 -subsubsection {* Filters *}
     1.8 +subsubsection {* Ultrafilters *}
     1.9  
    1.10 -locale filter =
    1.11 -  fixes F :: "'a set set"
    1.12 -  assumes UNIV [iff]:  "UNIV \<in> F"
    1.13 -  assumes empty [iff]: "{} \<notin> F"
    1.14 -  assumes Int:         "\<lbrakk>u \<in> F; v \<in> F\<rbrakk> \<Longrightarrow> u \<inter> v \<in> F"
    1.15 -  assumes subset:      "\<lbrakk>u \<in> F; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> F"
    1.16 +locale ultrafilter =
    1.17 +  fixes F :: "'a filter"
    1.18 +  assumes proper: "F \<noteq> bot"
    1.19 +  assumes ultra: "eventually P F \<or> eventually (\<lambda>x. \<not> P x) F"
    1.20  begin
    1.21  
    1.22 -lemma memD: "A \<in> F \<Longrightarrow> - A \<notin> F"
    1.23 -proof
    1.24 -  assume "A \<in> F" and "- A \<in> F"
    1.25 -  hence "A \<inter> (- A) \<in> F" by (rule Int)
    1.26 -  thus "False" by simp
    1.27 -qed
    1.28 +lemma eventually_imp_frequently: "frequently P F \<Longrightarrow> eventually P F"
    1.29 +  using ultra[of P] by (simp add: frequently_def)
    1.30  
    1.31 -lemma not_memI: "- A \<in> F \<Longrightarrow> A \<notin> F"
    1.32 -by (drule memD, simp)
    1.33 +lemma frequently_eq_eventually: "frequently P F = eventually P F"
    1.34 +  using eventually_imp_frequently eventually_frequently[OF proper] ..
    1.35  
    1.36 -lemma Int_iff: "(x \<inter> y \<in> F) = (x \<in> F \<and> y \<in> F)"
    1.37 -by (auto elim: subset intro: Int)
    1.38 -
    1.39 -end
    1.40 -
    1.41 -subsubsection {* Ultrafilters *}
    1.42 +lemma eventually_disj_iff: "eventually (\<lambda>x. P x \<or> Q x) F \<longleftrightarrow> eventually P F \<or> eventually Q F"
    1.43 +  unfolding frequently_eq_eventually[symmetric] frequently_disj_iff ..
    1.44  
    1.45 -locale ultrafilter = filter +
    1.46 -  assumes ultra: "A \<in> F \<or> - A \<in> F"
    1.47 -begin
    1.48 +lemma eventually_all_iff: "eventually (\<lambda>x. \<forall>y. P x y) F = (\<forall>Y. eventually (\<lambda>x. P x (Y x)) F)"
    1.49 +  using frequently_all[of P F] by (simp add: frequently_eq_eventually)
    1.50  
    1.51 -lemma memI: "- A \<notin> F \<Longrightarrow> A \<in> F"
    1.52 -using ultra [of A] by simp
    1.53 -
    1.54 -lemma not_memD: "A \<notin> F \<Longrightarrow> - A \<in> F"
    1.55 -by (rule memI, simp)
    1.56 +lemma eventually_imp_iff: "eventually (\<lambda>x. P x \<longrightarrow> Q x) F \<longleftrightarrow> (eventually P F \<longrightarrow> eventually Q F)"
    1.57 +  using frequently_imp_iff[of P Q F] by (simp add: frequently_eq_eventually)
    1.58  
    1.59 -lemma not_mem_iff: "(A \<notin> F) = (- A \<in> F)"
    1.60 -by (rule iffI [OF not_memD not_memI])
    1.61 -
    1.62 -lemma Compl_iff: "(- A \<in> F) = (A \<notin> F)"
    1.63 -by (rule iffI [OF not_memI not_memD])
    1.64 +lemma eventually_iff_iff: "eventually (\<lambda>x. P x \<longleftrightarrow> Q x) F \<longleftrightarrow> (eventually P F \<longleftrightarrow> eventually Q F)"
    1.65 +  unfolding iff_conv_conj_imp eventually_conj_iff eventually_imp_iff by simp
    1.66  
    1.67 -lemma Un_iff: "(x \<union> y \<in> F) = (x \<in> F \<or> y \<in> F)"
    1.68 - apply (rule iffI)
    1.69 -  apply (erule contrapos_pp)
    1.70 -  apply (simp add: Int_iff not_mem_iff)
    1.71 - apply (auto elim: subset)
    1.72 -done
    1.73 +lemma eventually_not_iff: "eventually (\<lambda>x. \<not> P x) F \<longleftrightarrow> \<not> eventually P F"
    1.74 +  unfolding not_eventually frequently_eq_eventually ..
    1.75  
    1.76  end
    1.77  
    1.78 -subsubsection {* Free Ultrafilters *}
    1.79 -
    1.80 -locale freeultrafilter = ultrafilter +
    1.81 -  assumes infinite: "A \<in> F \<Longrightarrow> infinite A"
    1.82 -begin
    1.83 -
    1.84 -lemma finite: "finite A \<Longrightarrow> A \<notin> F"
    1.85 -by (erule contrapos_pn, erule infinite)
    1.86 -
    1.87 -lemma singleton: "{x} \<notin> F"
    1.88 -by (rule finite, simp)
    1.89 -
    1.90 -lemma insert_iff [simp]: "(insert x A \<in> F) = (A \<in> F)"
    1.91 -apply (subst insert_is_Un)
    1.92 -apply (subst Un_iff)
    1.93 -apply (simp add: singleton)
    1.94 -done
    1.95 -
    1.96 -lemma filter: "filter F" ..
    1.97 -
    1.98 -lemma ultrafilter: "ultrafilter F" ..
    1.99 -
   1.100 -end
   1.101 -
   1.102 -subsection {* Collect properties *}
   1.103 -
   1.104 -lemma (in filter) Collect_ex:
   1.105 -  "({n. \<exists>x. P n x} \<in> F) = (\<exists>X. {n. P n (X n)} \<in> F)"
   1.106 -proof
   1.107 -  assume "{n. \<exists>x. P n x} \<in> F"
   1.108 -  hence "{n. P n (SOME x. P n x)} \<in> F"
   1.109 -    by (auto elim: someI subset)
   1.110 -  thus "\<exists>X. {n. P n (X n)} \<in> F" by fast
   1.111 -next
   1.112 -  show "\<exists>X. {n. P n (X n)} \<in> F \<Longrightarrow> {n. \<exists>x. P n x} \<in> F"
   1.113 -    by (auto elim: subset)
   1.114 -qed
   1.115 -
   1.116 -lemma (in filter) Collect_conj:
   1.117 -  "({n. P n \<and> Q n} \<in> F) = ({n. P n} \<in> F \<and> {n. Q n} \<in> F)"
   1.118 -by (subst Collect_conj_eq, rule Int_iff)
   1.119 -
   1.120 -lemma (in ultrafilter) Collect_not:
   1.121 -  "({n. \<not> P n} \<in> F) = ({n. P n} \<notin> F)"
   1.122 -by (subst Collect_neg_eq, rule Compl_iff)
   1.123 -
   1.124 -lemma (in ultrafilter) Collect_disj:
   1.125 -  "({n. P n \<or> Q n} \<in> F) = ({n. P n} \<in> F \<or> {n. Q n} \<in> F)"
   1.126 -by (subst Collect_disj_eq, rule Un_iff)
   1.127 -
   1.128 -lemma (in ultrafilter) Collect_all:
   1.129 -  "({n. \<forall>x. P n x} \<in> F) = (\<forall>X. {n. P n (X n)} \<in> F)"
   1.130 -apply (rule Not_eq_iff [THEN iffD1])
   1.131 -apply (simp add: Collect_not [symmetric])
   1.132 -apply (rule Collect_ex)
   1.133 -done
   1.134 -
   1.135  subsection {* Maximal filter = Ultrafilter *}
   1.136  
   1.137  text {*
   1.138 @@ -133,281 +55,146 @@
   1.139    property of ultrafilter.
   1.140  *}
   1.141  
   1.142 -lemma extend_lemma1: "UNIV \<in> F \<Longrightarrow> A \<in> {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
   1.143 -by blast
   1.144 -
   1.145 -lemma extend_lemma2: "F \<subseteq> {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
   1.146 -by blast
   1.147 +lemma extend_filter:
   1.148 +  "frequently P F \<Longrightarrow> inf F (principal {x. P x}) \<noteq> bot"
   1.149 +  unfolding trivial_limit_def eventually_inf_principal by (simp add: not_eventually)
   1.150  
   1.151 -lemma (in filter) extend_filter:
   1.152 -assumes A: "- A \<notin> F"
   1.153 -shows "filter {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}" (is "filter ?X")
   1.154 -proof (rule filter.intro)
   1.155 -  show "UNIV \<in> ?X" by blast
   1.156 -next
   1.157 -  show "{} \<notin> ?X"
   1.158 -  proof (clarify)
   1.159 -    fix f assume f: "f \<in> F" and Af: "A \<inter> f \<subseteq> {}"
   1.160 -    from Af have fA: "f \<subseteq> - A" by blast
   1.161 -    from f fA have "- A \<in> F" by (rule subset)
   1.162 -    with A show "False" by simp
   1.163 +lemma max_filter_ultrafilter:
   1.164 +  assumes proper: "F \<noteq> bot"
   1.165 +  assumes max: "\<And>G. G \<noteq> bot \<Longrightarrow> G \<le> F \<Longrightarrow> F = G"
   1.166 +  shows "ultrafilter F"
   1.167 +proof
   1.168 +  fix P show "eventually P F \<or> (\<forall>\<^sub>Fx in F. \<not> P x)"
   1.169 +  proof (rule disjCI)
   1.170 +    assume "\<not> (\<forall>\<^sub>Fx in F. \<not> P x)"
   1.171 +    then have "inf F (principal {x. P x}) \<noteq> bot"
   1.172 +      by (simp add: not_eventually extend_filter)
   1.173 +    then have F: "F = inf F (principal {x. P x})"
   1.174 +      by (rule max) simp
   1.175 +    show "eventually P F"
   1.176 +      by (subst F) (simp add: eventually_inf_principal)
   1.177    qed
   1.178 -next
   1.179 -  fix u and v
   1.180 -  assume u: "u \<in> ?X" and v: "v \<in> ?X"
   1.181 -  from u obtain f where f: "f \<in> F" and Af: "A \<inter> f \<subseteq> u" by blast
   1.182 -  from v obtain g where g: "g \<in> F" and Ag: "A \<inter> g \<subseteq> v" by blast
   1.183 -  from f g have fg: "f \<inter> g \<in> F" by (rule Int)
   1.184 -  from Af Ag have Afg: "A \<inter> (f \<inter> g) \<subseteq> u \<inter> v" by blast
   1.185 -  from fg Afg show "u \<inter> v \<in> ?X" by blast
   1.186 -next
   1.187 -  fix u and v
   1.188 -  assume uv: "u \<subseteq> v" and u: "u \<in> ?X"
   1.189 -  from u obtain f where f: "f \<in> F" and Afu: "A \<inter> f \<subseteq> u" by blast
   1.190 -  from Afu uv have Afv: "A \<inter> f \<subseteq> v" by blast
   1.191 -  from f Afv have "\<exists>f\<in>F. A \<inter> f \<subseteq> v" by blast
   1.192 -  thus "v \<in> ?X" by simp
   1.193 -qed
   1.194 +qed fact
   1.195  
   1.196 -lemma (in filter) max_filter_ultrafilter:
   1.197 -assumes max: "\<And>G. \<lbrakk>filter G; F \<subseteq> G\<rbrakk> \<Longrightarrow> F = G"
   1.198 -shows "ultrafilter_axioms F"
   1.199 -proof (rule ultrafilter_axioms.intro)
   1.200 -  fix A show "A \<in> F \<or> - A \<in> F"
   1.201 -  proof (rule disjCI)
   1.202 -    let ?X = "{X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
   1.203 -    assume AF: "- A \<notin> F"
   1.204 -    from AF have X: "filter ?X" by (rule extend_filter)
   1.205 -    from UNIV have AX: "A \<in> ?X" by (rule extend_lemma1)
   1.206 -    have FX: "F \<subseteq> ?X" by (rule extend_lemma2)
   1.207 -    from X FX have "F = ?X" by (rule max)
   1.208 -    with AX show "A \<in> F" by simp
   1.209 -  qed
   1.210 -qed
   1.211 +lemma le_filter_frequently: "F \<le> G \<longleftrightarrow> (\<forall>P. frequently P F \<longrightarrow> frequently P G)"
   1.212 +  unfolding frequently_def le_filter_def
   1.213 +  apply auto
   1.214 +  apply (erule_tac x="\<lambda>x. \<not> P x" in allE)
   1.215 +  apply auto
   1.216 +  done
   1.217  
   1.218  lemma (in ultrafilter) max_filter:
   1.219 -assumes G: "filter G" and sub: "F \<subseteq> G" shows "F = G"
   1.220 -proof
   1.221 -  show "F \<subseteq> G" using sub .
   1.222 -  show "G \<subseteq> F"
   1.223 -  proof
   1.224 -    fix A assume A: "A \<in> G"
   1.225 -    from G A have "- A \<notin> G" by (rule filter.memD)
   1.226 -    with sub have B: "- A \<notin> F" by blast
   1.227 -    thus "A \<in> F" by (rule memI)
   1.228 -  qed
   1.229 -qed
   1.230 +  assumes G: "G \<noteq> bot" and sub: "G \<le> F" shows "F = G"
   1.231 +proof (rule antisym)
   1.232 +  show "F \<le> G"
   1.233 +    using sub
   1.234 +    by (auto simp: le_filter_frequently[of F] frequently_eq_eventually le_filter_def[of G]
   1.235 +             intro!: eventually_frequently G proper)
   1.236 +qed fact
   1.237  
   1.238  subsection {* Ultrafilter Theorem *}
   1.239  
   1.240  text "A local context makes proof of ultrafilter Theorem more modular"
   1.241 -context
   1.242 -  fixes   frechet :: "'a set set"
   1.243 -  and     superfrechet :: "'a set set set"
   1.244 -
   1.245 -  assumes infinite_UNIV: "infinite (UNIV :: 'a set)"
   1.246  
   1.247 -  defines frechet_def: "frechet \<equiv> {A. finite (- A)}"
   1.248 -  and     superfrechet_def: "superfrechet \<equiv> {G. filter G \<and> frechet \<subseteq> G}"
   1.249 -begin
   1.250 +lemma ex_max_ultrafilter:
   1.251 +  fixes F :: "'a filter"
   1.252 +  assumes F: "F \<noteq> bot"
   1.253 +  shows "\<exists>U\<le>F. ultrafilter U"
   1.254 +proof -
   1.255 +  let ?X = "{G. G \<noteq> bot \<and> G \<le> F}"
   1.256 +  let ?R = "{(b, a). a \<noteq> bot \<and> a \<le> b \<and> b \<le> F}"
   1.257  
   1.258 -lemma superfrechetI:
   1.259 -  "\<lbrakk>filter G; frechet \<subseteq> G\<rbrakk> \<Longrightarrow> G \<in> superfrechet"
   1.260 -by (simp add: superfrechet_def)
   1.261 -
   1.262 -lemma superfrechetD1:
   1.263 -  "G \<in> superfrechet \<Longrightarrow> filter G"
   1.264 -by (simp add: superfrechet_def)
   1.265 +  have bot_notin_R: "\<And>c. c \<in> Chains ?R \<Longrightarrow> bot \<notin> c"
   1.266 +    by (auto simp: Chains_def)
   1.267  
   1.268 -lemma superfrechetD2:
   1.269 -  "G \<in> superfrechet \<Longrightarrow> frechet \<subseteq> G"
   1.270 -by (simp add: superfrechet_def)
   1.271 -
   1.272 -text {* A few properties of free filters *}
   1.273 +  have [simp]: "Field ?R = ?X"
   1.274 +    by (auto simp: Field_def bot_unique)
   1.275  
   1.276 -lemma filter_cofinite:
   1.277 -assumes inf: "infinite (UNIV :: 'a set)"
   1.278 -shows "filter {A:: 'a set. finite (- A)}" (is "filter ?F")
   1.279 -proof (rule filter.intro)
   1.280 -  show "UNIV \<in> ?F" by simp
   1.281 -next
   1.282 -  show "{} \<notin> ?F" using inf by simp
   1.283 -next
   1.284 -  fix u v assume "u \<in> ?F" and "v \<in> ?F"
   1.285 -  thus "u \<inter> v \<in> ?F" by simp
   1.286 -next
   1.287 -  fix u v assume uv: "u \<subseteq> v" and u: "u \<in> ?F"
   1.288 -  from uv have vu: "- v \<subseteq> - u" by simp
   1.289 -  from u show "v \<in> ?F"
   1.290 -    by (simp add: finite_subset [OF vu])
   1.291 -qed
   1.292 +  have "\<exists>m\<in>Field ?R. \<forall>a\<in>Field ?R. (m, a) \<in> ?R \<longrightarrow> a = m"
   1.293 +  proof (rule Zorns_po_lemma)
   1.294 +    show "Partial_order ?R"
   1.295 +      unfolding partial_order_on_def preorder_on_def
   1.296 +      by (auto simp: antisym_def refl_on_def trans_def Field_def bot_unique)
   1.297 +    show "\<forall>C\<in>Chains ?R. \<exists>u\<in>Field ?R. \<forall>a\<in>C. (a, u) \<in> ?R"
   1.298 +    proof (safe intro!: bexI del: notI)
   1.299 +      fix c x assume c: "c \<in> Chains ?R"
   1.300  
   1.301 -text {*
   1.302 -   We prove: 1. Existence of maximal filter i.e. ultrafilter;
   1.303 -             2. Freeness property i.e ultrafilter is free.
   1.304 -             Use a locale to prove various lemmas and then 
   1.305 -             export main result: The ultrafilter Theorem
   1.306 -*}
   1.307 -
   1.308 -lemma filter_frechet: "filter frechet"
   1.309 -by (unfold frechet_def, rule filter_cofinite [OF infinite_UNIV])
   1.310 -
   1.311 -lemma frechet_in_superfrechet: "frechet \<in> superfrechet"
   1.312 -by (rule superfrechetI [OF filter_frechet subset_refl])
   1.313 -
   1.314 -lemma lemma_mem_chain_filter:
   1.315 -  "\<lbrakk>c \<in> chains superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> filter x"
   1.316 -by (unfold chains_def superfrechet_def, blast)
   1.317 -
   1.318 -
   1.319 -subsubsection {* Unions of chains of superfrechets *}
   1.320 +      { assume "c \<noteq> {}"
   1.321 +        with c have "Inf c = bot \<longleftrightarrow> (\<exists>x\<in>c. x = bot)"
   1.322 +          unfolding trivial_limit_def by (intro eventually_Inf_base) (auto simp: Chains_def)
   1.323 +        with c have 1: "Inf c \<noteq> bot"
   1.324 +          by (simp add: bot_notin_R)
   1.325 +        from `c \<noteq> {}` obtain x where "x \<in> c" by auto
   1.326 +        with c have 2: "Inf c \<le> F"
   1.327 +          by (auto intro!: Inf_lower2[of x] simp: Chains_def)
   1.328 +        note 1 2 }
   1.329 +      note Inf_c = this
   1.330 +      then have [simp]: "inf F (Inf c) = (if c = {} then F else Inf c)"
   1.331 +        using c by (auto simp add: inf_absorb2)
   1.332  
   1.333 -text "In this section we prove that superfrechet is closed
   1.334 -with respect to unions of non-empty chains. We must show
   1.335 -  1) Union of a chain is a filter,
   1.336 -  2) Union of a chain contains frechet.
   1.337 +      show "inf F (Inf c) \<noteq> bot"
   1.338 +        using c by (simp add: F Inf_c)
   1.339  
   1.340 -Number 2 is trivial, but 1 requires us to prove all the filter rules."
   1.341 +      show "inf F (Inf c) \<in> Field ?R"
   1.342 +        using c by (simp add: Chains_def Inf_c F)
   1.343  
   1.344 -lemma Union_chain_UNIV:
   1.345 -  "\<lbrakk>c \<in> chains superfrechet; c \<noteq> {}\<rbrakk> \<Longrightarrow> UNIV \<in> \<Union>c"
   1.346 -proof -
   1.347 -  assume 1: "c \<in> chains superfrechet" and 2: "c \<noteq> {}"
   1.348 -  from 2 obtain x where 3: "x \<in> c" by blast
   1.349 -  from 1 3 have "filter x" by (rule lemma_mem_chain_filter)
   1.350 -  hence "UNIV \<in> x" by (rule filter.UNIV)
   1.351 -  with 3 show "UNIV \<in> \<Union>c" by blast
   1.352 -qed
   1.353 -
   1.354 -lemma Union_chain_empty:
   1.355 -  "c \<in> chains superfrechet \<Longrightarrow> {} \<notin> \<Union>c"
   1.356 -proof
   1.357 -  assume 1: "c \<in> chains superfrechet" and 2: "{} \<in> \<Union>c"
   1.358 -  from 2 obtain x where 3: "x \<in> c" and 4: "{} \<in> x" ..
   1.359 -  from 1 3 have "filter x" by (rule lemma_mem_chain_filter)
   1.360 -  hence "{} \<notin> x" by (rule filter.empty)
   1.361 -  with 4 show "False" by simp
   1.362 +      assume x: "x \<in> c"
   1.363 +      with c show "inf F (Inf c) \<le> x" "x \<le> F"
   1.364 +        by (auto intro: Inf_lower simp: Chains_def)
   1.365 +    qed
   1.366 +  qed
   1.367 +  then guess U ..
   1.368 +  then show ?thesis
   1.369 +    by (intro exI[of _ U] conjI max_filter_ultrafilter) auto
   1.370  qed
   1.371  
   1.372 -lemma Union_chain_Int:
   1.373 -  "\<lbrakk>c \<in> chains superfrechet; u \<in> \<Union>c; v \<in> \<Union>c\<rbrakk> \<Longrightarrow> u \<inter> v \<in> \<Union>c"
   1.374 -proof -
   1.375 -  assume c: "c \<in> chains superfrechet"
   1.376 -  assume "u \<in> \<Union>c"
   1.377 -    then obtain x where ux: "u \<in> x" and xc: "x \<in> c" ..
   1.378 -  assume "v \<in> \<Union>c"
   1.379 -    then obtain y where vy: "v \<in> y" and yc: "y \<in> c" ..
   1.380 -  from c xc yc have "x \<subseteq> y \<or> y \<subseteq> x" using c unfolding chains_def chain_subset_def by auto
   1.381 -  with xc yc have xyc: "x \<union> y \<in> c"
   1.382 -    by (auto simp add: Un_absorb1 Un_absorb2)
   1.383 -  with c have fxy: "filter (x \<union> y)" by (rule lemma_mem_chain_filter)
   1.384 -  from ux have uxy: "u \<in> x \<union> y" by simp
   1.385 -  from vy have vxy: "v \<in> x \<union> y" by simp
   1.386 -  from fxy uxy vxy have "u \<inter> v \<in> x \<union> y" by (rule filter.Int)
   1.387 -  with xyc show "u \<inter> v \<in> \<Union>c" ..
   1.388 -qed
   1.389 -
   1.390 -lemma Union_chain_subset:
   1.391 -  "\<lbrakk>c \<in> chains superfrechet; u \<in> \<Union>c; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> \<Union>c"
   1.392 -proof -
   1.393 -  assume c: "c \<in> chains superfrechet"
   1.394 -     and u: "u \<in> \<Union>c" and uv: "u \<subseteq> v"
   1.395 -  from u obtain x where ux: "u \<in> x" and xc: "x \<in> c" ..
   1.396 -  from c xc have fx: "filter x" by (rule lemma_mem_chain_filter)
   1.397 -  from fx ux uv have vx: "v \<in> x" by (rule filter.subset)
   1.398 -  with xc show "v \<in> \<Union>c" ..
   1.399 -qed
   1.400 -
   1.401 -lemma Union_chain_filter:
   1.402 -assumes chain: "c \<in> chains superfrechet" and nonempty: "c \<noteq> {}"
   1.403 -shows "filter (\<Union>c)" 
   1.404 -proof (rule filter.intro)
   1.405 -  show "UNIV \<in> \<Union>c" using chain nonempty by (rule Union_chain_UNIV)
   1.406 -next
   1.407 -  show "{} \<notin> \<Union>c" using chain by (rule Union_chain_empty)
   1.408 -next
   1.409 -  fix u v assume "u \<in> \<Union>c" and "v \<in> \<Union>c"
   1.410 -  with chain show "u \<inter> v \<in> \<Union>c" by (rule Union_chain_Int)
   1.411 -next
   1.412 -  fix u v assume "u \<in> \<Union>c" and "u \<subseteq> v"
   1.413 -  with chain show "v \<in> \<Union>c" by (rule Union_chain_subset)
   1.414 -qed
   1.415 -
   1.416 -lemma lemma_mem_chain_frechet_subset:
   1.417 -  "\<lbrakk>c \<in> chains superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> frechet \<subseteq> x"
   1.418 -by (unfold superfrechet_def chains_def, blast)
   1.419 -
   1.420 -lemma Union_chain_superfrechet:
   1.421 -  "\<lbrakk>c \<noteq> {}; c \<in> chains superfrechet\<rbrakk> \<Longrightarrow> \<Union>c \<in> superfrechet"
   1.422 -proof (rule superfrechetI)
   1.423 -  assume 1: "c \<in> chains superfrechet" and 2: "c \<noteq> {}"
   1.424 -  thus "filter (\<Union>c)" by (rule Union_chain_filter)
   1.425 -  from 2 obtain x where 3: "x \<in> c" by blast
   1.426 -  from 1 3 have "frechet \<subseteq> x" by (rule lemma_mem_chain_frechet_subset)
   1.427 -  also from 3 have "x \<subseteq> \<Union>c" by blast
   1.428 -  finally show "frechet \<subseteq> \<Union>c" .
   1.429 -qed
   1.430 -
   1.431 -subsubsection {* Existence of free ultrafilter *}
   1.432 -
   1.433 -lemma max_cofinite_filter_Ex:
   1.434 -  "\<exists>U\<in>superfrechet. \<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> G = U" 
   1.435 -proof (rule Zorn_Lemma2, safe)
   1.436 -  fix c assume c: "c \<in> chains superfrechet"
   1.437 -  show "\<exists>U\<in>superfrechet. \<forall>G\<in>c. G \<subseteq> U" (is "?U")
   1.438 -  proof (cases)
   1.439 -    assume "c = {}"
   1.440 -    with frechet_in_superfrechet show "?U" by blast
   1.441 -  next
   1.442 -    assume A: "c \<noteq> {}"
   1.443 -    from A c have "\<Union>c \<in> superfrechet"
   1.444 -      by (rule Union_chain_superfrechet)
   1.445 -    thus "?U" by blast
   1.446 -  qed
   1.447 -qed
   1.448 -
   1.449 -lemma mem_superfrechet_all_infinite:
   1.450 -  "\<lbrakk>U \<in> superfrechet; A \<in> U\<rbrakk> \<Longrightarrow> infinite A"
   1.451 -proof
   1.452 -  assume U: "U \<in> superfrechet" and A: "A \<in> U" and fin: "finite A"
   1.453 -  from U have fil: "filter U" and fre: "frechet \<subseteq> U"
   1.454 -    by (simp_all add: superfrechet_def)
   1.455 -  from fin have "- A \<in> frechet" by (simp add: frechet_def)
   1.456 -  with fre have cA: "- A \<in> U" by (rule subsetD)
   1.457 -  from fil A cA have "A \<inter> - A \<in> U" by (rule filter.Int)
   1.458 -  with fil show "False" by (simp add: filter.empty)
   1.459 -qed
   1.460 +subsubsection {* Free Ultrafilters *}
   1.461  
   1.462  text {* There exists a free ultrafilter on any infinite set *}
   1.463  
   1.464 +locale freeultrafilter = ultrafilter +
   1.465 +  assumes infinite: "eventually P F \<Longrightarrow> infinite {x. P x}"
   1.466 +begin
   1.467 +
   1.468 +lemma finite: "finite {x. P x} \<Longrightarrow> \<not> eventually P F"
   1.469 +  by (erule contrapos_pn, erule infinite)
   1.470 +
   1.471 +lemma finite': "finite {x. \<not> P x} \<Longrightarrow> eventually P F"
   1.472 +  by (drule finite) (simp add: not_eventually frequently_eq_eventually)
   1.473 +
   1.474 +lemma le_cofinite: "F \<le> cofinite"
   1.475 +  by (intro filter_leI)
   1.476 +     (auto simp add: eventually_cofinite not_eventually frequently_eq_eventually dest!: finite)
   1.477 +
   1.478 +lemma singleton: "\<not> eventually (\<lambda>x. x = a) F"
   1.479 +by (rule finite, simp)
   1.480 +
   1.481 +lemma singleton': "\<not> eventually (op = a) F"
   1.482 +by (rule finite, simp)
   1.483 +
   1.484 +lemma ultrafilter: "ultrafilter F" ..
   1.485 +
   1.486 +end
   1.487 +
   1.488  lemma freeultrafilter_Ex:
   1.489 -  "\<exists>U::'a set set. freeultrafilter U"
   1.490 +  assumes [simp]: "infinite (UNIV :: 'a set)"
   1.491 +  shows "\<exists>U::'a filter. freeultrafilter U"
   1.492  proof -
   1.493 -  from max_cofinite_filter_Ex obtain U
   1.494 -    where U: "U \<in> superfrechet"
   1.495 -      and max [rule_format]: "\<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> G = U" ..
   1.496 -  from U have fil: "filter U" by (rule superfrechetD1)
   1.497 -  from U have fre: "frechet \<subseteq> U" by (rule superfrechetD2)
   1.498 -  have ultra: "ultrafilter_axioms U"
   1.499 -  proof (rule filter.max_filter_ultrafilter [OF fil])
   1.500 -    fix G assume G: "filter G" and UG: "U \<subseteq> G"
   1.501 -    from fre UG have "frechet \<subseteq> G" by simp
   1.502 -    with G have "G \<in> superfrechet" by (rule superfrechetI)
   1.503 -    from this UG show "U = G" by (rule max[symmetric])
   1.504 +  from ex_max_ultrafilter[of "cofinite :: 'a filter"]
   1.505 +  obtain U :: "'a filter" where "U \<le> cofinite" "ultrafilter U"
   1.506 +    by auto
   1.507 +  interpret ultrafilter U by fact
   1.508 +  have "freeultrafilter U"
   1.509 +  proof
   1.510 +    fix P assume "eventually P U"
   1.511 +    with proper have "frequently P U"
   1.512 +      by (rule eventually_frequently)
   1.513 +    then have "frequently P cofinite"
   1.514 +      using `U \<le> cofinite` by (simp add: le_filter_frequently)
   1.515 +    then show "infinite {x. P x}"
   1.516 +      by (simp add: frequently_cofinite)
   1.517    qed
   1.518 -  have free: "freeultrafilter_axioms U"
   1.519 -  proof (rule freeultrafilter_axioms.intro)
   1.520 -    fix A assume "A \<in> U"
   1.521 -    with U show "infinite A" by (rule mem_superfrechet_all_infinite)
   1.522 -  qed
   1.523 -  from fil ultra free have "freeultrafilter U"
   1.524 -    by (rule freeultrafilter.intro [OF ultrafilter.intro])
   1.525 -    (* FIXME: unfold_locales should use chained facts *)
   1.526    then show ?thesis ..
   1.527  qed
   1.528  
   1.529  end
   1.530 -
   1.531 -hide_const (open) filter
   1.532 -
   1.533 -end