[isabelle-dev] HOL vs. HOL-Complex

[Tobias Nipkow]

I don't use Complex, but I strikes me as odd that some of our complex 
theories should be in the HOL image and other should not be. What is the 
rational for splitting something off? Only because it is based on NSA? 
Does a user care how something is defined?

Just wondering.

Tobias

Brian Huffman wrote:
> Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:
> 
>> There is no urgent need that the HOL image contains *all* the
>> HOL-Complex theories.  I also have been thinking about splitting off all
>> the Analysis stuff into a session HOL-Analysis, but on the other hand a
>> lot of functions which you naively expect for reals/complexes (log, ...)
>>  inherently depend on analysis, as far as I understand.
>>
>> 	Florian
> 
> If we all agree that reals and complexes really belong in the main HOL  
> image, then that is a good reason for merging some of HOL-Complex into  
> HOL. I also agree that not *all* of HOL-Complex needs to be in there.
> 
> A good piece to split off would be all of the nonstandard-analysis  
> stuff. Nothing else in HOL-Complex relies on any of the theories below  
> (except that Complex_Main currently imports CLim and Hyperreal, which  
> pulls in everything else).
> 
> Infinite_Set, Zorn, Filter, StarDef, HyperNat, HyperDef, NSA, Star,  
> HLim, NatStar, HSEQ, HDeriv, HSeries, HTranscendental, NSComplex,  
> NSCA, HLog, Hyperreal, CStar, CLim
> 
> It might make sense to split off some other stuff as well, but this  
> would be a good start. If there are no objections, I could go ahead  
> and split these theories myself. A good name might be HOL-NSA (for  
> Non-Standard Analysis). Let me know what you think.
> 
> - Brian
> 
> 
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev