*To*: John Matthews <matthews at galois.com>, Florian Haftmann <haftmann at in.tum.de>*Subject*: Re: [isabelle] Code generator: overloaded numeric constants*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Sat, 12 Jun 2010 08:49:32 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <C8BDF99A-E03A-4507-B1FB-158724B9587C@galois.com>*Organization*: TU München, Lehrstuhl Software and Systems Engineering*References*: <C8BDF99A-E03A-4507-B1FB-158724B9587C@galois.com>*User-agent*: Thunderbird 2.0.0.24 (X11/20100317)

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:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Code generator: overloaded numeric constants***From:*John Matthews

**References**:**[isabelle] Code generator: overloaded numeric constants***From:*John Matthews

- Previous by Date: Re: [isabelle] Haskell code generation feature request
- Next by Date: Re: [isabelle] Code generator "eq" instances
- Previous by Thread: [isabelle] Code generator: overloaded numeric constants
- Next by Thread: Re: [isabelle] Code generator: overloaded numeric constants
- Cl-isabelle-users June 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list