[isabelle-dev] HOL vs. HOL-Complex
brianh at cs.pdx.edu
Wed Jul 2 18:45:35 CEST 2008
Quoting Makarius <makarius at sketis.net>:
> Does it mean that there is no particular
> advantage in the NSA part anymore, unless you are specifically interested
> in the non-standard thing?
Quoting Lawrence Paulson <lp15 at cam.ac.uk>:
> I see a giant misconception coming. The point of nonstandard analysis
> is that it makes properties of limits, derivatives, and so forth much
> easier to prove than can be done with the standard definitions. They
> eliminate the necessity of arguments involving epsilon and delta. So
> it would be a mistake to imagine that the nonstandard theories are
> only useful for people who are exploring nonstandard analysis. They
> should be valuable to anybody who wants to prove anything in analysis.
> It would be a shame to see them buried somewhere.
Here's how I see it: If all you want to do is *use* analysis (e.g.
maybe you just want to calculate derivatives) then you won't notice
any difference between NSA and standard analysis. The same theorems
have been proved in either version. I expect that the users who
benefit most from having the real number theories in HOL would
generally fall into this camp.
On the other hand, if you want to *prove* things *in* analysis, then
the difference between standard and non-standard is immediately
I wouldn't consider NSA to be "buried" - until very recently, the NSA
theories were located in a logic image separate from the main HOL
image. If we split NSA as I have proposed, then it will be in a logic
image separate from HOL, just as it was before.
More information about the isabelle-dev