|
%------------------------------------------------------------------------------
% 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
¤ 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.
|
