Re: [isabelle] Gcd class and polynomials



I assume lcm does not exist because no one ever needed it. This was
actually one of the main reasons why I chose to overhaul the whole GCD
stuff in HOL – many results I needed about the GCD of polynomials were
missing.

For an instantiation of GCD for polynomials, see Polynomial.thy on my
Github repo: https://github.com/3of8/isabellehol_gcd

I know that the whole thing with gcd and gcd_eucl is a bit complicated;
this was because we wanted to keep the existing gcd/lcm constants purely
syntactical, as before.

Cheers,
Manuel


On 01.10.2014 10:58, Jose Divasón wrote:
> Dear all,
>
> In Isabelle there is the class gcd:
>
> class gcd = zero + one + dvd +
>   fixes gcd :: "'a => 'a => 'a"
>     and lcm :: "'a => 'a => 'a"
>
>
> Polynomials (
> http://isabelle.in.tum.de/library/HOL/HOL-Library/Polynomial.html) have
> been instantiated to such a class defining a gcd for polynomials, but
> saying nothing about lcm:
>
> instantiation poly :: (field) gcdbegin
> function gcd_poly :: "'a::field poly => 'a poly => 'a poly"where
>   "gcd (x::'a poly) 0 = smult (inverse (coeff x (degree x))) x"| "y ≠
> 0 ==> gcd (x::'a poly) y = gcd y (x mod y)"by auto
> termination "gcd :: _ poly => _"by (relation "measure (λ(x, y). if y =
> 0 then 0 else Suc (degree y))")
>    (auto dest: degree_mod_less)
> declare gcd_poly.simps [simp del]
> instance ..
> end
>
>
> So, I am wondering why there is no definition of lcm for polynomials, but
> polynomials have been made a gcd instance.
>
> In addition, gcd of polynomials can be computed:
>
> value "gcd [:2,3,6,5::real :] [:4,6,12,10:]" returns "[:2 / 5, 3 / 5, 6 /
> 5, 1:]"  :: "real poly"
>
> On the contrary, lcm can't be computed (since it has not been defined).
>
> The problem arose when I was trying to instantiate polynomials to the
> euclidean_ring_gcd class developed by Manuel Eberl (
> http://isabelle.in.tum.de/repos/isabelle/file/5f88c142676d/src/HOL/Number_Theory/Euclidean_Algorithm.thy).
> There I have to prove that "(lcm::'a poly⇒ 'a poly ⇒ 'a poly) = lcm_eucl",
> but I can't prove it since I don't know anything about lcm for polynomials.
>
> If lcm for polynomials is defined in the instance to the gcd class (for
> example, by means of the below definition), then lcm could be computed and
> the statement "(lcm::'a poly⇒ 'a poly ⇒ 'a poly) = lcm_eucl" can be proved.
>
> definition lcm_poly :: "'a::field poly ⇒ 'a poly ⇒ 'a poly"
> where "lcm_poly x xa = x * xa div (gcd x xa * [:coeff (x * xa) (degree (x *
> xa)):])"
>
>
> Cheers,
> Jose





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