# HG changeset patch
# User huffman
# Date 1244846781 25200
# Node ID 2651f172c38bd77d8964601377297a32142f183f
# Parent  a7e187205fc01d10a3c838368ec1d9f99dfec2fd
add lemma tendsto_setsum

diff -r a7e187205fc0 -r 2651f172c38b src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Fri Jun 12 12:00:30 2009 -0700
+++ b/src/HOL/Limits.thy	Fri Jun 12 15:46:21 2009 -0700
@@ -471,6 +471,24 @@
   shows "\<lbrakk>(f ---> a) net; (g ---> b) net\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - g x) ---> a - b) net"
 by (simp add: diff_minus tendsto_add tendsto_minus)
 
+lemma tendsto_setsum [tendsto_intros]:
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector"
+  assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> a i) net"
+  shows "((\<lambda>x. \<Sum>i\<in>S. f i x) ---> (\<Sum>i\<in>S. a i)) net"
+proof (cases "finite S")
+  assume "finite S" thus ?thesis using assms
+  proof (induct set: finite)
+    case empty show ?case
+      by (simp add: tendsto_const)
+  next
+    case (insert i F) thus ?case
+      by (simp add: tendsto_add)
+  qed
+next
+  assume "\<not> finite S" thus ?thesis
+    by (simp add: tendsto_const)
+qed
+
 lemma (in bounded_linear) tendsto [tendsto_intros]:
   "(g ---> a) net \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) net"
 by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
diff -r a7e187205fc0 -r 2651f172c38b src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Fri Jun 12 12:00:30 2009 -0700
+++ b/src/HOL/SEQ.thy	Fri Jun 12 15:46:21 2009 -0700
@@ -348,23 +348,7 @@
   fixes L :: "'a \<Rightarrow> 'b::real_normed_vector"
   assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
   shows "(\<lambda>m. \<Sum>n\<in>S. X n m) ----> (\<Sum>n\<in>S. L n)"
-proof (cases "finite S")
-  case True
-  thus ?thesis using n
-  proof (induct)
-    case empty
-    show ?case
-      by (simp add: LIMSEQ_const)
-  next
-    case insert
-    thus ?case
-      by (simp add: LIMSEQ_add)
-  qed
-next
-  case False
-  thus ?thesis
-    by (simp add: LIMSEQ_const)
-qed
+using n unfolding LIMSEQ_conv_tendsto by (rule tendsto_setsum)
 
 lemma LIMSEQ_setprod:
   fixes L :: "'a \<Rightarrow> 'b::{real_normed_algebra,comm_ring_1}"