sincos_def.pvs

sincos_def: THEORY
BEGIN

  IMPORTING reals@quadratic, reals@factorial, reals@sigma_nat
  IMPORTING trig_basic, taylor_help[real]

  x,x0:  VAR real
  px:    VAR posreal
  n:     VAR nat

  cos_ub: LEMMA cos(x)        <= 1
  sin_ub: AXIOM sin(px)       <  px
  cos_lb: AXIOM 1-px*px/2     <  cos(px)
  sin_lb: AXIOM px-px*px*px/6 <  sin(px)

  cos_pos_bnds:    LEMMA 1-px*px/2     < cos(px) AND cos(px) <= 1
  sin_pos_bnds:    LEMMA px-px*px*px/6 < sin(px) AND sin(px) <  px


  sin_series_term(x:real):[nat->real]
    = (LAMBDA (n:nat): (-1)^n*x^(2*n+1)/factorial(2*n+1))

  sin_series_n(x:real,n:nat):real
    = sigma(0,n,LAMBDA (i:nat): IF i>n THEN 0 ELSE sin_series_term(x)(i) ENDIF)

  cos_series_term(x:real):[nat->real]
    = (LAMBDA (n:nat): IF n=0 THEN 1 ELSE (-1)^n*x^(2*n)/factorial(2*n) ENDIF)

  cos_series_n(x:real,n:nat):real
    = sigma(0,n,LAMBDA (i:nat): IF i>n THEN 0 ELSE cos_series_term(x)(i) ENDIF)

  sin_series: AXIOM abs(sin(x)-sin_series_n(x,n))
                      <= abs(x^(2*n+3))/factorial(2*n+3)
  cos_series: AXIOM abs(cos(x)-cos_series_n(x,n))
                      <= abs(x^(2*n+2))/factorial(2*n+2)

  % THE FOLLOWING ARE IMPORTED TO MATCH trig_fnd
  IMPORTING asin, acos, atan
  a: VAR real

  sin_asin: AXIOM FORALL (x: trig_range): sin(asin(x)) = x
  cos_acos: AXIOM FORALL (x: trig_range): cos(acos(x)) = x
  tan_atan: AXIOM FORALL (x: trig_range): tan(atan(a)) = a

  asin_sin: AXIOM FORALL (x:real_abs_le_pi2): asin(sin(x)) = x
  acos_cos: AXIOM FORALL (x:nnreal_le_pi):   acos(cos(x)) = x
  atan_tan: AXIOM FORALL (x:real_abs_lt_pi2): atan(tan(x)) = x


END sincos_def