[isabelle-dev] construction of the real numbers

[Makarius]

On Sun, 9 May 2010, 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.

>From the feedback I've got so far for the coming release, it looks like we 
could can aim at mid June, before or after the isabelle-dev workshop at 
Cambridge.

This means there are about 1-2 weeks left for bigger changes.  Do you 
manage to exchange the reals by then?


> 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?

Making the HOL image smaller (and faster!) is always better than 
continuing the bloat trend in recent years, although it seems only 1% of 
the approx. 100MB of the current image size.

How is the timing for your theories?  Is there an impact on AFP, for 
example.  The latter can be taken as an indication how it will affect 
other users out there.


 	Makarius