src/HOL/SEQ.thy
changeset 50999 3de230ed0547
parent 50937 d249ef928ae1
child 51328 d63ec23c9125
     1.1 --- a/src/HOL/SEQ.thy	Thu Jan 31 11:31:22 2013 +0100
     1.2 +++ b/src/HOL/SEQ.thy	Thu Jan 31 11:31:27 2013 +0100
     1.3 @@ -368,19 +368,16 @@
     1.4        and bdd: "\<And>n. f n \<le> l"
     1.5        and en: "\<And>e. 0 < e \<Longrightarrow> \<exists>n. l \<le> f n + e"
     1.6    shows "f ----> l"
     1.7 -  unfolding LIMSEQ_def
     1.8 -proof safe
     1.9 -  fix r :: real assume "0 < r"
    1.10 -  with bdd en[of "r / 2"] obtain n where n: "dist (f n) l \<le> r / 2"
    1.11 -    by (auto simp add: field_simps dist_real_def)
    1.12 -  { fix N assume "n \<le> N"
    1.13 -    then have "dist (f N) l \<le> dist (f n) l"
    1.14 -      using incseq_SucI[of f] inc bdd by (auto dest!: incseqD simp: dist_real_def)
    1.15 -    then have "dist (f N) l < r"
    1.16 -      using `0 < r` n by simp }
    1.17 -  with `0 < r` show "\<exists>no. \<forall>n\<ge>no. dist (f n) l < r"
    1.18 -    by (auto simp add: LIMSEQ_def field_simps intro!: exI[of _ n])
    1.19 -qed
    1.20 +proof (rule increasing_tendsto)
    1.21 +  fix x assume "x < l"
    1.22 +  with dense[of 0 "l - x"] obtain e where "0 < e" "e < l - x"
    1.23 +    by auto
    1.24 +  from en[OF `0 < e`] obtain n where "l - e \<le> f n"
    1.25 +    by (auto simp: field_simps)
    1.26 +  with `e < l - x` `0 < e` have "x < f n" by simp
    1.27 +  with incseq_SucI[of f, OF inc] show "eventually (\<lambda>n. x < f n) sequentially"
    1.28 +    by (auto simp: eventually_sequentially incseq_def intro: less_le_trans)
    1.29 +qed (insert bdd, auto)
    1.30  
    1.31  lemma Bseq_inverse_lemma:
    1.32    fixes x :: "'a::real_normed_div_algebra"
    1.33 @@ -437,15 +434,15 @@
    1.34    by auto
    1.35  
    1.36  lemma LIMSEQ_le_const:
    1.37 -  "\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x"
    1.38 +  "\<lbrakk>X ----> (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x"
    1.39    using tendsto_le_const[of sequentially X x a] by (simp add: eventually_sequentially)
    1.40  
    1.41  lemma LIMSEQ_le:
    1.42 -  "\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::real)"
    1.43 +  "\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::'a::linorder_topology)"
    1.44    using tendsto_le[of sequentially Y y X x] by (simp add: eventually_sequentially)
    1.45  
    1.46  lemma LIMSEQ_le_const2:
    1.47 -  "\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a"
    1.48 +  "\<lbrakk>X ----> (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a"
    1.49    by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) (auto simp: tendsto_const)
    1.50  
    1.51  subsection {* Convergence *}