add lemmas poly_{div,mod}_minus_{left,right}
authorhuffman
Mon Feb 23 07:19:53 2009 -0800 (2009-02-23)
changeset 300724eecd8b9b6cf
parent 30071 be46f437ace2
child 30073 a4ad0c08b7d9
add lemmas poly_{div,mod}_minus_{left,right}
src/HOL/Library/Polynomial.thy
     1.1 --- a/src/HOL/Library/Polynomial.thy	Mon Feb 23 06:51:26 2009 -0800
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Mon Feb 23 07:19:53 2009 -0800
     1.3 @@ -1020,6 +1020,16 @@
     1.4  lemma mod_smult_left: "(smult a x) mod y = smult a (x mod y)"
     1.5    by (rule mod_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel)
     1.6  
     1.7 +lemma poly_div_minus_left [simp]:
     1.8 +  fixes x y :: "'a::field poly"
     1.9 +  shows "(- x) div y = - (x div y)"
    1.10 +  using div_smult_left [of "- 1::'a"] by simp
    1.11 +
    1.12 +lemma poly_mod_minus_left [simp]:
    1.13 +  fixes x y :: "'a::field poly"
    1.14 +  shows "(- x) mod y = - (x mod y)"
    1.15 +  using mod_smult_left [of "- 1::'a"] by simp
    1.16 +
    1.17  lemma pdivmod_rel_smult_right:
    1.18    "\<lbrakk>a \<noteq> 0; pdivmod_rel x y q r\<rbrakk>
    1.19      \<Longrightarrow> pdivmod_rel x (smult a y) (smult (inverse a) q) r"
    1.20 @@ -1032,6 +1042,17 @@
    1.21  lemma mod_smult_right: "a \<noteq> 0 \<Longrightarrow> x mod (smult a y) = x mod y"
    1.22    by (rule mod_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel)
    1.23  
    1.24 +lemma poly_div_minus_right [simp]:
    1.25 +  fixes x y :: "'a::field poly"
    1.26 +  shows "x div (- y) = - (x div y)"
    1.27 +  using div_smult_right [of "- 1::'a"]
    1.28 +  by (simp add: nonzero_inverse_minus_eq)
    1.29 +
    1.30 +lemma poly_mod_minus_right [simp]:
    1.31 +  fixes x y :: "'a::field poly"
    1.32 +  shows "x mod (- y) = x mod y"
    1.33 +  using mod_smult_right [of "- 1::'a"] by simp
    1.34 +
    1.35  lemma pdivmod_rel_mult:
    1.36    "\<lbrakk>pdivmod_rel x y q r; pdivmod_rel q z q' r'\<rbrakk>
    1.37      \<Longrightarrow> pdivmod_rel x (y * z) q' (y * r' + r)"