src/HOL/Library/Polynomial.thy
changeset 30930 11010e5f18f0
parent 30738 0842e906300c
child 30960 fec1a04b7220
equal deleted inserted replaced
30929:d9343c0aac11 30930:11010e5f18f0
   985   hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
   985   hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
   986     using pdivmod_rel [of x y]
   986     using pdivmod_rel [of x y]
   987     by (simp add: pdivmod_rel_def left_distrib)
   987     by (simp add: pdivmod_rel_def left_distrib)
   988   thus "(x + z * y) div y = z + x div y"
   988   thus "(x + z * y) div y = z + x div y"
   989     by (rule div_poly_eq)
   989     by (rule div_poly_eq)
       
   990 next
       
   991   fix x y z :: "'a poly"
       
   992   assume "x \<noteq> 0"
       
   993   show "(x * y) div (x * z) = y div z"
       
   994   proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
       
   995     have "\<And>x::'a poly. pdivmod_rel x 0 0 x"
       
   996       by (rule pdivmod_rel_by_0)
       
   997     then have [simp]: "\<And>x::'a poly. x div 0 = 0"
       
   998       by (rule div_poly_eq)
       
   999     have "\<And>x::'a poly. pdivmod_rel 0 x 0 0"
       
  1000       by (rule pdivmod_rel_0)
       
  1001     then have [simp]: "\<And>x::'a poly. 0 div x = 0"
       
  1002       by (rule div_poly_eq)
       
  1003     case False then show ?thesis by auto
       
  1004   next
       
  1005     case True then have "y \<noteq> 0" and "z \<noteq> 0" by auto
       
  1006     with `x \<noteq> 0`
       
  1007     have "\<And>q r. pdivmod_rel y z q r \<Longrightarrow> pdivmod_rel (x * y) (x * z) q (x * r)"
       
  1008       by (auto simp add: pdivmod_rel_def algebra_simps)
       
  1009         (rule classical, simp add: degree_mult_eq)
       
  1010     moreover from pdivmod_rel have "pdivmod_rel y z (y div z) (y mod z)" .
       
  1011     ultimately have "pdivmod_rel (x * y) (x * z) (y div z) (x * (y mod z))" .
       
  1012     then show ?thesis by (simp add: div_poly_eq)
       
  1013   qed
   990 qed
  1014 qed
   991 
  1015 
   992 end
  1016 end
   993 
  1017 
   994 lemma degree_mod_less:
  1018 lemma degree_mod_less: