src/HOL/Library/Polynomial.thy
 changeset 57482 60459c3853af parent 56544 b60d5d119489 child 57512 cc97b347b301
1.1 --- a/src/HOL/Library/Polynomial.thy	Tue Jul 01 23:02:25 2014 +0200
1.2 +++ b/src/HOL/Library/Polynomial.thy	Tue Jul 01 21:57:08 2014 -0700
1.3 @@ -1588,6 +1588,35 @@
1.4    shows "(- x) mod y = - (x mod y)"
1.5    using mod_smult_left [of "- 1::'a"] by simp
1.7 +lemma pdivmod_rel_add_left:
1.8 +  assumes "pdivmod_rel x y q r"
1.9 +  assumes "pdivmod_rel x' y q' r'"
1.10 +  shows "pdivmod_rel (x + x') y (q + q') (r + r')"
1.11 +  using assms unfolding pdivmod_rel_def
1.12 +  by (auto simp add: distrib degree_add_less)
1.13 +
1.14 +lemma poly_div_add_left:
1.15 +  fixes x y z :: "'a::field poly"
1.16 +  shows "(x + y) div z = x div z + y div z"
1.17 +  using pdivmod_rel_add_left [OF pdivmod_rel pdivmod_rel]
1.18 +  by (rule div_poly_eq)
1.19 +
1.20 +lemma poly_mod_add_left:
1.21 +  fixes x y z :: "'a::field poly"
1.22 +  shows "(x + y) mod z = x mod z + y mod z"
1.23 +  using pdivmod_rel_add_left [OF pdivmod_rel pdivmod_rel]
1.24 +  by (rule mod_poly_eq)
1.25 +
1.26 +lemma poly_div_diff_left:
1.27 +  fixes x y z :: "'a::field poly"
1.28 +  shows "(x - y) div z = x div z - y div z"
1.29 +  by (simp only: diff_conv_add_uminus poly_div_add_left poly_div_minus_left)
1.30 +
1.31 +lemma poly_mod_diff_left:
1.32 +  fixes x y z :: "'a::field poly"
1.33 +  shows "(x - y) mod z = x mod z - y mod z"
1.34 +  by (simp only: diff_conv_add_uminus poly_mod_add_left poly_mod_minus_left)
1.35 +
1.36  lemma pdivmod_rel_smult_right:
1.37    "\<lbrakk>a \<noteq> 0; pdivmod_rel x y q r\<rbrakk>
1.38      \<Longrightarrow> pdivmod_rel x (smult a y) (smult (inverse a) q) r"