author | haftmann |
Fri, 16 Mar 2007 21:32:10 +0100 | |
changeset 22454 | c3654ba76a09 |
parent 21854 | 42e9fd3ec1a3 |
child 23280 | 4e61c67a87e3 |
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 |
20809 | 12 |
imports Zorn Infinite_Set |
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 |
|
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
63 |
subsubsection {* Free Ultrafilters *} |
17290 | 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 |
||
21849 | 71 |
lemma (in freeultrafilter) singleton: "{x} \<notin> F" |
72 |
by (rule finite, simp) |
|
73 |
||
21854 | 74 |
lemma (in freeultrafilter) insert_iff [simp]: "(insert x A \<in> F) = (A \<in> F)" |
21849 | 75 |
apply (subst insert_is_Un) |
76 |
apply (subst Un_iff) |
|
77 |
apply (simp add: singleton) |
|
78 |
done |
|
79 |
||
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset
|
80 |
lemma (in freeultrafilter) filter: "filter F" by unfold_locales |
17290 | 81 |
|
82 |
lemma (in freeultrafilter) ultrafilter: "ultrafilter F" |
|
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset
|
83 |
by unfold_locales |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
17332
diff
changeset
|
84 |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
85 |
|
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
86 |
subsection {* Collect properties *} |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
87 |
|
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
88 |
lemma (in filter) Collect_ex: |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
89 |
"({n. \<exists>x. P n x} \<in> F) = (\<exists>X. {n. P n (X n)} \<in> F)" |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
90 |
proof |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
91 |
assume "{n. \<exists>x. P n x} \<in> F" |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
92 |
hence "{n. P n (SOME x. P n x)} \<in> F" |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
93 |
by (auto elim: someI subset) |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
94 |
thus "\<exists>X. {n. P n (X n)} \<in> F" by fast |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
95 |
next |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
96 |
show "\<exists>X. {n. P n (X n)} \<in> F \<Longrightarrow> {n. \<exists>x. P n x} \<in> F" |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
97 |
by (auto elim: subset) |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
98 |
qed |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
99 |
|
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
100 |
lemma (in filter) Collect_conj: |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
101 |
"({n. P n \<and> Q n} \<in> F) = ({n. P n} \<in> F \<and> {n. Q n} \<in> F)" |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
102 |
by (subst Collect_conj_eq, rule Int_iff) |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
103 |
|
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
104 |
lemma (in ultrafilter) Collect_not: |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
105 |
"({n. \<not> P n} \<in> F) = ({n. P n} \<notin> F)" |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
106 |
by (subst Collect_neg_eq, rule Compl_iff) |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
107 |
|
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
108 |
lemma (in ultrafilter) Collect_disj: |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
109 |
"({n. P n \<or> Q n} \<in> F) = ({n. P n} \<in> F \<or> {n. Q n} \<in> F)" |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
110 |
by (subst Collect_disj_eq, rule Un_iff) |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
111 |
|
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
112 |
lemma (in ultrafilter) Collect_all: |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
113 |
"({n. \<forall>x. P n x} \<in> F) = (\<forall>X. {n. P n (X n)} \<in> F)" |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
114 |
apply (rule Not_eq_iff [THEN iffD1]) |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
115 |
apply (simp add: Collect_not [symmetric]) |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
116 |
apply (rule Collect_ex) |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
117 |
done |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
118 |
|
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
119 |
subsection {* Maximal filter = Ultrafilter *} |
10750 | 120 |
|
17290 | 121 |
text {* |
122 |
A filter F is an ultrafilter iff it is a maximal filter, |
|
123 |
i.e. whenever G is a filter and @{term "F \<subseteq> G"} then @{term "F = G"} |
|
124 |
*} |
|
125 |
text {* |
|
126 |
Lemmas that shows existence of an extension to what was assumed to |
|
127 |
be a maximal filter. Will be used to derive contradiction in proof of |
|
128 |
property of ultrafilter. |
|
129 |
*} |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
130 |
|
17290 | 131 |
lemma extend_lemma1: "UNIV \<in> F \<Longrightarrow> A \<in> {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}" |
132 |
by blast |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
133 |
|
17290 | 134 |
lemma extend_lemma2: "F \<subseteq> {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}" |
135 |
by blast |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
136 |
|
17290 | 137 |
lemma (in filter) extend_filter: |
138 |
assumes A: "- A \<notin> F" |
|
139 |
shows "filter {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}" (is "filter ?X") |
|
140 |
proof (rule filter.intro) |
|
141 |
show "UNIV \<in> ?X" by blast |
|
142 |
next |
|
143 |
show "{} \<notin> ?X" |
|
144 |
proof (clarify) |
|
145 |
fix f assume f: "f \<in> F" and Af: "A \<inter> f \<subseteq> {}" |
|
146 |
from Af have fA: "f \<subseteq> - A" by blast |
|
147 |
from f fA have "- A \<in> F" by (rule subset) |
|
148 |
with A show "False" by simp |
|
149 |
qed |
|
150 |
next |
|
151 |
fix u and v |
|
152 |
assume u: "u \<in> ?X" and v: "v \<in> ?X" |
|
153 |
from u obtain f where f: "f \<in> F" and Af: "A \<inter> f \<subseteq> u" by blast |
|
154 |
from v obtain g where g: "g \<in> F" and Ag: "A \<inter> g \<subseteq> v" by blast |
|
155 |
from f g have fg: "f \<inter> g \<in> F" by (rule Int) |
|
156 |
from Af Ag have Afg: "A \<inter> (f \<inter> g) \<subseteq> u \<inter> v" by blast |
|
157 |
from fg Afg show "u \<inter> v \<in> ?X" by blast |
|
158 |
next |
|
159 |
fix u and v |
|
160 |
assume uv: "u \<subseteq> v" and u: "u \<in> ?X" |
|
161 |
from u obtain f where f: "f \<in> F" and Afu: "A \<inter> f \<subseteq> u" by blast |
|
162 |
from Afu uv have Afv: "A \<inter> f \<subseteq> v" by blast |
|
163 |
from f Afv have "\<exists>f\<in>F. A \<inter> f \<subseteq> v" by blast |
|
164 |
thus "v \<in> ?X" by simp |
|
165 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
166 |
|
17290 | 167 |
lemma (in filter) max_filter_ultrafilter: |
168 |
assumes max: "\<And>G. \<lbrakk>filter G; F \<subseteq> G\<rbrakk> \<Longrightarrow> F = G" |
|
169 |
shows "ultrafilter_axioms F" |
|
170 |
proof (rule ultrafilter_axioms.intro) |
|
171 |
fix A show "A \<in> F \<or> - A \<in> F" |
|
172 |
proof (rule disjCI) |
|
173 |
let ?X = "{X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}" |
|
174 |
assume AF: "- A \<notin> F" |
|
175 |
from AF have X: "filter ?X" by (rule extend_filter) |
|
176 |
from UNIV have AX: "A \<in> ?X" by (rule extend_lemma1) |
|
177 |
have FX: "F \<subseteq> ?X" by (rule extend_lemma2) |
|
178 |
from X FX have "F = ?X" by (rule max) |
|
179 |
with AX show "A \<in> F" by simp |
|
180 |
qed |
|
181 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
182 |
|
17290 | 183 |
lemma (in ultrafilter) max_filter: |
184 |
assumes G: "filter G" and sub: "F \<subseteq> G" shows "F = G" |
|
185 |
proof |
|
186 |
show "F \<subseteq> G" . |
|
187 |
show "G \<subseteq> F" |
|
188 |
proof |
|
189 |
fix A assume A: "A \<in> G" |
|
190 |
from G A have "- A \<notin> G" by (rule filter.memD) |
|
191 |
with sub have B: "- A \<notin> F" by blast |
|
192 |
thus "A \<in> F" by (rule memI) |
|
193 |
qed |
|
194 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
195 |
|
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17290
diff
changeset
|
196 |
subsection {* Ultrafilter Theorem *} |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
197 |
|
17290 | 198 |
text "A locale makes proof of ultrafilter Theorem more modular" |
199 |
locale (open) UFT = |
|
200 |
fixes frechet :: "'a set set" |
|
201 |
and superfrechet :: "'a set set set" |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
202 |
|
17290 | 203 |
assumes infinite_UNIV: "infinite (UNIV :: 'a set)" |
204 |
||
205 |
defines frechet_def: "frechet \<equiv> {A. finite (- A)}" |
|
206 |
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
|
207 |
|
17290 | 208 |
lemma (in UFT) superfrechetI: |
209 |
"\<lbrakk>filter G; frechet \<subseteq> G\<rbrakk> \<Longrightarrow> G \<in> superfrechet" |
|
210 |
by (simp add: superfrechet_def) |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
211 |
|
17290 | 212 |
lemma (in UFT) superfrechetD1: |
213 |
"G \<in> superfrechet \<Longrightarrow> filter G" |
|
214 |
by (simp add: superfrechet_def) |
|
215 |
||
216 |
lemma (in UFT) superfrechetD2: |
|
217 |
"G \<in> superfrechet \<Longrightarrow> frechet \<subseteq> G" |
|
218 |
by (simp add: superfrechet_def) |
|
219 |
||
220 |
text {* A few properties of free filters *} |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
221 |
|
17290 | 222 |
lemma filter_cofinite: |
223 |
assumes inf: "infinite (UNIV :: 'a set)" |
|
224 |
shows "filter {A:: 'a set. finite (- A)}" (is "filter ?F") |
|
225 |
proof (rule filter.intro) |
|
226 |
show "UNIV \<in> ?F" by simp |
|
227 |
next |
|
228 |
show "{} \<notin> ?F" by simp |
|
229 |
next |
|
230 |
fix u v assume "u \<in> ?F" and "v \<in> ?F" |
|
231 |
thus "u \<inter> v \<in> ?F" by simp |
|
232 |
next |
|
233 |
fix u v assume uv: "u \<subseteq> v" and u: "u \<in> ?F" |
|
234 |
from uv have vu: "- v \<subseteq> - u" by simp |
|
235 |
from u show "v \<in> ?F" |
|
236 |
by (simp add: finite_subset [OF vu]) |
|
237 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
238 |
|
17290 | 239 |
text {* |
240 |
We prove: 1. Existence of maximal filter i.e. ultrafilter; |
|
241 |
2. Freeness property i.e ultrafilter is free. |
|
242 |
Use a locale to prove various lemmas and then |
|
243 |
export main result: The ultrafilter Theorem |
|
244 |
*} |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
245 |
|
17290 | 246 |
lemma (in UFT) filter_frechet: "filter frechet" |
247 |
by (unfold frechet_def, rule filter_cofinite [OF infinite_UNIV]) |
|
248 |
||
249 |
lemma (in UFT) frechet_in_superfrechet: "frechet \<in> superfrechet" |
|
250 |
by (rule superfrechetI [OF filter_frechet subset_refl]) |
|
251 |
||
252 |
lemma (in UFT) lemma_mem_chain_filter: |
|
253 |
"\<lbrakk>c \<in> chain superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> filter x" |
|
254 |
by (unfold chain_def superfrechet_def, blast) |
|
10750 | 255 |
|
256 |
||
17290 | 257 |
subsubsection {* Unions of chains of superfrechets *} |
258 |
||
259 |
text "In this section we prove that superfrechet is closed |
|
260 |
with respect to unions of non-empty chains. We must show |
|
261 |
1) Union of a chain is a filter, |
|
262 |
2) Union of a chain contains frechet. |
|
263 |
||
264 |
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
|
265 |
|
17290 | 266 |
lemma (in UFT) Union_chain_UNIV: |
267 |
"\<lbrakk>c \<in> chain superfrechet; c \<noteq> {}\<rbrakk> \<Longrightarrow> UNIV \<in> \<Union>c" |
|
268 |
proof - |
|
269 |
assume 1: "c \<in> chain superfrechet" and 2: "c \<noteq> {}" |
|
270 |
from 2 obtain x where 3: "x \<in> c" by blast |
|
271 |
from 1 3 have "filter x" by (rule lemma_mem_chain_filter) |
|
272 |
hence "UNIV \<in> x" by (rule filter.UNIV) |
|
273 |
with 3 show "UNIV \<in> \<Union>c" by blast |
|
274 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
275 |
|
17290 | 276 |
lemma (in UFT) Union_chain_empty: |
277 |
"c \<in> chain superfrechet \<Longrightarrow> {} \<notin> \<Union>c" |
|
278 |
proof |
|
279 |
assume 1: "c \<in> chain superfrechet" and 2: "{} \<in> \<Union>c" |
|
280 |
from 2 obtain x where 3: "x \<in> c" and 4: "{} \<in> x" .. |
|
281 |
from 1 3 have "filter x" by (rule lemma_mem_chain_filter) |
|
282 |
hence "{} \<notin> x" by (rule filter.empty) |
|
283 |
with 4 show "False" by simp |
|
284 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
285 |
|
17290 | 286 |
lemma (in UFT) Union_chain_Int: |
287 |
"\<lbrakk>c \<in> chain superfrechet; u \<in> \<Union>c; v \<in> \<Union>c\<rbrakk> \<Longrightarrow> u \<inter> v \<in> \<Union>c" |
|
288 |
proof - |
|
289 |
assume c: "c \<in> chain superfrechet" |
|
290 |
assume "u \<in> \<Union>c" |
|
291 |
then obtain x where ux: "u \<in> x" and xc: "x \<in> c" .. |
|
292 |
assume "v \<in> \<Union>c" |
|
293 |
then obtain y where vy: "v \<in> y" and yc: "y \<in> c" .. |
|
294 |
from c xc yc have "x \<subseteq> y \<or> y \<subseteq> x" by (rule chainD) |
|
295 |
with xc yc have xyc: "x \<union> y \<in> c" |
|
296 |
by (auto simp add: Un_absorb1 Un_absorb2) |
|
297 |
with c have fxy: "filter (x \<union> y)" by (rule lemma_mem_chain_filter) |
|
298 |
from ux have uxy: "u \<in> x \<union> y" by simp |
|
299 |
from vy have vxy: "v \<in> x \<union> y" by simp |
|
300 |
from fxy uxy vxy have "u \<inter> v \<in> x \<union> y" by (rule filter.Int) |
|
301 |
with xyc show "u \<inter> v \<in> \<Union>c" .. |
|
302 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
303 |
|
17290 | 304 |
lemma (in UFT) Union_chain_subset: |
305 |
"\<lbrakk>c \<in> chain superfrechet; u \<in> \<Union>c; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> \<Union>c" |
|
306 |
proof - |
|
307 |
assume c: "c \<in> chain superfrechet" |
|
308 |
and u: "u \<in> \<Union>c" and uv: "u \<subseteq> v" |
|
309 |
from u obtain x where ux: "u \<in> x" and xc: "x \<in> c" .. |
|
310 |
from c xc have fx: "filter x" by (rule lemma_mem_chain_filter) |
|
311 |
from fx ux uv have vx: "v \<in> x" by (rule filter.subset) |
|
312 |
with xc show "v \<in> \<Union>c" .. |
|
313 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
314 |
|
17290 | 315 |
lemma (in UFT) Union_chain_filter: |
316 |
assumes "c \<in> chain superfrechet" and "c \<noteq> {}" |
|
317 |
shows "filter (\<Union>c)" |
|
318 |
proof (rule filter.intro) |
|
319 |
show "UNIV \<in> \<Union>c" by (rule Union_chain_UNIV) |
|
320 |
next |
|
321 |
show "{} \<notin> \<Union>c" by (rule Union_chain_empty) |
|
322 |
next |
|
323 |
fix u v assume "u \<in> \<Union>c" and "v \<in> \<Union>c" |
|
324 |
show "u \<inter> v \<in> \<Union>c" by (rule Union_chain_Int) |
|
325 |
next |
|
326 |
fix u v assume "u \<in> \<Union>c" and "u \<subseteq> v" |
|
327 |
show "v \<in> \<Union>c" by (rule Union_chain_subset) |
|
328 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
329 |
|
17290 | 330 |
lemma (in UFT) lemma_mem_chain_frechet_subset: |
331 |
"\<lbrakk>c \<in> chain superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> frechet \<subseteq> x" |
|
332 |
by (unfold superfrechet_def chain_def, blast) |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
333 |
|
17290 | 334 |
lemma (in UFT) Union_chain_superfrechet: |
335 |
"\<lbrakk>c \<noteq> {}; c \<in> chain superfrechet\<rbrakk> \<Longrightarrow> \<Union>c \<in> superfrechet" |
|
336 |
proof (rule superfrechetI) |
|
337 |
assume 1: "c \<in> chain superfrechet" and 2: "c \<noteq> {}" |
|
338 |
thus "filter (\<Union>c)" by (rule Union_chain_filter) |
|
339 |
from 2 obtain x where 3: "x \<in> c" by blast |
|
340 |
from 1 3 have "frechet \<subseteq> x" by (rule lemma_mem_chain_frechet_subset) |
|
341 |
also from 3 have "x \<subseteq> \<Union>c" by blast |
|
342 |
finally show "frechet \<subseteq> \<Union>c" . |
|
343 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
344 |
|
17290 | 345 |
subsubsection {* Existence of free ultrafilter *} |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
346 |
|
17290 | 347 |
lemma (in UFT) max_cofinite_filter_Ex: |
348 |
"\<exists>U\<in>superfrechet. \<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> U = G" |
|
349 |
proof (rule Zorn_Lemma2 [rule_format]) |
|
350 |
fix c assume c: "c \<in> chain superfrechet" |
|
351 |
show "\<exists>U\<in>superfrechet. \<forall>G\<in>c. G \<subseteq> U" (is "?U") |
|
352 |
proof (cases) |
|
353 |
assume "c = {}" |
|
354 |
with frechet_in_superfrechet show "?U" by blast |
|
355 |
next |
|
356 |
assume A: "c \<noteq> {}" |
|
357 |
from A c have "\<Union>c \<in> superfrechet" |
|
358 |
by (rule Union_chain_superfrechet) |
|
359 |
thus "?U" by blast |
|
360 |
qed |
|
361 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
362 |
|
17290 | 363 |
lemma (in UFT) mem_superfrechet_all_infinite: |
364 |
"\<lbrakk>U \<in> superfrechet; A \<in> U\<rbrakk> \<Longrightarrow> infinite A" |
|
365 |
proof |
|
366 |
assume U: "U \<in> superfrechet" and A: "A \<in> U" and fin: "finite A" |
|
367 |
from U have fil: "filter U" and fre: "frechet \<subseteq> U" |
|
368 |
by (simp_all add: superfrechet_def) |
|
369 |
from fin have "- A \<in> frechet" by (simp add: frechet_def) |
|
370 |
with fre have cA: "- A \<in> U" by (rule subsetD) |
|
371 |
from fil A cA have "A \<inter> - A \<in> U" by (rule filter.Int) |
|
372 |
with fil show "False" by (simp add: filter.empty) |
|
373 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
374 |
|
17290 | 375 |
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
|
376 |
|
17290 | 377 |
lemma (in UFT) freeultrafilter_ex: |
378 |
"\<exists>U::'a set set. freeultrafilter U" |
|
379 |
proof - |
|
380 |
from max_cofinite_filter_Ex obtain U |
|
381 |
where U: "U \<in> superfrechet" |
|
382 |
and max [rule_format]: "\<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> U = G" .. |
|
383 |
from U have fil: "filter U" by (rule superfrechetD1) |
|
384 |
from U have fre: "frechet \<subseteq> U" by (rule superfrechetD2) |
|
385 |
have ultra: "ultrafilter_axioms U" |
|
386 |
proof (rule filter.max_filter_ultrafilter [OF fil]) |
|
387 |
fix G assume G: "filter G" and UG: "U \<subseteq> G" |
|
388 |
from fre UG have "frechet \<subseteq> G" by simp |
|
389 |
with G have "G \<in> superfrechet" by (rule superfrechetI) |
|
390 |
from this UG show "U = G" by (rule max) |
|
391 |
qed |
|
392 |
have free: "freeultrafilter_axioms U" |
|
393 |
proof (rule freeultrafilter_axioms.intro) |
|
394 |
fix A assume "A \<in> U" |
|
395 |
with U show "infinite A" by (rule mem_superfrechet_all_infinite) |
|
396 |
qed |
|
397 |
from fil ultra free have "freeultrafilter U" |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
17332
diff
changeset
|
398 |
by (rule freeultrafilter.intro [OF ultrafilter.intro]) |
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset
|
399 |
(* FIXME: unfold_locales should use chained facts *) |
17290 | 400 |
thus ?thesis .. |
401 |
qed |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
402 |
|
17290 | 403 |
lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
404 |
|
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
10750
diff
changeset
|
405 |
end |