gcd instances for poly
authorhaftmann
Wed Feb 17 21:51:58 2016 +0100 (2016-02-17)
changeset 62351fd049b54ad68
parent 62350 66a381d3f88f
child 62352 35a9e1cbb5b3
gcd instances for poly
src/HOL/Library/Polynomial.thy
     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.9      by (simp add: mult_monom)
    1.10  qed
    1.11  
    1.12 @@ -1602,7 +1602,7 @@
    1.13  begin
    1.14  
    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.18  
    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.32      by (simp add: normalize_poly_def)
    1.33 @@ -1645,6 +1646,21 @@
    1.34  
    1.35  end
    1.36  
    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.58  
    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.82  
    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.87  
    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)))"
    1.91    by (simp add: gcd_poly.simps)
    1.92  
    1.93