[isabelle-dev] lots of interesting lemmas in the AFP entry Complex_Geometry

[Manuel Eberl]

Note that I set up something to deal with this (periodicity of
sin/cos/etc) in HOL-Library.Periodic_Fun.

I have some plans for making a simproc to deal with the obvious cases
automatically, but so far I have not found a suitable student to
implement it.

Manuel

On 19/02/2021 14:51, Tobias Nipkow wrote:
>
>
> On 19/02/2021 13:35, Lawrence Paulson wrote:
>> It’s common for AFP entries to include theories with names such as
>> T_extras, extending some theory T. Sometimes they look interesting.
>> The entry Complex_Geometry has quite a few of such theories. For
>> example, More_Transcendental contains a lot of facts about sines and
>> cosines, such as the following:
>>
>> lemma cos_periodic_int [simp]:
>>    fixes i :: int
>>    shows "cos (x + i * (2 * pi)) = cos x”
>>
>> Should we from time to time seek to import some of this material?
>
> If you can spare the time, by all means.
>
> 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/20210219/0c298677/attachment-0001.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5574 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20210219/0c298677/attachment-0001.bin>