214 |
214 |
215 lemma eventually_False: |
215 lemma eventually_False: |
216 "eventually (\<lambda>x. False) F \<longleftrightarrow> F = bot" |
216 "eventually (\<lambda>x. False) F \<longleftrightarrow> F = bot" |
217 unfolding filter_eq_iff by (auto elim: eventually_rev_mp) |
217 unfolding filter_eq_iff by (auto elim: eventually_rev_mp) |
218 |
218 |
|
219 abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool" |
|
220 where "trivial_limit F \<equiv> F = bot" |
|
221 |
|
222 lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F" |
|
223 by (rule eventually_False [symmetric]) |
|
224 |
|
225 |
219 subsection {* Map function for filters *} |
226 subsection {* Map function for filters *} |
220 |
227 |
221 definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter" |
228 definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter" |
222 where "filtermap f F = Abs_filter (\<lambda>P. eventually (\<lambda>x. P (f x)) F)" |
229 where "filtermap f F = Abs_filter (\<lambda>P. eventually (\<lambda>x. P (f x)) F)" |
223 |
230 |
257 then obtain i j where "\<forall>n\<ge>i. P n" and "\<forall>n\<ge>j. Q n" by auto |
264 then obtain i j where "\<forall>n\<ge>i. P n" and "\<forall>n\<ge>j. Q n" by auto |
258 then have "\<forall>n\<ge>max i j. P n \<and> Q n" by simp |
265 then have "\<forall>n\<ge>max i j. P n \<and> Q n" by simp |
259 then show "\<exists>k. \<forall>n\<ge>k. P n \<and> Q n" .. |
266 then show "\<exists>k. \<forall>n\<ge>k. P n \<and> Q n" .. |
260 qed auto |
267 qed auto |
261 |
268 |
262 lemma sequentially_bot [simp]: "sequentially \<noteq> bot" |
269 lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot" |
263 unfolding filter_eq_iff eventually_sequentially by auto |
270 unfolding filter_eq_iff eventually_sequentially by auto |
|
271 |
|
272 lemmas trivial_limit_sequentially = sequentially_bot |
264 |
273 |
265 lemma eventually_False_sequentially [simp]: |
274 lemma eventually_False_sequentially [simp]: |
266 "\<not> eventually (\<lambda>n. False) sequentially" |
275 "\<not> eventually (\<lambda>n. False) sequentially" |
267 by (simp add: eventually_False) |
276 by (simp add: eventually_False) |
268 |
277 |
269 lemma le_sequentially: |
278 lemma le_sequentially: |
270 "F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)" |
279 "F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)" |
271 unfolding le_filter_def eventually_sequentially |
280 unfolding le_filter_def eventually_sequentially |
272 by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp) |
281 by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp) |
273 |
282 |
274 |
|
275 definition trivial_limit :: "'a filter \<Rightarrow> bool" |
|
276 where "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F" |
|
277 |
|
278 lemma trivial_limit_sequentially [intro]: "\<not> trivial_limit sequentially" |
|
279 by (auto simp add: trivial_limit_def eventually_sequentially) |
|
280 |
283 |
281 subsection {* Standard filters *} |
284 subsection {* Standard filters *} |
282 |
285 |
283 definition within :: "'a filter \<Rightarrow> 'a set \<Rightarrow> 'a filter" (infixr "within" 70) |
286 definition within :: "'a filter \<Rightarrow> 'a set \<Rightarrow> 'a filter" (infixr "within" 70) |
284 where "F within S = Abs_filter (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) F)" |
287 where "F within S = Abs_filter (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) F)" |