10 imports "~~/src/HOL/Library/Infinite_Set" |
10 imports "~~/src/HOL/Library/Infinite_Set" |
11 begin |
11 begin |
12 |
12 |
13 subsection {* Definitions and basic properties *} |
13 subsection {* Definitions and basic properties *} |
14 |
14 |
15 subsubsection {* Filters *} |
15 subsubsection {* Ultrafilters *} |
16 |
16 |
17 locale filter = |
17 locale ultrafilter = |
18 fixes F :: "'a set set" |
18 fixes F :: "'a filter" |
19 assumes UNIV [iff]: "UNIV \<in> F" |
19 assumes proper: "F \<noteq> bot" |
20 assumes empty [iff]: "{} \<notin> F" |
20 assumes ultra: "eventually P F \<or> eventually (\<lambda>x. \<not> P x) F" |
21 assumes Int: "\<lbrakk>u \<in> F; v \<in> F\<rbrakk> \<Longrightarrow> u \<inter> v \<in> F" |
|
22 assumes subset: "\<lbrakk>u \<in> F; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> F" |
|
23 begin |
21 begin |
24 |
22 |
25 lemma memD: "A \<in> F \<Longrightarrow> - A \<notin> F" |
23 lemma eventually_imp_frequently: "frequently P F \<Longrightarrow> eventually P F" |
26 proof |
24 using ultra[of P] by (simp add: frequently_def) |
27 assume "A \<in> F" and "- A \<in> F" |
25 |
28 hence "A \<inter> (- A) \<in> F" by (rule Int) |
26 lemma frequently_eq_eventually: "frequently P F = eventually P F" |
29 thus "False" by simp |
27 using eventually_imp_frequently eventually_frequently[OF proper] .. |
30 qed |
28 |
31 |
29 lemma eventually_disj_iff: "eventually (\<lambda>x. P x \<or> Q x) F \<longleftrightarrow> eventually P F \<or> eventually Q F" |
32 lemma not_memI: "- A \<in> F \<Longrightarrow> A \<notin> F" |
30 unfolding frequently_eq_eventually[symmetric] frequently_disj_iff .. |
33 by (drule memD, simp) |
31 |
34 |
32 lemma eventually_all_iff: "eventually (\<lambda>x. \<forall>y. P x y) F = (\<forall>Y. eventually (\<lambda>x. P x (Y x)) F)" |
35 lemma Int_iff: "(x \<inter> y \<in> F) = (x \<in> F \<and> y \<in> F)" |
33 using frequently_all[of P F] by (simp add: frequently_eq_eventually) |
36 by (auto elim: subset intro: Int) |
34 |
|
35 lemma eventually_imp_iff: "eventually (\<lambda>x. P x \<longrightarrow> Q x) F \<longleftrightarrow> (eventually P F \<longrightarrow> eventually Q F)" |
|
36 using frequently_imp_iff[of P Q F] by (simp add: frequently_eq_eventually) |
|
37 |
|
38 lemma eventually_iff_iff: "eventually (\<lambda>x. P x \<longleftrightarrow> Q x) F \<longleftrightarrow> (eventually P F \<longleftrightarrow> eventually Q F)" |
|
39 unfolding iff_conv_conj_imp eventually_conj_iff eventually_imp_iff by simp |
|
40 |
|
41 lemma eventually_not_iff: "eventually (\<lambda>x. \<not> P x) F \<longleftrightarrow> \<not> eventually P F" |
|
42 unfolding not_eventually frequently_eq_eventually .. |
37 |
43 |
38 end |
44 end |
39 |
|
40 subsubsection {* Ultrafilters *} |
|
41 |
|
42 locale ultrafilter = filter + |
|
43 assumes ultra: "A \<in> F \<or> - A \<in> F" |
|
44 begin |
|
45 |
|
46 lemma memI: "- A \<notin> F \<Longrightarrow> A \<in> F" |
|
47 using ultra [of A] by simp |
|
48 |
|
49 lemma not_memD: "A \<notin> F \<Longrightarrow> - A \<in> F" |
|
50 by (rule memI, simp) |
|
51 |
|
52 lemma not_mem_iff: "(A \<notin> F) = (- A \<in> F)" |
|
53 by (rule iffI [OF not_memD not_memI]) |
|
54 |
|
55 lemma Compl_iff: "(- A \<in> F) = (A \<notin> F)" |
|
56 by (rule iffI [OF not_memI not_memD]) |
|
57 |
|
58 lemma Un_iff: "(x \<union> y \<in> F) = (x \<in> F \<or> y \<in> F)" |
|
59 apply (rule iffI) |
|
60 apply (erule contrapos_pp) |
|
61 apply (simp add: Int_iff not_mem_iff) |
|
62 apply (auto elim: subset) |
|
63 done |
|
64 |
|
65 end |
|
66 |
|
67 subsubsection {* Free Ultrafilters *} |
|
68 |
|
69 locale freeultrafilter = ultrafilter + |
|
70 assumes infinite: "A \<in> F \<Longrightarrow> infinite A" |
|
71 begin |
|
72 |
|
73 lemma finite: "finite A \<Longrightarrow> A \<notin> F" |
|
74 by (erule contrapos_pn, erule infinite) |
|
75 |
|
76 lemma singleton: "{x} \<notin> F" |
|
77 by (rule finite, simp) |
|
78 |
|
79 lemma insert_iff [simp]: "(insert x A \<in> F) = (A \<in> F)" |
|
80 apply (subst insert_is_Un) |
|
81 apply (subst Un_iff) |
|
82 apply (simp add: singleton) |
|
83 done |
|
84 |
|
85 lemma filter: "filter F" .. |
|
86 |
|
87 lemma ultrafilter: "ultrafilter F" .. |
|
88 |
|
89 end |
|
90 |
|
91 subsection {* Collect properties *} |
|
92 |
|
93 lemma (in filter) Collect_ex: |
|
94 "({n. \<exists>x. P n x} \<in> F) = (\<exists>X. {n. P n (X n)} \<in> F)" |
|
95 proof |
|
96 assume "{n. \<exists>x. P n x} \<in> F" |
|
97 hence "{n. P n (SOME x. P n x)} \<in> F" |
|
98 by (auto elim: someI subset) |
|
99 thus "\<exists>X. {n. P n (X n)} \<in> F" by fast |
|
100 next |
|
101 show "\<exists>X. {n. P n (X n)} \<in> F \<Longrightarrow> {n. \<exists>x. P n x} \<in> F" |
|
102 by (auto elim: subset) |
|
103 qed |
|
104 |
|
105 lemma (in filter) Collect_conj: |
|
106 "({n. P n \<and> Q n} \<in> F) = ({n. P n} \<in> F \<and> {n. Q n} \<in> F)" |
|
107 by (subst Collect_conj_eq, rule Int_iff) |
|
108 |
|
109 lemma (in ultrafilter) Collect_not: |
|
110 "({n. \<not> P n} \<in> F) = ({n. P n} \<notin> F)" |
|
111 by (subst Collect_neg_eq, rule Compl_iff) |
|
112 |
|
113 lemma (in ultrafilter) Collect_disj: |
|
114 "({n. P n \<or> Q n} \<in> F) = ({n. P n} \<in> F \<or> {n. Q n} \<in> F)" |
|
115 by (subst Collect_disj_eq, rule Un_iff) |
|
116 |
|
117 lemma (in ultrafilter) Collect_all: |
|
118 "({n. \<forall>x. P n x} \<in> F) = (\<forall>X. {n. P n (X n)} \<in> F)" |
|
119 apply (rule Not_eq_iff [THEN iffD1]) |
|
120 apply (simp add: Collect_not [symmetric]) |
|
121 apply (rule Collect_ex) |
|
122 done |
|
123 |
45 |
124 subsection {* Maximal filter = Ultrafilter *} |
46 subsection {* Maximal filter = Ultrafilter *} |
125 |
47 |
126 text {* |
48 text {* |
127 A filter F is an ultrafilter iff it is a maximal filter, |
49 A filter F is an ultrafilter iff it is a maximal filter, |
131 Lemmas that shows existence of an extension to what was assumed to |
53 Lemmas that shows existence of an extension to what was assumed to |
132 be a maximal filter. Will be used to derive contradiction in proof of |
54 be a maximal filter. Will be used to derive contradiction in proof of |
133 property of ultrafilter. |
55 property of ultrafilter. |
134 *} |
56 *} |
135 |
57 |
136 lemma extend_lemma1: "UNIV \<in> F \<Longrightarrow> A \<in> {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}" |
58 lemma extend_filter: |
137 by blast |
59 "frequently P F \<Longrightarrow> inf F (principal {x. P x}) \<noteq> bot" |
138 |
60 unfolding trivial_limit_def eventually_inf_principal by (simp add: not_eventually) |
139 lemma extend_lemma2: "F \<subseteq> {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}" |
61 |
140 by blast |
62 lemma max_filter_ultrafilter: |
141 |
63 assumes proper: "F \<noteq> bot" |
142 lemma (in filter) extend_filter: |
64 assumes max: "\<And>G. G \<noteq> bot \<Longrightarrow> G \<le> F \<Longrightarrow> F = G" |
143 assumes A: "- A \<notin> F" |
65 shows "ultrafilter F" |
144 shows "filter {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}" (is "filter ?X") |
66 proof |
145 proof (rule filter.intro) |
67 fix P show "eventually P F \<or> (\<forall>\<^sub>Fx in F. \<not> P x)" |
146 show "UNIV \<in> ?X" by blast |
68 proof (rule disjCI) |
147 next |
69 assume "\<not> (\<forall>\<^sub>Fx in F. \<not> P x)" |
148 show "{} \<notin> ?X" |
70 then have "inf F (principal {x. P x}) \<noteq> bot" |
149 proof (clarify) |
71 by (simp add: not_eventually extend_filter) |
150 fix f assume f: "f \<in> F" and Af: "A \<inter> f \<subseteq> {}" |
72 then have F: "F = inf F (principal {x. P x})" |
151 from Af have fA: "f \<subseteq> - A" by blast |
73 by (rule max) simp |
152 from f fA have "- A \<in> F" by (rule subset) |
74 show "eventually P F" |
153 with A show "False" by simp |
75 by (subst F) (simp add: eventually_inf_principal) |
154 qed |
76 qed |
155 next |
77 qed fact |
156 fix u and v |
78 |
157 assume u: "u \<in> ?X" and v: "v \<in> ?X" |
79 lemma le_filter_frequently: "F \<le> G \<longleftrightarrow> (\<forall>P. frequently P F \<longrightarrow> frequently P G)" |
158 from u obtain f where f: "f \<in> F" and Af: "A \<inter> f \<subseteq> u" by blast |
80 unfolding frequently_def le_filter_def |
159 from v obtain g where g: "g \<in> F" and Ag: "A \<inter> g \<subseteq> v" by blast |
81 apply auto |
160 from f g have fg: "f \<inter> g \<in> F" by (rule Int) |
82 apply (erule_tac x="\<lambda>x. \<not> P x" in allE) |
161 from Af Ag have Afg: "A \<inter> (f \<inter> g) \<subseteq> u \<inter> v" by blast |
83 apply auto |
162 from fg Afg show "u \<inter> v \<in> ?X" by blast |
84 done |
163 next |
85 |
164 fix u and v |
86 lemma (in ultrafilter) max_filter: |
165 assume uv: "u \<subseteq> v" and u: "u \<in> ?X" |
87 assumes G: "G \<noteq> bot" and sub: "G \<le> F" shows "F = G" |
166 from u obtain f where f: "f \<in> F" and Afu: "A \<inter> f \<subseteq> u" by blast |
88 proof (rule antisym) |
167 from Afu uv have Afv: "A \<inter> f \<subseteq> v" by blast |
89 show "F \<le> G" |
168 from f Afv have "\<exists>f\<in>F. A \<inter> f \<subseteq> v" by blast |
90 using sub |
169 thus "v \<in> ?X" by simp |
91 by (auto simp: le_filter_frequently[of F] frequently_eq_eventually le_filter_def[of G] |
|
92 intro!: eventually_frequently G proper) |
|
93 qed fact |
|
94 |
|
95 subsection {* Ultrafilter Theorem *} |
|
96 |
|
97 text "A local context makes proof of ultrafilter Theorem more modular" |
|
98 |
|
99 lemma ex_max_ultrafilter: |
|
100 fixes F :: "'a filter" |
|
101 assumes F: "F \<noteq> bot" |
|
102 shows "\<exists>U\<le>F. ultrafilter U" |
|
103 proof - |
|
104 let ?X = "{G. G \<noteq> bot \<and> G \<le> F}" |
|
105 let ?R = "{(b, a). a \<noteq> bot \<and> a \<le> b \<and> b \<le> F}" |
|
106 |
|
107 have bot_notin_R: "\<And>c. c \<in> Chains ?R \<Longrightarrow> bot \<notin> c" |
|
108 by (auto simp: Chains_def) |
|
109 |
|
110 have [simp]: "Field ?R = ?X" |
|
111 by (auto simp: Field_def bot_unique) |
|
112 |
|
113 have "\<exists>m\<in>Field ?R. \<forall>a\<in>Field ?R. (m, a) \<in> ?R \<longrightarrow> a = m" |
|
114 proof (rule Zorns_po_lemma) |
|
115 show "Partial_order ?R" |
|
116 unfolding partial_order_on_def preorder_on_def |
|
117 by (auto simp: antisym_def refl_on_def trans_def Field_def bot_unique) |
|
118 show "\<forall>C\<in>Chains ?R. \<exists>u\<in>Field ?R. \<forall>a\<in>C. (a, u) \<in> ?R" |
|
119 proof (safe intro!: bexI del: notI) |
|
120 fix c x assume c: "c \<in> Chains ?R" |
|
121 |
|
122 { assume "c \<noteq> {}" |
|
123 with c have "Inf c = bot \<longleftrightarrow> (\<exists>x\<in>c. x = bot)" |
|
124 unfolding trivial_limit_def by (intro eventually_Inf_base) (auto simp: Chains_def) |
|
125 with c have 1: "Inf c \<noteq> bot" |
|
126 by (simp add: bot_notin_R) |
|
127 from `c \<noteq> {}` obtain x where "x \<in> c" by auto |
|
128 with c have 2: "Inf c \<le> F" |
|
129 by (auto intro!: Inf_lower2[of x] simp: Chains_def) |
|
130 note 1 2 } |
|
131 note Inf_c = this |
|
132 then have [simp]: "inf F (Inf c) = (if c = {} then F else Inf c)" |
|
133 using c by (auto simp add: inf_absorb2) |
|
134 |
|
135 show "inf F (Inf c) \<noteq> bot" |
|
136 using c by (simp add: F Inf_c) |
|
137 |
|
138 show "inf F (Inf c) \<in> Field ?R" |
|
139 using c by (simp add: Chains_def Inf_c F) |
|
140 |
|
141 assume x: "x \<in> c" |
|
142 with c show "inf F (Inf c) \<le> x" "x \<le> F" |
|
143 by (auto intro: Inf_lower simp: Chains_def) |
|
144 qed |
|
145 qed |
|
146 then guess U .. |
|
147 then show ?thesis |
|
148 by (intro exI[of _ U] conjI max_filter_ultrafilter) auto |
170 qed |
149 qed |
171 |
150 |
172 lemma (in filter) max_filter_ultrafilter: |
151 subsubsection {* Free Ultrafilters *} |
173 assumes max: "\<And>G. \<lbrakk>filter G; F \<subseteq> G\<rbrakk> \<Longrightarrow> F = G" |
152 |
174 shows "ultrafilter_axioms F" |
153 text {* There exists a free ultrafilter on any infinite set *} |
175 proof (rule ultrafilter_axioms.intro) |
154 |
176 fix A show "A \<in> F \<or> - A \<in> F" |
155 locale freeultrafilter = ultrafilter + |
177 proof (rule disjCI) |
156 assumes infinite: "eventually P F \<Longrightarrow> infinite {x. P x}" |
178 let ?X = "{X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}" |
157 begin |
179 assume AF: "- A \<notin> F" |
158 |
180 from AF have X: "filter ?X" by (rule extend_filter) |
159 lemma finite: "finite {x. P x} \<Longrightarrow> \<not> eventually P F" |
181 from UNIV have AX: "A \<in> ?X" by (rule extend_lemma1) |
160 by (erule contrapos_pn, erule infinite) |
182 have FX: "F \<subseteq> ?X" by (rule extend_lemma2) |
161 |
183 from X FX have "F = ?X" by (rule max) |
162 lemma finite': "finite {x. \<not> P x} \<Longrightarrow> eventually P F" |
184 with AX show "A \<in> F" by simp |
163 by (drule finite) (simp add: not_eventually frequently_eq_eventually) |
|
164 |
|
165 lemma le_cofinite: "F \<le> cofinite" |
|
166 by (intro filter_leI) |
|
167 (auto simp add: eventually_cofinite not_eventually frequently_eq_eventually dest!: finite) |
|
168 |
|
169 lemma singleton: "\<not> eventually (\<lambda>x. x = a) F" |
|
170 by (rule finite, simp) |
|
171 |
|
172 lemma singleton': "\<not> eventually (op = a) F" |
|
173 by (rule finite, simp) |
|
174 |
|
175 lemma ultrafilter: "ultrafilter F" .. |
|
176 |
|
177 end |
|
178 |
|
179 lemma freeultrafilter_Ex: |
|
180 assumes [simp]: "infinite (UNIV :: 'a set)" |
|
181 shows "\<exists>U::'a filter. freeultrafilter U" |
|
182 proof - |
|
183 from ex_max_ultrafilter[of "cofinite :: 'a filter"] |
|
184 obtain U :: "'a filter" where "U \<le> cofinite" "ultrafilter U" |
|
185 by auto |
|
186 interpret ultrafilter U by fact |
|
187 have "freeultrafilter U" |
|
188 proof |
|
189 fix P assume "eventually P U" |
|
190 with proper have "frequently P U" |
|
191 by (rule eventually_frequently) |
|
192 then have "frequently P cofinite" |
|
193 using `U \<le> cofinite` by (simp add: le_filter_frequently) |
|
194 then show "infinite {x. P x}" |
|
195 by (simp add: frequently_cofinite) |
185 qed |
196 qed |
186 qed |
|
187 |
|
188 lemma (in ultrafilter) max_filter: |
|
189 assumes G: "filter G" and sub: "F \<subseteq> G" shows "F = G" |
|
190 proof |
|
191 show "F \<subseteq> G" using sub . |
|
192 show "G \<subseteq> F" |
|
193 proof |
|
194 fix A assume A: "A \<in> G" |
|
195 from G A have "- A \<notin> G" by (rule filter.memD) |
|
196 with sub have B: "- A \<notin> F" by blast |
|
197 thus "A \<in> F" by (rule memI) |
|
198 qed |
|
199 qed |
|
200 |
|
201 subsection {* Ultrafilter Theorem *} |
|
202 |
|
203 text "A local context makes proof of ultrafilter Theorem more modular" |
|
204 context |
|
205 fixes frechet :: "'a set set" |
|
206 and superfrechet :: "'a set set set" |
|
207 |
|
208 assumes infinite_UNIV: "infinite (UNIV :: 'a set)" |
|
209 |
|
210 defines frechet_def: "frechet \<equiv> {A. finite (- A)}" |
|
211 and superfrechet_def: "superfrechet \<equiv> {G. filter G \<and> frechet \<subseteq> G}" |
|
212 begin |
|
213 |
|
214 lemma superfrechetI: |
|
215 "\<lbrakk>filter G; frechet \<subseteq> G\<rbrakk> \<Longrightarrow> G \<in> superfrechet" |
|
216 by (simp add: superfrechet_def) |
|
217 |
|
218 lemma superfrechetD1: |
|
219 "G \<in> superfrechet \<Longrightarrow> filter G" |
|
220 by (simp add: superfrechet_def) |
|
221 |
|
222 lemma superfrechetD2: |
|
223 "G \<in> superfrechet \<Longrightarrow> frechet \<subseteq> G" |
|
224 by (simp add: superfrechet_def) |
|
225 |
|
226 text {* A few properties of free filters *} |
|
227 |
|
228 lemma filter_cofinite: |
|
229 assumes inf: "infinite (UNIV :: 'a set)" |
|
230 shows "filter {A:: 'a set. finite (- A)}" (is "filter ?F") |
|
231 proof (rule filter.intro) |
|
232 show "UNIV \<in> ?F" by simp |
|
233 next |
|
234 show "{} \<notin> ?F" using inf by simp |
|
235 next |
|
236 fix u v assume "u \<in> ?F" and "v \<in> ?F" |
|
237 thus "u \<inter> v \<in> ?F" by simp |
|
238 next |
|
239 fix u v assume uv: "u \<subseteq> v" and u: "u \<in> ?F" |
|
240 from uv have vu: "- v \<subseteq> - u" by simp |
|
241 from u show "v \<in> ?F" |
|
242 by (simp add: finite_subset [OF vu]) |
|
243 qed |
|
244 |
|
245 text {* |
|
246 We prove: 1. Existence of maximal filter i.e. ultrafilter; |
|
247 2. Freeness property i.e ultrafilter is free. |
|
248 Use a locale to prove various lemmas and then |
|
249 export main result: The ultrafilter Theorem |
|
250 *} |
|
251 |
|
252 lemma filter_frechet: "filter frechet" |
|
253 by (unfold frechet_def, rule filter_cofinite [OF infinite_UNIV]) |
|
254 |
|
255 lemma frechet_in_superfrechet: "frechet \<in> superfrechet" |
|
256 by (rule superfrechetI [OF filter_frechet subset_refl]) |
|
257 |
|
258 lemma lemma_mem_chain_filter: |
|
259 "\<lbrakk>c \<in> chains superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> filter x" |
|
260 by (unfold chains_def superfrechet_def, blast) |
|
261 |
|
262 |
|
263 subsubsection {* Unions of chains of superfrechets *} |
|
264 |
|
265 text "In this section we prove that superfrechet is closed |
|
266 with respect to unions of non-empty chains. We must show |
|
267 1) Union of a chain is a filter, |
|
268 2) Union of a chain contains frechet. |
|
269 |
|
270 Number 2 is trivial, but 1 requires us to prove all the filter rules." |
|
271 |
|
272 lemma Union_chain_UNIV: |
|
273 "\<lbrakk>c \<in> chains superfrechet; c \<noteq> {}\<rbrakk> \<Longrightarrow> UNIV \<in> \<Union>c" |
|
274 proof - |
|
275 assume 1: "c \<in> chains superfrechet" and 2: "c \<noteq> {}" |
|
276 from 2 obtain x where 3: "x \<in> c" by blast |
|
277 from 1 3 have "filter x" by (rule lemma_mem_chain_filter) |
|
278 hence "UNIV \<in> x" by (rule filter.UNIV) |
|
279 with 3 show "UNIV \<in> \<Union>c" by blast |
|
280 qed |
|
281 |
|
282 lemma Union_chain_empty: |
|
283 "c \<in> chains superfrechet \<Longrightarrow> {} \<notin> \<Union>c" |
|
284 proof |
|
285 assume 1: "c \<in> chains superfrechet" and 2: "{} \<in> \<Union>c" |
|
286 from 2 obtain x where 3: "x \<in> c" and 4: "{} \<in> x" .. |
|
287 from 1 3 have "filter x" by (rule lemma_mem_chain_filter) |
|
288 hence "{} \<notin> x" by (rule filter.empty) |
|
289 with 4 show "False" by simp |
|
290 qed |
|
291 |
|
292 lemma Union_chain_Int: |
|
293 "\<lbrakk>c \<in> chains superfrechet; u \<in> \<Union>c; v \<in> \<Union>c\<rbrakk> \<Longrightarrow> u \<inter> v \<in> \<Union>c" |
|
294 proof - |
|
295 assume c: "c \<in> chains superfrechet" |
|
296 assume "u \<in> \<Union>c" |
|
297 then obtain x where ux: "u \<in> x" and xc: "x \<in> c" .. |
|
298 assume "v \<in> \<Union>c" |
|
299 then obtain y where vy: "v \<in> y" and yc: "y \<in> c" .. |
|
300 from c xc yc have "x \<subseteq> y \<or> y \<subseteq> x" using c unfolding chains_def chain_subset_def by auto |
|
301 with xc yc have xyc: "x \<union> y \<in> c" |
|
302 by (auto simp add: Un_absorb1 Un_absorb2) |
|
303 with c have fxy: "filter (x \<union> y)" by (rule lemma_mem_chain_filter) |
|
304 from ux have uxy: "u \<in> x \<union> y" by simp |
|
305 from vy have vxy: "v \<in> x \<union> y" by simp |
|
306 from fxy uxy vxy have "u \<inter> v \<in> x \<union> y" by (rule filter.Int) |
|
307 with xyc show "u \<inter> v \<in> \<Union>c" .. |
|
308 qed |
|
309 |
|
310 lemma Union_chain_subset: |
|
311 "\<lbrakk>c \<in> chains superfrechet; u \<in> \<Union>c; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> \<Union>c" |
|
312 proof - |
|
313 assume c: "c \<in> chains superfrechet" |
|
314 and u: "u \<in> \<Union>c" and uv: "u \<subseteq> v" |
|
315 from u obtain x where ux: "u \<in> x" and xc: "x \<in> c" .. |
|
316 from c xc have fx: "filter x" by (rule lemma_mem_chain_filter) |
|
317 from fx ux uv have vx: "v \<in> x" by (rule filter.subset) |
|
318 with xc show "v \<in> \<Union>c" .. |
|
319 qed |
|
320 |
|
321 lemma Union_chain_filter: |
|
322 assumes chain: "c \<in> chains superfrechet" and nonempty: "c \<noteq> {}" |
|
323 shows "filter (\<Union>c)" |
|
324 proof (rule filter.intro) |
|
325 show "UNIV \<in> \<Union>c" using chain nonempty by (rule Union_chain_UNIV) |
|
326 next |
|
327 show "{} \<notin> \<Union>c" using chain by (rule Union_chain_empty) |
|
328 next |
|
329 fix u v assume "u \<in> \<Union>c" and "v \<in> \<Union>c" |
|
330 with chain show "u \<inter> v \<in> \<Union>c" by (rule Union_chain_Int) |
|
331 next |
|
332 fix u v assume "u \<in> \<Union>c" and "u \<subseteq> v" |
|
333 with chain show "v \<in> \<Union>c" by (rule Union_chain_subset) |
|
334 qed |
|
335 |
|
336 lemma lemma_mem_chain_frechet_subset: |
|
337 "\<lbrakk>c \<in> chains superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> frechet \<subseteq> x" |
|
338 by (unfold superfrechet_def chains_def, blast) |
|
339 |
|
340 lemma Union_chain_superfrechet: |
|
341 "\<lbrakk>c \<noteq> {}; c \<in> chains superfrechet\<rbrakk> \<Longrightarrow> \<Union>c \<in> superfrechet" |
|
342 proof (rule superfrechetI) |
|
343 assume 1: "c \<in> chains superfrechet" and 2: "c \<noteq> {}" |
|
344 thus "filter (\<Union>c)" by (rule Union_chain_filter) |
|
345 from 2 obtain x where 3: "x \<in> c" by blast |
|
346 from 1 3 have "frechet \<subseteq> x" by (rule lemma_mem_chain_frechet_subset) |
|
347 also from 3 have "x \<subseteq> \<Union>c" by blast |
|
348 finally show "frechet \<subseteq> \<Union>c" . |
|
349 qed |
|
350 |
|
351 subsubsection {* Existence of free ultrafilter *} |
|
352 |
|
353 lemma max_cofinite_filter_Ex: |
|
354 "\<exists>U\<in>superfrechet. \<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> G = U" |
|
355 proof (rule Zorn_Lemma2, safe) |
|
356 fix c assume c: "c \<in> chains superfrechet" |
|
357 show "\<exists>U\<in>superfrechet. \<forall>G\<in>c. G \<subseteq> U" (is "?U") |
|
358 proof (cases) |
|
359 assume "c = {}" |
|
360 with frechet_in_superfrechet show "?U" by blast |
|
361 next |
|
362 assume A: "c \<noteq> {}" |
|
363 from A c have "\<Union>c \<in> superfrechet" |
|
364 by (rule Union_chain_superfrechet) |
|
365 thus "?U" by blast |
|
366 qed |
|
367 qed |
|
368 |
|
369 lemma mem_superfrechet_all_infinite: |
|
370 "\<lbrakk>U \<in> superfrechet; A \<in> U\<rbrakk> \<Longrightarrow> infinite A" |
|
371 proof |
|
372 assume U: "U \<in> superfrechet" and A: "A \<in> U" and fin: "finite A" |
|
373 from U have fil: "filter U" and fre: "frechet \<subseteq> U" |
|
374 by (simp_all add: superfrechet_def) |
|
375 from fin have "- A \<in> frechet" by (simp add: frechet_def) |
|
376 with fre have cA: "- A \<in> U" by (rule subsetD) |
|
377 from fil A cA have "A \<inter> - A \<in> U" by (rule filter.Int) |
|
378 with fil show "False" by (simp add: filter.empty) |
|
379 qed |
|
380 |
|
381 text {* There exists a free ultrafilter on any infinite set *} |
|
382 |
|
383 lemma freeultrafilter_Ex: |
|
384 "\<exists>U::'a set set. freeultrafilter U" |
|
385 proof - |
|
386 from max_cofinite_filter_Ex obtain U |
|
387 where U: "U \<in> superfrechet" |
|
388 and max [rule_format]: "\<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> G = U" .. |
|
389 from U have fil: "filter U" by (rule superfrechetD1) |
|
390 from U have fre: "frechet \<subseteq> U" by (rule superfrechetD2) |
|
391 have ultra: "ultrafilter_axioms U" |
|
392 proof (rule filter.max_filter_ultrafilter [OF fil]) |
|
393 fix G assume G: "filter G" and UG: "U \<subseteq> G" |
|
394 from fre UG have "frechet \<subseteq> G" by simp |
|
395 with G have "G \<in> superfrechet" by (rule superfrechetI) |
|
396 from this UG show "U = G" by (rule max[symmetric]) |
|
397 qed |
|
398 have free: "freeultrafilter_axioms U" |
|
399 proof (rule freeultrafilter_axioms.intro) |
|
400 fix A assume "A \<in> U" |
|
401 with U show "infinite A" by (rule mem_superfrechet_all_infinite) |
|
402 qed |
|
403 from fil ultra free have "freeultrafilter U" |
|
404 by (rule freeultrafilter.intro [OF ultrafilter.intro]) |
|
405 (* FIXME: unfold_locales should use chained facts *) |
|
406 then show ?thesis .. |
197 then show ?thesis .. |
407 qed |
198 qed |
408 |
199 |
409 end |
200 end |
410 |
|
411 hide_const (open) filter |
|
412 |
|
413 end |
|