Email Gateway (Feb 19 2021 at 12:36): 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
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
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
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: Dec 21 2024 at 16:20 UTC