[isabelle] Real number numeric literals in Isabelle



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?

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


Out of need to try the different numerals I defined the following
constant:

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.

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...).


Thanks for any answers.

Primrose






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