src/HOL/Library/Polynomial.thy
 changeset 30930 11010e5f18f0 parent 30738 0842e906300c child 30960 fec1a04b7220
equal 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:`