Re: [isabelle] Gcd class and polynomials



Thank you both!!

I was working with my local clone of Polynomial.thy, but it's nice to see
such a trick. I have already seen the new lcm definition in the repository
version.

Cheers,
Jose

2014-10-02 11:30 GMT+02:00 Florian Haftmann <
florian.haftmann at informatik.tu-muenchen.de>:

> 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
>
>



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