SSL exp.pvs   Interaktion und
PortierbarkeitPVS

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

exp: THEORY

BEGIN

  IMPORTING prelude_aux, cauchy, inv, int, shift, powerseries, log,
            reals@factorial, lnexp_fnd@ln_exp, lnexp_fnd@ln_exp_series_alt,
            lnexp_fnd@ln_approx

  n,p: VAR nat
  x:   VAR real
  cx:  VAR cauchy_real
  sx:  VAR smallreal
  csx: VAR cauchy_smallreal

  cauchy_exp_series(n): cauchy_nnreal = cauchy_inv(cauchy_int(factorial(n)))

  exp_series_lemma: LEMMA cauchy_prop(expT(1)(n), cauchy_exp_series(n))

  exp_estimate_lemma:
    LEMMA cauchy_prop(x,cx) =>
          cauchy_prop(exp_estimate(x,n),
                      cauchy_powerseries(cx,cauchy_exp_series,n))

  cauchy_exp_dr(csx)(p):int
    = round(cauchy_powerseries(csx,cauchy_exp_series,p+3)(p+2)/4)

  exp_dr_lemma: LEMMA cauchy_prop(sx,csx) =>
                      cauchy_prop(exp(sx),cauchy_exp_dr(csx))

  JUDGEMENT cauchy_exp_dr(csx) HAS_TYPE cauchy_posreal

  cauchy_exp(cx):[nat->int]
    = LET n  = cauchy_div(cx,cauchy_ln2)(0),
          cy = cauchy_sub(cx,cauchy_mul(cauchy_int(n),cauchy_ln2))
      IN IF    n < 0 THEN cauchy_div2n(cauchy_exp_dr(cy),-n)
         ELSIF n > 0 THEN cauchy_mul2n(cauchy_exp_dr(cy),n)
                     ELSE cauchy_exp_dr(cy) ENDIF

  exp_lemma: LEMMA cauchy_prop(x,cx) => cauchy_prop(exp(x),cauchy_exp(cx))

  cauchy_exp_is_posreal: JUDGEMENT cauchy_exp(cx) HAS_TYPE cauchy_posreal

END exp