Quelle log.pvs Sprache: PVS

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

log: THEORY

BEGIN

  IMPORTING prelude_aux, cauchy, add, sub, neg, int, inv, mul, div, shift,
            sqrtx, powerseries, lnexp_fnd@ln_exp, lnexp_fnd@ln_exp_series_alt

  x:   VAR real
  c:   VAR [nat->int]
  n,p: VAR nat

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

  cauchy_ln_small?(c):bool = EXISTS (x:ln_smallreal): cauchy_prop(x,c)

  cauchy_ln_small: TYPE+ = (cauchy_ln_small?) CONTAINING cauchy_int(0)

  JUDGEMENT cauchy_ln_small SUBTYPE_OF cauchy_real

  ln_medreal: TYPE+ = {x | 1/4 <= x & x <= 9/4} CONTAINING 1

  cauchy_ln_med?(c):bool = EXISTS (x:ln_medreal): cauchy_prop(x,c)

  cauchy_ln_med: TYPE+ = (cauchy_ln_med?) CONTAINING cauchy_int(1)

  JUDGEMENT cauchy_ln_med SUBTYPE_OF cauchy_posreal

  posreal_gt_quarter: TYPE+ = {x | 1/4 < x} CONTAINING 1

  cauchy_gt_quarter?(c):bool = EXISTS (x:posreal_gt_quarter): cauchy_prop(x,c)

  cauchy_gt_quarter: TYPE+ = (cauchy_gt_quarter?) CONTAINING cauchy_int(1)

  JUDGEMENT cauchy_gt_quarter SUBTYPE_OF cauchy_posreal

  ssx:    VAR ln_smallreal
  cssx:   VAR cauchy_ln_small
  mx:     VAR ln_medreal
  cmx:    VAR cauchy_ln_med
  gt_14:  VAR posreal_gt_quarter
  cgt_14: VAR cauchy_gt_quarter
  px:     VAR posreal
  pcx:    VAR cauchy_posreal

  cauchy_ln_series(n:nat): cauchy_real
    = IF    n = 0    THEN cauchy_zero
      ELSIF even?(n) THEN cauchy_div(cauchy_int(-1),cauchy_int(n))
                     ELSE cauchy_div(cauchy_int( 1),cauchy_int(n)) ENDIF

  ln_series_lemma: LEMMA
    cauchy_prop(IF n = 0 THEN 0 ELSE lnT(1)(n-1) ENDIF, cauchy_ln_series(n))

  ln_estimate_lemma:
    LEMMA cauchy_prop(ssx,cssx) =>
          cauchy_prop(ln_estimate(ssx,n),
                      cauchy_powerseries(cssx,cauchy_ln_series,n))

  cauchy_ln_drx(cssx)(p):int
   = round(cauchy_powerseries(cssx,cauchy_ln_series,p+2)(p+2)/4)

  ln_drx_lemma: LEMMA cauchy_prop(ssx,cssx) =>
                      cauchy_prop(ln(1+ssx),cauchy_ln_drx(cssx))

  JUDGEMENT cauchy_ln_drx(cssx) HAS_TYPE cauchy_real

  cauchy_ln_half:cauchy_negreal
   = cauchy_ln_drx(cauchy_neg(cauchy_div2n(cauchy_int(1),1)))

  cauchy_ln_half_lemma: LEMMA cauchy_prop(ln(1/2),cauchy_ln_half)

  cauchy_ln2:cauchy_posreal = cauchy_neg(cauchy_ln_half)

  cauchy_ln2_lemma: LEMMA cauchy_prop(ln(2),cauchy_ln2)

  cauchy_ln_sqrt2:cauchy_posreal = cauchy_div2n(cauchy_ln2,1)

  cauchy_ln_sqrt2_lemma: LEMMA cauchy_prop(ln(sqrt(2)),cauchy_ln_sqrt2)

  cauchy_ln_dr(cmx):cauchy_real
   = IF   3 <= cmx(2) AND cmx(2) <= 5
     THEN cauchy_ln_drx(cauchy_sub(cmx,cauchy_int(1)))
     ELSE cauchy_mul2n(
              cauchy_ln_drx(cauchy_sub(cauchy_sqrt(cmx),cauchy_int(1))),1)
     ENDIF

  ln_dr_lemma: LEMMA cauchy_prop(mx,cmx) =>
                     cauchy_prop(ln(mx),cauchy_ln_dr(cmx))

  cauchy_lnx(cgt_14):[nat->int]
   = LET t = cgt_14(2) IN
     IF t <= 8 THEN cauchy_ln_dr(cgt_14) ELSE
        LET n = floor_log2(t) - 1 IN
            cauchy_add(cauchy_ln_dr(cauchy_div2n(cgt_14,n)),
                       cauchy_mul(cauchy_int(n),cauchy_ln2))
     ENDIF

  ln_lemma_x: LEMMA cauchy_prop(gt_14,cgt_14) =>
                        cauchy_prop(ln(gt_14),cauchy_lnx(cgt_14))

  JUDGEMENT cauchy_lnx(cgt_14) HAS_TYPE cauchy_real

  cauchy_ln(pcx):cauchy_real
   = IF pcx(2) <= 2 THEN cauchy_neg(cauchy_lnx(cauchy_inv(pcx)))
                    ELSE cauchy_lnx(pcx) ENDIF

  ln_lemma: LEMMA cauchy_prop(px,pcx) => cauchy_prop(ln(px),cauchy_ln(pcx))

END log

quality98%

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