|
%------------------------------------------------------------------------------
% 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
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
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.
|
