*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Gcd class and polynomials*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Wed, 01 Oct 2014 10:16:33 +0200*In-reply-to*: <CA+MUZ5ubp5VKTNj5Rej7W_wjNm13gzeD0SOy4PYJt=Kuyr-Nvw@mail.gmail.com>*References*: <CA+MUZ5ubp5VKTNj5Rej7W_wjNm13gzeD0SOy4PYJt=Kuyr-Nvw@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.1.2

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

**References**:**[isabelle] Gcd class and polynomials***From:*Jose Divasón

- Previous by Date: [isabelle] Gcd class and polynomials
- Next by Date: Re: [isabelle] Problems with code-datatype
- Previous by Thread: [isabelle] Gcd class and polynomials
- Next by Thread: Re: [isabelle] Gcd class and polynomials
- Cl-isabelle-users October 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list