src/HOL/Computational_Algebra/Polynomial.thy
changeset 66806 a4e82b58d833
parent 66805 274b4edca859
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Computational_Algebra/Polynomial.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Computational_Algebra/Polynomial.thy	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -3637,40 +3637,7 @@
     1.4    for x :: "'a::field poly"
     1.5    by (rule eucl_rel_poly_unique_mod [OF eucl_rel_poly])
     1.6  
     1.7 -instance poly :: (field) ring_div
     1.8 -proof
     1.9 -  fix x y z :: "'a poly"
    1.10 -  assume "y \<noteq> 0"
    1.11 -  with eucl_rel_poly [of x y] have "eucl_rel_poly (x + z * y) y (z + x div y, x mod y)"
    1.12 -    by (simp add: eucl_rel_poly_iff distrib_right)
    1.13 -  then show "(x + z * y) div y = z + x div y"
    1.14 -    by (rule div_poly_eq)
    1.15 -next
    1.16 -  fix x y z :: "'a poly"
    1.17 -  assume "x \<noteq> 0"
    1.18 -  show "(x * y) div (x * z) = y div z"
    1.19 -  proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
    1.20 -    have "\<And>x::'a poly. eucl_rel_poly x 0 (0, x)"
    1.21 -      by (rule eucl_rel_poly_by_0)
    1.22 -    then have [simp]: "\<And>x::'a poly. x div 0 = 0"
    1.23 -      by (rule div_poly_eq)
    1.24 -    have "\<And>x::'a poly. eucl_rel_poly 0 x (0, 0)"
    1.25 -      by (rule eucl_rel_poly_0)
    1.26 -    then have [simp]: "\<And>x::'a poly. 0 div x = 0"
    1.27 -      by (rule div_poly_eq)
    1.28 -    case False
    1.29 -    then show ?thesis by auto
    1.30 -  next
    1.31 -    case True
    1.32 -    then have "y \<noteq> 0" and "z \<noteq> 0" by auto
    1.33 -    with \<open>x \<noteq> 0\<close> have "\<And>q r. eucl_rel_poly y z (q, r) \<Longrightarrow> eucl_rel_poly (x * y) (x * z) (q, x * r)"
    1.34 -      by (auto simp: eucl_rel_poly_iff algebra_simps) (rule classical, simp add: degree_mult_eq)
    1.35 -    moreover from eucl_rel_poly have "eucl_rel_poly y z (y div z, y mod z)" .
    1.36 -    ultimately have "eucl_rel_poly (x * y) (x * z) (y div z, x * (y mod z))" .
    1.37 -    then show ?thesis
    1.38 -      by (simp add: div_poly_eq)
    1.39 -  qed
    1.40 -qed
    1.41 +instance poly :: (field) idom_modulo ..
    1.42  
    1.43  lemma div_pCons_eq:
    1.44    "pCons a p div q =