Gedichte Musik Bilder Quellcodebibliothek Diashow Normaldarstellung
Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis_ax/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 28.9.2014 mit Größe 5 kB image not shown  

Quelle  derivatives.pvs   Sprache: PVS

 
derivatives [T: TYPE FROM real ] : THEORY
%-----------------------------------------------------------------------------------------
%
%    The derivatives library has been generalized to handle a larger class of domains.
%    The following more general domain definition is now used
%
%        deriv_domain    : ASSUMPTION FORALL (e: posreal, x:T):
%                                        EXISTS (y: {u: nzreal | T_pred(u + x)}): abs(y) < e
%
%    This definition allows unions of closed and open intervals.
%    See deriv_domain and deriv_domains for more information and useful lemmas.
%    
%    See "derivatives_lam" for lambda-expression versions of the lemmas that are especially
%    suited to rewriting.  Note that when you expand a function, the PVS system does not
%    expand the definition using the real_fun_ops.  Instead it exapnds them using
%    lambda expressions.
%
%-----------------------------------------------------------------------------------------
BEGIN

  ASSUMING
    IMPORTING deriv_domain_def

    deriv_domain     : ASSUMPTION deriv_domain?[T]

    not_one_element  : ASSUMPTION not_one_element?[T]

  ENDASSUMING

  IMPORTING derivatives_def[T]

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


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

  deriv_fun    : TYPE = { f:[T -> real] | derivable?(f) }

  nz_deriv_fun : TYPE = { g:[T -> nzreal] | derivable?(g) }

  deriv(ff: deriv_fun)    : [T -> real] = LAMBDA x : deriv(ff, x)


  derivable_cont_fun     : LEMMA derivable?(f) IMPLIES continuous?(f)


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

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

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

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

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

  const_derivable_fun    : LEMMA derivable?(LAMBDA x: b)

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

  div_derivable_fun      : LEMMA derivable?(f) AND derivable?(g)
                             IMPLIES derivable?(f / g)

  identity_derivable_fun : LEMMA derivable?(I)

  id_derivable_fun       : LEMMA derivable?(LAMBDA x: x)
        

  ff, ff1, ff2 : VAR deriv_fun
  gg : VAR nz_deriv_fun

  derivable_cont   : JUDGEMENT deriv_fun SUBTYPE_OF continuous_fun[T]

  nz_derivable_cont: JUDGEMENT nz_deriv_fun SUBTYPE_OF nz_continuous_fun[T]

  derivable_sum    : JUDGEMENT +(ff1, ff2) HAS_TYPE deriv_fun

  derivable_diff   : JUDGEMENT -(ff1, ff2) HAS_TYPE deriv_fun

  derivable_prod   : JUDGEMENT *(ff1, ff2) HAS_TYPE deriv_fun

  derivable_scal   : JUDGEMENT *(b, ff) HAS_TYPE deriv_fun

  derivable_neg    : JUDGEMENT -(ff) HAS_TYPE deriv_fun

  derivable_div    : JUDGEMENT /(ff, gg) HAS_TYPE deriv_fun

  derivable_inv    : JUDGEMENT /(b, gg) HAS_TYPE deriv_fun

  derivable_const  : JUDGEMENT const_fun(b) HAS_TYPE deriv_fun

  derivable_id     : JUDGEMENT I[T] HAS_TYPE deriv_fun


  %------------------------
  %  Derivative function
  %------------------------

  % deriv_fun_def: LEMMA (FORALL x: convergence(NQ(f, x), 0, fp(x))) IMPLIES
  %                       derivable?(f) AND deriv(f) = fp

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

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

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

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

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

  deriv_inv_fun  : LEMMA deriv(1 / gg) = - deriv(gg) / (gg * gg)

  deriv_scaldiv_fun : LEMMA deriv(b / gg) = - (b * deriv(gg)) / (gg * gg)

  deriv_div_fun  : LEMMA deriv(ff / gg) = (deriv(ff)*gg - deriv(gg)*ff)/(gg*gg)

  deriv_const_fun: LEMMA deriv(LAMBDA x: b) = (LAMBDA x: 0)

  deriv_const_func: LEMMA deriv(const_fun(b)) = const_fun(0)

  deriv_id_fun    : LEMMA deriv(LAMBDA x: x) = (LAMBDA x: 1)

  deriv_I_fun     : LEMMA deriv(I) = (LAMBDA x: 1)

% ------------------ following added by Rick Butler ---------------------

  n: VAR nat
%  ^(f,n): [T -> real] =  (LAMBDA (t:T): f(t)^n)

  deriv_linear_fun: LEMMA FORALL (m,b: real):
                            LET f = (LAMBDA x: m*x + b) IN
                               derivable?(f) AND deriv(f) = (LAMBDA x: m)

  deriv_exp_fun: AXIOM derivable?(f) AND n > 0 IMPLIES
                       derivable?(f^n) AND
                       deriv(f^n) = n*f^(n-1)*deriv(f)

  
  deriv_x_n    : LEMMA n > 0 AND f = (LAMBDA x: x^n) IMPLIES
                          derivable?(f) AND deriv(f) = (LAMBDA x: n*x^(n-1))

  deriv_x_to_n : LEMMA FORALL (n: posnat, a: real):
                         LET f = (LAMBDA x: a*x^n) IN
                            derivable?(f) AND deriv(f) = (LAMBDA x: a*n*x^(n-1))

END derivatives

93%


¤ Dauer der Verarbeitung: 0.11 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




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.