declare smult rules [simp]
authorhuffman
Tue Jan 13 08:19:14 2009 -0800 (2009-01-13)
changeset 29472a63a2e46cec9
parent 29471 6a46a13ce1f9
child 29473 5fc19891652c
declare smult rules [simp]
src/HOL/Deriv.thy
src/HOL/Fundamental_Theorem_Algebra.thy
src/HOL/Polynomial.thy
     1.1 --- a/src/HOL/Deriv.thy	Tue Jan 13 07:40:05 2009 -0800
     1.2 +++ b/src/HOL/Deriv.thy	Tue Jan 13 08:19:14 2009 -0800
     1.3 @@ -1475,7 +1475,7 @@
     1.4  apply (subst power_Suc)
     1.5  apply (subst pderiv_mult)
     1.6  apply (erule ssubst)
     1.7 -apply (simp add: mult_smult_right mult_smult_left smult_add_left ring_simps)
     1.8 +apply (simp add: smult_add_left ring_simps)
     1.9  done
    1.10  
    1.11  lemma DERIV_cmult2: "DERIV f x :> D ==> DERIV (%x. (f x) * c :: real) x :> D * c"
     2.1 --- a/src/HOL/Fundamental_Theorem_Algebra.thy	Tue Jan 13 07:40:05 2009 -0800
     2.2 +++ b/src/HOL/Fundamental_Theorem_Algebra.thy	Tue Jan 13 08:19:14 2009 -0800
     2.3 @@ -1115,8 +1115,7 @@
     2.4            from k oop [of a] have "q ^ n = p * ?w"
     2.5              apply -
     2.6              apply (subst r, subst s, subst kpn)
     2.7 -            apply (subst power_mult_distrib)
     2.8 -            apply (simp add: mult_smult_left mult_smult_right smult_smult)
     2.9 +            apply (subst power_mult_distrib, simp)
    2.10              apply (subst power_add [symmetric], simp)
    2.11              done
    2.12  	  hence ?ths unfolding dvd_def by blast}
     3.1 --- a/src/HOL/Polynomial.thy	Tue Jan 13 07:40:05 2009 -0800
     3.2 +++ b/src/HOL/Polynomial.thy	Tue Jan 13 08:19:14 2009 -0800
     3.3 @@ -413,7 +413,7 @@
     3.4  lemma degree_smult_le: "degree (smult a p) \<le> degree p"
     3.5    by (rule degree_le, simp add: coeff_eq_0)
     3.6  
     3.7 -lemma smult_smult: "smult a (smult b p) = smult (a * b) p"
     3.8 +lemma smult_smult [simp]: "smult a (smult b p) = smult (a * b) p"
     3.9    by (rule poly_ext, simp add: mult_assoc)
    3.10  
    3.11  lemma smult_0_right [simp]: "smult a 0 = 0"
    3.12 @@ -449,6 +449,10 @@
    3.13    "smult (a - b::'a::comm_ring) p = smult a p - smult b p"
    3.14    by (rule poly_ext, simp add: ring_simps)
    3.15  
    3.16 +lemmas smult_distribs =
    3.17 +  smult_add_left smult_add_right
    3.18 +  smult_diff_left smult_diff_right
    3.19 +
    3.20  lemma smult_pCons [simp]:
    3.21    "smult a (pCons b p) = pCons (a * b) (smult a p)"
    3.22    by (rule poly_ext, simp add: coeff_pCons split: nat.split)
    3.23 @@ -591,11 +595,11 @@
    3.24    "p * pCons a q = smult a p + pCons 0 (p * q)"
    3.25    using mult_pCons_left [of a q p] by (simp add: mult_commute)
    3.26  
    3.27 -lemma mult_smult_left: "smult a p * q = smult a (p * q)"
    3.28 -  by (induct p, simp, simp add: smult_add_right smult_smult)
    3.29 +lemma mult_smult_left [simp]: "smult a p * q = smult a (p * q)"
    3.30 +  by (induct p, simp, simp add: smult_add_right)
    3.31  
    3.32 -lemma mult_smult_right: "p * smult a q = smult a (p * q)"
    3.33 -  using mult_smult_left [of a q p] by (simp add: mult_commute)
    3.34 +lemma mult_smult_right [simp]: "p * smult a q = smult a (p * q)"
    3.35 +  by (induct q, simp, simp add: smult_add_right)
    3.36  
    3.37  lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)"
    3.38    by (induct m, simp add: monom_0 smult_monom, simp add: monom_Suc)