src/HOL/Limits.thy
changeset 57276 49c51eeaa623
parent 57275 0ddb5b755cdc
child 57447 87429bdecad5
     1.1 --- a/src/HOL/Limits.thy	Wed Jun 18 07:31:12 2014 +0200
     1.2 +++ b/src/HOL/Limits.thy	Wed Jun 18 14:31:32 2014 +0200
     1.3 @@ -3,7 +3,6 @@
     1.4      Author:     Jacques D. Fleuriot, University of Cambridge
     1.5      Author:     Lawrence C Paulson
     1.6      Author:     Jeremy Avigad
     1.7 -
     1.8  *)
     1.9  
    1.10  header {* Limits on Real Vector Spaces *}
    1.11 @@ -15,43 +14,27 @@
    1.12  subsection {* Filter going to infinity norm *}
    1.13  
    1.14  definition at_infinity :: "'a::real_normed_vector filter" where
    1.15 -  "at_infinity = Abs_filter (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)"
    1.16 +  "at_infinity = (INF r. principal {x. r \<le> norm x})"
    1.17  
    1.18 -lemma eventually_at_infinity:
    1.19 -  "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> P x)"
    1.20 -unfolding at_infinity_def
    1.21 -proof (rule eventually_Abs_filter, rule is_filter.intro)
    1.22 -  fix P Q :: "'a \<Rightarrow> bool"
    1.23 -  assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<exists>s. \<forall>x. s \<le> norm x \<longrightarrow> Q x"
    1.24 -  then obtain r s where
    1.25 -    "\<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<forall>x. s \<le> norm x \<longrightarrow> Q x" by auto
    1.26 -  then have "\<forall>x. max r s \<le> norm x \<longrightarrow> P x \<and> Q x" by simp
    1.27 -  then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x \<and> Q x" ..
    1.28 -qed auto
    1.29 +lemma eventually_at_infinity: "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> P x)"
    1.30 +  unfolding at_infinity_def
    1.31 +  by (subst eventually_INF_base)
    1.32 +     (auto simp: subset_eq eventually_principal intro!: exI[of _ "max a b" for a b])
    1.33  
    1.34  lemma at_infinity_eq_at_top_bot:
    1.35    "(at_infinity \<Colon> real filter) = sup at_top at_bot"
    1.36 -  unfolding sup_filter_def at_infinity_def eventually_at_top_linorder eventually_at_bot_linorder
    1.37 -proof (intro arg_cong[where f=Abs_filter] ext iffI)
    1.38 -  fix P :: "real \<Rightarrow> bool"
    1.39 -  assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
    1.40 -  then obtain r where "\<forall>x. r \<le> norm x \<longrightarrow> P x" ..
    1.41 -  then have "(\<forall>x\<ge>r. P x) \<and> (\<forall>x\<le>-r. P x)" by auto
    1.42 -  then show "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)" by auto
    1.43 -next
    1.44 -  fix P :: "real \<Rightarrow> bool"
    1.45 -  assume "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)"
    1.46 -  then obtain p q where "\<forall>x\<ge>p. P x" "\<forall>x\<le>q. P x" by auto
    1.47 -  then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
    1.48 -    by (intro exI[of _ "max p (-q)"]) (auto simp: abs_real_def)
    1.49 -qed
    1.50 +  apply (simp add: filter_eq_iff eventually_sup eventually_at_infinity
    1.51 +                   eventually_at_top_linorder eventually_at_bot_linorder)
    1.52 +  apply safe
    1.53 +  apply (rule_tac x="b" in exI, simp)
    1.54 +  apply (rule_tac x="- b" in exI, simp)
    1.55 +  apply (rule_tac x="max (- Na) N" in exI, auto simp: abs_real_def)
    1.56 +  done
    1.57  
    1.58 -lemma at_top_le_at_infinity:
    1.59 -  "at_top \<le> (at_infinity :: real filter)"
    1.60 +lemma at_top_le_at_infinity: "at_top \<le> (at_infinity :: real filter)"
    1.61    unfolding at_infinity_eq_at_top_bot by simp
    1.62  
    1.63 -lemma at_bot_le_at_infinity:
    1.64 -  "at_bot \<le> (at_infinity :: real filter)"
    1.65 +lemma at_bot_le_at_infinity: "at_bot \<le> (at_infinity :: real filter)"
    1.66    unfolding at_infinity_eq_at_top_bot by simp
    1.67  
    1.68  lemma filterlim_at_top_imp_at_infinity: