[isabelle-dev] construction of the real numbers

[Walther Neuper]

Brian,

thank your for the re-formalization of real numbers. This kind of work 
is important when computer theorem proving is going to pervade "real 
world" engineering applications. In these applications efficiency is an 
issue, and many users will appreciate short code and image size.

A comment you ask for: Your assumption, that "users should not need to 
know or care which construction of reals we use", does not apply in 
education.

There are several attempts to design educational software for ("pure" 
and "applied") mathematics, which is _transparent_ in the sense, that 
the learner can access any knowledge underlying a particular calculation.
For instance, coming accross "2*pi" in some calculation, a learner (and 
probably a philosopher) might be interested, how "2 times (something) 
infinite" can be regarded the same as "(something) infinite times 2", 
i.e. "pi*2". Smart students ask questions like this, and smart 
educational software should answer such questions.

This comment is no objection, since the majority of users of (embedded 
functionality of) Isabelle will be engineers sooner or later, and not 
students (at least I hope so ;-)!

Walther

PS: In Austria we have special courses at high-schools which use 
Dedekind cuts. However, there are teachers which prefer "Intervall- 
Schachtelungen" which would be closer to Cauchy sequences.
-- 
------------------------------------------------------------------------
Walther Neuper                          Mailto: neuper at ist.tugraz.at
Institute for Software Technology          Tel: +43-(0)316/873-5728
University of Technology                   Fax: +43-(0)316/873-5706
Graz, Austria                             Home: www.ist.tugraz.at/neuper
------------------------------------------------------------------------
Brian Huffman wrote:
> Hello all,
> 
> 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?
> 
> - Brian
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev