trig_ineq : THEORY %----------------------------------------------------------------------------- % trig_ineq % --------- % - regions where functions are greater than 0 % - regions where functions are less than 0 % - regions where functions are increasing % - regions where functions are decreasing %----------------------------------------------------------------------------- BEGIN IMPORTING trig_approx a,b : VAR real % ------------------- Sign of sin, cos, and tan ----------------------- sin_gt_0 : LEMMA 0 < a AND a < PI IMPLIES sin(a) > 0 cos_gt_0 : LEMMA -PI/2 < a AND a < PI/2 IMPLIES cos(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_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 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 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 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_PI4_def : LEMMA -PI/4 <= a AND a <= PI/4 IMPLIES Tan?(a) tan_increasing_imp: LEMMA -PI/4 <= a AND a <= PI/4 AND -PI/4 <= b AND b <= PI/4 AND a > b IMPLIES tan(a) > tan(b) tan_increasing : LEMMA -PI/4 <= a AND a <= PI/4 AND -PI/4 <= b AND b <= PI/4 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/4 <= a AND a <= PI/4 AND -PI/4 <= b AND b <= PI/4 IMPLIES (tan(a) >= tan(b) <=> a >= b) END trig_ineq