[isabelle-dev] HOL vs. HOL-Complex

[Brian Huffman]

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  
apparent.

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.

- Brian