add lemmas about smult
authorhuffman
Wed Jan 21 20:20:56 2009 -0800 (2009-01-21)
changeset 29659f8d2c03ecfd8
parent 29607 2db3537c3535
child 29660 d59918e668b7
add lemmas about smult
src/HOL/Polynomial.thy
     1.1 --- a/src/HOL/Polynomial.thy	Wed Jan 21 23:25:17 2009 +0100
     1.2 +++ b/src/HOL/Polynomial.thy	Wed Jan 21 20:20:56 2009 -0800
     1.3 @@ -475,6 +475,16 @@
     1.4  lemma smult_monom: "smult a (monom b n) = monom (a * b) n"
     1.5    by (induct n, simp add: monom_0, simp add: monom_Suc)
     1.6  
     1.7 +lemma degree_smult_eq [simp]:
     1.8 +  fixes a :: "'a::idom"
     1.9 +  shows "degree (smult a p) = (if a = 0 then 0 else degree p)"
    1.10 +  by (cases "a = 0", simp, simp add: degree_def)
    1.11 +
    1.12 +lemma smult_eq_0_iff [simp]:
    1.13 +  fixes a :: "'a::idom"
    1.14 +  shows "smult a p = 0 \<longleftrightarrow> a = 0 \<or> p = 0"
    1.15 +  by (simp add: expand_poly_eq)
    1.16 +
    1.17  
    1.18  subsection {* Multiplication of polynomials *}
    1.19  
    1.20 @@ -861,6 +871,29 @@
    1.21    thus "x mod y = x" by (rule mod_poly_eq)
    1.22  qed
    1.23  
    1.24 +lemma pdivmod_rel_smult_left:
    1.25 +  "pdivmod_rel x y q r
    1.26 +    \<Longrightarrow> pdivmod_rel (smult a x) y (smult a q) (smult a r)"
    1.27 +  unfolding pdivmod_rel_def by (simp add: smult_add_right)
    1.28 +
    1.29 +lemma div_smult_left: "(smult a x) div y = smult a (x div y)"
    1.30 +  by (rule div_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel)
    1.31 +
    1.32 +lemma mod_smult_left: "(smult a x) mod y = smult a (x mod y)"
    1.33 +  by (rule mod_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel)
    1.34 +
    1.35 +lemma pdivmod_rel_smult_right:
    1.36 +  "\<lbrakk>a \<noteq> 0; pdivmod_rel x y q r\<rbrakk>
    1.37 +    \<Longrightarrow> pdivmod_rel x (smult a y) (smult (inverse a) q) r"
    1.38 +  unfolding pdivmod_rel_def by simp
    1.39 +
    1.40 +lemma div_smult_right:
    1.41 +  "a \<noteq> 0 \<Longrightarrow> x div (smult a y) = smult (inverse a) (x div y)"
    1.42 +  by (rule div_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel)
    1.43 +
    1.44 +lemma mod_smult_right: "a \<noteq> 0 \<Longrightarrow> x mod (smult a y) = x mod y"
    1.45 +  by (rule mod_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel)
    1.46 +
    1.47  lemma mod_pCons:
    1.48    fixes a and x
    1.49    assumes y: "y \<noteq> 0"