src/HOL/Series.thy
changeset 36657 f376af79f6b7
parent 36409 d323e7773aa8
child 36660 1cc4ab4b7ff7
--- a/src/HOL/Series.thy	Mon May 03 18:40:48 2010 -0700
+++ b/src/HOL/Series.thy	Mon May 03 20:42:58 2010 -0700
@@ -672,8 +672,8 @@
     by (rule convergentI)
   hence Cauchy: "Cauchy (\<lambda>n. setsum ?f (?S1 n))"
     by (rule convergent_Cauchy)
-  have "Zseq (\<lambda>n. setsum ?f (?S1 n - ?S2 n))"
-  proof (rule ZseqI, simp only: norm_setsum_f)
+  have "Zfun (\<lambda>n. setsum ?f (?S1 n - ?S2 n)) sequentially"
+  proof (rule ZfunI, simp only: eventually_sequentially norm_setsum_f)
     fix r :: real
     assume r: "0 < r"
     from CauchyD [OF Cauchy r] obtain N
@@ -694,14 +694,15 @@
       finally show "setsum ?f (?S1 n - ?S2 n) < r" .
     qed
   qed
-  hence "Zseq (\<lambda>n. setsum ?g (?S1 n - ?S2 n))"
-    apply (rule Zseq_le [rule_format])
+  hence "Zfun (\<lambda>n. setsum ?g (?S1 n - ?S2 n)) sequentially"
+    apply (rule Zfun_le [rule_format])
     apply (simp only: norm_setsum_f)
     apply (rule order_trans [OF norm_setsum setsum_mono])
     apply (auto simp add: norm_mult_ineq)
     done
   hence 2: "(\<lambda>n. setsum ?g (?S1 n) - setsum ?g (?S2 n)) ----> 0"
-    by (simp only: LIMSEQ_Zseq_iff setsum_diff finite_S1 S2_le_S1 diff_0_right)
+    unfolding LIMSEQ_conv_tendsto tendsto_Zfun_iff diff_0_right
+    by (simp only: setsum_diff finite_S1 S2_le_S1)
 
   with 1 have "(\<lambda>n. setsum ?g (?S2 n)) ----> (\<Sum>k. a k) * (\<Sum>k. b k)"
     by (rule LIMSEQ_diff_approach_zero2)