From: Lawrence Paulson <lp15@cam.ac.uk>

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?

Larry

isabelle-dev mailing list

isabelle-dev@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

From: Tobias Nipkow <nipkow@in.tum.de>

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@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

From: Manuel Eberl <eberlm@in.tum.de>

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

smime.p7s

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>

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

signature.asc

Last updated: Mar 04 2024 at 12:30 UTC