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

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Wed Jun 1 22:07:42 CEST 2016

>> 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
> These two lines are the plan. Is that a good one or a bad one?

I tinkered around with (a) fractions.gcd in Python and (b)

(a) has mixed signs for gcd
(b) has everything normalized

Maybe this is evidence that we are rather free in choosing our sign
rules, and then normalizing could be a legitimate choice, conceeding
that most practical occuring lcm computations concern non-negative


> Presently, I have used PolyML.IntInf.gcd and PolyML.IntInf.lcm for
> rat.ML (see da38571dd5bd). It somehow violates our cozy Isabelle/ML
> library environment to refer to structure PolyML.
> BTW, AFP has special code generator setup for PolyML.IntInf.gcd here:
> https://bitbucket.org/isa-afp/afp-devel/src/54c65361e6ed029f70572de89cfc5736153a0feb/thys/Gauss_Jordan/Code_Generation_IArrays_SML.thy?at=default&fileviewer=file-view-default#Code_Generation_IArrays_SML.thy-33
> https://bitbucket.org/isa-afp/afp-devel/src/54c65361e6ed029f70572de89cfc5736153a0feb/thys/Echelon_Form/Examples_Echelon_Form_IArrays.thy?at=default&fileviewer=file-view-default#Examples_Echelon_Form_IArrays.thy-44
> Luckily, this is only gcd and not lcm, so it coincides already.
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160601/979f6342/attachment.sig>

More information about the isabelle-dev mailing list