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.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.43  lemma div_pCons_eq:
1.44    "pCons a p div q =