Quellcode-Bibliothek nth_derivatives.pvs Sprache: 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

quality92%

¤ 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.0.0Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.