[isabelle-dev] construction of the real numbers
lp15 at cam.ac.uk
Mon May 10 12:49:27 CEST 2010
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.
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?
More information about the isabelle-dev