top: THEORY
%------------------------------------------------------------------------------
%
% Extended library for calculus: axiomatic version
%
% Formal Methods Team
% ICASE - NASA Langley
%
% C. Munoz (munoz@icase.edu)
% G. Dowek (gilles.dowek@inria.fr)
%
% Version 1.1 (May 21, 2001)
%
% Developed using Dutertre's real analysis library. The goal was
% to provide a compact, easy-to-use calculus theory for functions
% from [real -> real]. Once PVS 3 is released, this library will be
% formally shown to be consistent. Currently the soundness of this
% library is based upon a syntactic comparison with the Dutertre analysis
% library.
% The following theories were created by copying sections from
% Dutertre's library and changing lemmas into axioms.
%
% chain_rule_ax.pvs
% continuous_functions_ax.pvs
% derivative_props_ax.pvs
% derivatives_ax.pvs
% intermediate_value_ax.pvs
% restriction_continuous_ax.pvs
% real_fun_props_ax.pvs
%
% NOTE: User's of this library can quickly switch to Dutertre's analysis
% library by changing the IMPORTINGS in "derivatives_con" and "extra_con".
% See comments in these theories.
%
%
% LIBRARIES USED:
%
% reals (sqrt)
% trig
%
%------------------------------------------------------------------------------
BEGIN
IMPORTING calculus, % basic properties of derivatives
% of functions [real -> real]
% derivatives_ax[T],
% chain_rule_ax,
% deriv_sqrt,
% deriv_trig,
calculus_extra, % additional properties such as
% mean value theorem
% continuous_functions_ax,
% intermediate_value_ax,
% restriction_continuous_ax,
% derivative_props_ax
% ------- added to make sure both of the following get dumped -------
derivative_def,
derivative_def_ax
END top