src/HOL/MacLaurin.thy
changeset 57418 6ab1c7cb0b8d
parent 56536 aefb4a8da31f
child 57492 74bf65a1910a
     1.1 --- a/src/HOL/MacLaurin.thy	Fri Jun 27 22:08:55 2014 +0200
     1.2 +++ b/src/HOL/MacLaurin.thy	Sat Jun 28 09:16:42 2014 +0200
     1.3 @@ -87,7 +87,7 @@
     1.4        + (B * (t^n / real(fact n)))))"
     1.5  
     1.6    have g2: "g 0 = 0 & g h = 0"
     1.7 -    by (simp add: m f_h g_def lessThan_Suc_eq_insert_0 image_iff diff_0 setsum_reindex)
     1.8 +    by (simp add: m f_h g_def lessThan_Suc_eq_insert_0 image_iff diff_0 setsum.reindex)
     1.9  
    1.10    def difg \<equiv> "(%m t. diff m t -
    1.11      (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {..<n-m}
    1.12 @@ -101,7 +101,7 @@
    1.13      using diff_Suc m unfolding difg_def by (rule Maclaurin_lemma2)
    1.14  
    1.15    have difg_eq_0: "\<forall>m<n. difg m 0 = 0"
    1.16 -    by (auto simp: difg_def m Suc_diff_le lessThan_Suc_eq_insert_0 image_iff setsum_reindex)
    1.17 +    by (auto simp: difg_def m Suc_diff_le lessThan_Suc_eq_insert_0 image_iff setsum.reindex)
    1.18  
    1.19    have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x"
    1.20      by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp
    1.21 @@ -225,7 +225,7 @@
    1.22      by (auto simp add: power_mult_distrib[symmetric])
    1.23    moreover
    1.24    have "(SUM m<n. -1 ^ m * diff m 0 * (- h) ^ m / real (fact m)) = (SUM m<n. diff m 0 * h ^ m / real (fact m))"
    1.25 -    by (auto intro: setsum_cong simp add: power_mult_distrib[symmetric])
    1.26 +    by (auto intro: setsum.cong simp add: power_mult_distrib[symmetric])
    1.27    ultimately have " h < - t \<and>
    1.28      - t < 0 \<and>
    1.29      f h =
    1.30 @@ -419,13 +419,13 @@
    1.31  apply (simp (no_asm))
    1.32  apply (simp (no_asm) add: sin_expansion_lemma)
    1.33  apply (force intro!: derivative_eq_intros)
    1.34 -apply (subst (asm) setsum_0', clarify, case_tac "x", simp, simp)
    1.35 +apply (subst (asm) setsum.neutral, clarify, case_tac "x", simp, simp)
    1.36  apply (cases n, simp, simp)
    1.37  apply (rule ccontr, simp)
    1.38  apply (drule_tac x = x in spec, simp)
    1.39  apply (erule ssubst)
    1.40  apply (rule_tac x = t in exI, simp)
    1.41 -apply (rule setsum_cong[OF refl])
    1.42 +apply (rule setsum.cong[OF refl])
    1.43  apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
    1.44  done
    1.45  
    1.46 @@ -450,7 +450,7 @@
    1.47  apply (force intro!: derivative_eq_intros)
    1.48  apply (erule ssubst)
    1.49  apply (rule_tac x = t in exI, simp)
    1.50 -apply (rule setsum_cong[OF refl])
    1.51 +apply (rule setsum.cong[OF refl])
    1.52  apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
    1.53  done
    1.54  
    1.55 @@ -467,7 +467,7 @@
    1.56  apply (force intro!: derivative_eq_intros)
    1.57  apply (erule ssubst)
    1.58  apply (rule_tac x = t in exI, simp)
    1.59 -apply (rule setsum_cong[OF refl])
    1.60 +apply (rule setsum.cong[OF refl])
    1.61  apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
    1.62  done
    1.63  
    1.64 @@ -497,7 +497,7 @@
    1.65  apply (drule_tac x = x in spec, simp)
    1.66  apply (erule ssubst)
    1.67  apply (rule_tac x = t in exI, simp)
    1.68 -apply (rule setsum_cong[OF refl])
    1.69 +apply (rule setsum.cong[OF refl])
    1.70  apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
    1.71  done
    1.72  
    1.73 @@ -513,7 +513,7 @@
    1.74  apply (simp (no_asm) add: cos_expansion_lemma)
    1.75  apply (erule ssubst)
    1.76  apply (rule_tac x = t in exI, simp)
    1.77 -apply (rule setsum_cong[OF refl])
    1.78 +apply (rule setsum.cong[OF refl])
    1.79  apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
    1.80  done
    1.81  
    1.82 @@ -529,7 +529,7 @@
    1.83  apply (simp (no_asm) add: cos_expansion_lemma)
    1.84  apply (erule ssubst)
    1.85  apply (rule_tac x = t in exI, simp)
    1.86 -apply (rule setsum_cong[OF refl])
    1.87 +apply (rule setsum.cong[OF refl])
    1.88  apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
    1.89  done
    1.90  
    1.91 @@ -572,7 +572,7 @@
    1.92      unfolding sin_coeff_def
    1.93      apply (subst t2)
    1.94      apply (rule sin_bound_lemma)
    1.95 -    apply (rule setsum_cong[OF refl])
    1.96 +    apply (rule setsum.cong[OF refl])
    1.97      apply (subst diff_m_0, simp)
    1.98      apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
    1.99                  simp add: est mult_ac divide_inverse power_abs [symmetric] abs_mult)