Renamed {left,right}_distrib to distrib_{right,left}.
--- a/NEWS Fri Oct 19 10:46:42 2012 +0200
+++ b/NEWS Fri Oct 19 15:12:52 2012 +0200
@@ -76,7 +76,6 @@
written just "typedef t = A". INCOMPATIBILITY, need to adapt theories
accordingly.
-
* Theory "Library/Multiset":
- Renamed constants
@@ -142,6 +141,13 @@
INCOMPATIBILITY.
+* HOL/Rings: renamed lemmas
+
+left_distrib ~> distrib_right
+right_distrib ~> distrib_left
+
+in class semiring. INCOMPATIBILITY.
+
* HOL/BNF: New (co)datatype package based on bounded natural
functors with support for mixed, nested recursion and interesting
non-free datatypes.
--- a/src/HOL/Algebra/IntRing.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Algebra/IntRing.thy Fri Oct 19 15:12:52 2012 +0200
@@ -35,7 +35,7 @@
apply (rule abelian_groupI, simp_all)
defer 1
apply (rule comm_monoidI, simp_all)
- apply (rule left_distrib)
+ apply (rule distrib_right)
apply (fast intro: left_minus)
done
@@ -165,7 +165,7 @@
and "a_inv \<Z> x = - x"
and "a_minus \<Z> x y = x - y"
proof -
- show "domain \<Z>" by unfold_locales (auto simp: left_distrib right_distrib)
+ show "domain \<Z>" by unfold_locales (auto simp: distrib_right distrib_left)
qed (simp
add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq int_a_inv_eq int_a_minus_eq)+
--- a/src/HOL/Algebra/UnivPoly.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Fri Oct 19 15:12:52 2012 +0200
@@ -1818,7 +1818,7 @@
lemma INTEG_cring: "cring INTEG"
by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
- left_minus left_distrib)
+ left_minus distrib_right)
lemma INTEG_id_eval:
"UP_pre_univ_prop INTEG INTEG id"
--- a/src/HOL/Big_Operators.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Big_Operators.thy Fri Oct 19 15:12:52 2012 +0200
@@ -699,7 +699,7 @@
proof induct
case empty thus ?case by simp
next
- case (insert x A) thus ?case by (simp add: right_distrib)
+ case (insert x A) thus ?case by (simp add: distrib_left)
qed
next
case False thus ?thesis by (simp add: setsum_def)
@@ -713,7 +713,7 @@
proof induct
case empty thus ?case by simp
next
- case (insert x A) thus ?case by (simp add: left_distrib)
+ case (insert x A) thus ?case by (simp add: distrib_right)
qed
next
case False thus ?thesis by (simp add: setsum_def)
--- a/src/HOL/Code_Numeral.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Code_Numeral.thy Fri Oct 19 15:12:52 2012 +0200
@@ -153,7 +153,7 @@
"n < m \<longleftrightarrow> nat_of n < nat_of m"
instance proof
-qed (auto simp add: code_numeral left_distrib intro: mult_commute)
+qed (auto simp add: code_numeral distrib_right intro: mult_commute)
end
--- a/src/HOL/Complex.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Complex.thy Fri Oct 19 15:12:52 2012 +0200
@@ -141,7 +141,7 @@
instance
by intro_classes (simp_all add: complex_mult_def
- right_distrib left_distrib right_diff_distrib left_diff_distrib
+ distrib_left distrib_right right_diff_distrib left_diff_distrib
complex_inverse_def complex_divide_def
power2_eq_square add_divide_distrib [symmetric]
complex_eq_iff)
@@ -206,9 +206,9 @@
proof
fix a b :: real and x y :: complex
show "scaleR a (x + y) = scaleR a x + scaleR a y"
- by (simp add: complex_eq_iff right_distrib)
+ by (simp add: complex_eq_iff distrib_left)
show "scaleR (a + b) x = scaleR a x + scaleR b x"
- by (simp add: complex_eq_iff left_distrib)
+ by (simp add: complex_eq_iff distrib_right)
show "scaleR a (scaleR b x) = scaleR (a * b) x"
by (simp add: complex_eq_iff mult_assoc)
show "scaleR 1 x = x"
@@ -297,7 +297,7 @@
(simp add: real_sqrt_sum_squares_triangle_ineq)
show "norm (scaleR r x) = \<bar>r\<bar> * norm x"
by (induct x)
- (simp add: power_mult_distrib right_distrib [symmetric] real_sqrt_mult)
+ (simp add: power_mult_distrib distrib_left [symmetric] real_sqrt_mult)
show "norm (x * y) = norm x * norm y"
by (induct x, induct y)
(simp add: real_sqrt_mult [symmetric] power2_eq_square algebra_simps)
@@ -730,7 +730,7 @@
unfolding z b_def rcis_def using `r \<noteq> 0`
by (simp add: of_real_def sgn_scaleR sgn_if, simp add: cis_def)
have cis_2pi_nat: "\<And>n. cis (2 * pi * real_of_nat n) = 1"
- by (induct_tac n, simp_all add: right_distrib cis_mult [symmetric],
+ by (induct_tac n, simp_all add: distrib_left cis_mult [symmetric],
simp add: cis_def)
have cis_2pi_int: "\<And>x. cis (2 * pi * real_of_int x) = 1"
by (case_tac x rule: int_diff_cases,
--- a/src/HOL/Decision_Procs/Approximation.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Fri Oct 19 15:12:52 2012 +0200
@@ -305,7 +305,7 @@
finally have "sqrt x < (?b + x / ?b)/2" using sqrt_ub_pos_pos_1[OF Suc _ `0 < real x`] by auto
also have "\<dots> \<le> (?b + (float_divr prec x ?b))/2" by (rule divide_right_mono, auto simp add: float_divr)
also have "\<dots> = (Float 1 -1) * (?b + (float_divr prec x ?b))" by simp
- finally show ?case unfolding sqrt_iteration.simps Let_def right_distrib .
+ finally show ?case unfolding sqrt_iteration.simps Let_def distrib_left .
qed
lemma sqrt_iteration_lower_bound: assumes "0 < real x"
@@ -955,7 +955,7 @@
using Maclaurin_sin_expansion3[OF `0 < 2 * n + 1` `0 < real x`]
unfolding sin_coeff_def by auto
- have "?rest = cos t * -1^n" unfolding sin_add cos_add real_of_nat_add left_distrib right_distrib by auto
+ have "?rest = cos t * -1^n" unfolding sin_add cos_add real_of_nat_add distrib_right distrib_left by auto
moreover
have "t \<le> pi / 2" using `t < real x` and `x \<le> pi / 2` by auto
hence "0 \<le> cos t" using `0 < t` and cos_ge_zero by auto
@@ -1173,7 +1173,7 @@
proof (induct n arbitrary: x)
case (Suc n)
have split_pi_off: "x + (Suc n) * (2 * pi) = (x + n * (2 * pi)) + 2 * pi"
- unfolding Suc_eq_plus1 real_of_nat_add real_of_one left_distrib by auto
+ unfolding Suc_eq_plus1 real_of_nat_add real_of_one distrib_right by auto
show ?case unfolding split_pi_off using Suc by auto
qed auto
@@ -1714,7 +1714,7 @@
lemma ln_add: assumes "0 < x" and "0 < y" shows "ln (x + y) = ln x + ln (1 + y / x)"
proof -
have "x \<noteq> 0" using assms by auto
- 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
+ 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
moreover
have "0 < y / x" using assms divide_pos_pos by auto
hence "0 < 1 + y / x" by auto
--- a/src/HOL/Decision_Procs/Cooper.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Fri Oct 19 15:12:52 2012 +0200
@@ -413,7 +413,7 @@
apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
apply (case_tac "n1 = n2")
apply(simp_all add: algebra_simps)
-apply(simp add: left_distrib[symmetric])
+apply(simp add: distrib_right[symmetric])
done
lemma numadd_nb: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
@@ -727,7 +727,7 @@
by (simp add: Let_def split_def)
from abj 3 m0 have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \<and> ?N ?b" by blast
from th have "?I x (CN 0 n a') = ?I x (CN 0 (i+?j) ?b)" by simp
- also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))" by (simp add: left_distrib)
+ also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))" by (simp add: distrib_right)
finally have "?I x (CN 0 n a') = ?I x (CN 0 i a)" using th2 by simp
with th2 th have ?case using m0 by blast}
ultimately show ?case by blast
@@ -754,7 +754,7 @@
with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
from abjs 5 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
from th3[simplified] th2[simplified] th[simplified] show ?case
- by (simp add: left_distrib)
+ by (simp add: distrib_right)
next
case (6 s t n a)
let ?ns = "fst (zsplit0 s)"
@@ -779,7 +779,7 @@
by (simp add: Let_def split_def)
from abj 7 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
hence "?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)" by simp
- also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: right_distrib)
+ also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: distrib_left)
finally show ?case using th th2 by simp
qed
--- a/src/HOL/Decision_Procs/Ferrack.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Fri Oct 19 15:12:52 2012 +0200
@@ -569,7 +569,7 @@
apply (induct t s rule: numadd.induct, simp_all add: Let_def)
apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
apply (case_tac "n1 = n2", simp_all add: algebra_simps)
-by (simp only: left_distrib[symmetric],simp)
+by (simp only: distrib_right[symmetric],simp)
lemma numadd_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
by (induct t s rule: numadd.induct, auto simp add: Let_def)
@@ -937,7 +937,7 @@
by (simp add: Let_def split_def algebra_simps)
also have "\<dots> = Inum bs a + Inum bs b" using 2 by (cases "rsplit0 a") auto
finally show ?case using nb by simp
-qed (auto simp add: Let_def split_def algebra_simps, simp add: right_distrib[symmetric])
+qed (auto simp add: Let_def split_def algebra_simps, simp add: distrib_left[symmetric])
(* Linearize a formula*)
definition
--- a/src/HOL/Decision_Procs/MIR.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Fri Oct 19 15:12:52 2012 +0200
@@ -743,11 +743,11 @@
apply (induct t s rule: numadd.induct, simp_all add: Let_def)
apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
apply (case_tac "n1 = n2", simp_all add: algebra_simps)
- apply (simp only: left_distrib[symmetric])
+ apply (simp only: distrib_right[symmetric])
apply simp
apply (case_tac "lex_bnd t1 t2", simp_all)
apply (case_tac "c1+c2 = 0")
- 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)
+ 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)
lemma numadd_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
by (induct t s rule: numadd.induct, auto simp add: Let_def)
@@ -1493,7 +1493,7 @@
with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
from abjs 6 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
from th3[simplified] th2[simplified] th[simplified] show ?case
- by (simp add: left_distrib)
+ by (simp add: distrib_right)
next
case (7 s t n a)
let ?ns = "fst (zsplit0 s)"
@@ -1518,7 +1518,7 @@
by (simp add: Let_def split_def)
from abj 8 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
hence "?I x (Mul i t) = (real i) * ?I x (CN 0 ?nt ?at)" by simp
- also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: right_distrib)
+ also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: distrib_left)
finally show ?case using th th2 by simp
next
case (9 t n a)
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Oct 19 15:12:52 2012 +0200
@@ -224,7 +224,7 @@
apply (induct t s rule: tmadd.induct, simp_all add: Let_def)
apply (case_tac "c1 +\<^sub>p c2 = 0\<^sub>p",case_tac "n1 \<le> n2", simp_all)
apply (case_tac "n1 = n2", simp_all add: field_simps)
-apply (simp only: right_distrib[symmetric])
+apply (simp only: distrib_left[symmetric])
by (auto simp del: polyadd simp add: polyadd[symmetric])
lemma tmadd_nb0[simp]: "\<lbrakk> tmbound0 t ; tmbound0 s\<rbrakk> \<Longrightarrow> tmbound0 (tmadd (t,s))"
@@ -358,7 +358,7 @@
apply (simp add: Let_def split_def field_simps)
apply (simp add: Let_def split_def field_simps)
apply (simp add: Let_def split_def field_simps)
- apply (simp add: Let_def split_def mult_assoc right_distrib[symmetric])
+ apply (simp add: Let_def split_def mult_assoc distrib_left[symmetric])
apply (simp add: Let_def split_def field_simps)
apply (simp add: Let_def split_def field_simps)
done
@@ -1933,7 +1933,7 @@
also have "\<dots> \<longleftrightarrow> 2*?d * (?a * (-?s / (2*?d)) + ?r) = 0"
using d mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * (2*?d / (2*?d)) + 2*?d*?r= 0"
- by (simp add: field_simps right_distrib[of "2*?d"] del: right_distrib)
+ by (simp add: field_simps distrib_left[of "2*?d"] del: distrib_left)
also have "\<dots> \<longleftrightarrow> - (?a * ?s) + 2*?d*?r = 0" using d by simp
finally have ?thesis using c d
@@ -1947,7 +1947,7 @@
also have "\<dots> \<longleftrightarrow> 2*?c * (?a * (-?t / (2*?c)) + ?r) = 0"
using c mult_cancel_left[of "2*?c" "(?a * (-?t / (2*?c)) + ?r)" 0] by simp
also have "\<dots> \<longleftrightarrow> (?a * -?t)* (2*?c) / (2*?c) + 2*?c*?r= 0"
- by (simp add: field_simps right_distrib[of "2*?c"] del: right_distrib)
+ by (simp add: field_simps distrib_left[of "2*?c"] del: distrib_left)
also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2*?c*?r = 0" using c by simp
finally have ?thesis using c d
by (simp add: r[of "- (?t/ (2*?c))"] msubsteq_def Let_def evaldjf_ex)
@@ -1964,7 +1964,7 @@
using c d mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r =0"
using nonzero_mult_divide_cancel_left [OF dc] c d
- by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis using c d
by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubsteq_def Let_def evaldjf_ex field_simps)
}
@@ -2015,7 +2015,7 @@
also have "\<dots> \<longleftrightarrow> 2*?d * (?a * (-?s / (2*?d)) + ?r) \<noteq> 0"
using d mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * (2*?d / (2*?d)) + 2*?d*?r\<noteq> 0"
- by (simp add: field_simps right_distrib[of "2*?d"] del: right_distrib)
+ by (simp add: field_simps distrib_left[of "2*?d"] del: distrib_left)
also have "\<dots> \<longleftrightarrow> - (?a * ?s) + 2*?d*?r \<noteq> 0" using d by simp
finally have ?thesis using c d
@@ -2029,7 +2029,7 @@
also have "\<dots> \<longleftrightarrow> 2*?c * (?a * (-?t / (2*?c)) + ?r) \<noteq> 0"
using c mult_cancel_left[of "2*?c" "(?a * (-?t / (2*?c)) + ?r)" 0] by simp
also have "\<dots> \<longleftrightarrow> (?a * -?t)* (2*?c) / (2*?c) + 2*?c*?r \<noteq> 0"
- by (simp add: field_simps right_distrib[of "2*?c"] del: right_distrib)
+ by (simp add: field_simps distrib_left[of "2*?c"] del: distrib_left)
also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2*?c*?r \<noteq> 0" using c by simp
finally have ?thesis using c d
by (simp add: r[of "- (?t/ (2*?c))"] msubstneq_def Let_def evaldjf_ex)
@@ -2046,7 +2046,7 @@
using c d mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \<noteq> 0"
using nonzero_mult_divide_cancel_left[OF dc] c d
- by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis using c d
by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstneq_def Let_def evaldjf_ex field_simps)
}
@@ -2112,7 +2112,7 @@
using dc' dc'' mult_less_cancel_left_disj[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r < 0"
using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
- by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis using dc c d nc nd dc'
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)
}
@@ -2134,7 +2134,7 @@
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
also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2*?c*?d*?r < 0"
using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
- by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis using dc c d nc nd
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)
}
@@ -2149,7 +2149,7 @@
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
also have "\<dots> \<longleftrightarrow> - ?a*?t+ 2*?c *?r < 0"
using nonzero_mult_divide_cancel_left[OF c'] c
- by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
finally have ?thesis using c d nc nd
by(simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
}
@@ -2163,7 +2163,7 @@
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
also have "\<dots> \<longleftrightarrow> ?a*?t - 2*?c *?r < 0"
using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
- by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis using c d nc nd
by(simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
}
@@ -2179,7 +2179,7 @@
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
also have "\<dots> \<longleftrightarrow> - ?a*?s+ 2*?d *?r < 0"
using nonzero_mult_divide_cancel_left[OF d'] d
- by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
finally have ?thesis using c d nc nd
by(simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
}
@@ -2193,7 +2193,7 @@
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
also have "\<dots> \<longleftrightarrow> ?a*?s - 2*?d *?r < 0"
using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
- by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis using c d nc nd
by(simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
}
@@ -2258,7 +2258,7 @@
using dc' dc'' mult_le_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r <= 0"
using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
- by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis using dc c d nc nd dc'
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)
}
@@ -2280,7 +2280,7 @@
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
also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2*?c*?d*?r <= 0"
using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
- by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis using dc c d nc nd
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)
}
@@ -2295,7 +2295,7 @@
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
also have "\<dots> \<longleftrightarrow> - ?a*?t+ 2*?c *?r <= 0"
using nonzero_mult_divide_cancel_left[OF c'] c
- by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
finally have ?thesis using c d nc nd
by(simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
}
@@ -2309,7 +2309,7 @@
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
also have "\<dots> \<longleftrightarrow> ?a*?t - 2*?c *?r <= 0"
using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
- by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis using c d nc nd
by(simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
}
@@ -2325,7 +2325,7 @@
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
also have "\<dots> \<longleftrightarrow> - ?a*?s+ 2*?d *?r <= 0"
using nonzero_mult_divide_cancel_left[OF d'] d
- by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
finally have ?thesis using c d nc nd
by(simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
}
@@ -2339,7 +2339,7 @@
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
also have "\<dots> \<longleftrightarrow> ?a*?s - 2*?d *?r <= 0"
using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
- by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis using c d nc nd
by(simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
}
--- a/src/HOL/Decision_Procs/Polynomial_List.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy Fri Oct 19 15:12:52 2012 +0200
@@ -128,7 +128,7 @@
"\<forall>q. a %* ( p +++ q) = (a %* p +++ a %* q)"
apply (induct "p", simp, clarify)
apply (case_tac "q")
-apply (simp_all add: right_distrib)
+apply (simp_all add: distrib_left)
done
lemma pmult_by_x[simp]: "[0, 1] *** t = ((0)#t)"
@@ -142,13 +142,13 @@
apply (subgoal_tac "\<forall>p2. poly (p1 +++ p2) x = poly (p1) x + poly (p2) x")
apply (induct_tac [2] "p1", auto)
apply (case_tac "p2")
-apply (auto simp add: right_distrib)
+apply (auto simp add: distrib_left)
done
lemma poly_cmult: "poly (c %* p) x = c * poly p x"
apply (induct "p")
apply (case_tac [2] "x=0")
-apply (auto simp add: right_distrib mult_ac)
+apply (auto simp add: distrib_left mult_ac)
done
lemma poly_minus: "poly (-- p) x = - (poly p x)"
@@ -162,7 +162,7 @@
apply (induct "p1")
apply (auto simp add: poly_cmult)
apply (case_tac p1)
-apply (auto simp add: poly_cmult poly_add left_distrib right_distrib mult_ac)
+apply (auto simp add: poly_cmult poly_add distrib_right distrib_left mult_ac)
done
lemma poly_exp: "poly (p %^ n) (x::'a::comm_ring_1) = (poly p x) ^ n"
@@ -206,7 +206,7 @@
lemma poly_linear_divides: "(poly p a = 0) = ((p = []) | (\<exists>q. p = [-a, 1] *** q))"
-apply (auto simp add: poly_add poly_cmult right_distrib)
+apply (auto simp add: poly_add poly_cmult distrib_left)
apply (case_tac "p", simp)
apply (cut_tac h = aa and t = list and a = a in poly_linear_rem, safe)
apply (case_tac "q", auto)
@@ -408,7 +408,7 @@
by (auto simp add: field_simps poly_add poly_minus_def fun_eq poly_cmult)
lemma poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))"
-by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult right_distrib)
+by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult distrib_left)
lemma poly_mult_left_cancel: "(poly (p *** q) = poly (p *** r)) = (poly p = poly ([]::('a::{idom, ring_char_0}) list) | poly q = poly r)"
apply (rule_tac p1 = "p *** q" in poly_add_minus_zero_iff [THEN subst])
@@ -464,9 +464,9 @@
text{*Basics of divisibility.*}
lemma poly_primes: "([a, (1::'a::idom)] divides (p *** q)) = ([a, 1] divides p | [a, 1] divides q)"
-apply (auto simp add: divides_def fun_eq poly_mult poly_add poly_cmult left_distrib [symmetric])
+apply (auto simp add: divides_def fun_eq poly_mult poly_add poly_cmult distrib_right [symmetric])
apply (drule_tac x = "-a" in spec)
-apply (auto simp add: poly_linear_divides poly_add poly_cmult left_distrib [symmetric])
+apply (auto simp add: poly_linear_divides poly_add poly_cmult distrib_right [symmetric])
apply (rule_tac x = "qa *** q" in exI)
apply (rule_tac [2] x = "p *** qa" in exI)
apply (auto simp add: poly_add poly_mult poly_cmult mult_ac)
@@ -501,7 +501,7 @@
"[| p divides q; p divides r |] ==> p divides (q +++ r)"
apply (simp add: divides_def, auto)
apply (rule_tac x = "qa +++ qaa" in exI)
-apply (auto simp add: poly_add fun_eq poly_mult right_distrib)
+apply (auto simp add: poly_add fun_eq poly_mult distrib_left)
done
lemma poly_divides_diff:
@@ -557,7 +557,7 @@
apply (unfold divides_def)
apply (rule_tac x = q in exI)
apply (induct_tac "n", simp)
-apply (simp (no_asm_simp) add: poly_add poly_cmult poly_mult right_distrib mult_ac)
+apply (simp (no_asm_simp) add: poly_add poly_cmult poly_mult distrib_left mult_ac)
apply safe
apply (subgoal_tac "poly (mulexp n [- a, 1] q) \<noteq> poly ([- a, 1] %^ Suc n *** qa)")
apply simp
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Fri Oct 19 15:12:52 2012 +0200
@@ -304,7 +304,7 @@
qed auto
lemma polyadd[simp]: "Ipoly bs (polyadd p q) = Ipoly bs p + Ipoly bs q"
-by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps right_distrib[symmetric] simp del: right_distrib)
+by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left)
lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd p q)"
using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
--- a/src/HOL/Divides.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Divides.thy Fri Oct 19 15:12:52 2012 +0200
@@ -66,7 +66,7 @@
"\<dots> = (c + a div b) * b + (a + c * b) mod b"
by (simp add: algebra_simps)
finally have "a = a div b * b + (a + c * b) mod b"
- by (simp add: add_commute [of a] add_assoc left_distrib)
+ by (simp add: add_commute [of a] add_assoc distrib_right)
then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
by (simp add: mod_div_equality)
then show ?thesis by simp
@@ -1274,9 +1274,9 @@
prefer 2 apply (simp add: right_diff_distrib)
apply (subgoal_tac "0 < b * (1 + q - q') ")
apply (erule_tac [2] order_le_less_trans)
- prefer 2 apply (simp add: right_diff_distrib right_distrib)
+ prefer 2 apply (simp add: right_diff_distrib distrib_left)
apply (subgoal_tac "b * q' < b * (1 + q) ")
- prefer 2 apply (simp add: right_diff_distrib right_distrib)
+ prefer 2 apply (simp add: right_diff_distrib distrib_left)
apply (simp add: mult_less_cancel_left)
done
@@ -1332,11 +1332,11 @@
apply (induct a b rule: posDivAlg.induct)
apply auto
apply (simp add: divmod_int_rel_def)
- apply (subst posDivAlg_eqn, simp add: right_distrib)
+ apply (subst posDivAlg_eqn, simp add: distrib_left)
apply (case_tac "a < b")
apply simp_all
apply (erule splitE)
- apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
+ apply (auto simp add: distrib_left Let_def mult_ac mult_2_right)
done
@@ -1366,7 +1366,7 @@
apply (case_tac "a + b < (0\<Colon>int)")
apply simp_all
apply (erule splitE)
- apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
+ apply (auto simp add: distrib_left Let_def mult_ac mult_2_right)
done
@@ -1732,7 +1732,7 @@
"[| 0 \<le> b'*q' + r'; r' < b'; 0 < b' |] ==> 0 \<le> (q'::int)"
apply (subgoal_tac "0 < b'* (q' + 1) ")
apply (simp add: zero_less_mult_iff)
-apply (simp add: right_distrib)
+apply (simp add: distrib_left)
done
lemma zdiv_mono2_lemma:
@@ -1744,7 +1744,7 @@
apply (simp add: mult_less_cancel_left)
apply (subgoal_tac "b*q = r' - r + b'*q'")
prefer 2 apply simp
-apply (simp (no_asm_simp) add: right_distrib)
+apply (simp (no_asm_simp) add: distrib_left)
apply (subst add_commute, rule add_less_le_mono, arith)
apply (rule mult_right_mono, auto)
done
@@ -1773,7 +1773,7 @@
apply (frule q_neg_lemma, assumption+)
apply (subgoal_tac "b*q' < b* (q + 1) ")
apply (simp add: mult_less_cancel_left)
-apply (simp add: right_distrib)
+apply (simp add: distrib_left)
apply (subgoal_tac "b*q' \<le> b'*q'")
prefer 2 apply (simp add: mult_right_mono_neg, arith)
done
@@ -1795,7 +1795,7 @@
lemma zmult1_lemma:
"[| divmod_int_rel b c (q, r) |]
==> divmod_int_rel (a * b) c (a*q + a*r div c, a*r mod c)"
-by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_distrib mult_ac)
+by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left mult_ac)
lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
apply (case_tac "c = 0", simp)
@@ -1807,7 +1807,7 @@
lemma zadd1_lemma:
"[| divmod_int_rel a c (aq, ar); divmod_int_rel b c (bq, br) |]
==> divmod_int_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
-by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_distrib)
+by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left)
(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
lemma zdiv_zadd1_eq:
@@ -1900,7 +1900,7 @@
lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); 0 < c |]
==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
by (auto simp add: mult_ac divmod_int_rel_def linorder_neq_iff
- zero_less_mult_iff right_distrib [symmetric]
+ zero_less_mult_iff distrib_left [symmetric]
zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm)
lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"
--- a/src/HOL/GCD.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/GCD.thy Fri Oct 19 15:12:52 2012 +0200
@@ -1199,7 +1199,7 @@
from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
by simp
hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
- by (simp only: mult_assoc right_distrib)
+ by (simp only: mult_assoc distrib_left)
hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
by algebra
hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy Fri Oct 19 15:12:52 2012 +0200
@@ -411,7 +411,7 @@
from x y have "\<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>" ..
with a have " \<parallel>f\<parallel>\<hyphen>F * \<parallel>x + y\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>F * (\<parallel>x\<parallel> + \<parallel>y\<parallel>)"
by (simp add: mult_left_mono)
- also have "\<dots> = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel> + \<parallel>f\<parallel>\<hyphen>F * \<parallel>y\<parallel>" by (simp only: right_distrib)
+ also have "\<dots> = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel> + \<parallel>f\<parallel>\<hyphen>F * \<parallel>y\<parallel>" by (simp only: distrib_left)
also have "\<dots> = p x + p y" by (simp only: p_def)
finally show ?thesis .
qed
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy Fri Oct 19 15:12:52 2012 +0200
@@ -140,7 +140,7 @@
also from y1 y2 have "h (y1 + y2) = h y1 + h y2"
by simp
also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
- by (simp add: left_distrib)
+ by (simp add: distrib_right)
also from h'_def x1_rep E HE y1 x0
have "h y1 + a1 * xi = h' x1"
by (rule h'_definite [symmetric])
@@ -179,7 +179,7 @@
also from y1 have "h (c \<cdot> y1) = c * h y1"
by simp
also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"
- by (simp only: right_distrib)
+ by (simp only: distrib_left)
also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1"
by (rule h'_definite [symmetric])
finally show ?thesis .
--- a/src/HOL/Int.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Int.thy Fri Oct 19 15:12:52 2012 +0200
@@ -136,7 +136,7 @@
"(i::int)<j ==> 0<k ==> int k * i < int k * j"
apply (induct k)
apply simp
-apply (simp add: left_distrib)
+apply (simp add: distrib_right)
apply (case_tac "k=0")
apply (simp_all add: add_strict_mono)
done
@@ -193,8 +193,8 @@
done
lemmas int_distrib =
- left_distrib [of z1 z2 w]
- right_distrib [of w z1 z2]
+ distrib_right [of z1 z2 w]
+ distrib_left [of w z1 z2]
left_diff_distrib [of z1 z2 w]
right_diff_distrib [of w z1 z2]
for z1 z2 w :: int
@@ -499,7 +499,7 @@
lemma even_less_0_iff:
"a + a < 0 \<longleftrightarrow> a < (0::'a::linordered_idom)"
proof -
- have "a + a < 0 \<longleftrightarrow> (1+1)*a < 0" by (simp add: left_distrib del: one_add_one)
+ have "a + a < 0 \<longleftrightarrow> (1+1)*a < 0" by (simp add: distrib_right del: one_add_one)
also have "(1+1)*a < 0 \<longleftrightarrow> a < 0"
by (simp add: mult_less_0_iff zero_less_two
order_less_not_sym [OF zero_less_two])
@@ -1097,8 +1097,8 @@
text{*These distributive laws move literals inside sums and differences.*}
-lemmas left_distrib_numeral [simp] = left_distrib [of _ _ "numeral v"] for v
-lemmas right_distrib_numeral [simp] = right_distrib [of "numeral v"] for v
+lemmas distrib_right_numeral [simp] = distrib_right [of _ _ "numeral v"] for v
+lemmas distrib_left_numeral [simp] = distrib_left [of "numeral v"] for v
lemmas left_diff_distrib_numeral [simp] = left_diff_distrib [of _ _ "numeral v"] for v
lemmas right_diff_distrib_numeral [simp] = right_diff_distrib [of "numeral v"] for v
--- a/src/HOL/Library/Extended_Nat.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Library/Extended_Nat.thy Fri Oct 19 15:12:52 2012 +0200
@@ -196,7 +196,7 @@
by (simp split: enat.split)
show "(a + b) * c = a * c + b * c"
unfolding times_enat_def zero_enat_def
- by (simp split: enat.split add: left_distrib)
+ by (simp split: enat.split add: distrib_right)
show "0 * a = 0"
unfolding times_enat_def zero_enat_def
by (simp split: enat.split)
--- a/src/HOL/Library/Formal_Power_Series.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Fri Oct 19 15:12:52 2012 +0200
@@ -260,11 +260,11 @@
proof
fix a b c :: "'a fps"
show "(a + b) * c = a * c + b * c"
- by (simp add: expand_fps_eq fps_mult_nth left_distrib setsum_addf)
+ by (simp add: expand_fps_eq fps_mult_nth distrib_right setsum_addf)
next
fix a b c :: "'a fps"
show "a * (b + c) = a * b + a * c"
- by (simp add: expand_fps_eq fps_mult_nth right_distrib setsum_addf)
+ by (simp add: expand_fps_eq fps_mult_nth distrib_left setsum_addf)
qed
instance fps :: (semiring_0) semiring_0
@@ -363,10 +363,10 @@
instance fps :: (ring) ring ..
instance fps :: (ring_1) ring_1
- by (intro_classes, auto simp add: diff_minus left_distrib)
+ by (intro_classes, auto simp add: diff_minus distrib_right)
instance fps :: (comm_ring_1) comm_ring_1
- by (intro_classes, auto simp add: diff_minus left_distrib)
+ by (intro_classes, auto simp add: diff_minus distrib_right)
instance fps :: (ring_no_zero_divisors) ring_no_zero_divisors
proof
@@ -3200,7 +3200,7 @@
show ?thesis
using fps_sin_cos_sum_of_squares[of c]
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)
- unfolding right_distrib[symmetric]
+ unfolding distrib_left[symmetric]
by simp
qed
--- a/src/HOL/Library/FrechetDeriv.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Library/FrechetDeriv.thy Fri Oct 19 15:12:52 2012 +0200
@@ -55,7 +55,7 @@
apply (rule f.pos_bounded [THEN exE], rename_tac Kf)
apply (rule g.pos_bounded [THEN exE], rename_tac Kg)
apply (rule_tac x="Kf + Kg" in exI, safe)
- apply (subst right_distrib)
+ apply (subst distrib_left)
apply (rule order_trans [OF norm_triangle_ineq])
apply (rule add_mono, erule spec, erule spec)
done
@@ -413,8 +413,8 @@
apply (induct n)
apply (simp add: FDERIV_ident)
apply (drule FDERIV_mult [OF FDERIV_ident])
- apply (simp only: of_nat_Suc left_distrib mult_1_left)
- apply (simp only: power_Suc right_distrib add_ac mult_ac)
+ apply (simp only: of_nat_Suc distrib_right mult_1_left)
+ apply (simp only: power_Suc distrib_left add_ac mult_ac)
done
lemma FDERIV_power:
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Fri Oct 19 15:12:52 2012 +0200
@@ -238,7 +238,7 @@
have th4: "cmod (complex_of_real (cmod b) / b) *
cmod (1 + b * (v ^ n / complex_of_real (cmod b)))
< cmod (complex_of_real (cmod b) / b) * 1"
- apply (simp only: norm_mult[symmetric] right_distrib)
+ apply (simp only: norm_mult[symmetric] distrib_left)
using b v by (simp add: th2)
from mult_less_imp_less_left[OF th4 th3]
--- a/src/HOL/Library/Inner_Product.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Library/Inner_Product.thy Fri Oct 19 15:12:52 2012 +0200
@@ -201,7 +201,7 @@
show "inner x y = inner y x"
unfolding inner_real_def by (rule mult_commute)
show "inner (x + y) z = inner x z + inner y z"
- unfolding inner_real_def by (rule left_distrib)
+ unfolding inner_real_def by (rule distrib_right)
show "inner (scaleR r x) y = r * inner x y"
unfolding inner_real_def real_scaleR_def by (rule mult_assoc)
show "0 \<le> inner x x"
@@ -225,9 +225,9 @@
show "inner x y = inner y x"
unfolding inner_complex_def by (simp add: mult_commute)
show "inner (x + y) z = inner x z + inner y z"
- unfolding inner_complex_def by (simp add: left_distrib)
+ unfolding inner_complex_def by (simp add: distrib_right)
show "inner (scaleR r x) y = r * inner x y"
- unfolding inner_complex_def by (simp add: right_distrib)
+ unfolding inner_complex_def by (simp add: distrib_left)
show "0 \<le> inner x x"
unfolding inner_complex_def by simp
show "inner x x = 0 \<longleftrightarrow> x = 0"
--- a/src/HOL/Library/Kleene_Algebra.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Library/Kleene_Algebra.thy Fri Oct 19 15:12:52 2012 +0200
@@ -141,13 +141,13 @@
show "c * a \<le> c * b"
proof (rule ord_intro)
from `a \<le> b` have "c * (a + b) = c * b" by simp
- thus "c * a + c * b = c * b" by (simp add: right_distrib)
+ thus "c * a + c * b = c * b" by (simp add: distrib_left)
qed
show "a * c \<le> b * c"
proof (rule ord_intro)
from `a \<le> b` have "(a + b) * c = b * c" by simp
- thus "a * c + b * c = b * c" by (simp add: left_distrib)
+ thus "a * c + b * c = b * c" by (simp add: distrib_right)
qed
qed
@@ -206,7 +206,7 @@
by (metis less_add(2) star_unfold_left)
lemma star_mult_idem [simp]: "star x * star x = star x"
-by (metis add_commute add_est1 eq_iff mult_1_right right_distrib star3 star_unfold_left)
+by (metis add_commute add_est1 eq_iff mult_1_right distrib_left star3 star_unfold_left)
lemma less_star [simp]: "x \<le> star x"
by (metis less_add(2) mult_1_right mult_left_mono one_less_star order_trans star_unfold_left zero_minimum)
@@ -232,7 +232,7 @@
thus "x + star b * x * a \<le> x + star b * b * x"
using add_mono by auto
show "\<dots> \<le> star b * x"
- by (metis add_supremum left_distrib less_add mult.left_neutral mult_assoc mult_right_mono star_unfold_right zero_minimum)
+ by (metis add_supremum distrib_right less_add mult.left_neutral mult_assoc mult_right_mono star_unfold_right zero_minimum)
qed
lemma star_simulation [simp]:
@@ -273,10 +273,10 @@
by (metis add_commute ord_simp star_idemp star_mono star_mult_idem star_one star_unfold_left)
lemma star_unfold2: "star x * y = y + x * star x * y"
-by (subst star_unfold_right[symmetric]) (simp add: mult_assoc left_distrib)
+by (subst star_unfold_right[symmetric]) (simp add: mult_assoc distrib_right)
lemma star_absorb_one [simp]: "star (x + 1) = star x"
-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)
+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)
lemma star_absorb_one' [simp]: "star (1 + x) = star x"
by (subst add_commute) (fact star_absorb_one)
@@ -292,13 +292,13 @@
lemma ka18: "(x * star x) * star (y * star x) + (y * star x) * star (y * star x)
\<le> star x * star (y * star x)"
-by (metis ka16 ka17 left_distrib mult_assoc plus_leI)
+by (metis ka16 ka17 distrib_right mult_assoc plus_leI)
lemma star_decomp: "star (x + y) = star x * star (y * star x)"
proof (rule antisym)
have "1 + (x + y) * star x * star (y * star x) \<le>
1 + x * star x * star (y * star x) + y * star x * star (y * star x)"
- by (metis add_commute add_left_commute eq_iff left_distrib mult_assoc)
+ by (metis add_commute add_left_commute eq_iff distrib_right mult_assoc)
also have "\<dots> \<le> star x * star (y * star x)"
by (metis add_commute add_est1 add_left_commute ka18 plus_leI star_unfold_left x_less_star)
finally show "star (x + y) \<le> star x * star (y * star x)"
@@ -342,7 +342,7 @@
by (metis add_commute ka27)
lemma ka29: "(y * (1 + x) \<le> (1 + x) * star y) = (y * x \<le> (1 + x) * star y)"
-by (metis add_supremum left_distrib less_add(1) less_star mult.left_neutral mult.right_neutral order_trans right_distrib)
+by (metis add_supremum distrib_right less_add(1) less_star mult.left_neutral mult.right_neutral order_trans distrib_left)
lemma ka30: "star x * star y \<le> star (x + y)"
by (metis mult_left_mono star_decomp star_mono x_less_star zero_minimum)
--- a/src/HOL/Library/ListVector.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Library/ListVector.thy Fri Oct 19 15:12:52 2012 +0200
@@ -128,7 +128,7 @@
apply simp
apply(case_tac zs)
apply (simp)
-apply(simp add: left_distrib)
+apply(simp add: distrib_right)
done
lemma iprod_left_diff_distrib: "\<langle>xs - ys, zs\<rangle> = \<langle>xs,zs\<rangle> - \<langle>ys,zs\<rangle>"
@@ -146,7 +146,7 @@
apply simp
apply(case_tac ys)
apply (simp)
-apply (simp add: right_distrib mult_assoc)
+apply (simp add: distrib_left mult_assoc)
done
end
--- a/src/HOL/Library/Polynomial.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Library/Polynomial.thy Fri Oct 19 15:12:52 2012 +0200
@@ -975,7 +975,7 @@
assume "y \<noteq> 0"
hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
using pdivmod_rel [of x y]
- by (simp add: pdivmod_rel_def left_distrib)
+ by (simp add: pdivmod_rel_def distrib_right)
thus "(x + z * y) div y = z + x div y"
by (rule div_poly_eq)
next
--- a/src/HOL/Library/Product_Vector.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Library/Product_Vector.thy Fri Oct 19 15:12:52 2012 +0200
@@ -421,7 +421,7 @@
show "norm (scaleR r x) = \<bar>r\<bar> * norm x"
unfolding norm_prod_def
apply (simp add: power_mult_distrib)
- apply (simp add: right_distrib [symmetric])
+ apply (simp add: distrib_left [symmetric])
apply (simp add: real_sqrt_mult_distrib)
done
show "sgn x = scaleR (inverse (norm x)) x"
@@ -475,7 +475,7 @@
apply (rule allI)
apply (simp add: norm_Pair)
apply (rule order_trans [OF sqrt_add_le_add_sqrt], simp, simp)
- apply (simp add: right_distrib)
+ apply (simp add: distrib_left)
apply (rule add_mono [OF norm_f norm_g])
done
then show "\<exists>K. \<forall>x. norm (f x, g x) \<le> norm x * K" ..
@@ -528,7 +528,7 @@
by (simp add: inner_add_left)
show "inner (scaleR r x) y = r * inner x y"
unfolding inner_prod_def
- by (simp add: right_distrib)
+ by (simp add: distrib_left)
show "0 \<le> inner x x"
unfolding inner_prod_def
by (intro add_nonneg_nonneg inner_ge_zero)
--- a/src/HOL/Library/Univ_Poly.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Library/Univ_Poly.thy Fri Oct 19 15:12:52 2012 +0200
@@ -125,7 +125,7 @@
lemma (in semiring_0) poly_cmult_distr: "a %* ( p +++ q) = (a %* p +++ a %* q)"
apply (induct p arbitrary: q, simp)
-apply (case_tac q, simp_all add: right_distrib)
+apply (case_tac q, simp_all add: distrib_left)
done
lemma (in ring_1) pmult_by_x[simp]: "[0, 1] *** t = ((0)#t)"
@@ -141,17 +141,17 @@
case Nil thus ?case by simp
next
case (Cons a as p2) thus ?case
- by (cases p2, simp_all add: add_ac right_distrib)
+ by (cases p2, simp_all add: add_ac distrib_left)
qed
lemma (in comm_semiring_0) poly_cmult: "poly (c %* p) x = c * poly p x"
apply (induct "p")
apply (case_tac [2] "x=zero")
-apply (auto simp add: right_distrib mult_ac)
+apply (auto simp add: distrib_left mult_ac)
done
lemma (in comm_semiring_0) poly_cmult_map: "poly (map (op * c) p) x = c*poly p x"
- by (induct p, auto simp add: right_distrib mult_ac)
+ by (induct p, auto simp add: distrib_left mult_ac)
lemma (in comm_ring_1) poly_minus: "poly (-- p) x = - (poly p x)"
apply (simp add: poly_minus_def)
@@ -164,7 +164,7 @@
next
case (Cons a as p2)
thus ?case by (cases as,
- simp_all add: poly_cmult poly_add left_distrib right_distrib mult_ac)
+ simp_all add: poly_cmult poly_add distrib_right distrib_left mult_ac)
qed
class idom_char_0 = idom + ring_char_0
@@ -394,7 +394,7 @@
by (auto simp add: algebra_simps poly_add poly_minus_def fun_eq poly_cmult minus_mult_left[symmetric])
lemma (in comm_ring_1) poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))"
-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])
+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])
subclass (in idom_char_0) comm_ring_1 ..
lemma (in idom_char_0) poly_mult_left_cancel: "(poly (p *** q) = poly (p *** r)) = (poly p = poly [] | poly q = poly r)"
@@ -458,9 +458,9 @@
text{*Basics of divisibility.*}
lemma (in idom) poly_primes: "([a, 1] divides (p *** q)) = ([a, 1] divides p | [a, 1] divides q)"
-apply (auto simp add: divides_def fun_eq poly_mult poly_add poly_cmult left_distrib [symmetric])
+apply (auto simp add: divides_def fun_eq poly_mult poly_add poly_cmult distrib_right [symmetric])
apply (drule_tac x = "uminus a" in spec)
-apply (simp add: poly_linear_divides poly_add poly_cmult left_distrib [symmetric])
+apply (simp add: poly_linear_divides poly_add poly_cmult distrib_right [symmetric])
apply (cases "p = []")
apply (rule exI[where x="[]"])
apply simp
@@ -471,10 +471,10 @@
apply (cases "\<exists>q\<Colon>'a list. p = a %* q +++ ((0\<Colon>'a) # q)")
apply (clarsimp simp add: poly_add poly_cmult)
apply (rule_tac x="qa" in exI)
-apply (simp add: left_distrib [symmetric])
+apply (simp add: distrib_right [symmetric])
apply clarsimp
-apply (auto simp add: right_minus poly_linear_divides poly_add poly_cmult left_distrib [symmetric])
+apply (auto simp add: right_minus poly_linear_divides poly_add poly_cmult distrib_right [symmetric])
apply (rule_tac x = "pmult qa q" in exI)
apply (rule_tac [2] x = "pmult p qa" in exI)
apply (auto simp add: poly_add poly_mult poly_cmult mult_ac)
@@ -509,7 +509,7 @@
"[| p divides q; p divides r |] ==> p divides (q +++ r)"
apply (simp add: divides_def, auto)
apply (rule_tac x = "padd qa qaa" in exI)
-apply (auto simp add: poly_add fun_eq poly_mult right_distrib)
+apply (auto simp add: poly_add fun_eq poly_mult distrib_left)
done
lemma (in comm_ring_1) poly_divides_diff:
@@ -605,7 +605,7 @@
apply (unfold divides_def)
apply (rule_tac x = q in exI)
apply (induct_tac "n", simp)
-apply (simp (no_asm_simp) add: poly_add poly_cmult poly_mult right_distrib mult_ac)
+apply (simp (no_asm_simp) add: poly_add poly_cmult poly_mult distrib_left mult_ac)
apply safe
apply (subgoal_tac "?poly (?mulexp n [uminus a, one] q) \<noteq> ?poly (pmult (?pexp [uminus a, one] (Suc n)) qa)")
apply simp
@@ -948,7 +948,7 @@
case (Suc n a p)
have eq: "poly ([a,1] %^(Suc n) *** p) = poly ([a,1] %^ n *** ([a,1] *** p))"
apply (rule ext, simp add: poly_mult poly_add poly_cmult)
- by (simp add: mult_ac add_ac right_distrib)
+ by (simp add: mult_ac add_ac distrib_left)
note deq = degree_unique[OF eq]
{assume p: "poly p = poly []"
with eq have eq': "poly ([a,1] %^(Suc n) *** p) = poly []"
--- a/src/HOL/List.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/List.thy Fri Oct 19 15:12:52 2012 +0200
@@ -3166,11 +3166,11 @@
lemma (in monoid_add) listsum_triv:
"(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
- by (induct xs) (simp_all add: left_distrib)
+ by (induct xs) (simp_all add: distrib_right)
lemma (in monoid_add) listsum_0 [simp]:
"(\<Sum>x\<leftarrow>xs. 0) = 0"
- by (induct xs) (simp_all add: left_distrib)
+ by (induct xs) (simp_all add: distrib_right)
text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
lemma (in ab_group_add) uminus_listsum_map:
--- a/src/HOL/Log.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Log.thy Fri Oct 19 15:12:52 2012 +0200
@@ -34,7 +34,7 @@
lemma powr_mult:
"[| 0 < x; 0 < y |] ==> (x * y) powr a = (x powr a) * (y powr a)"
-by (simp add: powr_def exp_add [symmetric] ln_mult right_distrib)
+by (simp add: powr_def exp_add [symmetric] ln_mult distrib_left)
lemma powr_gt_zero [simp]: "0 < x powr a"
by (simp add: powr_def)
@@ -58,7 +58,7 @@
done
lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
-by (simp add: powr_def exp_add [symmetric] left_distrib)
+by (simp add: powr_def exp_add [symmetric] distrib_right)
lemma powr_mult_base:
"0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
@@ -112,7 +112,7 @@
lemma log_mult:
"[| 0 < a; a \<noteq> 1; 0 < x; 0 < y |]
==> log a (x * y) = log a x + log a y"
-by (simp add: log_def ln_mult divide_inverse left_distrib)
+by (simp add: log_def ln_mult divide_inverse distrib_right)
lemma log_eq_div_ln_mult_log:
"[| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]
--- a/src/HOL/MacLaurin.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/MacLaurin.thy Fri Oct 19 15:12:52 2012 +0200
@@ -415,7 +415,7 @@
lemma sin_expansion_lemma:
"sin (x + real (Suc m) * pi / 2) =
cos (x + real (m) * pi / 2)"
-by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
+by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib distrib_right, auto)
lemma Maclaurin_sin_expansion2:
"\<exists>t. abs t \<le> abs x &
@@ -489,7 +489,7 @@
lemma cos_expansion_lemma:
"cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)"
-by (simp only: cos_add sin_add real_of_nat_Suc left_distrib add_divide_distrib, auto)
+by (simp only: cos_add sin_add real_of_nat_Suc distrib_right add_divide_distrib, auto)
lemma Maclaurin_cos_expansion:
"\<exists>t. abs t \<le> abs x &
--- a/src/HOL/Metis_Examples/Binary_Tree.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Metis_Examples/Binary_Tree.thy Fri Oct 19 15:12:52 2012 +0200
@@ -223,7 +223,7 @@
apply (induct t1)
apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1)
Suc_eq_plus1)
-by (simp add: left_distrib)
+by (simp add: distrib_right)
lemma (*bt_map_append:*)
"bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)"
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Oct 19 15:12:52 2012 +0200
@@ -1068,7 +1068,7 @@
x: "setsum (\<lambda>i. (x$i) *s column i A) ?U = y2" by blast
let ?x = "(\<chi> j. if j = i then c + (x$i) else (x$j))::real^'m"
show "?P (c*s y1 + y2)"
- 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)
+ 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)
fix j
have th: "\<forall>xa \<in> ?U. (if xa = i then (c + (x$i)) * ((column xa A)$j)
else (x$xa) * ((column xa A$j))) = (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))"
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Oct 19 15:12:52 2012 +0200
@@ -1450,7 +1450,7 @@
have u2:"u2 \<le> 1" unfolding obt2(3)[symmetric] and not_le using obt2(2) by auto
have "u1 * u + u2 * v \<le> (max u1 u2) * u + (max u1 u2) * v" apply(rule add_mono)
apply(rule_tac [!] mult_right_mono) using as(1,2) obt1(1,2) obt2(1,2) by auto
- also have "\<dots> \<le> 1" unfolding right_distrib[symmetric] and as(3) using u1 u2 by auto
+ also have "\<dots> \<le> 1" unfolding distrib_left[symmetric] and as(3) using u1 u2 by auto
finally
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)
apply(rule conjI) defer apply(rule_tac x="1 - u * u1 - v * u2" in exI) unfolding Bex_def
--- a/src/HOL/Multivariate_Analysis/L2_Norm.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/L2_Norm.thy Fri Oct 19 15:12:52 2012 +0200
@@ -165,7 +165,7 @@
apply (simp add: mult_nonneg_nonneg setsum_nonneg)
apply (simp add: power2_sum)
apply (simp add: power_mult_distrib)
- apply (simp add: right_distrib left_distrib)
+ apply (simp add: distrib_left distrib_right)
apply (rule ord_le_eq_trans)
apply (rule setL2_mult_ineq_lemma)
apply simp
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Oct 19 15:12:52 2012 +0200
@@ -1456,7 +1456,7 @@
by (auto simp add: norm_minus_commute)
also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
- unfolding left_distrib using `x\<noteq>y`[unfolded dist_nz, unfolded dist_norm] by auto
+ unfolding distrib_right using `x\<noteq>y`[unfolded dist_nz, unfolded dist_norm] by auto
also have "\<dots> \<le> e - d/2" using `d \<le> dist x y` and `d>0` and `?rhs` by(auto simp add: dist_norm)
finally have "y - (d / (2 * dist y x)) *\<^sub>R (y - x) \<in> ball x e" using `d>0` by auto
@@ -1583,7 +1583,7 @@
by (auto simp add: algebra_simps)
also have "\<dots> = \<bar>1 + d / (2 * norm (y - x))\<bar> * norm (y - x)"
using ** by auto
- also have "\<dots> = (dist y x) + d/2"using ** by (auto simp add: left_distrib dist_norm)
+ also have "\<dots> = (dist y x) + d/2"using ** by (auto simp add: distrib_right dist_norm)
finally have "e \<ge> dist x y +d/2" using *[unfolded mem_cball] by (auto simp add: dist_commute)
thus "y \<in> ball x e" unfolding mem_ball using `d>0` by auto
qed }
--- a/src/HOL/NSA/CLim.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/NSA/CLim.thy Fri Oct 19 15:12:52 2012 +0200
@@ -140,7 +140,7 @@
"DERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))"
apply (induct n)
apply (drule_tac [2] DERIV_ident [THEN DERIV_mult])
-apply (auto simp add: left_distrib real_of_nat_Suc)
+apply (auto simp add: distrib_right real_of_nat_Suc)
apply (case_tac "n")
apply (auto simp add: mult_ac add_commute)
done
--- a/src/HOL/NSA/HDeriv.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/NSA/HDeriv.thy Fri Oct 19 15:12:52 2012 +0200
@@ -209,7 +209,7 @@
apply (drule_tac
approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]])
apply (auto intro!: approx_add_mono1
- simp add: left_distrib right_distrib mult_commute add_assoc)
+ simp add: distrib_right distrib_left mult_commute add_assoc)
apply (rule_tac b1 = "star_of Db * star_of (f x)"
in add_commute [THEN subst])
apply (auto intro!: Infinitesimal_add_approx_self2 [THEN approx_sym]
@@ -357,7 +357,7 @@
del: inverse_mult_distrib inverse_minus_eq
minus_mult_left [symmetric] minus_mult_right [symmetric])
apply (subst mult_commute, simp add: nonzero_mult_divide_cancel_right)
-apply (simp (no_asm_simp) add: mult_assoc [symmetric] left_distrib
+apply (simp (no_asm_simp) add: mult_assoc [symmetric] distrib_right
del: minus_mult_left [symmetric] minus_mult_right [symmetric])
apply (rule_tac y = "inverse (- (star_of x * star_of x))" in approx_trans)
apply (rule inverse_add_Infinitesimal_approx2)
@@ -451,7 +451,7 @@
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)
apply assumption
apply (simp add: times_divide_eq_right [symmetric])
-apply (auto simp add: left_distrib)
+apply (auto simp add: distrib_right)
done
lemma increment_thm2:
@@ -464,7 +464,7 @@
lemma increment_approx_zero: "[| NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 |]
==> increment f x h \<approx> 0"
apply (drule increment_thm2,
- auto intro!: Infinitesimal_HFinite_mult2 HFinite_add simp add: left_distrib [symmetric] mem_infmal_iff [symmetric])
+ auto intro!: Infinitesimal_HFinite_mult2 HFinite_add simp add: distrib_right [symmetric] mem_infmal_iff [symmetric])
apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
done
--- a/src/HOL/NSA/HyperDef.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/NSA/HyperDef.thy Fri Oct 19 15:12:52 2012 +0200
@@ -404,7 +404,7 @@
lemma two_hrealpow_gt [simp]: "hypreal_of_nat n < 2 ^ n"
apply (induct n)
-apply (auto simp add: left_distrib)
+apply (auto simp add: distrib_right)
apply (cut_tac n = n in two_hrealpow_ge_one, arith)
done
@@ -417,7 +417,7 @@
lemma hrealpow_sum_square_expand:
"(x + (y::hypreal)) ^ Suc (Suc 0) =
x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0)))*x*y"
-by (simp add: right_distrib left_distrib)
+by (simp add: distrib_left distrib_right)
lemma power_hypreal_of_real_numeral:
"(numeral v :: hypreal) ^ n = hypreal_of_real ((numeral v) ^ n)"
--- a/src/HOL/NSA/NSComplex.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/NSA/NSComplex.thy Fri Oct 19 15:12:52 2012 +0200
@@ -547,7 +547,7 @@
"!!a. hcis (hypreal_of_nat (Suc n) * a) =
hcis a * hcis (hypreal_of_nat n * a)"
apply transfer
-apply (simp add: left_distrib cis_mult)
+apply (simp add: distrib_right cis_mult)
done
lemma NSDeMoivre: "!!a. (hcis a) ^ n = hcis (hypreal_of_nat n * a)"
@@ -559,7 +559,7 @@
lemma hcis_hypreal_of_hypnat_Suc_mult:
"!! a n. hcis (hypreal_of_hypnat (n + 1) * a) =
hcis a * hcis (hypreal_of_hypnat n * a)"
-by transfer (simp add: left_distrib cis_mult)
+by transfer (simp add: distrib_right cis_mult)
lemma NSDeMoivre_ext:
"!!a n. (hcis a) pow n = hcis (hypreal_of_hypnat n * a)"
--- a/src/HOL/NSA/StarDef.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/NSA/StarDef.thy Fri Oct 19 15:12:52 2012 +0200
@@ -828,8 +828,8 @@
instance star :: (semiring) semiring
apply (intro_classes)
-apply (transfer, rule left_distrib)
-apply (transfer, rule right_distrib)
+apply (transfer, rule distrib_right)
+apply (transfer, rule distrib_left)
done
instance star :: (semiring_0) semiring_0
@@ -838,7 +838,7 @@
instance star :: (semiring_0_cancel) semiring_0_cancel ..
instance star :: (comm_semiring) comm_semiring
-by (intro_classes, transfer, rule left_distrib)
+by (intro_classes, transfer, rule distrib_right)
instance star :: (comm_semiring_0) comm_semiring_0 ..
instance star :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..
--- a/src/HOL/Nat.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Nat.thy Fri Oct 19 15:12:52 2012 +0200
@@ -312,7 +312,7 @@
by (rule mult_commute)
lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
- by (rule right_distrib)
+ by (rule distrib_left)
lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
by (induct m) auto
@@ -1342,7 +1342,7 @@
by (induct m) (simp_all add: add_ac)
lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
- by (induct m) (simp_all add: add_ac left_distrib)
+ by (induct m) (simp_all add: add_ac distrib_right)
primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
"of_nat_aux inc 0 i = i"
--- a/src/HOL/NthRoot.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/NthRoot.thy Fri Oct 19 15:12:52 2012 +0200
@@ -598,7 +598,7 @@
"sqrt ((a + c)\<twosuperior> + (b + d)\<twosuperior>) \<le> sqrt (a\<twosuperior> + b\<twosuperior>) + sqrt (c\<twosuperior> + d\<twosuperior>)"
apply (rule power2_le_imp_le, simp)
apply (simp add: power2_sum)
-apply (simp only: mult_assoc right_distrib [symmetric])
+apply (simp only: mult_assoc distrib_left [symmetric])
apply (rule mult_left_mono)
apply (rule power2_le_imp_le)
apply (simp add: power2_sum power_mult_distrib)
--- a/src/HOL/Num.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Num.thy Fri Oct 19 15:12:52 2012 +0200
@@ -138,7 +138,7 @@
"Bit1 m * Bit0 n = Bit0 (Bit1 m * n)"
"Bit1 m * Bit1 n = Bit1 (m + n + Bit0 (m * n))"
by (simp_all add: num_eq_iff nat_of_num_add
- nat_of_num_mult left_distrib right_distrib)
+ nat_of_num_mult distrib_right distrib_left)
lemma eq_num_simps:
"One = One \<longleftrightarrow> True"
@@ -510,7 +510,7 @@
lemma numeral_mult: "numeral (m * n) = numeral m * numeral n"
apply (induct n rule: num_induct)
apply (simp add: numeral_One)
- apply (simp add: mult_inc numeral_inc numeral_add right_distrib)
+ apply (simp add: mult_inc numeral_inc numeral_add distrib_left)
done
lemma numeral_times_numeral: "numeral m * numeral n = numeral (m * n)"
@@ -532,10 +532,10 @@
simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1)
lemma mult_2: "2 * z = z + z"
- unfolding one_add_one [symmetric] left_distrib by simp
+ unfolding one_add_one [symmetric] distrib_right by simp
lemma mult_2_right: "z * 2 = z + z"
- unfolding one_add_one [symmetric] right_distrib by simp
+ unfolding one_add_one [symmetric] distrib_left by simp
end
--- a/src/HOL/Number_Theory/Binomial.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Number_Theory/Binomial.thy Fri Oct 19 15:12:52 2012 +0200
@@ -205,7 +205,7 @@
also note two
also with less have "(n - k) * fact n + (k + 1) * fact n= fact (n + 1)"
apply (subst fact_plus_one_nat)
- apply (subst left_distrib [symmetric])
+ apply (subst distrib_right [symmetric])
apply simp
done
finally show "fact (k + 1) * fact (n - k) * (n + 1 choose (k + 1)) =
--- a/src/HOL/Old_Number_Theory/EvenOdd.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Old_Number_Theory/EvenOdd.thy Fri Oct 19 15:12:52 2012 +0200
@@ -85,7 +85,7 @@
lemma even_plus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x + y \<in> zEven"
apply (auto simp add: zEven_def)
- apply (auto simp only: right_distrib [symmetric])
+ apply (auto simp only: distrib_left [symmetric])
done
lemma even_times_either: "x \<in> zEven ==> x * y \<in> zEven"
@@ -113,9 +113,9 @@
done
lemma odd_times_odd: "[| x \<in> zOdd; y \<in> zOdd |] ==> x * y \<in> zOdd"
- apply (auto simp add: zOdd_def left_distrib right_distrib)
+ apply (auto simp add: zOdd_def distrib_right distrib_left)
apply (rule_tac x = "2 * ka * k + ka + k" in exI)
- apply (auto simp add: left_distrib)
+ apply (auto simp add: distrib_right)
done
lemma odd_iff_not_even: "(x \<in> zOdd) = (~ (x \<in> zEven))"
--- a/src/HOL/Old_Number_Theory/Finite2.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Old_Number_Theory/Finite2.thy Fri Oct 19 15:12:52 2012 +0200
@@ -38,18 +38,18 @@
lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)"
apply (induct set: finite)
- apply (auto simp add: left_distrib right_distrib)
+ apply (auto simp add: distrib_right distrib_left)
done
lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) =
int(c) * int(card X)"
apply (induct set: finite)
- apply (auto simp add: right_distrib)
+ apply (auto simp add: distrib_left)
done
lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A =
c * setsum f A"
- by (induct set: finite) (auto simp add: right_distrib)
+ by (induct set: finite) (auto simp add: distrib_left)
subsection {* Cardinality of explicit finite sets *}
--- a/src/HOL/Old_Number_Theory/Gauss.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Old_Number_Theory/Gauss.thy Fri Oct 19 15:12:52 2012 +0200
@@ -341,7 +341,7 @@
apply (elim zcong_trans)
by (simp only: zcong_refl)
also have "y * a + ya * a = a * (y + ya)"
- by (simp add: right_distrib mult_commute)
+ by (simp add: distrib_left mult_commute)
finally have "[a * (y + ya) = 0] (mod p)" .
with p_prime a_nonzero zcong_zprime_prod_zero [of p a "y + ya"]
p_a_relprime
--- a/src/HOL/Old_Number_Theory/IntPrimes.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy Fri Oct 19 15:12:52 2012 +0200
@@ -341,7 +341,7 @@
lemma xzgcda_linear_aux1:
"(a - r * b) * m + (c - r * d) * (n::int) =
(a * m + c * n) - r * (b * m + d * n)"
- by (simp add: left_diff_distrib right_distrib mult_assoc)
+ by (simp add: left_diff_distrib distrib_left mult_assoc)
lemma xzgcda_linear_aux2:
"r' = s' * m + t' * n ==> r = s * m + t * n
--- a/src/HOL/Old_Number_Theory/Pocklington.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy Fri Oct 19 15:12:52 2012 +0200
@@ -161,7 +161,7 @@
and q12': "y + n*q1' = y'+n*q2'" unfolding nat_mod by blast+
from th[OF q12 q12' yx yx']
have "(x - y) + n*(q1 + q2') = (x' - y') + n*(q2 + q1')"
- by (simp add: right_distrib)
+ by (simp add: distrib_left)
thus ?thesis unfolding nat_mod by blast
qed
--- a/src/HOL/Presburger.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Presburger.thy Fri Oct 19 15:12:52 2012 +0200
@@ -54,7 +54,7 @@
"(d::'a::{comm_ring,Rings.dvd}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)"
"\<forall>x k. F = F"
apply (auto elim!: dvdE simp add: algebra_simps)
-unfolding mult_assoc [symmetric] left_distrib [symmetric] left_diff_distrib [symmetric]
+unfolding mult_assoc [symmetric] distrib_right [symmetric] left_diff_distrib [symmetric]
unfolding dvd_def mult_commute [of d]
by auto
--- a/src/HOL/Quickcheck_Narrowing.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy Fri Oct 19 15:12:52 2012 +0200
@@ -107,7 +107,7 @@
"n < m \<longleftrightarrow> int_of n < int_of m"
instance proof
-qed (auto simp add: code_int left_distrib zmult_zless_mono2)
+qed (auto simp add: code_int distrib_right zmult_zless_mono2)
end
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Fri Oct 19 15:12:52 2012 +0200
@@ -208,7 +208,7 @@
apply(induct "k")
apply(simp)
apply(case_tac "k = 0")
- apply(simp_all add: left_distrib add_strict_mono)
+ apply(simp_all add: distrib_right add_strict_mono)
done
lemma zero_le_imp_eq_int_raw:
@@ -248,8 +248,8 @@
qed
lemmas int_distrib =
- left_distrib [of z1 z2 w]
- right_distrib [of w z1 z2]
+ distrib_right [of z1 z2 w]
+ distrib_left [of w z1 z2]
left_diff_distrib [of z1 z2 w]
right_diff_distrib [of w z1 z2]
minus_add_distrib[of z1 z2]
--- a/src/HOL/Quotient_Examples/Quotient_Rat.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy Fri Oct 19 15:12:52 2012 +0200
@@ -128,7 +128,7 @@
show "1 * a = a"
by partiality_descending auto
show "a + b + c = a + (b + c)"
- by partiality_descending (auto simp add: mult_commute right_distrib)
+ by partiality_descending (auto simp add: mult_commute distrib_left)
show "a + b = b + a"
by partiality_descending auto
show "0 + a = a"
@@ -138,7 +138,7 @@
show "a - b = a + - b"
by (simp add: minus_rat_def)
show "(a + b) * c = a * c + b * c"
- by partiality_descending (auto simp add: mult_commute right_distrib)
+ by partiality_descending (auto simp add: mult_commute distrib_left)
show "(0 :: rat) \<noteq> (1 :: rat)"
by partiality_descending auto
qed
--- a/src/HOL/RComplete.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/RComplete.thy Fri Oct 19 15:12:52 2012 +0200
@@ -447,7 +447,7 @@
done
thus "x / real y < real (natfloor x div y) + 1"
using assms
- by (simp add: divide_less_eq natfloor_less_iff left_distrib)
+ by (simp add: divide_less_eq natfloor_less_iff distrib_right)
qed
lemma le_mult_natfloor:
--- a/src/HOL/Rat.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Rat.thy Fri Oct 19 15:12:52 2012 +0200
@@ -123,7 +123,7 @@
lift_definition plus_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat"
is "\<lambda>x y. (fst x * snd y + fst y * snd x, snd x * snd y)"
- by (clarsimp, simp add: left_distrib, simp add: mult_ac)
+ by (clarsimp, simp add: distrib_right, simp add: mult_ac)
lemma add_rat [simp]:
assumes "b \<noteq> 0" and "d \<noteq> 0"
@@ -616,8 +616,8 @@
(* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *)
#> Lin_Arith.add_simps [@{thm neg_less_iff_less},
@{thm True_implies_equals},
- read_instantiate @{context} [(("a", 0), "(numeral ?v)")] @{thm right_distrib},
- read_instantiate @{context} [(("a", 0), "(neg_numeral ?v)")] @{thm right_distrib},
+ read_instantiate @{context} [(("a", 0), "(numeral ?v)")] @{thm distrib_left},
+ read_instantiate @{context} [(("a", 0), "(neg_numeral ?v)")] @{thm distrib_left},
@{thm divide_1}, @{thm divide_zero_left},
@{thm times_divide_eq_right}, @{thm times_divide_eq_left},
@{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
--- a/src/HOL/RealDef.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/RealDef.thy Fri Oct 19 15:12:52 2012 +0200
@@ -494,7 +494,7 @@
show "1 * a = a"
by transfer (simp add: mult_ac realrel_def)
show "(a + b) * c = a * c + b * c"
- by transfer (simp add: left_distrib realrel_def)
+ by transfer (simp add: distrib_right realrel_def)
show "(0\<Colon>real) \<noteq> (1\<Colon>real)"
by transfer (simp add: realrel_def)
show "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
--- a/src/HOL/RealVector.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/RealVector.thy Fri Oct 19 15:12:52 2012 +0200
@@ -1081,8 +1081,8 @@
lemma bounded_bilinear_mult:
"bounded_bilinear (op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
apply (rule bounded_bilinear.intro)
-apply (rule left_distrib)
-apply (rule right_distrib)
+apply (rule distrib_right)
+apply (rule distrib_left)
apply (rule mult_scaleR_left)
apply (rule mult_scaleR_right)
apply (rule_tac x="1" in exI)
--- a/src/HOL/Rings.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Rings.thy Fri Oct 19 15:12:52 2012 +0200
@@ -14,14 +14,14 @@
begin
class semiring = ab_semigroup_add + semigroup_mult +
- assumes left_distrib[algebra_simps, field_simps]: "(a + b) * c = a * c + b * c"
- assumes right_distrib[algebra_simps, field_simps]: "a * (b + c) = a * b + a * c"
+ assumes distrib_right[algebra_simps, field_simps]: "(a + b) * c = a * c + b * c"
+ assumes distrib_left[algebra_simps, field_simps]: "a * (b + c) = a * b + a * c"
begin
text{*For the @{text combine_numerals} simproc*}
lemma combine_common_factor:
"a * e + (b * e + c) = (a + b) * e + c"
-by (simp add: left_distrib add_ac)
+by (simp add: distrib_right add_ac)
end
@@ -37,11 +37,11 @@
subclass semiring_0
proof
fix a :: 'a
- have "0 * a + 0 * a = 0 * a + 0" by (simp add: left_distrib [symmetric])
+ have "0 * a + 0 * a = 0 * a + 0" by (simp add: distrib_right [symmetric])
thus "0 * a = 0" by (simp only: add_left_cancel)
next
fix a :: 'a
- have "a * 0 + a * 0 = a * 0 + 0" by (simp add: right_distrib [symmetric])
+ have "a * 0 + a * 0 = a * 0 + 0" by (simp add: distrib_left [symmetric])
thus "a * 0 = 0" by (simp only: add_left_cancel)
qed
@@ -177,7 +177,7 @@
proof -
from `a dvd b` obtain b' where "b = a * b'" ..
moreover from `a dvd c` obtain c' where "c = a * c'" ..
- ultimately have "b + c = a * (b' + c')" by (simp add: right_distrib)
+ ultimately have "b + c = a * (b' + c')" by (simp add: distrib_left)
then show ?thesis ..
qed
@@ -227,10 +227,10 @@
text {* Distribution rules *}
lemma minus_mult_left: "- (a * b) = - a * b"
-by (rule minus_unique) (simp add: left_distrib [symmetric])
+by (rule minus_unique) (simp add: distrib_right [symmetric])
lemma minus_mult_right: "- (a * b) = a * - b"
-by (rule minus_unique) (simp add: right_distrib [symmetric])
+by (rule minus_unique) (simp add: distrib_left [symmetric])
text{*Extract signs from products*}
lemmas mult_minus_left [simp, no_atp] = minus_mult_left [symmetric]
@@ -243,13 +243,13 @@
by simp
lemma right_diff_distrib[algebra_simps, field_simps]: "a * (b - c) = a * b - a * c"
-by (simp add: right_distrib diff_minus)
+by (simp add: distrib_left diff_minus)
lemma left_diff_distrib[algebra_simps, field_simps]: "(a - b) * c = a * c - b * c"
-by (simp add: left_distrib diff_minus)
+by (simp add: distrib_right diff_minus)
lemmas ring_distribs[no_atp] =
- right_distrib left_distrib left_diff_distrib right_diff_distrib
+ distrib_left distrib_right left_diff_distrib right_diff_distrib
lemma eq_add_iff1:
"a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
@@ -262,7 +262,7 @@
end
lemmas ring_distribs[no_atp] =
- right_distrib left_distrib left_diff_distrib right_diff_distrib
+ distrib_left distrib_right left_diff_distrib right_diff_distrib
class comm_ring = comm_semiring + ab_group_add
begin
@@ -506,7 +506,7 @@
proof-
from assms have "u * x + v * y \<le> u * a + v * a"
by (simp add: add_mono mult_left_mono)
- thus ?thesis using assms unfolding left_distrib[symmetric] by simp
+ thus ?thesis using assms unfolding distrib_right[symmetric] by simp
qed
end
@@ -640,7 +640,7 @@
from assms have "u * x + v * y < u * a + v * a"
by (cases "u = 0")
(auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
- thus ?thesis using assms unfolding left_distrib[symmetric] by simp
+ thus ?thesis using assms unfolding distrib_right[symmetric] by simp
qed
end
--- a/src/HOL/Transcendental.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Transcendental.thy Fri Oct 19 15:12:52 2012 +0200
@@ -35,7 +35,7 @@
apply (simp del: setsum_op_ivl_Suc)
apply (subst setsum_op_ivl_Suc)
apply (subst lemma_realpow_diff_sumr)
-apply (simp add: right_distrib del: setsum_op_ivl_Suc)
+apply (simp add: distrib_left del: setsum_op_ivl_Suc)
apply (subst mult_left_commute [of "x - y"])
apply (erule subst)
apply (simp add: algebra_simps)
@@ -922,7 +922,7 @@
by (simp only: Suc)
also have "\<dots> = x * (\<Sum>i=0..n. S x i * S y (n-i))
+ y * (\<Sum>i=0..n. S x i * S y (n-i))"
- by (rule left_distrib)
+ by (rule distrib_right)
also have "\<dots> = (\<Sum>i=0..n. (x * S x i) * S y (n-i))
+ (\<Sum>i=0..n. S x i * (y * S y (n-i)))"
by (simp only: setsum_right_distrib mult_ac)
@@ -1001,7 +1001,7 @@
lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
apply (induct "n")
-apply (auto simp add: real_of_nat_Suc right_distrib exp_add mult_commute)
+apply (auto simp add: real_of_nat_Suc distrib_left exp_add mult_commute)
done
text {* Strict monotonicity of exponential. *}
@@ -1626,7 +1626,7 @@
lemma cos_npi [simp]: "cos (real n * pi) = -1 ^ n"
apply (induct "n")
-apply (auto simp add: real_of_nat_Suc left_distrib)
+apply (auto simp add: real_of_nat_Suc distrib_right)
done
lemma cos_npi2 [simp]: "cos (pi * real n) = -1 ^ n"
@@ -1638,7 +1638,7 @@
lemma sin_npi [simp]: "sin (real (n::nat) * pi) = 0"
apply (induct "n")
-apply (auto simp add: real_of_nat_Suc left_distrib)
+apply (auto simp add: real_of_nat_Suc distrib_right)
done
lemma sin_npi2 [simp]: "sin (pi * real (n::nat)) = 0"
@@ -1784,7 +1784,7 @@
\<exists>n::nat. even n & x = real n * (pi/2)"
apply (subgoal_tac "\<exists>n::nat. ~ even n & x + pi/2 = real n * (pi/2) ")
apply (clarify, rule_tac x = "n - 1" in exI)
- apply (force simp add: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib)
+ apply (force simp add: odd_Suc_mult_two_ex real_of_nat_Suc distrib_right)
apply (rule cos_zero_lemma)
apply (simp_all add: cos_add)
done
@@ -1799,7 +1799,7 @@
apply (drule cos_zero_lemma, assumption+)
apply (cut_tac x="-x" in cos_zero_lemma, simp, simp)
apply (force simp add: minus_equation_iff [of x])
-apply (auto simp only: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib)
+apply (auto simp only: odd_Suc_mult_two_ex real_of_nat_Suc distrib_right)
apply (auto simp add: cos_add)
done
@@ -2029,7 +2029,7 @@
lemma tan_periodic_nat[simp]: fixes n :: nat shows "tan (x + real n * pi) = tan x"
proof (induct n arbitrary: x)
case (Suc n)
- 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
+ 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
show ?case unfolding split_pi_off using Suc by auto
qed auto
@@ -2212,7 +2212,7 @@
show "0 \<le> cos (arctan x)"
by (intro less_imp_le cos_gt_zero_pi arctan_lbound arctan_ubound)
have "(cos (arctan x))\<twosuperior> * (1 + (tan (arctan x))\<twosuperior>) = 1"
- unfolding tan_def by (simp add: right_distrib power_divide)
+ unfolding tan_def by (simp add: distrib_left power_divide)
thus "(cos (arctan x))\<twosuperior> = (1 / sqrt (1 + x\<twosuperior>))\<twosuperior>"
using `0 < 1 + x\<twosuperior>` by (simp add: power_divide eq_divide_eq)
qed
@@ -2226,7 +2226,7 @@
apply (rule power_inverse [THEN subst])
apply (rule_tac c1 = "(cos x)\<twosuperior>" in real_mult_right_cancel [THEN iffD1])
apply (auto dest: field_power_not_zero
- simp add: power_mult_distrib left_distrib power_divide tan_def
+ simp add: power_mult_distrib distrib_right power_divide tan_def
mult_assoc power_inverse [symmetric])
done
@@ -2397,7 +2397,7 @@
have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
by (auto simp add: algebra_simps sin_add)
thus ?thesis
- by (simp add: real_of_nat_Suc left_distrib add_divide_distrib
+ by (simp add: real_of_nat_Suc distrib_right add_divide_distrib
mult_commute [of pi])
qed
@@ -2418,7 +2418,7 @@
done
lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
-by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib add_divide_distrib, auto)
+by (simp only: cos_add sin_add real_of_nat_Suc distrib_right distrib_left add_divide_distrib, auto)
lemma DERIV_cos_add [simp]: "DERIV (%x. cos (x + k)) xa :> - sin (xa + k)"
by (auto intro!: DERIV_intros)
--- a/src/HOL/Word/Misc_Numeric.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy Fri Oct 19 15:12:52 2012 +0200
@@ -301,7 +301,7 @@
apply assumption
done
-lemmas less_le_mult = less_le_mult' [simplified left_distrib, simplified]
+lemmas less_le_mult = less_le_mult' [simplified distrib_right, simplified]
lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult,
simplified left_diff_distrib]
--- a/src/HOL/Word/WordBitwise.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Word/WordBitwise.thy Fri Oct 19 15:12:52 2012 +0200
@@ -308,7 +308,7 @@
using Cons
apply (simp add: trans [OF of_bl_append add_commute]
rbl_mul_simps rbl_word_plus'
- Cons.hyps left_distrib mult_bit
+ Cons.hyps distrib_right mult_bit
shiftl rbl_shiftl)
apply (simp add: takefill_alt word_size rev_map take_rbl_plus
min_def)
--- a/src/HOL/ex/BT.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/ex/BT.thy Fri Oct 19 15:12:52 2012 +0200
@@ -107,7 +107,7 @@
lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t"
apply (induct t)
- apply (simp_all add: left_distrib)
+ apply (simp_all add: distrib_right)
done
lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
@@ -148,7 +148,7 @@
lemma n_leaves_append [simp]:
"n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2"
apply (induct t1)
- apply (simp_all add: left_distrib)
+ apply (simp_all add: distrib_right)
done
lemma bt_map_append:
--- a/src/HOL/ex/Dedekind_Real.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy Fri Oct 19 15:12:52 2012 +0200
@@ -285,7 +285,7 @@
show "\<exists>x' \<in> A. \<exists>y'\<in>B. z = x' + y'"
proof (intro bexI)
show "z = x*?f + y*?f"
- by (simp add: left_distrib [symmetric] divide_inverse mult_ac
+ by (simp add: distrib_right [symmetric] divide_inverse mult_ac
order_less_imp_not_eq2)
next
show "y * ?f \<in> B"
@@ -534,7 +534,7 @@
lemma distrib_subset1:
"Rep_preal (w * (x + y)) \<subseteq> Rep_preal (w * x + w * y)"
apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_mult_iff)
-apply (force simp add: right_distrib)
+apply (force simp add: distrib_left)
done
lemma preal_add_mult_distrib_mean:
@@ -555,13 +555,13 @@
proof (cases rule: linorder_le_cases)
assume "a \<le> b"
hence "?c \<le> b"
- by (simp add: pos_divide_le_eq right_distrib mult_right_mono
+ by (simp add: pos_divide_le_eq distrib_left mult_right_mono
order_less_imp_le)
thus ?thesis by (rule preal_downwards_closed' [OF Rep_preal b cpos])
next
assume "b \<le> a"
hence "?c \<le> a"
- by (simp add: pos_divide_le_eq right_distrib mult_right_mono
+ by (simp add: pos_divide_le_eq distrib_left mult_right_mono
order_less_imp_le)
thus ?thesis by (rule preal_downwards_closed' [OF Rep_preal a cpos])
qed
@@ -1333,7 +1333,7 @@
x * x1 + y * y1 + (x * y2 + y * x2) =
x * x2 + y * y2 + (x * y1 + y * x1)"
apply (simp add: add_left_commute add_assoc [symmetric])
-apply (simp add: add_assoc right_distrib [symmetric])
+apply (simp add: add_assoc distrib_left [symmetric])
apply (simp add: add_commute)
done
@@ -1543,7 +1543,7 @@
apply (rule real_sum_gt_zero_less)
apply (drule real_less_sum_gt_zero [of x y])
apply (drule real_mult_order, assumption)
-apply (simp add: right_distrib)
+apply (simp add: distrib_left)
done
instantiation real :: distrib_lattice
@@ -1986,7 +1986,7 @@
from t_is_Lub have "x * of_nat (Suc n) \<le> t"
by (simp add: isLubD2)
hence "x * (of_nat n) + x \<le> t"
- by (simp add: right_distrib)
+ by (simp add: distrib_left)
thus "x * (of_nat n) \<le> t + - x" by arith
qed
--- a/src/HOL/ex/Gauge_Integration.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/ex/Gauge_Integration.thy Fri Oct 19 15:12:52 2012 +0200
@@ -521,9 +521,9 @@
= (f z - f x) / (z - x) - f' x")
apply (simp add: abs_mult [symmetric] mult_ac diff_minus)
apply (subst mult_commute)
-apply (simp add: left_distrib diff_minus)
+apply (simp add: distrib_right diff_minus)
apply (simp add: mult_assoc divide_inverse)
-apply (simp add: left_distrib)
+apply (simp add: distrib_right)
done
lemma lemma_straddle:
--- a/src/HOL/ex/Numeral_Representation.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/ex/Numeral_Representation.thy Fri Oct 19 15:12:52 2012 +0200
@@ -153,7 +153,7 @@
"Dig1 n * Dig0 m = Dig0 (n * Dig0 m + m)"
"Dig1 n * Dig1 m = Dig1 (n * Dig1 m + m)"
by (simp_all add: num_eq_iff nat_of_num_add nat_of_num_mult
- left_distrib right_distrib)
+ distrib_right distrib_left)
lemma less_eq_num_code [numeral, simp, code]:
"One \<le> n \<longleftrightarrow> True"
@@ -243,7 +243,7 @@
by (induct n rule: num_induct) (simp_all add: add_One add_inc of_num_inc add_ac)
lemma of_num_mult: "of_num (m * n) = of_num m * of_num n"
- by (induct n rule: num_induct) (simp_all add: mult_One mult_inc of_num_add of_num_inc right_distrib)
+ by (induct n rule: num_induct) (simp_all add: mult_One mult_inc of_num_add of_num_inc distrib_left)
declare of_num.simps [simp del]
@@ -792,7 +792,7 @@
lemma mult_of_num_commute: "x * of_num n = of_num n * x"
by (induct n)
- (simp_all only: of_num.simps left_distrib right_distrib mult_1_left mult_1_right)
+ (simp_all only: of_num.simps distrib_right distrib_left mult_1_left mult_1_right)
definition
"commutes_with a b \<longleftrightarrow> a * b = b * a"