Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: trig_extra.prf Sprache: PVS

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

¤ Dauer der Verarbeitung: 0.1 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.