src/HOL/MacLaurin.thy

   moreover
   from INIT2 have intvl: "{..<n - m} = insert 0 (Suc ` {..<n - Suc m})" and "0 < n - m"
     unfolding atLeast0LessThan[symmetric] by auto
   have "(\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / fact x) =
       (\<Sum>x<n - Suc m. real (Suc x) * t ^ x * diff (Suc m + x) 0 / fact (Suc x))"
-    unfolding intvl by (subst setsum.insert) (auto simp add: setsum.reindex)
+    unfolding intvl by (subst sum.insert) (auto simp add: sum.reindex)
   moreover
   have fact_neq_0: "\<And>x. (fact x) + real x * (fact x) \<noteq> 0"
     by (metis add_pos_pos fact_gt_zero less_add_same_cancel1 less_add_same_cancel2
         less_numeral_extra(3) mult_less_0_iff of_nat_less_0_iff)
   have "\<And>x. (Suc x) * t ^ x * diff (Suc m + x) 0 / fact (Suc x) = diff (Suc m + x) 0 * t^x / fact x"

     and n: "0 < n"
     and diff_0: "diff 0 = f"
     and diff_Suc: "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
   shows
     "\<exists>t::real. 0 < t \<and> t < h \<and>
-      f h = setsum (\<lambda>m. (diff m 0 / fact m) * h ^ m) {..<n} + (diff n t / fact n) * h ^ n"
+      f h = sum (\<lambda>m. (diff m 0 / fact m) * h ^ m) {..<n} + (diff n t / fact n) * h ^ n"
 proof -
   from n obtain m where m: "n = Suc m"
     by (cases n) (simp add: n)
   from m have "m < n" by simp
 
   obtain B where f_h: "f h = (\<Sum>m<n. diff m 0 / fact m * h ^ m) + B * (h ^ n / fact n)"
     using Maclaurin_lemma [OF h] ..
 
   define g where [abs_def]: "g t =
-    f t - (setsum (\<lambda>m. (diff m 0 / fact m) * t^m) {..<n} + B * (t^n / fact n))" for t
+    f t - (sum (\<lambda>m. (diff m 0 / fact m) * t^m) {..<n} + B * (t^n / fact n))" for t
   have g2: "g 0 = 0" "g h = 0"
-    by (simp_all add: m f_h g_def lessThan_Suc_eq_insert_0 image_iff diff_0 setsum.reindex)
+    by (simp_all add: m f_h g_def lessThan_Suc_eq_insert_0 image_iff diff_0 sum.reindex)
 
   define difg where [abs_def]: "difg m t =
