author | huffman |
Tue, 06 Sep 2005 19:22:31 +0200 | |
changeset 17290 | a39d1430d271 |
parent 15140 | 322485b816ac |
child 17332 | 4910cf8c0cd2 |
permissions | -rw-r--r-- |
10750 | 1 |
(* Title : Filter.thy |
2 |
ID : $Id$ |
|
3 |
Author : Jacques D. Fleuriot |
|
4 |
Copyright : 1998 University of Cambridge |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
5 |
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
17290 | 6 |
Conversion to locales by Brian Huffman, 2005 |
10750 | 7 |
*) |
8 |
||
17290 | 9 |
header {* Filters and Ultrafilters *} |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
10 |
|
15131 | 11 |
theory Filter |
15140 | 12 |
imports Zorn |
15131 | 13 |
begin |
10750 | 14 |
|
17290 | 15 |
subsection {* Definitions and basic properties *} |
10750 | 16 |
|
17290 | 17 |
subsubsection {* Filters *} |
10750 | 18 |
|
17290 | 19 |
locale filter = |
20 |
fixes F :: "'a set set" |
|
21 |
assumes UNIV [iff]: "UNIV \<in> F" |
|
22 |
assumes empty [iff]: "{} \<notin> F" |
|
23 |
assumes Int: "\<lbrakk>u \<in> F; v \<in> F\<rbrakk> \<Longrightarrow> u \<inter> v \<in> F" |
|
24 |
assumes subset: "\<lbrakk>u \<in> F; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> F" |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
25 |
|
17290 | 26 |
lemma (in filter) memD: "A \<in> F \<Longrightarrow> - A \<notin> F" |
27 |
proof |
|
28 |
assume "A \<in> F" and "- A \<in> F" |
|
29 |
hence "A \<inter> (- A) \<in> F" by (rule Int) |
|
30 |
thus "False" by simp |
|
31 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
32 |
|
17290 | 33 |
lemma (in filter) not_memI: "- A \<in> F \<Longrightarrow> A \<notin> F" |
34 |
by (drule memD, simp) |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
35 |
|
17290 | 36 |
lemma (in filter) Int_iff: "(x \<inter> y \<in> F) = (x \<in> F \<and> y \<in> F)" |
37 |
by (auto elim: subset intro: Int) |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
38 |
|
17290 | 39 |
subsubsection {* Ultrafilters *} |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
40 |
|
17290 | 41 |
locale ultrafilter = filter + |
42 |
assumes ultra: "A \<in> F \<or> - A \<in> F" |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
43 |
|
17290 | 44 |
lemma (in ultrafilter) memI: "- A \<notin> F \<Longrightarrow> A \<in> F" |
45 |
by (cut_tac ultra [of A], simp) |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
46 |
|
17290 | 47 |
lemma (in ultrafilter) not_memD: "A \<notin> F \<Longrightarrow> - A \<in> F" |
48 |
by (rule memI, simp) |
|
49 |
||
50 |
lemma (in ultrafilter) not_mem_iff: "(A \<notin> F) = (- A \<in> F)" |
|
51 |
by (rule iffI [OF not_memD not_memI]) |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
52 |
|
17290 | 53 |
lemma (in ultrafilter) Compl_iff: "(- A \<in> F) = (A \<notin> F)" |
54 |
by (rule iffI [OF not_memI not_memD]) |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
55 |
|
17290 | 56 |
lemma (in ultrafilter) Un_iff: "(x \<union> y \<in> F) = (x \<in> F \<or> y \<in> F)" |
57 |
apply (rule iffI) |
|
58 |
apply (erule contrapos_pp) |
|
59 |
apply (simp add: Int_iff not_mem_iff) |
|
60 |
apply (auto elim: subset) |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
61 |
done |
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
62 |
|
17290 | 63 |
subsubsection {* Free ultrafilters *} |
64 |
||
65 |
locale freeultrafilter = ultrafilter + |
|
66 |
assumes infinite: "A \<in> F \<Longrightarrow> infinite A" |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
67 |
|
17290 | 68 |
lemma (in freeultrafilter) finite: "finite A \<Longrightarrow> A \<notin> F" |
69 |
by (erule contrapos_pn, erule infinite) |
|
70 |
||
71 |
lemma (in freeultrafilter) filter: "filter F" . |
|
72 |
||
73 |
lemma (in freeultrafilter) ultrafilter: "ultrafilter F" |
|
74 |
by (rule ultrafilter.intro) |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
75 |
|
17290 | 76 |
subsection {* Maximal filter = ultrafilter *} |
10750 | 77 |
|
17290 | 78 |
text {* |
79 |
A filter F is an ultrafilter iff it is a maximal filter, |
|
80 |
i.e. whenever G is a filter and @{term "F \<subseteq> G"} then @{term "F = G"} |
|
81 |
*} |
|
82 |
text {* |
|
83 |
Lemmas that shows existence of an extension to what was assumed to |
|
84 |
be a maximal filter. Will be used to derive contradiction in proof of |
|
85 |
property of ultrafilter. |
|
86 |
*} |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
87 |
|
17290 | 88 |
lemma extend_lemma1: "UNIV \<in> F \<Longrightarrow> A \<in> {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}" |
89 |
by blast |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
90 |
|
17290 | 91 |
lemma extend_lemma2: "F \<subseteq> {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}" |
92 |
by blast |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
93 |
|
17290 | 94 |
lemma (in filter) extend_filter: |
95 |
assumes A: "- A \<notin> F" |
|
96 |
shows "filter {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}" (is "filter ?X") |
|
97 |
proof (rule filter.intro) |
|
98 |
show "UNIV \<in> ?X" by blast |
|
99 |
next |
|
100 |
show "{} \<notin> ?X" |
|
101 |
proof (clarify) |
|
102 |
fix f assume f: "f \<in> F" and Af: "A \<inter> f \<subseteq> {}" |
|
103 |
from Af have fA: "f \<subseteq> - A" by blast |
|
104 |
from f fA have "- A \<in> F" by (rule subset) |
|
105 |
with A show "False" by simp |
|
106 |
qed |
|
107 |
next |
|
108 |
fix u and v |
|
109 |
assume u: "u \<in> ?X" and v: "v \<in> ?X" |
|
110 |
from u obtain f where f: "f \<in> F" and Af: "A \<inter> f \<subseteq> u" by blast |
|
111 |
from v obtain g where g: "g \<in> F" and Ag: "A \<inter> g \<subseteq> v" by blast |
|
112 |
from f g have fg: "f \<inter> g \<in> F" by (rule Int) |
|
113 |
from Af Ag have Afg: "A \<inter> (f \<inter> g) \<subseteq> u \<inter> v" by blast |
|
114 |
from fg Afg show "u \<inter> v \<in> ?X" by blast |
|
115 |
next |
|
116 |
fix u and v |
|
117 |
assume uv: "u \<subseteq> v" and u: "u \<in> ?X" |
|
118 |
from u obtain f where f: "f \<in> F" and Afu: "A \<inter> f \<subseteq> u" by blast |
|
119 |
from Afu uv have Afv: "A \<inter> f \<subseteq> v" by blast |
|
120 |
from f Afv have "\<exists>f\<in>F. A \<inter> f \<subseteq> v" by blast |
|
121 |
thus "v \<in> ?X" by simp |
|
122 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
123 |
|
17290 | 124 |
lemma (in filter) max_filter_ultrafilter: |
125 |
assumes max: "\<And>G. \<lbrakk>filter G; F \<subseteq> G\<rbrakk> \<Longrightarrow> F = G" |
|
126 |
shows "ultrafilter_axioms F" |
|
127 |
proof (rule ultrafilter_axioms.intro) |
|
128 |
fix A show "A \<in> F \<or> - A \<in> F" |
|
129 |
proof (rule disjCI) |
|
130 |
let ?X = "{X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}" |
|
131 |
assume AF: "- A \<notin> F" |
|
132 |
from AF have X: "filter ?X" by (rule extend_filter) |
|
133 |
from UNIV have AX: "A \<in> ?X" by (rule extend_lemma1) |
|
134 |
have FX: "F \<subseteq> ?X" by (rule extend_lemma2) |
|
135 |
from X FX have "F = ?X" by (rule max) |
|
136 |
with AX show "A \<in> F" by simp |
|
137 |
qed |
|
138 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
139 |
|
17290 | 140 |
lemma (in ultrafilter) max_filter: |
141 |
assumes G: "filter G" and sub: "F \<subseteq> G" shows "F = G" |
|
142 |
proof |
|
143 |
show "F \<subseteq> G" . |
|
144 |
show "G \<subseteq> F" |
|
145 |
proof |
|
146 |
fix A assume A: "A \<in> G" |
|
147 |
from G A have "- A \<notin> G" by (rule filter.memD) |
|
148 |
with sub have B: "- A \<notin> F" by blast |
|
149 |
thus "A \<in> F" by (rule memI) |
|
150 |
qed |
|
151 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
152 |
|
17290 | 153 |
subsection {* ultrafilter Theorem *} |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
154 |
|
17290 | 155 |
text "A locale makes proof of ultrafilter Theorem more modular" |
156 |
locale (open) UFT = |
|
157 |
fixes frechet :: "'a set set" |
|
158 |
and superfrechet :: "'a set set set" |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
159 |
|
17290 | 160 |
assumes infinite_UNIV: "infinite (UNIV :: 'a set)" |
161 |
||
162 |
defines frechet_def: "frechet \<equiv> {A. finite (- A)}" |
|
163 |
and superfrechet_def: "superfrechet \<equiv> {G. filter G \<and> frechet \<subseteq> G}" |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
164 |
|
17290 | 165 |
lemma (in UFT) superfrechetI: |
166 |
"\<lbrakk>filter G; frechet \<subseteq> G\<rbrakk> \<Longrightarrow> G \<in> superfrechet" |
|
167 |
by (simp add: superfrechet_def) |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
168 |
|
17290 | 169 |
lemma (in UFT) superfrechetD1: |
170 |
"G \<in> superfrechet \<Longrightarrow> filter G" |
|
171 |
by (simp add: superfrechet_def) |
|
172 |
||
173 |
lemma (in UFT) superfrechetD2: |
|
174 |
"G \<in> superfrechet \<Longrightarrow> frechet \<subseteq> G" |
|
175 |
by (simp add: superfrechet_def) |
|
176 |
||
177 |
text {* A few properties of free filters *} |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
178 |
|
17290 | 179 |
lemma filter_cofinite: |
180 |
assumes inf: "infinite (UNIV :: 'a set)" |
|
181 |
shows "filter {A:: 'a set. finite (- A)}" (is "filter ?F") |
|
182 |
proof (rule filter.intro) |
|
183 |
show "UNIV \<in> ?F" by simp |
|
184 |
next |
|
185 |
show "{} \<notin> ?F" by simp |
|
186 |
next |
|
187 |
fix u v assume "u \<in> ?F" and "v \<in> ?F" |
|
188 |
thus "u \<inter> v \<in> ?F" by simp |
|
189 |
next |
|
190 |
fix u v assume uv: "u \<subseteq> v" and u: "u \<in> ?F" |
|
191 |
from uv have vu: "- v \<subseteq> - u" by simp |
|
192 |
from u show "v \<in> ?F" |
|
193 |
by (simp add: finite_subset [OF vu]) |
|
194 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
195 |
|
17290 | 196 |
text {* |
197 |
We prove: 1. Existence of maximal filter i.e. ultrafilter; |
|
198 |
2. Freeness property i.e ultrafilter is free. |
|
199 |
Use a locale to prove various lemmas and then |
|
200 |
export main result: The ultrafilter Theorem |
|
201 |
*} |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
202 |
|
17290 | 203 |
lemma (in UFT) filter_frechet: "filter frechet" |
204 |
by (unfold frechet_def, rule filter_cofinite [OF infinite_UNIV]) |
|
205 |
||
206 |
lemma (in UFT) frechet_in_superfrechet: "frechet \<in> superfrechet" |
|
207 |
by (rule superfrechetI [OF filter_frechet subset_refl]) |
|
208 |
||
209 |
lemma (in UFT) lemma_mem_chain_filter: |
|
210 |
"\<lbrakk>c \<in> chain superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> filter x" |
|
211 |
by (unfold chain_def superfrechet_def, blast) |
|
10750 | 212 |
|
213 |
||
17290 | 214 |
subsubsection {* Unions of chains of superfrechets *} |
215 |
||
216 |
text "In this section we prove that superfrechet is closed |
|
217 |
with respect to unions of non-empty chains. We must show |
|
218 |
1) Union of a chain is a filter, |
|
219 |
2) Union of a chain contains frechet. |
|
220 |
||
221 |
Number 2 is trivial, but 1 requires us to prove all the filter rules." |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
222 |
|
17290 | 223 |
lemma (in UFT) Union_chain_UNIV: |
224 |
"\<lbrakk>c \<in> chain superfrechet; c \<noteq> {}\<rbrakk> \<Longrightarrow> UNIV \<in> \<Union>c" |
|
225 |
proof - |
|
226 |
assume 1: "c \<in> chain superfrechet" and 2: "c \<noteq> {}" |
|
227 |
from 2 obtain x where 3: "x \<in> c" by blast |
|
228 |
from 1 3 have "filter x" by (rule lemma_mem_chain_filter) |
|
229 |
hence "UNIV \<in> x" by (rule filter.UNIV) |
|
230 |
with 3 show "UNIV \<in> \<Union>c" by blast |
|
231 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
232 |
|
17290 | 233 |
lemma (in UFT) Union_chain_empty: |
234 |
"c \<in> chain superfrechet \<Longrightarrow> {} \<notin> \<Union>c" |
|
235 |
proof |
|
236 |
assume 1: "c \<in> chain superfrechet" and 2: "{} \<in> \<Union>c" |
|
237 |
from 2 obtain x where 3: "x \<in> c" and 4: "{} \<in> x" .. |
|
238 |
from 1 3 have "filter x" by (rule lemma_mem_chain_filter) |
|
239 |
hence "{} \<notin> x" by (rule filter.empty) |
|
240 |
with 4 show "False" by simp |
|
241 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
242 |
|
17290 | 243 |
lemma (in UFT) Union_chain_Int: |
244 |
"\<lbrakk>c \<in> chain superfrechet; u \<in> \<Union>c; v \<in> \<Union>c\<rbrakk> \<Longrightarrow> u \<inter> v \<in> \<Union>c" |
|
245 |
proof - |
|
246 |
assume c: "c \<in> chain superfrechet" |
|
247 |
assume "u \<in> \<Union>c" |
|
248 |
then obtain x where ux: "u \<in> x" and xc: "x \<in> c" .. |
|
249 |
assume "v \<in> \<Union>c" |
|
250 |
then obtain y where vy: "v \<in> y" and yc: "y \<in> c" .. |
|
251 |
from c xc yc have "x \<subseteq> y \<or> y \<subseteq> x" by (rule chainD) |
|
252 |
with xc yc have xyc: "x \<union> y \<in> c" |
|
253 |
by (auto simp add: Un_absorb1 Un_absorb2) |
|
254 |
with c have fxy: "filter (x \<union> y)" by (rule lemma_mem_chain_filter) |
|
255 |
from ux have uxy: "u \<in> x \<union> y" by simp |
|
256 |
from vy have vxy: "v \<in> x \<union> y" by simp |
|
257 |
from fxy uxy vxy have "u \<inter> v \<in> x \<union> y" by (rule filter.Int) |
|
258 |
with xyc show "u \<inter> v \<in> \<Union>c" .. |
|
259 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
260 |
|
17290 | 261 |
lemma (in UFT) Union_chain_subset: |
262 |
"\<lbrakk>c \<in> chain superfrechet; u \<in> \<Union>c; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> \<Union>c" |
|
263 |
proof - |
|
264 |
assume c: "c \<in> chain superfrechet" |
|
265 |
and u: "u \<in> \<Union>c" and uv: "u \<subseteq> v" |
|
266 |
from u obtain x where ux: "u \<in> x" and xc: "x \<in> c" .. |
|
267 |
from c xc have fx: "filter x" by (rule lemma_mem_chain_filter) |
|
268 |
from fx ux uv have vx: "v \<in> x" by (rule filter.subset) |
|
269 |
with xc show "v \<in> \<Union>c" .. |
|
270 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
271 |
|
17290 | 272 |
lemma (in UFT) Union_chain_filter: |
273 |
assumes "c \<in> chain superfrechet" and "c \<noteq> {}" |
|
274 |
shows "filter (\<Union>c)" |
|
275 |
proof (rule filter.intro) |
|
276 |
show "UNIV \<in> \<Union>c" by (rule Union_chain_UNIV) |
|
277 |
next |
|
278 |
show "{} \<notin> \<Union>c" by (rule Union_chain_empty) |
|
279 |
next |
|
280 |
fix u v assume "u \<in> \<Union>c" and "v \<in> \<Union>c" |
|
281 |
show "u \<inter> v \<in> \<Union>c" by (rule Union_chain_Int) |
|
282 |
next |
|
283 |
fix u v assume "u \<in> \<Union>c" and "u \<subseteq> v" |
|
284 |
show "v \<in> \<Union>c" by (rule Union_chain_subset) |
|
285 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
286 |
|
17290 | 287 |
lemma (in UFT) lemma_mem_chain_frechet_subset: |
288 |
"\<lbrakk>c \<in> chain superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> frechet \<subseteq> x" |
|
289 |
by (unfold superfrechet_def chain_def, blast) |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
290 |
|
17290 | 291 |
lemma (in UFT) Union_chain_superfrechet: |
292 |
"\<lbrakk>c \<noteq> {}; c \<in> chain superfrechet\<rbrakk> \<Longrightarrow> \<Union>c \<in> superfrechet" |
|
293 |
proof (rule superfrechetI) |
|
294 |
assume 1: "c \<in> chain superfrechet" and 2: "c \<noteq> {}" |
|
295 |
thus "filter (\<Union>c)" by (rule Union_chain_filter) |
|
296 |
from 2 obtain x where 3: "x \<in> c" by blast |
|
297 |
from 1 3 have "frechet \<subseteq> x" by (rule lemma_mem_chain_frechet_subset) |
|
298 |
also from 3 have "x \<subseteq> \<Union>c" by blast |
|
299 |
finally show "frechet \<subseteq> \<Union>c" . |
|
300 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
301 |
|
17290 | 302 |
subsubsection {* Existence of free ultrafilter *} |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
303 |
|
17290 | 304 |
lemma (in UFT) max_cofinite_filter_Ex: |
305 |
"\<exists>U\<in>superfrechet. \<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> U = G" |
|
306 |
proof (rule Zorn_Lemma2 [rule_format]) |
|
307 |
fix c assume c: "c \<in> chain superfrechet" |
|
308 |
show "\<exists>U\<in>superfrechet. \<forall>G\<in>c. G \<subseteq> U" (is "?U") |
|
309 |
proof (cases) |
|
310 |
assume "c = {}" |
|
311 |
with frechet_in_superfrechet show "?U" by blast |
|
312 |
next |
|
313 |
assume A: "c \<noteq> {}" |
|
314 |
from A c have "\<Union>c \<in> superfrechet" |
|
315 |
by (rule Union_chain_superfrechet) |
|
316 |
thus "?U" by blast |
|
317 |
qed |
|
318 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
319 |
|
17290 | 320 |
lemma (in UFT) mem_superfrechet_all_infinite: |
321 |
"\<lbrakk>U \<in> superfrechet; A \<in> U\<rbrakk> \<Longrightarrow> infinite A" |
|
322 |
proof |
|
323 |
assume U: "U \<in> superfrechet" and A: "A \<in> U" and fin: "finite A" |
|
324 |
from U have fil: "filter U" and fre: "frechet \<subseteq> U" |
|
325 |
by (simp_all add: superfrechet_def) |
|
326 |
from fin have "- A \<in> frechet" by (simp add: frechet_def) |
|
327 |
with fre have cA: "- A \<in> U" by (rule subsetD) |
|
328 |
from fil A cA have "A \<inter> - A \<in> U" by (rule filter.Int) |
|
329 |
with fil show "False" by (simp add: filter.empty) |
|
330 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
331 |
|
17290 | 332 |
text {* There exists a free ultrafilter on any infinite set *} |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
333 |
|
17290 | 334 |
lemma (in UFT) freeultrafilter_ex: |
335 |
"\<exists>U::'a set set. freeultrafilter U" |
|
336 |
proof - |
|
337 |
from max_cofinite_filter_Ex obtain U |
|
338 |
where U: "U \<in> superfrechet" |
|
339 |
and max [rule_format]: "\<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> U = G" .. |
|
340 |
from U have fil: "filter U" by (rule superfrechetD1) |
|
341 |
from U have fre: "frechet \<subseteq> U" by (rule superfrechetD2) |
|
342 |
have ultra: "ultrafilter_axioms U" |
|
343 |
proof (rule filter.max_filter_ultrafilter [OF fil]) |
|
344 |
fix G assume G: "filter G" and UG: "U \<subseteq> G" |
|
345 |
from fre UG have "frechet \<subseteq> G" by simp |
|
346 |
with G have "G \<in> superfrechet" by (rule superfrechetI) |
|
347 |
from this UG show "U = G" by (rule max) |
|
348 |
qed |
|
349 |
have free: "freeultrafilter_axioms U" |
|
350 |
proof (rule freeultrafilter_axioms.intro) |
|
351 |
fix A assume "A \<in> U" |
|
352 |
with U show "infinite A" by (rule mem_superfrechet_all_infinite) |
|
353 |
qed |
|
354 |
from fil ultra free have "freeultrafilter U" |
|
355 |
by (rule freeultrafilter.intro) |
|
356 |
thus ?thesis .. |
|
357 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
358 |
|
17290 | 359 |
lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
360 |
|
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
361 |
end |