# Re: [isabelle] int vs. of_nat

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

On 8 Jun 2007, at 00:22, Brian Huffman wrote:

```
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 MHonArc.