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