SSL expt.pvs   Sprache: unbekannt

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