# HG changeset patch # User fleury # Date 1474308381 -7200 # Node ID 6bf55e6e0b754c35b857db935227d6e1c3f8baf0 # Parent 40d1c5e7f407a63d2666d1967b13bfc0e4c89ac1 left_distrib ~> distrib_right, right_distrib ~> distrib_left diff -r 40d1c5e7f407 -r 6bf55e6e0b75 NEWS --- a/NEWS Mon Sep 19 12:53:30 2016 +0200 +++ b/NEWS Mon Sep 19 20:06:21 2016 +0200 @@ -639,6 +639,11 @@ one_step_implies_mult instead. INCOMPATIBILITY. +* The following theorems have been renamed: + setsum_left_distrib ~> setsum_distrib_right + setsum_right_distrib ~> setsum_distrib_left +INCOMPATIBILITY. + * Compound constants INFIMUM and SUPREMUM are mere abbreviations now. INCOMPATIBILITY. diff -r 40d1c5e7f407 -r 6bf55e6e0b75 src/HOL/Analysis/Bounded_Linear_Function.thy --- a/src/HOL/Analysis/Bounded_Linear_Function.thy Mon Sep 19 12:53:30 2016 +0200 +++ b/src/HOL/Analysis/Bounded_Linear_Function.thy Mon Sep 19 20:06:21 2016 +0200 @@ -352,7 +352,7 @@ apply (rule norm_blinfun_bound) apply (simp add: setsum_nonneg) apply (subst euclidean_representation[symmetric, where 'a='a]) - apply (simp only: blinfun.bilinear_simps setsum_left_distrib) + apply (simp only: blinfun.bilinear_simps setsum_distrib_right) apply (rule order.trans[OF norm_setsum setsum_mono]) apply (simp add: abs_mult mult_right_mono ac_simps Basis_le_norm) done @@ -406,7 +406,7 @@ "norm (blinfun_of_matrix a) \ (\i\Basis. \j\Basis. \a i j\)" apply (rule norm_blinfun_bound) apply (simp add: setsum_nonneg) - apply (simp only: blinfun_of_matrix_apply setsum_left_distrib) + apply (simp only: blinfun_of_matrix_apply setsum_distrib_right) apply (rule order_trans[OF norm_setsum setsum_mono]) apply (rule order_trans[OF norm_setsum setsum_mono]) apply (simp add: abs_mult mult_right_mono ac_simps Basis_le_norm) diff -r 40d1c5e7f407 -r 6bf55e6e0b75 src/HOL/Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Mon Sep 19 12:53:30 2016 +0200 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Mon Sep 19 20:06:21 2016 +0200 @@ -119,8 +119,8 @@ val ss1 = simpset_of (put_simpset HOL_basic_ss @{context} addsimps [@{thm setsum.distrib} RS sym, - @{thm setsum_subtractf} RS sym, @{thm setsum_right_distrib}, - @{thm setsum_left_distrib}, @{thm setsum_negf} RS sym]) + @{thm setsum_subtractf} RS sym, @{thm setsum_distrib_left}, + @{thm setsum_distrib_right}, @{thm setsum_negf} RS sym]) val ss2 = simpset_of (@{context} addsimps [@{thm plus_vec_def}, @{thm times_vec_def}, @@ -326,7 +326,7 @@ lemma setsum_cmul: fixes f:: "'c \ ('a::semiring_1)^'n" shows "setsum (\x. c *s f x) S = c *s setsum f S" - by (simp add: vec_eq_iff setsum_right_distrib) + by (simp add: vec_eq_iff setsum_distrib_left) lemma setsum_norm_allsubsets_bound_cart: fixes f:: "'a \ real ^'n" @@ -517,14 +517,14 @@ done lemma matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C" - apply (vector matrix_matrix_mult_def setsum_right_distrib setsum_left_distrib mult.assoc) + apply (vector matrix_matrix_mult_def setsum_distrib_left setsum_distrib_right mult.assoc) apply (subst setsum.commute) apply simp done lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x" apply (vector matrix_matrix_mult_def matrix_vector_mult_def - setsum_right_distrib setsum_left_distrib mult.assoc) + setsum_distrib_left setsum_distrib_right mult.assoc) apply (subst setsum.commute) apply simp done @@ -555,7 +555,7 @@ by (simp add: matrix_vector_mult_def inner_vec_def) lemma dot_lmul_matrix: "((x::real ^_) v* A) \ y = x \ (A *v y)" - apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib ac_simps) + apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def setsum_distrib_right setsum_distrib_left ac_simps) apply (subst setsum.commute) apply simp done @@ -630,7 +630,7 @@ lemma matrix_vector_mul_linear: "linear(\x. A *v (x::real ^ _))" by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff - field_simps setsum_right_distrib setsum.distrib) + field_simps setsum_distrib_left setsum.distrib) lemma matrix_works: assumes lf: "linear f" @@ -660,7 +660,7 @@ lemma adjoint_matrix: "adjoint(\x. (A::real^'n^'m) *v x) = (\x. transpose A *v x)" apply (rule adjoint_unique) apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def - setsum_left_distrib setsum_right_distrib) + setsum_distrib_right setsum_distrib_left) apply (subst setsum.commute) apply (auto simp add: ac_simps) done diff -r 40d1c5e7f407 -r 6bf55e6e0b75 src/HOL/Analysis/Cauchy_Integral_Theorem.thy --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Mon Sep 19 12:53:30 2016 +0200 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Mon Sep 19 20:06:21 2016 +0200 @@ -6215,7 +6215,7 @@ by (metis (no_types) dist_norm divide_eq_1_iff less_irrefl mem_ball norm_minus_commute r w) have "norm ((\kk0 < B\ apply (auto simp: geometric_sum [OF wzu_not1]) diff -r 40d1c5e7f407 -r 6bf55e6e0b75 src/HOL/Analysis/Complex_Analysis_Basics.thy --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Mon Sep 19 12:53:30 2016 +0200 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Mon Sep 19 20:06:21 2016 +0200 @@ -951,7 +951,7 @@ then have "cmod h * cmod ((\i cmod h * e" by (auto simp: antisym_conv2 mult_le_cancel_left norm_triangle_ineq2) then show "cmod ((\i e * cmod h" - by (simp add: norm_mult [symmetric] field_simps setsum_right_distrib) + by (simp add: norm_mult [symmetric] field_simps setsum_distrib_left) qed } note ** = this show ?thesis diff -r 40d1c5e7f407 -r 6bf55e6e0b75 src/HOL/Analysis/Complex_Transcendental.thy --- a/src/HOL/Analysis/Complex_Transcendental.thy Mon Sep 19 12:53:30 2016 +0200 +++ b/src/HOL/Analysis/Complex_Transcendental.thy Mon Sep 19 20:06:21 2016 +0200 @@ -597,7 +597,7 @@ text\32-bit Approximation to e\ lemma e_approx_32: "\exp(1) - 5837465777 / 2147483648\ \ (inverse(2 ^ 32)::real)" using Taylor_exp [of 1 14] exp_le - apply (simp add: setsum_left_distrib in_Reals_norm Re_exp atMost_nat_numeral fact_numeral) + apply (simp add: setsum_distrib_right in_Reals_norm Re_exp atMost_nat_numeral fact_numeral) apply (simp only: pos_le_divide_eq [symmetric], linarith) done diff -r 40d1c5e7f407 -r 6bf55e6e0b75 src/HOL/Analysis/Conformal_Mappings.thy --- a/src/HOL/Analysis/Conformal_Mappings.thy Mon Sep 19 12:53:30 2016 +0200 +++ b/src/HOL/Analysis/Conformal_Mappings.thy Mon Sep 19 20:06:21 2016 +0200 @@ -2846,7 +2846,7 @@ qed qed also have "... = c * (\p\pts. winding_number g p * residue f p)" - by (simp add: setsum_right_distrib algebra_simps) + by (simp add: setsum_distrib_left algebra_simps) finally show ?thesis unfolding c_def . qed @@ -3459,7 +3459,7 @@ qed qed then have "(\p\zeros. w p * cont p) = c * (\p\zeros. w p * h p * zorder f p)" - apply (subst setsum_right_distrib) + apply (subst setsum_distrib_left) by (simp add:algebra_simps) moreover have "(\p\poles. w p * cont p) = (\p\poles. - c * w p * h p * porder f p)" proof (rule setsum.cong[of poles poles,simplified]) @@ -3479,7 +3479,7 @@ qed qed then have "(\p\poles. w p * cont p) = - c * (\p\poles. w p * h p * porder f p)" - apply (subst setsum_right_distrib) + apply (subst setsum_distrib_left) by (simp add:algebra_simps) ultimately show ?thesis by (simp add: right_diff_distrib) qed diff -r 40d1c5e7f407 -r 6bf55e6e0b75 src/HOL/Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Mon Sep 19 12:53:30 2016 +0200 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Mon Sep 19 20:06:21 2016 +0200 @@ -523,7 +523,7 @@ qed auto then show ?thesis apply (rule_tac IA[of "s - {x}" "\y. (inverse (1 - u x) * u y)"]) - unfolding setsum_right_distrib[symmetric] + unfolding setsum_distrib_left[symmetric] using as and *** and True apply auto done @@ -536,7 +536,7 @@ then show ?thesis using as(3)[THEN bspec[where x=a], THEN bspec[where x=b]] using *** *(2) and \s \ V\ - unfolding setsum_right_distrib + unfolding setsum_distrib_left by (auto simp add: setsum_clauses(2)) qed then have "u x + (1 - u x) = 1 \ @@ -619,7 +619,7 @@ unfolding scaleR_left_distrib setsum.distrib if_smult scaleR_zero_left ** setsum.inter_restrict[OF xy, symmetric] unfolding scaleR_scaleR[symmetric] Real_Vector_Spaces.scaleR_right.setsum [symmetric] - and setsum_right_distrib[symmetric] + and setsum_distrib_left[symmetric] unfolding x y using x(1-3) y(1-3) uv apply simp @@ -1323,7 +1323,7 @@ apply (rule_tac x="s - {v}" in exI) apply (rule_tac x="\x. - (1 / u v) * u x" in exI) unfolding scaleR_scaleR[symmetric] and scaleR_right.setsum [symmetric] - unfolding setsum_right_distrib[symmetric] and setsum_diff1[OF as(1)] + unfolding setsum_distrib_left[symmetric] and setsum_diff1[OF as(1)] using as apply auto done @@ -1793,7 +1793,7 @@ apply rule unfolding * and setsum.If_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]] and setsum.reindex[OF inj] and o_def Collect_mem_eq - unfolding scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] setsum_right_distrib[symmetric] + unfolding scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] setsum_distrib_left[symmetric] proof - fix i assume i: "i \ {1..k1+k2}" @@ -1844,7 +1844,7 @@ } moreover have "(\x\s. u * ux x + v * uy x) = 1" - unfolding setsum.distrib and setsum_right_distrib[symmetric] and ux(2) uy(2) + unfolding setsum.distrib and setsum_distrib_left[symmetric] and ux(2) uy(2) using uv(3) by auto moreover have "(\x\s. (u * ux x + v * uy x) *\<^sub>R x) = u *\<^sub>R (\x\s. ux x *\<^sub>R x) + v *\<^sub>R (\x\s. uy x *\<^sub>R x)" @@ -3306,7 +3306,7 @@ have *: "\f. setsum f (s - {a}) = setsum f s - ((f a)::'b::ab_group_add)" unfolding setsum.remove[OF obt(1) \a\s\] by auto have "(\v\s. u v + t * w v) = 1" - unfolding setsum.distrib wv(1) setsum_right_distrib[symmetric] obt(5) by auto + unfolding setsum.distrib wv(1) setsum_distrib_left[symmetric] obt(5) by auto moreover have "(\v\s. u v *\<^sub>R v + (t * w v) *\<^sub>R v) - (u a *\<^sub>R a + (t * w a) *\<^sub>R a) = y" unfolding setsum.distrib obt(6) scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] wv(4) using a(2) [THEN eq_neg_iff_add_eq_0 [THEN iffD2]] by simp @@ -5279,7 +5279,7 @@ apply (rule_tac x="{v \ c. u v < 0}" in exI) apply (rule_tac x="\y. inverse (setsum u {x\c. u x > 0}) * - u y" in exI) using assms(1) unfolding scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] and z_def - apply (auto simp add: setsum_negf setsum_right_distrib[symmetric]) + apply (auto simp add: setsum_negf setsum_distrib_left[symmetric]) done moreover have "\x\{v \ c. 0 < u v}. 0 \ inverse (setsum u {x \ c. 0 < u x}) * u x" apply rule @@ -5294,7 +5294,7 @@ using assms(1) unfolding scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] and z_def using * - apply (auto simp add: setsum_negf setsum_right_distrib[symmetric]) + apply (auto simp add: setsum_negf setsum_distrib_left[symmetric]) done ultimately show ?thesis apply (rule_tac x="{v\c. u v \ 0}" in exI) @@ -5683,7 +5683,7 @@ unfolding convex_hull_indexed mem_Collect_eq by auto have "(\i = 1..k. u i * f (v i)) \ b" using setsum_mono[of "{1..k}" "\i. u i * f (v i)" "\i. u i * b"] - unfolding setsum_left_distrib[symmetric] obt(2) mult_1 + unfolding setsum_distrib_right[symmetric] obt(2) mult_1 apply (drule_tac meta_mp) apply (rule mult_left_mono) using assms(2) obt(1) @@ -9200,9 +9200,9 @@ have ge0: "\i\I. e i \ 0" using e_def xc yc uv by simp have "setsum (\i. u * c i) I = u * setsum c I" - by (simp add: setsum_right_distrib) + by (simp add: setsum_distrib_left) moreover have "setsum (\i. v * d i) I = v * setsum d I" - by (simp add: setsum_right_distrib) + by (simp add: setsum_distrib_left) ultimately have sum1: "setsum e I = 1" using e_def xc yc uv by (simp add: setsum.distrib) define q where "q i = (if e i = 0 then p i else (u * c i / e i) *\<^sub>R s i + (v * d i / e i) *\<^sub>R t i)" @@ -11857,7 +11857,7 @@ have sum_dd0: "setsum dd S = 0" unfolding dd_def using S by (simp add: sumSS' comm_monoid_add_class.setsum.distrib setsum_subtractf - algebra_simps setsum_left_distrib [symmetric] b1) + algebra_simps setsum_distrib_right [symmetric] b1) have "(\v\S. (b v * x) *\<^sub>R v) = x *\<^sub>R (\v\S. b v *\<^sub>R v)" for x by (simp add: pth_5 real_vector.scale_setsum_right mult.commute) then have *: "(\v\S. (b v * x) *\<^sub>R v) = x *\<^sub>R a" for x diff -r 40d1c5e7f407 -r 6bf55e6e0b75 src/HOL/Analysis/Derivative.thy --- a/src/HOL/Analysis/Derivative.thy Mon Sep 19 12:53:30 2016 +0200 +++ b/src/HOL/Analysis/Derivative.thy Mon Sep 19 20:06:21 2016 +0200 @@ -2244,7 +2244,7 @@ { fix n :: nat and x h :: 'a assume nx: "n \ N" "x \ s" have "norm ((\iii e" by simp hence "norm ((\i e * norm h" by (intro mult_right_mono) simp_all diff -r 40d1c5e7f407 -r 6bf55e6e0b75 src/HOL/Analysis/Determinants.thy --- a/src/HOL/Analysis/Determinants.thy Mon Sep 19 12:53:30 2016 +0200 +++ b/src/HOL/Analysis/Determinants.thy Mon Sep 19 20:06:21 2016 +0200 @@ -226,7 +226,7 @@ fixes A :: "'a::comm_ring_1^'n^'n" assumes p: "p permutes (UNIV :: 'n::finite set)" shows "det (\ i. A$p i :: 'a^'n^'n) = of_int (sign p) * det A" - apply (simp add: det_def setsum_right_distrib mult.assoc[symmetric]) + apply (simp add: det_def setsum_distrib_left mult.assoc[symmetric]) apply (subst sum_permutations_compose_right[OF p]) proof (rule setsum.cong) let ?U = "UNIV :: 'n set" @@ -372,7 +372,7 @@ fixes a b :: "'n::finite \ _ ^ 'n" shows "det((\ i. if i = k then c *s a i else b i)::'a::comm_ring_1^'n^'n) = c * det((\ i. if i = k then a i else b i)::'a::comm_ring_1^'n^'n)" - unfolding det_def vec_lambda_beta setsum_right_distrib + unfolding det_def vec_lambda_beta setsum_distrib_left proof (rule setsum.cong) let ?U = "UNIV :: 'n set" let ?pU = "{p. p permutes ?U}" @@ -645,7 +645,7 @@ lemma det_rows_mul: "det((\ i. c i *s a i)::'a::comm_ring_1^'n^'n) = setprod (\i. c i) (UNIV:: 'n set) * det((\ i. a i)::'a^'n^'n)" -proof (simp add: det_def setsum_right_distrib cong add: setprod.cong, rule setsum.cong) +proof (simp add: det_def setsum_distrib_left cong add: setprod.cong, rule setsum.cong) let ?U = "UNIV :: 'n set" let ?PU = "{p. p permutes ?U}" fix p diff -r 40d1c5e7f407 -r 6bf55e6e0b75 src/HOL/Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Mon Sep 19 12:53:30 2016 +0200 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Mon Sep 19 20:06:21 2016 +0200 @@ -461,7 +461,7 @@ by (simp add: inner_add_left setsum.distrib) show "inner (scaleR r x) y = r * inner x y" unfolding inner_vec_def - by (simp add: setsum_right_distrib) + by (simp add: setsum_distrib_left) show "0 \ inner x x" unfolding inner_vec_def by (simp add: setsum_nonneg) diff -r 40d1c5e7f407 -r 6bf55e6e0b75 src/HOL/Analysis/Gamma_Function.thy --- a/src/HOL/Analysis/Gamma_Function.thy Mon Sep 19 12:53:30 2016 +0200 +++ b/src/HOL/Analysis/Gamma_Function.thy Mon Sep 19 20:06:21 2016 +0200 @@ -450,7 +450,7 @@ (\k=Suc m..n. 2 * (norm t + (norm t)\<^sup>2) / (real_of_nat k)\<^sup>2)" using t_nz N(2) mn norm_t by (intro order.trans[OF norm_setsum setsum_mono[OF ln_Gamma_series_complex_converges_aux]]) simp_all also have "... \ 2 * (norm t + norm t^2) * (\k=Suc m..n. 1 / (of_nat k)\<^sup>2)" - by (simp add: setsum_right_distrib) + by (simp add: setsum_distrib_left) also have "... < 2 * (norm t + norm t^2) * e'" using mn z t_nz by (intro mult_strict_left_mono N mult_pos_pos add_pos_pos) simp_all also from e''_pos have "... = e * ((cmod t + (cmod t)\<^sup>2) / e'')" @@ -543,7 +543,7 @@ by (subst atLeast0LessThan [symmetric], subst setsum_shift_bounds_Suc_ivl [symmetric], subst atLeastLessThanSuc_atLeastAtMost) simp_all also have "\ = z * of_real (harm n) - (\k=1..n. ln (1 + z / of_nat k))" - by (simp add: harm_def setsum_subtractf setsum_right_distrib divide_inverse) + by (simp add: harm_def setsum_subtractf setsum_distrib_left divide_inverse) also from n have "\ - ?g n = 0" by (simp add: ln_Gamma_series_def setsum_subtractf algebra_simps Ln_of_nat) finally show "(\kk z. \ik. - of_nat n' * inverse ((z + of_nat k) ^ (n' + 1))) = (- of_nat n') * (\k. inverse ((z + of_nat k) ^ (n' + 1)))" @@ -2573,7 +2573,7 @@ proof - have "(\k=1..n. exp (z * of_real (ln (1 + 1 / of_nat k)))) = exp (z * of_real (\k = 1..n. ln (1 + 1 / real_of_nat k)))" - by (subst exp_setsum [symmetric]) (simp_all add: setsum_right_distrib) + by (subst exp_setsum [symmetric]) (simp_all add: setsum_distrib_left) also have "(\k=1..n. ln (1 + 1 / of_nat k) :: real) = ln (\k=1..n. 1 + 1 / real_of_nat k)" by (subst ln_setprod [symmetric]) (auto intro!: add_pos_nonneg) also have "(\k=1..n. 1 + 1 / of_nat k :: real) = (\k=1..n. (of_nat k + 1) / of_nat k)" diff -r 40d1c5e7f407 -r 6bf55e6e0b75 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Mon Sep 19 12:53:30 2016 +0200 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Mon Sep 19 20:06:21 2016 +0200 @@ -3756,7 +3756,7 @@ have "norm (setsum (\l. content l *\<^sub>R c) p) \ (\i\p. norm (content i *\<^sub>R c))" using norm_setsum by blast also have "... \ e * (\i\p. \content i\)" - by (simp add: setsum_right_distrib[symmetric] mult.commute assms(2) mult_right_mono setsum_nonneg) + by (simp add: setsum_distrib_left[symmetric] mult.commute assms(2) mult_right_mono setsum_nonneg) also have "... \ e * content (cbox a b)" apply (rule mult_left_mono [OF _ e]) apply (simp add: sumeq) @@ -3792,7 +3792,7 @@ apply (rule order_trans[OF setsum_mono]) apply (rule mult_left_mono[OF _ abs_ge_zero, of _ e]) apply (metis norm) - unfolding setsum_left_distrib[symmetric] + unfolding setsum_distrib_right[symmetric] using con setsum_le apply (auto simp: mult.commute intro: mult_left_mono [OF _ e]) done @@ -4697,7 +4697,7 @@ done have "norm ((\(x, k)\p. content k *\<^sub>R f x) - 0) \ setsum (\i. (real i + 1) * norm (setsum (\(x,k). content k *\<^sub>R indicator s x :: real) (q i))) {..N+1}" - unfolding real_norm_def setsum_right_distrib abs_of_nonneg[OF *] diff_0_right + unfolding real_norm_def setsum_distrib_left abs_of_nonneg[OF *] diff_0_right apply (rule order_trans) apply (rule norm_setsum) apply (subst sum_sum_product) @@ -4775,7 +4775,7 @@ done qed also have "\ < e * inverse 2 * 2" - unfolding divide_inverse setsum_right_distrib[symmetric] + unfolding divide_inverse setsum_distrib_left[symmetric] apply (rule mult_strict_left_mono) unfolding power_inverse [symmetric] lessThan_Suc_atMost[symmetric] apply (subst geometric_sum) @@ -5313,7 +5313,7 @@ show "norm ((\(x, k)\p. content k *\<^sub>R f' x) - (f b - f a)) \ e * content (cbox a b)" 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] unfolding additive_tagged_division_1[OF assms(1) as(1)[simplified box_real],of "\x. x",symmetric] - unfolding setsum_right_distrib + unfolding setsum_distrib_left defer unfolding setsum_subtractf[symmetric] proof (rule setsum_norm_le,safe) @@ -6479,7 +6479,7 @@ by arith show ?case unfolding content_real[OF assms(1)] and *[of "\x. x"] *[of f] setsum_subtractf[symmetric] split_minus - unfolding setsum_right_distrib + unfolding setsum_distrib_left apply (subst(2) pA) apply (subst pA) unfolding setsum.union_disjoint[OF pA(2-)] @@ -6548,7 +6548,7 @@ apply (unfold split_paired_all split_conv) defer unfolding setsum.union_disjoint[OF pA(2-),symmetric] pA(1)[symmetric] - unfolding setsum_right_distrib[symmetric] + unfolding setsum_distrib_left[symmetric] apply (subst additive_tagged_division_1[OF _ as(1)]) apply (rule assms) proof - @@ -8856,7 +8856,7 @@ apply rule apply (drule qq) defer - unfolding divide_inverse setsum_left_distrib[symmetric] + unfolding divide_inverse setsum_distrib_right[symmetric] unfolding divide_inverse[symmetric] using * apply (auto simp add: field_simps) done @@ -8976,7 +8976,7 @@ done have th: "op ^ x \ op + m = (\i. x^m * x^i)" by (rule ext) (simp add: power_add power_mult) - from setsum.reindex[OF i, of "op ^ x", unfolded f th setsum_right_distrib[symmetric]] + from setsum.reindex[OF i, of "op ^ x", unfolded f th setsum_distrib_left[symmetric]] have "?lhs = x^m * ((1 - x) * setsum (op ^ x) {0..n - m})" by simp then show ?thesis @@ -9164,7 +9164,7 @@ apply (rule norm_setsum) apply (rule setsum_mono) unfolding split_paired_all split_conv - unfolding split_def setsum_left_distrib[symmetric] scaleR_diff_right[symmetric] + unfolding split_def setsum_distrib_right[symmetric] scaleR_diff_right[symmetric] unfolding additive_content_tagged_division[OF p(1), unfolded split_def] proof - fix x k @@ -9201,7 +9201,7 @@ proof show "(\i = 0..s. e / 2 ^ (i + 2)) < e / 2" unfolding power_add divide_inverse inverse_mult_distrib - unfolding setsum_right_distrib[symmetric] setsum_left_distrib[symmetric] + unfolding setsum_distrib_left[symmetric] setsum_distrib_right[symmetric] unfolding power_inverse [symmetric] sum_gp apply(rule mult_strict_left_mono[OF _ e]) unfolding power2_eq_square @@ -10350,7 +10350,7 @@ by auto qed finally show "(\i\d. \content (l \ i)\ * norm (f x)) = content l *\<^sub>R norm (f x)" - unfolding setsum_left_distrib[symmetric] real_scaleR_def + unfolding setsum_distrib_right[symmetric] real_scaleR_def apply (subst(asm) additive_content_division[OF division_inter_1[OF d(1)]]) using xl(2)[unfolded uv] unfolding uv @@ -10614,7 +10614,7 @@ proof goal_cases case prems: (2 d) have "(\k\d. norm (integral k (h \ f))) \ setsum (\k. norm(integral k f)) d * b" - unfolding setsum_left_distrib + unfolding setsum_distrib_right apply (rule setsum_mono) proof goal_cases case (1 k) diff -r 40d1c5e7f407 -r 6bf55e6e0b75 src/HOL/Analysis/Homeomorphism.thy --- a/src/HOL/Analysis/Homeomorphism.thy Mon Sep 19 12:53:30 2016 +0200 +++ b/src/HOL/Analysis/Homeomorphism.thy Mon Sep 19 20:06:21 2016 +0200 @@ -1007,7 +1007,7 @@ have gf[simp]: "g (f x) = x" for x apply (rule euclidean_eqI) apply (simp add: f_def g_def inner_setsum_left scaleR_setsum_left algebra_simps) - apply (simp add: Groups_Big.setsum_right_distrib [symmetric] *) + apply (simp add: Groups_Big.setsum_distrib_left [symmetric] *) done then have "inj f" by (metis injI) have gfU: "g ` f ` U = U" diff -r 40d1c5e7f407 -r 6bf55e6e0b75 src/HOL/Analysis/L2_Norm.thy --- a/src/HOL/Analysis/L2_Norm.thy Mon Sep 19 12:53:30 2016 +0200 +++ b/src/HOL/Analysis/L2_Norm.thy Mon Sep 19 20:06:21 2016 +0200 @@ -58,7 +58,7 @@ "0 \ r \ r * setL2 f A = setL2 (\x. r * f x) A" unfolding setL2_def apply (simp add: power_mult_distrib) - apply (simp add: setsum_right_distrib [symmetric]) + apply (simp add: setsum_distrib_left [symmetric]) apply (simp add: real_sqrt_mult setsum_nonneg) done @@ -66,7 +66,7 @@ "0 \ r \ setL2 f A * r = setL2 (\x. f x * r) A" unfolding setL2_def apply (simp add: power_mult_distrib) - apply (simp add: setsum_left_distrib [symmetric]) + apply (simp add: setsum_distrib_right [symmetric]) apply (simp add: real_sqrt_mult setsum_nonneg) done diff -r 40d1c5e7f407 -r 6bf55e6e0b75 src/HOL/Analysis/Lebesgue_Measure.thy --- a/src/HOL/Analysis/Lebesgue_Measure.thy Mon Sep 19 12:53:30 2016 +0200 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy Mon Sep 19 20:06:21 2016 +0200 @@ -235,7 +235,7 @@ by auto also have "... = (\i \ S. F(r i) - F(l i)) + (epsilon / 4) * (\i \ S. (1 / 2)^i)" (is "_ = ?t + _") - by (subst setsum.distrib) (simp add: field_simps setsum_right_distrib) + by (subst setsum.distrib) (simp add: field_simps setsum_distrib_left) also have "... \ ?t + (epsilon / 4) * (\ i < Suc n. (1 / 2)^i)" apply (rule add_left_mono) apply (rule mult_left_mono) diff -r 40d1c5e7f407 -r 6bf55e6e0b75 src/HOL/Analysis/Linear_Algebra.thy --- a/src/HOL/Analysis/Linear_Algebra.thy Mon Sep 19 12:53:30 2016 +0200 +++ b/src/HOL/Analysis/Linear_Algebra.thy Mon Sep 19 20:06:21 2016 +0200 @@ -1960,7 +1960,7 @@ qed from setsum_norm_le[of _ ?g, OF th] show "norm (f x) \ ?B * norm x" - unfolding th0 setsum_left_distrib by metis + unfolding th0 setsum_distrib_right by metis qed qed @@ -2021,7 +2021,7 @@ unfolding bilinear_setsum[OF bh finite_Basis finite_Basis] .. finally have th: "norm (h x y) = \" . show "norm (h x y) \ (\i\Basis. \j\Basis. norm (h i j)) * norm x * norm y" - apply (auto simp add: setsum_left_distrib th setsum.cartesian_product) + apply (auto simp add: setsum_distrib_right th setsum.cartesian_product) apply (rule setsum_norm_le) apply simp apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] diff -r 40d1c5e7f407 -r 6bf55e6e0b75 src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy --- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Mon Sep 19 12:53:30 2016 +0200 +++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Mon Sep 19 20:06:21 2016 +0200 @@ -550,7 +550,7 @@ qed also have "\ = (\y\f`space M. (\z\g`space M. if \x\space M. y = f x \ z = g x then y * emeasure M {x\space M. g x = z} else 0))" - by (auto intro!: setsum.cong simp: setsum_right_distrib) + by (auto intro!: setsum.cong simp: setsum_distrib_left) also have "\ = ?r" by (subst setsum.commute) (auto intro!: setsum.cong simp: setsum.If_cases scaleR_setsum_right[symmetric] eq) @@ -592,7 +592,7 @@ using f by (intro simple_function_partition) auto also have "\ = c * integral\<^sup>S M f" using f unfolding simple_integral_def - by (subst setsum_right_distrib) (auto simp: mult.assoc Int_def conj_commute) + by (subst setsum_distrib_left) (auto simp: mult.assoc Int_def conj_commute) finally show ?thesis . qed diff -r 40d1c5e7f407 -r 6bf55e6e0b75 src/HOL/Analysis/Poly_Roots.thy --- a/src/HOL/Analysis/Poly_Roots.thy Mon Sep 19 12:53:30 2016 +0200 +++ b/src/HOL/Analysis/Poly_Roots.thy Mon Sep 19 20:06:21 2016 +0200 @@ -24,7 +24,7 @@ lemma setsum_power_add: fixes x :: "'a::{comm_ring,monoid_mult}" shows "(\i\I. x^(m+i)) = x^m * (\i\I. x^i)" - by (simp add: setsum_right_distrib power_add) + by (simp add: setsum_distrib_left power_add) lemma setsum_power_shift: fixes x :: "'a::{comm_ring,monoid_mult}" @@ -32,7 +32,7 @@ shows "(\i=m..n. x^i) = x^m * (\i\n-m. x^i)" proof - have "(\i=m..n. x^i) = x^m * (\i=m..n. x^(i-m))" - by (simp add: setsum_right_distrib power_add [symmetric]) + by (simp add: setsum_distrib_left power_add [symmetric]) also have "(\i=m..n. x^(i-m)) = (\i\n-m. x^i)" using \m \ n\ by (intro setsum.reindex_bij_witness[where j="\i. i - m" and i="\i. i + m"]) auto finally show ?thesis . @@ -88,7 +88,7 @@ also have "... = (\i\n. a i * (x - y) * (\ji\n. (\jji=Suc j..n. a i * y^(i - Suc j) * x^j))" by (simp add: nested_setsum_swap') finally show ?thesis . @@ -115,7 +115,7 @@ { fix z have "(\i\n. c i * z^i) - (\i\n. c i * a^i) = (z - a) * (\jk = Suc j..n. c k * a^(k - Suc j)) * z^j)" - by (simp add: sub_polyfun setsum_left_distrib) + by (simp add: sub_polyfun setsum_distrib_right) then have "(\i\n. c i * z^i) = (z - a) * (\jk = Suc j..n. c k * a^(k - Suc j)) * z^j) + (\i\n. c i * a^i)" diff -r 40d1c5e7f407 -r 6bf55e6e0b75 src/HOL/Analysis/Polytope.thy --- a/src/HOL/Analysis/Polytope.thy Mon Sep 19 12:53:30 2016 +0200 +++ b/src/HOL/Analysis/Polytope.thy Mon Sep 19 20:06:21 2016 +0200 @@ -303,7 +303,7 @@ have cge0: "\i. i \ S \ 0 \ c i" using a b u01 by (simp add: c_def) have sumc1: "setsum c S = 1" - by (simp add: c_def setsum.distrib setsum_right_distrib [symmetric] asum bsum) + by (simp add: c_def setsum.distrib setsum_distrib_left [symmetric] asum bsum) have sumci_xy: "(\i\S. c i *\<^sub>R i) = (1 - u) *\<^sub>R x + u *\<^sub>R y" apply (simp add: c_def setsum.distrib scaleR_left_distrib) by (simp only: scaleR_scaleR [symmetric] Real_Vector_Spaces.scaleR_right.setsum [symmetric] aeqx beqy) @@ -357,7 +357,7 @@ apply (rule_tac x="\i. inverse (1-k) * c i" in exI) apply auto apply (metis sumcf cge0 inverse_nonnegative_iff_nonnegative mult_nonneg_nonneg S(2) setsum_nonneg subsetCE) - apply (metis False mult.commute right_inverse right_minus_eq setsum_right_distrib sumcf) + apply (metis False mult.commute right_inverse right_minus_eq setsum_distrib_left sumcf) by (metis (mono_tags, lifting) scaleR_right.setsum scaleR_scaleR setsum.cong) with \0 < k\ have "inverse(k) *\<^sub>R (w - setsum (\i. c i *\<^sub>R i) T) \ affine hull T" by (simp add: affine_diff_divide [OF affine_affine_hull] False waff convex_hull_subset_affine_hull [THEN subsetD]) @@ -365,7 +365,7 @@ apply (simp add: weq_sumsum convex_hull_finite fin) apply (rule_tac x="\i. inverse k * c i" in exI) using \k > 0\ cge0 - apply (auto simp: scaleR_right.setsum setsum_right_distrib [symmetric] k_def [symmetric]) + apply (auto simp: scaleR_right.setsum setsum_distrib_left [symmetric] k_def [symmetric]) done ultimately show ?thesis using disj by blast diff -r 40d1c5e7f407 -r 6bf55e6e0b75 src/HOL/Analysis/Summation_Tests.thy --- a/src/HOL/Analysis/Summation_Tests.thy Mon Sep 19 12:53:30 2016 +0200 +++ b/src/HOL/Analysis/Summation_Tests.thy Mon Sep 19 20:06:21 2016 +0200 @@ -288,7 +288,7 @@ qed from this and A have "Bseq (\n. \kn. \kn. (\k=Suc 0..n. (\k=0.. m" by (simp add: n_def) from r have "r * norm (\k\n. f k) = norm (\k\n. r * f k)" - by (simp add: setsum_right_distrib[symmetric] abs_mult) + by (simp add: setsum_distrib_left[symmetric] abs_mult) also from n have "{..n} = {..m} \ {Suc m..n}" by auto hence "(\k\n. r * f k) = (\k\{..m} \ {Suc m..n}. r * f k)" by (simp only:) also have "\ = (\k\m. r * f k) + (\k=Suc m..n. r * f k)" diff -r 40d1c5e7f407 -r 6bf55e6e0b75 src/HOL/Analysis/Weierstrass_Theorems.thy --- a/src/HOL/Analysis/Weierstrass_Theorems.thy Mon Sep 19 12:53:30 2016 +0200 +++ b/src/HOL/Analysis/Weierstrass_Theorems.thy Mon Sep 19 20:06:21 2016 +0200 @@ -38,7 +38,7 @@ lemma sum_k_Bernstein [simp]: "(\k = 0..n. real k * Bernstein n k x) = of_nat n * x" apply (subst binomial_deriv1 [of n x "1-x", simplified, symmetric]) - apply (simp add: setsum_left_distrib) + apply (simp add: setsum_distrib_right) apply (auto simp: Bernstein_def algebra_simps realpow_num_eq_if intro!: setsum.cong) done @@ -46,7 +46,7 @@ proof - have "(\ k = 0..n. real k * (real k - 1) * Bernstein n k x) = real_of_nat n * real_of_nat (n - Suc 0) * x\<^sup>2" apply (subst binomial_deriv2 [of n x "1-x", simplified, symmetric]) - apply (simp add: setsum_left_distrib) + apply (simp add: setsum_distrib_right) apply (rule setsum.cong [OF refl]) apply (simp add: Bernstein_def power2_eq_square algebra_simps) apply (rename_tac k) @@ -98,7 +98,7 @@ by (simp add: algebra_simps power2_eq_square) have "(\ k = 0..n. (k - n * x)\<^sup>2 * Bernstein n k x) = n * x * (1 - x)" apply (simp add: * setsum.distrib) - apply (simp add: setsum_right_distrib [symmetric] mult.assoc) + apply (simp add: setsum_distrib_left [symmetric] mult.assoc) apply (simp add: algebra_simps power2_eq_square) done then have "(\ k = 0..n. (k - n * x)\<^sup>2 * Bernstein n k x)/n^2 = x * (1 - x) / n" @@ -138,14 +138,14 @@ qed } note * = this have "\f x - (\ k = 0..n. f(k / n) * Bernstein n k x)\ \ \\ k = 0..n. (f x - f(k / n)) * Bernstein n k x\" - by (simp add: setsum_subtractf setsum_right_distrib [symmetric] algebra_simps) + by (simp add: setsum_subtractf setsum_distrib_left [symmetric] algebra_simps) also have "... \ (\ k = 0..n. (e/2 + (2 * M / d\<^sup>2) * (x - k / n)\<^sup>2) * Bernstein n k x)" apply (rule order_trans [OF setsum_abs setsum_mono]) using * apply (simp add: abs_mult Bernstein_nonneg x mult_right_mono) done also have "... \ e/2 + (2 * M) / (d\<^sup>2 * n)" - apply (simp only: setsum.distrib Rings.semiring_class.distrib_right setsum_right_distrib [symmetric] mult.assoc sum_bern) + apply (simp only: setsum.distrib Rings.semiring_class.distrib_right setsum_distrib_left [symmetric] mult.assoc sum_bern) using \d>0\ x apply (simp add: divide_simps Mge0 mult_le_one mult_left_le) done diff -r 40d1c5e7f407 -r 6bf55e6e0b75 src/HOL/Analysis/ex/Approximations.thy --- a/src/HOL/Analysis/ex/Approximations.thy Mon Sep 19 12:53:30 2016 +0200 +++ b/src/HOL/Analysis/ex/Approximations.thy Mon Sep 19 20:06:21 2016 +0200 @@ -30,7 +30,7 @@ by (subst atLeast0LessThan [symmetric], subst setsum_head_upt_Suc) simp_all also have "(\k=Suc 0..kkkk2 ^ k) = (\ki. x * ((- x\<^sup>2) ^ (i + n) / real (2 * (i + n) + 1))) sums (arctan x - arctan_approx n x)" - by (simp add: arctan_approx_def setsum_right_distrib) + by (simp add: arctan_approx_def setsum_distrib_left) from sums_group[OF this, of 2] assms have sums: "(\k. x * (x\<^sup>2)^n * (x^4)^k * c k) sums (arctan x - arctan_approx n x)" by (simp add: algebra_simps power_add power_mult [symmetric] c_def) @@ -423,7 +423,7 @@ by (subst atLeast0LessThan [symmetric], subst setsum_head_upt_Suc) simp_all also have "(\k=Suc 0..kkk = (\k=0..n. of_nat (n choose k) * a^(k+1) * b^(n-k)) + (\k=0..n. of_nat (n choose k) * a^k * b^(n - k + 1))" - by (auto simp add: setsum_right_distrib ac_simps) + by (auto simp add: setsum_distrib_left ac_simps) also have "\ = (\k=0..n. of_nat (n choose k) * a^k * b^(n + 1 - k)) + (\k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n + 1 - k))" by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le field_simps del: setsum_cl_ivl_Suc) @@ -463,7 +463,7 @@ also have "\ = (\i\n. of_nat (n choose i) + (-1) ^ i * of_nat (n choose i))" by (simp add: setsum.distrib) also have "\ = 2 * (\i\n. if even i then of_nat (n choose i) else 0)" - by (subst setsum_right_distrib, intro setsum.cong) simp_all + by (subst setsum_distrib_left, intro setsum.cong) simp_all finally show ?thesis .. qed @@ -477,7 +477,7 @@ also have "\ = (\i\n. of_nat (n choose i) - (-1) ^ i * of_nat (n choose i))" by (simp add: setsum_subtractf) also have "\ = 2 * (\i\n. if odd i then of_nat (n choose i) else 0)" - by (subst setsum_right_distrib, intro setsum.cong) simp_all + by (subst setsum_distrib_left, intro setsum.cong) simp_all finally show ?thesis .. qed @@ -914,7 +914,7 @@ have "(\i\n. i * (n choose i)) = (\i\Suc m. i * (Suc m choose i))" by (simp add: Suc) also have "\ = Suc m * 2 ^ m" - by (simp only: setsum_atMost_Suc_shift Suc_times_binomial setsum_right_distrib[symmetric]) + by (simp only: setsum_atMost_Suc_shift Suc_times_binomial setsum_distrib_left[symmetric]) (simp add: choose_row_sum') finally show ?thesis using Suc by simp @@ -934,9 +934,9 @@ (\i\Suc m. (-1) ^ i * of_nat i * of_nat (Suc m choose i))" by (simp add: Suc) also have "\ = (\i\m. (-1) ^ (Suc i) * of_nat (Suc i * (Suc m choose Suc i)))" - by (simp only: setsum_atMost_Suc_shift setsum_right_distrib[symmetric] mult_ac of_nat_mult) simp + by (simp only: setsum_atMost_Suc_shift setsum_distrib_left[symmetric] mult_ac of_nat_mult) simp also have "\ = - of_nat (Suc m) * (\i\m. (-1) ^ i * of_nat (m choose i))" - by (subst setsum_right_distrib, rule setsum.cong[OF refl], subst Suc_times_binomial) + by (subst setsum_distrib_left, rule setsum.cong[OF refl], subst Suc_times_binomial) (simp add: algebra_simps) also have "(\i\m. (-1 :: 'a) ^ i * of_nat ((m choose i))) = 0" using choose_alternating_sum[OF \m > 0\] by simp @@ -978,7 +978,7 @@ by (subst setsum_atMost_Suc_shift) (simp add: ring_distribs setsum.distrib) also have "(\i\n. of_nat (n choose i) * pochhammer a (Suc i) * pochhammer b (n - i)) = a * pochhammer ((a + 1) + b) n" - by (subst Suc) (simp add: setsum_right_distrib pochhammer_rec mult_ac) + by (subst Suc) (simp add: setsum_distrib_left pochhammer_rec mult_ac) also have "(\i\n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) + pochhammer b (Suc n) = (\i=0..Suc n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))" @@ -992,7 +992,7 @@ also have "\ = (\i\n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc (n - i)))" by (intro setsum.cong) (simp_all add: Suc_diff_le) also have "\ = b * pochhammer (a + (b + 1)) n" - by (subst Suc) (simp add: setsum_right_distrib mult_ac pochhammer_rec) + by (subst Suc) (simp add: setsum_distrib_left mult_ac pochhammer_rec) also have "a * pochhammer ((a + 1) + b) n + b * pochhammer (a + (b + 1)) n = pochhammer (a + b) (Suc n)" by (simp add: pochhammer_rec algebra_simps) @@ -1263,9 +1263,9 @@ by (simp only:) qed also have "\ + ?B = y * (\k=1..mm. (G mm k)) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)" - unfolding G_def by (subst setsum_right_distrib) (simp add: algebra_simps) + unfolding G_def by (subst setsum_distrib_left) (simp add: algebra_simps) also have "(\k=0..mm. (of_nat mm + r gchoose k) * x^(Suc k) * y^(mm - k)) = x * (S mm)" - unfolding S_def by (subst setsum_right_distrib) (simp add: atLeast0AtMost algebra_simps) + unfolding S_def by (subst setsum_distrib_left) (simp add: atLeast0AtMost algebra_simps) also have "(G (Suc mm) 0) = y * (G mm 0)" by (simp add: G_def) finally have "S (Suc mm) = @@ -1283,7 +1283,7 @@ also have "(x + y) * S mm + \ = (x + y) * ?rhs mm + (- r gchoose (Suc mm)) * (- x)^Suc mm" unfolding S_def by (subst Suc.IH) simp also have "(x + y) * ?rhs mm = (\n\mm. ((- r gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n)))" - by (subst setsum_right_distrib, rule setsum.cong) (simp_all add: Suc_diff_le) + by (subst setsum_distrib_left, rule setsum.cong) (simp_all add: Suc_diff_le) also have "\ + (-r gchoose (Suc mm)) * (-x)^Suc mm = (\n\Suc mm. (- r gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n))" by simp @@ -1345,7 +1345,7 @@ using gbinomial_partial_sum_poly_xpos[where x="1" and y="1" and r="of_nat m + 1" and m="m"] by (simp add: add_ac) also have "\ = 2 ^ m * (\k\m. (of_nat (m + k) gchoose k) / 2 ^ k)" - by (subst setsum_right_distrib) (simp add: algebra_simps power_diff) + by (subst setsum_distrib_left) (simp add: algebra_simps power_diff) finally show ?thesis by (subst (asm) mult_left_cancel) simp_all qed @@ -1444,7 +1444,7 @@ by simp also have "\ = nat (\I | I \ A \ I \ {}. (\_\\I. (- 1) ^ (card I + 1)))" (is "_ = nat ?rhs") - by (subst setsum_right_distrib) simp + by (subst setsum_distrib_left) simp also have "?rhs = (\(I, _)\Sigma {I. I \ A \ I \ {}} Inter. (- 1) ^ (card I + 1))" using assms by (subst setsum.Sigma) auto also have "\ = (\(x, I)\(SIGMA x:UNIV. {I. I \ A \ I \ {} \ x \ \I}). (- 1) ^ (card I + 1))" @@ -1474,7 +1474,7 @@ also have "\ = (\i=1..card A. (\I|I \ A \ card I = i \ x \ \I. (- 1) ^ (i + 1)))" using assms by (subst setsum.Sigma) auto also have "\ = (\i=1..card A. (- 1) ^ (i + 1) * (\I|I \ A \ card I = i \ x \ \I. 1))" - by (subst setsum_right_distrib) simp + by (subst setsum_distrib_left) simp also have "\ = (\i=1..card K. (- 1) ^ (i + 1) * (\I|I \ K \ card I = i. 1))" (is "_ = ?rhs") proof (rule setsum.mono_neutral_cong_right[rule_format]) @@ -1508,7 +1508,7 @@ also have "\ = (\i = 0..card K. (- 1) * ((- 1) ^ i * int (card K choose i))) + 1" using K by (subst n_subsets[symmetric]) simp_all also have "\ = - (\i = 0..card K. (- 1) ^ i * int (card K choose i)) + 1" - by (subst setsum_right_distrib[symmetric]) simp + by (subst setsum_distrib_left[symmetric]) simp also have "\ = - ((-1 + 1) ^ card K) + 1" by (subst binomial_ring) (simp add: ac_simps) also have "\ = 1" diff -r 40d1c5e7f407 -r 6bf55e6e0b75 src/HOL/Decision_Procs/Approximation.thy --- 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: "\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 "\ 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) \ ?S n" using bounds(1) \0 \