[isabelle] Real number numeric literals in Isabelle
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
consts totosum :: "real * real => real"
recdef totosum "measure((\<lambda>(n, m). nat (floor n)) :: real*real
"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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and