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. LarryOn 4 Nov 2019, at 12:19, Manuel Eberl <[email protected]> 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".
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
