|
%% interval_lnexp.pvs
interval_lnexp : THEORY
BEGIN
IMPORTING lnexp_fnd@exp_approx,
lnexp_fnd@ln_approx,
interval
X,Y : VAR Interval
x : VAR real
n : VAR nat
Exp(n)(X) : (Pos?) =
[|exp_lb(lb(X),n),exp_ub(ub(X),n)|]
Exp_fundamental: LEMMA
X << Y IMPLIES
Exp(n)(X) << Exp(n)(Y)
Ln(n)(X) : Interval =
if lb(X) > 0 AND ub(X) > 0 then
[|ln_lb(lb(X),n),ln_ub(ub(X),n)|]
else
EmptyInterval
endif
% lemmas
Ln_fundamental: LEMMA
Pos?(Y) AND Proper?(X) AND
X << Y IMPLIES
Ln(n)(X) << Ln(n)(Y)
Exp_inclusion : LEMMA
x ## X IMPLIES
exp(x) ## Exp(n)(X)
% En
En(n) : (Pos?) = Exp(n)([|1|])
Ln_inclusion : LEMMA
Pos?(X) AND
x ## X IMPLIES
ln(x) ## Ln(n)(X)
%% Safe version of ln and exp
IMPORTING safe_arith
safe_Ln(n) : [Interval->Interval] = Safe1(Ln(n))
safe_Exp(n) : [Interval->Interval] = Safe1(Exp(n))
%% Proper version of ln and exp
IMPORTING proper_arith
Xp : VAR ProperInterval
XP : VAR PosInterval
Proper_Ln : JUDGEMENT
Ln(n)(XP) HAS_TYPE ProperInterval
Proper_Exp : JUDGEMENT
Exp(n)(Xp) HAS_TYPE ProperInterval
proper_Ln(n)(XP) : ProperInterval = Ln(n)(XP)
proper_Exp(n)(Xp) : PosInterval = Exp(n)(Xp)
END interval_lnexp
¤ Dauer der Verarbeitung: 0.18 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.
|
