60036
|
1 |
(* Title: HOL/Filter.thy
|
|
2 |
Author: Brian Huffman
|
|
3 |
Author: Johannes Hölzl
|
|
4 |
*)
|
|
5 |
|
|
6 |
section {* Filters on predicates *}
|
|
7 |
|
|
8 |
theory Filter
|
|
9 |
imports Set_Interval Lifting_Set
|
|
10 |
begin
|
|
11 |
|
|
12 |
subsection {* Filters *}
|
|
13 |
|
|
14 |
text {*
|
|
15 |
This definition also allows non-proper filters.
|
|
16 |
*}
|
|
17 |
|
|
18 |
locale is_filter =
|
|
19 |
fixes F :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
|
|
20 |
assumes True: "F (\<lambda>x. True)"
|
|
21 |
assumes conj: "F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x) \<Longrightarrow> F (\<lambda>x. P x \<and> Q x)"
|
|
22 |
assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x)"
|
|
23 |
|
|
24 |
typedef 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}"
|
|
25 |
proof
|
|
26 |
show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro)
|
|
27 |
qed
|
|
28 |
|
|
29 |
lemma is_filter_Rep_filter: "is_filter (Rep_filter F)"
|
|
30 |
using Rep_filter [of F] by simp
|
|
31 |
|
|
32 |
lemma Abs_filter_inverse':
|
|
33 |
assumes "is_filter F" shows "Rep_filter (Abs_filter F) = F"
|
|
34 |
using assms by (simp add: Abs_filter_inverse)
|
|
35 |
|
|
36 |
|
|
37 |
subsubsection {* Eventually *}
|
|
38 |
|
|
39 |
definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
|
|
40 |
where "eventually P F \<longleftrightarrow> Rep_filter F P"
|
|
41 |
|
|
42 |
lemma eventually_Abs_filter:
|
|
43 |
assumes "is_filter F" shows "eventually P (Abs_filter F) = F P"
|
|
44 |
unfolding eventually_def using assms by (simp add: Abs_filter_inverse)
|
|
45 |
|
|
46 |
lemma filter_eq_iff:
|
|
47 |
shows "F = F' \<longleftrightarrow> (\<forall>P. eventually P F = eventually P F')"
|
|
48 |
unfolding Rep_filter_inject [symmetric] fun_eq_iff eventually_def ..
|
|
49 |
|
|
50 |
lemma eventually_True [simp]: "eventually (\<lambda>x. True) F"
|
|
51 |
unfolding eventually_def
|
|
52 |
by (rule is_filter.True [OF is_filter_Rep_filter])
|
|
53 |
|
|
54 |
lemma always_eventually: "\<forall>x. P x \<Longrightarrow> eventually P F"
|
|
55 |
proof -
|
|
56 |
assume "\<forall>x. P x" hence "P = (\<lambda>x. True)" by (simp add: ext)
|
|
57 |
thus "eventually P F" by simp
|
|
58 |
qed
|
|
59 |
|
|
60 |
lemma eventually_mono:
|
|
61 |
"(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P F \<Longrightarrow> eventually Q F"
|
|
62 |
unfolding eventually_def
|
|
63 |
by (rule is_filter.mono [OF is_filter_Rep_filter])
|
|
64 |
|
|
65 |
lemma eventually_conj:
|
|
66 |
assumes P: "eventually (\<lambda>x. P x) F"
|
|
67 |
assumes Q: "eventually (\<lambda>x. Q x) F"
|
|
68 |
shows "eventually (\<lambda>x. P x \<and> Q x) F"
|
|
69 |
using assms unfolding eventually_def
|
|
70 |
by (rule is_filter.conj [OF is_filter_Rep_filter])
|
|
71 |
|
|
72 |
lemma eventually_Ball_finite:
|
|
73 |
assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net"
|
|
74 |
shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"
|
|
75 |
using assms by (induct set: finite, simp, simp add: eventually_conj)
|
|
76 |
|
|
77 |
lemma eventually_all_finite:
|
|
78 |
fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool"
|
|
79 |
assumes "\<And>y. eventually (\<lambda>x. P x y) net"
|
|
80 |
shows "eventually (\<lambda>x. \<forall>y. P x y) net"
|
|
81 |
using eventually_Ball_finite [of UNIV P] assms by simp
|
|
82 |
|
|
83 |
lemma eventually_mp:
|
|
84 |
assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
|
|
85 |
assumes "eventually (\<lambda>x. P x) F"
|
|
86 |
shows "eventually (\<lambda>x. Q x) F"
|
|
87 |
proof (rule eventually_mono)
|
|
88 |
show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp
|
|
89 |
show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F"
|
|
90 |
using assms by (rule eventually_conj)
|
|
91 |
qed
|
|
92 |
|
|
93 |
lemma eventually_rev_mp:
|
|
94 |
assumes "eventually (\<lambda>x. P x) F"
|
|
95 |
assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
|
|
96 |
shows "eventually (\<lambda>x. Q x) F"
|
|
97 |
using assms(2) assms(1) by (rule eventually_mp)
|
|
98 |
|
|
99 |
lemma eventually_conj_iff:
|
|
100 |
"eventually (\<lambda>x. P x \<and> Q x) F \<longleftrightarrow> eventually P F \<and> eventually Q F"
|
|
101 |
by (auto intro: eventually_conj elim: eventually_rev_mp)
|
|
102 |
|
|
103 |
lemma eventually_elim1:
|
|
104 |
assumes "eventually (\<lambda>i. P i) F"
|
|
105 |
assumes "\<And>i. P i \<Longrightarrow> Q i"
|
|
106 |
shows "eventually (\<lambda>i. Q i) F"
|
|
107 |
using assms by (auto elim!: eventually_rev_mp)
|
|
108 |
|
|
109 |
lemma eventually_elim2:
|
|
110 |
assumes "eventually (\<lambda>i. P i) F"
|
|
111 |
assumes "eventually (\<lambda>i. Q i) F"
|
|
112 |
assumes "\<And>i. P i \<Longrightarrow> Q i \<Longrightarrow> R i"
|
|
113 |
shows "eventually (\<lambda>i. R i) F"
|
|
114 |
using assms by (auto elim!: eventually_rev_mp)
|
|
115 |
|
|
116 |
lemma not_eventually_impI: "eventually P F \<Longrightarrow> \<not> eventually Q F \<Longrightarrow> \<not> eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
|
|
117 |
by (auto intro: eventually_mp)
|
|
118 |
|
|
119 |
lemma not_eventuallyD: "\<not> eventually P F \<Longrightarrow> \<exists>x. \<not> P x"
|
|
120 |
by (metis always_eventually)
|
|
121 |
|
|
122 |
lemma eventually_subst:
|
|
123 |
assumes "eventually (\<lambda>n. P n = Q n) F"
|
|
124 |
shows "eventually P F = eventually Q F" (is "?L = ?R")
|
|
125 |
proof -
|
|
126 |
from assms have "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
|
|
127 |
and "eventually (\<lambda>x. Q x \<longrightarrow> P x) F"
|
|
128 |
by (auto elim: eventually_elim1)
|
|
129 |
then show ?thesis by (auto elim: eventually_elim2)
|
|
130 |
qed
|
|
131 |
|
|
132 |
ML {*
|
|
133 |
fun eventually_elim_tac ctxt facts = SUBGOAL_CASES (fn (goal, i) =>
|
|
134 |
let
|
|
135 |
val mp_thms = facts RL @{thms eventually_rev_mp}
|
|
136 |
val raw_elim_thm =
|
|
137 |
(@{thm allI} RS @{thm always_eventually})
|
|
138 |
|> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
|
|
139 |
|> fold (fn _ => fn thm => @{thm impI} RS thm) facts
|
|
140 |
val cases_prop = Thm.prop_of (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal))
|
|
141 |
val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
|
|
142 |
in
|
|
143 |
CASES cases (rtac raw_elim_thm i)
|
|
144 |
end)
|
|
145 |
*}
|
|
146 |
|
|
147 |
method_setup eventually_elim = {*
|
|
148 |
Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt))
|
|
149 |
*} "elimination of eventually quantifiers"
|
|
150 |
|
|
151 |
|
|
152 |
subsubsection {* Finer-than relation *}
|
|
153 |
|
|
154 |
text {* @{term "F \<le> F'"} means that filter @{term F} is finer than
|
|
155 |
filter @{term F'}. *}
|
|
156 |
|
|
157 |
instantiation filter :: (type) complete_lattice
|
|
158 |
begin
|
|
159 |
|
|
160 |
definition le_filter_def:
|
|
161 |
"F \<le> F' \<longleftrightarrow> (\<forall>P. eventually P F' \<longrightarrow> eventually P F)"
|
|
162 |
|
|
163 |
definition
|
|
164 |
"(F :: 'a filter) < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"
|
|
165 |
|
|
166 |
definition
|
|
167 |
"top = Abs_filter (\<lambda>P. \<forall>x. P x)"
|
|
168 |
|
|
169 |
definition
|
|
170 |
"bot = Abs_filter (\<lambda>P. True)"
|
|
171 |
|
|
172 |
definition
|
|
173 |
"sup F F' = Abs_filter (\<lambda>P. eventually P F \<and> eventually P F')"
|
|
174 |
|
|
175 |
definition
|
|
176 |
"inf F F' = Abs_filter
|
|
177 |
(\<lambda>P. \<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
|
|
178 |
|
|
179 |
definition
|
|
180 |
"Sup S = Abs_filter (\<lambda>P. \<forall>F\<in>S. eventually P F)"
|
|
181 |
|
|
182 |
definition
|
|
183 |
"Inf S = Sup {F::'a filter. \<forall>F'\<in>S. F \<le> F'}"
|
|
184 |
|
|
185 |
lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)"
|
|
186 |
unfolding top_filter_def
|
|
187 |
by (rule eventually_Abs_filter, rule is_filter.intro, auto)
|
|
188 |
|
|
189 |
lemma eventually_bot [simp]: "eventually P bot"
|
|
190 |
unfolding bot_filter_def
|
|
191 |
by (subst eventually_Abs_filter, rule is_filter.intro, auto)
|
|
192 |
|
|
193 |
lemma eventually_sup:
|
|
194 |
"eventually P (sup F F') \<longleftrightarrow> eventually P F \<and> eventually P F'"
|
|
195 |
unfolding sup_filter_def
|
|
196 |
by (rule eventually_Abs_filter, rule is_filter.intro)
|
|
197 |
(auto elim!: eventually_rev_mp)
|
|
198 |
|
|
199 |
lemma eventually_inf:
|
|
200 |
"eventually P (inf F F') \<longleftrightarrow>
|
|
201 |
(\<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
|
|
202 |
unfolding inf_filter_def
|
|
203 |
apply (rule eventually_Abs_filter, rule is_filter.intro)
|
|
204 |
apply (fast intro: eventually_True)
|
|
205 |
apply clarify
|
|
206 |
apply (intro exI conjI)
|
|
207 |
apply (erule (1) eventually_conj)
|
|
208 |
apply (erule (1) eventually_conj)
|
|
209 |
apply simp
|
|
210 |
apply auto
|
|
211 |
done
|
|
212 |
|
|
213 |
lemma eventually_Sup:
|
|
214 |
"eventually P (Sup S) \<longleftrightarrow> (\<forall>F\<in>S. eventually P F)"
|
|
215 |
unfolding Sup_filter_def
|
|
216 |
apply (rule eventually_Abs_filter, rule is_filter.intro)
|
|
217 |
apply (auto intro: eventually_conj elim!: eventually_rev_mp)
|
|
218 |
done
|
|
219 |
|
|
220 |
instance proof
|
|
221 |
fix F F' F'' :: "'a filter" and S :: "'a filter set"
|
|
222 |
{ show "F < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"
|
|
223 |
by (rule less_filter_def) }
|
|
224 |
{ show "F \<le> F"
|
|
225 |
unfolding le_filter_def by simp }
|
|
226 |
{ assume "F \<le> F'" and "F' \<le> F''" thus "F \<le> F''"
|
|
227 |
unfolding le_filter_def by simp }
|
|
228 |
{ assume "F \<le> F'" and "F' \<le> F" thus "F = F'"
|
|
229 |
unfolding le_filter_def filter_eq_iff by fast }
|
|
230 |
{ show "inf F F' \<le> F" and "inf F F' \<le> F'"
|
|
231 |
unfolding le_filter_def eventually_inf by (auto intro: eventually_True) }
|
|
232 |
{ assume "F \<le> F'" and "F \<le> F''" thus "F \<le> inf F' F''"
|
|
233 |
unfolding le_filter_def eventually_inf
|
|
234 |
by (auto elim!: eventually_mono intro: eventually_conj) }
|
|
235 |
{ show "F \<le> sup F F'" and "F' \<le> sup F F'"
|
|
236 |
unfolding le_filter_def eventually_sup by simp_all }
|
|
237 |
{ assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''"
|
|
238 |
unfolding le_filter_def eventually_sup by simp }
|
|
239 |
{ assume "F'' \<in> S" thus "Inf S \<le> F''"
|
|
240 |
unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
|
|
241 |
{ assume "\<And>F'. F' \<in> S \<Longrightarrow> F \<le> F'" thus "F \<le> Inf S"
|
|
242 |
unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
|
|
243 |
{ assume "F \<in> S" thus "F \<le> Sup S"
|
|
244 |
unfolding le_filter_def eventually_Sup by simp }
|
|
245 |
{ assume "\<And>F. F \<in> S \<Longrightarrow> F \<le> F'" thus "Sup S \<le> F'"
|
|
246 |
unfolding le_filter_def eventually_Sup by simp }
|
|
247 |
{ show "Inf {} = (top::'a filter)"
|
|
248 |
by (auto simp: top_filter_def Inf_filter_def Sup_filter_def)
|
|
249 |
(metis (full_types) top_filter_def always_eventually eventually_top) }
|
|
250 |
{ show "Sup {} = (bot::'a filter)"
|
|
251 |
by (auto simp: bot_filter_def Sup_filter_def) }
|
|
252 |
qed
|
|
253 |
|
|
254 |
end
|
|
255 |
|
|
256 |
lemma filter_leD:
|
|
257 |
"F \<le> F' \<Longrightarrow> eventually P F' \<Longrightarrow> eventually P F"
|
|
258 |
unfolding le_filter_def by simp
|
|
259 |
|
|
260 |
lemma filter_leI:
|
|
261 |
"(\<And>P. eventually P F' \<Longrightarrow> eventually P F) \<Longrightarrow> F \<le> F'"
|
|
262 |
unfolding le_filter_def by simp
|
|
263 |
|
|
264 |
lemma eventually_False:
|
|
265 |
"eventually (\<lambda>x. False) F \<longleftrightarrow> F = bot"
|
|
266 |
unfolding filter_eq_iff by (auto elim: eventually_rev_mp)
|
|
267 |
|
|
268 |
abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
|
|
269 |
where "trivial_limit F \<equiv> F = bot"
|
|
270 |
|
|
271 |
lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
|
|
272 |
by (rule eventually_False [symmetric])
|
|
273 |
|
|
274 |
lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
|
|
275 |
by (cases P) (simp_all add: eventually_False)
|
|
276 |
|
|
277 |
lemma eventually_Inf: "eventually P (Inf B) \<longleftrightarrow> (\<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X))"
|
|
278 |
proof -
|
|
279 |
let ?F = "\<lambda>P. \<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X)"
|
|
280 |
|
|
281 |
{ fix P have "eventually P (Abs_filter ?F) \<longleftrightarrow> ?F P"
|
|
282 |
proof (rule eventually_Abs_filter is_filter.intro)+
|
|
283 |
show "?F (\<lambda>x. True)"
|
|
284 |
by (rule exI[of _ "{}"]) (simp add: le_fun_def)
|
|
285 |
next
|
|
286 |
fix P Q
|
|
287 |
assume "?F P" then guess X ..
|
|
288 |
moreover
|
|
289 |
assume "?F Q" then guess Y ..
|
|
290 |
ultimately show "?F (\<lambda>x. P x \<and> Q x)"
|
|
291 |
by (intro exI[of _ "X \<union> Y"])
|
|
292 |
(auto simp: Inf_union_distrib eventually_inf)
|
|
293 |
next
|
|
294 |
fix P Q
|
|
295 |
assume "?F P" then guess X ..
|
|
296 |
moreover assume "\<forall>x. P x \<longrightarrow> Q x"
|
|
297 |
ultimately show "?F Q"
|
|
298 |
by (intro exI[of _ X]) (auto elim: eventually_elim1)
|
|
299 |
qed }
|
|
300 |
note eventually_F = this
|
|
301 |
|
|
302 |
have "Inf B = Abs_filter ?F"
|
|
303 |
proof (intro antisym Inf_greatest)
|
|
304 |
show "Inf B \<le> Abs_filter ?F"
|
|
305 |
by (auto simp: le_filter_def eventually_F dest: Inf_superset_mono)
|
|
306 |
next
|
|
307 |
fix F assume "F \<in> B" then show "Abs_filter ?F \<le> F"
|
|
308 |
by (auto simp add: le_filter_def eventually_F intro!: exI[of _ "{F}"])
|
|
309 |
qed
|
|
310 |
then show ?thesis
|
|
311 |
by (simp add: eventually_F)
|
|
312 |
qed
|
|
313 |
|
|
314 |
lemma eventually_INF: "eventually P (INF b:B. F b) \<longleftrightarrow> (\<exists>X\<subseteq>B. finite X \<and> eventually P (INF b:X. F b))"
|
|
315 |
unfolding INF_def[of B] eventually_Inf[of P "F`B"]
|
|
316 |
by (metis Inf_image_eq finite_imageI image_mono finite_subset_image)
|
|
317 |
|
|
318 |
lemma Inf_filter_not_bot:
|
|
319 |
fixes B :: "'a filter set"
|
|
320 |
shows "(\<And>X. X \<subseteq> B \<Longrightarrow> finite X \<Longrightarrow> Inf X \<noteq> bot) \<Longrightarrow> Inf B \<noteq> bot"
|
|
321 |
unfolding trivial_limit_def eventually_Inf[of _ B]
|
|
322 |
bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
|
|
323 |
|
|
324 |
lemma INF_filter_not_bot:
|
|
325 |
fixes F :: "'i \<Rightarrow> 'a filter"
|
|
326 |
shows "(\<And>X. X \<subseteq> B \<Longrightarrow> finite X \<Longrightarrow> (INF b:X. F b) \<noteq> bot) \<Longrightarrow> (INF b:B. F b) \<noteq> bot"
|
|
327 |
unfolding trivial_limit_def eventually_INF[of _ B]
|
|
328 |
bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
|
|
329 |
|
|
330 |
lemma eventually_Inf_base:
|
|
331 |
assumes "B \<noteq> {}" and base: "\<And>F G. F \<in> B \<Longrightarrow> G \<in> B \<Longrightarrow> \<exists>x\<in>B. x \<le> inf F G"
|
|
332 |
shows "eventually P (Inf B) \<longleftrightarrow> (\<exists>b\<in>B. eventually P b)"
|
|
333 |
proof (subst eventually_Inf, safe)
|
|
334 |
fix X assume "finite X" "X \<subseteq> B"
|
|
335 |
then have "\<exists>b\<in>B. \<forall>x\<in>X. b \<le> x"
|
|
336 |
proof induct
|
|
337 |
case empty then show ?case
|
|
338 |
using `B \<noteq> {}` by auto
|
|
339 |
next
|
|
340 |
case (insert x X)
|
|
341 |
then obtain b where "b \<in> B" "\<And>x. x \<in> X \<Longrightarrow> b \<le> x"
|
|
342 |
by auto
|
|
343 |
with `insert x X \<subseteq> B` base[of b x] show ?case
|
|
344 |
by (auto intro: order_trans)
|
|
345 |
qed
|
|
346 |
then obtain b where "b \<in> B" "b \<le> Inf X"
|
|
347 |
by (auto simp: le_Inf_iff)
|
|
348 |
then show "eventually P (Inf X) \<Longrightarrow> Bex B (eventually P)"
|
|
349 |
by (intro bexI[of _ b]) (auto simp: le_filter_def)
|
|
350 |
qed (auto intro!: exI[of _ "{x}" for x])
|
|
351 |
|
|
352 |
lemma eventually_INF_base:
|
|
353 |
"B \<noteq> {} \<Longrightarrow> (\<And>a b. a \<in> B \<Longrightarrow> b \<in> B \<Longrightarrow> \<exists>x\<in>B. F x \<le> inf (F a) (F b)) \<Longrightarrow>
|
|
354 |
eventually P (INF b:B. F b) \<longleftrightarrow> (\<exists>b\<in>B. eventually P (F b))"
|
|
355 |
unfolding INF_def by (subst eventually_Inf_base) auto
|
|
356 |
|
|
357 |
|
|
358 |
subsubsection {* Map function for filters *}
|
|
359 |
|
|
360 |
definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter"
|
|
361 |
where "filtermap f F = Abs_filter (\<lambda>P. eventually (\<lambda>x. P (f x)) F)"
|
|
362 |
|
|
363 |
lemma eventually_filtermap:
|
|
364 |
"eventually P (filtermap f F) = eventually (\<lambda>x. P (f x)) F"
|
|
365 |
unfolding filtermap_def
|
|
366 |
apply (rule eventually_Abs_filter)
|
|
367 |
apply (rule is_filter.intro)
|
|
368 |
apply (auto elim!: eventually_rev_mp)
|
|
369 |
done
|
|
370 |
|
|
371 |
lemma filtermap_ident: "filtermap (\<lambda>x. x) F = F"
|
|
372 |
by (simp add: filter_eq_iff eventually_filtermap)
|
|
373 |
|
|
374 |
lemma filtermap_filtermap:
|
|
375 |
"filtermap f (filtermap g F) = filtermap (\<lambda>x. f (g x)) F"
|
|
376 |
by (simp add: filter_eq_iff eventually_filtermap)
|
|
377 |
|
|
378 |
lemma filtermap_mono: "F \<le> F' \<Longrightarrow> filtermap f F \<le> filtermap f F'"
|
|
379 |
unfolding le_filter_def eventually_filtermap by simp
|
|
380 |
|
|
381 |
lemma filtermap_bot [simp]: "filtermap f bot = bot"
|
|
382 |
by (simp add: filter_eq_iff eventually_filtermap)
|
|
383 |
|
|
384 |
lemma filtermap_sup: "filtermap f (sup F1 F2) = sup (filtermap f F1) (filtermap f F2)"
|
|
385 |
by (auto simp: filter_eq_iff eventually_filtermap eventually_sup)
|
|
386 |
|
|
387 |
lemma filtermap_inf: "filtermap f (inf F1 F2) \<le> inf (filtermap f F1) (filtermap f F2)"
|
|
388 |
by (auto simp: le_filter_def eventually_filtermap eventually_inf)
|
|
389 |
|
|
390 |
lemma filtermap_INF: "filtermap f (INF b:B. F b) \<le> (INF b:B. filtermap f (F b))"
|
|
391 |
proof -
|
|
392 |
{ fix X :: "'c set" assume "finite X"
|
|
393 |
then have "filtermap f (INFIMUM X F) \<le> (INF b:X. filtermap f (F b))"
|
|
394 |
proof induct
|
|
395 |
case (insert x X)
|
|
396 |
have "filtermap f (INF a:insert x X. F a) \<le> inf (filtermap f (F x)) (filtermap f (INF a:X. F a))"
|
|
397 |
by (rule order_trans[OF _ filtermap_inf]) simp
|
|
398 |
also have "\<dots> \<le> inf (filtermap f (F x)) (INF a:X. filtermap f (F a))"
|
|
399 |
by (intro inf_mono insert order_refl)
|
|
400 |
finally show ?case
|
|
401 |
by simp
|
|
402 |
qed simp }
|
|
403 |
then show ?thesis
|
|
404 |
unfolding le_filter_def eventually_filtermap
|
|
405 |
by (subst (1 2) eventually_INF) auto
|
|
406 |
qed
|
|
407 |
subsubsection {* Standard filters *}
|
|
408 |
|
|
409 |
definition principal :: "'a set \<Rightarrow> 'a filter" where
|
|
410 |
"principal S = Abs_filter (\<lambda>P. \<forall>x\<in>S. P x)"
|
|
411 |
|
|
412 |
lemma eventually_principal: "eventually P (principal S) \<longleftrightarrow> (\<forall>x\<in>S. P x)"
|
|
413 |
unfolding principal_def
|
|
414 |
by (rule eventually_Abs_filter, rule is_filter.intro) auto
|
|
415 |
|
|
416 |
lemma eventually_inf_principal: "eventually P (inf F (principal s)) \<longleftrightarrow> eventually (\<lambda>x. x \<in> s \<longrightarrow> P x) F"
|
|
417 |
unfolding eventually_inf eventually_principal by (auto elim: eventually_elim1)
|
|
418 |
|
|
419 |
lemma principal_UNIV[simp]: "principal UNIV = top"
|
|
420 |
by (auto simp: filter_eq_iff eventually_principal)
|
|
421 |
|
|
422 |
lemma principal_empty[simp]: "principal {} = bot"
|
|
423 |
by (auto simp: filter_eq_iff eventually_principal)
|
|
424 |
|
|
425 |
lemma principal_eq_bot_iff: "principal X = bot \<longleftrightarrow> X = {}"
|
|
426 |
by (auto simp add: filter_eq_iff eventually_principal)
|
|
427 |
|
|
428 |
lemma principal_le_iff[iff]: "principal A \<le> principal B \<longleftrightarrow> A \<subseteq> B"
|
|
429 |
by (auto simp: le_filter_def eventually_principal)
|
|
430 |
|
|
431 |
lemma le_principal: "F \<le> principal A \<longleftrightarrow> eventually (\<lambda>x. x \<in> A) F"
|
|
432 |
unfolding le_filter_def eventually_principal
|
|
433 |
apply safe
|
|
434 |
apply (erule_tac x="\<lambda>x. x \<in> A" in allE)
|
|
435 |
apply (auto elim: eventually_elim1)
|
|
436 |
done
|
|
437 |
|
|
438 |
lemma principal_inject[iff]: "principal A = principal B \<longleftrightarrow> A = B"
|
|
439 |
unfolding eq_iff by simp
|
|
440 |
|
|
441 |
lemma sup_principal[simp]: "sup (principal A) (principal B) = principal (A \<union> B)"
|
|
442 |
unfolding filter_eq_iff eventually_sup eventually_principal by auto
|
|
443 |
|
|
444 |
lemma inf_principal[simp]: "inf (principal A) (principal B) = principal (A \<inter> B)"
|
|
445 |
unfolding filter_eq_iff eventually_inf eventually_principal
|
|
446 |
by (auto intro: exI[of _ "\<lambda>x. x \<in> A"] exI[of _ "\<lambda>x. x \<in> B"])
|
|
447 |
|
|
448 |
lemma SUP_principal[simp]: "(SUP i : I. principal (A i)) = principal (\<Union>i\<in>I. A i)"
|
|
449 |
unfolding filter_eq_iff eventually_Sup SUP_def by (auto simp: eventually_principal)
|
|
450 |
|
|
451 |
lemma INF_principal_finite: "finite X \<Longrightarrow> (INF x:X. principal (f x)) = principal (\<Inter>x\<in>X. f x)"
|
|
452 |
by (induct X rule: finite_induct) auto
|
|
453 |
|
|
454 |
lemma filtermap_principal[simp]: "filtermap f (principal A) = principal (f ` A)"
|
|
455 |
unfolding filter_eq_iff eventually_filtermap eventually_principal by simp
|
|
456 |
|
|
457 |
subsubsection {* Order filters *}
|
|
458 |
|
|
459 |
definition at_top :: "('a::order) filter"
|
|
460 |
where "at_top = (INF k. principal {k ..})"
|
|
461 |
|
|
462 |
lemma at_top_sub: "at_top = (INF k:{c::'a::linorder..}. principal {k ..})"
|
|
463 |
by (auto intro!: INF_eq max.cobounded1 max.cobounded2 simp: at_top_def)
|
|
464 |
|
|
465 |
lemma eventually_at_top_linorder: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>n\<ge>N. P n)"
|
|
466 |
unfolding at_top_def
|
|
467 |
by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
|
|
468 |
|
|
469 |
lemma eventually_ge_at_top:
|
|
470 |
"eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
|
|
471 |
unfolding eventually_at_top_linorder by auto
|
|
472 |
|
|
473 |
lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::{no_top, linorder}. \<forall>n>N. P n)"
|
|
474 |
proof -
|
|
475 |
have "eventually P (INF k. principal {k <..}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n>N. P n)"
|
|
476 |
by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
|
|
477 |
also have "(INF k. principal {k::'a <..}) = at_top"
|
|
478 |
unfolding at_top_def
|
|
479 |
by (intro INF_eq) (auto intro: less_imp_le simp: Ici_subset_Ioi_iff gt_ex)
|
|
480 |
finally show ?thesis .
|
|
481 |
qed
|
|
482 |
|
|
483 |
lemma eventually_gt_at_top:
|
|
484 |
"eventually (\<lambda>x. (c::_::unbounded_dense_linorder) < x) at_top"
|
|
485 |
unfolding eventually_at_top_dense by auto
|
|
486 |
|
|
487 |
definition at_bot :: "('a::order) filter"
|
|
488 |
where "at_bot = (INF k. principal {.. k})"
|
|
489 |
|
|
490 |
lemma at_bot_sub: "at_bot = (INF k:{.. c::'a::linorder}. principal {.. k})"
|
|
491 |
by (auto intro!: INF_eq min.cobounded1 min.cobounded2 simp: at_bot_def)
|
|
492 |
|
|
493 |
lemma eventually_at_bot_linorder:
|
|
494 |
fixes P :: "'a::linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n\<le>N. P n)"
|
|
495 |
unfolding at_bot_def
|
|
496 |
by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
|
|
497 |
|
|
498 |
lemma eventually_le_at_bot:
|
|
499 |
"eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot"
|
|
500 |
unfolding eventually_at_bot_linorder by auto
|
|
501 |
|
|
502 |
lemma eventually_at_bot_dense: "eventually P at_bot \<longleftrightarrow> (\<exists>N::'a::{no_bot, linorder}. \<forall>n<N. P n)"
|
|
503 |
proof -
|
|
504 |
have "eventually P (INF k. principal {..< k}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n<N. P n)"
|
|
505 |
by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
|
|
506 |
also have "(INF k. principal {..< k::'a}) = at_bot"
|
|
507 |
unfolding at_bot_def
|
|
508 |
by (intro INF_eq) (auto intro: less_imp_le simp: Iic_subset_Iio_iff lt_ex)
|
|
509 |
finally show ?thesis .
|
|
510 |
qed
|
|
511 |
|
|
512 |
lemma eventually_gt_at_bot:
|
|
513 |
"eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
|
|
514 |
unfolding eventually_at_bot_dense by auto
|
|
515 |
|
|
516 |
lemma trivial_limit_at_bot_linorder: "\<not> trivial_limit (at_bot ::('a::linorder) filter)"
|
|
517 |
unfolding trivial_limit_def
|
|
518 |
by (metis eventually_at_bot_linorder order_refl)
|
|
519 |
|
|
520 |
lemma trivial_limit_at_top_linorder: "\<not> trivial_limit (at_top ::('a::linorder) filter)"
|
|
521 |
unfolding trivial_limit_def
|
|
522 |
by (metis eventually_at_top_linorder order_refl)
|
|
523 |
|
|
524 |
subsection {* Sequentially *}
|
|
525 |
|
|
526 |
abbreviation sequentially :: "nat filter"
|
|
527 |
where "sequentially \<equiv> at_top"
|
|
528 |
|
|
529 |
lemma eventually_sequentially:
|
|
530 |
"eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
|
|
531 |
by (rule eventually_at_top_linorder)
|
|
532 |
|
|
533 |
lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"
|
|
534 |
unfolding filter_eq_iff eventually_sequentially by auto
|
|
535 |
|
|
536 |
lemmas trivial_limit_sequentially = sequentially_bot
|
|
537 |
|
|
538 |
lemma eventually_False_sequentially [simp]:
|
|
539 |
"\<not> eventually (\<lambda>n. False) sequentially"
|
|
540 |
by (simp add: eventually_False)
|
|
541 |
|
|
542 |
lemma le_sequentially:
|
|
543 |
"F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)"
|
|
544 |
by (simp add: at_top_def le_INF_iff le_principal)
|
|
545 |
|
|
546 |
lemma eventually_sequentiallyI:
|
|
547 |
assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
|
|
548 |
shows "eventually P sequentially"
|
|
549 |
using assms by (auto simp: eventually_sequentially)
|
|
550 |
|
|
551 |
lemma eventually_sequentially_seg:
|
|
552 |
"eventually (\<lambda>n. P (n + k)) sequentially \<longleftrightarrow> eventually P sequentially"
|
|
553 |
unfolding eventually_sequentially
|
|
554 |
apply safe
|
|
555 |
apply (rule_tac x="N + k" in exI)
|
|
556 |
apply rule
|
|
557 |
apply (erule_tac x="n - k" in allE)
|
|
558 |
apply auto []
|
|
559 |
apply (rule_tac x=N in exI)
|
|
560 |
apply auto []
|
|
561 |
done
|
|
562 |
|
|
563 |
|
|
564 |
subsection {* Limits *}
|
|
565 |
|
|
566 |
definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
|
|
567 |
"filterlim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2"
|
|
568 |
|
|
569 |
syntax
|
|
570 |
"_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10)
|
|
571 |
|
|
572 |
translations
|
|
573 |
"LIM x F1. f :> F2" == "CONST filterlim (%x. f) F2 F1"
|
|
574 |
|
|
575 |
lemma filterlim_iff:
|
|
576 |
"(LIM x F1. f x :> F2) \<longleftrightarrow> (\<forall>P. eventually P F2 \<longrightarrow> eventually (\<lambda>x. P (f x)) F1)"
|
|
577 |
unfolding filterlim_def le_filter_def eventually_filtermap ..
|
|
578 |
|
|
579 |
lemma filterlim_compose:
|
|
580 |
"filterlim g F3 F2 \<Longrightarrow> filterlim f F2 F1 \<Longrightarrow> filterlim (\<lambda>x. g (f x)) F3 F1"
|
|
581 |
unfolding filterlim_def filtermap_filtermap[symmetric] by (metis filtermap_mono order_trans)
|
|
582 |
|
|
583 |
lemma filterlim_mono:
|
|
584 |
"filterlim f F2 F1 \<Longrightarrow> F2 \<le> F2' \<Longrightarrow> F1' \<le> F1 \<Longrightarrow> filterlim f F2' F1'"
|
|
585 |
unfolding filterlim_def by (metis filtermap_mono order_trans)
|
|
586 |
|
|
587 |
lemma filterlim_ident: "LIM x F. x :> F"
|
|
588 |
by (simp add: filterlim_def filtermap_ident)
|
|
589 |
|
|
590 |
lemma filterlim_cong:
|
|
591 |
"F1 = F1' \<Longrightarrow> F2 = F2' \<Longrightarrow> eventually (\<lambda>x. f x = g x) F2 \<Longrightarrow> filterlim f F1 F2 = filterlim g F1' F2'"
|
|
592 |
by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2)
|
|
593 |
|
|
594 |
lemma filterlim_mono_eventually:
|
|
595 |
assumes "filterlim f F G" and ord: "F \<le> F'" "G' \<le> G"
|
|
596 |
assumes eq: "eventually (\<lambda>x. f x = f' x) G'"
|
|
597 |
shows "filterlim f' F' G'"
|
|
598 |
apply (rule filterlim_cong[OF refl refl eq, THEN iffD1])
|
|
599 |
apply (rule filterlim_mono[OF _ ord])
|
|
600 |
apply fact
|
|
601 |
done
|
|
602 |
|
|
603 |
lemma filtermap_mono_strong: "inj f \<Longrightarrow> filtermap f F \<le> filtermap f G \<longleftrightarrow> F \<le> G"
|
|
604 |
apply (auto intro!: filtermap_mono) []
|
|
605 |
apply (auto simp: le_filter_def eventually_filtermap)
|
|
606 |
apply (erule_tac x="\<lambda>x. P (inv f x)" in allE)
|
|
607 |
apply auto
|
|
608 |
done
|
|
609 |
|
|
610 |
lemma filtermap_eq_strong: "inj f \<Longrightarrow> filtermap f F = filtermap f G \<longleftrightarrow> F = G"
|
|
611 |
by (simp add: filtermap_mono_strong eq_iff)
|
|
612 |
|
|
613 |
lemma filterlim_principal:
|
|
614 |
"(LIM x F. f x :> principal S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F)"
|
|
615 |
unfolding filterlim_def eventually_filtermap le_principal ..
|
|
616 |
|
|
617 |
lemma filterlim_inf:
|
|
618 |
"(LIM x F1. f x :> inf F2 F3) \<longleftrightarrow> ((LIM x F1. f x :> F2) \<and> (LIM x F1. f x :> F3))"
|
|
619 |
unfolding filterlim_def by simp
|
|
620 |
|
|
621 |
lemma filterlim_INF:
|
|
622 |
"(LIM x F. f x :> (INF b:B. G b)) \<longleftrightarrow> (\<forall>b\<in>B. LIM x F. f x :> G b)"
|
|
623 |
unfolding filterlim_def le_INF_iff ..
|
|
624 |
|
|
625 |
lemma filterlim_INF_INF:
|
|
626 |
"(\<And>m. m \<in> J \<Longrightarrow> \<exists>i\<in>I. filtermap f (F i) \<le> G m) \<Longrightarrow> LIM x (INF i:I. F i). f x :> (INF j:J. G j)"
|
|
627 |
unfolding filterlim_def by (rule order_trans[OF filtermap_INF INF_mono])
|
|
628 |
|
|
629 |
lemma filterlim_base:
|
|
630 |
"(\<And>m x. m \<in> J \<Longrightarrow> i m \<in> I) \<Longrightarrow> (\<And>m x. m \<in> J \<Longrightarrow> x \<in> F (i m) \<Longrightarrow> f x \<in> G m) \<Longrightarrow>
|
|
631 |
LIM x (INF i:I. principal (F i)). f x :> (INF j:J. principal (G j))"
|
|
632 |
by (force intro!: filterlim_INF_INF simp: image_subset_iff)
|
|
633 |
|
|
634 |
lemma filterlim_base_iff:
|
|
635 |
assumes "I \<noteq> {}" and chain: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> F i \<subseteq> F j \<or> F j \<subseteq> F i"
|
|
636 |
shows "(LIM x (INF i:I. principal (F i)). f x :> INF j:J. principal (G j)) \<longleftrightarrow>
|
|
637 |
(\<forall>j\<in>J. \<exists>i\<in>I. \<forall>x\<in>F i. f x \<in> G j)"
|
|
638 |
unfolding filterlim_INF filterlim_principal
|
|
639 |
proof (subst eventually_INF_base)
|
|
640 |
fix i j assume "i \<in> I" "j \<in> I"
|
|
641 |
with chain[OF this] show "\<exists>x\<in>I. principal (F x) \<le> inf (principal (F i)) (principal (F j))"
|
|
642 |
by auto
|
|
643 |
qed (auto simp: eventually_principal `I \<noteq> {}`)
|
|
644 |
|
|
645 |
lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"
|
|
646 |
unfolding filterlim_def filtermap_filtermap ..
|
|
647 |
|
|
648 |
lemma filterlim_sup:
|
|
649 |
"filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)"
|
|
650 |
unfolding filterlim_def filtermap_sup by auto
|
|
651 |
|
|
652 |
lemma eventually_sequentially_Suc: "eventually (\<lambda>i. P (Suc i)) sequentially \<longleftrightarrow> eventually P sequentially"
|
|
653 |
unfolding eventually_sequentially by (metis Suc_le_D Suc_le_mono le_Suc_eq)
|
|
654 |
|
|
655 |
lemma filterlim_sequentially_Suc:
|
|
656 |
"(LIM x sequentially. f (Suc x) :> F) \<longleftrightarrow> (LIM x sequentially. f x :> F)"
|
|
657 |
unfolding filterlim_iff by (subst eventually_sequentially_Suc) simp
|
|
658 |
|
|
659 |
lemma filterlim_Suc: "filterlim Suc sequentially sequentially"
|
|
660 |
by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq)
|
|
661 |
|
|
662 |
|
|
663 |
subsection {* Limits to @{const at_top} and @{const at_bot} *}
|
|
664 |
|
|
665 |
lemma filterlim_at_top:
|
|
666 |
fixes f :: "'a \<Rightarrow> ('b::linorder)"
|
|
667 |
shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z \<le> f x) F)"
|
|
668 |
by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_elim1)
|
|
669 |
|
|
670 |
lemma filterlim_at_top_mono:
|
|
671 |
"LIM x F. f x :> at_top \<Longrightarrow> eventually (\<lambda>x. f x \<le> (g x::'a::linorder)) F \<Longrightarrow>
|
|
672 |
LIM x F. g x :> at_top"
|
|
673 |
by (auto simp: filterlim_at_top elim: eventually_elim2 intro: order_trans)
|
|
674 |
|
|
675 |
lemma filterlim_at_top_dense:
|
|
676 |
fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)"
|
|
677 |
shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)"
|
|
678 |
by (metis eventually_elim1[of _ F] eventually_gt_at_top order_less_imp_le
|
|
679 |
filterlim_at_top[of f F] filterlim_iff[of f at_top F])
|
|
680 |
|
|
681 |
lemma filterlim_at_top_ge:
|
|
682 |
fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
|
|
683 |
shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z\<ge>c. eventually (\<lambda>x. Z \<le> f x) F)"
|
|
684 |
unfolding at_top_sub[of c] filterlim_INF by (auto simp add: filterlim_principal)
|
|
685 |
|
|
686 |
lemma filterlim_at_top_at_top:
|
|
687 |
fixes f :: "'a::linorder \<Rightarrow> 'b::linorder"
|
|
688 |
assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
|
|
689 |
assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
|
|
690 |
assumes Q: "eventually Q at_top"
|
|
691 |
assumes P: "eventually P at_top"
|
|
692 |
shows "filterlim f at_top at_top"
|
|
693 |
proof -
|
|
694 |
from P obtain x where x: "\<And>y. x \<le> y \<Longrightarrow> P y"
|
|
695 |
unfolding eventually_at_top_linorder by auto
|
|
696 |
show ?thesis
|
|
697 |
proof (intro filterlim_at_top_ge[THEN iffD2] allI impI)
|
|
698 |
fix z assume "x \<le> z"
|
|
699 |
with x have "P z" by auto
|
|
700 |
have "eventually (\<lambda>x. g z \<le> x) at_top"
|
|
701 |
by (rule eventually_ge_at_top)
|
|
702 |
with Q show "eventually (\<lambda>x. z \<le> f x) at_top"
|
|
703 |
by eventually_elim (metis mono bij `P z`)
|
|
704 |
qed
|
|
705 |
qed
|
|
706 |
|
|
707 |
lemma filterlim_at_top_gt:
|
|
708 |
fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
|
|
709 |
shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z>c. eventually (\<lambda>x. Z \<le> f x) F)"
|
|
710 |
by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge)
|
|
711 |
|
|
712 |
lemma filterlim_at_bot:
|
|
713 |
fixes f :: "'a \<Rightarrow> ('b::linorder)"
|
|
714 |
shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F)"
|
|
715 |
by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_elim1)
|
|
716 |
|
|
717 |
lemma filterlim_at_bot_dense:
|
|
718 |
fixes f :: "'a \<Rightarrow> ('b::{dense_linorder, no_bot})"
|
|
719 |
shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x < Z) F)"
|
|
720 |
proof (auto simp add: filterlim_at_bot[of f F])
|
|
721 |
fix Z :: 'b
|
|
722 |
from lt_ex [of Z] obtain Z' where 1: "Z' < Z" ..
|
|
723 |
assume "\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F"
|
|
724 |
hence "eventually (\<lambda>x. f x \<le> Z') F" by auto
|
|
725 |
thus "eventually (\<lambda>x. f x < Z) F"
|
|
726 |
apply (rule eventually_mono[rotated])
|
|
727 |
using 1 by auto
|
|
728 |
next
|
|
729 |
fix Z :: 'b
|
|
730 |
show "\<forall>Z. eventually (\<lambda>x. f x < Z) F \<Longrightarrow> eventually (\<lambda>x. f x \<le> Z) F"
|
|
731 |
by (drule spec [of _ Z], erule eventually_mono[rotated], auto simp add: less_imp_le)
|
|
732 |
qed
|
|
733 |
|
|
734 |
lemma filterlim_at_bot_le:
|
|
735 |
fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
|
|
736 |
shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F)"
|
|
737 |
unfolding filterlim_at_bot
|
|
738 |
proof safe
|
|
739 |
fix Z assume *: "\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F"
|
|
740 |
with *[THEN spec, of "min Z c"] show "eventually (\<lambda>x. Z \<ge> f x) F"
|
|
741 |
by (auto elim!: eventually_elim1)
|
|
742 |
qed simp
|
|
743 |
|
|
744 |
lemma filterlim_at_bot_lt:
|
|
745 |
fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
|
|
746 |
shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z \<ge> f x) F)"
|
|
747 |
by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
|
|
748 |
|
|
749 |
|
|
750 |
subsection {* Setup @{typ "'a filter"} for lifting and transfer *}
|
|
751 |
|
|
752 |
context begin interpretation lifting_syntax .
|
|
753 |
|
|
754 |
definition rel_filter :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> 'b filter \<Rightarrow> bool"
|
|
755 |
where "rel_filter R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)"
|
|
756 |
|
|
757 |
lemma rel_filter_eventually:
|
|
758 |
"rel_filter R F G \<longleftrightarrow>
|
|
759 |
((R ===> op =) ===> op =) (\<lambda>P. eventually P F) (\<lambda>P. eventually P G)"
|
|
760 |
by(simp add: rel_filter_def eventually_def)
|
|
761 |
|
|
762 |
lemma filtermap_id [simp, id_simps]: "filtermap id = id"
|
|
763 |
by(simp add: fun_eq_iff id_def filtermap_ident)
|
|
764 |
|
|
765 |
lemma filtermap_id' [simp]: "filtermap (\<lambda>x. x) = (\<lambda>F. F)"
|
|
766 |
using filtermap_id unfolding id_def .
|
|
767 |
|
|
768 |
lemma Quotient_filter [quot_map]:
|
|
769 |
assumes Q: "Quotient R Abs Rep T"
|
|
770 |
shows "Quotient (rel_filter R) (filtermap Abs) (filtermap Rep) (rel_filter T)"
|
|
771 |
unfolding Quotient_alt_def
|
|
772 |
proof(intro conjI strip)
|
|
773 |
from Q have *: "\<And>x y. T x y \<Longrightarrow> Abs x = y"
|
|
774 |
unfolding Quotient_alt_def by blast
|
|
775 |
|
|
776 |
fix F G
|
|
777 |
assume "rel_filter T F G"
|
|
778 |
thus "filtermap Abs F = G" unfolding filter_eq_iff
|
|
779 |
by(auto simp add: eventually_filtermap rel_filter_eventually * rel_funI del: iffI elim!: rel_funD)
|
|
780 |
next
|
|
781 |
from Q have *: "\<And>x. T (Rep x) x" unfolding Quotient_alt_def by blast
|
|
782 |
|
|
783 |
fix F
|
|
784 |
show "rel_filter T (filtermap Rep F) F"
|
|
785 |
by(auto elim: rel_funD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] rel_funI
|
|
786 |
del: iffI simp add: eventually_filtermap rel_filter_eventually)
|
|
787 |
qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff rel_filter_eventually
|
|
788 |
fun_quotient[OF fun_quotient[OF Q identity_quotient] identity_quotient, unfolded Quotient_alt_def])
|
|
789 |
|
|
790 |
lemma eventually_parametric [transfer_rule]:
|
|
791 |
"((A ===> op =) ===> rel_filter A ===> op =) eventually eventually"
|
|
792 |
by(simp add: rel_fun_def rel_filter_eventually)
|
|
793 |
|
|
794 |
lemma rel_filter_eq [relator_eq]: "rel_filter op = = op ="
|
|
795 |
by(auto simp add: rel_filter_eventually rel_fun_eq fun_eq_iff filter_eq_iff)
|
|
796 |
|
|
797 |
lemma rel_filter_mono [relator_mono]:
|
|
798 |
"A \<le> B \<Longrightarrow> rel_filter A \<le> rel_filter B"
|
|
799 |
unfolding rel_filter_eventually[abs_def]
|
|
800 |
by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl)
|
|
801 |
|
|
802 |
lemma rel_filter_conversep [simp]: "rel_filter A\<inverse>\<inverse> = (rel_filter A)\<inverse>\<inverse>"
|
|
803 |
by(auto simp add: rel_filter_eventually fun_eq_iff rel_fun_def)
|
|
804 |
|
|
805 |
lemma is_filter_parametric_aux:
|
|
806 |
assumes "is_filter F"
|
|
807 |
assumes [transfer_rule]: "bi_total A" "bi_unique A"
|
|
808 |
and [transfer_rule]: "((A ===> op =) ===> op =) F G"
|
|
809 |
shows "is_filter G"
|
|
810 |
proof -
|
|
811 |
interpret is_filter F by fact
|
|
812 |
show ?thesis
|
|
813 |
proof
|
|
814 |
have "F (\<lambda>_. True) = G (\<lambda>x. True)" by transfer_prover
|
|
815 |
thus "G (\<lambda>x. True)" by(simp add: True)
|
|
816 |
next
|
|
817 |
fix P' Q'
|
|
818 |
assume "G P'" "G Q'"
|
|
819 |
moreover
|
|
820 |
from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def]
|
|
821 |
obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast
|
|
822 |
have "F P = G P'" "F Q = G Q'" by transfer_prover+
|
|
823 |
ultimately have "F (\<lambda>x. P x \<and> Q x)" by(simp add: conj)
|
|
824 |
moreover have "F (\<lambda>x. P x \<and> Q x) = G (\<lambda>x. P' x \<and> Q' x)" by transfer_prover
|
|
825 |
ultimately show "G (\<lambda>x. P' x \<and> Q' x)" by simp
|
|
826 |
next
|
|
827 |
fix P' Q'
|
|
828 |
assume "\<forall>x. P' x \<longrightarrow> Q' x" "G P'"
|
|
829 |
moreover
|
|
830 |
from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def]
|
|
831 |
obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast
|
|
832 |
have "F P = G P'" by transfer_prover
|
|
833 |
moreover have "(\<forall>x. P x \<longrightarrow> Q x) \<longleftrightarrow> (\<forall>x. P' x \<longrightarrow> Q' x)" by transfer_prover
|
|
834 |
ultimately have "F Q" by(simp add: mono)
|
|
835 |
moreover have "F Q = G Q'" by transfer_prover
|
|
836 |
ultimately show "G Q'" by simp
|
|
837 |
qed
|
|
838 |
qed
|
|
839 |
|
|
840 |
lemma is_filter_parametric [transfer_rule]:
|
|
841 |
"\<lbrakk> bi_total A; bi_unique A \<rbrakk>
|
|
842 |
\<Longrightarrow> (((A ===> op =) ===> op =) ===> op =) is_filter is_filter"
|
|
843 |
apply(rule rel_funI)
|
|
844 |
apply(rule iffI)
|
|
845 |
apply(erule (3) is_filter_parametric_aux)
|
|
846 |
apply(erule is_filter_parametric_aux[where A="conversep A"])
|
|
847 |
apply(auto simp add: rel_fun_def)
|
|
848 |
done
|
|
849 |
|
|
850 |
lemma left_total_rel_filter [transfer_rule]:
|
|
851 |
assumes [transfer_rule]: "bi_total A" "bi_unique A"
|
|
852 |
shows "left_total (rel_filter A)"
|
|
853 |
proof(rule left_totalI)
|
|
854 |
fix F :: "'a filter"
|
|
855 |
from bi_total_fun[OF bi_unique_fun[OF `bi_total A` bi_unique_eq] bi_total_eq]
|
|
856 |
obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\<lambda>P. eventually P F) G"
|
|
857 |
unfolding bi_total_def by blast
|
|
858 |
moreover have "is_filter (\<lambda>P. eventually P F) \<longleftrightarrow> is_filter G" by transfer_prover
|
|
859 |
hence "is_filter G" by(simp add: eventually_def is_filter_Rep_filter)
|
|
860 |
ultimately have "rel_filter A F (Abs_filter G)"
|
|
861 |
by(simp add: rel_filter_eventually eventually_Abs_filter)
|
|
862 |
thus "\<exists>G. rel_filter A F G" ..
|
|
863 |
qed
|
|
864 |
|
|
865 |
lemma right_total_rel_filter [transfer_rule]:
|
|
866 |
"\<lbrakk> bi_total A; bi_unique A \<rbrakk> \<Longrightarrow> right_total (rel_filter A)"
|
|
867 |
using left_total_rel_filter[of "A\<inverse>\<inverse>"] by simp
|
|
868 |
|
|
869 |
lemma bi_total_rel_filter [transfer_rule]:
|
|
870 |
assumes "bi_total A" "bi_unique A"
|
|
871 |
shows "bi_total (rel_filter A)"
|
|
872 |
unfolding bi_total_alt_def using assms
|
|
873 |
by(simp add: left_total_rel_filter right_total_rel_filter)
|
|
874 |
|
|
875 |
lemma left_unique_rel_filter [transfer_rule]:
|
|
876 |
assumes "left_unique A"
|
|
877 |
shows "left_unique (rel_filter A)"
|
|
878 |
proof(rule left_uniqueI)
|
|
879 |
fix F F' G
|
|
880 |
assume [transfer_rule]: "rel_filter A F G" "rel_filter A F' G"
|
|
881 |
show "F = F'"
|
|
882 |
unfolding filter_eq_iff
|
|
883 |
proof
|
|
884 |
fix P :: "'a \<Rightarrow> bool"
|
|
885 |
obtain P' where [transfer_rule]: "(A ===> op =) P P'"
|
|
886 |
using left_total_fun[OF assms left_total_eq] unfolding left_total_def by blast
|
|
887 |
have "eventually P F = eventually P' G"
|
|
888 |
and "eventually P F' = eventually P' G" by transfer_prover+
|
|
889 |
thus "eventually P F = eventually P F'" by simp
|
|
890 |
qed
|
|
891 |
qed
|
|
892 |
|
|
893 |
lemma right_unique_rel_filter [transfer_rule]:
|
|
894 |
"right_unique A \<Longrightarrow> right_unique (rel_filter A)"
|
|
895 |
using left_unique_rel_filter[of "A\<inverse>\<inverse>"] by simp
|
|
896 |
|
|
897 |
lemma bi_unique_rel_filter [transfer_rule]:
|
|
898 |
"bi_unique A \<Longrightarrow> bi_unique (rel_filter A)"
|
|
899 |
by(simp add: bi_unique_alt_def left_unique_rel_filter right_unique_rel_filter)
|
|
900 |
|
|
901 |
lemma top_filter_parametric [transfer_rule]:
|
|
902 |
"bi_total A \<Longrightarrow> (rel_filter A) top top"
|
|
903 |
by(simp add: rel_filter_eventually All_transfer)
|
|
904 |
|
|
905 |
lemma bot_filter_parametric [transfer_rule]: "(rel_filter A) bot bot"
|
|
906 |
by(simp add: rel_filter_eventually rel_fun_def)
|
|
907 |
|
|
908 |
lemma sup_filter_parametric [transfer_rule]:
|
|
909 |
"(rel_filter A ===> rel_filter A ===> rel_filter A) sup sup"
|
|
910 |
by(fastforce simp add: rel_filter_eventually[abs_def] eventually_sup dest: rel_funD)
|
|
911 |
|
|
912 |
lemma Sup_filter_parametric [transfer_rule]:
|
|
913 |
"(rel_set (rel_filter A) ===> rel_filter A) Sup Sup"
|
|
914 |
proof(rule rel_funI)
|
|
915 |
fix S T
|
|
916 |
assume [transfer_rule]: "rel_set (rel_filter A) S T"
|
|
917 |
show "rel_filter A (Sup S) (Sup T)"
|
|
918 |
by(simp add: rel_filter_eventually eventually_Sup) transfer_prover
|
|
919 |
qed
|
|
920 |
|
|
921 |
lemma principal_parametric [transfer_rule]:
|
|
922 |
"(rel_set A ===> rel_filter A) principal principal"
|
|
923 |
proof(rule rel_funI)
|
|
924 |
fix S S'
|
|
925 |
assume [transfer_rule]: "rel_set A S S'"
|
|
926 |
show "rel_filter A (principal S) (principal S')"
|
|
927 |
by(simp add: rel_filter_eventually eventually_principal) transfer_prover
|
|
928 |
qed
|
|
929 |
|
|
930 |
context
|
|
931 |
fixes A :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
|
|
932 |
assumes [transfer_rule]: "bi_unique A"
|
|
933 |
begin
|
|
934 |
|
|
935 |
lemma le_filter_parametric [transfer_rule]:
|
|
936 |
"(rel_filter A ===> rel_filter A ===> op =) op \<le> op \<le>"
|
|
937 |
unfolding le_filter_def[abs_def] by transfer_prover
|
|
938 |
|
|
939 |
lemma less_filter_parametric [transfer_rule]:
|
|
940 |
"(rel_filter A ===> rel_filter A ===> op =) op < op <"
|
|
941 |
unfolding less_filter_def[abs_def] by transfer_prover
|
|
942 |
|
|
943 |
context
|
|
944 |
assumes [transfer_rule]: "bi_total A"
|
|
945 |
begin
|
|
946 |
|
|
947 |
lemma Inf_filter_parametric [transfer_rule]:
|
|
948 |
"(rel_set (rel_filter A) ===> rel_filter A) Inf Inf"
|
|
949 |
unfolding Inf_filter_def[abs_def] by transfer_prover
|
|
950 |
|
|
951 |
lemma inf_filter_parametric [transfer_rule]:
|
|
952 |
"(rel_filter A ===> rel_filter A ===> rel_filter A) inf inf"
|
|
953 |
proof(intro rel_funI)+
|
|
954 |
fix F F' G G'
|
|
955 |
assume [transfer_rule]: "rel_filter A F F'" "rel_filter A G G'"
|
|
956 |
have "rel_filter A (Inf {F, G}) (Inf {F', G'})" by transfer_prover
|
|
957 |
thus "rel_filter A (inf F G) (inf F' G')" by simp
|
|
958 |
qed
|
|
959 |
|
|
960 |
end
|
|
961 |
|
|
962 |
end
|
|
963 |
|
|
964 |
end
|
|
965 |
|
|
966 |
end |