src/HOL/Series.thy
changeset 44710 9caf6883f1f4
parent 44568 e6f291cb5810
child 44726 8478eab380e9
     1.1 --- a/src/HOL/Series.thy	Sun Sep 04 07:15:13 2011 -0700
     1.2 +++ b/src/HOL/Series.thy	Sun Sep 04 09:49:45 2011 -0700
     1.3 @@ -122,7 +122,7 @@
     1.4    shows "f sums s ==> (\<lambda>n. f(n + k)) sums (s - (SUM i = 0..< k. f i))"
     1.5    apply (unfold sums_def)
     1.6    apply (simp add: sumr_offset)
     1.7 -  apply (rule LIMSEQ_diff_const)
     1.8 +  apply (rule tendsto_diff [OF _ tendsto_const])
     1.9    apply (rule LIMSEQ_ignore_initial_segment)
    1.10    apply assumption
    1.11  done
    1.12 @@ -166,7 +166,7 @@
    1.13  proof -
    1.14    from sumSuc[unfolded sums_def]
    1.15    have "(\<lambda>i. \<Sum>n = Suc 0..<Suc i. f n) ----> l" unfolding setsum_reindex[OF inj_Suc] image_Suc_atLeastLessThan[symmetric] comp_def .
    1.16 -  from LIMSEQ_add_const[OF this, where b="f 0"]
    1.17 +  from tendsto_add[OF this tendsto_const, where b="f 0"]
    1.18    have "(\<lambda>i. \<Sum>n = 0..<Suc i. f n) ----> l + f 0" unfolding add_commute setsum_head_upt_Suc[OF zero_less_Suc] .
    1.19    thus ?thesis unfolding sums_def by (rule LIMSEQ_imp_Suc)
    1.20  qed
    1.21 @@ -625,7 +625,7 @@
    1.22   apply (simp add:diff_Suc split:nat.splits)
    1.23   apply (blast intro: norm_ratiotest_lemma)
    1.24  apply (rule_tac x = "Suc N" in exI, clarify)
    1.25 -apply(simp cong:setsum_ivl_cong)
    1.26 +apply(simp cong del: setsum_cong cong: setsum_ivl_cong)
    1.27  done
    1.28  
    1.29  lemma ratio_test: