Top File of PVS power Library

 
%------------------------------------------------------------------------------
% Generalized Power function (without ln/exp)
%
%     Author: David Lester, Manchester University & NIA
%
%     Version 1.0            19/08/08   Initial version (DRL)
%
% This library provides Roots, Powers and Generalized Logs
%
% The (achieved) aim is to avoid using all libraries except those in
% the standard prelude. Hooks are provided so that the power function
% along with root and log can be shown to be continuous (over
% suitable domains), but no continuity libraries have been used to
% construct this library, meaning that it is built directly onto the
% standard SRI prelude.
%
% Features include:
% 
% By INCLUDING root, you can have statements like:
%
%   root(8,3) = 2
%
% By INCLUDING real_expt, you can have statements like:
%
%   8^(1/3) = 2
%
% BY INCLUDING log, you can have statements like:
%
%   log(2)(8) = 3 /* = ln(8)/ln(2) */
%
%------------------------------------------------------------------------------

top: THEORY

BEGIN

  IMPORTING rational_props_aux, % Extra properties for prelude
            exponentiation_aux, % Extra properties for prelude
            nn_root,            % nth-roots of nnreals 
            root,               % nth-roots of reals
                                %  (includes negative reals, for odd n)
            nn_rational_expt,   % x^y (x:nnreal, y: nnrat) Note 0^0 = 1
            nnreal_expt,        % x^y (x,y: nnreal)
            real_expt,          % x^y (x:nnreal, y:real) provided y>=0 when 0^y
            nn_log,             % inverse of nnreal_expt
            log,                % inverse of real_expt
            real_fun_power,     % exponentiation of functions

            ln_exp_def          % linking log to ln and ^ to exp
END top

The tag identifies links that are outside the NASA domain