Email Gateway (Aug 18 2022 at 10:34): Email Gateway (Aug 18 2022 at 10:34):From: Brian Huffman <brianh@cs.pdx.edu>
Hello all,
Isabelle's standard library has two different coercions from the naturals to
the integers: IntDef.thy defines "int::nat=>int" which is monomorphic, and
Nat.thy defines "of_nat::nat=>'a" which coerces from naturals into an
arbitrary semiring. At type "nat=>int" they both mean exactly the same thing
(see lemma IntDef.int_eq_of_nat). The only difference is that they are each
set up with different sets of simp rules.
My question is, why do we have both? If any of you have chosen to use one over
the other, which one did you choose, and why?
Unless there is a compelling reason to keep both, I would propose to either
make "int" an abbreviation for "of_nat::nat=>int", or just eliminate it
altogether. Also, if users prefer the way the simplifier works with "int",
then the simp rules for "of_nat" should be changed accordingly.
I could also ask the same thing about the overloaded function "real::'a=>real"
from the HOL-Complex library, which is redundant with "of_nat::nat=>real" and
"of_int::int=>real" at those types. Do we need separate constants for these?
Email Gateway (Aug 18 2022 at 10:34):From: Tobias Nipkow <nipkow@in.tum.de>
The duplication is not intentional and it would be nice to eliminate it.
One could choose either "ty :: 'a => ty" or "of_ty :: ty => 'a" as
primitive (int::nat=>int should have been int::'a=>int) and relate them
via (ty :: ty' => ty) = (of_ty' :: ty' => ty) for specif ty and ty'.
Function ty :: 'a => ty has the advantage of being the familiar one
whereas of_ty is somewhat unusual. However, I gather that of_ty often
allows to formulate polymorphic theorems whereas ty does not.
Maybe one could combine both advantages: of_ty is the primitive, but
monomorphic instances are printed as ty (and ty is also allowed upon input).
Tobias
Brian Huffman wrote:
Email Gateway (Aug 18 2022 at 10:34):From: Lawrence Paulson <lp15@cam.ac.uk>
The reasons are historical. Function "int" belongs to the original
construction of the integers. When (a few years ago) I reworked the
numeric types to take advantage of type classes, I realised that a
polymorphic "of_nat" function could easily be defined. Naturally most
developments should use of_nat rather than int, but function "int"
appears to be necessary to develop the integers in the first place
and to establish the type class axioms.
Note that "of_nat" has a single polymorphic definition. There is a
similar function of_int, and we could easily define of_rat too, all
using type classes. On the other hand, "real" is merely an overloaded
constant, which is far less attractive.
Larry
Last updated: May 03 2024 at 08:18 UTC