# Re: [isabelle] int vs. of_nat

`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:

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?
`
- Brian

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*