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

[Florian Haftmann]

>> 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.

Some AFP contributors hold to the convention to place generic lemmas
into More_*-Theories, e. g.

> /srv/data/tum/afp/master/thys/Dirichlet_Series/More_Totient.thy
> /srv/data/tum/afp/master/thys/Subresultants/More_Homomorphisms.thy
> /srv/data/tum/afp/master/thys/Count_Complex_Roots/More_Polynomials.thy
> /srv/data/tum/afp/master/thys/Isabelle_Marries_Dirac/More_Tensor.thy
> /srv/data/tum/afp/master/thys/Groebner_Bases/More_MPoly_Type_Class.thy
> /srv/data/tum/afp/master/thys/Polynomials/More_Modules.thy
> /srv/data/tum/afp/master/thys/Polynomials/More_MPoly_Type.thy
> /srv/data/tum/afp/master/thys/PAC_Checker/More_Loops.thy
> /srv/data/tum/afp/master/thys/Prime_Distribution_Elementary/More_Dirichlet_Misc.thy
> /srv/data/tum/afp/master/thys/Ribbon_Proofs/More_Finite_Map.thy
> /srv/data/tum/afp/master/thys/Stateful_Protocol_Composition_and_Typing/More_Unification.thy
> /srv/data/tum/afp/master/thys/Linear_Programming/More_Jordan_Normal_Forms.thy
> /srv/data/tum/afp/master/thys/Relational_Paths/More_Relation_Algebra.thy
> /srv/data/tum/afp/master/thys/Relation_Algebra/More_Boolean_Algebra.thy
> /srv/data/tum/afp/master/thys/Probabilistic_Timed_Automata/library/More_List.thy
> /srv/data/tum/afp/master/thys/LLL_Basis_Reduction/More_IArray.thy
> /srv/data/tum/afp/master/thys/Signature_Groebner/More_MPoly.thy
> /srv/data/tum/afp/master/thys/Complex_Geometry/More_Set.thy
> /srv/data/tum/afp/master/thys/Complex_Geometry/More_Transcendental.thy
> /srv/data/tum/afp/master/thys/Complex_Geometry/More_Complex.thy

I guess these are worth candidates for exploring.

Cheers,
	Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20210225/5f276be4/attachment.sig>