[isabelle-dev] Proper sign of gcd / lcm on type int
florian.haftmann at informatik.tu-muenchen.de
Wed Jun 1 21:27:58 CEST 2016
> 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?
well, I tend to say they are Isabelle/HOLish.
You could also legitimately specify polymorphic gcd as
gcd :: nat => nat => nat
gcd :: int => int => nat
gcd :: …
but then you cannot use (single-parameter) type classes.
Or you could only specify properties on equivalence classes, e.g.
gcd a a =[dvd]= a
where a =[dvd]= b <--> a dvd b && b dvd a
but such properties cannot be used as rewrite rules of the simplifier.
> An investigation of the (very few) uses of the above Poly/ML and
> Isabelle/ML operations in Isabelle + AFP supports the following working
> 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.)
Note that the mixed signs of PolyML.IntInf.lcm maintain the property
gcd a b * lcm a b = a * b
whereas the lcm in GCD.thy obeys
gcd a b * lcm a b = normalize a * normalize b
which emphasises the dual nature of the gcd/lcm lattice.
Both are ok in my view; ironically, lcm is used more often in
Isabelle/ML than gcd. Providing an lcm in the manner of HOL is trivial,
Integer.gcd = PolyML.gcd
Integer.lcm = abs oo PolyML.lcm
> Does this sound like a good idea?
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 819 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev