# HG changeset patch
# User krauss
# Date 1334264111 -7200
# Node ID d21c95af2df776e6111f9fb864a8f9047b4cec0b
# Parent  aeff49a3369b85ed56c2da13840179bce0d3828f
removed "setsum_set", now subsumed by generic setsum

diff -r aeff49a3369b -r d21c95af2df7 src/HOL/Library/Set_Algebras.thy
--- a/src/HOL/Library/Set_Algebras.thy	Thu Apr 12 19:58:59 2012 +0200
+++ b/src/HOL/Library/Set_Algebras.thy	Thu Apr 12 22:55:11 2012 +0200
@@ -333,18 +333,13 @@
   fixes S T :: "'n::semigroup_add set" shows "S \<oplus> T = (\<lambda>(x, y). x + y) ` (S \<times> T)"
   unfolding set_plus_def by (fastforce simp: image_iff)
 
-text {* Legacy syntax: *}
-
-abbreviation (input) setsum_set :: "('b \<Rightarrow> ('a::comm_monoid_add) set) \<Rightarrow> 'b set \<Rightarrow> 'a set" where
-   "setsum_set == setsum"
-
 lemma set_setsum_alt:
   assumes fin: "finite I"
-  shows "setsum_set S I = {setsum s I |s. \<forall>i\<in>I. s i \<in> S i}"
+  shows "setsum S I = {setsum s I |s. \<forall>i\<in>I. s i \<in> S i}"
     (is "_ = ?setsum I")
 using fin proof induct
   case (insert x F)
-  have "setsum_set S (insert x F) = S x \<oplus> ?setsum F"
+  have "setsum S (insert x F) = S x \<oplus> ?setsum F"
     using insert.hyps by auto
   also have "...= {s x + setsum s F |s. \<forall> i\<in>insert x F. s i \<in> S i}"
     unfolding set_plus_def
@@ -363,12 +358,12 @@
   assumes [intro!]: "\<And>A B. P A  \<Longrightarrow> P B  \<Longrightarrow> P (A \<oplus> B)" "P {0}"
     and f: "\<And>A B. P A  \<Longrightarrow> P B \<Longrightarrow> f (A \<oplus> B) = f A \<oplus> f B" "f {0} = {0}"
   assumes all: "\<And>i. i \<in> I \<Longrightarrow> P (S i)"
-  shows "f (setsum_set S I) = setsum_set (f \<circ> S) I"
+  shows "f (setsum S I) = setsum (f \<circ> S) I"
 proof cases
   assume "finite I" from this all show ?thesis
   proof induct
     case (insert x F)
-    from `finite F` `\<And>i. i \<in> insert x F \<Longrightarrow> P (S i)` have "P (setsum_set S F)"
+    from `finite F` `\<And>i. i \<in> insert x F \<Longrightarrow> P (S i)` have "P (setsum S F)"
       by induct auto
     with insert show ?case
       by (simp, subst f) auto
@@ -378,7 +373,7 @@
 lemma setsum_set_linear:
   fixes f :: "('a::comm_monoid_add) set => ('b::comm_monoid_add) set"
   assumes "\<And>A B. f(A) \<oplus> f(B) = f(A \<oplus> B)" "f {0} = {0}"
-  shows "f (setsum_set S I) = setsum_set (f \<circ> S) I"
+  shows "f (setsum S I) = setsum (f \<circ> S) I"
   using setsum_set_cond_linear[of "\<lambda>x. True" f I S] assms by auto
 
 end
diff -r aeff49a3369b -r d21c95af2df7 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Apr 12 19:58:59 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Apr 12 22:55:11 2012 +0200
@@ -5479,7 +5479,7 @@
 lemma convex_sum_gen:
   fixes S :: "'a \<Rightarrow> 'n::euclidean_space set"
   assumes "\<And>i. i \<in> I \<Longrightarrow> (convex (S i))"
-  shows "convex (setsum_set S I)"
+  shows "convex (setsum S I)"
 proof cases
   assume "finite I" from this assms show ?thesis
     by induct (auto simp: convex_oplus)
@@ -5487,14 +5487,14 @@
 
 lemma convex_hull_sum_gen:
 fixes S :: "'a => ('n::euclidean_space) set"
-shows "convex hull (setsum_set S I) = setsum_set (%i. (convex hull (S i))) I"
+shows "convex hull (setsum S I) = setsum (%i. (convex hull (S i))) I"
 apply (subst setsum_set_linear) using convex_hull_sum convex_hull_singleton by auto
 
 
 lemma rel_interior_sum_gen:
 fixes S :: "'a => ('n::euclidean_space) set"
 assumes "!i:I. (convex (S i))"
-shows "rel_interior (setsum_set S I) = setsum_set (%i. (rel_interior (S i))) I"
+shows "rel_interior (setsum S I) = setsum (%i. (rel_interior (S i))) I"
 apply (subst setsum_set_cond_linear[of convex])
   using rel_interior_sum rel_interior_sing[of "0"] assms by (auto simp add: convex_oplus)
 
@@ -5513,7 +5513,7 @@
 lemma convex_hull_finite_union_cones:
 assumes "finite I" "I ~= {}"
 assumes "!i:I. (convex (S i) & cone (S i) & (S i) ~= {})"
-shows "convex hull (Union (S ` I)) = setsum_set S I"
+shows "convex hull (Union (S ` I)) = setsum S I"
   (is "?lhs = ?rhs")
 proof-
 { fix x assume "x : ?lhs"
@@ -5553,10 +5553,10 @@
 def A == "(%i. (if i=(1::nat) then S else T))"
 have "Union (A ` I) = S Un T" using A_def I_def by auto
 hence "convex hull (Union (A ` I)) = convex hull (S Un T)" by auto
-moreover have "convex hull Union (A ` I) = setsum_set A I"
+moreover have "convex hull Union (A ` I) = setsum A I"
     apply (subst convex_hull_finite_union_cones[of I A]) using assms A_def I_def by auto
 moreover have
-  "setsum_set A I = S \<oplus> T" using A_def I_def
+  "setsum A I = S \<oplus> T" using A_def I_def
      unfolding set_plus_def apply auto unfolding set_plus_def by auto
 ultimately show ?thesis by auto
 qed
@@ -5600,15 +5600,15 @@
   ultimately have "convex hull (Union (K ` I)) >= K0"
      unfolding K0_def using hull_minimal[of _ "convex hull (Union (K ` I))" "cone"] by blast
   hence "K0 = convex hull (Union (K ` I))" using geq by auto
-  also have "...=setsum_set K I"
+  also have "...=setsum K I"
      apply (subst convex_hull_finite_union_cones[of I K])
      using assms apply blast
      using `I ~= {}` apply blast
      unfolding K_def apply rule
      apply (subst convex_cone_hull) apply (subst convex_direct_sum)
      using assms cone_cone_hull `!i:I. K i ~= {}` K_def by auto
-  finally have "K0 = setsum_set K I" by auto
-  hence *: "rel_interior K0 = setsum_set (%i. (rel_interior (K i))) I"
+  finally have "K0 = setsum K I" by auto
+  hence *: "rel_interior K0 = setsum (%i. (rel_interior (K i))) I"
      using rel_interior_sum_gen[of I K] convK by auto
   { fix x assume "x : ?lhs"
     hence "((1::real),x) : rel_interior K0" using K0_def C0_def