--- a/src/HOL/Library/Polynomial.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Library/Polynomial.thy Wed Feb 17 21:51:58 2016 +0100
@@ -1551,7 +1551,7 @@
assumes "a \<noteq> 0"
shows "is_unit (monom a 0)"
proof
- from assms show "1 = monom a 0 * monom (1 / a) 0"
+ from assms show "1 = monom a 0 * monom (inverse a) 0"
by (simp add: mult_monom)
qed
@@ -1602,7 +1602,7 @@
begin
definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
- where "normalize_poly p = smult (1 / coeff p (degree p)) p"
+ where "normalize_poly p = smult (inverse (coeff p (degree p))) p"
definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
where "unit_factor_poly p = monom (coeff p (degree p)) 0"
@@ -1611,8 +1611,9 @@
proof
fix p :: "'a poly"
show "unit_factor p * normalize p = p"
- by (simp add: normalize_poly_def unit_factor_poly_def)
- (simp only: mult_smult_left [symmetric] smult_monom, simp)
+ by (cases "p = 0")
+ (simp_all add: normalize_poly_def unit_factor_poly_def,
+ simp only: mult_smult_left [symmetric] smult_monom, simp)
next
show "normalize 0 = (0::'a poly)"
by (simp add: normalize_poly_def)
@@ -1645,6 +1646,21 @@
end
+lemma unit_factor_monom [simp]:
+ "unit_factor (monom a n) =
+ (if a = 0 then 0 else monom a 0)"
+ by (simp add: unit_factor_poly_def degree_monom_eq)
+
+lemma unit_factor_pCons [simp]:
+ "unit_factor (pCons a p) =
+ (if p = 0 then monom a 0 else unit_factor p)"
+ by (simp add: unit_factor_poly_def)
+
+lemma normalize_monom [simp]:
+ "normalize (monom a n) =
+ (if a = 0 then 0 else monom 1 n)"
+ by (simp add: normalize_poly_def degree_monom_eq smult_monom)
+
lemma degree_mod_less:
"y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
using pdivmod_rel [of x y]
@@ -1983,20 +1999,16 @@
by (rule poly_dvd_antisym)
qed
-interpretation gcd_poly: abel_semigroup "gcd :: _ poly \<Rightarrow> _"
+instance poly :: (field) semiring_gcd
proof
- fix x y z :: "'a poly"
- show "gcd (gcd x y) z = gcd x (gcd y z)"
- by (rule poly_gcd_unique) (auto intro: dvd_trans simp add: poly_gcd_monic)
- show "gcd x y = gcd y x"
- by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
-qed
-
-lemmas poly_gcd_assoc = gcd_poly.assoc
-lemmas poly_gcd_commute = gcd_poly.commute
-lemmas poly_gcd_left_commute = gcd_poly.left_commute
-
-lemmas poly_gcd_ac = poly_gcd_assoc poly_gcd_commute poly_gcd_left_commute
+ fix p q :: "'a::field poly"
+ show "normalize (gcd p q) = gcd p q"
+ by (induct p q rule: gcd_poly.induct)
+ (simp_all add: gcd_poly.simps normalize_poly_def)
+ show "lcm p q = normalize (p * q) div gcd p q"
+ by (simp add: coeff_degree_mult div_smult_left div_smult_right lcm_poly_def normalize_poly_def)
+ (metis (no_types, lifting) div_smult_right inverse_mult_distrib inverse_zero mult.commute pdivmod_rel pdivmod_rel_def smult_eq_0_iff)
+qed simp_all
lemma poly_gcd_1_left [simp]: "gcd 1 y = (1 :: _ poly)"
by (rule poly_gcd_unique) simp_all
@@ -2011,7 +2023,7 @@
by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
lemma poly_gcd_code [code]:
- "gcd x y = (if y = 0 then smult (inverse (coeff x (degree x))) x else gcd y (x mod (y :: _ poly)))"
+ "gcd x y = (if y = 0 then normalize x else gcd y (x mod (y :: _ poly)))"
by (simp add: gcd_poly.simps)