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

[Florian Haftmann]

Hi Makarius,

> 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
> 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.)

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,
though:

	Integer.gcd = PolyML.gcd
	Integer.lcm = abs oo PolyML.lcm

Cheers,
	Florian


> 
> 
> Does this sound like a good idea?
> 
> 
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160601/943378bd/attachment.asc>