Renamed {left,right}_distrib to distrib_{right,left}.
authorwebertj
Fri Oct 19 15:12:52 2012 +0200 (2012-10-19)
changeset 49962a8cc904a6820
parent 49961 d3d2b78b1c19
child 49963 326f87427719
Renamed {left,right}_distrib to distrib_{right,left}.
NEWS
src/HOL/Algebra/IntRing.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Big_Operators.thy
src/HOL/Code_Numeral.thy
src/HOL/Complex.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/Polynomial_List.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/Divides.thy
src/HOL/GCD.thy
src/HOL/Hahn_Banach/Hahn_Banach.thy
src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
src/HOL/Int.thy
src/HOL/Library/Extended_Nat.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/FrechetDeriv.thy
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/Library/Inner_Product.thy
src/HOL/Library/Kleene_Algebra.thy
src/HOL/Library/ListVector.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/Product_Vector.thy
src/HOL/Library/Univ_Poly.thy
src/HOL/List.thy
src/HOL/Log.thy
src/HOL/MacLaurin.thy
src/HOL/Metis_Examples/Binary_Tree.thy
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/L2_Norm.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/NSA/CLim.thy
src/HOL/NSA/HDeriv.thy
src/HOL/NSA/HyperDef.thy
src/HOL/NSA/NSComplex.thy
src/HOL/NSA/StarDef.thy
src/HOL/Nat.thy
src/HOL/NthRoot.thy
src/HOL/Num.thy
src/HOL/Number_Theory/Binomial.thy
src/HOL/Old_Number_Theory/EvenOdd.thy
src/HOL/Old_Number_Theory/Finite2.thy
src/HOL/Old_Number_Theory/Gauss.thy
src/HOL/Old_Number_Theory/IntPrimes.thy
src/HOL/Old_Number_Theory/Pocklington.thy
src/HOL/Presburger.thy
src/HOL/Quickcheck_Narrowing.thy
src/HOL/Quotient_Examples/Quotient_Int.thy
src/HOL/Quotient_Examples/Quotient_Rat.thy
src/HOL/RComplete.thy
src/HOL/Rat.thy
src/HOL/RealDef.thy
src/HOL/RealVector.thy
src/HOL/Rings.thy
src/HOL/Transcendental.thy
src/HOL/Word/Misc_Numeric.thy
src/HOL/Word/WordBitwise.thy
src/HOL/ex/BT.thy
src/HOL/ex/Dedekind_Real.thy
src/HOL/ex/Gauge_Integration.thy
src/HOL/ex/Numeral_Representation.thy
     1.1 --- a/NEWS	Fri Oct 19 10:46:42 2012 +0200
     1.2 +++ b/NEWS	Fri Oct 19 15:12:52 2012 +0200
     1.3 @@ -76,7 +76,6 @@
     1.4  written just "typedef t = A".  INCOMPATIBILITY, need to adapt theories
     1.5  accordingly.
     1.6  
     1.7 -
     1.8  * Theory "Library/Multiset":
     1.9  
    1.10    - Renamed constants
    1.11 @@ -142,6 +141,13 @@
    1.12  
    1.13      INCOMPATIBILITY.
    1.14  
    1.15 +* HOL/Rings: renamed lemmas
    1.16 +
    1.17 +left_distrib ~> distrib_right
    1.18 +right_distrib ~> distrib_left
    1.19 +
    1.20 +in class semiring.  INCOMPATIBILITY.
    1.21 +
    1.22  * HOL/BNF: New (co)datatype package based on bounded natural
    1.23  functors with support for mixed, nested recursion and interesting
    1.24  non-free datatypes.
     2.1 --- a/src/HOL/Algebra/IntRing.thy	Fri Oct 19 10:46:42 2012 +0200
     2.2 +++ b/src/HOL/Algebra/IntRing.thy	Fri Oct 19 15:12:52 2012 +0200
     2.3 @@ -35,7 +35,7 @@
     2.4    apply (rule abelian_groupI, simp_all)
     2.5    defer 1
     2.6    apply (rule comm_monoidI, simp_all)
     2.7 - apply (rule left_distrib)
     2.8 + apply (rule distrib_right)
     2.9  apply (fast intro: left_minus)
    2.10  done
    2.11  
    2.12 @@ -165,7 +165,7 @@
    2.13      and "a_inv \<Z> x = - x"
    2.14      and "a_minus \<Z> x y = x - y"
    2.15  proof -
    2.16 -  show "domain \<Z>" by unfold_locales (auto simp: left_distrib right_distrib)
    2.17 +  show "domain \<Z>" by unfold_locales (auto simp: distrib_right distrib_left)
    2.18  qed (simp
    2.19      add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq int_a_inv_eq int_a_minus_eq)+
    2.20  
     3.1 --- a/src/HOL/Algebra/UnivPoly.thy	Fri Oct 19 10:46:42 2012 +0200
     3.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Fri Oct 19 15:12:52 2012 +0200
     3.3 @@ -1818,7 +1818,7 @@
     3.4  
     3.5  lemma INTEG_cring: "cring INTEG"
     3.6    by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
     3.7 -    left_minus left_distrib)
     3.8 +    left_minus distrib_right)
     3.9  
    3.10  lemma INTEG_id_eval:
    3.11    "UP_pre_univ_prop INTEG INTEG id"
     4.1 --- a/src/HOL/Big_Operators.thy	Fri Oct 19 10:46:42 2012 +0200
     4.2 +++ b/src/HOL/Big_Operators.thy	Fri Oct 19 15:12:52 2012 +0200
     4.3 @@ -699,7 +699,7 @@
     4.4    proof induct
     4.5      case empty thus ?case by simp
     4.6    next
     4.7 -    case (insert x A) thus ?case by (simp add: right_distrib)
     4.8 +    case (insert x A) thus ?case by (simp add: distrib_left)
     4.9    qed
    4.10  next
    4.11    case False thus ?thesis by (simp add: setsum_def)
    4.12 @@ -713,7 +713,7 @@
    4.13    proof induct
    4.14      case empty thus ?case by simp
    4.15    next
    4.16 -    case (insert x A) thus ?case by (simp add: left_distrib)
    4.17 +    case (insert x A) thus ?case by (simp add: distrib_right)
    4.18    qed
    4.19  next
    4.20    case False thus ?thesis by (simp add: setsum_def)
     5.1 --- a/src/HOL/Code_Numeral.thy	Fri Oct 19 10:46:42 2012 +0200
     5.2 +++ b/src/HOL/Code_Numeral.thy	Fri Oct 19 15:12:52 2012 +0200
     5.3 @@ -153,7 +153,7 @@
     5.4    "n < m \<longleftrightarrow> nat_of n < nat_of m"
     5.5  
     5.6  instance proof
     5.7 -qed (auto simp add: code_numeral left_distrib intro: mult_commute)
     5.8 +qed (auto simp add: code_numeral distrib_right intro: mult_commute)
     5.9  
    5.10  end
    5.11  
     6.1 --- a/src/HOL/Complex.thy	Fri Oct 19 10:46:42 2012 +0200
     6.2 +++ b/src/HOL/Complex.thy	Fri Oct 19 15:12:52 2012 +0200
     6.3 @@ -141,7 +141,7 @@
     6.4  
     6.5  instance
     6.6    by intro_classes (simp_all add: complex_mult_def
     6.7 -    right_distrib left_distrib right_diff_distrib left_diff_distrib
     6.8 +    distrib_left distrib_right right_diff_distrib left_diff_distrib
     6.9      complex_inverse_def complex_divide_def
    6.10      power2_eq_square add_divide_distrib [symmetric]
    6.11      complex_eq_iff)
    6.12 @@ -206,9 +206,9 @@
    6.13  proof
    6.14    fix a b :: real and x y :: complex
    6.15    show "scaleR a (x + y) = scaleR a x + scaleR a y"
    6.16 -    by (simp add: complex_eq_iff right_distrib)
    6.17 +    by (simp add: complex_eq_iff distrib_left)
    6.18    show "scaleR (a + b) x = scaleR a x + scaleR b x"
    6.19 -    by (simp add: complex_eq_iff left_distrib)
    6.20 +    by (simp add: complex_eq_iff distrib_right)
    6.21    show "scaleR a (scaleR b x) = scaleR (a * b) x"
    6.22      by (simp add: complex_eq_iff mult_assoc)
    6.23    show "scaleR 1 x = x"
    6.24 @@ -297,7 +297,7 @@
    6.25         (simp add: real_sqrt_sum_squares_triangle_ineq)
    6.26    show "norm (scaleR r x) = \<bar>r\<bar> * norm x"
    6.27      by (induct x)
    6.28 -       (simp add: power_mult_distrib right_distrib [symmetric] real_sqrt_mult)
    6.29 +       (simp add: power_mult_distrib distrib_left [symmetric] real_sqrt_mult)
    6.30    show "norm (x * y) = norm x * norm y"
    6.31      by (induct x, induct y)
    6.32         (simp add: real_sqrt_mult [symmetric] power2_eq_square algebra_simps)
    6.33 @@ -730,7 +730,7 @@
    6.34      unfolding z b_def rcis_def using `r \<noteq> 0`
    6.35      by (simp add: of_real_def sgn_scaleR sgn_if, simp add: cis_def)
    6.36    have cis_2pi_nat: "\<And>n. cis (2 * pi * real_of_nat n) = 1"
    6.37 -    by (induct_tac n, simp_all add: right_distrib cis_mult [symmetric],
    6.38 +    by (induct_tac n, simp_all add: distrib_left cis_mult [symmetric],
    6.39        simp add: cis_def)
    6.40    have cis_2pi_int: "\<And>x. cis (2 * pi * real_of_int x) = 1"
    6.41      by (case_tac x rule: int_diff_cases,
     7.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Fri Oct 19 10:46:42 2012 +0200
     7.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Oct 19 15:12:52 2012 +0200
     7.3 @@ -305,7 +305,7 @@
     7.4    finally have "sqrt x < (?b + x / ?b)/2" using sqrt_ub_pos_pos_1[OF Suc _ `0 < real x`] by auto
     7.5    also have "\<dots> \<le> (?b + (float_divr prec x ?b))/2" by (rule divide_right_mono, auto simp add: float_divr)
     7.6    also have "\<dots> = (Float 1 -1) * (?b + (float_divr prec x ?b))" by simp
     7.7 -  finally show ?case unfolding sqrt_iteration.simps Let_def right_distrib .
     7.8 +  finally show ?case unfolding sqrt_iteration.simps Let_def distrib_left .
     7.9  qed
    7.10  
    7.11  lemma sqrt_iteration_lower_bound: assumes "0 < real x"
    7.12 @@ -955,7 +955,7 @@
    7.13        using Maclaurin_sin_expansion3[OF `0 < 2 * n + 1` `0 < real x`]
    7.14        unfolding sin_coeff_def by auto
    7.15  
    7.16 -    have "?rest = cos t * -1^n" unfolding sin_add cos_add real_of_nat_add left_distrib right_distrib by auto
    7.17 +    have "?rest = cos t * -1^n" unfolding sin_add cos_add real_of_nat_add distrib_right distrib_left by auto
    7.18      moreover
    7.19      have "t \<le> pi / 2" using `t < real x` and `x \<le> pi / 2` by auto
    7.20      hence "0 \<le> cos t" using `0 < t` and cos_ge_zero by auto
    7.21 @@ -1173,7 +1173,7 @@
    7.22  proof (induct n arbitrary: x)
    7.23    case (Suc n)
    7.24    have split_pi_off: "x + (Suc n) * (2 * pi) = (x + n * (2 * pi)) + 2 * pi"
    7.25 -    unfolding Suc_eq_plus1 real_of_nat_add real_of_one left_distrib by auto
    7.26 +    unfolding Suc_eq_plus1 real_of_nat_add real_of_one distrib_right by auto
    7.27    show ?case unfolding split_pi_off using Suc by auto
    7.28  qed auto
    7.29  
    7.30 @@ -1714,7 +1714,7 @@
    7.31  lemma ln_add: assumes "0 < x" and "0 < y" shows "ln (x + y) = ln x + ln (1 + y / x)"
    7.32  proof -
    7.33    have "x \<noteq> 0" using assms by auto
    7.34 -  have "x + y = x * (1 + y / x)" unfolding right_distrib times_divide_eq_right nonzero_mult_divide_cancel_left[OF `x \<noteq> 0`] by auto
    7.35 +  have "x + y = x * (1 + y / x)" unfolding distrib_left times_divide_eq_right nonzero_mult_divide_cancel_left[OF `x \<noteq> 0`] by auto
    7.36    moreover
    7.37    have "0 < y / x" using assms divide_pos_pos by auto
    7.38    hence "0 < 1 + y / x" by auto
     8.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Fri Oct 19 10:46:42 2012 +0200
     8.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Fri Oct 19 15:12:52 2012 +0200
     8.3 @@ -413,7 +413,7 @@
     8.4  apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
     8.5   apply (case_tac "n1 = n2")
     8.6    apply(simp_all add: algebra_simps)
     8.7 -apply(simp add: left_distrib[symmetric])
     8.8 +apply(simp add: distrib_right[symmetric])
     8.9  done
    8.10  
    8.11  lemma numadd_nb: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
    8.12 @@ -727,7 +727,7 @@
    8.13        by (simp add: Let_def split_def)
    8.14      from abj 3 m0 have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \<and> ?N ?b" by blast
    8.15      from th have "?I x (CN 0 n a') = ?I x (CN 0 (i+?j) ?b)" by simp
    8.16 -    also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))" by (simp add: left_distrib)
    8.17 +    also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))" by (simp add: distrib_right)
    8.18    finally have "?I x (CN 0 n a') = ?I  x (CN 0 i a)" using th2 by simp
    8.19    with th2 th have ?case using m0 by blast} 
    8.20  ultimately show ?case by blast
    8.21 @@ -754,7 +754,7 @@
    8.22    with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
    8.23    from abjs 5 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
    8.24    from th3[simplified] th2[simplified] th[simplified] show ?case 
    8.25 -    by (simp add: left_distrib)
    8.26 +    by (simp add: distrib_right)
    8.27  next
    8.28    case (6 s t n a)
    8.29    let ?ns = "fst (zsplit0 s)"
    8.30 @@ -779,7 +779,7 @@
    8.31      by (simp add: Let_def split_def)
    8.32    from abj 7 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
    8.33    hence "?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)" by simp
    8.34 -  also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: right_distrib)
    8.35 +  also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: distrib_left)
    8.36    finally show ?case using th th2 by simp
    8.37  qed
    8.38  
     9.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Fri Oct 19 10:46:42 2012 +0200
     9.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Fri Oct 19 15:12:52 2012 +0200
     9.3 @@ -569,7 +569,7 @@
     9.4  apply (induct t s rule: numadd.induct, simp_all add: Let_def)
     9.5  apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
     9.6  apply (case_tac "n1 = n2", simp_all add: algebra_simps)
     9.7 -by (simp only: left_distrib[symmetric],simp)
     9.8 +by (simp only: distrib_right[symmetric],simp)
     9.9  
    9.10  lemma numadd_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
    9.11  by (induct t s rule: numadd.induct, auto simp add: Let_def)
    9.12 @@ -937,7 +937,7 @@
    9.13      by (simp add: Let_def split_def algebra_simps)
    9.14    also have "\<dots> = Inum bs a + Inum bs b" using 2 by (cases "rsplit0 a") auto
    9.15    finally show ?case using nb by simp 
    9.16 -qed (auto simp add: Let_def split_def algebra_simps, simp add: right_distrib[symmetric])
    9.17 +qed (auto simp add: Let_def split_def algebra_simps, simp add: distrib_left[symmetric])
    9.18  
    9.19      (* Linearize a formula*)
    9.20  definition
    10.1 --- a/src/HOL/Decision_Procs/MIR.thy	Fri Oct 19 10:46:42 2012 +0200
    10.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Fri Oct 19 15:12:52 2012 +0200
    10.3 @@ -743,11 +743,11 @@
    10.4  apply (induct t s rule: numadd.induct, simp_all add: Let_def)
    10.5   apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
    10.6    apply (case_tac "n1 = n2", simp_all add: algebra_simps)
    10.7 -  apply (simp only: left_distrib[symmetric])
    10.8 +  apply (simp only: distrib_right[symmetric])
    10.9   apply simp
   10.10  apply (case_tac "lex_bnd t1 t2", simp_all)
   10.11   apply (case_tac "c1+c2 = 0")
   10.12 -  by (case_tac "t1 = t2", simp_all add: algebra_simps left_distrib[symmetric] real_of_int_mult[symmetric] real_of_int_add[symmetric]del: real_of_int_mult real_of_int_add left_distrib)
   10.13 +  by (case_tac "t1 = t2", simp_all add: algebra_simps distrib_right[symmetric] real_of_int_mult[symmetric] real_of_int_add[symmetric]del: real_of_int_mult real_of_int_add distrib_right)
   10.14  
   10.15  lemma numadd_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
   10.16  by (induct t s rule: numadd.induct, auto simp add: Let_def)
   10.17 @@ -1493,7 +1493,7 @@
   10.18    with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
   10.19    from abjs 6  have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
   10.20    from th3[simplified] th2[simplified] th[simplified] show ?case 
   10.21 -    by (simp add: left_distrib)
   10.22 +    by (simp add: distrib_right)
   10.23  next
   10.24    case (7 s t n a)
   10.25    let ?ns = "fst (zsplit0 s)"
   10.26 @@ -1518,7 +1518,7 @@
   10.27      by (simp add: Let_def split_def)
   10.28    from abj 8 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
   10.29    hence "?I x (Mul i t) = (real i) * ?I x (CN 0 ?nt ?at)" by simp
   10.30 -  also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: right_distrib)
   10.31 +  also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: distrib_left)
   10.32    finally show ?case using th th2 by simp
   10.33  next
   10.34    case (9 t n a)
    11.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Oct 19 10:46:42 2012 +0200
    11.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Oct 19 15:12:52 2012 +0200
    11.3 @@ -224,7 +224,7 @@
    11.4  apply (induct t s rule: tmadd.induct, simp_all add: Let_def)
    11.5  apply (case_tac "c1 +\<^sub>p c2 = 0\<^sub>p",case_tac "n1 \<le> n2", simp_all)
    11.6  apply (case_tac "n1 = n2", simp_all add: field_simps)
    11.7 -apply (simp only: right_distrib[symmetric]) 
    11.8 +apply (simp only: distrib_left[symmetric]) 
    11.9  by (auto simp del: polyadd simp add: polyadd[symmetric])
   11.10  
   11.11  lemma tmadd_nb0[simp]: "\<lbrakk> tmbound0 t ; tmbound0 s\<rbrakk> \<Longrightarrow> tmbound0 (tmadd (t,s))"
   11.12 @@ -358,7 +358,7 @@
   11.13    apply (simp add: Let_def split_def field_simps)
   11.14    apply (simp add: Let_def split_def field_simps)
   11.15    apply (simp add: Let_def split_def field_simps)
   11.16 -  apply (simp add: Let_def split_def mult_assoc right_distrib[symmetric])
   11.17 +  apply (simp add: Let_def split_def mult_assoc distrib_left[symmetric])
   11.18    apply (simp add: Let_def split_def field_simps)
   11.19    apply (simp add: Let_def split_def field_simps)
   11.20    done
   11.21 @@ -1933,7 +1933,7 @@
   11.22      also have "\<dots> \<longleftrightarrow> 2*?d * (?a * (-?s / (2*?d)) + ?r) = 0"
   11.23        using d mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
   11.24      also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * (2*?d / (2*?d)) + 2*?d*?r= 0"
   11.25 -      by (simp add: field_simps right_distrib[of "2*?d"] del: right_distrib)
   11.26 +      by (simp add: field_simps distrib_left[of "2*?d"] del: distrib_left)
   11.27      
   11.28      also have "\<dots> \<longleftrightarrow> - (?a * ?s) + 2*?d*?r = 0" using d by simp 
   11.29      finally have ?thesis using c d 
   11.30 @@ -1947,7 +1947,7 @@
   11.31      also have "\<dots> \<longleftrightarrow> 2*?c * (?a * (-?t / (2*?c)) + ?r) = 0" 
   11.32        using c mult_cancel_left[of "2*?c" "(?a * (-?t / (2*?c)) + ?r)" 0] by simp
   11.33      also have "\<dots> \<longleftrightarrow> (?a * -?t)* (2*?c) / (2*?c) + 2*?c*?r= 0"
   11.34 -      by (simp add: field_simps right_distrib[of "2*?c"] del: right_distrib)
   11.35 +      by (simp add: field_simps distrib_left[of "2*?c"] del: distrib_left)
   11.36      also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2*?c*?r = 0" using c by simp 
   11.37      finally have ?thesis using c d 
   11.38        by (simp add: r[of "- (?t/ (2*?c))"] msubsteq_def Let_def evaldjf_ex)
   11.39 @@ -1964,7 +1964,7 @@
   11.40        using c d mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
   11.41      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r =0" 
   11.42        using nonzero_mult_divide_cancel_left [OF dc] c d
   11.43 -      by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
   11.44 +      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
   11.45      finally  have ?thesis using c d 
   11.46        by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubsteq_def Let_def evaldjf_ex field_simps)
   11.47    }
   11.48 @@ -2015,7 +2015,7 @@
   11.49      also have "\<dots> \<longleftrightarrow> 2*?d * (?a * (-?s / (2*?d)) + ?r) \<noteq> 0" 
   11.50        using d mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
   11.51      also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * (2*?d / (2*?d)) + 2*?d*?r\<noteq> 0"
   11.52 -      by (simp add: field_simps right_distrib[of "2*?d"] del: right_distrib)
   11.53 +      by (simp add: field_simps distrib_left[of "2*?d"] del: distrib_left)
   11.54      
   11.55      also have "\<dots> \<longleftrightarrow> - (?a * ?s) + 2*?d*?r \<noteq> 0" using d by simp 
   11.56      finally have ?thesis using c d 
   11.57 @@ -2029,7 +2029,7 @@
   11.58      also have "\<dots> \<longleftrightarrow> 2*?c * (?a * (-?t / (2*?c)) + ?r) \<noteq> 0" 
   11.59        using c mult_cancel_left[of "2*?c" "(?a * (-?t / (2*?c)) + ?r)" 0] by simp
   11.60      also have "\<dots> \<longleftrightarrow> (?a * -?t)* (2*?c) / (2*?c) + 2*?c*?r \<noteq> 0"
   11.61 -      by (simp add: field_simps right_distrib[of "2*?c"] del: right_distrib)
   11.62 +      by (simp add: field_simps distrib_left[of "2*?c"] del: distrib_left)
   11.63      also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2*?c*?r \<noteq> 0" using c by simp 
   11.64      finally have ?thesis using c d 
   11.65        by (simp add: r[of "- (?t/ (2*?c))"] msubstneq_def Let_def evaldjf_ex)
   11.66 @@ -2046,7 +2046,7 @@
   11.67        using c d mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
   11.68      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \<noteq> 0" 
   11.69        using nonzero_mult_divide_cancel_left[OF dc] c d
   11.70 -      by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
   11.71 +      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
   11.72      finally  have ?thesis using c d 
   11.73        by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstneq_def Let_def evaldjf_ex field_simps)
   11.74    }
   11.75 @@ -2112,7 +2112,7 @@
   11.76        using dc' dc'' mult_less_cancel_left_disj[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
   11.77      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r < 0" 
   11.78        using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
   11.79 -      by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
   11.80 +      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
   11.81      finally  have ?thesis using dc c d  nc nd dc'
   11.82        by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) 
   11.83    }
   11.84 @@ -2134,7 +2134,7 @@
   11.85        using dc' order_less_not_sym[OF dc'] mult_less_cancel_left_disj[of "2 * ?c * ?d" 0 "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r"] by simp
   11.86      also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2*?c*?d*?r < 0" 
   11.87        using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
   11.88 -      by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
   11.89 +      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
   11.90      finally  have ?thesis using dc c d  nc nd
   11.91        by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) 
   11.92    }
   11.93 @@ -2149,7 +2149,7 @@
   11.94        using c mult_less_cancel_left_disj[of "2 * ?c" "?a* (- ?t / (2*?c))+ ?r" 0] c' c'' order_less_not_sym[OF c''] by simp
   11.95      also have "\<dots> \<longleftrightarrow> - ?a*?t+  2*?c *?r < 0" 
   11.96        using nonzero_mult_divide_cancel_left[OF c'] c
   11.97 -      by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
   11.98 +      by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
   11.99      finally have ?thesis using c d nc nd 
  11.100        by(simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
  11.101    }
  11.102 @@ -2163,7 +2163,7 @@
  11.103        using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c'' mult_less_cancel_left_disj[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"] by simp
  11.104      also have "\<dots> \<longleftrightarrow> ?a*?t -  2*?c *?r < 0" 
  11.105        using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
  11.106 -        by (simp add: algebra_simps diff_divide_distrib del:  left_distrib)
  11.107 +        by (simp add: algebra_simps diff_divide_distrib del:  distrib_right)
  11.108      finally have ?thesis using c d nc nd 
  11.109        by(simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
  11.110    }
  11.111 @@ -2179,7 +2179,7 @@
  11.112        using d mult_less_cancel_left_disj[of "2 * ?d" "?a* (- ?s / (2*?d))+ ?r" 0] d' d'' order_less_not_sym[OF d''] by simp
  11.113      also have "\<dots> \<longleftrightarrow> - ?a*?s+  2*?d *?r < 0" 
  11.114        using nonzero_mult_divide_cancel_left[OF d'] d
  11.115 -      by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
  11.116 +      by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
  11.117      finally have ?thesis using c d nc nd 
  11.118        by(simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
  11.119    }
  11.120 @@ -2193,7 +2193,7 @@
  11.121        using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d'' mult_less_cancel_left_disj[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"] by simp
  11.122      also have "\<dots> \<longleftrightarrow> ?a*?s -  2*?d *?r < 0" 
  11.123        using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
  11.124 -        by (simp add: algebra_simps diff_divide_distrib del:  left_distrib)
  11.125 +        by (simp add: algebra_simps diff_divide_distrib del:  distrib_right)
  11.126      finally have ?thesis using c d nc nd 
  11.127        by(simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
  11.128    }
  11.129 @@ -2258,7 +2258,7 @@
  11.130        using dc' dc'' mult_le_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
  11.131      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r <= 0" 
  11.132        using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
  11.133 -      by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
  11.134 +      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
  11.135      finally  have ?thesis using dc c d  nc nd dc'
  11.136        by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) 
  11.137    }
  11.138 @@ -2280,7 +2280,7 @@
  11.139        using dc' order_less_not_sym[OF dc'] mult_le_cancel_left[of "2 * ?c * ?d" 0 "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r"] by simp
  11.140      also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2*?c*?d*?r <= 0" 
  11.141        using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
  11.142 -      by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
  11.143 +      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
  11.144      finally  have ?thesis using dc c d  nc nd
  11.145        by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) 
  11.146    }
  11.147 @@ -2295,7 +2295,7 @@
  11.148        using c mult_le_cancel_left[of "2 * ?c" "?a* (- ?t / (2*?c))+ ?r" 0] c' c'' order_less_not_sym[OF c''] by simp
  11.149      also have "\<dots> \<longleftrightarrow> - ?a*?t+  2*?c *?r <= 0" 
  11.150        using nonzero_mult_divide_cancel_left[OF c'] c
  11.151 -      by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
  11.152 +      by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
  11.153      finally have ?thesis using c d nc nd 
  11.154        by(simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
  11.155    }
  11.156 @@ -2309,7 +2309,7 @@
  11.157        using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c'' mult_le_cancel_left[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"] by simp
  11.158      also have "\<dots> \<longleftrightarrow> ?a*?t -  2*?c *?r <= 0" 
  11.159        using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
  11.160 -        by (simp add: algebra_simps diff_divide_distrib del:  left_distrib)
  11.161 +        by (simp add: algebra_simps diff_divide_distrib del:  distrib_right)
  11.162      finally have ?thesis using c d nc nd 
  11.163        by(simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
  11.164    }
  11.165 @@ -2325,7 +2325,7 @@
  11.166        using d mult_le_cancel_left[of "2 * ?d" "?a* (- ?s / (2*?d))+ ?r" 0] d' d'' order_less_not_sym[OF d''] by simp
  11.167      also have "\<dots> \<longleftrightarrow> - ?a*?s+  2*?d *?r <= 0" 
  11.168        using nonzero_mult_divide_cancel_left[OF d'] d
  11.169 -      by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
  11.170 +      by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
  11.171      finally have ?thesis using c d nc nd 
  11.172        by(simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
  11.173    }
  11.174 @@ -2339,7 +2339,7 @@
  11.175        using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d'' mult_le_cancel_left[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"] by simp
  11.176      also have "\<dots> \<longleftrightarrow> ?a*?s -  2*?d *?r <= 0" 
  11.177        using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
  11.178 -        by (simp add: algebra_simps diff_divide_distrib del:  left_distrib)
  11.179 +        by (simp add: algebra_simps diff_divide_distrib del:  distrib_right)
  11.180      finally have ?thesis using c d nc nd 
  11.181        by(simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
  11.182    }
    12.1 --- a/src/HOL/Decision_Procs/Polynomial_List.thy	Fri Oct 19 10:46:42 2012 +0200
    12.2 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Fri Oct 19 15:12:52 2012 +0200
    12.3 @@ -128,7 +128,7 @@
    12.4       "\<forall>q. a %* ( p +++ q) = (a %* p +++ a %* q)"
    12.5  apply (induct "p", simp, clarify) 
    12.6  apply (case_tac "q")
    12.7 -apply (simp_all add: right_distrib)
    12.8 +apply (simp_all add: distrib_left)
    12.9  done
   12.10  
   12.11  lemma pmult_by_x[simp]: "[0, 1] *** t = ((0)#t)"
   12.12 @@ -142,13 +142,13 @@
   12.13  apply (subgoal_tac "\<forall>p2. poly (p1 +++ p2) x = poly (p1) x + poly (p2) x")
   12.14  apply (induct_tac [2] "p1", auto)
   12.15  apply (case_tac "p2")
   12.16 -apply (auto simp add: right_distrib)
   12.17 +apply (auto simp add: distrib_left)
   12.18  done
   12.19  
   12.20  lemma poly_cmult: "poly (c %* p) x = c * poly p x"
   12.21  apply (induct "p") 
   12.22  apply (case_tac [2] "x=0")
   12.23 -apply (auto simp add: right_distrib mult_ac)
   12.24 +apply (auto simp add: distrib_left mult_ac)
   12.25  done
   12.26  
   12.27  lemma poly_minus: "poly (-- p) x = - (poly p x)"
   12.28 @@ -162,7 +162,7 @@
   12.29  apply (induct "p1")
   12.30  apply (auto simp add: poly_cmult)
   12.31  apply (case_tac p1)
   12.32 -apply (auto simp add: poly_cmult poly_add left_distrib right_distrib mult_ac)
   12.33 +apply (auto simp add: poly_cmult poly_add distrib_right distrib_left mult_ac)
   12.34  done
   12.35  
   12.36  lemma poly_exp: "poly (p %^ n) (x::'a::comm_ring_1) = (poly p x) ^ n"
   12.37 @@ -206,7 +206,7 @@
   12.38  
   12.39  
   12.40  lemma poly_linear_divides: "(poly p a = 0) = ((p = []) | (\<exists>q. p = [-a, 1] *** q))"
   12.41 -apply (auto simp add: poly_add poly_cmult right_distrib)
   12.42 +apply (auto simp add: poly_add poly_cmult distrib_left)
   12.43  apply (case_tac "p", simp) 
   12.44  apply (cut_tac h = aa and t = list and a = a in poly_linear_rem, safe)
   12.45  apply (case_tac "q", auto)
   12.46 @@ -408,7 +408,7 @@
   12.47  by (auto simp add: field_simps poly_add poly_minus_def fun_eq poly_cmult)
   12.48  
   12.49  lemma poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))"
   12.50 -by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult right_distrib)
   12.51 +by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult distrib_left)
   12.52  
   12.53  lemma poly_mult_left_cancel: "(poly (p *** q) = poly (p *** r)) = (poly p = poly ([]::('a::{idom, ring_char_0}) list) | poly q = poly r)"
   12.54  apply (rule_tac p1 = "p *** q" in poly_add_minus_zero_iff [THEN subst])
   12.55 @@ -464,9 +464,9 @@
   12.56  text{*Basics of divisibility.*}
   12.57  
   12.58  lemma poly_primes: "([a, (1::'a::idom)] divides (p *** q)) = ([a, 1] divides p | [a, 1] divides q)"
   12.59 -apply (auto simp add: divides_def fun_eq poly_mult poly_add poly_cmult left_distrib [symmetric])
   12.60 +apply (auto simp add: divides_def fun_eq poly_mult poly_add poly_cmult distrib_right [symmetric])
   12.61  apply (drule_tac x = "-a" in spec)
   12.62 -apply (auto simp add: poly_linear_divides poly_add poly_cmult left_distrib [symmetric])
   12.63 +apply (auto simp add: poly_linear_divides poly_add poly_cmult distrib_right [symmetric])
   12.64  apply (rule_tac x = "qa *** q" in exI)
   12.65  apply (rule_tac [2] x = "p *** qa" in exI)
   12.66  apply (auto simp add: poly_add poly_mult poly_cmult mult_ac)
   12.67 @@ -501,7 +501,7 @@
   12.68     "[| p divides q; p divides r |] ==> p divides (q +++ r)"
   12.69  apply (simp add: divides_def, auto)
   12.70  apply (rule_tac x = "qa +++ qaa" in exI)
   12.71 -apply (auto simp add: poly_add fun_eq poly_mult right_distrib)
   12.72 +apply (auto simp add: poly_add fun_eq poly_mult distrib_left)
   12.73  done
   12.74  
   12.75  lemma poly_divides_diff:
   12.76 @@ -557,7 +557,7 @@
   12.77  apply (unfold divides_def)
   12.78  apply (rule_tac x = q in exI)
   12.79  apply (induct_tac "n", simp)
   12.80 -apply (simp (no_asm_simp) add: poly_add poly_cmult poly_mult right_distrib mult_ac)
   12.81 +apply (simp (no_asm_simp) add: poly_add poly_cmult poly_mult distrib_left mult_ac)
   12.82  apply safe
   12.83  apply (subgoal_tac "poly (mulexp n [- a, 1] q) \<noteq> poly ([- a, 1] %^ Suc n *** qa)") 
   12.84  apply simp 
    13.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Fri Oct 19 10:46:42 2012 +0200
    13.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Fri Oct 19 15:12:52 2012 +0200
    13.3 @@ -304,7 +304,7 @@
    13.4  qed auto
    13.5  
    13.6  lemma polyadd[simp]: "Ipoly bs (polyadd p q) = Ipoly bs p + Ipoly bs q"
    13.7 -by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps right_distrib[symmetric] simp del: right_distrib)
    13.8 +by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left)
    13.9  
   13.10  lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd p q)"
   13.11    using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
    14.1 --- a/src/HOL/Divides.thy	Fri Oct 19 10:46:42 2012 +0200
    14.2 +++ b/src/HOL/Divides.thy	Fri Oct 19 15:12:52 2012 +0200
    14.3 @@ -66,7 +66,7 @@
    14.4      "\<dots> = (c + a div b) * b + (a + c * b) mod b"
    14.5        by (simp add: algebra_simps)
    14.6    finally have "a = a div b * b + (a + c * b) mod b"
    14.7 -    by (simp add: add_commute [of a] add_assoc left_distrib)
    14.8 +    by (simp add: add_commute [of a] add_assoc distrib_right)
    14.9    then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
   14.10      by (simp add: mod_div_equality)
   14.11    then show ?thesis by simp
   14.12 @@ -1274,9 +1274,9 @@
   14.13   prefer 2 apply (simp add: right_diff_distrib)
   14.14  apply (subgoal_tac "0 < b * (1 + q - q') ")
   14.15  apply (erule_tac [2] order_le_less_trans)
   14.16 - prefer 2 apply (simp add: right_diff_distrib right_distrib)
   14.17 + prefer 2 apply (simp add: right_diff_distrib distrib_left)
   14.18  apply (subgoal_tac "b * q' < b * (1 + q) ")
   14.19 - prefer 2 apply (simp add: right_diff_distrib right_distrib)
   14.20 + prefer 2 apply (simp add: right_diff_distrib distrib_left)
   14.21  apply (simp add: mult_less_cancel_left)
   14.22  done
   14.23  
   14.24 @@ -1332,11 +1332,11 @@
   14.25    apply (induct a b rule: posDivAlg.induct)
   14.26    apply auto
   14.27    apply (simp add: divmod_int_rel_def)
   14.28 -  apply (subst posDivAlg_eqn, simp add: right_distrib)
   14.29 +  apply (subst posDivAlg_eqn, simp add: distrib_left)
   14.30    apply (case_tac "a < b")
   14.31    apply simp_all
   14.32    apply (erule splitE)
   14.33 -  apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
   14.34 +  apply (auto simp add: distrib_left Let_def mult_ac mult_2_right)
   14.35    done
   14.36  
   14.37  
   14.38 @@ -1366,7 +1366,7 @@
   14.39    apply (case_tac "a + b < (0\<Colon>int)")
   14.40    apply simp_all
   14.41    apply (erule splitE)
   14.42 -  apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
   14.43 +  apply (auto simp add: distrib_left Let_def mult_ac mult_2_right)
   14.44    done
   14.45  
   14.46  
   14.47 @@ -1732,7 +1732,7 @@
   14.48       "[| 0 \<le> b'*q' + r'; r' < b';  0 < b' |] ==> 0 \<le> (q'::int)"
   14.49  apply (subgoal_tac "0 < b'* (q' + 1) ")
   14.50   apply (simp add: zero_less_mult_iff)
   14.51 -apply (simp add: right_distrib)
   14.52 +apply (simp add: distrib_left)
   14.53  done
   14.54  
   14.55  lemma zdiv_mono2_lemma:
   14.56 @@ -1744,7 +1744,7 @@
   14.57   apply (simp add: mult_less_cancel_left)
   14.58  apply (subgoal_tac "b*q = r' - r + b'*q'")
   14.59   prefer 2 apply simp
   14.60 -apply (simp (no_asm_simp) add: right_distrib)
   14.61 +apply (simp (no_asm_simp) add: distrib_left)
   14.62  apply (subst add_commute, rule add_less_le_mono, arith)
   14.63  apply (rule mult_right_mono, auto)
   14.64  done
   14.65 @@ -1773,7 +1773,7 @@
   14.66  apply (frule q_neg_lemma, assumption+) 
   14.67  apply (subgoal_tac "b*q' < b* (q + 1) ")
   14.68   apply (simp add: mult_less_cancel_left)
   14.69 -apply (simp add: right_distrib)
   14.70 +apply (simp add: distrib_left)
   14.71  apply (subgoal_tac "b*q' \<le> b'*q'")
   14.72   prefer 2 apply (simp add: mult_right_mono_neg, arith)
   14.73  done
   14.74 @@ -1795,7 +1795,7 @@
   14.75  lemma zmult1_lemma:
   14.76       "[| divmod_int_rel b c (q, r) |]  
   14.77        ==> divmod_int_rel (a * b) c (a*q + a*r div c, a*r mod c)"
   14.78 -by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_distrib mult_ac)
   14.79 +by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left mult_ac)
   14.80  
   14.81  lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
   14.82  apply (case_tac "c = 0", simp)
   14.83 @@ -1807,7 +1807,7 @@
   14.84  lemma zadd1_lemma:
   14.85       "[| divmod_int_rel a c (aq, ar);  divmod_int_rel b c (bq, br) |]  
   14.86        ==> divmod_int_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
   14.87 -by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_distrib)
   14.88 +by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left)
   14.89  
   14.90  (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
   14.91  lemma zdiv_zadd1_eq:
   14.92 @@ -1900,7 +1900,7 @@
   14.93  lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); 0 < c |]  
   14.94        ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
   14.95  by (auto simp add: mult_ac divmod_int_rel_def linorder_neq_iff
   14.96 -                   zero_less_mult_iff right_distrib [symmetric] 
   14.97 +                   zero_less_mult_iff distrib_left [symmetric] 
   14.98                     zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm)
   14.99  
  14.100  lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"
    15.1 --- a/src/HOL/GCD.thy	Fri Oct 19 10:46:42 2012 +0200
    15.2 +++ b/src/HOL/GCD.thy	Fri Oct 19 15:12:52 2012 +0200
    15.3 @@ -1199,7 +1199,7 @@
    15.4            from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
    15.5              by simp
    15.6            hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
    15.7 -            by (simp only: mult_assoc right_distrib)
    15.8 +            by (simp only: mult_assoc distrib_left)
    15.9            hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
   15.10              by algebra
   15.11            hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
    16.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Fri Oct 19 10:46:42 2012 +0200
    16.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Fri Oct 19 15:12:52 2012 +0200
    16.3 @@ -411,7 +411,7 @@
    16.4        from x y have "\<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>" ..
    16.5        with a have " \<parallel>f\<parallel>\<hyphen>F * \<parallel>x + y\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>F * (\<parallel>x\<parallel> + \<parallel>y\<parallel>)"
    16.6          by (simp add: mult_left_mono)
    16.7 -      also have "\<dots> = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel> + \<parallel>f\<parallel>\<hyphen>F * \<parallel>y\<parallel>" by (simp only: right_distrib)
    16.8 +      also have "\<dots> = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel> + \<parallel>f\<parallel>\<hyphen>F * \<parallel>y\<parallel>" by (simp only: distrib_left)
    16.9        also have "\<dots> = p x + p y" by (simp only: p_def)
   16.10        finally show ?thesis .
   16.11      qed
    17.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Fri Oct 19 10:46:42 2012 +0200
    17.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Fri Oct 19 15:12:52 2012 +0200
    17.3 @@ -140,7 +140,7 @@
    17.4          also from y1 y2 have "h (y1 + y2) = h y1 + h y2"
    17.5            by simp
    17.6          also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
    17.7 -          by (simp add: left_distrib)
    17.8 +          by (simp add: distrib_right)
    17.9          also from h'_def x1_rep E HE y1 x0
   17.10          have "h y1 + a1 * xi = h' x1"
   17.11            by (rule h'_definite [symmetric])
   17.12 @@ -179,7 +179,7 @@
   17.13          also from y1 have "h (c \<cdot> y1) = c * h y1"
   17.14            by simp
   17.15          also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"
   17.16 -          by (simp only: right_distrib)
   17.17 +          by (simp only: distrib_left)
   17.18          also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1"
   17.19            by (rule h'_definite [symmetric])
   17.20          finally show ?thesis .
    18.1 --- a/src/HOL/Int.thy	Fri Oct 19 10:46:42 2012 +0200
    18.2 +++ b/src/HOL/Int.thy	Fri Oct 19 15:12:52 2012 +0200
    18.3 @@ -136,7 +136,7 @@
    18.4       "(i::int)<j ==> 0<k ==> int k * i < int k * j"
    18.5  apply (induct k)
    18.6  apply simp
    18.7 -apply (simp add: left_distrib)
    18.8 +apply (simp add: distrib_right)
    18.9  apply (case_tac "k=0")
   18.10  apply (simp_all add: add_strict_mono)
   18.11  done
   18.12 @@ -193,8 +193,8 @@
   18.13  done
   18.14  
   18.15  lemmas int_distrib =
   18.16 -  left_distrib [of z1 z2 w]
   18.17 -  right_distrib [of w z1 z2]
   18.18 +  distrib_right [of z1 z2 w]
   18.19 +  distrib_left [of w z1 z2]
   18.20    left_diff_distrib [of z1 z2 w]
   18.21    right_diff_distrib [of w z1 z2]
   18.22    for z1 z2 w :: int
   18.23 @@ -499,7 +499,7 @@
   18.24  lemma even_less_0_iff:
   18.25    "a + a < 0 \<longleftrightarrow> a < (0::'a::linordered_idom)"
   18.26  proof -
   18.27 -  have "a + a < 0 \<longleftrightarrow> (1+1)*a < 0" by (simp add: left_distrib del: one_add_one)
   18.28 +  have "a + a < 0 \<longleftrightarrow> (1+1)*a < 0" by (simp add: distrib_right del: one_add_one)
   18.29    also have "(1+1)*a < 0 \<longleftrightarrow> a < 0"
   18.30      by (simp add: mult_less_0_iff zero_less_two 
   18.31                    order_less_not_sym [OF zero_less_two])
   18.32 @@ -1097,8 +1097,8 @@
   18.33  
   18.34  text{*These distributive laws move literals inside sums and differences.*}
   18.35  
   18.36 -lemmas left_distrib_numeral [simp] = left_distrib [of _ _ "numeral v"] for v
   18.37 -lemmas right_distrib_numeral [simp] = right_distrib [of "numeral v"] for v
   18.38 +lemmas distrib_right_numeral [simp] = distrib_right [of _ _ "numeral v"] for v
   18.39 +lemmas distrib_left_numeral [simp] = distrib_left [of "numeral v"] for v
   18.40  lemmas left_diff_distrib_numeral [simp] = left_diff_distrib [of _ _ "numeral v"] for v
   18.41  lemmas right_diff_distrib_numeral [simp] = right_diff_distrib [of "numeral v"] for v
   18.42  
    19.1 --- a/src/HOL/Library/Extended_Nat.thy	Fri Oct 19 10:46:42 2012 +0200
    19.2 +++ b/src/HOL/Library/Extended_Nat.thy	Fri Oct 19 15:12:52 2012 +0200
    19.3 @@ -196,7 +196,7 @@
    19.4      by (simp split: enat.split)
    19.5    show "(a + b) * c = a * c + b * c"
    19.6      unfolding times_enat_def zero_enat_def
    19.7 -    by (simp split: enat.split add: left_distrib)
    19.8 +    by (simp split: enat.split add: distrib_right)
    19.9    show "0 * a = 0"
   19.10      unfolding times_enat_def zero_enat_def
   19.11      by (simp split: enat.split)
    20.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Fri Oct 19 10:46:42 2012 +0200
    20.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Oct 19 15:12:52 2012 +0200
    20.3 @@ -260,11 +260,11 @@
    20.4  proof
    20.5    fix a b c :: "'a fps"
    20.6    show "(a + b) * c = a * c + b * c"
    20.7 -    by (simp add: expand_fps_eq fps_mult_nth left_distrib setsum_addf)
    20.8 +    by (simp add: expand_fps_eq fps_mult_nth distrib_right setsum_addf)
    20.9  next
   20.10    fix a b c :: "'a fps"
   20.11    show "a * (b + c) = a * b + a * c"
   20.12 -    by (simp add: expand_fps_eq fps_mult_nth right_distrib setsum_addf)
   20.13 +    by (simp add: expand_fps_eq fps_mult_nth distrib_left setsum_addf)
   20.14  qed
   20.15  
   20.16  instance fps :: (semiring_0) semiring_0
   20.17 @@ -363,10 +363,10 @@
   20.18  instance fps :: (ring) ring ..
   20.19  
   20.20  instance fps :: (ring_1) ring_1
   20.21 -  by (intro_classes, auto simp add: diff_minus left_distrib)
   20.22 +  by (intro_classes, auto simp add: diff_minus distrib_right)
   20.23  
   20.24  instance fps :: (comm_ring_1) comm_ring_1
   20.25 -  by (intro_classes, auto simp add: diff_minus left_distrib)
   20.26 +  by (intro_classes, auto simp add: diff_minus distrib_right)
   20.27  
   20.28  instance fps :: (ring_no_zero_divisors) ring_no_zero_divisors
   20.29  proof
   20.30 @@ -3200,7 +3200,7 @@
   20.31    show ?thesis
   20.32      using fps_sin_cos_sum_of_squares[of c]
   20.33      apply (simp add: fps_tan_def fps_divide_deriv[OF th0] fps_sin_deriv fps_cos_deriv add: fps_const_neg[symmetric] field_simps power2_eq_square del: fps_const_neg)
   20.34 -    unfolding right_distrib[symmetric]
   20.35 +    unfolding distrib_left[symmetric]
   20.36      by simp
   20.37  qed
   20.38  
    21.1 --- a/src/HOL/Library/FrechetDeriv.thy	Fri Oct 19 10:46:42 2012 +0200
    21.2 +++ b/src/HOL/Library/FrechetDeriv.thy	Fri Oct 19 15:12:52 2012 +0200
    21.3 @@ -55,7 +55,7 @@
    21.4      apply (rule f.pos_bounded [THEN exE], rename_tac Kf)
    21.5      apply (rule g.pos_bounded [THEN exE], rename_tac Kg)
    21.6      apply (rule_tac x="Kf + Kg" in exI, safe)
    21.7 -    apply (subst right_distrib)
    21.8 +    apply (subst distrib_left)
    21.9      apply (rule order_trans [OF norm_triangle_ineq])
   21.10      apply (rule add_mono, erule spec, erule spec)
   21.11      done
   21.12 @@ -413,8 +413,8 @@
   21.13   apply (induct n)
   21.14    apply (simp add: FDERIV_ident)
   21.15   apply (drule FDERIV_mult [OF FDERIV_ident])
   21.16 - apply (simp only: of_nat_Suc left_distrib mult_1_left)
   21.17 - apply (simp only: power_Suc right_distrib add_ac mult_ac)
   21.18 + apply (simp only: of_nat_Suc distrib_right mult_1_left)
   21.19 + apply (simp only: power_Suc distrib_left add_ac mult_ac)
   21.20  done
   21.21  
   21.22  lemma FDERIV_power:
    22.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Fri Oct 19 10:46:42 2012 +0200
    22.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Fri Oct 19 15:12:52 2012 +0200
    22.3 @@ -238,7 +238,7 @@
    22.4      have th4: "cmod (complex_of_real (cmod b) / b) *
    22.5     cmod (1 + b * (v ^ n / complex_of_real (cmod b)))
    22.6     < cmod (complex_of_real (cmod b) / b) * 1"
    22.7 -      apply (simp only: norm_mult[symmetric] right_distrib)
    22.8 +      apply (simp only: norm_mult[symmetric] distrib_left)
    22.9        using b v by (simp add: th2)
   22.10  
   22.11      from mult_less_imp_less_left[OF th4 th3]
    23.1 --- a/src/HOL/Library/Inner_Product.thy	Fri Oct 19 10:46:42 2012 +0200
    23.2 +++ b/src/HOL/Library/Inner_Product.thy	Fri Oct 19 15:12:52 2012 +0200
    23.3 @@ -201,7 +201,7 @@
    23.4    show "inner x y = inner y x"
    23.5      unfolding inner_real_def by (rule mult_commute)
    23.6    show "inner (x + y) z = inner x z + inner y z"
    23.7 -    unfolding inner_real_def by (rule left_distrib)
    23.8 +    unfolding inner_real_def by (rule distrib_right)
    23.9    show "inner (scaleR r x) y = r * inner x y"
   23.10      unfolding inner_real_def real_scaleR_def by (rule mult_assoc)
   23.11    show "0 \<le> inner x x"
   23.12 @@ -225,9 +225,9 @@
   23.13    show "inner x y = inner y x"
   23.14      unfolding inner_complex_def by (simp add: mult_commute)
   23.15    show "inner (x + y) z = inner x z + inner y z"
   23.16 -    unfolding inner_complex_def by (simp add: left_distrib)
   23.17 +    unfolding inner_complex_def by (simp add: distrib_right)
   23.18    show "inner (scaleR r x) y = r * inner x y"
   23.19 -    unfolding inner_complex_def by (simp add: right_distrib)
   23.20 +    unfolding inner_complex_def by (simp add: distrib_left)
   23.21    show "0 \<le> inner x x"
   23.22      unfolding inner_complex_def by simp
   23.23    show "inner x x = 0 \<longleftrightarrow> x = 0"
    24.1 --- a/src/HOL/Library/Kleene_Algebra.thy	Fri Oct 19 10:46:42 2012 +0200
    24.2 +++ b/src/HOL/Library/Kleene_Algebra.thy	Fri Oct 19 15:12:52 2012 +0200
    24.3 @@ -141,13 +141,13 @@
    24.4    show "c * a \<le> c * b"
    24.5    proof (rule ord_intro)
    24.6      from `a \<le> b` have "c * (a + b) = c * b" by simp
    24.7 -    thus "c * a + c * b = c * b" by (simp add: right_distrib)
    24.8 +    thus "c * a + c * b = c * b" by (simp add: distrib_left)
    24.9    qed
   24.10  
   24.11    show "a * c \<le> b * c"
   24.12    proof (rule ord_intro)
   24.13      from `a \<le> b` have "(a + b) * c = b * c" by simp
   24.14 -    thus "a * c + b * c = b * c" by (simp add: left_distrib)
   24.15 +    thus "a * c + b * c = b * c" by (simp add: distrib_right)
   24.16    qed
   24.17  qed
   24.18  
   24.19 @@ -206,7 +206,7 @@
   24.20  by (metis less_add(2) star_unfold_left)
   24.21  
   24.22  lemma star_mult_idem [simp]: "star x * star x = star x"
   24.23 -by (metis add_commute add_est1 eq_iff mult_1_right right_distrib star3 star_unfold_left)
   24.24 +by (metis add_commute add_est1 eq_iff mult_1_right distrib_left star3 star_unfold_left)
   24.25  
   24.26  lemma less_star [simp]: "x \<le> star x"
   24.27  by (metis less_add(2) mult_1_right mult_left_mono one_less_star order_trans star_unfold_left zero_minimum)
   24.28 @@ -232,7 +232,7 @@
   24.29    thus "x + star b * x * a \<le> x + star b * b * x"
   24.30      using add_mono by auto
   24.31    show "\<dots> \<le> star b * x"
   24.32 -    by (metis add_supremum left_distrib less_add mult.left_neutral mult_assoc mult_right_mono star_unfold_right zero_minimum)
   24.33 +    by (metis add_supremum distrib_right less_add mult.left_neutral mult_assoc mult_right_mono star_unfold_right zero_minimum)
   24.34  qed
   24.35  
   24.36  lemma star_simulation [simp]:
   24.37 @@ -273,10 +273,10 @@
   24.38  by (metis add_commute ord_simp star_idemp star_mono star_mult_idem star_one star_unfold_left)
   24.39  
   24.40  lemma star_unfold2: "star x * y = y + x * star x * y"
   24.41 -by (subst star_unfold_right[symmetric]) (simp add: mult_assoc left_distrib)
   24.42 +by (subst star_unfold_right[symmetric]) (simp add: mult_assoc distrib_right)
   24.43  
   24.44  lemma star_absorb_one [simp]: "star (x + 1) = star x"
   24.45 -by (metis add_commute eq_iff left_distrib less_add mult_1_left mult_assoc star3 star_mono star_mult_idem star_unfold2 x_less_star)
   24.46 +by (metis add_commute eq_iff distrib_right less_add mult_1_left mult_assoc star3 star_mono star_mult_idem star_unfold2 x_less_star)
   24.47  
   24.48  lemma star_absorb_one' [simp]: "star (1 + x) = star x"
   24.49  by (subst add_commute) (fact star_absorb_one)
   24.50 @@ -292,13 +292,13 @@
   24.51  
   24.52  lemma ka18: "(x * star x) * star (y * star x) + (y * star x) * star (y * star x)
   24.53    \<le> star x * star (y * star x)"
   24.54 -by (metis ka16 ka17 left_distrib mult_assoc plus_leI)
   24.55 +by (metis ka16 ka17 distrib_right mult_assoc plus_leI)
   24.56  
   24.57  lemma star_decomp: "star (x + y) = star x * star (y * star x)"
   24.58  proof (rule antisym)
   24.59    have "1 + (x + y) * star x * star (y * star x) \<le>
   24.60      1 + x * star x * star (y * star x) + y * star x * star (y * star x)"
   24.61 -    by (metis add_commute add_left_commute eq_iff left_distrib mult_assoc)
   24.62 +    by (metis add_commute add_left_commute eq_iff distrib_right mult_assoc)
   24.63    also have "\<dots> \<le> star x * star (y * star x)"
   24.64      by (metis add_commute add_est1 add_left_commute ka18 plus_leI star_unfold_left x_less_star)
   24.65    finally show "star (x + y) \<le> star x * star (y * star x)"
   24.66 @@ -342,7 +342,7 @@
   24.67  by (metis add_commute ka27)
   24.68  
   24.69  lemma ka29: "(y * (1 + x) \<le> (1 + x) * star y) = (y * x \<le> (1 + x) * star y)"
   24.70 -by (metis add_supremum left_distrib less_add(1) less_star mult.left_neutral mult.right_neutral order_trans right_distrib)
   24.71 +by (metis add_supremum distrib_right less_add(1) less_star mult.left_neutral mult.right_neutral order_trans distrib_left)
   24.72  
   24.73  lemma ka30: "star x * star y \<le> star (x + y)"
   24.74  by (metis mult_left_mono star_decomp star_mono x_less_star zero_minimum)
    25.1 --- a/src/HOL/Library/ListVector.thy	Fri Oct 19 10:46:42 2012 +0200
    25.2 +++ b/src/HOL/Library/ListVector.thy	Fri Oct 19 15:12:52 2012 +0200
    25.3 @@ -128,7 +128,7 @@
    25.4  apply simp
    25.5  apply(case_tac zs)
    25.6  apply (simp)
    25.7 -apply(simp add: left_distrib)
    25.8 +apply(simp add: distrib_right)
    25.9  done
   25.10  
   25.11  lemma iprod_left_diff_distrib: "\<langle>xs - ys, zs\<rangle> = \<langle>xs,zs\<rangle> - \<langle>ys,zs\<rangle>"
   25.12 @@ -146,7 +146,7 @@
   25.13  apply simp
   25.14  apply(case_tac ys)
   25.15  apply (simp)
   25.16 -apply (simp add: right_distrib mult_assoc)
   25.17 +apply (simp add: distrib_left mult_assoc)
   25.18  done
   25.19  
   25.20  end
    26.1 --- a/src/HOL/Library/Polynomial.thy	Fri Oct 19 10:46:42 2012 +0200
    26.2 +++ b/src/HOL/Library/Polynomial.thy	Fri Oct 19 15:12:52 2012 +0200
    26.3 @@ -975,7 +975,7 @@
    26.4    assume "y \<noteq> 0"
    26.5    hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
    26.6      using pdivmod_rel [of x y]
    26.7 -    by (simp add: pdivmod_rel_def left_distrib)
    26.8 +    by (simp add: pdivmod_rel_def distrib_right)
    26.9    thus "(x + z * y) div y = z + x div y"
   26.10      by (rule div_poly_eq)
   26.11  next
    27.1 --- a/src/HOL/Library/Product_Vector.thy	Fri Oct 19 10:46:42 2012 +0200
    27.2 +++ b/src/HOL/Library/Product_Vector.thy	Fri Oct 19 15:12:52 2012 +0200
    27.3 @@ -421,7 +421,7 @@
    27.4    show "norm (scaleR r x) = \<bar>r\<bar> * norm x"
    27.5      unfolding norm_prod_def
    27.6      apply (simp add: power_mult_distrib)
    27.7 -    apply (simp add: right_distrib [symmetric])
    27.8 +    apply (simp add: distrib_left [symmetric])
    27.9      apply (simp add: real_sqrt_mult_distrib)
   27.10      done
   27.11    show "sgn x = scaleR (inverse (norm x)) x"
   27.12 @@ -475,7 +475,7 @@
   27.13      apply (rule allI)
   27.14      apply (simp add: norm_Pair)
   27.15      apply (rule order_trans [OF sqrt_add_le_add_sqrt], simp, simp)
   27.16 -    apply (simp add: right_distrib)
   27.17 +    apply (simp add: distrib_left)
   27.18      apply (rule add_mono [OF norm_f norm_g])
   27.19      done
   27.20    then show "\<exists>K. \<forall>x. norm (f x, g x) \<le> norm x * K" ..
   27.21 @@ -528,7 +528,7 @@
   27.22      by (simp add: inner_add_left)
   27.23    show "inner (scaleR r x) y = r * inner x y"
   27.24      unfolding inner_prod_def
   27.25 -    by (simp add: right_distrib)
   27.26 +    by (simp add: distrib_left)
   27.27    show "0 \<le> inner x x"
   27.28      unfolding inner_prod_def
   27.29      by (intro add_nonneg_nonneg inner_ge_zero)
    28.1 --- a/src/HOL/Library/Univ_Poly.thy	Fri Oct 19 10:46:42 2012 +0200
    28.2 +++ b/src/HOL/Library/Univ_Poly.thy	Fri Oct 19 15:12:52 2012 +0200
    28.3 @@ -125,7 +125,7 @@
    28.4  
    28.5  lemma (in semiring_0) poly_cmult_distr: "a %* ( p +++ q) = (a %* p +++ a %* q)"
    28.6  apply (induct p arbitrary: q, simp)
    28.7 -apply (case_tac q, simp_all add: right_distrib)
    28.8 +apply (case_tac q, simp_all add: distrib_left)
    28.9  done
   28.10  
   28.11  lemma (in ring_1) pmult_by_x[simp]: "[0, 1] *** t = ((0)#t)"
   28.12 @@ -141,17 +141,17 @@
   28.13    case Nil thus ?case by simp
   28.14  next
   28.15    case (Cons a as p2) thus ?case
   28.16 -    by (cases p2, simp_all  add: add_ac right_distrib)
   28.17 +    by (cases p2, simp_all  add: add_ac distrib_left)
   28.18  qed
   28.19  
   28.20  lemma (in comm_semiring_0) poly_cmult: "poly (c %* p) x = c * poly p x"
   28.21  apply (induct "p")
   28.22  apply (case_tac [2] "x=zero")
   28.23 -apply (auto simp add: right_distrib mult_ac)
   28.24 +apply (auto simp add: distrib_left mult_ac)
   28.25  done
   28.26  
   28.27  lemma (in comm_semiring_0) poly_cmult_map: "poly (map (op * c) p) x = c*poly p x"
   28.28 -  by (induct p, auto simp add: right_distrib mult_ac)
   28.29 +  by (induct p, auto simp add: distrib_left mult_ac)
   28.30  
   28.31  lemma (in comm_ring_1) poly_minus: "poly (-- p) x = - (poly p x)"
   28.32  apply (simp add: poly_minus_def)
   28.33 @@ -164,7 +164,7 @@
   28.34  next
   28.35    case (Cons a as p2)
   28.36    thus ?case by (cases as,
   28.37 -    simp_all add: poly_cmult poly_add left_distrib right_distrib mult_ac)
   28.38 +    simp_all add: poly_cmult poly_add distrib_right distrib_left mult_ac)
   28.39  qed
   28.40  
   28.41  class idom_char_0 = idom + ring_char_0
   28.42 @@ -394,7 +394,7 @@
   28.43  by (auto simp add: algebra_simps poly_add poly_minus_def fun_eq poly_cmult minus_mult_left[symmetric])
   28.44  
   28.45  lemma (in comm_ring_1) poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))"
   28.46 -by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult right_distrib minus_mult_left[symmetric] minus_mult_right[symmetric])
   28.47 +by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult distrib_left minus_mult_left[symmetric] minus_mult_right[symmetric])
   28.48  
   28.49  subclass (in idom_char_0) comm_ring_1 ..
   28.50  lemma (in idom_char_0) poly_mult_left_cancel: "(poly (p *** q) = poly (p *** r)) = (poly p = poly [] | poly q = poly r)"
   28.51 @@ -458,9 +458,9 @@
   28.52  text{*Basics of divisibility.*}
   28.53  
   28.54  lemma (in idom) poly_primes: "([a, 1] divides (p *** q)) = ([a, 1] divides p | [a, 1] divides q)"
   28.55 -apply (auto simp add: divides_def fun_eq poly_mult poly_add poly_cmult left_distrib [symmetric])
   28.56 +apply (auto simp add: divides_def fun_eq poly_mult poly_add poly_cmult distrib_right [symmetric])
   28.57  apply (drule_tac x = "uminus a" in spec)
   28.58 -apply (simp add: poly_linear_divides poly_add poly_cmult left_distrib [symmetric])
   28.59 +apply (simp add: poly_linear_divides poly_add poly_cmult distrib_right [symmetric])
   28.60  apply (cases "p = []")
   28.61  apply (rule exI[where x="[]"])
   28.62  apply simp
   28.63 @@ -471,10 +471,10 @@
   28.64  apply (cases "\<exists>q\<Colon>'a list. p = a %* q +++ ((0\<Colon>'a) # q)")
   28.65  apply (clarsimp simp add: poly_add poly_cmult)
   28.66  apply (rule_tac x="qa" in exI)
   28.67 -apply (simp add: left_distrib [symmetric])
   28.68 +apply (simp add: distrib_right [symmetric])
   28.69  apply clarsimp
   28.70  
   28.71 -apply (auto simp add: right_minus poly_linear_divides poly_add poly_cmult left_distrib [symmetric])
   28.72 +apply (auto simp add: right_minus poly_linear_divides poly_add poly_cmult distrib_right [symmetric])
   28.73  apply (rule_tac x = "pmult qa q" in exI)
   28.74  apply (rule_tac [2] x = "pmult p qa" in exI)
   28.75  apply (auto simp add: poly_add poly_mult poly_cmult mult_ac)
   28.76 @@ -509,7 +509,7 @@
   28.77     "[| p divides q; p divides r |] ==> p divides (q +++ r)"
   28.78  apply (simp add: divides_def, auto)
   28.79  apply (rule_tac x = "padd qa qaa" in exI)
   28.80 -apply (auto simp add: poly_add fun_eq poly_mult right_distrib)
   28.81 +apply (auto simp add: poly_add fun_eq poly_mult distrib_left)
   28.82  done
   28.83  
   28.84  lemma (in comm_ring_1) poly_divides_diff:
   28.85 @@ -605,7 +605,7 @@
   28.86  apply (unfold divides_def)
   28.87  apply (rule_tac x = q in exI)
   28.88  apply (induct_tac "n", simp)
   28.89 -apply (simp (no_asm_simp) add: poly_add poly_cmult poly_mult right_distrib mult_ac)
   28.90 +apply (simp (no_asm_simp) add: poly_add poly_cmult poly_mult distrib_left mult_ac)
   28.91  apply safe
   28.92  apply (subgoal_tac "?poly (?mulexp n [uminus a, one] q) \<noteq> ?poly (pmult (?pexp [uminus a, one] (Suc n)) qa)")
   28.93  apply simp
   28.94 @@ -948,7 +948,7 @@
   28.95    case (Suc n a p)
   28.96    have eq: "poly ([a,1] %^(Suc n) *** p) = poly ([a,1] %^ n *** ([a,1] *** p))"
   28.97      apply (rule ext, simp add: poly_mult poly_add poly_cmult)
   28.98 -    by (simp add: mult_ac add_ac right_distrib)
   28.99 +    by (simp add: mult_ac add_ac distrib_left)
  28.100    note deq = degree_unique[OF eq]
  28.101    {assume p: "poly p = poly []"
  28.102      with eq have eq': "poly ([a,1] %^(Suc n) *** p) = poly []"
    29.1 --- a/src/HOL/List.thy	Fri Oct 19 10:46:42 2012 +0200
    29.2 +++ b/src/HOL/List.thy	Fri Oct 19 15:12:52 2012 +0200
    29.3 @@ -3166,11 +3166,11 @@
    29.4  
    29.5  lemma (in monoid_add) listsum_triv:
    29.6    "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
    29.7 -  by (induct xs) (simp_all add: left_distrib)
    29.8 +  by (induct xs) (simp_all add: distrib_right)
    29.9  
   29.10  lemma (in monoid_add) listsum_0 [simp]:
   29.11    "(\<Sum>x\<leftarrow>xs. 0) = 0"
   29.12 -  by (induct xs) (simp_all add: left_distrib)
   29.13 +  by (induct xs) (simp_all add: distrib_right)
   29.14  
   29.15  text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
   29.16  lemma (in ab_group_add) uminus_listsum_map:
    30.1 --- a/src/HOL/Log.thy	Fri Oct 19 10:46:42 2012 +0200
    30.2 +++ b/src/HOL/Log.thy	Fri Oct 19 15:12:52 2012 +0200
    30.3 @@ -34,7 +34,7 @@
    30.4  
    30.5  lemma powr_mult: 
    30.6        "[| 0 < x; 0 < y |] ==> (x * y) powr a = (x powr a) * (y powr a)"
    30.7 -by (simp add: powr_def exp_add [symmetric] ln_mult right_distrib)
    30.8 +by (simp add: powr_def exp_add [symmetric] ln_mult distrib_left)
    30.9  
   30.10  lemma powr_gt_zero [simp]: "0 < x powr a"
   30.11  by (simp add: powr_def)
   30.12 @@ -58,7 +58,7 @@
   30.13  done
   30.14  
   30.15  lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
   30.16 -by (simp add: powr_def exp_add [symmetric] left_distrib)
   30.17 +by (simp add: powr_def exp_add [symmetric] distrib_right)
   30.18  
   30.19  lemma powr_mult_base:
   30.20    "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
   30.21 @@ -112,7 +112,7 @@
   30.22  lemma log_mult: 
   30.23       "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y |]  
   30.24        ==> log a (x * y) = log a x + log a y"
   30.25 -by (simp add: log_def ln_mult divide_inverse left_distrib)
   30.26 +by (simp add: log_def ln_mult divide_inverse distrib_right)
   30.27  
   30.28  lemma log_eq_div_ln_mult_log: 
   30.29       "[| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]  
    31.1 --- a/src/HOL/MacLaurin.thy	Fri Oct 19 10:46:42 2012 +0200
    31.2 +++ b/src/HOL/MacLaurin.thy	Fri Oct 19 15:12:52 2012 +0200
    31.3 @@ -415,7 +415,7 @@
    31.4  lemma sin_expansion_lemma:
    31.5       "sin (x + real (Suc m) * pi / 2) =
    31.6        cos (x + real (m) * pi / 2)"
    31.7 -by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
    31.8 +by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib distrib_right, auto)
    31.9  
   31.10  lemma Maclaurin_sin_expansion2:
   31.11       "\<exists>t. abs t \<le> abs x &
   31.12 @@ -489,7 +489,7 @@
   31.13  
   31.14  lemma cos_expansion_lemma:
   31.15    "cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)"
   31.16 -by (simp only: cos_add sin_add real_of_nat_Suc left_distrib add_divide_distrib, auto)
   31.17 +by (simp only: cos_add sin_add real_of_nat_Suc distrib_right add_divide_distrib, auto)
   31.18  
   31.19  lemma Maclaurin_cos_expansion:
   31.20       "\<exists>t. abs t \<le> abs x &
    32.1 --- a/src/HOL/Metis_Examples/Binary_Tree.thy	Fri Oct 19 10:46:42 2012 +0200
    32.2 +++ b/src/HOL/Metis_Examples/Binary_Tree.thy	Fri Oct 19 15:12:52 2012 +0200
    32.3 @@ -223,7 +223,7 @@
    32.4  apply (induct t1)
    32.5   apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1)
    32.6                Suc_eq_plus1)
    32.7 -by (simp add: left_distrib)
    32.8 +by (simp add: distrib_right)
    32.9  
   32.10  lemma (*bt_map_append:*)
   32.11       "bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)"
    33.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Fri Oct 19 10:46:42 2012 +0200
    33.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Fri Oct 19 15:12:52 2012 +0200
    33.3 @@ -1068,7 +1068,7 @@
    33.4            x: "setsum (\<lambda>i. (x$i) *s column i A) ?U = y2" by blast
    33.5          let ?x = "(\<chi> j. if j = i then c + (x$i) else (x$j))::real^'m"
    33.6          show "?P (c*s y1 + y2)"
    33.7 -        proof (rule exI[where x= "?x"], vector, auto simp add: i x[symmetric] if_distrib right_distrib cond_application_beta cong del: if_weak_cong)
    33.8 +        proof (rule exI[where x= "?x"], vector, auto simp add: i x[symmetric] if_distrib distrib_left cond_application_beta cong del: if_weak_cong)
    33.9            fix j
   33.10            have th: "\<forall>xa \<in> ?U. (if xa = i then (c + (x$i)) * ((column xa A)$j)
   33.11                else (x$xa) * ((column xa A$j))) = (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))"
    34.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Oct 19 10:46:42 2012 +0200
    34.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Oct 19 15:12:52 2012 +0200
    34.3 @@ -1450,7 +1450,7 @@
    34.4      have u2:"u2 \<le> 1" unfolding obt2(3)[symmetric] and not_le using obt2(2) by auto
    34.5      have "u1 * u + u2 * v \<le> (max u1 u2) * u + (max u1 u2) * v" apply(rule add_mono)
    34.6        apply(rule_tac [!] mult_right_mono) using as(1,2) obt1(1,2) obt2(1,2) by auto
    34.7 -    also have "\<dots> \<le> 1" unfolding right_distrib[symmetric] and as(3) using u1 u2 by auto
    34.8 +    also have "\<dots> \<le> 1" unfolding distrib_left[symmetric] and as(3) using u1 u2 by auto
    34.9      finally
   34.10      show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull" unfolding mem_Collect_eq apply(rule_tac x="u * u1 + v * u2" in exI)
   34.11        apply(rule conjI) defer apply(rule_tac x="1 - u * u1 - v * u2" in exI) unfolding Bex_def
    35.1 --- a/src/HOL/Multivariate_Analysis/L2_Norm.thy	Fri Oct 19 10:46:42 2012 +0200
    35.2 +++ b/src/HOL/Multivariate_Analysis/L2_Norm.thy	Fri Oct 19 15:12:52 2012 +0200
    35.3 @@ -165,7 +165,7 @@
    35.4    apply (simp add: mult_nonneg_nonneg setsum_nonneg)
    35.5    apply (simp add: power2_sum)
    35.6    apply (simp add: power_mult_distrib)
    35.7 -  apply (simp add: right_distrib left_distrib)
    35.8 +  apply (simp add: distrib_left distrib_right)
    35.9    apply (rule ord_le_eq_trans)
   35.10    apply (rule setL2_mult_ineq_lemma)
   35.11    apply simp
    36.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Oct 19 10:46:42 2012 +0200
    36.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Oct 19 15:12:52 2012 +0200
    36.3 @@ -1456,7 +1456,7 @@
    36.4            by (auto simp add: norm_minus_commute)
    36.5          also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
    36.6            unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
    36.7 -          unfolding left_distrib using `x\<noteq>y`[unfolded dist_nz, unfolded dist_norm] by auto
    36.8 +          unfolding distrib_right using `x\<noteq>y`[unfolded dist_nz, unfolded dist_norm] by auto
    36.9          also have "\<dots> \<le> e - d/2" using `d \<le> dist x y` and `d>0` and `?rhs` by(auto simp add: dist_norm)
   36.10          finally have "y - (d / (2 * dist y x)) *\<^sub>R (y - x) \<in> ball x e" using `d>0` by auto
   36.11  
   36.12 @@ -1583,7 +1583,7 @@
   36.13          by (auto simp add: algebra_simps)
   36.14        also have "\<dots> = \<bar>1 + d / (2 * norm (y - x))\<bar> * norm (y - x)"
   36.15          using ** by auto
   36.16 -      also have "\<dots> = (dist y x) + d/2"using ** by (auto simp add: left_distrib dist_norm)
   36.17 +      also have "\<dots> = (dist y x) + d/2"using ** by (auto simp add: distrib_right dist_norm)
   36.18        finally have "e \<ge> dist x y +d/2" using *[unfolded mem_cball] by (auto simp add: dist_commute)
   36.19        thus "y \<in> ball x e" unfolding mem_ball using `d>0` by auto
   36.20      qed  }
    37.1 --- a/src/HOL/NSA/CLim.thy	Fri Oct 19 10:46:42 2012 +0200
    37.2 +++ b/src/HOL/NSA/CLim.thy	Fri Oct 19 15:12:52 2012 +0200
    37.3 @@ -140,7 +140,7 @@
    37.4       "DERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))"
    37.5  apply (induct n)
    37.6  apply (drule_tac [2] DERIV_ident [THEN DERIV_mult])
    37.7 -apply (auto simp add: left_distrib real_of_nat_Suc)
    37.8 +apply (auto simp add: distrib_right real_of_nat_Suc)
    37.9  apply (case_tac "n")
   37.10  apply (auto simp add: mult_ac add_commute)
   37.11  done
    38.1 --- a/src/HOL/NSA/HDeriv.thy	Fri Oct 19 10:46:42 2012 +0200
    38.2 +++ b/src/HOL/NSA/HDeriv.thy	Fri Oct 19 15:12:52 2012 +0200
    38.3 @@ -209,7 +209,7 @@
    38.4  apply (drule_tac
    38.5       approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]])
    38.6  apply (auto intro!: approx_add_mono1
    38.7 -            simp add: left_distrib right_distrib mult_commute add_assoc)
    38.8 +            simp add: distrib_right distrib_left mult_commute add_assoc)
    38.9  apply (rule_tac b1 = "star_of Db * star_of (f x)"
   38.10           in add_commute [THEN subst])
   38.11  apply (auto intro!: Infinitesimal_add_approx_self2 [THEN approx_sym]
   38.12 @@ -357,7 +357,7 @@
   38.13              del: inverse_mult_distrib inverse_minus_eq
   38.14                   minus_mult_left [symmetric] minus_mult_right [symmetric])
   38.15  apply (subst mult_commute, simp add: nonzero_mult_divide_cancel_right)
   38.16 -apply (simp (no_asm_simp) add: mult_assoc [symmetric] left_distrib
   38.17 +apply (simp (no_asm_simp) add: mult_assoc [symmetric] distrib_right
   38.18              del: minus_mult_left [symmetric] minus_mult_right [symmetric])
   38.19  apply (rule_tac y = "inverse (- (star_of x * star_of x))" in approx_trans)
   38.20  apply (rule inverse_add_Infinitesimal_approx2)
   38.21 @@ -451,7 +451,7 @@
   38.22  apply (erule_tac [2] V = "(( *f* f) (hypreal_of_real (x) + h) - hypreal_of_real (f x)) / h = hypreal_of_real (D) + y" in thin_rl)
   38.23  apply assumption
   38.24  apply (simp add: times_divide_eq_right [symmetric])
   38.25 -apply (auto simp add: left_distrib)
   38.26 +apply (auto simp add: distrib_right)
   38.27  done
   38.28  
   38.29  lemma increment_thm2:
   38.30 @@ -464,7 +464,7 @@
   38.31  lemma increment_approx_zero: "[| NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 |]
   38.32        ==> increment f x h \<approx> 0"
   38.33  apply (drule increment_thm2,
   38.34 -       auto intro!: Infinitesimal_HFinite_mult2 HFinite_add simp add: left_distrib [symmetric] mem_infmal_iff [symmetric])
   38.35 +       auto intro!: Infinitesimal_HFinite_mult2 HFinite_add simp add: distrib_right [symmetric] mem_infmal_iff [symmetric])
   38.36  apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
   38.37  done
   38.38  
    39.1 --- a/src/HOL/NSA/HyperDef.thy	Fri Oct 19 10:46:42 2012 +0200
    39.2 +++ b/src/HOL/NSA/HyperDef.thy	Fri Oct 19 15:12:52 2012 +0200
    39.3 @@ -404,7 +404,7 @@
    39.4  
    39.5  lemma two_hrealpow_gt [simp]: "hypreal_of_nat n < 2 ^ n"
    39.6  apply (induct n)
    39.7 -apply (auto simp add: left_distrib)
    39.8 +apply (auto simp add: distrib_right)
    39.9  apply (cut_tac n = n in two_hrealpow_ge_one, arith)
   39.10  done
   39.11  
   39.12 @@ -417,7 +417,7 @@
   39.13  lemma hrealpow_sum_square_expand:
   39.14       "(x + (y::hypreal)) ^ Suc (Suc 0) =
   39.15        x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0)))*x*y"
   39.16 -by (simp add: right_distrib left_distrib)
   39.17 +by (simp add: distrib_left distrib_right)
   39.18  
   39.19  lemma power_hypreal_of_real_numeral:
   39.20       "(numeral v :: hypreal) ^ n = hypreal_of_real ((numeral v) ^ n)"
    40.1 --- a/src/HOL/NSA/NSComplex.thy	Fri Oct 19 10:46:42 2012 +0200
    40.2 +++ b/src/HOL/NSA/NSComplex.thy	Fri Oct 19 15:12:52 2012 +0200
    40.3 @@ -547,7 +547,7 @@
    40.4     "!!a. hcis (hypreal_of_nat (Suc n) * a) =
    40.5       hcis a * hcis (hypreal_of_nat n * a)"
    40.6  apply transfer
    40.7 -apply (simp add: left_distrib cis_mult)
    40.8 +apply (simp add: distrib_right cis_mult)
    40.9  done
   40.10  
   40.11  lemma NSDeMoivre: "!!a. (hcis a) ^ n = hcis (hypreal_of_nat n * a)"
   40.12 @@ -559,7 +559,7 @@
   40.13  lemma hcis_hypreal_of_hypnat_Suc_mult:
   40.14       "!! a n. hcis (hypreal_of_hypnat (n + 1) * a) =
   40.15        hcis a * hcis (hypreal_of_hypnat n * a)"
   40.16 -by transfer (simp add: left_distrib cis_mult)
   40.17 +by transfer (simp add: distrib_right cis_mult)
   40.18  
   40.19  lemma NSDeMoivre_ext:
   40.20    "!!a n. (hcis a) pow n = hcis (hypreal_of_hypnat n * a)"
    41.1 --- a/src/HOL/NSA/StarDef.thy	Fri Oct 19 10:46:42 2012 +0200
    41.2 +++ b/src/HOL/NSA/StarDef.thy	Fri Oct 19 15:12:52 2012 +0200
    41.3 @@ -828,8 +828,8 @@
    41.4  
    41.5  instance star :: (semiring) semiring
    41.6  apply (intro_classes)
    41.7 -apply (transfer, rule left_distrib)
    41.8 -apply (transfer, rule right_distrib)
    41.9 +apply (transfer, rule distrib_right)
   41.10 +apply (transfer, rule distrib_left)
   41.11  done
   41.12  
   41.13  instance star :: (semiring_0) semiring_0 
   41.14 @@ -838,7 +838,7 @@
   41.15  instance star :: (semiring_0_cancel) semiring_0_cancel ..
   41.16  
   41.17  instance star :: (comm_semiring) comm_semiring 
   41.18 -by (intro_classes, transfer, rule left_distrib)
   41.19 +by (intro_classes, transfer, rule distrib_right)
   41.20  
   41.21  instance star :: (comm_semiring_0) comm_semiring_0 ..
   41.22  instance star :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..
    42.1 --- a/src/HOL/Nat.thy	Fri Oct 19 10:46:42 2012 +0200
    42.2 +++ b/src/HOL/Nat.thy	Fri Oct 19 15:12:52 2012 +0200
    42.3 @@ -312,7 +312,7 @@
    42.4    by (rule mult_commute)
    42.5  
    42.6  lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
    42.7 -  by (rule right_distrib)
    42.8 +  by (rule distrib_left)
    42.9  
   42.10  lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
   42.11    by (induct m) auto
   42.12 @@ -1342,7 +1342,7 @@
   42.13    by (induct m) (simp_all add: add_ac)
   42.14  
   42.15  lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
   42.16 -  by (induct m) (simp_all add: add_ac left_distrib)
   42.17 +  by (induct m) (simp_all add: add_ac distrib_right)
   42.18  
   42.19  primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
   42.20    "of_nat_aux inc 0 i = i"
    43.1 --- a/src/HOL/NthRoot.thy	Fri Oct 19 10:46:42 2012 +0200
    43.2 +++ b/src/HOL/NthRoot.thy	Fri Oct 19 15:12:52 2012 +0200
    43.3 @@ -598,7 +598,7 @@
    43.4    "sqrt ((a + c)\<twosuperior> + (b + d)\<twosuperior>) \<le> sqrt (a\<twosuperior> + b\<twosuperior>) + sqrt (c\<twosuperior> + d\<twosuperior>)"
    43.5  apply (rule power2_le_imp_le, simp)
    43.6  apply (simp add: power2_sum)
    43.7 -apply (simp only: mult_assoc right_distrib [symmetric])
    43.8 +apply (simp only: mult_assoc distrib_left [symmetric])
    43.9  apply (rule mult_left_mono)
   43.10  apply (rule power2_le_imp_le)
   43.11  apply (simp add: power2_sum power_mult_distrib)
    44.1 --- a/src/HOL/Num.thy	Fri Oct 19 10:46:42 2012 +0200
    44.2 +++ b/src/HOL/Num.thy	Fri Oct 19 15:12:52 2012 +0200
    44.3 @@ -138,7 +138,7 @@
    44.4    "Bit1 m * Bit0 n = Bit0 (Bit1 m * n)"
    44.5    "Bit1 m * Bit1 n = Bit1 (m + n + Bit0 (m * n))"
    44.6    by (simp_all add: num_eq_iff nat_of_num_add
    44.7 -    nat_of_num_mult left_distrib right_distrib)
    44.8 +    nat_of_num_mult distrib_right distrib_left)
    44.9  
   44.10  lemma eq_num_simps:
   44.11    "One = One \<longleftrightarrow> True"
   44.12 @@ -510,7 +510,7 @@
   44.13  lemma numeral_mult: "numeral (m * n) = numeral m * numeral n"
   44.14    apply (induct n rule: num_induct)
   44.15    apply (simp add: numeral_One)
   44.16 -  apply (simp add: mult_inc numeral_inc numeral_add right_distrib)
   44.17 +  apply (simp add: mult_inc numeral_inc numeral_add distrib_left)
   44.18    done
   44.19  
   44.20  lemma numeral_times_numeral: "numeral m * numeral n = numeral (m * n)"
   44.21 @@ -532,10 +532,10 @@
   44.22      simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1)
   44.23  
   44.24  lemma mult_2: "2 * z = z + z"
   44.25 -  unfolding one_add_one [symmetric] left_distrib by simp
   44.26 +  unfolding one_add_one [symmetric] distrib_right by simp
   44.27  
   44.28  lemma mult_2_right: "z * 2 = z + z"
   44.29 -  unfolding one_add_one [symmetric] right_distrib by simp
   44.30 +  unfolding one_add_one [symmetric] distrib_left by simp
   44.31  
   44.32  end
   44.33  
    45.1 --- a/src/HOL/Number_Theory/Binomial.thy	Fri Oct 19 10:46:42 2012 +0200
    45.2 +++ b/src/HOL/Number_Theory/Binomial.thy	Fri Oct 19 15:12:52 2012 +0200
    45.3 @@ -205,7 +205,7 @@
    45.4    also note two
    45.5    also with less have "(n - k) * fact n + (k + 1) * fact n= fact (n + 1)" 
    45.6      apply (subst fact_plus_one_nat)
    45.7 -    apply (subst left_distrib [symmetric])
    45.8 +    apply (subst distrib_right [symmetric])
    45.9      apply simp
   45.10      done
   45.11    finally show "fact (k + 1) * fact (n - k) * (n + 1 choose (k + 1)) = 
    46.1 --- a/src/HOL/Old_Number_Theory/EvenOdd.thy	Fri Oct 19 10:46:42 2012 +0200
    46.2 +++ b/src/HOL/Old_Number_Theory/EvenOdd.thy	Fri Oct 19 15:12:52 2012 +0200
    46.3 @@ -85,7 +85,7 @@
    46.4  
    46.5  lemma even_plus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x + y \<in> zEven"
    46.6    apply (auto simp add: zEven_def)
    46.7 -  apply (auto simp only: right_distrib [symmetric])
    46.8 +  apply (auto simp only: distrib_left [symmetric])
    46.9    done
   46.10  
   46.11  lemma even_times_either: "x \<in> zEven ==> x * y \<in> zEven"
   46.12 @@ -113,9 +113,9 @@
   46.13    done
   46.14  
   46.15  lemma odd_times_odd: "[| x \<in> zOdd;  y \<in> zOdd |] ==> x * y \<in> zOdd"
   46.16 -  apply (auto simp add: zOdd_def left_distrib right_distrib)
   46.17 +  apply (auto simp add: zOdd_def distrib_right distrib_left)
   46.18    apply (rule_tac x = "2 * ka * k + ka + k" in exI)
   46.19 -  apply (auto simp add: left_distrib)
   46.20 +  apply (auto simp add: distrib_right)
   46.21    done
   46.22  
   46.23  lemma odd_iff_not_even: "(x \<in> zOdd) = (~ (x \<in> zEven))"
    47.1 --- a/src/HOL/Old_Number_Theory/Finite2.thy	Fri Oct 19 10:46:42 2012 +0200
    47.2 +++ b/src/HOL/Old_Number_Theory/Finite2.thy	Fri Oct 19 15:12:52 2012 +0200
    47.3 @@ -38,18 +38,18 @@
    47.4  
    47.5  lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)"
    47.6    apply (induct set: finite)
    47.7 -  apply (auto simp add: left_distrib right_distrib)
    47.8 +  apply (auto simp add: distrib_right distrib_left)
    47.9    done
   47.10  
   47.11  lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) =
   47.12      int(c) * int(card X)"
   47.13    apply (induct set: finite)
   47.14 -  apply (auto simp add: right_distrib)
   47.15 +  apply (auto simp add: distrib_left)
   47.16    done
   47.17  
   47.18  lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A =
   47.19      c * setsum f A"
   47.20 -  by (induct set: finite) (auto simp add: right_distrib)
   47.21 +  by (induct set: finite) (auto simp add: distrib_left)
   47.22  
   47.23  
   47.24  subsection {* Cardinality of explicit finite sets *}
    48.1 --- a/src/HOL/Old_Number_Theory/Gauss.thy	Fri Oct 19 10:46:42 2012 +0200
    48.2 +++ b/src/HOL/Old_Number_Theory/Gauss.thy	Fri Oct 19 15:12:52 2012 +0200
    48.3 @@ -341,7 +341,7 @@
    48.4      apply (elim zcong_trans)
    48.5      by (simp only: zcong_refl)
    48.6    also have "y * a + ya * a = a * (y + ya)"
    48.7 -    by (simp add: right_distrib mult_commute)
    48.8 +    by (simp add: distrib_left mult_commute)
    48.9    finally have "[a * (y + ya) = 0] (mod p)" .
   48.10    with p_prime a_nonzero zcong_zprime_prod_zero [of p a "y + ya"]
   48.11      p_a_relprime
    49.1 --- a/src/HOL/Old_Number_Theory/IntPrimes.thy	Fri Oct 19 10:46:42 2012 +0200
    49.2 +++ b/src/HOL/Old_Number_Theory/IntPrimes.thy	Fri Oct 19 15:12:52 2012 +0200
    49.3 @@ -341,7 +341,7 @@
    49.4  lemma xzgcda_linear_aux1:
    49.5    "(a - r * b) * m + (c - r * d) * (n::int) =
    49.6     (a * m + c * n) - r * (b * m + d * n)"
    49.7 -  by (simp add: left_diff_distrib right_distrib mult_assoc)
    49.8 +  by (simp add: left_diff_distrib distrib_left mult_assoc)
    49.9  
   49.10  lemma xzgcda_linear_aux2:
   49.11    "r' = s' * m + t' * n ==> r = s * m + t * n
    50.1 --- a/src/HOL/Old_Number_Theory/Pocklington.thy	Fri Oct 19 10:46:42 2012 +0200
    50.2 +++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Fri Oct 19 15:12:52 2012 +0200
    50.3 @@ -161,7 +161,7 @@
    50.4      and q12': "y + n*q1' = y'+n*q2'" unfolding nat_mod by blast+
    50.5    from th[OF q12 q12' yx yx']
    50.6    have "(x - y) + n*(q1 + q2') = (x' - y') + n*(q2 + q1')"
    50.7 -    by (simp add: right_distrib)
    50.8 +    by (simp add: distrib_left)
    50.9    thus ?thesis unfolding nat_mod by blast
   50.10  qed
   50.11  
    51.1 --- a/src/HOL/Presburger.thy	Fri Oct 19 10:46:42 2012 +0200
    51.2 +++ b/src/HOL/Presburger.thy	Fri Oct 19 15:12:52 2012 +0200
    51.3 @@ -54,7 +54,7 @@
    51.4    "(d::'a::{comm_ring,Rings.dvd}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)"
    51.5    "\<forall>x k. F = F"
    51.6  apply (auto elim!: dvdE simp add: algebra_simps)
    51.7 -unfolding mult_assoc [symmetric] left_distrib [symmetric] left_diff_distrib [symmetric]
    51.8 +unfolding mult_assoc [symmetric] distrib_right [symmetric] left_diff_distrib [symmetric]
    51.9  unfolding dvd_def mult_commute [of d] 
   51.10  by auto
   51.11  
    52.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Fri Oct 19 10:46:42 2012 +0200
    52.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Oct 19 15:12:52 2012 +0200
    52.3 @@ -107,7 +107,7 @@
    52.4    "n < m \<longleftrightarrow> int_of n < int_of m"
    52.5  
    52.6  instance proof
    52.7 -qed (auto simp add: code_int left_distrib zmult_zless_mono2)
    52.8 +qed (auto simp add: code_int distrib_right zmult_zless_mono2)
    52.9  
   52.10  end
   52.11  
    53.1 --- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Fri Oct 19 10:46:42 2012 +0200
    53.2 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Fri Oct 19 15:12:52 2012 +0200
    53.3 @@ -208,7 +208,7 @@
    53.4    apply(induct "k")
    53.5    apply(simp)
    53.6    apply(case_tac "k = 0")
    53.7 -  apply(simp_all add: left_distrib add_strict_mono)
    53.8 +  apply(simp_all add: distrib_right add_strict_mono)
    53.9    done
   53.10  
   53.11  lemma zero_le_imp_eq_int_raw:
   53.12 @@ -248,8 +248,8 @@
   53.13  qed
   53.14  
   53.15  lemmas int_distrib =
   53.16 -  left_distrib [of z1 z2 w]
   53.17 -  right_distrib [of w z1 z2]
   53.18 +  distrib_right [of z1 z2 w]
   53.19 +  distrib_left [of w z1 z2]
   53.20    left_diff_distrib [of z1 z2 w]
   53.21    right_diff_distrib [of w z1 z2]
   53.22    minus_add_distrib[of z1 z2]
    54.1 --- a/src/HOL/Quotient_Examples/Quotient_Rat.thy	Fri Oct 19 10:46:42 2012 +0200
    54.2 +++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy	Fri Oct 19 15:12:52 2012 +0200
    54.3 @@ -128,7 +128,7 @@
    54.4    show "1 * a = a"
    54.5      by partiality_descending auto
    54.6    show "a + b + c = a + (b + c)"
    54.7 -    by partiality_descending (auto simp add: mult_commute right_distrib)
    54.8 +    by partiality_descending (auto simp add: mult_commute distrib_left)
    54.9    show "a + b = b + a"
   54.10      by partiality_descending auto
   54.11    show "0 + a = a"
   54.12 @@ -138,7 +138,7 @@
   54.13    show "a - b = a + - b"
   54.14      by (simp add: minus_rat_def)
   54.15    show "(a + b) * c = a * c + b * c"
   54.16 -    by partiality_descending (auto simp add: mult_commute right_distrib)
   54.17 +    by partiality_descending (auto simp add: mult_commute distrib_left)
   54.18    show "(0 :: rat) \<noteq> (1 :: rat)"
   54.19      by partiality_descending auto
   54.20  qed
    55.1 --- a/src/HOL/RComplete.thy	Fri Oct 19 10:46:42 2012 +0200
    55.2 +++ b/src/HOL/RComplete.thy	Fri Oct 19 15:12:52 2012 +0200
    55.3 @@ -447,7 +447,7 @@
    55.4      done
    55.5    thus "x / real y < real (natfloor x div y) + 1"
    55.6      using assms
    55.7 -    by (simp add: divide_less_eq natfloor_less_iff left_distrib)
    55.8 +    by (simp add: divide_less_eq natfloor_less_iff distrib_right)
    55.9  qed
   55.10  
   55.11  lemma le_mult_natfloor:
    56.1 --- a/src/HOL/Rat.thy	Fri Oct 19 10:46:42 2012 +0200
    56.2 +++ b/src/HOL/Rat.thy	Fri Oct 19 15:12:52 2012 +0200
    56.3 @@ -123,7 +123,7 @@
    56.4  
    56.5  lift_definition plus_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat"
    56.6    is "\<lambda>x y. (fst x * snd y + fst y * snd x, snd x * snd y)"
    56.7 -  by (clarsimp, simp add: left_distrib, simp add: mult_ac)
    56.8 +  by (clarsimp, simp add: distrib_right, simp add: mult_ac)
    56.9  
   56.10  lemma add_rat [simp]:
   56.11    assumes "b \<noteq> 0" and "d \<noteq> 0"
   56.12 @@ -616,8 +616,8 @@
   56.13      (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *)
   56.14    #> Lin_Arith.add_simps [@{thm neg_less_iff_less},
   56.15        @{thm True_implies_equals},
   56.16 -      read_instantiate @{context} [(("a", 0), "(numeral ?v)")] @{thm right_distrib},
   56.17 -      read_instantiate @{context} [(("a", 0), "(neg_numeral ?v)")] @{thm right_distrib},
   56.18 +      read_instantiate @{context} [(("a", 0), "(numeral ?v)")] @{thm distrib_left},
   56.19 +      read_instantiate @{context} [(("a", 0), "(neg_numeral ?v)")] @{thm distrib_left},
   56.20        @{thm divide_1}, @{thm divide_zero_left},
   56.21        @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
   56.22        @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
    57.1 --- a/src/HOL/RealDef.thy	Fri Oct 19 10:46:42 2012 +0200
    57.2 +++ b/src/HOL/RealDef.thy	Fri Oct 19 15:12:52 2012 +0200
    57.3 @@ -494,7 +494,7 @@
    57.4    show "1 * a = a"
    57.5      by transfer (simp add: mult_ac realrel_def)
    57.6    show "(a + b) * c = a * c + b * c"
    57.7 -    by transfer (simp add: left_distrib realrel_def)
    57.8 +    by transfer (simp add: distrib_right realrel_def)
    57.9    show "(0\<Colon>real) \<noteq> (1\<Colon>real)"
   57.10      by transfer (simp add: realrel_def)
   57.11    show "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
    58.1 --- a/src/HOL/RealVector.thy	Fri Oct 19 10:46:42 2012 +0200
    58.2 +++ b/src/HOL/RealVector.thy	Fri Oct 19 15:12:52 2012 +0200
    58.3 @@ -1081,8 +1081,8 @@
    58.4  lemma bounded_bilinear_mult:
    58.5    "bounded_bilinear (op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
    58.6  apply (rule bounded_bilinear.intro)
    58.7 -apply (rule left_distrib)
    58.8 -apply (rule right_distrib)
    58.9 +apply (rule distrib_right)
   58.10 +apply (rule distrib_left)
   58.11  apply (rule mult_scaleR_left)
   58.12  apply (rule mult_scaleR_right)
   58.13  apply (rule_tac x="1" in exI)
    59.1 --- a/src/HOL/Rings.thy	Fri Oct 19 10:46:42 2012 +0200
    59.2 +++ b/src/HOL/Rings.thy	Fri Oct 19 15:12:52 2012 +0200
    59.3 @@ -14,14 +14,14 @@
    59.4  begin
    59.5  
    59.6  class semiring = ab_semigroup_add + semigroup_mult +
    59.7 -  assumes left_distrib[algebra_simps, field_simps]: "(a + b) * c = a * c + b * c"
    59.8 -  assumes right_distrib[algebra_simps, field_simps]: "a * (b + c) = a * b + a * c"
    59.9 +  assumes distrib_right[algebra_simps, field_simps]: "(a + b) * c = a * c + b * c"
   59.10 +  assumes distrib_left[algebra_simps, field_simps]: "a * (b + c) = a * b + a * c"
   59.11  begin
   59.12  
   59.13  text{*For the @{text combine_numerals} simproc*}
   59.14  lemma combine_common_factor:
   59.15    "a * e + (b * e + c) = (a + b) * e + c"
   59.16 -by (simp add: left_distrib add_ac)
   59.17 +by (simp add: distrib_right add_ac)
   59.18  
   59.19  end
   59.20  
   59.21 @@ -37,11 +37,11 @@
   59.22  subclass semiring_0
   59.23  proof
   59.24    fix a :: 'a
   59.25 -  have "0 * a + 0 * a = 0 * a + 0" by (simp add: left_distrib [symmetric])
   59.26 +  have "0 * a + 0 * a = 0 * a + 0" by (simp add: distrib_right [symmetric])
   59.27    thus "0 * a = 0" by (simp only: add_left_cancel)
   59.28  next
   59.29    fix a :: 'a
   59.30 -  have "a * 0 + a * 0 = a * 0 + 0" by (simp add: right_distrib [symmetric])
   59.31 +  have "a * 0 + a * 0 = a * 0 + 0" by (simp add: distrib_left [symmetric])
   59.32    thus "a * 0 = 0" by (simp only: add_left_cancel)
   59.33  qed
   59.34  
   59.35 @@ -177,7 +177,7 @@
   59.36  proof -
   59.37    from `a dvd b` obtain b' where "b = a * b'" ..
   59.38    moreover from `a dvd c` obtain c' where "c = a * c'" ..
   59.39 -  ultimately have "b + c = a * (b' + c')" by (simp add: right_distrib)
   59.40 +  ultimately have "b + c = a * (b' + c')" by (simp add: distrib_left)
   59.41    then show ?thesis ..
   59.42  qed
   59.43  
   59.44 @@ -227,10 +227,10 @@
   59.45  text {* Distribution rules *}
   59.46  
   59.47  lemma minus_mult_left: "- (a * b) = - a * b"
   59.48 -by (rule minus_unique) (simp add: left_distrib [symmetric]) 
   59.49 +by (rule minus_unique) (simp add: distrib_right [symmetric]) 
   59.50  
   59.51  lemma minus_mult_right: "- (a * b) = a * - b"
   59.52 -by (rule minus_unique) (simp add: right_distrib [symmetric]) 
   59.53 +by (rule minus_unique) (simp add: distrib_left [symmetric]) 
   59.54  
   59.55  text{*Extract signs from products*}
   59.56  lemmas mult_minus_left [simp, no_atp] = minus_mult_left [symmetric]
   59.57 @@ -243,13 +243,13 @@
   59.58  by simp
   59.59  
   59.60  lemma right_diff_distrib[algebra_simps, field_simps]: "a * (b - c) = a * b - a * c"
   59.61 -by (simp add: right_distrib diff_minus)
   59.62 +by (simp add: distrib_left diff_minus)
   59.63  
   59.64  lemma left_diff_distrib[algebra_simps, field_simps]: "(a - b) * c = a * c - b * c"
   59.65 -by (simp add: left_distrib diff_minus)
   59.66 +by (simp add: distrib_right diff_minus)
   59.67  
   59.68  lemmas ring_distribs[no_atp] =
   59.69 -  right_distrib left_distrib left_diff_distrib right_diff_distrib
   59.70 +  distrib_left distrib_right left_diff_distrib right_diff_distrib
   59.71  
   59.72  lemma eq_add_iff1:
   59.73    "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
   59.74 @@ -262,7 +262,7 @@
   59.75  end
   59.76  
   59.77  lemmas ring_distribs[no_atp] =
   59.78 -  right_distrib left_distrib left_diff_distrib right_diff_distrib
   59.79 +  distrib_left distrib_right left_diff_distrib right_diff_distrib
   59.80  
   59.81  class comm_ring = comm_semiring + ab_group_add
   59.82  begin
   59.83 @@ -506,7 +506,7 @@
   59.84  proof-
   59.85    from assms have "u * x + v * y \<le> u * a + v * a"
   59.86      by (simp add: add_mono mult_left_mono)
   59.87 -  thus ?thesis using assms unfolding left_distrib[symmetric] by simp
   59.88 +  thus ?thesis using assms unfolding distrib_right[symmetric] by simp
   59.89  qed
   59.90  
   59.91  end
   59.92 @@ -640,7 +640,7 @@
   59.93    from assms have "u * x + v * y < u * a + v * a"
   59.94      by (cases "u = 0")
   59.95         (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
   59.96 -  thus ?thesis using assms unfolding left_distrib[symmetric] by simp
   59.97 +  thus ?thesis using assms unfolding distrib_right[symmetric] by simp
   59.98  qed
   59.99  
  59.100  end
    60.1 --- a/src/HOL/Transcendental.thy	Fri Oct 19 10:46:42 2012 +0200
    60.2 +++ b/src/HOL/Transcendental.thy	Fri Oct 19 15:12:52 2012 +0200
    60.3 @@ -35,7 +35,7 @@
    60.4  apply (simp del: setsum_op_ivl_Suc)
    60.5  apply (subst setsum_op_ivl_Suc)
    60.6  apply (subst lemma_realpow_diff_sumr)
    60.7 -apply (simp add: right_distrib del: setsum_op_ivl_Suc)
    60.8 +apply (simp add: distrib_left del: setsum_op_ivl_Suc)
    60.9  apply (subst mult_left_commute [of "x - y"])
   60.10  apply (erule subst)
   60.11  apply (simp add: algebra_simps)
   60.12 @@ -922,7 +922,7 @@
   60.13      by (simp only: Suc)
   60.14    also have "\<dots> = x * (\<Sum>i=0..n. S x i * S y (n-i))
   60.15                  + y * (\<Sum>i=0..n. S x i * S y (n-i))"
   60.16 -    by (rule left_distrib)
   60.17 +    by (rule distrib_right)
   60.18    also have "\<dots> = (\<Sum>i=0..n. (x * S x i) * S y (n-i))
   60.19                  + (\<Sum>i=0..n. S x i * (y * S y (n-i)))"
   60.20      by (simp only: setsum_right_distrib mult_ac)
   60.21 @@ -1001,7 +1001,7 @@
   60.22  
   60.23  lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
   60.24  apply (induct "n")
   60.25 -apply (auto simp add: real_of_nat_Suc right_distrib exp_add mult_commute)
   60.26 +apply (auto simp add: real_of_nat_Suc distrib_left exp_add mult_commute)
   60.27  done
   60.28  
   60.29  text {* Strict monotonicity of exponential. *}
   60.30 @@ -1626,7 +1626,7 @@
   60.31  
   60.32  lemma cos_npi [simp]: "cos (real n * pi) = -1 ^ n"
   60.33  apply (induct "n")
   60.34 -apply (auto simp add: real_of_nat_Suc left_distrib)
   60.35 +apply (auto simp add: real_of_nat_Suc distrib_right)
   60.36  done
   60.37  
   60.38  lemma cos_npi2 [simp]: "cos (pi * real n) = -1 ^ n"
   60.39 @@ -1638,7 +1638,7 @@
   60.40  
   60.41  lemma sin_npi [simp]: "sin (real (n::nat) * pi) = 0"
   60.42  apply (induct "n")
   60.43 -apply (auto simp add: real_of_nat_Suc left_distrib)
   60.44 +apply (auto simp add: real_of_nat_Suc distrib_right)
   60.45  done
   60.46  
   60.47  lemma sin_npi2 [simp]: "sin (pi * real (n::nat)) = 0"
   60.48 @@ -1784,7 +1784,7 @@
   60.49        \<exists>n::nat. even n & x = real n * (pi/2)"
   60.50  apply (subgoal_tac "\<exists>n::nat. ~ even n & x + pi/2 = real n * (pi/2) ")
   60.51   apply (clarify, rule_tac x = "n - 1" in exI)
   60.52 - apply (force simp add: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib)
   60.53 + apply (force simp add: odd_Suc_mult_two_ex real_of_nat_Suc distrib_right)
   60.54  apply (rule cos_zero_lemma)
   60.55  apply (simp_all add: cos_add)
   60.56  done
   60.57 @@ -1799,7 +1799,7 @@
   60.58  apply (drule cos_zero_lemma, assumption+)
   60.59  apply (cut_tac x="-x" in cos_zero_lemma, simp, simp)
   60.60  apply (force simp add: minus_equation_iff [of x])
   60.61 -apply (auto simp only: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib)
   60.62 +apply (auto simp only: odd_Suc_mult_two_ex real_of_nat_Suc distrib_right)
   60.63  apply (auto simp add: cos_add)
   60.64  done
   60.65  
   60.66 @@ -2029,7 +2029,7 @@
   60.67  lemma tan_periodic_nat[simp]: fixes n :: nat shows "tan (x + real n * pi) = tan x"
   60.68  proof (induct n arbitrary: x)
   60.69    case (Suc n)
   60.70 -  have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi" unfolding Suc_eq_plus1 real_of_nat_add real_of_one left_distrib by auto
   60.71 +  have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi" unfolding Suc_eq_plus1 real_of_nat_add real_of_one distrib_right by auto
   60.72    show ?case unfolding split_pi_off using Suc by auto
   60.73  qed auto
   60.74  
   60.75 @@ -2212,7 +2212,7 @@
   60.76    show "0 \<le> cos (arctan x)"
   60.77      by (intro less_imp_le cos_gt_zero_pi arctan_lbound arctan_ubound)
   60.78    have "(cos (arctan x))\<twosuperior> * (1 + (tan (arctan x))\<twosuperior>) = 1"
   60.79 -    unfolding tan_def by (simp add: right_distrib power_divide)
   60.80 +    unfolding tan_def by (simp add: distrib_left power_divide)
   60.81    thus "(cos (arctan x))\<twosuperior> = (1 / sqrt (1 + x\<twosuperior>))\<twosuperior>"
   60.82      using `0 < 1 + x\<twosuperior>` by (simp add: power_divide eq_divide_eq)
   60.83  qed
   60.84 @@ -2226,7 +2226,7 @@
   60.85  apply (rule power_inverse [THEN subst])
   60.86  apply (rule_tac c1 = "(cos x)\<twosuperior>" in real_mult_right_cancel [THEN iffD1])
   60.87  apply (auto dest: field_power_not_zero
   60.88 -        simp add: power_mult_distrib left_distrib power_divide tan_def
   60.89 +        simp add: power_mult_distrib distrib_right power_divide tan_def
   60.90                    mult_assoc power_inverse [symmetric])
   60.91  done
   60.92  
   60.93 @@ -2397,7 +2397,7 @@
   60.94    have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
   60.95      by (auto simp add: algebra_simps sin_add)
   60.96    thus ?thesis
   60.97 -    by (simp add: real_of_nat_Suc left_distrib add_divide_distrib
   60.98 +    by (simp add: real_of_nat_Suc distrib_right add_divide_distrib
   60.99                    mult_commute [of pi])
  60.100  qed
  60.101  
  60.102 @@ -2418,7 +2418,7 @@
  60.103  done
  60.104  
  60.105  lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
  60.106 -by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib add_divide_distrib, auto)
  60.107 +by (simp only: cos_add sin_add real_of_nat_Suc distrib_right distrib_left add_divide_distrib, auto)
  60.108  
  60.109  lemma DERIV_cos_add [simp]: "DERIV (%x. cos (x + k)) xa :> - sin (xa + k)"
  60.110    by (auto intro!: DERIV_intros)
    61.1 --- a/src/HOL/Word/Misc_Numeric.thy	Fri Oct 19 10:46:42 2012 +0200
    61.2 +++ b/src/HOL/Word/Misc_Numeric.thy	Fri Oct 19 15:12:52 2012 +0200
    61.3 @@ -301,7 +301,7 @@
    61.4    apply assumption
    61.5    done
    61.6  
    61.7 -lemmas less_le_mult = less_le_mult' [simplified left_distrib, simplified]
    61.8 +lemmas less_le_mult = less_le_mult' [simplified distrib_right, simplified]
    61.9  
   61.10  lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult, 
   61.11    simplified left_diff_distrib]
    62.1 --- a/src/HOL/Word/WordBitwise.thy	Fri Oct 19 10:46:42 2012 +0200
    62.2 +++ b/src/HOL/Word/WordBitwise.thy	Fri Oct 19 15:12:52 2012 +0200
    62.3 @@ -308,7 +308,7 @@
    62.4      using Cons
    62.5      apply (simp add: trans [OF of_bl_append add_commute]
    62.6                       rbl_mul_simps rbl_word_plus'
    62.7 -                     Cons.hyps left_distrib mult_bit
    62.8 +                     Cons.hyps distrib_right mult_bit
    62.9                       shiftl rbl_shiftl)
   62.10      apply (simp add: takefill_alt word_size rev_map take_rbl_plus
   62.11                       min_def)
    63.1 --- a/src/HOL/ex/BT.thy	Fri Oct 19 10:46:42 2012 +0200
    63.2 +++ b/src/HOL/ex/BT.thy	Fri Oct 19 15:12:52 2012 +0200
    63.3 @@ -107,7 +107,7 @@
    63.4  
    63.5  lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t"
    63.6    apply (induct t)
    63.7 -   apply (simp_all add: left_distrib)
    63.8 +   apply (simp_all add: distrib_right)
    63.9    done
   63.10  
   63.11  lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
   63.12 @@ -148,7 +148,7 @@
   63.13  lemma n_leaves_append [simp]:
   63.14       "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2"
   63.15    apply (induct t1)
   63.16 -   apply (simp_all add: left_distrib)
   63.17 +   apply (simp_all add: distrib_right)
   63.18    done
   63.19  
   63.20  lemma bt_map_append:
    64.1 --- a/src/HOL/ex/Dedekind_Real.thy	Fri Oct 19 10:46:42 2012 +0200
    64.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Fri Oct 19 15:12:52 2012 +0200
    64.3 @@ -285,7 +285,7 @@
    64.4    show "\<exists>x' \<in> A. \<exists>y'\<in>B. z = x' + y'"
    64.5    proof (intro bexI)
    64.6      show "z = x*?f + y*?f"
    64.7 -      by (simp add: left_distrib [symmetric] divide_inverse mult_ac
    64.8 +      by (simp add: distrib_right [symmetric] divide_inverse mult_ac
    64.9            order_less_imp_not_eq2)
   64.10    next
   64.11      show "y * ?f \<in> B"
   64.12 @@ -534,7 +534,7 @@
   64.13  lemma distrib_subset1:
   64.14       "Rep_preal (w * (x + y)) \<subseteq> Rep_preal (w * x + w * y)"
   64.15  apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_mult_iff)
   64.16 -apply (force simp add: right_distrib)
   64.17 +apply (force simp add: distrib_left)
   64.18  done
   64.19  
   64.20  lemma preal_add_mult_distrib_mean:
   64.21 @@ -555,13 +555,13 @@
   64.22    proof (cases rule: linorder_le_cases)
   64.23      assume "a \<le> b"
   64.24      hence "?c \<le> b"
   64.25 -      by (simp add: pos_divide_le_eq right_distrib mult_right_mono
   64.26 +      by (simp add: pos_divide_le_eq distrib_left mult_right_mono
   64.27                      order_less_imp_le)
   64.28      thus ?thesis by (rule preal_downwards_closed' [OF Rep_preal b cpos])
   64.29    next
   64.30      assume "b \<le> a"
   64.31      hence "?c \<le> a"
   64.32 -      by (simp add: pos_divide_le_eq right_distrib mult_right_mono
   64.33 +      by (simp add: pos_divide_le_eq distrib_left mult_right_mono
   64.34                      order_less_imp_le)
   64.35      thus ?thesis by (rule preal_downwards_closed' [OF Rep_preal a cpos])
   64.36    qed
   64.37 @@ -1333,7 +1333,7 @@
   64.38            x * x1 + y * y1 + (x * y2 + y * x2) =
   64.39            x * x2 + y * y2 + (x * y1 + y * x1)"
   64.40  apply (simp add: add_left_commute add_assoc [symmetric])
   64.41 -apply (simp add: add_assoc right_distrib [symmetric])
   64.42 +apply (simp add: add_assoc distrib_left [symmetric])
   64.43  apply (simp add: add_commute)
   64.44  done
   64.45  
   64.46 @@ -1543,7 +1543,7 @@
   64.47  apply (rule real_sum_gt_zero_less)
   64.48  apply (drule real_less_sum_gt_zero [of x y])
   64.49  apply (drule real_mult_order, assumption)
   64.50 -apply (simp add: right_distrib)
   64.51 +apply (simp add: distrib_left)
   64.52  done
   64.53  
   64.54  instantiation real :: distrib_lattice
   64.55 @@ -1986,7 +1986,7 @@
   64.56      from t_is_Lub have "x * of_nat (Suc n) \<le> t"
   64.57        by (simp add: isLubD2)
   64.58      hence  "x * (of_nat n) + x \<le> t"
   64.59 -      by (simp add: right_distrib)
   64.60 +      by (simp add: distrib_left)
   64.61      thus  "x * (of_nat n) \<le> t + - x" by arith
   64.62    qed
   64.63  
    65.1 --- a/src/HOL/ex/Gauge_Integration.thy	Fri Oct 19 10:46:42 2012 +0200
    65.2 +++ b/src/HOL/ex/Gauge_Integration.thy	Fri Oct 19 15:12:52 2012 +0200
    65.3 @@ -521,9 +521,9 @@
    65.4                      = (f z - f x) / (z - x) - f' x")
    65.5   apply (simp add: abs_mult [symmetric] mult_ac diff_minus)
    65.6  apply (subst mult_commute)
    65.7 -apply (simp add: left_distrib diff_minus)
    65.8 +apply (simp add: distrib_right diff_minus)
    65.9  apply (simp add: mult_assoc divide_inverse)
   65.10 -apply (simp add: left_distrib)
   65.11 +apply (simp add: distrib_right)
   65.12  done
   65.13  
   65.14  lemma lemma_straddle:
    66.1 --- a/src/HOL/ex/Numeral_Representation.thy	Fri Oct 19 10:46:42 2012 +0200
    66.2 +++ b/src/HOL/ex/Numeral_Representation.thy	Fri Oct 19 15:12:52 2012 +0200
    66.3 @@ -153,7 +153,7 @@
    66.4    "Dig1 n * Dig0 m = Dig0 (n * Dig0 m + m)"
    66.5    "Dig1 n * Dig1 m = Dig1 (n * Dig1 m + m)"
    66.6    by (simp_all add: num_eq_iff nat_of_num_add nat_of_num_mult
    66.7 -                    left_distrib right_distrib)
    66.8 +                    distrib_right distrib_left)
    66.9  
   66.10  lemma less_eq_num_code [numeral, simp, code]:
   66.11    "One \<le> n \<longleftrightarrow> True"
   66.12 @@ -243,7 +243,7 @@
   66.13    by (induct n rule: num_induct) (simp_all add: add_One add_inc of_num_inc add_ac)
   66.14  
   66.15  lemma of_num_mult: "of_num (m * n) = of_num m * of_num n"
   66.16 -  by (induct n rule: num_induct) (simp_all add: mult_One mult_inc of_num_add of_num_inc right_distrib)
   66.17 +  by (induct n rule: num_induct) (simp_all add: mult_One mult_inc of_num_add of_num_inc distrib_left)
   66.18  
   66.19  declare of_num.simps [simp del]
   66.20  
   66.21 @@ -792,7 +792,7 @@
   66.22  
   66.23  lemma mult_of_num_commute: "x * of_num n = of_num n * x"
   66.24  by (induct n)
   66.25 -  (simp_all only: of_num.simps left_distrib right_distrib mult_1_left mult_1_right)
   66.26 +  (simp_all only: of_num.simps distrib_right distrib_left mult_1_left mult_1_right)
   66.27  
   66.28  definition
   66.29    "commutes_with a b \<longleftrightarrow> a * b = b * a"