Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: include Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.