# HG changeset patch
# User huffman
# Date 1272724522 25200
# Node ID 39b2516a197028f4d7c953e260bd3a8476231bc2
# Parent  72d2cb5c3db96d2aaa7d713ece0e986b5a811285
move setsum lemmas to Product_plus.thy

diff -r 72d2cb5c3db9 -r 39b2516a1970 src/HOL/Library/Product_plus.thy
--- a/src/HOL/Library/Product_plus.thy	Fri Apr 30 13:51:17 2010 -0700
+++ b/src/HOL/Library/Product_plus.thy	Sat May 01 07:35:22 2010 -0700
@@ -112,4 +112,10 @@
 instance "*" :: (ab_group_add, ab_group_add) ab_group_add
   by default (simp_all add: expand_prod_eq)
 
+lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
+by (cases "finite A", induct set: finite, simp_all)
+
+lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
+by (cases "finite A", induct set: finite, simp_all)
+
 end
diff -r 72d2cb5c3db9 -r 39b2516a1970 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Apr 30 13:51:17 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat May 01 07:35:22 2010 -0700
@@ -2205,14 +2205,6 @@
 
 subsection {* Use this to derive general bound property of convex function. *}
 
-(* TODO: move *)
-lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
-by (cases "finite A", induct set: finite, simp_all)
-
-(* TODO: move *)
-lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
-by (cases "finite A", induct set: finite, simp_all)
-
 lemma convex_on:
   assumes "convex s"
   shows "convex_on s f \<longleftrightarrow> (\<forall>k u x. (\<forall>i\<in>{1..k::nat}. 0 \<le> u i \<and> x i \<in> s) \<and> setsum u {1..k} = 1 \<longrightarrow>