Quelle  trig_ineq.pvs

trig_ineq: THEORY

  BEGIN

  IMPORTING trig_basic

  a,b  : VAR real
  n    : VAR int

% ------------------- Sign of sin, cos, and tan  -----------------------

  cos_gt_0    : AXIOM -pi/2 < a  AND a <  pi/2   IMPLIES cos(a) >  0
  sin_gt_0    : LEMMA 0 < a      AND a <  pi     IMPLIES sin(a) >  0
  sin_ge_0    : LEMMA 0 <= a     AND a <= pi     IMPLIES sin(a) >= 0
  cos_ge_0    : LEMMA -pi/2 <= a AND a <= pi/2   IMPLIES cos(a) >= 0
  sin_lt_0    : LEMMA pi < a     AND a <  2*pi   IMPLIES sin(a) <  0
  cos_lt_0    : LEMMA pi/2 < a   AND a <  3*pi/2 IMPLIES cos(a) <  0
  sin_le_0    : LEMMA pi <= a    AND a <= 2*pi   IMPLIES sin(a) <= 0
  cos_le_0    : LEMMA pi/2 <= a  AND a <= 3*pi/2 IMPLIES cos(a) <= 0
  tan_gt_0    : LEMMA 0 < a      AND a <  pi/2   IMPLIES tan(a) >  0
  tan_lt_0    : LEMMA -pi/2 < a  AND a <  0      IMPLIES tan(a) <  0

  tan_pi2_def   : LEMMA  -pi/2 < a AND a < pi/2   IMPLIES Tan?(a) 
  tan_npi_def   : LEMMA Tan?(n*pi)
  cos_ge_0_3pi2 : LEMMA 3*pi/2 <= a AND a <= 2*pi IMPLIES cos(a) >= 0 

% -------------------- Strict Inequalities --------------------

  sin_increasing_imp : LEMMA
                     a <= pi/2 AND a >= -pi/2 AND
                     b <= pi/2 AND b >= -pi/2 AND
                     a > b 
                     => 
                     sin(a) > sin(b)

  sin_increasing : LEMMA
                     a <= pi/2 AND a >= -pi/2 AND
                     b <= pi/2 AND b >= -pi/2 IMPLIES
                     (sin(a) > sin(b)
                     <=> 
                     a > b)

  sin_decreasing : LEMMA
                     a <= 3*pi/2 AND a >= pi/2 AND
                     b <= 3*pi/2 AND b >= pi/2 IMPLIES
                     (sin(b) > sin(a)
                     <=> 
                     a > b)


  cos_increasing : LEMMA
                     a >= pi AND a <= 2*pi AND
                     b >= pi AND b <= 2*pi IMPLIES
                     (cos(a) > cos(b)
                     <=> 
                     a > b)

  cos_decreasing : LEMMA
                     a <= pi AND a >= 0 AND
                     b <= pi AND b >= 0 IMPLIES
                     (cos(b) > cos(a)
                     <=> 
                     a > b)

  tan_increasing_imp: LEMMA
                      -pi/2 < a AND a < pi/2 AND
                      -pi/2 < b AND b < pi/2 AND
                       a > b IMPLIES
                       tan(a) > tan(b)

  tan_increasing : LEMMA
                     -pi/2 < a AND a < pi/2 AND
                     -pi/2 < b AND b < pi/2 IMPLIES
                         (tan(a) > tan(b) <=> a > b)
                      
% -------------------- Non-Strict Inequalities --------------------

  sin_incr  : LEMMA  a <= pi/2 AND a >= -pi/2 AND
                     b <= pi/2 AND b >= -pi/2 IMPLIES
                     (sin(a) >= sin(b) <=> a >= b)

  sin_decr  : LEMMA  a <= 3*pi/2 AND a >= pi/2 AND
                     b <= 3*pi/2 AND b >= pi/2 IMPLIES
                     (sin(b) >= sin(a) <=> a >= b)

  cos_incr  : LEMMA  a >= pi AND a <= 2*pi AND
                     b >= pi AND b <= 2*pi IMPLIES
                     (cos(a) >= cos(b) <=> a >= b)

  cos_decr  : LEMMA  a <= pi AND a >= 0 AND
                     b <= pi AND b >= 0 IMPLIES
                     (cos(b) >= cos(a) <=> a >= b)

  tan_incr  : LEMMA  -pi/2 < a AND a < pi/2 AND
                     -pi/2 < b AND b < pi/2 IMPLIES
                     (tan(a) >= tan(b) <=> a >= b)

% -------------------- Some properties about sin --------------------

  sin_gt : LEMMA
    -pi/2 <= a AND a < 3*pi/2 AND
    -pi/2 <= b AND b <= pi/2 IMPLIES
   (sin(a) > sin(b) IFF b < a AND a < pi-b)

  sin_lt : LEMMA
    -pi/2 <= a AND a < 3*pi/2 AND
    -pi/2 <= b AND b <= pi/2 IMPLIES
   (sin(a) < sin(b) IFF b > a OR a > pi-b)

  sin_ge : LEMMA
    -pi/2 <= a AND a < 3*pi/2 AND
    -pi/2 <= b AND b <= pi/2 IMPLIES
   (sin(a) >= sin(b) IFF b <= a AND a <= pi-b)


  END trig_ineq