Email Gateway (Aug 17 2022 at 13:26): Email Gateway (Aug 17 2022 at 13:26):From: Chen Chunqing <g0301019@nus.edu.sg>
Hi, all,
I am curious that how Isabelle/HOL represent real number, for example,
the positive square root of 2.
I know in the theory PReal, it applies Dedekind's cut to construct
positive real numbers from rational numbers.
However, it does not illustrate the way to express explicit real number,
for example, the positive square root of 2 in Isabelle/HOL, like the
normal floating number, e.g., 3222 * 10^-5 in Isabelle/HOL.
Could you kindly enlighten me how Isabelle/HOL specify explicit real
numbers?
Thanks & Regards
Chunqing
Email Gateway (Aug 17 2022 at 13:26):From: Steven Obua <obua@in.tum.de>
There is only very rudimentary support for explicit real number
representation in Isabelle. In Isabelle 2004, there is none. In the
Isabelle developer version you will find a theory HOL/Real/Float.thy
which defines a binary floating point representation via a function
float : int * int => real
The first argument is the mantissa, the second the exponent, so for example
float (5034375, 6) = 3222 * 105
There are already theorems for addition and multiplication of such
floats. There are no theorems for square roots, division and the like.
Note that the result of these operations may not be representable as a
float but can only be approximated by intervals.
Last updated: May 03 2024 at 08:18 UTC