# HG changeset patch
# User huffman
# Date 1232600475 28800
# Node ID d59918e668b7a3f632a4d73de61c7242391d0991
# Parent  f8d2c03ecfd8002d3072abaed2b1bf02e704b335
add lemmas about div/mod with multiplication

diff -r f8d2c03ecfd8 -r d59918e668b7 src/HOL/Polynomial.thy
--- a/src/HOL/Polynomial.thy	Wed Jan 21 20:20:56 2009 -0800
+++ b/src/HOL/Polynomial.thy	Wed Jan 21 21:01:15 2009 -0800
@@ -787,6 +787,12 @@
   qed
 qed
 
+lemma pdivmod_rel_0_iff: "pdivmod_rel 0 y q r \<longleftrightarrow> q = 0 \<and> r = 0"
+by (auto dest: pdivmod_rel_unique intro: pdivmod_rel_0)
+
+lemma pdivmod_rel_by_0_iff: "pdivmod_rel x 0 q r \<longleftrightarrow> q = 0 \<and> r = x"
+by (auto dest: pdivmod_rel_unique intro: pdivmod_rel_by_0)
+
 lemmas pdivmod_rel_unique_div =
   pdivmod_rel_unique [THEN conjunct1, standard]
 
@@ -894,6 +900,31 @@
 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 pdivmod_rel_mult:
+  "\<lbrakk>pdivmod_rel x y q r; pdivmod_rel q z q' r'\<rbrakk>
+    \<Longrightarrow> pdivmod_rel x (y * z) q' (y * r' + r)"
+apply (cases "z = 0", simp add: pdivmod_rel_def)
+apply (cases "y = 0", simp add: pdivmod_rel_by_0_iff pdivmod_rel_0_iff)
+apply (cases "r = 0")
+apply (cases "r' = 0")
+apply (simp add: pdivmod_rel_def)
+apply (simp add: pdivmod_rel_def ring_simps degree_mult_eq)
+apply (cases "r' = 0")
+apply (simp add: pdivmod_rel_def degree_mult_eq)
+apply (simp add: pdivmod_rel_def ring_simps)
+apply (simp add: degree_mult_eq degree_add_less)
+done
+
+lemma poly_div_mult_right:
+  fixes x y z :: "'a::field poly"
+  shows "x div (y * z) = (x div y) div z"
+  by (rule div_poly_eq, rule pdivmod_rel_mult, (rule pdivmod_rel)+)
+
+lemma poly_mod_mult_right:
+  fixes x y z :: "'a::field poly"
+  shows "x mod (y * z) = y * (x div y mod z) + x mod y"
+  by (rule mod_poly_eq, rule pdivmod_rel_mult, (rule pdivmod_rel)+)
+
 lemma mod_pCons:
   fixes a and x
   assumes y: "y \<noteq> 0"