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