Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: scott_continuity.pvs Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

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.