[isabelle-dev] Proper sign of gcd / lcm on type int

[Makarius]

Dear integer experts,

presently on Isabelle/c3896c385c3e and AFP/d9305abd02e9, I am trying to
understand the situation of gcd / lcm for negative arguments.

We have the following slightly divergent operations:

  * HOL gcd / lcm: always >= 0 (via "normalize" which is "abs")

  * PolyML.IntInf.gcd: always >= 0
    PolyML.IntInf.lcm: mixed signs, according to product of arguments

  * Integer.gcd / lcm: mixed signs -- IIRC the implementation was only
meant to operate on "nat", which happens to be spelled "int" in ML.

My impression is that the HOL definitions are canonical: several number
theory experts have gone over it over the years. Is this correct?


An investigation of the (very few) uses of the above Poly/ML and
Isabelle/ML operations in Isabelle + AFP supports the following working
hypothesis:

Integer.gcd / lcm should follow the HOL versions, in "normalizing" the
sign, i.e. removing it. (The updated implementation will use
PolyML.IntInf gcd for improved performance.)


Does this sound like a good idea?


	Makarius