[isabelle-dev] Reorganising Analysis

[Fabian Immler]

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

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