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