Quelle  trig_extra.pvs

trig_extra : THEORY
%-----------------------------------------------------------------------------
%      trig_extra
%      ----------
%         - reduction theorems
%         - sum and product identities
%         - half-angle identities and zeros
%         - triple angle formulas
%-----------------------------------------------------------------------------
BEGIN

   IMPORTING trig_basic, trig_values


  a,b             : VAR real

% ------------------------- Reduction Theorems -------------------------

  sin_minus_2pi    : LEMMA sin(a - 2*pi) = sin(a)  
  cos_minus_2pi    : LEMMA cos(a - 2*pi) = cos(a) 
  tan_minus_2pi    : LEMMA cos(a) /= 0 IMPLIES tan(a - 2*pi) = tan(a) 

  sin_minus_3pi2   : LEMMA sin(a - 3*pi/2) =   cos(a)
  cos_minus_3pi2   : LEMMA cos(a - 3*pi/2) = - sin(a)
  tan_minus_3pi2   : LEMMA sin(a) /= 0 AND cos(a) /= 0 
                              IMPLIES tan(a - 3*pi/2) = - 1/tan(a)

  sin_minus_pi     : LEMMA sin(a - pi) = - sin(a)
  cos_minus_pi     : LEMMA cos(a - pi) = - cos(a)
  tan_minus_pi     : LEMMA cos(a) /= 0 IMPLIES tan(a - pi) =   tan(a)

  sin_minus_pi2    : LEMMA sin(a - pi/2) = - cos(a)
  cos_minus_pi2    : LEMMA cos(a - pi/2) =   sin(a)
  tan_minus_pi2    : LEMMA sin(a) /= 0 AND cos(a) /= 0 
                              IMPLIES tan(a - pi/2) = - 1/tan(a)

  sin_2pi_minus    : LEMMA sin(2*pi - a) = - sin(a)
  cos_2pi_minus    : LEMMA cos(2*pi - a) =   cos(a)
  tan_2pi_minus    : LEMMA sin(a) /= 0 AND cos(a) /= 0 
                              IMPLIES tan(2*pi - a) =   - tan(a)
                               
  sin_3pi2_minus   : LEMMA sin(3*pi/2 - a) = - cos(a)
  cos_3pi2_minus   : LEMMA cos(3*pi/2 - a) = - sin(a)
  tan_3pi2_minus   : LEMMA sin(a) /= 0 AND cos(a) /= 0 
                              IMPLIES tan(3*pi/2 - a) =   1/tan(a)
                               
  sin_pi_minus     : LEMMA sin(pi - a) =   sin(a)
  cos_pi_minus     : LEMMA cos(pi - a) = - cos(a)
  tan_pi_minus     : LEMMA cos(a) /= 0 IMPLIES tan(pi - a) = - tan(a)
                               
  sin_pi2_minus    : LEMMA sin(pi/2 - a) = cos(a)
  cos_pi2_minus    : LEMMA cos(pi/2 - a) = sin(a)
  tan_pi2_minus    : LEMMA sin(a) /= 0 AND cos(a) /= 0 
                              IMPLIES tan(pi/2 - a) = 1/tan(a)

% ------------------------- Sum and Product Formulas -------------------------

  sin_times_cos    : LEMMA sin(a)*cos(b) = (sin(a+b) + sin(a-b))/2
  cos_times_cos    : LEMMA cos(a)*cos(b) = (cos(a+b) + cos(a-b))/2
  sin_times_sin    : LEMMA sin(a)*sin(b) = (cos(a-b) - cos(a+b))/2

  sin_sum          : LEMMA sin(a) + sin(b) =   2 * sin((a+b)/2)*cos((a-b)/2)
  sin_diff         : LEMMA sin(a) - sin(b) =   2 * cos((a+b)/2)*sin((a-b)/2)
  cos_sum          : LEMMA cos(a) + cos(b) =   2 * cos((a+b)/2)*cos((a-b)/2)
  cos_diff         : LEMMA cos(a) - cos(b) = - 2 * sin((a+b)/2)*sin((a-b)/2)

  tan_diff         : LEMMA Tan?(a) AND Tan?(b) IMPLIES
                              tan(a) - tan(b) = sin(a-b)/(cos(a)*cos(b))

