# HG changeset patch
# User huffman
# Date 1180453024 -7200
# Node ID 0082459a255b50adb13071c90f5d0502c296d00e
# Parent  ce3cf072ae14e89d89870736925e49d547dfbc62
add bounded_linear lemmas

diff -r ce3cf072ae14 -r 0082459a255b src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Tue May 29 17:36:35 2007 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Tue May 29 17:37:04 2007 +0200
@@ -164,6 +164,18 @@
   apply (rule sums_zero);
 done;
   
+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)
+
+lemma (in bounded_linear) summable:
+  "summable (\<lambda>n. X n) \<Longrightarrow> summable (\<lambda>n. f (X n))"
+unfolding summable_def by (auto intro: sums)
+
+lemma (in bounded_linear) suminf:
+  "summable (\<lambda>n. X n) \<Longrightarrow> f (\<Sum>n. X n) = (\<Sum>n. f (X n))"
+by (rule summable_sums [THEN sums, THEN sums_unique])
+
 lemma sums_mult:
   fixes c :: "'a::real_normed_algebra"
   shows "f sums a \<Longrightarrow> (\<lambda>n. c * f n) sums (c * a)"