-    diff m t - (setsum (\<lambda>p. (diff (m + p) 0 / fact p) * (t ^ p)) {..<n-m} +
+    diff m t - (sum (\<lambda>p. (diff (m + p) 0 / fact p) * (t ^ p)) {..<n-m} +
       B * ((t ^ (n - m)) / fact (n - m)))" for m t
   have difg_0: "difg 0 = g"
     by (simp add: difg_def g_def diff_0)
   have difg_Suc: "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t"
     using diff_Suc m unfolding difg_def [abs_def] by (rule Maclaurin_lemma2)
   have difg_eq_0: "\<forall>m<n. difg m 0 = 0"
-    by (auto simp: difg_def m Suc_diff_le lessThan_Suc_eq_insert_0 image_iff setsum.reindex)
+    by (auto simp: difg_def m Suc_diff_le lessThan_Suc_eq_insert_0 image_iff sum.reindex)
   have isCont_difg: "\<And>m x. m < n \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> h \<Longrightarrow> isCont (difg m) x"
     by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp
   have differentiable_difg: "\<And>m x. m < n \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> h \<Longrightarrow> difg m differentiable (at x)"
     by (rule differentiableI [OF difg_Suc [rule_format]]) simp
   have difg_Suc_eq_0:

     by blast
   moreover have "(- 1) ^ n * diff n (- t) * (- h) ^ n / fact n = diff n (- t) * h ^ n / fact n"
     by (auto simp: power_mult_distrib[symmetric])
   moreover
     have "(\<Sum>m<n. (- 1) ^ m * diff m 0 * (- h) ^ m / fact m) = (\<Sum>m<n. diff m 0 * h ^ m / fact m)"
-    by (auto intro: setsum.cong simp add: power_mult_distrib[symmetric])
+    by (auto intro: sum.cong simp add: power_mult_distrib[symmetric])
   ultimately have "h < - t \<and> - t < 0 \<and>
     f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n (- t) / (fact n) * h ^ n"
     by auto
   then show ?thesis ..
 qed

     [where f = sin and n = n and x = x and diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)"]
   apply safe
       apply simp
      apply (simp add: sin_expansion_lemma del: of_nat_Suc)
      apply (force intro!: derivative_eq_intros)
-    apply (subst (asm) setsum.neutral; auto)
+    apply (subst (asm) sum.neutral; auto)
    apply (rule ccontr)
    apply simp
    apply (drule_tac x = x in spec)
    apply simp
   apply (erule ssubst)
   apply (rule_tac x = t in exI)
   apply simp
-  apply (rule setsum.cong[OF refl])
+  apply (rule sum.cong[OF refl])
   apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
   done
 
 lemma Maclaurin_sin_expansion:
   "\<exists>t. sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n"

    apply (simp (no_asm) add: sin_expansion_lemma del: of_nat_Suc)
    apply (force intro!: derivative_eq_intros)
   apply (erule ssubst)
   apply (rule_tac x = t in exI)
   apply simp
-  apply (rule setsum.cong[OF refl])
+  apply (rule sum.cong[OF refl])
   apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
   done
 
 lemma Maclaurin_sin_expansion4:
   "0 < x \<Longrightarrow>

    apply (simp (no_asm) add: sin_expansion_lemma del: of_nat_Suc)
    apply (force intro!: derivative_eq_intros)
   apply (erule ssubst)
   apply (rule_tac x = t in exI)
   apply simp
-  apply (rule setsum.cong[OF refl])
+  apply (rule sum.cong[OF refl])
   apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
   done
 
 
 subsection \<open>Maclaurin Expansion for Cosine Function\<close>

   apply safe
       apply simp
      apply (simp add: cos_expansion_lemma del: of_nat_Suc)
     apply (cases n)
      apply simp
-    apply (simp del: setsum_lessThan_Suc)
+    apply (simp del: sum_lessThan_Suc)
    apply (rule ccontr)
    apply simp
    apply (drule_tac x = x in spec)
    apply simp
   apply (erule ssubst)
   apply (rule_tac x = t in exI)
   apply simp
-  apply (rule setsum.cong[OF refl])
+  apply (rule sum.cong[OF refl])
   apply (auto simp add: cos_coeff_def cos_zero_iff elim: evenE)
   done
 
 lemma Maclaurin_cos_expansion2:
   "0 < x \<Longrightarrow> n > 0 \<Longrightarrow>

     apply simp
    apply (simp add: cos_expansion_lemma del: of_nat_Suc)
   apply (erule ssubst)
   apply (rule_tac x = t in exI)
   apply simp
-  apply (rule setsum.cong[OF refl])
+  apply (rule sum.cong[OF refl])
   apply (auto simp: cos_coeff_def cos_zero_iff elim: evenE)
   done
 
 lemma Maclaurin_minus_cos_expansion:
   "x < 0 \<Longrightarrow> n > 0 \<Longrightarrow>

     apply simp
    apply (simp add: cos_expansion_lemma del: of_nat_Suc)
   apply (erule ssubst)
   apply (rule_tac x = t in exI)
   apply simp
-  apply (rule setsum.cong[OF refl])
+  apply (rule sum.cong[OF refl])
   apply (auto simp: cos_coeff_def cos_zero_iff elim: evenE)
   done
 
 
 (* Version for ln(1 +/- x). Where is it?? *)

     done
   show ?thesis
     unfolding sin_coeff_def
     apply (subst t2)
     apply (rule sin_bound_lemma)
-     apply (rule setsum.cong[OF refl])
+     apply (rule sum.cong[OF refl])
      apply (subst diff_m_0, simp)
     using est
     apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
         simp: ac_simps divide_inverse power_abs [symmetric] abs_mult)
     done