src/HOL/Library/Polynomial.thy
 changeset 30930 11010e5f18f0 parent 30738 0842e906300c child 30960 fec1a04b7220
```     1.1 --- a/src/HOL/Library/Polynomial.thy	Wed Apr 15 15:52:37 2009 +0200
1.2 +++ b/src/HOL/Library/Polynomial.thy	Thu Apr 16 10:11:34 2009 +0200
1.3 @@ -987,6 +987,30 @@
1.4      by (simp add: pdivmod_rel_def left_distrib)
1.5    thus "(x + z * y) div y = z + x div y"
1.6      by (rule div_poly_eq)
1.7 +next
1.8 +  fix x y z :: "'a poly"
1.9 +  assume "x \<noteq> 0"
1.10 +  show "(x * y) div (x * z) = y div z"
1.11 +  proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
1.12 +    have "\<And>x::'a poly. pdivmod_rel x 0 0 x"
1.13 +      by (rule pdivmod_rel_by_0)
1.14 +    then have [simp]: "\<And>x::'a poly. x div 0 = 0"
1.15 +      by (rule div_poly_eq)
1.16 +    have "\<And>x::'a poly. pdivmod_rel 0 x 0 0"
1.17 +      by (rule pdivmod_rel_0)
1.18 +    then have [simp]: "\<And>x::'a poly. 0 div x = 0"
1.19 +      by (rule div_poly_eq)
1.20 +    case False then show ?thesis by auto
1.21 +  next
1.22 +    case True then have "y \<noteq> 0" and "z \<noteq> 0" by auto
1.23 +    with `x \<noteq> 0`
1.24 +    have "\<And>q r. pdivmod_rel y z q r \<Longrightarrow> pdivmod_rel (x * y) (x * z) q (x * r)"
1.25 +      by (auto simp add: pdivmod_rel_def algebra_simps)
1.26 +        (rule classical, simp add: degree_mult_eq)
1.27 +    moreover from pdivmod_rel have "pdivmod_rel y z (y div z) (y mod z)" .
1.28 +    ultimately have "pdivmod_rel (x * y) (x * z) (y div z) (x * (y mod z))" .
1.29 +    then show ?thesis by (simp add: div_poly_eq)
1.30 +  qed
1.31  qed
1.32
1.33  end
```