% ------------------------- Squares of sin and cos -------------------------

  sq_sin           : LEMMA sq(sin(a)) = (1-cos(2*a))/2
  sq_cos           : LEMMA sq(cos(a)) = (1+cos(2*a))/2
  sin_half_zeroes  : LEMMA sin(a/2) = 0 IFF 1-cos(a) = 0
  cos_half_zeroes  : LEMMA cos(a/2) = 0 IFF 1+cos(a) = 0
  cos_half_zeroes2 : LEMMA cos(a/2) = 0 IMPLIES sin(a) = 0
  sq_tan           : LEMMA (1+cos(2*a)) /= 0 
                                IMPLIES sq(tan(a)) = (1-cos(2*a))/(1+cos(2*a))

% ------------------------- Half Angle Formulas -------------------------

  IMPORTING trig_ineq 

  sin_half  : LEMMA 
                ( 0 <= a/2 AND a/2 <= pi IMPLIES
                  sin(a/2) = sqrt((1-cos(a))/2))  AND
                ( pi <= a/2 AND a/2 <= 2*pi IMPLIES
                  sin(a/2) = -sqrt((1-cos(a))/2))

  cos_half  : LEMMA 
                ( 0 <= a/2 AND a/2 <= pi/2 IMPLIES
                  cos(a/2) = sqrt((1+cos(a))/2))  AND
                ( pi/2 <= a/2 AND a/2 <= 3*pi/2 IMPLIES
                  cos(a/2) = -sqrt((1+cos(a))/2)) AND 
                ( 3*pi/2 <= a/2 AND a/2 <= 2*pi IMPLIES
                  cos(a/2) = sqrt((1+cos(a))/2)) 

  tan_half  : LEMMA
                cos(a) /= -1 IMPLIES tan(a/2) = sin(a)/(1 + cos(a)) 

  tan_half2 : LEMMA
                sin(a) /= 0 IMPLIES tan(a/2) = (1 - cos(a))/sin(a)

% ---------------------- Triple Angle Formulas ----------------------

  sin_3a      : LEMMA sin(3*a) = 3 * sin(a) - 4 * expt(sin(a),3)
  cos_3a      : LEMMA cos(3*a) = 4 * expt(cos(a),3) - 3 * cos(a)

% ---------------------- Base equations ---------------------

  sin_eq_sin  : LEMMA sin(a) = sin(b) <=> 
                   (EXISTS (k: int): (a = b + 2*k*pi) OR (a = pi - b + 2*k*pi)) 

  cos_eq_cos  : LEMMA cos(a) = cos(b) <=> 
                   (EXISTS (k: int): (a = b + 2*k*pi) OR (a = -b + 2*k*pi)) 

  tan_eq_tan  : LEMMA Tan?(a) AND Tan?(b) IMPLIES
                      ( tan(a) = tan(b) <=> (EXISTS (k: int): (a = b + k*pi)) )

  sin_cos_eq: LEMMA FORALL (a,b: {x:nnreal | x < 2*pi}): 
                               sin(a) = sin(b) AND cos(a) = cos(b)
                               IMPLIES a = b

  sin_eq_cos: LEMMA sin(a) = cos(a) IMPLIES (EXISTS (i:int): a = pi/4 + i*pi)

  tan_eq_1  : LEMMA Tan?(a) AND tan(a) = 1 IMPLIES (EXISTS (i:int): a = pi/4 + i*pi)


  i,j: VAR integer

  sin_eq_pm1  : LEMMA sin(a) = (-1)^i IFF (EXISTS j: a = (i+2*j)*pi + pi/2)
  cos_eq_pm1  : LEMMA cos(a) = (-1)^i IFF (EXISTS j: a = (i+2*j)*pi)

% --------------------- Superposition ----------------------

  A,B: VAR real
  C: VAR nzreal
  x,y,del,W, alpha: VAR real

  sin_plus_cos: LEMMA sq(C) = sq(A) + sq(B) AND sin(del) = B/C
                        AND cos(del) = A/C  IMPLIES
                        A*sin(x) + B*cos(x) = C*sin(x+del)

  spc_tan_prep: LEMMA A /= 0 AND Tan?(del) AND tan(del) = B/A AND 
                      sq(C) = sq(A) + sq(B) IMPLIES
                         sq(sin(del)) = sq(B/C) AND sq(cos(del)) = sq(A/C)

  IMPORTING atan2

  sin_plus_cos_atan2: LEMMA
     x /= 0 OR y /= 0 IMPLIES
       x*sin(alpha) + y*cos(alpha) = sqrt(sq(x)+sq(y))*sin(alpha + atan2(x,y))


                         

%   sin_superpos: LEMMA A + B*cos(W) = C*cos(del) AND  % need to find f:
%                           B*sin(W) = C*sin(del)      % del = f(A,B,C,W)
%                       IMPLIES
%                           A*sin(x) + B*sin(x+W) = C*sin(x+del)

END trig_extra