[isabelle-dev] Complex.thy

[Manuel Eberl]

The references to i in Formal_Power_Series are restricted to a very
small and simple (almost trivial) set of theorems that are completely
disconnected from everything else in there. They are about the
relationship between sin, cos, tan, and exp as formal power series and
I'm pretty sure they're not used anywhere in the distribution or the AFP
(a quick grep seems to confirm that). They're certainly relevant, but I
see no problem in moving them somewhere else.

On the other hand, I'm not sure what your exact plans for restructuring
are, but I thought we were going to have some session that contains
complex number and the basic operations on them but not integration.
Then Computational_Algebra could import that. Or perhaps Complex could
import Computational_Algebra (not sure if that makes sense). But as I
said, I also don't see a problem with simply moving those few theorems
out of Formal_Power_Series.

Manuel


On 20/11/2019 16:41, Tobias Nipkow wrote:
>
>
> On 20/11/2019 16:20, Lawrence Paulson wrote:
>> As a small experiment, I tried moving this theory from the main HOL
>> directory to Analysis. I discovered a number of minor, unexpected
>> dependencies:
>>
>> Library/OptionalSugar.thy: There is code to hide coercions, surely
>> unnecessary since we have had implicit coercions for years.
>
> It is necessary because the coercions are printed. But removing the
> complex bits is no problem.
>
>> Library/Nonpos_Ints.thy: There is material relating these primitives
>> to the complex numbers, which could easily be moved to Complex.thy.
>>
>> Computational_Algebra/Formal_Power_Series.thy: There are references
>> to i. These could be harder to deal with.
>>
>> I suppose that we can leave things as they are, but it seems weird to
>> introduce an absolutely minimal signature of the complex numbers in
>> one place and then the basics much later in Analysis.
>
> I would prefer the latter.
>
> Tobias
>
>> Larry
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
>>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20191120/9af3c2d5/attachment.html>