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 
%
%      Version 1.1 Foundational (DRL) 27/10/03
%
%-----------------------------------------------------------------------------
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)
  cos_3pi4    : LEMMA cos(3*pi/4) = - 1/sqrt(2) 
  sin_3pi4    : 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_cos_5pi4 : LEMMA sin(5*pi/4) = cos(5*pi/4)

% ---------- The following are included for easy reference ---------
%            They are all from "trig"            

%  cos_0       : LEMMA cos(0) = 1 
%  sin_0       : LEMMA sin(0) = 0
%  sin_pi2     : LEMMA 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