# HG changeset patch
# User huffman
# Date 1232598056 28800
# Node ID f8d2c03ecfd8002d3072abaed2b1bf02e704b335
# Parent  2db3537c35359b6de460d4a3de1ed90766a986a0
add lemmas about smult

diff -r 2db3537c3535 -r f8d2c03ecfd8 src/HOL/Polynomial.thy
--- a/src/HOL/Polynomial.thy	Wed Jan 21 23:25:17 2009 +0100
+++ b/src/HOL/Polynomial.thy	Wed Jan 21 20:20:56 2009 -0800
@@ -475,6 +475,16 @@
 lemma smult_monom: "smult a (monom b n) = monom (a * b) n"
   by (induct n, simp add: monom_0, simp add: monom_Suc)
 
+lemma degree_smult_eq [simp]:
+  fixes a :: "'a::idom"
+  shows "degree (smult a p) = (if a = 0 then 0 else degree p)"
+  by (cases "a = 0", simp, simp add: degree_def)
+
+lemma smult_eq_0_iff [simp]:
+  fixes a :: "'a::idom"
+  shows "smult a p = 0 \<longleftrightarrow> a = 0 \<or> p = 0"
+  by (simp add: expand_poly_eq)
+
 
 subsection {* Multiplication of polynomials *}
 
@@ -861,6 +871,29 @@
   thus "x mod y = x" by (rule mod_poly_eq)
 qed
 
+lemma pdivmod_rel_smult_left:
+  "pdivmod_rel x y q r
+    \<Longrightarrow> pdivmod_rel (smult a x) y (smult a q) (smult a r)"
+  unfolding pdivmod_rel_def by (simp add: smult_add_right)
+
+lemma div_smult_left: "(smult a x) div y = smult a (x div y)"
+  by (rule div_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel)
+
+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 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"
+  unfolding pdivmod_rel_def by simp
+
+lemma div_smult_right:
+  "a \<noteq> 0 \<Longrightarrow> x div (smult a y) = smult (inverse a) (x div y)"
+  by (rule div_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel)
+
+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 mod_pCons:
   fixes a and x
   assumes y: "y \<noteq> 0"