Re: [isabelle] query about real number representation
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
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.
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.
Technische Universität München
Institut für Informatik
Tel: ++49 (0)89 / 289-17328
EMail: obua at in.tum.de
This archive was generated by a fusion of
Pipermail (Mailman edition) and