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