# HG changeset patch # User haftmann # Date 1484044638 -3600 # Node ID 9e8de30fd8598df673a0fdf6f399e67091fe8a2e # Parent 4d56170d97b3713a869293bbac7b1cdb6ba5a19e separate instance for semidom_modulo diff -r 4d56170d97b3 -r 9e8de30fd859 src/HOL/Library/Polynomial.thy --- a/src/HOL/Library/Polynomial.thy Mon Jan 09 23:00:11 2017 +0100 +++ b/src/HOL/Library/Polynomial.thy Tue Jan 10 11:37:18 2017 +0100 @@ -3650,29 +3650,36 @@ lemmas eucl_rel_poly_unique_mod = eucl_rel_poly_unique [THEN conjunct2] -instantiation poly :: (field) ring_div +instantiation poly :: (field) semidom_modulo begin - -definition modulo_poly where - mod_poly_def: "f mod g \ - if g = 0 then f - else pseudo_mod (smult ((1/coeff g (degree g)) ^ (Suc (degree f) - degree g)) f) g" - -lemma eucl_rel_poly: "eucl_rel_poly (x::'a::field poly) y (x div y, x mod y)" - unfolding eucl_rel_poly_iff -proof (intro conjI) - show "x = x div y * y + x mod y" - proof(cases "y = 0") - case True show ?thesis by(simp add: True divide_poly_def divide_poly_0 mod_poly_def) + +definition modulo_poly :: "'a poly \ 'a poly \ 'a poly" + where mod_poly_def: "f mod g = (if g = 0 then f + else pseudo_mod (smult ((1 / lead_coeff g) ^ (Suc (degree f) - degree g)) f) g)" + +instance proof + fix x y :: "'a poly" + show "x div y * y + x mod y = x" + proof (cases "y = 0") + case True then show ?thesis + by (simp add: divide_poly_0 mod_poly_def) next case False - then have "pseudo_divmod (smult ((1 / coeff y (degree y)) ^ (Suc (degree x) - degree y)) x) y = - (x div y, x mod y)" - unfolding divide_poly_field mod_poly_def pseudo_mod_def by simp - from pseudo_divmod[OF False this] + then have "pseudo_divmod (smult ((1 / lead_coeff y) ^ (Suc (degree x) - degree y)) x) y = + (x div y, x mod y)" + by (simp add: divide_poly_field mod_poly_def pseudo_mod_def) + from pseudo_divmod [OF False this] show ?thesis using False - by (simp add: power_mult_distrib[symmetric] mult.commute) + by (simp add: power_mult_distrib [symmetric] ac_simps) qed +qed + +end + +lemma eucl_rel_poly: "eucl_rel_poly x y (x div y, x mod y)" +unfolding eucl_rel_poly_iff proof + show "x = x div y * y + x mod y" + by (simp add: div_mult_mod_eq) show "if y = 0 then x div y = 0 else x mod y = 0 \ degree (x mod y) < degree y" proof (cases "y = 0") case True then show ?thesis by auto @@ -3684,18 +3691,14 @@ lemma div_poly_eq: "eucl_rel_poly (x::'a::field poly) y (q, r) \ x div y = q" - by(rule eucl_rel_poly_unique_div[OF eucl_rel_poly]) + by(rule eucl_rel_poly_unique_div [OF eucl_rel_poly]) lemma mod_poly_eq: "eucl_rel_poly (x::'a::field poly) y (q, r) \ x mod y = r" - by (rule eucl_rel_poly_unique_mod[OF eucl_rel_poly]) - -instance + by (rule eucl_rel_poly_unique_mod [OF eucl_rel_poly]) + +instance poly :: (field) ring_div proof - fix x y :: "'a poly" - from eucl_rel_poly[of x y,unfolded eucl_rel_poly_iff] - show "x div y * y + x mod y = x" by auto -next fix x y z :: "'a poly" assume "y \ 0" hence "eucl_rel_poly (x + z * y) y (z + x div y, x mod y)" @@ -3729,8 +3732,6 @@ qed qed -end - lemma div_pCons_eq: "pCons a p div q = (if q = 0 then 0 else pCons (coeff (pCons a (p mod q)) (degree q) / lead_coeff q)