[isabelle] int vs. of_nat
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and