*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] Code generator: overloaded numeric constants*From*: John Matthews <matthews at galois.com>*Date*: Sat, 12 Jun 2010 13:50:22 -0700*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4C132DFC.4060301@informatik.tu-muenchen.de>*References*: <C8BDF99A-E03A-4507-B1FB-158724B9587C@galois.com> <4C132DFC.4060301@informatik.tu-muenchen.de>

Hi Florian,

definition "foo (x::'a::{number,plus,times}) y = x + number_of 2 * y"

definition "foo (x::'a::{number,plus,times}) y = x + 2 * y"

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 showup that often since it is only syntactic -- a classical joke is thatyoucannot prove "2 + 2 = (4::'a::number)". Of more relevance is theclassnumber_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 wouldrequire 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**

**Follow-Ups**:**Re: [isabelle] Code generator: overloaded numeric constants***From:*Florian Haftmann

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

**Re: [isabelle] Code generator: overloaded numeric constants***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] Code generator "eq" instances
- Next by Date: Re: [isabelle] power class instantiation
- Previous by Thread: Re: [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