src/HOL/Limits.thy
changeset 44342 8321948340ea
parent 44282 f0de18b62d63
child 44568 e6f291cb5810
equal deleted inserted replaced
44320:33439faadd67 44342:8321948340ea
   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)"