Re: [isabelle] Real number numeric literals in Isabelle



Hello Primrose,

On Thursday 15 December 2005 12:07, Primrose.Mbanefo at Infineon.com wrote:
> 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?
>
> Is there any other way of representing such constants? Maybe one of the
> theories uses the mantissa and exponent representation?

I am not familiar with the real-numerals in Isabelle.

> consts totosum :: "real * real => real"
>
> recdef totosum  "measure((\<lambda>(n, m). nat (floor n)) :: real*real
> => nat)"
> "totosum (n, x) =  (if n < 0 then -1 else if (0 <= n \<and> n < 1) then
> x else totosum ((n - 1), (x + 1)))"
>
> Now out of curiosity, I am wondering how I could have defined that
> better... espescially the "measure" part.

Why do you think this measure is bad?

> I am trying to translate files in c++ format to Isabelle/hol theory
> files. I have not reached this generation stage yet but just out of
> curiosity:
> It is possible in c++ to leave out some of the cases e.g the n < 0 case.
> Is there a way of making isabelle also ignore these cases or build in a
> default for them?
> I suspect that this is not possible (I do not know if it would make much
> sense to do such a thing...) and the user would have to modify the
> generated file(which might not be very helpful either...).

HOL is a logic of total functions. So you cannot just leave out cases. But 
since every type in HOL has at least one member,  there is indeed a default 
value called arbitrary. You can return it instead of -1, to emphasise that 
this is a "dead end"...

   Norbert





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