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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
