Re: [isabelle] query about real number representation


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.

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.

Steven Obua
Technische Universität München
Institut für Informatik
Boltzmannstr. 3
D-85748 Garching

Tel: ++49 (0)89 / 289-17328
EMail: obua at
Raum: 01.11.059

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