--- 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
--- 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>