src/HOL/Analysis/Tagged_Division.thy

 qed auto
 
 lemma sum_sum_product:
   assumes "finite s"
     and "\<forall>i\<in>s. finite (t i)"
-  shows "setsum (\<lambda>i. setsum (x i) (t i)::real) s =
-    setsum (\<lambda>(i,j). x i j) {(i,j) | i j. i \<in> s \<and> j \<in> t i}"
+  shows "sum (\<lambda>i. sum (x i) (t i)::real) s =
+    sum (\<lambda>(i,j). x i j) {(i,j) | i j. i \<in> s \<and> j \<in> t i}"
   using assms
 proof induct
   case (insert a s)
   have *: "{(i, j) |i j. i \<in> insert a s \<and> j \<in> t i} =
     (\<lambda>y. (a,y)) ` (t a) \<union> {(i, j) |i j. i \<in> s \<and> j \<in> t i}" by auto
   show ?case
     unfolding *
-    apply (subst setsum.union_disjoint)
-    unfolding setsum.insert[OF insert(1-2)]
+    apply (subst sum.union_disjoint)
+    unfolding sum.insert[OF insert(1-2)]
     prefer 4
     apply (subst insert(3))
     unfolding add_right_cancel
   proof -
-    show "setsum (x a) (t a) = (\<Sum>(xa, y)\<in> Pair a ` t a. x xa y)"
-      apply (subst setsum.reindex)
+    show "sum (x a) (t a) = (\<Sum>(xa, y)\<in> Pair a ` t a. x xa y)"
+      apply (subst sum.reindex)
       unfolding inj_on_def
       apply auto
       done
     show "finite {(i, j) |i j. i \<in> s \<and> j \<in> t i}"
       apply (rule finite_product_dependent)

   where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
 
 lemma interval_upperbound[simp]:
   "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
     interval_upperbound (cbox a b) = (b::'a::euclidean_space)"
-  unfolding interval_upperbound_def euclidean_representation_setsum cbox_def
+  unfolding interval_upperbound_def euclidean_representation_sum cbox_def
   by (safe intro!: cSup_eq) auto
 
 lemma interval_lowerbound[simp]:
   "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
     interval_lowerbound (cbox a b) = (a::'a::euclidean_space)"
-  unfolding interval_lowerbound_def euclidean_representation_setsum cbox_def
+  unfolding interval_lowerbound_def euclidean_representation_sum cbox_def
   by (safe intro!: cInf_eq) auto
 
 lemmas interval_bounds = interval_upperbound interval_lowerbound
 
 lemma

       by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
   moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
   have "(\<Sum>i\<in>Basis. (SUP x:A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x:B. x \<bullet> i) *\<^sub>R i)"
       by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
   ultimately show ?thesis unfolding interval_upperbound_def
-      by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod)
+      by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
 qed
 
 lemma interval_lowerbound_Times:
   assumes "A \<noteq> {}" and "B \<noteq> {}"
   shows "interval_lowerbound (A \<times> B) = (interval_lowerbound A, interval_lowerbound B)"

       by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
   moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
   have "(\<Sum>i\<in>Basis. (INF x:A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x:B. x \<bullet> i) *\<^sub>R i)"
       by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
   ultimately show ?thesis unfolding interval_lowerbound_def
-      by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod)
+      by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
 qed
 
 subsection \<open>The notion of a gauge --- simply an open set containing the point.\<close>
 
 definition "gauge d \<longleftrightarrow> (\<forall>x. x \<in> d x \<and> open (d x))"

 
 lemma (in comm_monoid) operative_empty:
   assumes g: "operative g" shows "g {} = \<^bold>1"
 proof -
   have *: "cbox One (-One) = ({}::'b set)"
-    by (auto simp: box_eq_empty inner_setsum_left inner_Basis setsum.If_cases ex_in_conv)
+    by (auto simp: box_eq_empty inner_sum_left inner_Basis sum.If_cases ex_in_conv)
   moreover have "box One (-One) = ({}::'b set)"
     using box_subset_cbox[of One "-One"] by (auto simp: *)
   ultimately show ?thesis
     using operativeD(1)[OF g, of One "-One"] by simp
 qed

     unfolding *
     unfolding subset_eq
     apply rule
     unfolding mem_Collect_eq split_beta
     apply (erule bexE conjE)+
-    apply (simp only: mem_Collect_eq inner_setsum_left_Basis simp_thms)
+    apply (simp only: mem_Collect_eq inner_sum_left_Basis simp_thms)
     apply (erule exE conjE)+
   proof
     fix i l x
     assume as:
       "(if fst x = k then c else a \<bullet> fst x) < snd x" "snd x < b \<bullet> fst x"

 
 lemma additive_tagged_division_1:
   fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
   assumes "a \<le> b"
     and "p tagged_division_of {a..b}"
