[isabelle-dev] construction of the real numbers
Walther Neuper
neuper at ist.tugraz.at
Mon May 10 09:41:05 CEST 2010
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
More information about the isabelle-dev
mailing list