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
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.
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 ..
> 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 (
> 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 *
This archive was generated by a fusion of
Pipermail (Mailman edition) and