[isabelle-dev] Reorganising Analysis

[Tobias Nipkow]

I am very much in agreement here.

Tobias

On 04/11/2019 19:41, Fabian Immler wrote:
> I just checked: it is easy to remove Path_Connected and Starlike from the 
> imports of Ordered_Euclidean_Space:
> http://isabelle.in.tum.de/repos/testboard/rev/53e22c7bb5f9
> 
> Therefore I would keep Ordered_Euclidean_Space (it fits to the rest of the 
> material in Multivariate_Analysis and is now only 300 lines).
> 
> I might be biased because I never really worked with complex numbers, but I 
> would keep Complex_Transcendental out.
> 
> This is simply because I find it easier to draw the line before complex numbers 
> instead of having to argue which parts of complex analysis should be part of 
> this "Basic Analysis" session and which ones should not (I'd also vote for 
> moving theory Complex out of Complex_Main).
> 
> Fabian
> 
> 
> On 11/4/2019 11:09 AM, Lawrence Paulson wrote:
>> As today, I would suggest omitting Ordered_Euclidean_Space and adding 
>> Complex_Transcendental.
>> Larry
>>
>>> On 4 Nov 2019, at 15:50, Fabian Immler <immler at in.tum.de> wrote:
>>>
>>> In afp-devel/49f30bd (and its parent changesets) Tobias and I experimented 
>>> with reducing the imports of many AFP-entries that build on HOL-Analysis.
>>> We introduced a theory Multivariate_Analysis to collect the theories that we 
>>> deemed "Basic Analysis" material (perhaps Basic_Analysis.thy would be a 
>>> better name).
>>>
>>> Currently (afp/c5c88012f116) we have 20 imports of 
>>> "HOL-Analysis.Multivariate_Analysis", and 35 imports of 
>>> "HOL-Analysis.Analysis", so Multivariate_Analysis seems like a reasonable 
>>> point to split HOL-Analysis.
>>>
>>> The imports of Multivariate_Analysis can (or should) still be refined:
>>> It currently(isa/c85efa2be619) imports Path_Connected and Starlike and I am 
>>> pretty sure much of the material in those theories is not necessary for a 
>>> "Basic Analysis" library.
>>
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5579 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20191104/e3bb2dc6/attachment-0001.bin>