Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Period of tangent

Email Gateway (Aug 18 2022 at 12:44):

From: Dominik Luecke <luecke@informatik.uni-bremen.de>
Hello,

the period of the tangent function in HOL-Complex: transcendental is
defined in a too coarse manner as:

lemma tan_periodic [simp]: "tan (x + 2*pi) = tan x"

in fact the period of tangent is pi, which is also provable as:

lemma tan_periodic [simp] : "!! x . tan (x) = tan(x + pi)"
by (simp add: tan_def)

Cheers,
Dominik

Email Gateway (Aug 18 2022 at 12:45):

From: Tobias Nipkow <nipkow@in.tum.de>
We'll add this and more general versions, although in the other
direction to avoid looping.

Thanks
Tobias

Email Gateway (Aug 18 2022 at 12:45):

From: Johannes Hoelzl <johannes.hoelzl@gmx.de>
Hello Dominik,

The following lemmas will be added:

lemma tan_periodic_pi[simp]: "tan (x + pi) = tan x"
lemma tan_periodic_nat[simp]: fixes n :: nat shows "tan (x + real n * pi) = tan x"
lemma tan_periodic_int[simp]: fixes i :: int shows "tan (x + real i * pi) = tan x"
lemma tan_periodic[simp]: "tan (x + number_of n * pi) = tan x"

this should handle nearly all cases.

Johannes

Last updated: May 03 2024 at 04:19 UTC