--- a/src/HOL/Decision_Procs/Approximation.thy Mon Sep 19 12:53:30 2016 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Mon Sep 19 20:06:21 2016 +0200
@@ -31,7 +31,7 @@
have shift_pow: "\<And>i. - (x * ((-1)^i * a (Suc i) * x ^ i)) = (-1)^(Suc i) * a (Suc i) * x ^ (Suc i)"
by auto
show ?thesis
- unfolding setsum_right_distrib shift_pow uminus_add_conv_diff [symmetric] setsum_negf[symmetric]
+ unfolding setsum_distrib_left shift_pow uminus_add_conv_diff [symmetric] setsum_negf[symmetric]
setsum_head_upt_Suc[OF zero_less_Suc]
setsum.reindex[OF inj_Suc, unfolded comp_def, symmetric, of "\<lambda> n. (-1)^n *a n * x^n"] by auto
qed
@@ -514,7 +514,7 @@
proof -
have "(sqrt y * lb_arctan_horner prec n 1 y) \<le> ?S n"
using bounds(1) \<open>0 \<le> sqrt y\<close>
- apply (simp only: power_add power_one_right mult.assoc[symmetric] setsum_left_distrib[symmetric])
+ apply (simp only: power_add power_one_right mult.assoc[symmetric] setsum_distrib_right[symmetric])
apply (simp only: mult.commute[where 'a=real] mult.commute[of _ "2::nat"] power_mult)
apply (auto intro!: mult_left_mono)
done
@@ -527,7 +527,7 @@
have "arctan (sqrt y) \<le> ?S (Suc n)" using arctan_bounds ..
also have "\<dots> \<le> (sqrt y * ub_arctan_horner prec (Suc n) 1 y)"
using bounds(2)[of "Suc n"] \<open>0 \<le> sqrt y\<close>
- apply (simp only: power_add power_one_right mult.assoc[symmetric] setsum_left_distrib[symmetric])
+ apply (simp only: power_add power_one_right mult.assoc[symmetric] setsum_distrib_right[symmetric])
apply (simp only: mult.commute[where 'a=real] mult.commute[of _ "2::nat"] power_mult)
apply (auto intro!: mult_left_mono)
done
@@ -1212,7 +1212,7 @@
from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0,
OF \<open>0 \<le> real_of_float (x * x)\<close> f_eq lb_sin_cos_aux.simps ub_sin_cos_aux.simps]
show "?lb" and "?ub" using \<open>0 \<le> real_of_float x\<close>
- apply (simp_all only: power_add power_one_right mult.assoc[symmetric] setsum_left_distrib[symmetric])
+ apply (simp_all only: power_add power_one_right mult.assoc[symmetric] setsum_distrib_right[symmetric])
apply (simp_all only: mult.commute[where 'a=real] of_nat_fact)
apply (auto intro!: mult_left_mono simp add: power_mult power2_eq_square[of "real_of_float x"])
done
@@ -2193,7 +2193,7 @@
let "?s n" = "(- 1) ^ n * (1 / real (1 + n)) * (real_of_float x)^(Suc n)"
have "?lb \<le> setsum ?s {0 ..< 2 * ev}"
- unfolding power_Suc2 mult.assoc[symmetric] times_float.rep_eq setsum_left_distrib[symmetric]
+ unfolding power_Suc2 mult.assoc[symmetric] times_float.rep_eq setsum_distrib_right[symmetric]
unfolding mult.commute[of "real_of_float x"] ev
using horner_bounds(1)[where G="\<lambda> i k. Suc k" and F="\<lambda>x. x" and f="\<lambda>x. x"
and lb="\<lambda>n i k x. lb_ln_horner prec n k x"
@@ -2208,7 +2208,7 @@
have "?ln \<le> setsum ?s {0 ..< 2 * od + 1}"
using ln_bounds(2)[OF \<open>0 \<le> real_of_float x\<close> \<open>real_of_float x < 1\<close>] by auto
also have "\<dots> \<le> ?ub"
- unfolding power_Suc2 mult.assoc[symmetric] times_float.rep_eq setsum_left_distrib[symmetric]
+ unfolding power_Suc2 mult.assoc[symmetric] times_float.rep_eq setsum_distrib_right[symmetric]
unfolding mult.commute[of "real_of_float x"] od
using horner_bounds(2)[where G="\<lambda> i k. Suc k" and F="\<lambda>x. x" and f="\<lambda>x. x" and lb="\<lambda>n i k x. lb_ln_horner prec n k x" and ub="\<lambda>n i k x. ub_ln_horner prec n k x" and j'=1 and n="2*od+1",
OF \<open>0 \<le> real_of_float x\<close> refl lb_ln_horner.simps ub_ln_horner.simps] \<open>0 \<le> real_of_float x\<close>
@@ -4019,7 +4019,7 @@
inverse (real (\<Prod> j \<in> {k..<k+Suc n}. j)) * ?f (Suc n) t * (xs!x - c)^Suc n" (is "_ = ?T")
unfolding funpow_Suc C_def[symmetric] setsum_move0 setprod_head_Suc
by (auto simp add: algebra_simps)
- (simp only: mult.left_commute [of _ "inverse (real k)"] setsum_right_distrib [symmetric])
+ (simp only: mult.left_commute [of _ "inverse (real k)"] setsum_distrib_left [symmetric])
finally have "?T \<in> {l .. u}" .
}
thus ?thesis using DERIV by blast