author huffman Mon, 23 Feb 2009 07:19:53 -0800 changeset 30072 4eecd8b9b6cf parent 30071 be46f437ace2 child 30073 a4ad0c08b7d9
```--- a/src/HOL/Library/Polynomial.thy	Mon Feb 23 06:51:26 2009 -0800
+++ b/src/HOL/Library/Polynomial.thy	Mon Feb 23 07:19:53 2009 -0800
@@ -1020,6 +1020,16 @@
lemma mod_smult_left: "(smult a x) mod y = smult a (x mod y)"
by (rule mod_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel)

+lemma poly_div_minus_left [simp]:
+  fixes x y :: "'a::field poly"
+  shows "(- x) div y = - (x div y)"
+  using div_smult_left [of "- 1::'a"] by simp
+
+lemma poly_mod_minus_left [simp]:
+  fixes x y :: "'a::field poly"
+  shows "(- x) mod y = - (x mod y)"
+  using mod_smult_left [of "- 1::'a"] by simp
+
lemma pdivmod_rel_smult_right:
"\<lbrakk>a \<noteq> 0; pdivmod_rel x y q r\<rbrakk>
\<Longrightarrow> pdivmod_rel x (smult a y) (smult (inverse a) q) r"
@@ -1032,6 +1042,17 @@
lemma mod_smult_right: "a \<noteq> 0 \<Longrightarrow> x mod (smult a y) = x mod y"
by (rule mod_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel)

+lemma poly_div_minus_right [simp]:
+  fixes x y :: "'a::field poly"
+  shows "x div (- y) = - (x div y)"
+  using div_smult_right [of "- 1::'a"]