[isabelle-dev] Reorganising Analysis

[Manuel Eberl]

On 04/11/2019 19:41, Fabian Immler wrote:
> I might be biased because I never really worked with complex numbers,
> but I would keep Complex_Transcendental out.

I have been working with complex numbers a lot and think they are the
best thing ever, but I don't object. If a clean separation can be made,
I don't see why we shouldn't make it there.

The downside would be that e.g. the Gamma function would not be
available in this "reduced" Analysis image.


> 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

The obvious choice would be: all the complex analogues of standard real
operations (exp, ln, sin, cos, tan) and the most basic operations (cis,
Arg). Possibly the Gamma function. But nothing that involves
integration. (Gamma_Function contains a few things using integrals, but
I think those can easily be pulled out)


> I'd also vote for moving theory Complex out of Complex_Main

That probably makes a lot of sense in any case.

Manuel