Theory Free_Ultrafilter

(*  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 propF  G then propF = 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"
      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 "UF. 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 "mField ?R. aField ?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 "uField ?R. aC. (a, u)  ?R" if C: "C  Chains ?R" for C
    proof (simp, intro exI conjI ballI)
      have Inf_C: "Inf C  bot" "Inf C  F" if "C  {}"
      proof -
        from C that have "Inf C = bot  (xC. 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)  F"
        by (simp add: Chains_def Inf_C F)
      with C show "inf F (Inf C)  x" "x  F" if "x  C" for x
        using that  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 ((=) 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