|
expt: THEORY
%----------------------------------------------------------------------------
%
% Exponentiation: a^x where both a and x are real-valued
%
% Author: Rick Butler NASA Langley Research Center
% Olga Lightfoot, QMUL
%
% Version 1.0 8/27/04
%
%----------------------------------------------------------------------------
BEGIN
IMPORTING ln_exp
k,n,m: VAR nat
x,t: VAR real
epsilon: VAR posreal
^^(a: nnreal,x: {r:real | a /= 0 OR r /= 0}): nnreal = IF a = 0 THEN 0
ELSE exp(x*ln(a))
ENDIF
a,b: VAR posreal
px,py: VAR posreal
nzx: VAR nzreal
hathat_sum : LEMMA a^^(n + m) = (a^^n)*(a^^m)
hathat_diff : LEMMA a^^(n - m) = (a^^n)/(a^^m)
hathat_to_0 : LEMMA px^^0 = 1
hathat_to_1 : LEMMA a^^1 = a
hathat_0 : LEMMA 0^^nzx = 0
hathat_1 : LEMMA 1^^x = 1
hathat_nat : LEMMA a^^n = a^n
hathat_lt_cross: LEMMA a^^(1/px) < b IMPLIES a < b^^px
hathat_gt_cross: LEMMA a^^(1/px) > b IMPLIES a > b^^px
hathat_eq_0 : LEMMA a^^nzx = 0 IFF a = 0
hathat_eq_1 : LEMMA px^^x = 1 IFF (x = 0 OR px = 1)
hathat_cross : LEMMA a^^(1/px)=b IMPLIES a=b^^px
hathat_mult : LEMMA (a^^px)^^py=a^^(px*py)
hathat_div : LEMMA (a/px)^^x = a^^x/px^^x
hathat_abs : LEMMA abs(a^^x) = abs(a)^^x
hathat_sum_posreal: LEMMA (a^^px)*(a^^py)=a^^(px+py)
hathat_diff_posreal: LEMMA (a^^px)/(a^^py)=a^^(px-py)
hathat_cont : LEMMA continuous?(LAMBDA x: a^^x)
% hathat_cont_nn : LEMMA continuous?(LAMBDA (x: posreal): x^^t)
% hathat_cont_nnpos : LEMMA continuous?(LAMBDA (x: nnreal): x^^a)
AUTO_REWRITE+ hathat_to_0
AUTO_REWRITE+ hathat_to_1
AUTO_REWRITE+ hathat_0
AUTO_REWRITE+ hathat_1
% There are now multiple versions of f(x) = a^x
% available in PVS. The prelude provides a version for a^n where n is natural
% This theory provides a definition for non-negative a and x real
% The complex library provides exp(z) for complex z, from which
% we could defined another ^ (not yet done).
% I am not happy with naming the lemmas "hathat" but I can't think
% of a better name. One could explore the use of theory interpretations
% to create an axiomatic version of ^ which is more general than
% the current version in the prelude and use these other theories
% to show that this axiomatic version is consistent.
END expt
¤ Dauer der Verarbeitung: 0.21 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.
|
