[isabelle] Gcd class and polynomials



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.