Quelle sincosx.pvs Sprache: PVS

%------------------------------------------------------------------------------
% sin/cos
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            18/2/09   Initial Release Version
%------------------------------------------------------------------------------

sincosx: THEORY

BEGIN

  IMPORTING prelude_aux, atanx, trig_fnd@sincos, trig_fnd@trig_values,
            reals@factorial_props, trig_fnd@trig_approx, remx

  n,p: VAR nat
  x:   VAR real
  cx:  VAR cauchy_real

  real_3pi16: TYPE+ = {x | -3*pi/16 < x & x < 3*pi/16} CONTAINING 0

  cauchy_real_3pi16?(c:[nat->int]):bool
                                    =EXISTS (x:real_3pi16): cauchy_prop(x,c)

  cauchy_real_3pi16: TYPE+=(cauchy_real_3pi16?) CONTAINING (LAMBDA p:0)

  nnsreal: TYPE+ = {x | 0 <= x & x < 1/2} CONTAINING 0

  cauchy_nnsreal?(c:[nat->int]):bool = EXISTS (x:nnsreal): cauchy_prop(x,c)

  cauchy_nnsreal: TYPE+=(cauchy_nnsreal?) CONTAINING (LAMBDA p:0)

  JUDGEMENT nnsreal           SUBTYPE_OF nnreal
  JUDGEMENT cauchy_nnsreal    SUBTYPE_OF cauchy_real
  JUDGEMENT cauchy_real_3pi16 SUBTYPE_OF cauchy_real

  sx:   VAR real_3pi16
  snx:  VAR nnsreal
  csx:  VAR cauchy_real_3pi16
  ssx:  VAR ssmallreal
  cssx: VAR cauchy_ssmallreal
  csnx: VAR cauchy_nnsreal

  cauchy_sin_series(n):cauchy_real
    = cauchy_div(cauchy_int((-1)^n),cauchy_int(factorial(2*n+1)))

  cauchy_cos_series(n):cauchy_real
    = cauchy_div(cauchy_int((-1)^n),cauchy_int(factorial(2*n)))

  sin_series_lemma: LEMMA cauchy_prop(sin_term(1)(n), cauchy_sin_series(n))

  cos_series_lemma: LEMMA cauchy_prop(cos_term(1)(n), cauchy_cos_series(n))

  cauchy_sin_drx(csnx): cauchy_real
    = (LAMBDA p: round(cauchy_powerseries(csnx,cauchy_sin_series,p+2)(p+2)/4))

  cauchy_cos_drx(csnx): cauchy_real
    = (LAMBDA p: round(cauchy_powerseries(csnx,cauchy_cos_series,p+2)(p+2)/4))

  sin_drx_lemma: LEMMA cauchy_prop(snx,csnx) AND snx /= 0 =>
                cauchy_prop(sin(sqrt(snx))/sqrt(snx),cauchy_sin_drx(csnx))

  cauchy_sin_dr(csx): cauchy_real
    = cauchy_mul(csx,cauchy_sin_drx(cauchy_mul(csx,csx)))

  cauchy_cos_dr(csx): cauchy_real = cauchy_cos_drx(cauchy_mul(csx,csx))

  sin_dr_lemma: LEMMA cauchy_prop(sx,csx) =>
                      cauchy_prop(sin(sx),cauchy_sin_dr(csx))

  cos_dr_lemma: LEMMA cauchy_prop(sx,csx) =>
                      cauchy_prop(cos(sx),cauchy_cos_dr(csx))

  cauchy_sin(cx): cauchy_real
    = LET p2  = cauchy_div2n(cauchy_pi,2),
          s2  = cauchy_sqrt(cauchy_div2n(cauchy_int(1),1)),
          s   = round(cauchy_div(cx,p2)(2)/4),
          n   = remx(8)(s),
          cy  = cauchy_sub(cx, cauchy_mul(p2, cauchy_int(s))),
          sin = cauchy_sin_dr(cy),
          cos = cauchy_cos_dr(cy)
      IN IF    n = 0 THEN sin
         ELSIF n = 1 THEN cauchy_mul(s2, cauchy_add(cos, sin))
         ELSIF n = 2 THEN cos
         ELSIF n = 3 THEN cauchy_mul(s2, cauchy_sub(cos, sin))
         ELSIF n = 4 THEN cauchy_neg(sin)
         ELSIF n = 5 THEN cauchy_neg(cauchy_mul(s2, cauchy_add(cos, sin)))
         ELSIF n = 6 THEN cauchy_neg(cos)
                     ELSE cauchy_neg(cauchy_mul(s2, cauchy_sub(cos, sin)))
         ENDIF

  sin_lemma: LEMMA cauchy_prop(x,cx) => cauchy_prop(sin(x),cauchy_sin(cx))

  cauchy_cos(cx): cauchy_real
    = LET p2  = cauchy_div2n(cauchy_pi,2),
          s2  = cauchy_sqrt(cauchy_div2n(cauchy_int(1),1)),
          s   = round(cauchy_div(cx,p2)(2)/4),
          n   = remx(8)(s),
          cy  = cauchy_sub(cx, cauchy_mul(p2, cauchy_int(s))),
          sin = cauchy_sin_dr(cy),
          cos = cauchy_cos_dr(cy)
      IN IF    n = 0 THEN cos
         ELSIF n = 1 THEN cauchy_mul(s2, cauchy_sub(cos, sin))
         ELSIF n = 2 THEN cauchy_neg(sin)
         ELSIF n = 3 THEN cauchy_neg(cauchy_mul(s2, cauchy_add(cos, sin)))
         ELSIF n = 4 THEN cauchy_neg(cos)
         ELSIF n = 5 THEN cauchy_neg(cauchy_mul(s2, cauchy_sub(cos, sin)))
         ELSIF n = 6 THEN sin
                     ELSE cauchy_mul(s2, cauchy_add(cos, sin))
         ENDIF

  cos_lemma: LEMMA cauchy_prop(x,cx) => cauchy_prop(cos(x),cauchy_cos(cx))

END sincosx

quality93%

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.