author huffman Tue, 13 Jan 2009 08:19:14 -0800 changeset 29472 a63a2e46cec9 parent 29471 6a46a13ce1f9 child 29473 5fc19891652c
declare smult rules [simp]
 src/HOL/Deriv.thy file | annotate | diff | comparison | revisions src/HOL/Fundamental_Theorem_Algebra.thy file | annotate | diff | comparison | revisions src/HOL/Polynomial.thy file | annotate | diff | comparison | revisions
```--- 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)
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_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)```