|
1 (* Title : Filter.ML |
|
2 ID : $Id$ |
|
3 Author : Jacques D. Fleuriot |
|
4 Copyright : 1998 University of Cambridge |
|
5 Description : Filters and Ultrafilter |
|
6 *) |
|
7 |
|
8 (*------------------------------------------------------------------ |
|
9 Properties of Filters and Freefilters - |
|
10 rules for intro, destruction etc. |
|
11 ------------------------------------------------------------------*) |
|
12 |
|
13 Goalw [is_Filter_def] "is_Filter X S ==> X <= Pow(S)"; |
|
14 by (Blast_tac 1); |
|
15 qed "is_FilterD1"; |
|
16 |
|
17 Goalw [is_Filter_def] "is_Filter X S ==> X ~= {}"; |
|
18 by (Blast_tac 1); |
|
19 qed "is_FilterD2"; |
|
20 |
|
21 Goalw [is_Filter_def] "is_Filter X S ==> {} ~: X"; |
|
22 by (Blast_tac 1); |
|
23 qed "is_FilterD3"; |
|
24 |
|
25 Goalw [Filter_def] "is_Filter X S ==> X : Filter S"; |
|
26 by (Blast_tac 1); |
|
27 qed "mem_FiltersetI"; |
|
28 |
|
29 Goalw [Filter_def] "X : Filter S ==> is_Filter X S"; |
|
30 by (Blast_tac 1); |
|
31 qed "mem_FiltersetD"; |
|
32 |
|
33 Goal "X : Filter S ==> {} ~: X"; |
|
34 by (etac (mem_FiltersetD RS is_FilterD3) 1); |
|
35 qed "Filter_empty_not_mem"; |
|
36 |
|
37 bind_thm ("Filter_empty_not_memE",(Filter_empty_not_mem RS notE)); |
|
38 |
|
39 Goalw [Filter_def,is_Filter_def] |
|
40 "[| X: Filter S; A: X; B: X |] ==> A Int B : X"; |
|
41 by (Blast_tac 1); |
|
42 qed "mem_FiltersetD1"; |
|
43 |
|
44 Goalw [Filter_def,is_Filter_def] |
|
45 "[| X: Filter S; A: X; A <= B; B <= S|] ==> B : X"; |
|
46 by (Blast_tac 1); |
|
47 qed "mem_FiltersetD2"; |
|
48 |
|
49 Goalw [Filter_def,is_Filter_def] |
|
50 "[| X: Filter S; A: X |] ==> A : Pow S"; |
|
51 by (Blast_tac 1); |
|
52 qed "mem_FiltersetD3"; |
|
53 |
|
54 Goalw [Filter_def,is_Filter_def] |
|
55 "X: Filter S ==> S : X"; |
|
56 by (Blast_tac 1); |
|
57 qed "mem_FiltersetD4"; |
|
58 |
|
59 Goalw [is_Filter_def] |
|
60 "[| X <= Pow(S);\ |
|
61 \ S : X; \ |
|
62 \ X ~= {}; \ |
|
63 \ {} ~: X; \ |
|
64 \ ALL u: X. ALL v: X. u Int v : X; \ |
|
65 \ ALL u v. u: X & u<=v & v<=S --> v: X \ |
|
66 \ |] ==> is_Filter X S"; |
|
67 by (Blast_tac 1); |
|
68 qed "is_FilterI"; |
|
69 |
|
70 Goal "[| X <= Pow(S);\ |
|
71 \ S : X; \ |
|
72 \ X ~= {}; \ |
|
73 \ {} ~: X; \ |
|
74 \ ALL u: X. ALL v: X. u Int v : X; \ |
|
75 \ ALL u v. u: X & u<=v & v<=S --> v: X \ |
|
76 \ |] ==> X: Filter S"; |
|
77 by (blast_tac (claset() addIs [mem_FiltersetI,is_FilterI]) 1); |
|
78 qed "mem_FiltersetI2"; |
|
79 |
|
80 Goalw [is_Filter_def] |
|
81 "is_Filter X S ==> X <= Pow(S) & \ |
|
82 \ S : X & \ |
|
83 \ X ~= {} & \ |
|
84 \ {} ~: X & \ |
|
85 \ (ALL u: X. ALL v: X. u Int v : X) & \ |
|
86 \ (ALL u v. u: X & u <= v & v<=S --> v: X)"; |
|
87 by (Fast_tac 1); |
|
88 qed "is_FilterE_lemma"; |
|
89 |
|
90 Goalw [is_Filter_def] |
|
91 "X : Filter S ==> X <= Pow(S) &\ |
|
92 \ S : X & \ |
|
93 \ X ~= {} & \ |
|
94 \ {} ~: X & \ |
|
95 \ (ALL u: X. ALL v: X. u Int v : X) & \ |
|
96 \ (ALL u v. u: X & u <= v & v<=S --> v: X)"; |
|
97 by (etac (mem_FiltersetD RS is_FilterE_lemma) 1); |
|
98 qed "memFiltersetE_lemma"; |
|
99 |
|
100 Goalw [Filter_def,Freefilter_def] |
|
101 "X: Freefilter S ==> X: Filter S"; |
|
102 by (Fast_tac 1); |
|
103 qed "Freefilter_Filter"; |
|
104 |
|
105 Goalw [Freefilter_def] |
|
106 "X: Freefilter S ==> ALL y: X. ~finite(y)"; |
|
107 by (Blast_tac 1); |
|
108 qed "mem_Freefilter_not_finite"; |
|
109 |
|
110 Goal "[| X: Freefilter S; x: X |] ==> ~ finite x"; |
|
111 by (blast_tac (claset() addSDs [mem_Freefilter_not_finite]) 1); |
|
112 qed "mem_FreefiltersetD1"; |
|
113 |
|
114 bind_thm ("mem_FreefiltersetE1", (mem_FreefiltersetD1 RS notE)); |
|
115 |
|
116 Goal "[| X: Freefilter S; finite x|] ==> x ~: X"; |
|
117 by (blast_tac (claset() addSDs [mem_Freefilter_not_finite]) 1); |
|
118 qed "mem_FreefiltersetD2"; |
|
119 |
|
120 Goalw [Freefilter_def] |
|
121 "[| X: Filter S; ALL x. ~(x: X & finite x) |] ==> X: Freefilter S"; |
|
122 by (Blast_tac 1); |
|
123 qed "mem_FreefiltersetI1"; |
|
124 |
|
125 Goalw [Freefilter_def] |
|
126 "[| X: Filter S; ALL x. (x ~: X | ~ finite x) |] ==> X: Freefilter S"; |
|
127 by (Blast_tac 1); |
|
128 qed "mem_FreefiltersetI2"; |
|
129 |
|
130 Goal "[| X: Filter S; A: X; B: X |] ==> A Int B ~= {}"; |
|
131 by (forw_inst_tac [("A","A"),("B","B")] mem_FiltersetD1 1); |
|
132 by (auto_tac (claset() addSDs [Filter_empty_not_mem],simpset())); |
|
133 qed "Filter_Int_not_empty"; |
|
134 |
|
135 bind_thm ("Filter_Int_not_emptyE",(Filter_Int_not_empty RS notE)); |
|
136 |
|
137 (*---------------------------------------------------------------------------------- |
|
138 Ultrafilters and Free ultrafilters |
|
139 ----------------------------------------------------------------------------------*) |
|
140 |
|
141 Goalw [Ultrafilter_def] "X : Ultrafilter S ==> X: Filter S"; |
|
142 by (Blast_tac 1); |
|
143 qed "Ultrafilter_Filter"; |
|
144 |
|
145 Goalw [Ultrafilter_def] |
|
146 "X : Ultrafilter S ==> !A: Pow(S). A : X | S - A: X"; |
|
147 by (Blast_tac 1); |
|
148 qed "mem_UltrafiltersetD2"; |
|
149 |
|
150 Goalw [Ultrafilter_def] |
|
151 "[|X : Ultrafilter S; A <= S; A ~: X |] ==> S - A: X"; |
|
152 by (Blast_tac 1); |
|
153 qed "mem_UltrafiltersetD3"; |
|
154 |
|
155 Goalw [Ultrafilter_def] |
|
156 "[|X : Ultrafilter S; A <= S; S - A ~: X |] ==> A: X"; |
|
157 by (Blast_tac 1); |
|
158 qed "mem_UltrafiltersetD4"; |
|
159 |
|
160 Goalw [Ultrafilter_def] |
|
161 "[| X: Filter S; \ |
|
162 \ ALL A: Pow(S). A: X | S - A : X |] ==> X: Ultrafilter S"; |
|
163 by (Blast_tac 1); |
|
164 qed "mem_UltrafiltersetI"; |
|
165 |
|
166 Goalw [Ultrafilter_def,FreeUltrafilter_def] |
|
167 "X: FreeUltrafilter S ==> X: Ultrafilter S"; |
|
168 by (Blast_tac 1); |
|
169 qed "FreeUltrafilter_Ultrafilter"; |
|
170 |
|
171 Goalw [FreeUltrafilter_def] |
|
172 "X: FreeUltrafilter S ==> ALL y: X. ~finite(y)"; |
|
173 by (Blast_tac 1); |
|
174 qed "mem_FreeUltrafilter_not_finite"; |
|
175 |
|
176 Goal "[| X: FreeUltrafilter S; x: X |] ==> ~ finite x"; |
|
177 by (blast_tac (claset() addSDs [mem_FreeUltrafilter_not_finite]) 1); |
|
178 qed "mem_FreeUltrafiltersetD1"; |
|
179 |
|
180 bind_thm ("mem_FreeUltrafiltersetE1", (mem_FreeUltrafiltersetD1 RS notE)); |
|
181 |
|
182 Goal "[| X: FreeUltrafilter S; finite x|] ==> x ~: X"; |
|
183 by (blast_tac (claset() addSDs [mem_FreeUltrafilter_not_finite]) 1); |
|
184 qed "mem_FreeUltrafiltersetD2"; |
|
185 |
|
186 Goalw [FreeUltrafilter_def] |
|
187 "[| X: Ultrafilter S; \ |
|
188 \ ALL x. ~(x: X & finite x) |] ==> X: FreeUltrafilter S"; |
|
189 by (Blast_tac 1); |
|
190 qed "mem_FreeUltrafiltersetI1"; |
|
191 |
|
192 Goalw [FreeUltrafilter_def] |
|
193 "[| X: Ultrafilter S; \ |
|
194 \ ALL x. (x ~: X | ~ finite x) |] ==> X: FreeUltrafilter S"; |
|
195 by (Blast_tac 1); |
|
196 qed "mem_FreeUltrafiltersetI2"; |
|
197 |
|
198 Goalw [FreeUltrafilter_def,Freefilter_def,Ultrafilter_def] |
|
199 "(X: FreeUltrafilter S) = (X: Freefilter S & (ALL x:Pow(S). x: X | S - x: X))"; |
|
200 by (Blast_tac 1); |
|
201 qed "FreeUltrafilter_iff"; |
|
202 |
|
203 (*------------------------------------------------------------------- |
|
204 A Filter F on S is an ultrafilter iff it is a maximal filter |
|
205 i.e. whenever G is a filter on I and F <= F then F = G |
|
206 --------------------------------------------------------------------*) |
|
207 (*--------------------------------------------------------------------- |
|
208 lemmas that shows existence of an extension to what was assumed to |
|
209 be a maximal filter. Will be used to derive contradiction in proof of |
|
210 property of ultrafilter |
|
211 ---------------------------------------------------------------------*) |
|
212 Goal "[| F ~= {}; A <= S |] ==> \ |
|
213 \ EX x. x: {X. X <= S & (EX f:F. A Int f <= X)}"; |
|
214 by (Blast_tac 1); |
|
215 qed "lemma_set_extend"; |
|
216 |
|
217 Goal "a: X ==> X ~= {}"; |
|
218 by (Step_tac 1); |
|
219 qed "lemma_set_not_empty"; |
|
220 |
|
221 Goal "x Int F <= {} ==> F <= - x"; |
|
222 by (Blast_tac 1); |
|
223 qed "lemma_empty_Int_subset_Compl"; |
|
224 |
|
225 Goalw [Filter_def,is_Filter_def] |
|
226 "[| F: Filter S; A ~: F; A <= S|] \ |
|
227 \ ==> ALL B. B ~: F | ~ B <= A"; |
|
228 by (Blast_tac 1); |
|
229 qed "mem_Filterset_disjI"; |
|
230 |
|
231 Goal "F : Ultrafilter S ==> \ |
|
232 \ (F: Filter S & (ALL G: Filter S. F <= G --> F = G))"; |
|
233 by (auto_tac (claset(),simpset() addsimps [Ultrafilter_def])); |
|
234 by (dres_inst_tac [("x","x")] bspec 1); |
|
235 by (etac mem_FiltersetD3 1 THEN assume_tac 1); |
|
236 by (Step_tac 1); |
|
237 by (dtac subsetD 1 THEN assume_tac 1); |
|
238 by (blast_tac (claset() addSDs [Filter_Int_not_empty]) 1); |
|
239 qed "Ultrafilter_max_Filter"; |
|
240 |
|
241 |
|
242 (*-------------------------------------------------------------------------------- |
|
243 This is a very long and tedious proof; need to break it into parts. |
|
244 Have proof that {X. X <= S & (EX f: F. A Int f <= X)} is a filter as |
|
245 a lemma |
|
246 --------------------------------------------------------------------------------*) |
|
247 Goalw [Ultrafilter_def] |
|
248 "[| F: Filter S; \ |
|
249 \ ALL G: Filter S. F <= G --> F = G |] ==> F : Ultrafilter S"; |
|
250 by (Step_tac 1); |
|
251 by (rtac ccontr 1); |
|
252 by (forward_tac [mem_FiltersetD RS is_FilterD2] 1); |
|
253 by (forw_inst_tac [("x","{X. X <= S & (EX f: F. A Int f <= X)}")] bspec 1); |
|
254 by (EVERY1[rtac mem_FiltersetI2, Blast_tac, Asm_full_simp_tac]); |
|
255 by (blast_tac (claset() addDs [mem_FiltersetD3]) 1); |
|
256 by (etac (lemma_set_extend RS exE) 1); |
|
257 by (assume_tac 1 THEN etac lemma_set_not_empty 1); |
|
258 by (REPEAT(rtac ballI 2) THEN Asm_full_simp_tac 2); |
|
259 by (rtac conjI 2 THEN Blast_tac 2); |
|
260 by (REPEAT(etac conjE 2) THEN REPEAT(etac bexE 2)); |
|
261 by (res_inst_tac [("x","f Int fa")] bexI 2); |
|
262 by (etac mem_FiltersetD1 3); |
|
263 by (assume_tac 3 THEN assume_tac 3); |
|
264 by (Fast_tac 2); |
|
265 by (EVERY[REPEAT(rtac allI 2), rtac impI 2,Asm_full_simp_tac 2]); |
|
266 by (EVERY[REPEAT(etac conjE 2), etac bexE 2]); |
|
267 by (res_inst_tac [("x","f")] bexI 2); |
|
268 by (rtac subsetI 2); |
|
269 by (Fast_tac 2 THEN assume_tac 2); |
|
270 by (Step_tac 2); |
|
271 by (Blast_tac 3); |
|
272 by (eres_inst_tac [("c","A")] equalityCE 3); |
|
273 by (REPEAT(Blast_tac 3)); |
|
274 by (dres_inst_tac [("A","xa")] mem_FiltersetD3 2 THEN assume_tac 2); |
|
275 by (Blast_tac 2); |
|
276 by (dtac lemma_empty_Int_subset_Compl 1); |
|
277 by (EVERY1[ftac mem_Filterset_disjI , assume_tac, Fast_tac]); |
|
278 by (dtac mem_FiltersetD3 1 THEN assume_tac 1); |
|
279 by (dres_inst_tac [("x","f")] spec 1); |
|
280 by (Blast_tac 1); |
|
281 qed "max_Filter_Ultrafilter"; |
|
282 |
|
283 Goal "(F : Ultrafilter S) = (F: Filter S & (ALL G: Filter S. F <= G --> F = G))"; |
|
284 by (blast_tac (claset() addSIs [Ultrafilter_max_Filter,max_Filter_Ultrafilter]) 1); |
|
285 qed "Ultrafilter_iff"; |
|
286 |
|
287 (*-------------------------------------------------------------------- |
|
288 A few properties of freefilters |
|
289 -------------------------------------------------------------------*) |
|
290 |
|
291 Goal "F1 Int F2 = ((F1 Int Y) Int F2) Un ((F2 Int (- Y)) Int F1)"; |
|
292 by (Auto_tac); |
|
293 qed "lemma_Compl_cancel_eq"; |
|
294 |
|
295 Goal "finite X ==> finite (X Int Y)"; |
|
296 by (etac (Int_lower1 RS finite_subset) 1); |
|
297 qed "finite_IntI1"; |
|
298 |
|
299 Goal "finite Y ==> finite (X Int Y)"; |
|
300 by (etac (Int_lower2 RS finite_subset) 1); |
|
301 qed "finite_IntI2"; |
|
302 |
|
303 Goal "[| finite (F1 Int Y); \ |
|
304 \ finite (F2 Int (- Y)) \ |
|
305 \ |] ==> finite (F1 Int F2)"; |
|
306 by (res_inst_tac [("Y1","Y")] (lemma_Compl_cancel_eq RS ssubst) 1); |
|
307 by (rtac finite_UnI 1); |
|
308 by (auto_tac (claset() addSIs [finite_IntI1,finite_IntI2],simpset())); |
|
309 qed "finite_Int_Compl_cancel"; |
|
310 |
|
311 Goal "U: Freefilter S ==> \ |
|
312 \ ~ (EX f1: U. EX f2: U. finite (f1 Int x) \ |
|
313 \ & finite (f2 Int (- x)))"; |
|
314 by (Step_tac 1); |
|
315 by (forw_inst_tac [("A","f1"),("B","f2")] |
|
316 (Freefilter_Filter RS mem_FiltersetD1) 1); |
|
317 by (dres_inst_tac [("x","f1 Int f2")] mem_FreefiltersetD1 3); |
|
318 by (dtac finite_Int_Compl_cancel 4); |
|
319 by (Auto_tac); |
|
320 qed "Freefilter_lemma_not_finite"; |
|
321 |
|
322 (* the lemmas below follow *) |
|
323 Goal "U: Freefilter S ==> \ |
|
324 \ ALL f: U. ~ finite (f Int x) | ~finite (f Int (- x))"; |
|
325 by (blast_tac (claset() addSDs [Freefilter_lemma_not_finite,bspec]) 1); |
|
326 qed "Freefilter_Compl_not_finite_disjI"; |
|
327 |
|
328 Goal "U: Freefilter S ==> \ |
|
329 \ (ALL f: U. ~ finite (f Int x)) | (ALL f:U. ~finite (f Int (- x)))"; |
|
330 by (blast_tac (claset() addSDs [Freefilter_lemma_not_finite,bspec]) 1); |
|
331 qed "Freefilter_Compl_not_finite_disjI2"; |
|
332 |
|
333 Goal "- UNIV = {}"; |
|
334 by (Auto_tac ); |
|
335 qed "Compl_UNIV_eq"; |
|
336 |
|
337 Addsimps [Compl_UNIV_eq]; |
|
338 |
|
339 Goal "- {} = UNIV"; |
|
340 by (Auto_tac ); |
|
341 qed "Compl_empty_eq"; |
|
342 |
|
343 Addsimps [Compl_empty_eq]; |
|
344 |
|
345 val [prem] = goal (the_context ()) "~ finite (UNIV:: 'a set) ==> \ |
|
346 \ {A:: 'a set. finite (- A)} : Filter UNIV"; |
|
347 by (cut_facts_tac [prem] 1); |
|
348 by (rtac mem_FiltersetI2 1); |
|
349 by (auto_tac (claset(), simpset() delsimps [Collect_empty_eq])); |
|
350 by (eres_inst_tac [("c","UNIV")] equalityCE 1); |
|
351 by (Auto_tac); |
|
352 by (etac (Compl_anti_mono RS finite_subset) 1); |
|
353 by (assume_tac 1); |
|
354 qed "cofinite_Filter"; |
|
355 |
|
356 Goal "~finite(UNIV :: 'a set) ==> ~finite (X :: 'a set) | ~finite (- X)"; |
|
357 by (dres_inst_tac [("A1","X")] (Compl_partition RS ssubst) 1); |
|
358 by (Asm_full_simp_tac 1); |
|
359 qed "not_finite_UNIV_disjI"; |
|
360 |
|
361 Goal "[| ~finite(UNIV :: 'a set); \ |
|
362 \ finite (X :: 'a set) \ |
|
363 \ |] ==> ~finite (- X)"; |
|
364 by (dres_inst_tac [("X","X")] not_finite_UNIV_disjI 1); |
|
365 by (Blast_tac 1); |
|
366 qed "not_finite_UNIV_Compl"; |
|
367 |
|
368 val [prem] = goal (the_context ()) "~ finite (UNIV:: 'a set) ==> \ |
|
369 \ !X: {A:: 'a set. finite (- A)}. ~ finite X"; |
|
370 by (cut_facts_tac [prem] 1); |
|
371 by (auto_tac (claset() addDs [not_finite_UNIV_disjI],simpset())); |
|
372 qed "mem_cofinite_Filter_not_finite"; |
|
373 |
|
374 val [prem] = goal (the_context ()) "~ finite (UNIV:: 'a set) ==> \ |
|
375 \ {A:: 'a set. finite (- A)} : Freefilter UNIV"; |
|
376 by (cut_facts_tac [prem] 1); |
|
377 by (rtac mem_FreefiltersetI2 1); |
|
378 by (rtac cofinite_Filter 1 THEN assume_tac 1); |
|
379 by (blast_tac (claset() addSDs [mem_cofinite_Filter_not_finite]) 1); |
|
380 qed "cofinite_Freefilter"; |
|
381 |
|
382 Goal "UNIV - x = - x"; |
|
383 by (Auto_tac); |
|
384 qed "UNIV_diff_Compl"; |
|
385 Addsimps [UNIV_diff_Compl]; |
|
386 |
|
387 Goalw [Ultrafilter_def,FreeUltrafilter_def] |
|
388 "[| ~finite(UNIV :: 'a set); (U :: 'a set set): FreeUltrafilter UNIV\ |
|
389 \ |] ==> {X. finite(- X)} <= U"; |
|
390 by (ftac cofinite_Filter 1); |
|
391 by (Step_tac 1); |
|
392 by (forw_inst_tac [("X","- x :: 'a set")] not_finite_UNIV_Compl 1); |
|
393 by (assume_tac 1); |
|
394 by (Step_tac 1 THEN Fast_tac 1); |
|
395 by (dres_inst_tac [("x","x")] bspec 1); |
|
396 by (Blast_tac 1); |
|
397 by (asm_full_simp_tac (simpset() addsimps [UNIV_diff_Compl]) 1); |
|
398 qed "FreeUltrafilter_contains_cofinite_set"; |
|
399 |
|
400 (*-------------------------------------------------------------------- |
|
401 We prove: 1. Existence of maximal filter i.e. ultrafilter |
|
402 2. Freeness property i.e ultrafilter is free |
|
403 Use a locale to prove various lemmas and then |
|
404 export main result: The Ultrafilter Theorem |
|
405 -------------------------------------------------------------------*) |
|
406 Open_locale "UFT"; |
|
407 |
|
408 Goalw [chain_def, thm "superfrechet_def", thm "frechet_def"] |
|
409 "!!(c :: 'a set set set). c : chain (superfrechet S) ==> Union c <= Pow S"; |
|
410 by (Step_tac 1); |
|
411 by (dtac subsetD 1 THEN assume_tac 1); |
|
412 by (Step_tac 1); |
|
413 by (dres_inst_tac [("X","X")] mem_FiltersetD3 1); |
|
414 by (Auto_tac); |
|
415 qed "chain_Un_subset_Pow"; |
|
416 |
|
417 Goalw [chain_def,Filter_def,is_Filter_def, |
|
418 thm "superfrechet_def", thm "frechet_def"] |
|
419 "!!(c :: 'a set set set). c: chain (superfrechet S) \ |
|
420 \ ==> !x: c. {} < x"; |
|
421 by (blast_tac (claset() addSIs [psubsetI]) 1); |
|
422 qed "mem_chain_psubset_empty"; |
|
423 |
|
424 Goal "!!(c :: 'a set set set). \ |
|
425 \ [| c: chain (superfrechet S);\ |
|
426 \ c ~= {} \ |
|
427 \ |]\ |
|
428 \ ==> Union(c) ~= {}"; |
|
429 by (dtac mem_chain_psubset_empty 1); |
|
430 by (Step_tac 1); |
|
431 by (dtac bspec 1 THEN assume_tac 1); |
|
432 by (auto_tac (claset() addDs [Union_upper,bspec], |
|
433 simpset() addsimps [psubset_def])); |
|
434 qed "chain_Un_not_empty"; |
|
435 |
|
436 Goalw [is_Filter_def,Filter_def,chain_def,thm "superfrechet_def"] |
|
437 "!!(c :: 'a set set set). \ |
|
438 \ c : chain (superfrechet S) \ |
|
439 \ ==> {} ~: Union(c)"; |
|
440 by (Blast_tac 1); |
|
441 qed "Filter_empty_not_mem_Un"; |
|
442 |
|
443 Goal "c: chain (superfrechet S) \ |
|
444 \ ==> ALL u : Union(c). ALL v: Union(c). u Int v : Union(c)"; |
|
445 by (Step_tac 1); |
|
446 by (forw_inst_tac [("x","X"),("y","Xa")] chainD 1); |
|
447 by (REPEAT(assume_tac 1)); |
|
448 by (dtac chainD2 1); |
|
449 by (etac disjE 1); |
|
450 by (res_inst_tac [("X","Xa")] UnionI 1 THEN assume_tac 1); |
|
451 by (dres_inst_tac [("A","X")] subsetD 1 THEN assume_tac 1); |
|
452 by (dres_inst_tac [("c","Xa")] subsetD 1 THEN assume_tac 1); |
|
453 by (res_inst_tac [("X","X")] UnionI 2 THEN assume_tac 2); |
|
454 by (dres_inst_tac [("A","Xa")] subsetD 2 THEN assume_tac 2); |
|
455 by (dres_inst_tac [("c","X")] subsetD 2 THEN assume_tac 2); |
|
456 by (auto_tac (claset() addIs [mem_FiltersetD1], |
|
457 simpset() addsimps [thm "superfrechet_def"])); |
|
458 qed "Filter_Un_Int"; |
|
459 |
|
460 Goal "c: chain (superfrechet S) \ |
|
461 \ ==> ALL u v. u: Union(c) & \ |
|
462 \ (u :: 'a set) <= v & v <= S --> v: Union(c)"; |
|
463 by (Step_tac 1); |
|
464 by (dtac chainD2 1); |
|
465 by (dtac subsetD 1 THEN assume_tac 1); |
|
466 by (rtac UnionI 1 THEN assume_tac 1); |
|
467 by (auto_tac (claset() addIs [mem_FiltersetD2], |
|
468 simpset() addsimps [thm "superfrechet_def"])); |
|
469 qed "Filter_Un_subset"; |
|
470 |
|
471 Goalw [chain_def,thm "superfrechet_def"] |
|
472 "!!(c :: 'a set set set). \ |
|
473 \ [| c: chain (superfrechet S);\ |
|
474 \ x: c \ |
|
475 \ |] ==> x : Filter S"; |
|
476 by (Blast_tac 1); |
|
477 qed "lemma_mem_chain_Filter"; |
|
478 |
|
479 Goalw [chain_def,thm "superfrechet_def"] |
|
480 "!!(c :: 'a set set set). \ |
|
481 \ [| c: chain (superfrechet S);\ |
|
482 \ x: c \ |
|
483 \ |] ==> frechet S <= x"; |
|
484 by (Blast_tac 1); |
|
485 qed "lemma_mem_chain_frechet_subset"; |
|
486 |
|
487 Goal "!!(c :: 'a set set set). \ |
|
488 \ [| c ~= {}; \ |
|
489 \ c : chain (superfrechet (UNIV :: 'a set))\ |
|
490 \ |] ==> Union c : superfrechet (UNIV)"; |
|
491 by (simp_tac (simpset() addsimps |
|
492 [thm "superfrechet_def",thm "frechet_def"]) 1); |
|
493 by (Step_tac 1); |
|
494 by (rtac mem_FiltersetI2 1); |
|
495 by (etac chain_Un_subset_Pow 1); |
|
496 by (rtac UnionI 1 THEN assume_tac 1); |
|
497 by (etac (lemma_mem_chain_Filter RS mem_FiltersetD4) 1 THEN assume_tac 1); |
|
498 by (etac chain_Un_not_empty 1); |
|
499 by (etac Filter_empty_not_mem_Un 2); |
|
500 by (etac Filter_Un_Int 2); |
|
501 by (etac Filter_Un_subset 2); |
|
502 by (subgoal_tac "xa : frechet (UNIV)" 2); |
|
503 by (rtac UnionI 2 THEN assume_tac 2); |
|
504 by (rtac (lemma_mem_chain_frechet_subset RS subsetD) 2); |
|
505 by (auto_tac (claset(),simpset() addsimps [thm "frechet_def"])); |
|
506 qed "Un_chain_mem_cofinite_Filter_set"; |
|
507 |
|
508 Goal "EX U: superfrechet (UNIV). \ |
|
509 \ ALL G: superfrechet (UNIV). U <= G --> U = G"; |
|
510 by (rtac Zorn_Lemma2 1); |
|
511 by (cut_facts_tac [thm "not_finite_UNIV" RS cofinite_Filter] 1); |
|
512 by (Step_tac 1); |
|
513 by (res_inst_tac [("Q","c={}")] (excluded_middle RS disjE) 1); |
|
514 by (res_inst_tac [("x","Union c")] bexI 1 THEN Blast_tac 1); |
|
515 by (rtac Un_chain_mem_cofinite_Filter_set 1 THEN REPEAT(assume_tac 1)); |
|
516 by (res_inst_tac [("x","frechet (UNIV)")] bexI 1 THEN Blast_tac 1); |
|
517 by (auto_tac (claset(), |
|
518 simpset() addsimps |
|
519 [thm "superfrechet_def", thm "frechet_def"])); |
|
520 qed "max_cofinite_Filter_Ex"; |
|
521 |
|
522 Goal "EX U: superfrechet UNIV. (\ |
|
523 \ ALL G: superfrechet UNIV. U <= G --> U = G) \ |
|
524 \ & (ALL x: U. ~finite x)"; |
|
525 by (cut_facts_tac [thm "not_finite_UNIV" RS |
|
526 (export max_cofinite_Filter_Ex)] 1); |
|
527 by (Step_tac 1); |
|
528 by (res_inst_tac [("x","U")] bexI 1); |
|
529 by (auto_tac (claset(),simpset() addsimps |
|
530 [thm "superfrechet_def", thm "frechet_def"])); |
|
531 by (dres_inst_tac [("c","- x")] subsetD 1); |
|
532 by (Asm_simp_tac 1); |
|
533 by (forw_inst_tac [("A","x"),("B","- x")] mem_FiltersetD1 1); |
|
534 by (dtac Filter_empty_not_mem 3); |
|
535 by (ALLGOALS(Asm_full_simp_tac )); |
|
536 qed "max_cofinite_Freefilter_Ex"; |
|
537 |
|
538 (*-------------------------------------------------------------------------------- |
|
539 There exists a free ultrafilter on any infinite set |
|
540 --------------------------------------------------------------------------------*) |
|
541 |
|
542 Goalw [FreeUltrafilter_def] "EX U. U: FreeUltrafilter (UNIV :: 'a set)"; |
|
543 by (cut_facts_tac [thm "not_finite_UNIV" RS (export max_cofinite_Freefilter_Ex)] 1); |
|
544 by (asm_full_simp_tac (simpset() addsimps |
|
545 [thm "superfrechet_def", Ultrafilter_iff, thm "frechet_def"]) 1); |
|
546 by (Step_tac 1); |
|
547 by (res_inst_tac [("x","U")] exI 1); |
|
548 by (Step_tac 1); |
|
549 by (Blast_tac 1); |
|
550 qed "FreeUltrafilter_ex"; |
|
551 |
|
552 bind_thm ("FreeUltrafilter_Ex", export FreeUltrafilter_ex); |
|
553 |
|
554 Close_locale "UFT"; |