author haftmann Wed Feb 17 21:51:58 2016 +0100 (2016-02-17) changeset 62351 fd049b54ad68 parent 62350 66a381d3f88f child 62352 35a9e1cbb5b3
gcd instances for poly
1.1 --- a/src/HOL/Library/Polynomial.thy	Wed Feb 17 21:51:57 2016 +0100
1.2 +++ b/src/HOL/Library/Polynomial.thy	Wed Feb 17 21:51:58 2016 +0100
1.3 @@ -1551,7 +1551,7 @@
1.4    assumes "a \<noteq> 0"
1.5    shows "is_unit (monom a 0)"
1.6  proof
1.7 -  from assms show "1 = monom a 0 * monom (1 / a) 0"
1.8 +  from assms show "1 = monom a 0 * monom (inverse a) 0"
1.10  qed
1.12 @@ -1602,7 +1602,7 @@
1.13  begin
1.15  definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
1.16 -  where "normalize_poly p = smult (1 / coeff p (degree p)) p"
1.17 +  where "normalize_poly p = smult (inverse (coeff p (degree p))) p"
1.19  definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
1.20    where "unit_factor_poly p = monom (coeff p (degree p)) 0"
1.21 @@ -1611,8 +1611,9 @@
1.22  proof
1.23    fix p :: "'a poly"
1.24    show "unit_factor p * normalize p = p"
1.25 -    by (simp add: normalize_poly_def unit_factor_poly_def)
1.26 -      (simp only: mult_smult_left [symmetric] smult_monom, simp)
1.27 +    by (cases "p = 0")
1.28 +      (simp_all add: normalize_poly_def unit_factor_poly_def,
1.29 +      simp only: mult_smult_left [symmetric] smult_monom, simp)
1.30  next
1.31    show "normalize 0 = (0::'a poly)"
1.33 @@ -1645,6 +1646,21 @@
1.35  end
1.37 +lemma unit_factor_monom [simp]:
1.38 +  "unit_factor (monom a n) =
1.39 +     (if a = 0 then 0 else monom a 0)"
1.40 +  by (simp add: unit_factor_poly_def degree_monom_eq)
1.41 +
1.42 +lemma unit_factor_pCons [simp]:
1.43 +  "unit_factor (pCons a p) =
1.44 +     (if p = 0 then monom a 0 else unit_factor p)"
1.45 +  by (simp add: unit_factor_poly_def)
1.46 +
1.47 +lemma normalize_monom [simp]:
1.48 +  "normalize (monom a n) =
1.49 +     (if a = 0 then 0 else monom 1 n)"
1.50 +  by (simp add: normalize_poly_def degree_monom_eq smult_monom)
1.51 +
1.52  lemma degree_mod_less:
1.53    "y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
1.54    using pdivmod_rel [of x y]
1.55 @@ -1983,20 +1999,16 @@
1.56      by (rule poly_dvd_antisym)
1.57  qed
1.59 -interpretation gcd_poly: abel_semigroup "gcd :: _ poly \<Rightarrow> _"
1.60 +instance poly :: (field) semiring_gcd
1.61  proof
1.62 -  fix x y z :: "'a poly"
1.63 -  show "gcd (gcd x y) z = gcd x (gcd y z)"
1.64 -    by (rule poly_gcd_unique) (auto intro: dvd_trans simp add: poly_gcd_monic)
1.65 -  show "gcd x y = gcd y x"
1.66 -    by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
1.67 -qed
1.68 -
1.69 -lemmas poly_gcd_assoc = gcd_poly.assoc
1.70 -lemmas poly_gcd_commute = gcd_poly.commute
1.71 -lemmas poly_gcd_left_commute = gcd_poly.left_commute
1.72 -
1.73 -lemmas poly_gcd_ac = poly_gcd_assoc poly_gcd_commute poly_gcd_left_commute
1.74 +  fix p q :: "'a::field poly"
1.75 +  show "normalize (gcd p q) = gcd p q"
1.76 +    by (induct p q rule: gcd_poly.induct)
1.77 +      (simp_all add: gcd_poly.simps normalize_poly_def)
1.78 +  show "lcm p q = normalize (p * q) div gcd p q"
1.79 +    by (simp add: coeff_degree_mult div_smult_left div_smult_right lcm_poly_def normalize_poly_def)
1.80 +      (metis (no_types, lifting) div_smult_right inverse_mult_distrib inverse_zero mult.commute pdivmod_rel pdivmod_rel_def smult_eq_0_iff)
1.81 +qed simp_all
1.83  lemma poly_gcd_1_left [simp]: "gcd 1 y = (1 :: _ poly)"
1.84  by (rule poly_gcd_unique) simp_all
1.85 @@ -2011,7 +2023,7 @@
1.86  by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
1.88  lemma poly_gcd_code [code]:
1.89 -  "gcd x y = (if y = 0 then smult (inverse (coeff x (degree x))) x else gcd y (x mod (y :: _ poly)))"
1.90 +  "gcd x y = (if y = 0 then normalize x else gcd y (x mod (y :: _ poly)))"