Quellcode-Bibliothek deriv_real_vect.pvs Sprache: PVS

deriv_real_vect[T: TYPE FROM real, n: posnat ] : THEORY
%------------------------------------------------------------------------------
% Derivatives of Vector-Valued Functions
%
%    Author:  Rick Butler     NASA Langley Research Center
%
%------------------------------------------------------------------------------
BEGIN

  ASSUMING

    IMPORTING analysis@deriv_domain_def

    deriv_domain     : ASSUMPTION deriv_domain?[T]

    not_one_element  : ASSUMPTION not_one_element?[T]

  ENDASSUMING

  IMPORTING deriv_real_vect_def[T,n], deriv_dot_prod[T,n]

  f, f1, f2, fp : VAR [T -> Vector[n]]
  g : VAR [T -> nzreal]
  x : VAR T
  u : VAR nzreal
  b : VAR real
  l, l1, l2 : VAR real

  h:[T -> real]

  derivable?(f) : bool = FORALL x : derivable?(f, x)

  deriv_vfun    : TYPE = { f:[T -> Vector[n]] | derivable?(f) }

  nz_deriv_vfun : TYPE = { g:[T -> Nz_vector[n]] | derivable?(g) }

  deriv(ff: deriv_vfun) : [T -> Vector[n]] = LAMBDA x : deriv(ff, x)

  sum_derivable_vfun     : LEMMA derivable?(f1) AND derivable?(f2)
                             IMPLIES derivable?(f1 + f2)

  neg_derivable_vfun     : LEMMA derivable?(f) IMPLIES derivable?(- f)

  diff_derivable_vfun    : LEMMA derivable?(f1) AND derivable?(f2)
                             IMPLIES derivable?(f1 - f2)

%%  prod_derivable_rv       : LEMMA derivable?(h) IMPLIES derivable?(LAMBDA (x: T): h(x)*f(x))

  dot_derivable_vfun      : LEMMA derivable?(f1) AND derivable?(f2)
                             IMPLIES derivable?(f1 * f2)

  scal_derivable_vfun    : LEMMA derivable?(f) IMPLIES derivable?(b * f)

  const_derivable_vfun   : LEMMA derivable?(const_vfun(b))

  inv_derivable_vfun     : LEMMA derivable?(g) IMPLIES derivable?(1/g)

  ff, ff1, ff2 : VAR deriv_vfun
  hh: VAR deriv_fun[T]
  derivable_sum    : JUDGEMENT +(ff1, ff2) HAS_TYPE deriv_vfun
  derivable_diff   : JUDGEMENT -(ff1, ff2) HAS_TYPE deriv_vfun
  derivable_scal   : JUDGEMENT *(b, ff) HAS_TYPE deriv_vfun
  derivable_neg    : JUDGEMENT -(ff) HAS_TYPE deriv_vfun
  derivable_const  : JUDGEMENT const_vfun(b) HAS_TYPE deriv_vfun

  %-----------------------------------
  %  Derivative vector-valued function
  %-----------------------------------

  deriv_sum_vfun      : LEMMA deriv(ff1 + ff2) = deriv(ff1) + deriv(ff2)

  deriv_neg_vfun      : LEMMA deriv(- ff) = - deriv(ff)

  deriv_diff_vfun     : LEMMA deriv(ff1 - ff2) = deriv(ff1) - deriv(ff2)

%%  deriv_prod_vfun     : LEMMA deriv(LAMBDA (x: T): hh(x) * ff1(x)) = deriv(hh)*ff1 + hh*deriv(ff1)

  deriv_dot_vfun      : LEMMA deriv(ff1 * ff2) = deriv(ff1) * ff2 + deriv(ff2) * ff1

  deriv_scal_vfun     : LEMMA deriv(b * ff) = b * deriv(ff)

  deriv_const_vfun    : LEMMA deriv(const_vfun(b)) = const_vfun(0)

END deriv_real_vect

quality91%

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

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.