# Re: [isabelle] Code generator: overloaded numeric constants

```Hi Florian,

```
I'd like to stay with just the "syntactic" number, plus, etc. classes, since our Haskell number instances don't necessarily satisfy the ring axioms. So I can generate reasonable Haskell code from this Isabelle definition:
```
definition
"foo (x::'a::{number,plus,times}) y = x + number_of 2 * y"

```
However I don't want to have to insert "number_of" functions wherever I'm using a numeric literal. But right now I don't see any way of generating reasonable Haskell code from this more readable version of the above definition:
```
definition
"foo (x::'a::{number,plus,times}) y = x + 2 * y"

```
Is there any way to get the code generator to work well on this second form?
```
Thanks,
-john

On Jun 11, 2010, at 11:49 PM, Florian Haftmann wrote:

```
```Hi John,

the number class in Isabelle/HOL is a little bit arcane;  concerning
code generation, you may use numerals on numeric types (nat, int, rat,
real), but not polymorphic ('a::number).  Otherwise you only get
formally and partially correct code:

```
``` foo :: forall a. (Plus a, Times a, Number a) => a -> a -> a;
foo x y =
plus x (times (number_of (error "Bit0" (error "Bit1" (error
"Pls")))) y);
```
```
In typical Isabelle/HOL specifications, the number class will not show
```
up that often since it is only syntactic -- a classical joke is that you cannot prove "2 + 2 = (4::'a::number)". Of more relevance is the class
```number_ring which describes structures in which the integers can be
embedded semantically (number_of = of_int).  This you can use to
circumvent the number_of problem: instead of

definition double :: "'a::number_ring ⇒ 'a" where
"double k = 2 * k"

write

definition double :: "'a::number_ring ⇒ 'a" where
"double k = of_int 2 * k"

Since (number_of = of_int), you can even prove the second version from
the first.  This could also be done by the preprocessor but would
```
require writing a simproc since the naive rewrite (number_of k = of_int
```(number_of k)) does not terminate.

Hope this helps,
Florian

--

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

```
```
```

Attachment: smime.p7s
Description: S/MIME cryptographic signature

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