# 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 in.tum.de
Raum: 01.11.059

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