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"