Quelle expt.pvs Sprache: PVS

expt: THEORY
%----------------------------------------------------------------------------
%
%  Exponentiation: a^x where both a and x are real-valued
%
%  Author:  Rick Butler     NASA Langely Research Center
%
%  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:  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_div   : LEMMA (a/px)^^x = a^^x/px^^x

   hathat_abs   : LEMMA abs(a^^x) = abs(a)^^x

%   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

quality91%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.