# Theory Free_Ultrafilter

theory Free_Ultrafilter
imports Infinite_Set
```(*  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 ∨ (∀⇩Fx in F. ¬ P x)" for P
proof (rule disjCI)
assume "¬ (∀⇩Fx in F. ¬ P x)"
then have "inf F (principal {x. P x}) ≠ bot"
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"
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"
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}"