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

[David Matthews]

On 02/06/2016 08:19, Manuel Eberl wrote:
> I do think that we should enforce the same thing in the ML
> implementation of gcd/lcm. Any definition of gcd/lcm for integers where
> either of them may be negative does not make much sense to me. My guess
> would be that lcm can be negative in the implementation you mentioned
> because the author defined "lcm a b = a * b / gcd a b" with the unstated
> assumption that it is only called for non-negative numbers. Or perhaps
> they thought the sign does not matter.

The Poly/ML implementation was based on the idea that something called a 
"multiple" ought to follow the usual rules of multiplication; nothing 
stronger than that.  I don't think I found anything that indicated what 
the sign should be.  The GCD code uses GMP's GCD if possible; the LCM 
code is just derived from that.

I have no strong opinions on this and I'm happy to change it.  There's 
also the question of whether to add it to the IntInf structure and 
signature despite the incompatibility with the "official" library 
definition.

David