(* Title: HOL/Nonstandard_Analysis/Free_Ultrafilter.thy Author: Jacques D. Fleuriot, University of Cambridge Author: Lawrence C Paulson Author: Brian Huffman *) section ‹Filters and Ultrafilters› theory Free_Ultrafilter imports "HOL-Library.Infinite_Set" begin subsection ‹Definitions and basic properties› subsubsection ‹Ultrafilters› locale ultrafilter = fixes F :: "'a filter" assumes proper: "F ≠ bot" assumes ultra: "eventually P F ∨ eventually (λx. ¬ P x) F" begin lemma eventually_imp_frequently: "frequently P F ⟹ eventually P F" using ultra[of P] by (simp add: frequently_def) lemma frequently_eq_eventually: "frequently P F = eventually P F" using eventually_imp_frequently eventually_frequently[OF proper] .. lemma eventually_disj_iff: "eventually (λx. P x ∨ Q x) F ⟷ eventually P F ∨ eventually Q F" unfolding frequently_eq_eventually[symmetric] frequently_disj_iff .. lemma eventually_all_iff: "eventually (λx. ∀y. P x y) F = (∀Y. eventually (λx. P x (Y x)) F)" using frequently_all[of P F] by (simp add: frequently_eq_eventually) lemma eventually_imp_iff: "eventually (λx. P x ⟶ Q x) F ⟷ (eventually P F ⟶ eventually Q F)" using frequently_imp_iff[of P Q F] by (simp add: frequently_eq_eventually) lemma eventually_iff_iff: "eventually (λx. P x ⟷ Q x) F ⟷ (eventually P F ⟷ eventually Q F)" unfolding iff_conv_conj_imp eventually_conj_iff eventually_imp_iff by simp lemma eventually_not_iff: "eventually (λx. ¬ P x) F ⟷ ¬ eventually P F" unfolding not_eventually frequently_eq_eventually .. end subsection ‹Maximal filter = Ultrafilter› text ‹ A filter ‹F› is an ultrafilter iff it is a maximal filter, i.e. whenever ‹G› is a filter and @{prop "F ⊆ G"} then @{prop "F = G"} › text ‹ Lemma that shows existence of an extension to what was assumed to be a maximal filter. Will be used to derive contradiction in proof of property of ultrafilter. › lemma extend_filter: "frequently P F ⟹ inf F (principal {x. P x}) ≠ bot" by (simp add: trivial_limit_def eventually_inf_principal not_eventually) lemma max_filter_ultrafilter: assumes "F ≠ bot" assumes max: "⋀G. G ≠ bot ⟹ G ≤ F ⟹ F = G" shows "ultrafilter F" proof show "eventually P F ∨ (∀⇩_{F}x in F. ¬ P x)" for P proof (rule disjCI) assume "¬ (∀⇩_{F}x in F. ¬ P x)" then have "inf F (principal {x. P x}) ≠ bot" by (simp add: not_eventually extend_filter) then have F: "F = inf F (principal {x. P x})" by (rule max) simp show "eventually P F" by (subst F) (simp add: eventually_inf_principal) qed qed fact lemma le_filter_frequently: "F ≤ G ⟷ (∀P. frequently P F ⟶ frequently P G)" unfolding frequently_def le_filter_def apply auto apply (erule_tac x="λx. ¬ P x" in allE) apply auto done lemma (in ultrafilter) max_filter: assumes G: "G ≠ bot" and sub: "G ≤ F" shows "F = G" proof (rule antisym) show "F ≤ G" using sub by (auto simp: le_filter_frequently[of F] frequently_eq_eventually le_filter_def[of G] intro!: eventually_frequently G proper) qed fact subsection ‹Ultrafilter Theorem› lemma ex_max_ultrafilter: fixes F :: "'a filter" assumes F: "F ≠ bot" shows "∃U≤F. ultrafilter U" proof - let ?X = "{G. G ≠ bot ∧ G ≤ F}" let ?R = "{(b, a). a ≠ bot ∧ a ≤ b ∧ b ≤ F}" have bot_notin_R: "c ∈ Chains ?R ⟹ bot ∉ c" for c by (auto simp: Chains_def) have [simp]: "Field ?R = ?X" by (auto simp: Field_def bot_unique) have "∃m∈Field ?R. ∀a∈Field ?R. (m, a) ∈ ?R ⟶ a = m" (is "∃m∈?A. ?B m") proof (rule Zorns_po_lemma) show "Partial_order ?R" by (auto simp: partial_order_on_def preorder_on_def antisym_def refl_on_def trans_def Field_def bot_unique) show "∀C∈Chains ?R. ∃u∈Field ?R. ∀a∈C. (a, u) ∈ ?R" proof (safe intro!: bexI del: notI) fix c x assume c: "c ∈ Chains ?R" have Inf_c: "Inf c ≠ bot" "Inf c ≤ F" if "c ≠ {}" proof - from c that have "Inf c = bot ⟷ (∃x∈c. x = bot)" unfolding trivial_limit_def by (intro eventually_Inf_base) (auto simp: Chains_def) with c show "Inf c ≠ bot" by (simp add: bot_notin_R) from that obtain x where "x ∈ c" by auto with c show "Inf c ≤ F" by (auto intro!: Inf_lower2[of x] simp: Chains_def) qed then have [simp]: "inf F (Inf c) = (if c = {} then F else Inf c)" using c by (auto simp add: inf_absorb2) from c show "inf F (Inf c) ≠ bot" by (simp add: F Inf_c) from c show "inf F (Inf c) ∈ Field ?R" by (simp add: Chains_def Inf_c F) assume "x ∈ c" with c show "inf F (Inf c) ≤ x" "x ≤ F" by (auto intro: Inf_lower simp: Chains_def) qed qed then obtain U where U: "U ∈ ?A" "?B U" .. show ?thesis proof from U show "U ≤ F ∧ ultrafilter U" by (auto intro!: max_filter_ultrafilter) qed qed subsubsection ‹Free Ultrafilters› text ‹There exists a free ultrafilter on any infinite set.› locale freeultrafilter = ultrafilter + assumes infinite: "eventually P F ⟹ infinite {x. P x}" begin lemma finite: "finite {x. P x} ⟹ ¬ eventually P F" by (erule contrapos_pn) (erule infinite) lemma finite': "finite {x. ¬ P x} ⟹ eventually P F" by (drule finite) (simp add: not_eventually frequently_eq_eventually) lemma le_cofinite: "F ≤ cofinite" by (intro filter_leI) (auto simp add: eventually_cofinite not_eventually frequently_eq_eventually dest!: finite) lemma singleton: "¬ eventually (λx. x = a) F" by (rule finite) simp lemma singleton': "¬ eventually (op = a) F" by (rule finite) simp lemma ultrafilter: "ultrafilter F" .. end lemma freeultrafilter_Ex: assumes [simp]: "infinite (UNIV :: 'a set)" shows "∃U::'a filter. freeultrafilter U" proof - from ex_max_ultrafilter[of "cofinite :: 'a filter"] obtain U :: "'a filter" where "U ≤ cofinite" "ultrafilter U" by auto interpret ultrafilter U by fact have "freeultrafilter U" proof fix P assume "eventually P U" with proper have "frequently P U" by (rule eventually_frequently) then have "frequently P cofinite" using ‹U ≤ cofinite› by (simp add: le_filter_frequently) then show "infinite {x. P x}" by (simp add: frequently_cofinite) qed then show ?thesis .. qed end