src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
changeset 64267 b9a1486e79be
parent 63957 c3da799b1b45
child 64272 f76b6dda2e56
     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Oct 16 22:43:51 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Oct 17 11:46:22 2016 +0200
     1.3 @@ -176,11 +176,11 @@
     1.4    unfolding forall_in_division[OF assms(2)]
     1.5    by (metis antisym_conv assms content_pos_le content_subset division_ofD(2))
     1.6  
     1.7 -lemma setsum_content_null:
     1.8 +lemma sum_content_null:
     1.9    assumes "content (cbox a b) = 0"
    1.10      and "p tagged_division_of (cbox a b)"
    1.11 -  shows "setsum (\<lambda>(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)"
    1.12 -proof (rule setsum.neutral, rule)
    1.13 +  shows "sum (\<lambda>(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)"
    1.14 +proof (rule sum.neutral, rule)
    1.15    fix y
    1.16    assume y: "y \<in> p"
    1.17    obtain x k where xk: "y = (x, k)"
    1.18 @@ -199,12 +199,12 @@
    1.19  lemma operative_content[intro]: "add.operative content"
    1.20    by (force simp add: add.operative_def content_split[symmetric] content_eq_0_interior)
    1.21  
    1.22 -lemma additive_content_division: "d division_of (cbox a b) \<Longrightarrow> setsum content d = content (cbox a b)"
    1.23 -  by (metis operative_content setsum.operative_division)
    1.24 +lemma additive_content_division: "d division_of (cbox a b) \<Longrightarrow> sum content d = content (cbox a b)"
    1.25 +  by (metis operative_content sum.operative_division)
    1.26  
    1.27  lemma additive_content_tagged_division:
    1.28 -  "d tagged_division_of (cbox a b) \<Longrightarrow> setsum (\<lambda>(x,l). content l) d = content (cbox a b)"
    1.29 -  unfolding setsum.operative_tagged_division[OF operative_content, symmetric] by blast
    1.30 +  "d tagged_division_of (cbox a b) \<Longrightarrow> sum (\<lambda>(x,l). content l) d = content (cbox a b)"
    1.31 +  unfolding sum.operative_tagged_division[OF operative_content, symmetric] by blast
    1.32  
    1.33  lemma content_real_eq_0: "content {a .. b::real} = 0 \<longleftrightarrow> a \<ge> b"
    1.34    by (metis atLeastatMost_empty_iff2 content_empty content_real diff_self eq_iff le_cases le_iff_diff_le_0)
    1.35 @@ -234,14 +234,14 @@
    1.36    "(f has_integral y) (cbox a b) \<longleftrightarrow>
    1.37      (\<forall>e>0. \<exists>d. gauge d \<and>
    1.38        (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
    1.39 -        norm (setsum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))"
    1.40 +        norm (sum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))"
    1.41    by (auto simp: dist_norm eventually_division_filter has_integral_def tendsto_iff)
    1.42  
    1.43  lemma has_integral_real:
    1.44    "(f has_integral y) {a .. b::real} \<longleftrightarrow>
    1.45      (\<forall>e>0. \<exists>d. gauge d \<and>
    1.46        (\<forall>p. p tagged_division_of {a .. b} \<and> d fine p \<longrightarrow>
    1.47 -        norm (setsum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))"
    1.48 +        norm (sum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))"
    1.49    unfolding box_real[symmetric]
    1.50    by (rule has_integral)
    1.51  
    1.52 @@ -364,7 +364,7 @@
    1.53    shows "((\<lambda>x. c) has_integral (content (cbox a b) *\<^sub>R c)) (cbox a b)"
    1.54    using eventually_division_filter_tagged_division[of "cbox a b"]
    1.55       additive_content_tagged_division[of _ a b]
    1.56 -  by (auto simp: has_integral_cbox split_beta' scaleR_setsum_left[symmetric]
    1.57 +  by (auto simp: has_integral_cbox split_beta' scaleR_sum_left[symmetric]
    1.58             elim!: eventually_mono intro!: tendsto_cong[THEN iffD1, OF _ tendsto_const])
    1.59  
    1.60  lemma has_integral_const_real [intro]:
    1.61 @@ -391,7 +391,7 @@
    1.62      unfolding has_integral_cbox
    1.63      using eventually_division_filter_tagged_division[of "cbox a b"]
    1.64      by (subst tendsto_cong[where g="\<lambda>_. 0"])
    1.65 -       (auto elim!: eventually_mono intro!: setsum.neutral simp: tag_in_interval)
    1.66 +       (auto elim!: eventually_mono intro!: sum.neutral simp: tag_in_interval)
    1.67    {
    1.68      presume "\<not> (\<exists>a b. s = cbox a b) \<Longrightarrow> ?thesis"
    1.69      with assms lem show ?thesis
    1.70 @@ -425,7 +425,7 @@
    1.71    from pos_bounded obtain B where B: "0 < B" "\<And>x. norm (h x) \<le> norm x * B"
    1.72      by blast
    1.73    have lem: "\<And>a b y f::'n\<Rightarrow>'a. (f has_integral y) (cbox a b) \<Longrightarrow> ((h \<circ> f) has_integral h y) (cbox a b)"
    1.74 -    unfolding has_integral_cbox by (drule tendsto) (simp add: setsum scaleR split_beta')
    1.75 +    unfolding has_integral_cbox by (drule tendsto) (simp add: sum scaleR split_beta')
    1.76    {
    1.77      presume "\<not> (\<exists>a b. s = cbox a b) \<Longrightarrow> ?thesis"
    1.78      then show ?thesis
    1.79 @@ -531,7 +531,7 @@
    1.80      ((\<lambda>x. f x + g x) has_integral (k + l)) (cbox a b)"
    1.81      for f :: "'n \<Rightarrow> 'a" and g a b k l
    1.82      unfolding has_integral_cbox
    1.83 -    by (simp add: split_beta' scaleR_add_right setsum.distrib[abs_def] tendsto_add)
    1.84 +    by (simp add: split_beta' scaleR_add_right sum.distrib[abs_def] tendsto_add)
    1.85    {
    1.86      presume "\<not> (\<exists>a b. s = cbox a b) \<Longrightarrow> ?thesis"
    1.87      then show ?thesis
    1.88 @@ -666,10 +666,10 @@
    1.89    shows "integral s (\<lambda>x. f x \<bullet> k) = integral s f \<bullet> k"
    1.90    unfolding integral_linear[OF assms(1) bounded_linear_inner_left,unfolded o_def] ..
    1.91  
    1.92 -lemma has_integral_setsum:
    1.93 +lemma has_integral_sum:
    1.94    assumes "finite t"
    1.95      and "\<forall>a\<in>t. ((f a) has_integral (i a)) s"
    1.96 -  shows "((\<lambda>x. setsum (\<lambda>a. f a x) t) has_integral (setsum i t)) s"
    1.97 +  shows "((\<lambda>x. sum (\<lambda>a. f a x) t) has_integral (sum i t)) s"
    1.98    using assms(1) subset_refl[of t]
    1.99  proof (induct rule: finite_subset_induct)
   1.100    case empty
   1.101 @@ -680,16 +680,16 @@
   1.102      by (simp add: has_integral_add)
   1.103  qed
   1.104  
   1.105 -lemma integral_setsum:
   1.106 +lemma integral_sum:
   1.107    "\<lbrakk>finite t;  \<forall>a\<in>t. (f a) integrable_on s\<rbrakk> \<Longrightarrow>
   1.108 -   integral s (\<lambda>x. setsum (\<lambda>a. f a x) t) = setsum (\<lambda>a. integral s (f a)) t"
   1.109 -  by (auto intro: has_integral_setsum integrable_integral)
   1.110 -
   1.111 -lemma integrable_setsum:
   1.112 -  "\<lbrakk>finite t;  \<forall>a\<in>t. (f a) integrable_on s\<rbrakk> \<Longrightarrow> (\<lambda>x. setsum (\<lambda>a. f a x) t) integrable_on s"
   1.113 +   integral s (\<lambda>x. sum (\<lambda>a. f a x) t) = sum (\<lambda>a. integral s (f a)) t"
   1.114 +  by (auto intro: has_integral_sum integrable_integral)
   1.115 +
   1.116 +lemma integrable_sum:
   1.117 +  "\<lbrakk>finite t;  \<forall>a\<in>t. (f a) integrable_on s\<rbrakk> \<Longrightarrow> (\<lambda>x. sum (\<lambda>a. f a x) t) integrable_on s"
   1.118    unfolding integrable_on_def
   1.119    apply (drule bchoice)
   1.120 -  using has_integral_setsum[of t]
   1.121 +  using has_integral_sum[of t]
   1.122    apply auto
   1.123    done
   1.124  
   1.125 @@ -760,7 +760,7 @@
   1.126  lemma has_integral_null [intro]: "content(cbox a b) = 0 \<Longrightarrow> (f has_integral 0) (cbox a b)"
   1.127    unfolding has_integral_cbox
   1.128    using eventually_division_filter_tagged_division[of "cbox a b"]
   1.129 -  by (subst tendsto_cong[where g="\<lambda>_. 0"]) (auto elim: eventually_mono intro: setsum_content_null)
   1.130 +  by (subst tendsto_cong[where g="\<lambda>_. 0"]) (auto elim: eventually_mono intro: sum_content_null)
   1.131  
   1.132  lemma has_integral_null_real [intro]: "content {a .. b::real} = 0 \<Longrightarrow> (f has_integral 0) {a .. b}"
   1.133    by (metis box_real(2) has_integral_null)
   1.134 @@ -840,7 +840,7 @@
   1.135    hence "\<forall>b\<in>Basis. (((\<lambda>x. x *\<^sub>R b) \<circ> (\<lambda>x. f x \<bullet> b)) has_integral ((y \<bullet> b) *\<^sub>R b)) A"
   1.136      by (intro ballI has_integral_linear) (simp_all add: bounded_linear_scaleR_left)
   1.137    hence "((\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) has_integral (\<Sum>b\<in>Basis. (y \<bullet> b) *\<^sub>R b)) A"
   1.138 -    by (intro has_integral_setsum) (simp_all add: o_def)
   1.139 +    by (intro has_integral_sum) (simp_all add: o_def)
   1.140    thus "(f has_integral y) A" by (simp add: euclidean_representation)
   1.141  qed
   1.142  
   1.143 @@ -865,7 +865,7 @@
   1.144    hence "\<forall>b\<in>Basis. (((\<lambda>x. x *\<^sub>R b) \<circ> (\<lambda>x. f x \<bullet> b)) has_integral (y b *\<^sub>R b)) A"
   1.145      by (intro ballI has_integral_linear) (simp_all add: bounded_linear_scaleR_left)
   1.146    hence "((\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) has_integral (\<Sum>b\<in>Basis. y b *\<^sub>R b)) A"
   1.147 -    by (intro has_integral_setsum) (simp_all add: o_def)
   1.148 +    by (intro has_integral_sum) (simp_all add: o_def)
   1.149    thus "f integrable_on A" by (auto simp: integrable_on_def o_def euclidean_representation)
   1.150  qed
   1.151  
   1.152 @@ -885,7 +885,7 @@
   1.153    have "integral A f = integral A (\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b)"
   1.154      by (simp add: euclidean_representation)
   1.155    also from integrable have "\<dots> = (\<Sum>a\<in>Basis. integral A (\<lambda>x. (f x \<bullet> a) *\<^sub>R a))"
   1.156 -    by (subst integral_setsum) (simp_all add: o_def)
   1.157 +    by (subst integral_sum) (simp_all add: o_def)
   1.158    finally show ?thesis .
   1.159  qed
   1.160  
   1.161 @@ -944,7 +944,7 @@
   1.162    from choice[OF this] guess p .. note p = conjunctD2[OF this[rule_format]]
   1.163    have dp: "\<And>i n. i\<le>n \<Longrightarrow> d i fine p n"
   1.164      using p(2) unfolding fine_inters by auto
   1.165 -  have "Cauchy (\<lambda>n. setsum (\<lambda>(x,k). content k *\<^sub>R (f x)) (p n))"
   1.166 +  have "Cauchy (\<lambda>n. sum (\<lambda>(x,k). content k *\<^sub>R (f x)) (p n))"
   1.167    proof (rule CauchyI, goal_cases)
   1.168      case (1 e)
   1.169      then guess N unfolding real_arch_inverse[of e] .. note N=this
   1.170 @@ -1124,9 +1124,9 @@
   1.171          unfolding xk split_conv by auto
   1.172      } note [simp] = this
   1.173      have lem3: "\<And>g :: 'a set \<Rightarrow> 'a set. finite p \<Longrightarrow>
   1.174 -                  setsum (\<lambda>(x, k). content k *\<^sub>R f x) {(x,g k) |x k. (x,k) \<in> p \<and> g k \<noteq> {}} =
   1.175 -                  setsum (\<lambda>(x, k). content k *\<^sub>R f x) ((\<lambda>(x, k). (x, g k)) ` p)"
   1.176 -      by (rule setsum.mono_neutral_left) auto
   1.177 +                  sum (\<lambda>(x, k). content k *\<^sub>R f x) {(x,g k) |x k. (x,k) \<in> p \<and> g k \<noteq> {}} =
   1.178 +                  sum (\<lambda>(x, k). content k *\<^sub>R f x) ((\<lambda>(x, k). (x, g k)) ` p)"
   1.179 +      by (rule sum.mono_neutral_left) auto
   1.180      let ?M1 = "{(x, kk \<inter> {x. x\<bullet>k \<le> c}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}"
   1.181      have d1_fine: "d1 fine ?M1"
   1.182        by (force intro: fineI dest: fineD[OF p(2)] simp add: split: if_split_asm)
   1.183 @@ -1218,10 +1218,10 @@
   1.184        also have "\<dots> = (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f x) +
   1.185          (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f x) - (i + j)"
   1.186          unfolding lem3[OF p(3)]
   1.187 -        by (subst (1 2) setsum.reindex_nontrivial[OF p(3)])
   1.188 +        by (subst (1 2) sum.reindex_nontrivial[OF p(3)])
   1.189             (auto intro!: k eq0 tagged_division_split_left_inj_content[OF p(1)] tagged_division_split_right_inj_content[OF p(1)]
   1.190                   simp: cont_eq)+
   1.191 -      also note setsum.distrib[symmetric]
   1.192 +      also note sum.distrib[symmetric]
   1.193        also have "\<And>x. x \<in> p \<Longrightarrow>
   1.194                      (\<lambda>(x,ka). content (ka \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f x) x +
   1.195                      (\<lambda>(x,ka). content (ka \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f x) x =
   1.196 @@ -1236,7 +1236,7 @@
   1.197            unfolding uv content_split[OF k,of u v c]
   1.198            by auto
   1.199        qed
   1.200 -      note setsum.cong [OF _ this]
   1.201 +      note sum.cong [OF _ this]
   1.202        finally have "(\<Sum>(x, k)\<in>{(x, kk \<inter> {x. x \<bullet> k \<le> c}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. x \<bullet> k \<le> c} \<noteq> {}}. content k *\<^sub>R f x) - i +
   1.203          ((\<Sum>(x, k)\<in>{(x, kk \<inter> {x. c \<le> x \<bullet> k}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. c \<le> x \<bullet> k} \<noteq> {}}. content k *\<^sub>R f x) - j) =
   1.204          (\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f x) - (i + j)"
   1.205 @@ -1258,7 +1258,7 @@
   1.206    obtains d where "gauge d"
   1.207      "\<forall>p1 p2. p1 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<and> d fine p1 \<and>
   1.208          p2 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c}) \<and> d fine p2 \<longrightarrow>
   1.209 -        norm ((setsum (\<lambda>(x,k). content k *\<^sub>R f x) p1 + setsum (\<lambda>(x,k). content k *\<^sub>R f x) p2) - i) < e"
   1.210 +        norm ((sum (\<lambda>(x,k). content k *\<^sub>R f x) p1 + sum (\<lambda>(x,k). content k *\<^sub>R f x) p2) - i) < e"
   1.211  proof -
   1.212    guess d using has_integralD[OF assms(1-2)] . note d=this
   1.213    { fix p1 p2
   1.214 @@ -1287,9 +1287,9 @@
   1.215            using e k by (auto simp: inner_simps inner_not_same_Basis)
   1.216          have "(\<Sum>i\<in>Basis. \<bar>(x - (x + (e / 2 ) *\<^sub>R k)) \<bullet> i\<bar>) =
   1.217                (\<Sum>i\<in>Basis. (if i = k then e / 2 else 0))"
   1.218 -          using "*" by (blast intro: setsum.cong)
   1.219 +          using "*" by (blast intro: sum.cong)
   1.220          also have "\<dots> < e"
   1.221 -          apply (subst setsum.delta)
   1.222 +          apply (subst sum.delta)
   1.223            using e
   1.224            apply auto
   1.225            done
   1.226 @@ -1308,7 +1308,7 @@
   1.227      }
   1.228      then have "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - i) =
   1.229                 norm ((\<Sum>(x, k)\<in>p1 \<union> p2. content k *\<^sub>R f x) - i)"
   1.230 -      by (subst setsum.union_inter_neutral) (auto simp: p1 p2)
   1.231 +      by (subst sum.union_inter_neutral) (auto simp: p1 p2)
   1.232      also have "\<dots> < e"
   1.233        by (rule k d(2) p12 fine_union p1 p2)+
   1.234      finally have "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - i) < e" .
   1.235 @@ -1426,20 +1426,20 @@
   1.236  lemma dsum_bound:
   1.237    assumes "p division_of (cbox a b)"
   1.238      and "norm c \<le> e"
   1.239 -  shows "norm (setsum (\<lambda>l. content l *\<^sub>R c) p) \<le> e * content(cbox a b)"
   1.240 +  shows "norm (sum (\<lambda>l. content l *\<^sub>R c) p) \<le> e * content(cbox a b)"
   1.241  proof -
   1.242 -  have sumeq: "(\<Sum>i\<in>p. \<bar>content i\<bar>) = setsum content p"
   1.243 -    apply (rule setsum.cong)
   1.244 +  have sumeq: "(\<Sum>i\<in>p. \<bar>content i\<bar>) = sum content p"
   1.245 +    apply (rule sum.cong)
   1.246      using assms
   1.247      apply simp
   1.248      apply (metis abs_of_nonneg assms(1) content_pos_le division_ofD(4))
   1.249      done
   1.250    have e: "0 \<le> e"
   1.251      using assms(2) norm_ge_zero order_trans by blast
   1.252 -  have "norm (setsum (\<lambda>l. content l *\<^sub>R c) p) \<le> (\<Sum>i\<in>p. norm (content i *\<^sub>R c))"
   1.253 -    using norm_setsum by blast
   1.254 +  have "norm (sum (\<lambda>l. content l *\<^sub>R c) p) \<le> (\<Sum>i\<in>p. norm (content i *\<^sub>R c))"
   1.255 +    using norm_sum by blast
   1.256    also have "...  \<le> e * (\<Sum>i\<in>p. \<bar>content i\<bar>)"
   1.257 -    by (simp add: setsum_distrib_left[symmetric] mult.commute assms(2) mult_right_mono setsum_nonneg)
   1.258 +    by (simp add: sum_distrib_left[symmetric] mult.commute assms(2) mult_right_mono sum_nonneg)
   1.259    also have "... \<le> e * content (cbox a b)"
   1.260      apply (rule mult_left_mono [OF _ e])
   1.261      apply (simp add: sumeq)
   1.262 @@ -1451,7 +1451,7 @@
   1.263  lemma rsum_bound:
   1.264    assumes p: "p tagged_division_of (cbox a b)"
   1.265        and "\<forall>x\<in>cbox a b. norm (f x) \<le> e"
   1.266 -    shows "norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p) \<le> e * content (cbox a b)"
   1.267 +    shows "norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p) \<le> e * content (cbox a b)"
   1.268  proof (cases "cbox a b = {}")
   1.269    case True show ?thesis
   1.270      using p unfolding True tagged_division_of_trivial by auto
   1.271 @@ -1459,7 +1459,7 @@
   1.272    case False
   1.273    then have e: "e \<ge> 0"
   1.274      by (meson ex_in_conv assms(2) norm_ge_zero order_trans)
   1.275 -  have setsum_le: "setsum (content \<circ> snd) p \<le> content (cbox a b)"
   1.276 +  have sum_le: "sum (content \<circ> snd) p \<le> content (cbox a b)"
   1.277      unfolding additive_content_tagged_division[OF p, symmetric] split_def
   1.278      by (auto intro: eq_refl)
   1.279    have con: "\<And>xk. xk \<in> p \<Longrightarrow> 0 \<le> content (snd xk)"
   1.280 @@ -1468,15 +1468,15 @@
   1.281    have norm: "\<And>xk. xk \<in> p \<Longrightarrow> norm (f (fst xk)) \<le> e"
   1.282      unfolding fst_conv using tagged_division_ofD(2,3)[OF p] assms
   1.283      by (metis prod.collapse subset_eq)
   1.284 -  have "norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p) \<le> (\<Sum>i\<in>p. norm (case i of (x, k) \<Rightarrow> content k *\<^sub>R f x))"
   1.285 -    by (rule norm_setsum)
   1.286 +  have "norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p) \<le> (\<Sum>i\<in>p. norm (case i of (x, k) \<Rightarrow> content k *\<^sub>R f x))"
   1.287 +    by (rule norm_sum)
   1.288    also have "...  \<le> e * content (cbox a b)"
   1.289      unfolding split_def norm_scaleR
   1.290 -    apply (rule order_trans[OF setsum_mono])
   1.291 +    apply (rule order_trans[OF sum_mono])
   1.292      apply (rule mult_left_mono[OF _ abs_ge_zero, of _ e])
   1.293      apply (metis norm)
   1.294 -    unfolding setsum_distrib_right[symmetric]
   1.295 -    using con setsum_le
   1.296 +    unfolding sum_distrib_right[symmetric]
   1.297 +    using con sum_le
   1.298      apply (auto simp: mult.commute intro: mult_left_mono [OF _ e])
   1.299      done
   1.300    finally show ?thesis .
   1.301 @@ -1485,10 +1485,10 @@
   1.302  lemma rsum_diff_bound:
   1.303    assumes "p tagged_division_of (cbox a b)"
   1.304      and "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e"
   1.305 -  shows "norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - setsum (\<lambda>(x,k). content k *\<^sub>R g x) p) \<le>
   1.306 +  shows "norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p - sum (\<lambda>(x,k). content k *\<^sub>R g x) p) \<le>
   1.307           e * content (cbox a b)"
   1.308    apply (rule order_trans[OF _ rsum_bound[OF assms]])
   1.309 -  apply (simp add: split_def scaleR_diff_right setsum_subtractf eq_refl)
   1.310 +  apply (simp add: split_def scaleR_diff_right sum_subtractf eq_refl)
   1.311    done
   1.312  
   1.313  lemma has_integral_bound:
   1.314 @@ -1534,9 +1534,9 @@
   1.315    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   1.316    assumes "p tagged_division_of (cbox a b)"
   1.317        and "\<forall>x\<in>cbox a b. (f x)\<bullet>i \<le> (g x)\<bullet>i"
   1.318 -    shows "(setsum (\<lambda>(x,k). content k *\<^sub>R f x) p)\<bullet>i \<le> (setsum (\<lambda>(x,k). content k *\<^sub>R g x) p)\<bullet>i"
   1.319 -unfolding inner_setsum_left
   1.320 -proof (rule setsum_mono, clarify)
   1.321 +    shows "(sum (\<lambda>(x,k). content k *\<^sub>R f x) p)\<bullet>i \<le> (sum (\<lambda>(x,k). content k *\<^sub>R g x) p)\<bullet>i"
   1.322 +unfolding inner_sum_left
   1.323 +proof (rule sum_mono, clarify)
   1.324    fix a b
   1.325    assume ab: "(a, b) \<in> p"
   1.326    note tagged = tagged_division_ofD(2-4)[OF assms(1) ab]
   1.327 @@ -1877,7 +1877,7 @@
   1.328    also have "(\<Prod>j\<in>Basis. (b' 0 - a' 0) \<bullet> j) = 0"
   1.329      using k *
   1.330      by (intro setprod_zero bexI[OF _ k])
   1.331 -       (auto simp: b'_def a'_def inner_diff inner_setsum_left inner_not_same_Basis intro!: setsum.cong)
   1.332 +       (auto simp: b'_def a'_def inner_diff inner_sum_left inner_not_same_Basis intro!: sum.cong)
   1.333    also have "((\<lambda>d. \<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) \<longlongrightarrow> 0) (at_right 0) =
   1.334      ((\<lambda>d. content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d})) \<longlongrightarrow> 0) (at_right 0)"
   1.335    proof (intro tendsto_cong eventually_at_rightI)
   1.336 @@ -1952,7 +1952,7 @@
   1.337      assume p: "p tagged_division_of (cbox a b) \<and> (\<lambda>x. ball x d) fine p"
   1.338      have *: "(\<Sum>(x, ka)\<in>p. content ka *\<^sub>R ?i x) =
   1.339        (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d}) *\<^sub>R ?i x)"
   1.340 -      apply (rule setsum.cong)
   1.341 +      apply (rule sum.cong)
   1.342        apply (rule refl)
   1.343        unfolding split_paired_all real_scaleR_def mult_cancel_right split_conv
   1.344        apply cases
   1.345 @@ -1989,7 +1989,7 @@
   1.346        unfolding diff_0_right *
   1.347        unfolding real_scaleR_def real_norm_def
   1.348        apply (subst abs_of_nonneg)
   1.349 -      apply (rule setsum_nonneg)
   1.350 +      apply (rule sum_nonneg)
   1.351        apply rule
   1.352        unfolding split_paired_all split_conv
   1.353        apply (rule mult_nonneg_nonneg)
   1.354 @@ -2005,14 +2005,14 @@
   1.355      proof -
   1.356        have "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) \<le>
   1.357          (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}))"
   1.358 -        apply (rule setsum_mono)
   1.359 +        apply (rule sum_mono)
   1.360          unfolding split_paired_all split_conv
   1.361          apply (rule mult_right_le_one_le)
   1.362          apply (drule p'(4))
   1.363          apply (auto simp add:interval_doublesplit[OF k])
   1.364          done
   1.365        also have "\<dots> < e"
   1.366 -      proof (subst setsum.over_tagged_division_lemma[OF p[THEN conjunct1]], goal_cases)
   1.367 +      proof (subst sum.over_tagged_division_lemma[OF p[THEN conjunct1]], goal_cases)
   1.368          case prems: (1 u v)
   1.369          then have *: "content (cbox u v) = 0"
   1.370            unfolding content_eq_0_interior by simp
   1.371 @@ -2027,8 +2027,8 @@
   1.372            by (blast intro: antisym)
   1.373        next
   1.374          have "(\<Sum>l\<in>snd ` p. content (l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) =
   1.375 -          setsum content ((\<lambda>l. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})`{l\<in>snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}})"
   1.376 -        proof (subst (2) setsum.reindex_nontrivial)
   1.377 +          sum content ((\<lambda>l. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})`{l\<in>snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}})"
   1.378 +        proof (subst (2) sum.reindex_nontrivial)
   1.379            fix x y assume "x \<in> {l \<in> snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}" "y \<in> {l \<in> snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}"
   1.380              "x \<noteq> y" and eq: "x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} = y \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}"
   1.381            then obtain x' y' where "(x', x) \<in> p" "x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}" "(y', y) \<in> p" "y \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}"
   1.382 @@ -2041,7 +2041,7 @@
   1.383              by (auto simp: eq)
   1.384            then show "content (x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = 0"
   1.385              using p'(4)[OF \<open>(x', x) \<in> p\<close>] by (auto simp: interval_doublesplit[OF k] content_eq_0_interior simp del: interior_Int)
   1.386 -        qed (insert p'(1), auto intro!: setsum.mono_neutral_right)
   1.387 +        qed (insert p'(1), auto intro!: sum.mono_neutral_right)
   1.388          also have "\<dots> \<le> norm (\<Sum>l\<in>(\<lambda>l. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})`{l\<in>snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}. content l *\<^sub>R 1::real)"
   1.389            by simp
   1.390          also have "\<dots> \<le> 1 * content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})"
   1.391 @@ -2144,15 +2144,15 @@
   1.392          by (auto intro: tagged_division_finer[OF as(1) d(1)])
   1.393        from choice[OF this] guess q .. note q=conjunctD3[OF this[rule_format]]
   1.394        have *: "\<And>i. (\<Sum>(x, k)\<in>q i. content k *\<^sub>R indicator s x) \<ge> (0::real)"
   1.395 -        apply (rule setsum_nonneg)
   1.396 +        apply (rule sum_nonneg)
   1.397          apply safe
   1.398          unfolding real_scaleR_def
   1.399          apply (drule tagged_division_ofD(4)[OF q(1)])
   1.400          apply (auto intro: mult_nonneg_nonneg)
   1.401          done
   1.402        have **: "finite s \<Longrightarrow> finite t \<Longrightarrow> (\<forall>(x,y) \<in> t. (0::real) \<le> g(x,y)) \<Longrightarrow>
   1.403 -        (\<forall>y\<in>s. \<exists>x. (x,y) \<in> t \<and> f(y) \<le> g(x,y)) \<Longrightarrow> setsum f s \<le> setsum g t" for f g s t
   1.404 -        apply (rule setsum_le_included[of s t g snd f])
   1.405 +        (\<forall>y\<in>s. \<exists>x. (x,y) \<in> t \<and> f(y) \<le> g(x,y)) \<Longrightarrow> sum f s \<le> sum g t" for f g s t
   1.406 +        apply (rule sum_le_included[of s t g snd f])
   1.407          prefer 4
   1.408          apply safe
   1.409          apply (erule_tac x=x in ballE)
   1.410 @@ -2160,11 +2160,11 @@
   1.411          apply (rule_tac x="(xa,x)" in bexI)
   1.412          apply auto
   1.413          done
   1.414 -      have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) \<le> setsum (\<lambda>i. (real i + 1) *
   1.415 -        norm (setsum (\<lambda>(x,k). content k *\<^sub>R indicator s x :: real) (q i))) {..N+1}"
   1.416 -        unfolding real_norm_def setsum_distrib_left abs_of_nonneg[OF *] diff_0_right
   1.417 +      have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) \<le> sum (\<lambda>i. (real i + 1) *
   1.418 +        norm (sum (\<lambda>(x,k). content k *\<^sub>R indicator s x :: real) (q i))) {..N+1}"
   1.419 +        unfolding real_norm_def sum_distrib_left abs_of_nonneg[OF *] diff_0_right
   1.420          apply (rule order_trans)
   1.421 -        apply (rule norm_setsum)
   1.422 +        apply (rule norm_sum)
   1.423          apply (subst sum_sum_product)
   1.424          prefer 3
   1.425        proof (rule **, safe)
   1.426 @@ -2229,8 +2229,8 @@
   1.427            apply auto
   1.428            done
   1.429        qed (insert as, auto)
   1.430 -      also have "\<dots> \<le> setsum (\<lambda>i. e / 2 / 2 ^ i) {..N+1}"
   1.431 -      proof (rule setsum_mono, goal_cases)
   1.432 +      also have "\<dots> \<le> sum (\<lambda>i. e / 2 / 2 ^ i) {..N+1}"
   1.433 +      proof (rule sum_mono, goal_cases)
   1.434          case (1 i)
   1.435          then show ?case
   1.436            apply (subst mult.commute, subst pos_le_divide_eq[symmetric])
   1.437 @@ -2240,7 +2240,7 @@
   1.438            done
   1.439        qed
   1.440        also have "\<dots> < e * inverse 2 * 2"
   1.441 -        unfolding divide_inverse setsum_distrib_left[symmetric]
   1.442 +        unfolding divide_inverse sum_distrib_left[symmetric]
   1.443          apply (rule mult_strict_left_mono)
   1.444          unfolding power_inverse [symmetric] lessThan_Suc_atMost[symmetric]
   1.445          apply (subst geometric_sum)
   1.446 @@ -2640,14 +2640,14 @@
   1.447  lemma has_integral_factor_content:
   1.448    "(f has_integral i) (cbox a b) \<longleftrightarrow>
   1.449      (\<forall>e>0. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
   1.450 -      norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - i) \<le> e * content (cbox a b)))"
   1.451 +      norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p - i) \<le> e * content (cbox a b)))"
   1.452  proof (cases "content (cbox a b) = 0")
   1.453    case True
   1.454    show ?thesis
   1.455      unfolding has_integral_null_eq[OF True]
   1.456      apply safe
   1.457      apply (rule, rule, rule gauge_trivial, safe)
   1.458 -    unfolding setsum_content_null[OF True] True
   1.459 +    unfolding sum_content_null[OF True] True
   1.460      defer
   1.461      apply (erule_tac x=1 in allE)
   1.462      apply safe
   1.463 @@ -2655,7 +2655,7 @@
   1.464      apply (rule fine_division_exists[of _ a b])
   1.465      apply assumption
   1.466      apply (erule_tac x=p in allE)
   1.467 -    unfolding setsum_content_null[OF True]
   1.468 +    unfolding sum_content_null[OF True]
   1.469      apply auto
   1.470      done
   1.471  next
   1.472 @@ -2696,7 +2696,7 @@
   1.473  lemma has_integral_factor_content_real:
   1.474    "(f has_integral i) {a .. b::real} \<longleftrightarrow>
   1.475      (\<forall>e>0. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a .. b}  \<and> d fine p \<longrightarrow>
   1.476 -      norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - i) \<le> e * content {a .. b} ))"
   1.477 +      norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p - i) \<le> e * content {a .. b} ))"
   1.478    unfolding box_real[symmetric]
   1.479    by (rule has_integral_factor_content)
   1.480  
   1.481 @@ -2738,10 +2738,10 @@
   1.482      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content (cbox a b)"
   1.483        unfolding content_real[OF assms(1), simplified box_real[symmetric]] additive_tagged_division_1[OF assms(1) as(1)[simplified box_real],of f,symmetric]
   1.484        unfolding additive_tagged_division_1[OF assms(1) as(1)[simplified box_real],of "\<lambda>x. x",symmetric]
   1.485 -      unfolding setsum_distrib_left
   1.486 +      unfolding sum_distrib_left
   1.487        defer
   1.488 -      unfolding setsum_subtractf[symmetric]
   1.489 -    proof (rule setsum_norm_le,safe)
   1.490 +      unfolding sum_subtractf[symmetric]
   1.491 +    proof (rule sum_norm_le,safe)
   1.492        fix x k
   1.493        assume "(x, k) \<in> p"
   1.494        note xk = tagged_division_ofD(2-4)[OF as(1) this]
   1.495 @@ -2809,7 +2809,7 @@
   1.496  
   1.497  subsection \<open>Taylor series expansion\<close>
   1.498  
   1.499 -lemma (in bounded_bilinear) setsum_prod_derivatives_has_vector_derivative:
   1.500 +lemma (in bounded_bilinear) sum_prod_derivatives_has_vector_derivative:
   1.501    assumes "p>0"
   1.502    and f0: "Df 0 = f"
   1.503    and Df: "\<And>m t. m < p \<Longrightarrow> a \<le> t \<Longrightarrow> t \<le> b \<Longrightarrow>
   1.504 @@ -2835,7 +2835,7 @@
   1.505      prod (Df (Suc i) t) (Dg (p - Suc i) t))) =
   1.506      (\<Sum>i\<le>(Suc p'). ?f i - ?f (Suc i))"
   1.507      by (auto simp: algebra_simps p'(2) numeral_2_eq_2 * lessThan_Suc_atMost)
   1.508 -  also note setsum_telescope
   1.509 +  also note sum_telescope
   1.510    finally
   1.511    have "(\<Sum>i<p. (-1) ^ i *\<^sub>R (prod (Df i t) (Dg (Suc (p - Suc i)) t) +
   1.512      prod (Df (Suc i) t) (Dg (p - Suc i) t)))
   1.513 @@ -2884,7 +2884,7 @@
   1.514      unfolding Dg_def
   1.515      by (auto intro!: derivative_eq_intros simp: has_vector_derivative_def fact_eq divide_simps)
   1.516    let ?sum = "\<lambda>t. \<Sum>i<p. (- 1) ^ i *\<^sub>R Dg i t *\<^sub>R Df (p - Suc i) t"
   1.517 -  from setsum_prod_derivatives_has_vector_derivative[of _ Dg _ _ _ Df,
   1.518 +  from sum_prod_derivatives_has_vector_derivative[of _ Dg _ _ _ Df,
   1.519        OF \<open>p > 0\<close> g0 Dg f0 Df]
   1.520    have deriv: "\<And>t. a \<le> t \<Longrightarrow> t \<le> b \<Longrightarrow>
   1.521      (?sum has_vector_derivative
   1.522 @@ -2903,7 +2903,7 @@
   1.523    then have "?sum b = f b"
   1.524      using Suc_pred'[OF \<open>p > 0\<close>]
   1.525      by (simp add: diff_eq_eq Dg_def power_0_left le_Suc_eq if_distrib
   1.526 -        cond_application_beta setsum.If_cases f0)
   1.527 +        cond_application_beta sum.If_cases f0)
   1.528    also
   1.529    have "{..<p} = (\<lambda>x. p - x - 1) ` {..<p}"
   1.530    proof safe
   1.531 @@ -2914,7 +2914,7 @@
   1.532    qed simp
   1.533    from _ this
   1.534    have "?sum a = (\<Sum>i<p. ((b - a) ^ i / fact i) *\<^sub>R Df i a)"
   1.535 -    by (rule setsum.reindex_cong) (auto simp add: inj_on_def Dg_def one)
   1.536 +    by (rule sum.reindex_cong) (auto simp add: inj_on_def Dg_def one)
   1.537    finally show c: ?case .
   1.538    case 2 show ?case using c integral_unique by force
   1.539    case 3 show ?case using c by force
   1.540 @@ -3003,10 +3003,10 @@
   1.541          unfolding euclidean_eq_iff[where 'a='a] using i by auto
   1.542        have *: "Basis = insert i (Basis - {i})"
   1.543          using i by auto
   1.544 -      have "norm (y - x) < e + setsum (\<lambda>i. 0) Basis"
   1.545 +      have "norm (y - x) < e + sum (\<lambda>i. 0) Basis"
   1.546          apply (rule le_less_trans[OF norm_le_l1])
   1.547          apply (subst *)
   1.548 -        apply (subst setsum.insert)
   1.549 +        apply (subst sum.insert)
   1.550          prefer 3
   1.551          apply (rule add_less_le_mono)
   1.552        proof -
   1.553 @@ -3436,9 +3436,9 @@
   1.554            using inj(1) unfolding inj_on_def by fastforce
   1.555          have "(\<Sum>(x, k)\<in>(\<lambda>(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - i" (is "?l = _")
   1.556            using assms(7)
   1.557 -          apply (simp only: algebra_simps add_left_cancel scaleR_right.setsum)
   1.558 -          apply (subst setsum.reindex_bij_betw[symmetric, where h="\<lambda>(x, k). (g x, g ` k)" and S=p])
   1.559 -          apply (auto intro!: * setsum.cong simp: bij_betw_def dest!: p(4))
   1.560 +          apply (simp only: algebra_simps add_left_cancel scaleR_right.sum)
   1.561 +          apply (subst sum.reindex_bij_betw[symmetric, where h="\<lambda>(x, k). (g x, g ` k)" and S=p])
   1.562 +          apply (auto intro!: * sum.cong simp: bij_betw_def dest!: p(4))
   1.563            done
   1.564        also have "\<dots> = r *\<^sub>R ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r")
   1.565          unfolding scaleR_diff_right scaleR_scaleR
   1.566 @@ -3865,18 +3865,18 @@
   1.567      have **: "\<And>n1 s1 n2 s2::real. n2 \<le> s2 / 2 \<Longrightarrow> n1 - s1 \<le> s2 / 2 \<Longrightarrow> n1 + n2 \<le> s1 + s2"
   1.568        by arith
   1.569      show ?case
   1.570 -      unfolding content_real[OF assms(1)] and *[of "\<lambda>x. x"] *[of f] setsum_subtractf[symmetric] split_minus
   1.571 -      unfolding setsum_distrib_left
   1.572 +      unfolding content_real[OF assms(1)] and *[of "\<lambda>x. x"] *[of f] sum_subtractf[symmetric] split_minus
   1.573 +      unfolding sum_distrib_left
   1.574        apply (subst(2) pA)
   1.575        apply (subst pA)
   1.576 -      unfolding setsum.union_disjoint[OF pA(2-)]
   1.577 +      unfolding sum.union_disjoint[OF pA(2-)]
   1.578      proof (rule norm_triangle_le, rule **, goal_cases)
   1.579        case 1
   1.580        show ?case
   1.581          apply (rule order_trans)
   1.582 -        apply (rule setsum_norm_le)
   1.583 +        apply (rule sum_norm_le)
   1.584          defer
   1.585 -        apply (subst setsum_divide_distrib)
   1.586 +        apply (subst sum_divide_distrib)
   1.587          apply (rule order_refl)
   1.588          apply safe
   1.589          apply (unfold not_le o_def split_conv fst_conv)
   1.590 @@ -3930,12 +3930,12 @@
   1.591        case 2
   1.592        show ?case
   1.593          apply (rule *)
   1.594 -        apply (rule setsum_nonneg)
   1.595 +        apply (rule sum_nonneg)
   1.596          apply rule
   1.597          apply (unfold split_paired_all split_conv)
   1.598          defer
   1.599 -        unfolding setsum.union_disjoint[OF pA(2-),symmetric] pA(1)[symmetric]
   1.600 -        unfolding setsum_distrib_left[symmetric]
   1.601 +        unfolding sum.union_disjoint[OF pA(2-),symmetric] pA(1)[symmetric]
   1.602 +        unfolding sum_distrib_left[symmetric]
   1.603          apply (subst additive_tagged_division_1[OF _ as(1)])
   1.604          apply (rule assms)
   1.605        proof -
   1.606 @@ -3948,12 +3948,12 @@
   1.607          then show "0 \<le> e * ((Sup k) - (Inf k))"
   1.608            unfolding uv using e by (auto simp add: field_simps)
   1.609        next
   1.610 -        have *: "\<And>s f t e. setsum f s = setsum f t \<Longrightarrow> norm (setsum f t) \<le> e \<Longrightarrow> norm (setsum f s) \<le> e"
   1.611 +        have *: "\<And>s f t e. sum f s = sum f t \<Longrightarrow> norm (sum f t) \<le> e \<Longrightarrow> norm (sum f s) \<le> e"
   1.612            by auto
   1.613          show "norm (\<Sum>(x, k)\<in>p \<inter> ?A. content k *\<^sub>R f' x -
   1.614            (f ((Sup k)) - f ((Inf k)))) \<le> e * (b - a) / 2"
   1.615            apply (rule *[where t1="p \<inter> {t. fst t \<in> {a, b} \<and> content(snd t) \<noteq> 0}"])
   1.616 -          apply (rule setsum.mono_neutral_right[OF pA(2)])
   1.617 +          apply (rule sum.mono_neutral_right[OF pA(2)])
   1.618            defer
   1.619            apply rule
   1.620            unfolding split_paired_all split_conv o_def
   1.621 @@ -3975,7 +3975,7 @@
   1.622            have *: "p \<inter> {t. fst t \<in> {a, b} \<and> content(snd t) \<noteq> 0} =
   1.623              {t. t\<in>p \<and> fst t = a \<and> content(snd t) \<noteq> 0} \<union> {t. t\<in>p \<and> fst t = b \<and> content(snd t) \<noteq> 0}"
   1.624              by blast
   1.625 -          have **: "norm (setsum f s) \<le> e"
   1.626 +          have **: "norm (sum f s) \<le> e"
   1.627              if "\<forall>x y. x \<in> s \<and> y \<in> s \<longrightarrow> x = y"
   1.628              and "\<forall>x. x \<in> s \<longrightarrow> norm (f x) \<le> e"
   1.629              and "e > 0"
   1.630 @@ -3995,7 +3995,7 @@
   1.631            case 2
   1.632            show ?case
   1.633              apply (subst *)
   1.634 -            apply (subst setsum.union_disjoint)
   1.635 +            apply (subst sum.union_disjoint)
   1.636              prefer 4
   1.637              apply (rule order_trans[of _ "e * (b - a)/4 + e * (b - a)/4"])
   1.638              apply (rule norm_triangle_le,rule add_mono)
   1.639 @@ -4425,7 +4425,7 @@
   1.640        then show ?thesis
   1.641          unfolding ** box_real
   1.642          apply -
   1.643 -        apply (subst setsum.insert)
   1.644 +        apply (subst sum.insert)
   1.645          apply (rule p')
   1.646          unfolding split_conv
   1.647          defer
   1.648 @@ -5003,7 +5003,7 @@
   1.649        show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i" if "norm x \<le> B" and "i \<in> Basis"
   1.650          using that and Basis_le_norm[OF \<open>i\<in>Basis\<close>, of x]
   1.651          unfolding c_def d_def
   1.652 -        by (auto simp add: field_simps setsum_negf)
   1.653 +        by (auto simp add: field_simps sum_negf)
   1.654      qed
   1.655      have "ball 0 C \<subseteq> cbox c d"
   1.656        apply (rule subsetI)
   1.657 @@ -5014,7 +5014,7 @@
   1.658        show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i"
   1.659          using Basis_le_norm[OF i, of x] and x i
   1.660          unfolding c_def d_def
   1.661 -        by (auto simp: setsum_negf)
   1.662 +        by (auto simp: sum_negf)
   1.663      qed
   1.664      from C(2)[OF this] have "\<exists>y. (f has_integral y) (cbox a b)"
   1.665        unfolding has_integral_restrict_closed_subintervals_eq[OF c_d,symmetric]
   1.666 @@ -5040,7 +5040,7 @@
   1.667          then show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i"
   1.668            using Basis_le_norm[of i x]
   1.669            unfolding c_def d_def
   1.670 -          by (auto simp add: field_simps setsum_negf)
   1.671 +          by (auto simp add: field_simps sum_negf)
   1.672        qed
   1.673        have "ball 0 C \<subseteq> cbox c d"
   1.674          apply (rule subsetI)
   1.675 @@ -5051,7 +5051,7 @@
   1.676          then show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i"
   1.677            using Basis_le_norm[of i x]
   1.678            unfolding c_def d_def
   1.679 -          by (auto simp: setsum_negf)
   1.680 +          by (auto simp: sum_negf)
   1.681        qed
   1.682        note C(2)[OF this] then guess z .. note z = conjunctD2[OF this, unfolded s]
   1.683        note this[unfolded has_integral_restrict_closed_subintervals_eq[OF c_d]]
   1.684 @@ -5425,7 +5425,7 @@
   1.685          then show ?case
   1.686            using Basis_le_norm[of i x] \<open>i\<in>Basis\<close>
   1.687            using n N
   1.688 -          by (auto simp add: field_simps setsum_negf)
   1.689 +          by (auto simp add: field_simps sum_negf)
   1.690        qed
   1.691      }
   1.692      then show ?case
   1.693 @@ -5482,7 +5482,7 @@
   1.694            then show ?case
   1.695              using Basis_le_norm[of i x] \<open>i \<in> Basis\<close>
   1.696              using n
   1.697 -            by (auto simp add: field_simps setsum_negf)
   1.698 +            by (auto simp add: field_simps sum_negf)
   1.699          qed
   1.700        qed
   1.701      qed
   1.702 @@ -5541,9 +5541,9 @@
   1.703        and "0 \<le> (\<Sum>(x, k)\<in>p2. content k *\<^sub>R h x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)"
   1.704        and "(\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R g x) \<ge> 0"
   1.705        and "0 \<le> (\<Sum>(x, k)\<in>p1. content k *\<^sub>R h x) - (\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x)"
   1.706 -      unfolding setsum_subtractf[symmetric]
   1.707 +      unfolding sum_subtractf[symmetric]
   1.708        apply -
   1.709 -      apply (rule_tac[!] setsum_nonneg)
   1.710 +      apply (rule_tac[!] sum_nonneg)
   1.711        apply safe
   1.712        unfolding real_scaleR_def right_diff_distrib[symmetric]
   1.713        apply (rule_tac[!] mult_nonneg_nonneg)
   1.714 @@ -5774,7 +5774,7 @@
   1.715    assumes "finite t"
   1.716      and "\<forall>s\<in>t. (f has_integral (i s)) s"
   1.717      and "\<forall>s\<in>t. \<forall>s'\<in>t. s \<noteq> s' \<longrightarrow> negligible (s \<inter> s')"
   1.718 -  shows "(f has_integral (setsum i t)) (\<Union>t)"
   1.719 +  shows "(f has_integral (sum i t)) (\<Union>t)"
   1.720  proof -
   1.721    note * = has_integral_restrict_univ[symmetric, of f]
   1.722    have **: "negligible (\<Union>((\<lambda>(a,b). a \<inter> b) ` {(a,b). a \<in> t \<and> b \<in> {y. y \<in> t \<and> a \<noteq> y}}))"
   1.723 @@ -5787,7 +5787,7 @@
   1.724      apply auto
   1.725      done
   1.726    note assms(2)[unfolded *]
   1.727 -  note has_integral_setsum[OF assms(1) this]
   1.728 +  note has_integral_sum[OF assms(1) this]
   1.729    then show ?thesis
   1.730      unfolding *
   1.731      apply -
   1.732 @@ -5807,12 +5807,12 @@
   1.733          unfolding if_P[OF True]
   1.734          apply (rule trans)
   1.735          defer
   1.736 -        apply (rule setsum.cong)
   1.737 +        apply (rule sum.cong)
   1.738          apply (rule refl)
   1.739          apply (subst *)
   1.740          apply assumption
   1.741          apply (rule refl)
   1.742 -        unfolding setsum.delta[OF assms(1)]
   1.743 +        unfolding sum.delta[OF assms(1)]
   1.744          using s
   1.745          apply auto
   1.746          done
   1.747 @@ -5827,7 +5827,7 @@
   1.748    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   1.749    assumes "d division_of s"
   1.750      and "\<forall>k\<in>d. (f has_integral (i k)) k"
   1.751 -  shows "(f has_integral (setsum i d)) s"
   1.752 +  shows "(f has_integral (sum i d)) s"
   1.753  proof -
   1.754    note d = division_ofD[OF assms(1)]
   1.755    show ?thesis
   1.756 @@ -5854,7 +5854,7 @@
   1.757    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   1.758    assumes "d division_of s"
   1.759      and "\<forall>k\<in>d. f integrable_on k"
   1.760 -  shows "integral s f = setsum (\<lambda>i. integral i f) d"
   1.761 +  shows "integral s f = sum (\<lambda>i. integral i f) d"
   1.762    apply (rule integral_unique)
   1.763    apply (rule has_integral_combine_division[OF assms(1)])
   1.764    using assms(2)
   1.765 @@ -5867,7 +5867,7 @@
   1.766    assumes "f integrable_on s"
   1.767      and "d division_of k"
   1.768      and "k \<subseteq> s"
   1.769 -  shows "(f has_integral (setsum (\<lambda>i. integral i f) d)) k"
   1.770 +  shows "(f has_integral (sum (\<lambda>i. integral i f) d)) k"
   1.771    apply (rule has_integral_combine_division[OF assms(2)])
   1.772    apply safe
   1.773    unfolding has_integral_integral[symmetric]
   1.774 @@ -5887,7 +5887,7 @@
   1.775    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   1.776    assumes "f integrable_on s"
   1.777      and "d division_of s"
   1.778 -  shows "integral s f = setsum (\<lambda>i. integral i f) d"
   1.779 +  shows "integral s f = sum (\<lambda>i. integral i f) d"
   1.780    apply (rule integral_unique)
   1.781    apply (rule has_integral_combine_division_topdown)
   1.782    using assms
   1.783 @@ -5941,17 +5941,17 @@
   1.784      apply auto
   1.785      done
   1.786    also have "(\<Sum>k\<in>snd`p. integral k f) = (\<Sum>(x, k)\<in>p. integral k f)"
   1.787 -    by (intro setsum.over_tagged_division_lemma[OF assms(1), symmetric] integral_null)
   1.788 +    by (intro sum.over_tagged_division_lemma[OF assms(1), symmetric] integral_null)
   1.789         (simp add: content_eq_0_interior)
   1.790    finally show ?thesis
   1.791 -    using assms by (auto simp add: has_integral_iff intro!: setsum.cong)
   1.792 +    using assms by (auto simp add: has_integral_iff intro!: sum.cong)
   1.793  qed
   1.794  
   1.795  lemma integral_combine_tagged_division_bottomup:
   1.796    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   1.797    assumes "p tagged_division_of (cbox a b)"
   1.798      and "\<forall>(x,k)\<in>p. f integrable_on k"
   1.799 -  shows "integral (cbox a b) f = setsum (\<lambda>(x,k). integral k f) p"
   1.800 +  shows "integral (cbox a b) f = sum (\<lambda>(x,k). integral k f) p"
   1.801    apply (rule integral_unique)
   1.802    apply (rule has_integral_combine_tagged_division[OF assms(1)])
   1.803    using assms(2)
   1.804 @@ -5962,7 +5962,7 @@
   1.805    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   1.806    assumes "f integrable_on cbox a b"
   1.807      and "p tagged_division_of (cbox a b)"
   1.808 -  shows "(f has_integral (setsum (\<lambda>(x,k). integral k f) p)) (cbox a b)"
   1.809 +  shows "(f has_integral (sum (\<lambda>(x,k). integral k f) p)) (cbox a b)"
   1.810    apply (rule has_integral_combine_tagged_division[OF assms(2)])
   1.811    apply safe
   1.812  proof goal_cases
   1.813 @@ -5976,7 +5976,7 @@
   1.814    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   1.815    assumes "f integrable_on cbox a b"
   1.816      and "p tagged_division_of (cbox a b)"
   1.817 -  shows "integral (cbox a b) f = setsum (\<lambda>(x,k). integral k f) p"
   1.818 +  shows "integral (cbox a b) f = sum (\<lambda>(x,k). integral k f) p"
   1.819    apply (rule integral_unique)
   1.820    apply (rule has_integral_combine_tagged_division_topdown)
   1.821    using assms
   1.822 @@ -5992,9 +5992,9 @@
   1.823      and "e > 0"
   1.824      and "gauge d"
   1.825      and "(\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
   1.826 -      norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - integral(cbox a b) f) < e)"
   1.827 +      norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p - integral(cbox a b) f) < e)"
   1.828      and p: "p tagged_partial_division_of (cbox a b)" "d fine p"
   1.829 -  shows "norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x - integral k f) p) \<le> e"
   1.830 +  shows "norm (sum (\<lambda>(x,k). content k *\<^sub>R f x - integral k f) p) \<le> e"
   1.831    (is "?x \<le> e")
   1.832  proof -
   1.833    { presume "\<And>k. 0<k \<Longrightarrow> ?x \<le> e + k" then show ?thesis by (blast intro: field_le_epsilon) }
   1.834 @@ -6012,7 +6012,7 @@
   1.835      using q' unfolding r_def by auto
   1.836  
   1.837    have "\<forall>i\<in>r. \<exists>p. p tagged_division_of i \<and> d fine p \<and>
   1.838 -    norm (setsum (\<lambda>(x,j). content j *\<^sub>R f x) p - integral i f) < k / (real (card r) + 1)"
   1.839 +    norm (sum (\<lambda>(x,j). content j *\<^sub>R f x) p - integral i f) < k / (real (card r) + 1)"
   1.840      apply safe
   1.841    proof goal_cases
   1.842      case (1 i)
   1.843 @@ -6100,7 +6100,7 @@
   1.844  
   1.845    then have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>\<Union>(qq ` r). content k *\<^sub>R f x) -
   1.846      integral (cbox a b) f) < e"
   1.847 -    apply (subst setsum.union_inter_neutral[symmetric])
   1.848 +    apply (subst sum.union_inter_neutral[symmetric])
   1.849      apply (rule p')
   1.850      prefer 3
   1.851      apply assumption
   1.852 @@ -6124,9 +6124,9 @@
   1.853        unfolding uv content_eq_0_interior[symmetric] by auto
   1.854    qed auto
   1.855  
   1.856 -  then have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + setsum (setsum (\<lambda>(x, k). content k *\<^sub>R f x))
   1.857 +  then have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + sum (sum (\<lambda>(x, k). content k *\<^sub>R f x))
   1.858      (qq ` r) - integral (cbox a b) f) < e"
   1.859 -    apply (subst (asm) setsum.Union_comp)
   1.860 +    apply (subst (asm) sum.Union_comp)
   1.861      prefer 2
   1.862      unfolding split_paired_all split_conv image_iff
   1.863      apply (erule bexE)+
   1.864 @@ -6150,11 +6150,11 @@
   1.865        by auto
   1.866    qed (insert qq, auto)
   1.867  
   1.868 -  then have **: "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + setsum (setsum (\<lambda>(x, k). content k *\<^sub>R f x) \<circ> qq) r -
   1.869 +  then have **: "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + sum (sum (\<lambda>(x, k). content k *\<^sub>R f x) \<circ> qq) r -
   1.870      integral (cbox a b) f) < e"
   1.871 -    apply (subst (asm) setsum.reindex_nontrivial)
   1.872 +    apply (subst (asm) sum.reindex_nontrivial)
   1.873      apply fact
   1.874 -    apply (rule setsum.neutral)
   1.875 +    apply (rule sum.neutral)
   1.876      apply rule
   1.877      unfolding split_paired_all split_conv
   1.878      defer
   1.879 @@ -6180,28 +6180,28 @@
   1.880    qed
   1.881  
   1.882    have "?x =  norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p. integral k f))"
   1.883 -    unfolding split_def setsum_subtractf ..
   1.884 +    unfolding split_def sum_subtractf ..
   1.885    also have "\<dots> \<le> e + k"
   1.886 -    apply (rule *[OF **, where ir1="setsum (\<lambda>k. integral k f) r"])
   1.887 +    apply (rule *[OF **, where ir1="sum (\<lambda>k. integral k f) r"])
   1.888    proof goal_cases
   1.889      case 1
   1.890      have *: "k * real (card r) / (1 + real (card r)) < k"
   1.891        using k by (auto simp add: field_simps)
   1.892      show ?case
   1.893 -      apply (rule le_less_trans[of _ "setsum (\<lambda>x. k / (real (card r) + 1)) r"])
   1.894 -      unfolding setsum_subtractf[symmetric]
   1.895 -      apply (rule setsum_norm_le)
   1.896 +      apply (rule le_less_trans[of _ "sum (\<lambda>x. k / (real (card r) + 1)) r"])
   1.897 +      unfolding sum_subtractf[symmetric]
   1.898 +      apply (rule sum_norm_le)
   1.899        apply rule
   1.900        apply (drule qq)
   1.901        defer
   1.902 -      unfolding divide_inverse setsum_distrib_right[symmetric]
   1.903 +      unfolding divide_inverse sum_distrib_right[symmetric]
   1.904        unfolding divide_inverse[symmetric]
   1.905        using * apply (auto simp add: field_simps)
   1.906        done
   1.907    next
   1.908      case 2
   1.909      have *: "(\<Sum>(x, k)\<in>p. integral k f) = (\<Sum>k\<in>snd ` p. integral k f)"
   1.910 -      apply (subst setsum.reindex_nontrivial)
   1.911 +      apply (subst sum.reindex_nontrivial)
   1.912        apply fact
   1.913        unfolding split_paired_all snd_conv split_def o_def
   1.914      proof -
   1.915 @@ -6221,7 +6221,7 @@
   1.916      from q(1) have **: "snd ` p \<union> q = q" by auto
   1.917      show ?case
   1.918        unfolding integral_combine_division_topdown[OF assms(1) q(2)] * r_def
   1.919 -      using ** q'(1) p'(1) setsum.union_disjoint [of "snd ` p" "q - snd ` p" "\<lambda>k. integral k f", symmetric]
   1.920 +      using ** q'(1) p'(1) sum.union_disjoint [of "snd ` p" "q - snd ` p" "\<lambda>k. integral k f", symmetric]
   1.921          by simp
   1.922    qed
   1.923    finally show "?x \<le> e + k" .
   1.924 @@ -6233,12 +6233,12 @@
   1.925      and "e > 0"
   1.926      and "gauge d"
   1.927      and "\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
   1.928 -      norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - integral (cbox a b) f) < e"
   1.929 +      norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p - integral (cbox a b) f) < e"
   1.930      and "p tagged_partial_division_of (cbox a b)"
   1.931      and "d fine p"
   1.932 -  shows "setsum (\<lambda>(x,k). norm (content k *\<^sub>R f x - integral k f)) p \<le> 2 * real (DIM('n)) * e"
   1.933 +  shows "sum (\<lambda>(x,k). norm (content k *\<^sub>R f x - integral k f)) p \<le> 2 * real (DIM('n)) * e"
   1.934    unfolding split_def
   1.935 -  apply (rule setsum_norm_allsubsets_bound)
   1.936 +  apply (rule sum_norm_allsubsets_bound)
   1.937    defer
   1.938    apply (rule henstock_lemma_part1[unfolded split_def,OF assms(1-3)])
   1.939    apply safe
   1.940 @@ -6260,7 +6260,7 @@
   1.941      and "e > 0"
   1.942    obtains d where "gauge d"
   1.943      and "\<forall>p. p tagged_partial_division_of (cbox a b) \<and> d fine p \<longrightarrow>
   1.944 -      setsum (\<lambda>(x,k). norm(content k *\<^sub>R f x - integral k f)) p < e"
   1.945 +      sum (\<lambda>(x,k). norm(content k *\<^sub>R f x - integral k f)) p < e"
   1.946  proof -
   1.947    have *: "e / (2 * (real DIM('n) + 1)) > 0" using assms(2) by simp
   1.948    from integrable_integral[OF assms(1),unfolded has_integral[of f],rule_format,OF this]
   1.949 @@ -6287,7 +6287,7 @@
   1.950  
   1.951  lemma sum_gp_basic:
   1.952    fixes x :: "'a::ring_1"
   1.953 -  shows "(1 - x) * setsum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
   1.954 +  shows "(1 - x) * sum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
   1.955  proof -
   1.956    define y where "y = 1 - x"
   1.957    have "y * (\<Sum>i=0..n. (1 - y) ^ i) = 1 - (1 - y) ^ Suc n"
   1.958 @@ -6298,7 +6298,7 @@
   1.959  
   1.960  lemma sum_gp_multiplied:
   1.961    assumes mn: "m \<le> n"
   1.962 -  shows "((1::'a::{field}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n"
   1.963 +  shows "((1::'a::{field}) - x) * sum (op ^ x) {m..n} = x^m - x^ Suc n"
   1.964    (is "?lhs = ?rhs")
   1.965  proof -
   1.966    let ?S = "{0..(n - m)}"
   1.967 @@ -6314,8 +6314,8 @@
   1.968      done
   1.969    have th: "op ^ x \<circ> op + m = (\<lambda>i. x^m * x^i)"
   1.970      by (rule ext) (simp add: power_add power_mult)
   1.971 -  from setsum.reindex[OF i, of "op ^ x", unfolded f th setsum_distrib_left[symmetric]]
   1.972 -  have "?lhs = x^m * ((1 - x) * setsum (op ^ x) {0..n - m})"
   1.973 +  from sum.reindex[OF i, of "op ^ x", unfolded f th sum_distrib_left[symmetric]]
   1.974 +  have "?lhs = x^m * ((1 - x) * sum (op ^ x) {0..n - m})"
   1.975      by simp
   1.976    then show ?thesis
   1.977      unfolding sum_gp_basic
   1.978 @@ -6324,7 +6324,7 @@
   1.979  qed
   1.980  
   1.981  lemma sum_gp:
   1.982 -  "setsum (op ^ (x::'a::{field})) {m .. n} =
   1.983 +  "sum (op ^ (x::'a::{field})) {m .. n} =
   1.984      (if n < m then 0
   1.985       else if x = 1 then of_nat ((n + 1) - m)
   1.986       else (x^ m - x^ (Suc n)) / (1 - x))"
   1.987 @@ -6357,7 +6357,7 @@
   1.988  qed
   1.989  
   1.990  lemma sum_gp_offset:
   1.991 -  "setsum (op ^ (x::'a::{field})) {m .. m+n} =
   1.992 +  "sum (op ^ (x::'a::{field})) {m .. m+n} =
   1.993      (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
   1.994    unfolding sum_gp[of x m "m + n"] power_Suc
   1.995    by (simp add: field_simps power_add)
   1.996 @@ -6497,12 +6497,12 @@
   1.997          case 1
   1.998          show ?case
   1.999            apply (rule order_trans[of _ "\<Sum>(x, k)\<in>p. content k * (e / (4 * content (cbox a b)))"])
  1.1000 -          unfolding setsum_subtractf[symmetric]
  1.1001 +          unfolding sum_subtractf[symmetric]
  1.1002            apply (rule order_trans)
  1.1003 -          apply (rule norm_setsum)
  1.1004 -          apply (rule setsum_mono)
  1.1005 +          apply (rule norm_sum)
  1.1006 +          apply (rule sum_mono)
  1.1007            unfolding split_paired_all split_conv
  1.1008 -          unfolding split_def setsum_distrib_right[symmetric] scaleR_diff_right[symmetric]
  1.1009 +          unfolding split_def sum_distrib_right[symmetric] scaleR_diff_right[symmetric]
  1.1010            unfolding additive_content_tagged_division[OF p(1), unfolded split_def]
  1.1011          proof -
  1.1012            fix x k
  1.1013 @@ -6524,22 +6524,22 @@
  1.1014          show ?case
  1.1015            apply (rule le_less_trans[of _ "norm (\<Sum>j = 0..s.
  1.1016              \<Sum>(x, k)\<in>{xk\<in>p. m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x)))"])
  1.1017 -          apply (subst setsum_group)
  1.1018 +          apply (subst sum_group)
  1.1019            apply fact
  1.1020            apply (rule finite_atLeastAtMost)
  1.1021            defer
  1.1022            apply (subst split_def)+
  1.1023 -          unfolding setsum_subtractf
  1.1024 +          unfolding sum_subtractf
  1.1025            apply rule
  1.1026          proof -
  1.1027            show "norm (\<Sum>j = 0..s. \<Sum>(x, k)\<in>{xk \<in> p.
  1.1028              m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x))) < e / 2"
  1.1029 -            apply (rule le_less_trans[of _ "setsum (\<lambda>i. e / 2^(i+2)) {0..s}"])
  1.1030 -            apply (rule setsum_norm_le)
  1.1031 +            apply (rule le_less_trans[of _ "sum (\<lambda>i. e / 2^(i+2)) {0..s}"])
  1.1032 +            apply (rule sum_norm_le)
  1.1033            proof
  1.1034              show "(\<Sum>i = 0..s. e / 2 ^ (i + 2)) < e / 2"
  1.1035                unfolding power_add divide_inverse inverse_mult_distrib
  1.1036 -              unfolding setsum_distrib_left[symmetric] setsum_distrib_right[symmetric]
  1.1037 +              unfolding sum_distrib_left[symmetric] sum_distrib_right[symmetric]
  1.1038                unfolding power_inverse [symmetric] sum_gp
  1.1039                apply(rule mult_strict_left_mono[OF _ e])
  1.1040                unfolding power2_eq_square
  1.1041 @@ -6550,10 +6550,10 @@
  1.1042              show "norm (\<Sum>(x, k)\<in>{xk \<in> p. m (fst xk) = t}. content k *\<^sub>R f (m x) x -
  1.1043                integral k (f (m x))) \<le> e / 2 ^ (t + 2)"
  1.1044                apply (rule order_trans
  1.1045 -                [of _ "norm (setsum (\<lambda>(x,k). content k *\<^sub>R f t x - integral k (f t)) {xk \<in> p. m (fst xk) = t})"])
  1.1046 +                [of _ "norm (sum (\<lambda>(x,k). content k *\<^sub>R f t x - integral k (f t)) {xk \<in> p. m (fst xk) = t})"])
  1.1047                apply (rule eq_refl)
  1.1048                apply (rule arg_cong[where f=norm])
  1.1049 -              apply (rule setsum.cong)
  1.1050 +              apply (rule sum.cong)
  1.1051                apply (rule refl)
  1.1052                defer
  1.1053                apply (rule henstock_lemma_part1)
  1.1054 @@ -6587,7 +6587,7 @@
  1.1055            apply (rule comb[of r])
  1.1056            apply (rule comb[of s])
  1.1057            apply (rule i'[unfolded real_inner_1_right])
  1.1058 -          apply (rule_tac[1-2] setsum_mono)
  1.1059 +          apply (rule_tac[1-2] sum_mono)
  1.1060            unfolding split_paired_all split_conv
  1.1061            apply (rule_tac[1-2] integral_le[OF ])
  1.1062          proof safe
  1.1063 @@ -7013,7 +7013,7 @@
  1.1064        defer
  1.1065        apply (rule d1(2)[OF conjI[OF p(1)]])
  1.1066        defer
  1.1067 -      apply (rule setsum_norm_le)
  1.1068 +      apply (rule sum_norm_le)
  1.1069      proof safe
  1.1070        fix x k
  1.1071        assume "(x, k) \<in> p"