[isabelle-dev] construction of the real numbers

[Lawrence Paulson]

Thank you for doing this. It's interesting that you have found a shorter formalisation, because the approach previously adopted had been carefully selected to require the minimum effort.

I agree that the old formalisation should be kept somewhere (possibly in the AFP) because comparing formalisations can be instructive.

Larry

On 10 May 2010, at 07:52, Brian Huffman wrote:

> I recently finished a formalization of real numbers that uses Cauchy
> sequences. I thought it might be good to replace the current
> formalization (which uses Dedekind cuts) with this new one in time for
> the upcoming Isabelle release.
> 
> Users should not need to know or care which construction of reals we
> use. The primary advantage of the new formalization is its size: It is
> shorter than the current development of the reals by about a thousand
> lines of code. It reduces the size of the Isabelle/HOL heap image
> (without proof objects) by almost a megabyte.
> 
> I would propose to move the current development of the reals into an
> example theory, say HOL/ex/Dedekind_Real.thy.
> 
> Are there any objections or comments?