src/HOL/Series.thy
changeset 44568 e6f291cb5810
parent 44289 d81d09cdab9c
child 44710 9caf6883f1f4
--- a/src/HOL/Series.thy	Sat Aug 27 17:26:14 2011 +0200
+++ b/src/HOL/Series.thy	Sun Aug 28 09:20:12 2011 -0700
@@ -183,12 +183,12 @@
     unfolding sums_def
     apply (rule LIMSEQ_offset[of _ n])
     unfolding setsum_const
-    apply (rule LIMSEQ_const)
+    apply (rule tendsto_const)
     done
 qed
 
 lemma sums_zero[simp, intro]: "(\<lambda>n. 0) sums 0"
-unfolding sums_def by (simp add: LIMSEQ_const)
+  unfolding sums_def by (simp add: tendsto_const)
 
 lemma summable_zero[simp, intro]: "summable (\<lambda>n. 0)"
 by (rule sums_zero [THEN sums_summable])
@@ -198,7 +198,7 @@
 
 lemma (in bounded_linear) sums:
   "(\<lambda>n. X n) sums a \<Longrightarrow> (\<lambda>n. f (X n)) sums (f a)"
-unfolding sums_def by (drule LIMSEQ, simp only: setsum)
+  unfolding sums_def by (drule tendsto, simp only: setsum)
 
 lemma (in bounded_linear) summable:
   "summable (\<lambda>n. X n) \<Longrightarrow> summable (\<lambda>n. f (X n))"
@@ -260,7 +260,7 @@
 lemma sums_add:
   fixes a b :: "'a::real_normed_field"
   shows "\<lbrakk>X sums a; Y sums b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) sums (a + b)"
-unfolding sums_def by (simp add: setsum_addf LIMSEQ_add)
+  unfolding sums_def by (simp add: setsum_addf tendsto_add)
 
 lemma summable_add:
   fixes X Y :: "nat \<Rightarrow> 'a::real_normed_field"
@@ -275,7 +275,7 @@
 lemma sums_diff:
   fixes X Y :: "nat \<Rightarrow> 'a::real_normed_field"
   shows "\<lbrakk>X sums a; Y sums b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n - Y n) sums (a - b)"
-unfolding sums_def by (simp add: setsum_subtractf LIMSEQ_diff)
+  unfolding sums_def by (simp add: setsum_subtractf tendsto_diff)
 
 lemma summable_diff:
   fixes X Y :: "nat \<Rightarrow> 'a::real_normed_field"
@@ -290,7 +290,7 @@
 lemma sums_minus:
   fixes X :: "nat \<Rightarrow> 'a::real_normed_field"
   shows "X sums a ==> (\<lambda>n. - X n) sums (- a)"
-unfolding sums_def by (simp add: setsum_negf LIMSEQ_minus)
+  unfolding sums_def by (simp add: setsum_negf tendsto_minus)
 
 lemma summable_minus:
   fixes X :: "nat \<Rightarrow> 'a::real_normed_field"
@@ -344,7 +344,7 @@
   shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 \<le> f m\<rbrakk> \<Longrightarrow> setsum f {0..<n} \<le> suminf f"
 apply (drule summable_sums)
 apply (simp add: sums_def)
-apply (cut_tac k = "setsum f {0..<n}" in LIMSEQ_const)
+apply (cut_tac k = "setsum f {0..<n}" in tendsto_const)
 apply (erule LIMSEQ_le, blast)
 apply (rule_tac x="n" in exI, clarify)
 apply (rule setsum_mono2)
@@ -403,7 +403,7 @@
   from less_1 have lim_0: "(\<lambda>n. x ^ n) ----> 0"
     by (rule LIMSEQ_power_zero)
   hence "(\<lambda>n. x ^ n / (x - 1) - 1 / (x - 1)) ----> 0 / (x - 1) - 1 / (x - 1)"
-    using neq_0 by (intro LIMSEQ_divide LIMSEQ_diff LIMSEQ_const)
+    using neq_0 by (intro tendsto_intros)
   hence "(\<lambda>n. (x ^ n - 1) / (x - 1)) ----> 1 / (1 - x)"
     by (simp add: nonzero_minus_divide_right [OF neq_0] diff_divide_distrib)
   thus "(\<lambda>n. x ^ n) sums (1 / (1 - x))"
@@ -583,7 +583,7 @@
 lemma summable_norm:
   fixes f :: "nat \<Rightarrow> 'a::banach"
   shows "summable (\<lambda>n. norm (f n)) \<Longrightarrow> norm (suminf f) \<le> (\<Sum>n. norm (f n))"
-by (auto intro: LIMSEQ_le LIMSEQ_norm summable_norm_cancel
+  by (auto intro: LIMSEQ_le tendsto_norm summable_norm_cancel
                 summable_sumr_LIMSEQ_suminf norm_setsum)
 
 lemma summable_rabs:
@@ -692,7 +692,7 @@
 
   have "(\<lambda>n. (\<Sum>k=0..<n. a k) * (\<Sum>k=0..<n. b k))
            ----> (\<Sum>k. a k) * (\<Sum>k. b k)"
-    by (intro LIMSEQ_mult summable_sumr_LIMSEQ_suminf
+    by (intro tendsto_mult summable_sumr_LIMSEQ_suminf
         summable_norm_cancel [OF a] summable_norm_cancel [OF b])
   hence 1: "(\<lambda>n. setsum ?g (?S1 n)) ----> (\<Sum>k. a k) * (\<Sum>k. b k)"
     by (simp only: setsum_product setsum_Sigma [rule_format]
@@ -700,7 +700,7 @@
 
   have "(\<lambda>n. (\<Sum>k=0..<n. norm (a k)) * (\<Sum>k=0..<n. norm (b k)))
        ----> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))"
-    using a b by (intro LIMSEQ_mult summable_sumr_LIMSEQ_suminf)
+    using a b by (intro tendsto_mult summable_sumr_LIMSEQ_suminf)
   hence "(\<lambda>n. setsum ?f (?S1 n)) ----> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))"
     by (simp only: setsum_product setsum_Sigma [rule_format]
                    finite_atLeastLessThan)