declare smult rules [simp]

--- a/src/HOL/Deriv.thy	Tue Jan 13 07:40:05 2009 -0800
+++ b/src/HOL/Deriv.thy	Tue Jan 13 08:19:14 2009 -0800
@@ -1475,7 +1475,7 @@
 apply (subst power_Suc)
 apply (subst pderiv_mult)
 apply (erule ssubst)
-apply (simp add: mult_smult_right mult_smult_left smult_add_left ring_simps)
+apply (simp add: smult_add_left ring_simps)
 done
 
 lemma DERIV_cmult2: "DERIV f x :> D ==> DERIV (%x. (f x) * c :: real) x :> D * c"

--- a/src/HOL/Fundamental_Theorem_Algebra.thy	Tue Jan 13 07:40:05 2009 -0800
+++ b/src/HOL/Fundamental_Theorem_Algebra.thy	Tue Jan 13 08:19:14 2009 -0800
@@ -1115,8 +1115,7 @@
           from k oop [of a] have "q ^ n = p * ?w"
             apply -
             apply (subst r, subst s, subst kpn)
-            apply (subst power_mult_distrib)
-            apply (simp add: mult_smult_left mult_smult_right smult_smult)
+            apply (subst power_mult_distrib, simp)
             apply (subst power_add [symmetric], simp)
             done
 	  hence ?ths unfolding dvd_def by blast}

--- a/src/HOL/Polynomial.thy	Tue Jan 13 07:40:05 2009 -0800
+++ b/src/HOL/Polynomial.thy	Tue Jan 13 08:19:14 2009 -0800
@@ -413,7 +413,7 @@
 lemma degree_smult_le: "degree (smult a p) \<le> degree p"
   by (rule degree_le, simp add: coeff_eq_0)
 
-lemma smult_smult: "smult a (smult b p) = smult (a * b) p"
+lemma smult_smult [simp]: "smult a (smult b p) = smult (a * b) p"
   by (rule poly_ext, simp add: mult_assoc)
 
 lemma smult_0_right [simp]: "smult a 0 = 0"
@@ -449,6 +449,10 @@
   "smult (a - b::'a::comm_ring) p = smult a p - smult b p"
   by (rule poly_ext, simp add: ring_simps)
 
+lemmas smult_distribs =
+  smult_add_left smult_add_right
+  smult_diff_left smult_diff_right
+
 lemma smult_pCons [simp]:
   "smult a (pCons b p) = pCons (a * b) (smult a p)"
   by (rule poly_ext, simp add: coeff_pCons split: nat.split)
@@ -591,11 +595,11 @@
   "p * pCons a q = smult a p + pCons 0 (p * q)"
   using mult_pCons_left [of a q p] by (simp add: mult_commute)
 
-lemma mult_smult_left: "smult a p * q = smult a (p * q)"
-  by (induct p, simp, simp add: smult_add_right smult_smult)
+lemma mult_smult_left [simp]: "smult a p * q = smult a (p * q)"
+  by (induct p, simp, simp add: smult_add_right)
 
-lemma mult_smult_right: "p * smult a q = smult a (p * q)"
-  using mult_smult_left [of a q p] by (simp add: mult_commute)
+lemma mult_smult_right [simp]: "p * smult a q = smult a (p * q)"
+  by (induct q, simp, simp add: smult_add_right)
 
 lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)"
   by (induct m, simp add: monom_0 smult_monom, simp add: monom_Suc)