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).


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.