Re: [isabelle] Real number numeric literals in Isabelle
On Thursday 15 December 2005 03:07, Primrose.Mbanefo at Infineon.com wrote:
> 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).
This archive was generated by a fusion of
Pipermail (Mailman edition) and