src/HOL/Nonstandard_Analysis/Free_Ultrafilter.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 64435 c93b0e6131c3
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
executable domain membership checks
     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 
     7 section \<open>Filters and Ultrafilters\<close>
     8 
     9 theory Free_Ultrafilter
    10   imports "~~/src/HOL/Library/Infinite_Set"
    11 begin
    12 
    13 
    14 subsection \<open>Definitions and basic properties\<close>
    15 
    16 subsubsection \<open>Ultrafilters\<close>
    17 
    18 locale 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"
    22 begin
    23 
    24 lemma eventually_imp_frequently: "frequently P F \<Longrightarrow> eventually P F"
    25   using ultra[of P] by (simp add: frequently_def)
    26 
    27 lemma frequently_eq_eventually: "frequently P F = eventually P F"
    28   using eventually_imp_frequently eventually_frequently[OF proper] ..
    29 
    30 lemma 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 
    33 lemma 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 
    36 lemma 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 
    39 lemma 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 
    42 lemma eventually_not_iff: "eventually (\<lambda>x. \<not> P x) F \<longleftrightarrow> \<not> eventually P F"
    43   unfolding not_eventually frequently_eq_eventually ..
    44 
    45 end
    46 
    47 
    48 subsection \<open>Maximal filter = Ultrafilter\<close>
    49 
    50 text \<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 "F \<subseteq> G"} then @{prop "F = G"}
    53 \<close>
    54 
    55 text \<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 
    61 lemma 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 
    64 lemma 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"
    68 proof
    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
    79 qed fact
    80 
    81 lemma 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 
    88 lemma (in ultrafilter) max_filter:
    89   assumes G: "G \<noteq> bot"
    90     and sub: "G \<le> F"
    91   shows "F = G"
    92 proof (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)
    97 qed fact
    98 
    99 
   100 subsection \<open>Ultrafilter Theorem\<close>
   101 
   102 lemma ex_max_ultrafilter:
   103   fixes F :: "'a filter"
   104   assumes F: "F \<noteq> bot"
   105   shows "\<exists>U\<le>F. ultrafilter U"
   106 proof -
   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 "\<forall>C\<in>Chains ?R. \<exists>u\<in>Field ?R. \<forall>a\<in>C. (a, u) \<in> ?R"
   122     proof (safe intro!: bexI del: notI)
   123       fix c x
   124       assume c: "c \<in> Chains ?R"
   125 
   126       have Inf_c: "Inf c \<noteq> bot" "Inf c \<le> F" if "c \<noteq> {}"
   127       proof -
   128         from c that have "Inf c = bot \<longleftrightarrow> (\<exists>x\<in>c. x = bot)"
   129           unfolding trivial_limit_def by (intro eventually_Inf_base) (auto simp: Chains_def)
   130         with c show "Inf c \<noteq> bot"
   131           by (simp add: bot_notin_R)
   132         from that obtain x where "x \<in> c" by auto
   133         with c show "Inf c \<le> F"
   134           by (auto intro!: Inf_lower2[of x] simp: Chains_def)
   135       qed
   136       then have [simp]: "inf F (Inf c) = (if c = {} then F else Inf c)"
   137         using c by (auto simp add: inf_absorb2)
   138 
   139       from c show "inf F (Inf c) \<noteq> bot"
   140         by (simp add: F Inf_c)
   141       from c show "inf F (Inf c) \<in> Field ?R"
   142         by (simp add: Chains_def Inf_c F)
   143 
   144       assume "x \<in> c"
   145       with c show "inf F (Inf c) \<le> x" "x \<le> F"
   146         by (auto intro: Inf_lower simp: Chains_def)
   147     qed
   148   qed
   149   then obtain U where U: "U \<in> ?A" "?B U" ..
   150   show ?thesis
   151   proof
   152     from U show "U \<le> F \<and> ultrafilter U"
   153       by (auto intro!: max_filter_ultrafilter)
   154   qed
   155 qed
   156 
   157 
   158 subsubsection \<open>Free Ultrafilters\<close>
   159 
   160 text \<open>There exists a free ultrafilter on any infinite set.\<close>
   161 
   162 locale freeultrafilter = ultrafilter +
   163   assumes infinite: "eventually P F \<Longrightarrow> infinite {x. P x}"
   164 begin
   165 
   166 lemma finite: "finite {x. P x} \<Longrightarrow> \<not> eventually P F"
   167   by (erule contrapos_pn) (erule infinite)
   168 
   169 lemma finite': "finite {x. \<not> P x} \<Longrightarrow> eventually P F"
   170   by (drule finite) (simp add: not_eventually frequently_eq_eventually)
   171 
   172 lemma le_cofinite: "F \<le> cofinite"
   173   by (intro filter_leI)
   174     (auto simp add: eventually_cofinite not_eventually frequently_eq_eventually dest!: finite)
   175 
   176 lemma singleton: "\<not> eventually (\<lambda>x. x = a) F"
   177   by (rule finite) simp
   178 
   179 lemma singleton': "\<not> eventually (op = a) F"
   180   by (rule finite) simp
   181 
   182 lemma ultrafilter: "ultrafilter F" ..
   183 
   184 end
   185 
   186 lemma freeultrafilter_Ex:
   187   assumes [simp]: "infinite (UNIV :: 'a set)"
   188   shows "\<exists>U::'a filter. freeultrafilter U"
   189 proof -
   190   from ex_max_ultrafilter[of "cofinite :: 'a filter"]
   191   obtain U :: "'a filter" where "U \<le> cofinite" "ultrafilter U"
   192     by auto
   193   interpret ultrafilter U by fact
   194   have "freeultrafilter U"
   195   proof
   196     fix P
   197     assume "eventually P U"
   198     with proper have "frequently P U"
   199       by (rule eventually_frequently)
   200     then have "frequently P cofinite"
   201       using \<open>U \<le> cofinite\<close> by (simp add: le_filter_frequently)
   202     then show "infinite {x. P x}"
   203       by (simp add: frequently_cofinite)
   204   qed
   205   then show ?thesis ..
   206 qed
   207 
   208 end