src/HOL/Library/Set_Algebras.thy

--- a/src/HOL/Library/Set_Algebras.thy	Sun Oct 16 22:43:51 2016 +0200
+++ b/src/HOL/Library/Set_Algebras.thy	Mon Oct 17 11:46:22 2016 +0200
@@ -347,24 +347,24 @@
 lemma finite_set_times: "finite s \<Longrightarrow> finite t \<Longrightarrow> finite (s * t)"
   by (simp add: set_times_image)
 
-lemma set_setsum_alt:
+lemma set_sum_alt:
   assumes fin: "finite I"
-  shows "setsum S I = {setsum s I |s. \<forall>i\<in>I. s i \<in> S i}"
-    (is "_ = ?setsum I")
+  shows "sum S I = {sum s I |s. \<forall>i\<in>I. s i \<in> S i}"
+    (is "_ = ?sum I")
   using fin
 proof induct
   case empty
   then show ?case by simp
 next
   case (insert x F)
-  have "setsum S (insert x F) = S x + ?setsum F"
+  have "sum S (insert x F) = S x + ?sum F"
     using insert.hyps by auto
-  also have "\<dots> = {s x + setsum s F |s. \<forall> i\<in>insert x F. s i \<in> S i}"
+  also have "\<dots> = {s x + sum s F |s. \<forall> i\<in>insert x F. s i \<in> S i}"
     unfolding set_plus_def
   proof safe
     fix y s
     assume "y \<in> S x" "\<forall>i\<in>F. s i \<in> S i"
-    then show "\<exists>s'. y + setsum s F = s' x + setsum s' F \<and> (\<forall>i\<in>insert x F. s' i \<in> S i)"
+    then show "\<exists>s'. y + sum s F = s' x + sum s' F \<and> (\<forall>i\<in>insert x F. s' i \<in> S i)"
       using insert.hyps
       by (intro exI[of _ "\<lambda>i. if i \<in> F then s i else y"]) (auto simp add: set_plus_def)
   qed auto
@@ -372,12 +372,12 @@
     using insert.hyps by auto
 qed
 
-lemma setsum_set_cond_linear:
+lemma sum_set_cond_linear:
   fixes f :: "'a::comm_monoid_add set \<Rightarrow> 'b::comm_monoid_add set"
   assumes [intro!]: "\<And>A B. P A  \<Longrightarrow> P B  \<Longrightarrow> P (A + B)" "P {0}"
     and f: "\<And>A B. P A  \<Longrightarrow> P B \<Longrightarrow> f (A + B) = f A + f B" "f {0} = {0}"
   assumes all: "\<And>i. i \<in> I \<Longrightarrow> P (S i)"
-  shows "f (setsum S I) = setsum (f \<circ> S) I"
+  shows "f (sum S I) = sum (f \<circ> S) I"
 proof (cases "finite I")
   case True
   from this all show ?thesis
@@ -386,7 +386,7 @@
     then show ?case by (auto intro!: f)
   next
     case (insert x F)
-    from \<open>finite F\<close> \<open>\<And>i. i \<in> insert x F \<Longrightarrow> P (S i)\<close> have "P (setsum S F)"
+    from \<open>finite F\<close> \<open>\<And>i. i \<in> insert x F \<Longrightarrow> P (S i)\<close> have "P (sum S F)"
       by induct auto
     with insert show ?case
       by (simp, subst f) auto
@@ -396,11 +396,11 @@
   then show ?thesis by (auto intro!: f)
 qed
 
-lemma setsum_set_linear:
+lemma sum_set_linear:
   fixes f :: "'a::comm_monoid_add set \<Rightarrow> 'b::comm_monoid_add set"
   assumes "\<And>A B. f(A) + f(B) = f(A + B)" "f {0} = {0}"
-  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
+  shows "f (sum S I) = sum (f \<circ> S) I"
+  using sum_set_cond_linear[of "\<lambda>x. True" f I S] assms by auto
 
 lemma set_times_Un_distrib:
   "A * (B \<union> C) = A * B \<union> A * C"