[isabelle] Period of tangent


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)


Dominik Luecke                 Phone +49-421-218-64265
Dept. of Computer Science      Fax   +49-421-218-9864265
University of Bremen           luecke at informatik.uni-bremen.de
P.O.Box 330440, D-28334 Bremen
PGP-Key ID 0x766B1F6B

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.