src/HOL/Polynomial.thy
changeset 29472 a63a2e46cec9
parent 29471 6a46a13ce1f9
child 29474 674a21226c5a
     1.1 --- a/src/HOL/Polynomial.thy	Tue Jan 13 07:40:05 2009 -0800
     1.2 +++ b/src/HOL/Polynomial.thy	Tue Jan 13 08:19:14 2009 -0800
     1.3 @@ -413,7 +413,7 @@
     1.4  lemma degree_smult_le: "degree (smult a p) \<le> degree p"
     1.5    by (rule degree_le, simp add: coeff_eq_0)
     1.6  
     1.7 -lemma smult_smult: "smult a (smult b p) = smult (a * b) p"
     1.8 +lemma smult_smult [simp]: "smult a (smult b p) = smult (a * b) p"
     1.9    by (rule poly_ext, simp add: mult_assoc)
    1.10  
    1.11  lemma smult_0_right [simp]: "smult a 0 = 0"
    1.12 @@ -449,6 +449,10 @@
    1.13    "smult (a - b::'a::comm_ring) p = smult a p - smult b p"
    1.14    by (rule poly_ext, simp add: ring_simps)
    1.15  
    1.16 +lemmas smult_distribs =
    1.17 +  smult_add_left smult_add_right
    1.18 +  smult_diff_left smult_diff_right
    1.19 +
    1.20  lemma smult_pCons [simp]:
    1.21    "smult a (pCons b p) = pCons (a * b) (smult a p)"
    1.22    by (rule poly_ext, simp add: coeff_pCons split: nat.split)
    1.23 @@ -591,11 +595,11 @@
    1.24    "p * pCons a q = smult a p + pCons 0 (p * q)"
    1.25    using mult_pCons_left [of a q p] by (simp add: mult_commute)
    1.26  
    1.27 -lemma mult_smult_left: "smult a p * q = smult a (p * q)"
    1.28 -  by (induct p, simp, simp add: smult_add_right smult_smult)
    1.29 +lemma mult_smult_left [simp]: "smult a p * q = smult a (p * q)"
    1.30 +  by (induct p, simp, simp add: smult_add_right)
    1.31  
    1.32 -lemma mult_smult_right: "p * smult a q = smult a (p * q)"
    1.33 -  using mult_smult_left [of a q p] by (simp add: mult_commute)
    1.34 +lemma mult_smult_right [simp]: "p * smult a q = smult a (p * q)"
    1.35 +  by (induct q, simp, simp add: smult_add_right)
    1.36  
    1.37  lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)"
    1.38    by (induct m, simp add: monom_0 smult_monom, simp add: monom_Suc)