Re: [isabelle] Code generator: overloaded numeric constants



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
Description: OpenPGP digital signature



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