sincos_phase: THEORY
%------------------------------------------------------------------------------
%
%  Definitions of sin and cos from infinite series
%
%          David Lester                    Manchester University
% 
%------------------------------------------------------------------------------

  BEGIN

  IMPORTING sincos_quad

  trig_phase: NONEMPTY_TYPE = {x:nnreal| x < 2*pi} CONTAINING 0

  x,y:   VAR trig_phase
  px,py: VAR {x:posreal| x < 2*pi}
  xa:    VAR real_abs_le1
  
% Principle Phase [0,2*pi)
  sin_phase(x:trig_phase):real_abs_le1
     = LET   i = floor((2*x)/pi) IN
       IF    i = 0 THEN  sin_value(x)
       ELSIF i = 1 THEN  sin_value(pi-x)
       ELSIF i = 2 THEN -sin_value(x-pi)
                   ELSE -sin_value(2*pi-x)
       ENDIF

  cos_phase(x:trig_phase):real_abs_le1
     = LET i = floor(x/pi) IN
       IF i = 0 THEN cos_value(x) ELSE cos_value(2*pi-x) ENDIF

  phase_sin_q1: LEMMA floor((2*x)/pi) = 0 IFF 0 <= x      AND x < pi/2
  phase_sin_q2: LEMMA floor((2*x)/pi) = 1 IFF pi/2 <= x   AND x < pi
  phase_sin_q3: LEMMA floor((2*x)/pi) = 2 IFF pi <= x     AND x < 3*pi/2
  phase_sin_q4: LEMMA floor((2*x)/pi) = 3 IFF 3*pi/2 <= x AND x < 2*pi

  phases_sin:   LEMMA floor((2*x)/pi) = 0 OR floor((2*x)/pi) = 1 OR 
                      floor((2*x)/pi) = 2 OR floor((2*x)/pi) = 3

  sin_q1: LEMMA floor((2*x)/pi) = 0 => sin_phase(x) =  sin_value(x)
  sin_q2: LEMMA floor((2*x)/pi) = 1 => sin_phase(x) =  cos_value(x-pi/2)
  sin_q3: LEMMA floor((2*x)/pi) = 2 => sin_phase(x) = -sin_value(x-pi)
  sin_q4: LEMMA floor((2*x)/pi) = 3 => sin_phase(x) = -cos_value(x-3*pi/2)

  phase_cos_q1: LEMMA floor(x/pi) = 0 IFF 0  <= x AND x < pi
  phase_cos_q2: LEMMA floor(x/pi) = 1 IFF pi <= x AND x < 2*pi

  phases_cos:   LEMMA floor(x/pi) = 0 OR floor(x/pi) = 1

  cos_q1: LEMMA floor((2*x)/pi) = 0 => cos_phase(x) =  cos_value(x)
  cos_q2: LEMMA floor((2*x)/pi) = 1 => cos_phase(x) = -sin_value(x-pi/2)
  cos_q3: LEMMA floor((2*x)/pi) = 2 => cos_phase(x) = -cos_value(x-pi)
  cos_q4: LEMMA floor((2*x)/pi) = 3 => cos_phase(x) =  sin_value(x-3*pi/2)

  sin_h2: LEMMA floor(x/pi) = 1 => sin_phase(x) = -sin_phase(x-pi)
  sin_h1: LEMMA floor(x/pi) = 0 => sin_phase(x) = -sin_phase(x+pi)
  cos_h1: LEMMA floor(x/pi) = 0 => cos_phase(x) = -cos_phase(x+pi)
  cos_h2: LEMMA floor(x/pi) = 1 => cos_phase(x) = -cos_phase(x-pi)

  sin_phase_neg:       LEMMA sin_phase(2*pi-px) = -sin_phase(px)
  cos_phase_neg:       LEMMA cos_phase(2*pi-px) =  cos_phase(px)
  sin_eqv_cos_phase:   LEMMA
    sin_phase(x) = IF x < 3*pi/2 THEN -cos_phase(pi/2+x)
                                 ELSE -cos_phase(x-3*pi/2) ENDIF
  cos_eqv_sin_phase:   LEMMA
    cos_phase(x) = IF x < 3*pi/2 THEN sin_phase(pi/2+x)
                                 ELSE sin_phase(x-3*pi/2) ENDIF
  sin_phase_inv:       LEMMA
    sin_phase(x) = IF x < pi THEN -sin_phase(x+pi) ELSE -sin_phase(x-pi) ENDIF
  cos_phase_inv:       LEMMA
    cos_phase(x) = IF x < pi THEN -cos_phase(x+pi) ELSE -cos_phase(x-pi) ENDIF
  sin_phase_3pi2:      LEMMA sin_phase(3*pi/2) = -1
  sin_phase_0:         LEMMA sin_phase(0)      =  0
  sin_phase_pi4:       LEMMA sin_phase(pi/4)   =  sqrt(1/2)
  sin_phase_pi2:       LEMMA sin_phase(pi/2)   =  1
  cos_phase_0:         LEMMA cos_phase(0)      =  1
  cos_phase_pi4:       LEMMA cos_phase(pi/4)   =  sqrt(1/2)
  cos_phase_pi2:       LEMMA cos_phase(pi/2)   =  0
  cos_phase_pi:        LEMMA cos_phase(pi)     = -1

  sin_phase_asin:      LEMMA IF xa < 0 THEN sin_phase(asin(xa)+2*pi)
                                       ELSE sin_phase(asin(xa)) ENDIF = xa
  cos_phase_acos:      LEMMA cos_phase(acos(xa)) = xa

  sin2_cos2_phase:     LEMMA sq(sin_phase(x))+sq(cos_phase(x)) = 1

  sin_phase_diff: LEMMA sin_phase(x)*cos_phase(y)-cos_phase(x)*sin_phase(y)
     = IF x-y >= 0   THEN sin_phase(x-y) ELSE sin_phase(x-y+2*pi) ENDIF

  cos_phase_sum:  LEMMA cos_phase(x)*cos_phase(y)-sin_phase(x)*sin_phase(y)
     = IF x+y < 2*pi THEN cos_phase(x+y) ELSE cos_phase(x+y-2*pi) ENDIF 

  cos_phase_diff:  LEMMA cos_phase(x)*cos_phase(y)+sin_phase(x)*sin_phase(y)
     = IF x-y >= 0   THEN cos_phase(x-y) ELSE cos_phase(x-y+2*pi) ENDIF 

  sin_phase_sum:  LEMMA sin_phase(x)*cos_phase(y)+cos_phase(x)*sin_phase(y)
     = IF x+y < 2*pi THEN sin_phase(x+y) ELSE sin_phase(x+y-2*pi) ENDIF

  END sincos_phase