Quelle  nth_derivatives.pvs

nth_derivatives[T: TYPE FROM real]: THEORY
%------------------------------------------------------------------------------
% The nth_derivatives theory defines the nth derivative of a function
%
% Developed  by Ricky W. Butler      NASA Langley Research Center
%               David Lester         Manchester University
% 
%      Version 1.0    last modified 10/30/00
%      Version 1.1    Generalised for an arbitrary interval: T DRL 27/10/03
%  
%------------------------------------------------------------------------------
BEGIN

   ASSUMING

%    connected_domain : ASSUMPTION
%         FORALL (x, y : T), (z : real) :
%             x <= z AND z <= y IMPLIES T_pred(z)

   IMPORTING deriv_domain_def

   deriv_domain    : ASSUMPTION deriv_domain?[T]

   not_one_element : ASSUMPTION not_one_element?[T]

   ENDASSUMING

   IMPORTING derivatives

   f: VAR [T -> real]
   m, n: VAR nat

   derivable_n_times?(f,n): RECURSIVE bool =
                                IF n = 0 THEN TRUE
                                ELSE
                                   derivable?(f) AND
                                   derivable_n_times?(deriv(f),n-1)
                                ENDIF MEASURE n


   derivable_n_times_lem: LEMMA derivable_n_times?(f,n) AND m <= n IMPLIES
                                   derivable_n_times?(f,m) 


   derivable_n_times_def: LEMMA derivable_n_times?(f, n+1) IMPLIES
                                  derivable_n_times?(deriv(f), n)



   nderiv_fun(n: nat): TYPE = {g: [T -> real] | derivable_n_times?(g,n)}


   nderiv(n: nat,f:nderiv_fun(n)):RECURSIVE [T -> real] = 
                 IF n = 0 THEN f
                 ELSE
                    nderiv(n-1,deriv(f))
                 ENDIF MEASURE n


   nderiv_derivable: LEMMA m <= n AND derivable_n_times?(f, 1 + n)
                             IMPLIES derivable?(nderiv(m, f))

   nderiv_derivable_aux: LEMMA derivable_n_times?(f, n+1) IMPLIES
                               nderiv(n+1,f) = deriv(nderiv(n,f))

   nderiv_derivable_eqv: LEMMA derivable_n_times?(f, 1 + n) IFF
                             derivable_n_times?(f,n) AND derivable?(nderiv(n, f))


END nth_derivatives