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 >> [email protected] >> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev >> > > > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
