# HG changeset patch
# User huffman
# Date 1178986590 -7200
# Node ID bf718970e5ef068200e435fe8f2d0872c0fa4512
# Parent  314b45eb422d5cea183cb3af337bbe89702f483d
add lemma additive.setsum

diff -r 314b45eb422d -r bf718970e5ef src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Fri May 11 20:47:30 2007 +0200
+++ b/src/HOL/Real/RealVector.thy	Sat May 12 18:16:30 2007 +0200
@@ -32,6 +32,14 @@
 lemma (in additive) diff: "f (x - y) = f x - f y"
 by (simp add: diff_def add minus)
 
+lemma (in additive) setsum: "f (setsum g A) = (\<Sum>x\<in>A. f (g x))"
+apply (cases "finite A")
+apply (induct set: finite)
+apply (simp add: zero)
+apply (simp add: add)
+apply (simp add: zero)
+done
+
 
 subsection {* Real vector spaces *}