Re: [isabelle] Period of tangent



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

Am Mittwoch, den 10.12.2008, 12:29 +0100 schrieb Dominik Luecke:
> 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
> 






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