trig_values : THEORY %----------------------------------------------------------------------------- % trig_values Lemma names % ----------- ------------------------------------ % - trig functions at 0 : sin_0 , cos_0 , tan_0 % - trig functions at PI/6 : sin_PI6 , cos_PI6 , tan_PI6 % - trig functions at PI/4 : sin_PI4 , cos_PI4 , tan_PI4 % - trig functions at PI/3 : sin_PI3 , cos_PI3 , tan_PI3 % - trig functions at PI/2 : sin_PI2 , cos_PI2 , tan_PI2 % - trig functions at PI : sin_PI , cos_PI , tan_PI % - trig functions at 2*PI/3 : sin_2PI3 , cos_2PI3 , tan_2PI3 % - trig functions at 3*PI/4 : sin_3PI4 , cos_3PI4 , tan_3PI4 % - trig functions at 5*PI/4 : sin_5PI4 , cos_5PI4 , tan_5PI4 %----------------------------------------------------------------------------- BEGIN IMPORTING trig_ineq a,b : VAR real sin_cos_PI4 : LEMMA sin(PI/4) = cos(PI/4) cos_PI4 : LEMMA cos(PI/4) = 1/sqrt(2) sin_PI4 : LEMMA sin(PI/4) = 1/sqrt(2) cos3PI4 : LEMMA cos(3*PI/4) = - 1/sqrt(2) sin3PI4 : LEMMA sin(3*PI/4) = 1/ sqrt(2) tan_PI4 : LEMMA tan(PI/4) = 1 sin_PI3_cos_PI6 : LEMMA sin(PI/3) = cos(PI/6) sin_PI6_cos_PI3 : LEMMA sin(PI/6) = cos(PI/3) sin_PI6 : LEMMA sin(PI/6) = 1/2 cos_PI6 : LEMMA cos(PI/6) = sqrt(3)/2 tan_PI6 : LEMMA tan(PI/6) = 1/sqrt(3) sin_PI3 : LEMMA sin(PI/3) = sqrt(3)/2 cos_PI3 : LEMMA cos(PI/3) = 1/2 tan_PI3 : LEMMA tan(PI/3) = sqrt(3) sin_2PI3 : LEMMA sin(2*PI/3) = sqrt(3)/2 cos_2PI3 : LEMMA cos(2*PI/3) = -1/2 tan_2PI3 : LEMMA tan(2*PI/3) = -sqrt(3) cos_5PI4 : LEMMA cos(5*PI/4) = - 1/sqrt(2) sin_5PI4 : LEMMA sin(5*PI/4) = - 1/sqrt(2) sin_cos5PI4 : LEMMA sin(5*PI/4) = cos(5*PI/4) % ---------- The following are included for easy reference --------- % They are all from "trig" % cos_0 : AXIOM cos(0) = 1 % sin_0 : LEMMA sin(0) = 0 % sin_PI2 : AXIOM sin(PI/2) = 1 % cos_PI2 : LEMMA cos(PI/2) = 0 % tan_0 : LEMMA tan(0)=0 % sin_PI : LEMMA sin(PI) = 0 % cos_PI : LEMMA cos(PI) = -1 % tan_PI : LEMMA tan(PI) = 0 % sin_3PI2 : LEMMA sin(3*PI/2) = -1 % cos_3PI2 : LEMMA cos(3*PI/2) = 0 % sin_2PI : LEMMA sin(2*PI) = 0 % cos_2PI : LEMMA cos(2*PI) = 1 % tan_2PI : LEMMA tan(2*PI) = 0 END trig_values