Re: [isabelle] Real number numeric literals in Isabelle

On Thursday 15 December 2005 03:07, Primrose.Mbanefo at wrote:
> Hello,
> I have a short question on which real numbers numerals are syntactically
> correct in Isabelle.
> The manual says literals like 4, (5/15), 2 * 10^6 are accepted.
> I am wondering if it is possible to represent literals like:
> 2 * 10 ^-6 and 1.3?

In Isabelle the power operator (^) takes a natural number as its second 
argument. Since there are no negative naturals, -6::nat is actually 
interpreted as being equal to 0::nat. So 2 * 10 ^-6 is probably not what you 
want; you can use 2 / 10^6 instead.

Isabelle currently does not have support for decimal point syntax for numbers 
like 1.3 (although it would be possible to add support for it by writing some 
ML code). You could just translate 1.3 as 13/10, and longer decimals like 
123.4567 as 1234567/10^4.

> Is there any other way of representing such constants? Maybe one of the
> theories uses the mantissa and exponent representation?

Check out the file HOL/Real/Float.thy in the Isabelle sources. There is a 
constant float :: int * int => real that might be close to what you want (but 
it uses base 2 instead of base 10 for the exponent).

- Brian

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