src/HOL/Analysis/ex/Approximations.thy
changeset 63918 6bf55e6e0b75
parent 63627 6ddb43c6b711
child 64267 b9a1486e79be
     1.1 --- a/src/HOL/Analysis/ex/Approximations.thy	Mon Sep 19 12:53:30 2016 +0200
     1.2 +++ b/src/HOL/Analysis/ex/Approximations.thy	Mon Sep 19 20:06:21 2016 +0200
     1.3 @@ -30,7 +30,7 @@
     1.4        by (subst atLeast0LessThan [symmetric], subst setsum_head_upt_Suc) simp_all
     1.5      also have "(\<Sum>k=Suc 0..<Suc m. f k * x^k) = (\<Sum>k<m. f (k+1) * x^k) * x"
     1.6        by (subst setsum_shift_bounds_Suc_ivl)
     1.7 -         (simp add: setsum_left_distrib algebra_simps atLeast0LessThan power_commutes)
     1.8 +         (simp add: setsum_distrib_right algebra_simps atLeast0LessThan power_commutes)
     1.9      finally have "(\<Sum>k<Suc m. f k * x ^ k) = f 0 + (\<Sum>k<m. f (k + 1) * x ^ k) * x" .
    1.10    }
    1.11    from this[of "pred_numeral n"]
    1.12 @@ -199,7 +199,7 @@
    1.13  lemma euler_approx_aux_Suc:
    1.14    "euler_approx_aux (Suc m) = 1 + Suc m * euler_approx_aux m"
    1.15    unfolding euler_approx_aux_def
    1.16 -  by (subst setsum_right_distrib) (simp add: atLeastAtMostSuc_conv)
    1.17 +  by (subst setsum_distrib_left) (simp add: atLeastAtMostSuc_conv)
    1.18  
    1.19  lemma eval_euler_approx_aux:
    1.20    "euler_approx_aux 0 = 1"
    1.21 @@ -209,7 +209,7 @@
    1.22  proof -
    1.23    have A: "euler_approx_aux (Suc m) = 1 + Suc m * euler_approx_aux m" for m :: nat
    1.24      unfolding euler_approx_aux_def
    1.25 -    by (subst setsum_right_distrib) (simp add: atLeastAtMostSuc_conv)
    1.26 +    by (subst setsum_distrib_left) (simp add: atLeastAtMostSuc_conv)
    1.27    show ?th by (subst numeral_eq_Suc, subst A, subst numeral_eq_Suc [symmetric]) simp
    1.28  qed (simp_all add: euler_approx_aux_def)
    1.29  
    1.30 @@ -281,7 +281,7 @@
    1.31                     y_def [symmetric] d_def [symmetric])
    1.32    also have "2 * y * (\<Sum>k<n. inverse (real (2 * k + 1)) * y\<^sup>2 ^ k) = 
    1.33                 (\<Sum>k<n. 2 * y^(2*k+1) / (real (2 * k + 1)))"
    1.34 -    by (subst setsum_right_distrib, simp, subst power_mult) 
    1.35 +    by (subst setsum_distrib_left, simp, subst power_mult) 
    1.36         (simp_all add: divide_simps mult_ac power_mult)
    1.37    finally show ?case by (simp only: d_def y_def approx_def) 
    1.38  qed
    1.39 @@ -380,7 +380,7 @@
    1.40    from sums_split_initial_segment[OF this, of n]
    1.41      have "(\<lambda>i. x * ((- x\<^sup>2) ^ (i + n) / real (2 * (i + n) + 1))) sums
    1.42              (arctan x - arctan_approx n x)"
    1.43 -    by (simp add: arctan_approx_def setsum_right_distrib)
    1.44 +    by (simp add: arctan_approx_def setsum_distrib_left)
    1.45    from sums_group[OF this, of 2] assms
    1.46      have sums: "(\<lambda>k. x * (x\<^sup>2)^n * (x^4)^k * c k) sums (arctan x - arctan_approx n x)"
    1.47      by (simp add: algebra_simps power_add power_mult [symmetric] c_def)
    1.48 @@ -423,7 +423,7 @@
    1.49        by (subst atLeast0LessThan [symmetric], subst setsum_head_upt_Suc) simp_all
    1.50      also have "(\<Sum>k=Suc 0..<Suc m. inverse (f k * x^k)) = (\<Sum>k<m. inverse (f (k+1) * x^k)) / x"
    1.51        by (subst setsum_shift_bounds_Suc_ivl)
    1.52 -         (simp add: setsum_right_distrib divide_inverse algebra_simps
    1.53 +         (simp add: setsum_distrib_left divide_inverse algebra_simps
    1.54                      atLeast0LessThan power_commutes)
    1.55      finally have "(\<Sum>k<Suc m. inverse (f k) * inverse (x ^ k)) =
    1.56                        inverse (f 0) + (\<Sum>k<m. inverse (f (k + 1)) * inverse (x ^ k)) / x" by simp