1(* Title: HOL/Nonstandard_Analysis/Free_Ultrafilter.thy 2 Author: Jacques D. Fleuriot, University of Cambridge 3 Author: Lawrence C Paulson 4 Author: Brian Huffman 5*) 6 7section \<open>Filters and Ultrafilters\<close> 8 9theory Free_Ultrafilter 10 imports "HOL-Library.Infinite_Set" 11begin 12 13 14subsection \<open>Definitions and basic properties\<close> 15 16subsubsection \<open>Ultrafilters\<close> 17 18locale ultrafilter = 19 fixes F :: "'a filter" 20 assumes proper: "F \<noteq> bot" 21 assumes ultra: "eventually P F \<or> eventually (\<lambda>x. \<not> P x) F" 22begin 23 24lemma eventually_imp_frequently: "frequently P F \<Longrightarrow> eventually P F" 25 using ultra[of P] by (simp add: frequently_def) 26 27lemma frequently_eq_eventually: "frequently P F = eventually P F" 28 using eventually_imp_frequently eventually_frequently[OF proper] .. 29 30lemma eventually_disj_iff: "eventually (\<lambda>x. P x \<or> Q x) F \<longleftrightarrow> eventually P F \<or> eventually Q F" 31 unfolding frequently_eq_eventually[symmetric] frequently_disj_iff .. 32 33lemma eventually_all_iff: "eventually (\<lambda>x. \<forall>y. P x y) F = (\<forall>Y. eventually (\<lambda>x. P x (Y x)) F)" 34 using frequently_all[of P F] by (simp add: frequently_eq_eventually) 35 36lemma eventually_imp_iff: "eventually (\<lambda>x. P x \<longrightarrow> Q x) F \<longleftrightarrow> (eventually P F \<longrightarrow> eventually Q F)" 37 using frequently_imp_iff[of P Q F] by (simp add: frequently_eq_eventually) 38 39lemma eventually_iff_iff: "eventually (\<lambda>x. P x \<longleftrightarrow> Q x) F \<longleftrightarrow> (eventually P F \<longleftrightarrow> eventually Q F)" 40 unfolding iff_conv_conj_imp eventually_conj_iff eventually_imp_iff by simp 41 42lemma eventually_not_iff: "eventually (\<lambda>x. \<not> P x) F \<longleftrightarrow> \<not> eventually P F" 43 unfolding not_eventually frequently_eq_eventually .. 44 45end 46 47 48subsection \<open>Maximal filter = Ultrafilter\<close> 49 50text \<open> 51 A filter \<open>F\<close> is an ultrafilter iff it is a maximal filter, 52 i.e. whenever \<open>G\<close> is a filter and \<^prop>\<open>F \<subseteq> G\<close> then \<^prop>\<open>F = G\<close> 53\<close> 54 55text \<open> 56 Lemma that shows existence of an extension to what was assumed to 57 be a maximal filter. Will be used to derive contradiction in proof of 58 property of ultrafilter. 59\<close> 60 61lemma extend_filter: "frequently P F \<Longrightarrow> inf F (principal {x. P x}) \<noteq> bot" 62 by (simp add: trivial_limit_def eventually_inf_principal not_eventually) 63 64lemma max_filter_ultrafilter: 65 assumes "F \<noteq> bot" 66 assumes max: "\<And>G. G \<noteq> bot \<Longrightarrow> G \<le> F \<Longrightarrow> F = G" 67 shows "ultrafilter F" 68proof 69 show "eventually P F \<or> (\<forall>\<^sub>Fx in F. \<not> P x)" for P 70 proof (rule disjCI) 71 assume "\<not> (\<forall>\<^sub>Fx in F. \<not> P x)" 72 then have "inf F (principal {x. P x}) \<noteq> bot" 73 by (simp add: not_eventually extend_filter) 74 then have F: "F = inf F (principal {x. P x})" 75 by (rule max) simp 76 show "eventually P F" 77 by (subst F) (simp add: eventually_inf_principal) 78 qed 79qed fact 80 81lemma le_filter_frequently: "F \<le> G \<longleftrightarrow> (\<forall>P. frequently P F \<longrightarrow> frequently P G)" 82 unfolding frequently_def le_filter_def 83 apply auto 84 apply (erule_tac x="\<lambda>x. \<not> P x" in allE) 85 apply auto 86 done 87 88lemma (in ultrafilter) max_filter: 89 assumes G: "G \<noteq> bot" 90 and sub: "G \<le> F" 91 shows "F = G" 92proof (rule antisym) 93 show "F \<le> G" 94 using sub 95 by (auto simp: le_filter_frequently[of F] frequently_eq_eventually le_filter_def[of G] 96 intro!: eventually_frequently G proper) 97qed fact 98 99 100subsection \<open>Ultrafilter Theorem\<close> 101 102lemma ex_max_ultrafilter: 103 fixes F :: "'a filter" 104 assumes F: "F \<noteq> bot" 105 shows "\<exists>U\<le>F. ultrafilter U" 106proof - 107 let ?X = "{G. G \<noteq> bot \<and> G \<le> F}" 108 let ?R = "{(b, a). a \<noteq> bot \<and> a \<le> b \<and> b \<le> F}" 109 110 have bot_notin_R: "c \<in> Chains ?R \<Longrightarrow> bot \<notin> c" for c 111 by (auto simp: Chains_def) 112 113 have [simp]: "Field ?R = ?X" 114 by (auto simp: Field_def bot_unique) 115 116 have "\<exists>m\<in>Field ?R. \<forall>a\<in>Field ?R. (m, a) \<in> ?R \<longrightarrow> a = m" (is "\<exists>m\<in>?A. ?B m") 117 proof (rule Zorns_po_lemma) 118 show "Partial_order ?R" 119 by (auto simp: partial_order_on_def preorder_on_def 120 antisym_def refl_on_def trans_def Field_def bot_unique) 121 show "\<exists>u\<in>Field ?R. \<forall>a\<in>C. (a, u) \<in> ?R" if C: "C \<in> Chains ?R" for C 122 proof (simp, intro exI conjI ballI) 123 have Inf_C: "Inf C \<noteq> bot" "Inf C \<le> F" if "C \<noteq> {}" 124 proof - 125 from C that have "Inf C = bot \<longleftrightarrow> (\<exists>x\<in>C. x = bot)" 126 unfolding trivial_limit_def by (intro eventually_Inf_base) (auto simp: Chains_def) 127 with C show "Inf C \<noteq> bot" 128 by (simp add: bot_notin_R) 129 from that obtain x where "x \<in> C" by auto 130 with C show "Inf C \<le> F" 131 by (auto intro!: Inf_lower2[of x] simp: Chains_def) 132 qed 133 then have [simp]: "inf F (Inf C) = (if C = {} then F else Inf C)" 134 using C by (auto simp add: inf_absorb2) 135 from C show "inf F (Inf C) \<noteq> bot" 136 by (simp add: F Inf_C) 137 from C show "inf F (Inf C) \<le> F" 138 by (simp add: Chains_def Inf_C F) 139 with C show "inf F (Inf C) \<le> x" "x \<le> F" if "x \<in> C" for x 140 using that by (auto intro: Inf_lower simp: Chains_def) 141 qed 142 qed 143 then obtain U where U: "U \<in> ?A" "?B U" .. 144 show ?thesis 145 proof 146 from U show "U \<le> F \<and> ultrafilter U" 147 by (auto intro!: max_filter_ultrafilter) 148 qed 149qed 150 151 152subsubsection \<open>Free Ultrafilters\<close> 153 154text \<open>There exists a free ultrafilter on any infinite set.\<close> 155 156locale freeultrafilter = ultrafilter + 157 assumes infinite: "eventually P F \<Longrightarrow> infinite {x. P x}" 158begin 159 160lemma finite: "finite {x. P x} \<Longrightarrow> \<not> eventually P F" 161 by (erule contrapos_pn) (erule infinite) 162 163lemma finite': "finite {x. \<not> P x} \<Longrightarrow> eventually P F" 164 by (drule finite) (simp add: not_eventually frequently_eq_eventually) 165 166lemma le_cofinite: "F \<le> cofinite" 167 by (intro filter_leI) 168 (auto simp add: eventually_cofinite not_eventually frequently_eq_eventually dest!: finite) 169 170lemma singleton: "\<not> eventually (\<lambda>x. x = a) F" 171 by (rule finite) simp 172 173lemma singleton': "\<not> eventually ((=) a) F" 174 by (rule finite) simp 175 176lemma ultrafilter: "ultrafilter F" .. 177 178end 179 180lemma freeultrafilter_Ex: 181 assumes [simp]: "infinite (UNIV :: 'a set)" 182 shows "\<exists>U::'a filter. freeultrafilter U" 183proof - 184 from ex_max_ultrafilter[of "cofinite :: 'a filter"] 185 obtain U :: "'a filter" where "U \<le> cofinite" "ultrafilter U" 186 by auto 187 interpret ultrafilter U by fact 188 have "freeultrafilter U" 189 proof 190 fix P 191 assume "eventually P U" 192 with proper have "frequently P U" 193 by (rule eventually_frequently) 194 then have "frequently P cofinite" 195 using \<open>U \<le> cofinite\<close> by (simp add: le_filter_frequently) 196 then show "infinite {x. P x}" 197 by (simp add: frequently_cofinite) 198 qed 199 then show ?thesis .. 200qed 201 202end 203