-  shows "setsum (\<lambda>(x,k). f(Sup k) - f(Inf k)) p = f b - f a"
+  shows "sum (\<lambda>(x,k). f(Sup k) - f(Inf k)) p = f b - f a"
 proof -
   let ?f = "(\<lambda>k::(real) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))"
   have ***: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
     using assms by auto
   have *: "add.operative ?f"
     unfolding add.operative_1_lt box_eq_empty
     by auto
   have **: "cbox a b \<noteq> {}"
     using assms(1) by auto
-  note setsum.operative_tagged_division[OF * assms(2)[simplified box_real[symmetric]]]
+  note sum.operative_tagged_division[OF * assms(2)[simplified box_real[symmetric]]]
   note * = this[unfolded if_not_P[OF **] interval_bounds[OF ***],symmetric]
   show ?thesis
     unfolding *
-    apply (rule setsum.cong)
+    apply (rule sum.cong)
     unfolding split_paired_all split_conv
     using assms(2)
     apply auto
     done
 qed

 
 lemma additive_tagged_division_1':
   fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
   assumes "a \<le> b"
     and "p tagged_division_of {a..b}"
-  shows "setsum (\<lambda>(x,k). f (Sup k) - f(Inf k)) p = f b - f a"
+  shows "sum (\<lambda>(x,k). f (Sup k) - f(Inf k)) p = f b - f a"
   using additive_tagged_division_1[OF _ assms(2), of f]
   using assms(1)
   by auto
 
 subsection \<open>Fine-ness of a partition w.r.t. a gauge.\<close>

 
   have interv: "\<exists>n. \<forall>x\<in>cbox (A n) (B n). \<forall>y\<in>cbox (A n) (B n). dist x y < e"
     if e: "0 < e" for e
   proof -
     obtain n where n: "(\<Sum>i\<in>Basis. b \<bullet> i - a \<bullet> i) / e < 2 ^ n"
-      using real_arch_pow[of 2 "(setsum (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis) / e"] by auto
+      using real_arch_pow[of 2 "(sum (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis) / e"] by auto
     show ?thesis
     proof (rule exI [where x=n], clarify)
       fix x y
       assume xy: "x\<in>cbox (A n) (B n)" "y\<in>cbox (A n) (B n)"
-      have "dist x y \<le> setsum (\<lambda>i. \<bar>(x - y)\<bullet>i\<bar>) Basis"
+      have "dist x y \<le> sum (\<lambda>i. \<bar>(x - y)\<bullet>i\<bar>) Basis"
         unfolding dist_norm by(rule norm_le_l1)
-      also have "\<dots> \<le> setsum (\<lambda>i. B n\<bullet>i - A n\<bullet>i) Basis"
-      proof (rule setsum_mono)
+      also have "\<dots> \<le> sum (\<lambda>i. B n\<bullet>i - A n\<bullet>i) Basis"
+      proof (rule sum_mono)
         fix i :: 'a
         assume i: "i \<in> Basis"
         show "\<bar>(x - y) \<bullet> i\<bar> \<le> B n \<bullet> i - A n \<bullet> i"
           using xy[unfolded mem_box,THEN bspec, OF i]
           by (auto simp: inner_diff_left)
       qed
-      also have "\<dots> \<le> setsum (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis / 2^n"
-        unfolding setsum_divide_distrib
-      proof (rule setsum_mono)
+      also have "\<dots> \<le> sum (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis / 2^n"
+        unfolding sum_divide_distrib
+      proof (rule sum_mono)
         show "B n \<bullet> i - A n \<bullet> i \<le> (b \<bullet> i - a \<bullet> i) / 2 ^ n" if i: "i \<in> Basis" for i
         proof (induct n)
           case 0
           then show ?case
             unfolding AB by auto

             using openE by blast
           have "norm (x - y) < \<epsilon>"
                if "(\<And>i. i \<in> Basis \<Longrightarrow> \<bar>x \<bullet> i - y \<bullet> i\<bar> \<le> \<epsilon> / (2 * real DIM('a)))" for y
           proof -
             have "norm (x - y) \<le> (\<Sum>i\<in>Basis. \<bar>x \<bullet> i - y \<bullet> i\<bar>)"
-              by (metis (no_types, lifting) inner_diff_left norm_le_l1 setsum.cong)
+              by (metis (no_types, lifting) inner_diff_left norm_le_l1 sum.cong)
             also have "... \<le> DIM('a) * (\<epsilon> / (2 * real DIM('a)))"
-              by (meson setsum_bounded_above that)
+              by (meson sum_bounded_above that)
             also have "... = \<epsilon> / 2"
               by (simp add: divide_simps)
             also have "... < \<epsilon>"
               by (simp add: \<open>0 < \<epsilon>\<close>)
             finally show ?thesis .