Re: [isabelle] Gcd class and polynomials



Hi Jose,

> So, I am wondering why there is no definition of lcm for polynomials, but
> polynomials have been made a gcd instance.

this is indeed an omission.

You can add a lcm definition either by making your local clone of
Polynomial.thy, or by a low-level trick:

defs
  lcm_gcd_inst_def: "gcd_poly_inst.lcm_poly a b == a * b div smult
(coeff a (degree a) * coeff b (degree b)) (gcd a b)"

lemma lcm_gcd_def:
  "lcm a b = a * b div smult (coeff a (degree a) * coeff b (degree b))
(gcd a b)"
  apply (tactic ‹ALLGOALS (CONVERSION (Axclass.unoverload_conv @{theory}))›)
  unfolding lcm_gcd_inst_def
  apply (tactic ‹ALLGOALS (CONVERSION (Axclass.overload_conv @{theory}))›)
  ..

I am currently underway to incorporate a proper lcm definition into
Polynomial.thy, so in future releases this issue is resolved.

Hope this helps,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.