Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] lots of interesting lemmas in the AFP entr...


view this post on Zulip Email Gateway (Feb 19 2021 at 12:36):

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

view this post on Zulip Email Gateway (Feb 19 2021 at 13:51):

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

smime.p7s

view this post on Zulip Email Gateway (Feb 19 2021 at 14:41):

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

view this post on Zulip Email Gateway (Feb 25 2021 at 16:28):

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: Jul 15 2022 at 23:21 UTC