[isabelle-dev] Reorganising Analysis

[Fabian Immler]

On 11/4/2019 7:44 AM, Lawrence Paulson wrote:
> Then the obvious stopping point is one line above: Derivative.
Yes (with some additional theories):

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.

Fabian


> The problem at the moment with basing a development around the Cauchy integral theorem is that you might also  want to include Winding_Numbers, but that theory inherits almost the whole of Analysis: even the Jordan curve theorem.
> 
> Larry
> 
>> On 4 Nov 2019, at 12:19, Manuel Eberl <eberlm at in.tum.de> wrote:
>>
>> Great work, thanks for taking care of this!
>>
>> Just abstractly speaking, it would seem very odd to me to have a "complex analysis" directory without integration. Complex integration and the Cauchy integral formula are such basic tools in complex analysis that not including them in a "complex analysis" entry would seem… unusual to me.
>>
>> Perhaps "complex analysis prerequisites".
>>
> 

-------------- 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/0bc42468/attachment-0001.bin>