Quelle  sincos.pvs

sincos: THEORY

  BEGIN

  IMPORTING reals@quadratic
  IMPORTING trig_basic, analysis@deriv_domain

  AUTO_REWRITE- abs_0
  AUTO_REWRITE- abs_nat

  IMPORTING analysis@deriv_domains

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

  noa_nnreal_lt_pi2     : LEMMA not_one_element?[{x: nnreal | x < pi / 2}]
  noa_real_lt_pi2       : LEMMA not_one_element?[real_abs_lt_pi2]
  noa_posreal_lt_pi     : LEMMA not_one_element?[posreal_lt_pi]
  noa_nnreal_pi4_to_pi  : LEMMA not_one_element?[{x: nnreal | pi / 4 <= x & x < pi}]
  noa_posreal_pi2_to_pi : LEMMA not_one_element?[{x: posreal | pi / 2 <= x & x < pi}]
  noa_nnreal_lt_pi4     : LEMMA not_one_element?[{x: nnreal | x < pi / 4}] 
  noa_mpi4_to_pi4       : LEMMA not_one_element?[{x: real | -pi / 4 < x & x < pi / 4}]

  conn_nnreal_lt_p2     : LEMMA connected?[{x: nnreal | x < pi / 2}]
  conn_nnreal_pi4_to_pi : LEMMA connected?[{x: nnreal | pi / 4 <= x & x < pi}]
  conn_posreal_pi2_to_pi: LEMMA connected?[{x: posreal | pi / 2 <= x & x < pi}]
  conn_nnreal_lt_pi4    : LEMMA connected?[{x: nnreal | x < pi / 4}]

  deriv_domain_nnreal_lt_pi2    : LEMMA deriv_domain?[{x: nnreal | x < pi / 2}]
  deriv_domain_real_abs_lt_pi2  : LEMMA deriv_domain?[real_abs_lt_pi2]
  deriv_domain_posreal_pi2_to_pi: LEMMA deriv_domain?[{x: posreal | pi / 2 <= x & x < pi}]
  deriv_domain_posreal_lt_pi    : LEMMA deriv_domain?[posreal_lt_pi]
  deriv_domain_nnreal_pi4_to_pi : LEMMA deriv_domain?[{x: nnreal | pi / 4 <= x & x < pi}]
  deriv_domain_nnreal_lt_pi4    : LEMMA deriv_domain?[{x: nnreal | x < pi / 4}]
  deriv_domain_mpi4_to_pi4      : LEMMA deriv_domain?[{x: real | -pi / 4 < x & x < pi / 4}]

  AUTO_REWRITE+ noa_nnreal_lt_pi2
  AUTO_REWRITE+ noa_real_lt_pi2  
  AUTO_REWRITE+ noa_posreal_lt_pi    
  AUTO_REWRITE+ noa_nnreal_pi4_to_pi 
  AUTO_REWRITE+ noa_posreal_pi2_to_pi 
  AUTO_REWRITE+ noa_nnreal_lt_pi4
  AUTO_REWRITE+ noa_mpi4_to_pi4   

  AUTO_REWRITE+ conn_nnreal_lt_p2
  AUTO_REWRITE+ conn_nnreal_pi4_to_pi
  AUTO_REWRITE+ conn_posreal_pi2_to_pi
  AUTO_REWRITE+ conn_nnreal_lt_pi4

  AUTO_REWRITE+ deriv_domain_nnreal_lt_pi2
  AUTO_REWRITE+ deriv_domain_real_abs_lt_pi2
  AUTO_REWRITE+ deriv_domain_posreal_pi2_to_pi
  AUTO_REWRITE+ deriv_domain_posreal_lt_pi  
  AUTO_REWRITE+ deriv_domain_nnreal_pi4_to_pi
  AUTO_REWRITE+ deriv_domain_nnreal_lt_pi4 
  AUTO_REWRITE+ deriv_domain_mpi4_to_pi4




  cos_ub: LEMMA cos(x)        <= 1
  sin_ub: LEMMA sin(px)       <  px
  cos_lb: LEMMA 1-px*px/2     <  cos(px)
  sin_lb: LEMMA 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_convergence  : LEMMA convergence(NQ(sin,x),0,cos(x))
  sin_derivable    : LEMMA derivable?(sin,x)
  sin_derivable_fun: LEMMA derivable?(sin)
  deriv_sin_fun    : LEMMA deriv(sin) = cos

  cos_convergence  : LEMMA convergence(NQ(cos,x),0,-sin(x))
  cos_derivable    : LEMMA derivable?(cos,x)
  cos_derivable_fun: LEMMA derivable?(cos)
  deriv_cos_fun    : LEMMA deriv(cos) = -sin

  sin_continuous   : LEMMA continuous?(sin,x0)
  cos_continuous   : LEMMA continuous?(cos,x0)
  sin_cont_fun     : LEMMA continuous?(sin)
  cos_cont_fun     : LEMMA continuous?(cos)

  nderiv_sin_fun:  LEMMA derivable_n_times?(sin,n) AND
                         nderiv(n,sin) = LAMBDA (x:real): sin((n*pi/2)+x)
  nderiv_cos_fun:  LEMMA derivable_n_times?(cos,n) AND
                         nderiv(n,cos) = LAMBDA (x:real): cos((n*pi/2)+x)

  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_taylors: LEMMA (EXISTS (c: between(0,x)): 
    sin(x) = sin_series_n(x,n)+nderiv(2*n+3,sin)(c)*x^(2*n+3)/factorial(2*n+3))

  cos_taylors: LEMMA (EXISTS (c: between(0,x)): 
    cos(x) = cos_series_n(x,n)+nderiv(2*n+2,cos)(c)*x^(2*n+2)/factorial(2*n+2))

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


  END sincos