Quelle  chain_rule.pvs   Sprache: PVS

chain_rule [ T1, T2 : TYPE FROM real ] : THEORY
%----------------------------------------------------------------------------
%  Author:  Bruno Dutertre    Royal Holloway & Bedford New College
%----------------------------------------------------------------------------
BEGIN

  ASSUMING

    IMPORTING deriv_domain_def

     deriv_domain1     : ASSUMPTION deriv_domain?[T1]

     not_one_element1  : ASSUMPTION not_one_element?[T1]

     deriv_domain2     : ASSUMPTION deriv_domain?[T2]

     not_one_element2  : ASSUMPTION not_one_element?[T2]

  ENDASSUMING

  IMPORTING derivative_props % , lim_of_composition

  f : VAR [T1 -> T2]
  g : VAR [T2 -> real]
  x : VAR T1
  DF, DG : VAR real

  % chain_rule_cnvg        : LEMMA convergence(NQ(f, x), 0, DF) AND 
  %                             convergence(NQ(g, f(x)), 0, DG)
  %                           IMPLIES convergence(NQ(g o f, x), 0, DG * DF)

  composition_derivable : AXIOM derivable?(f, x) AND derivable?(g, f(x))
                            IMPLIES derivable?(g o f, x)

  composition_derivable_fun : LEMMA derivable?(f) AND derivable?(g) 
                                       IMPLIES derivable?(g o f)

  deriv_composition : AXIOM derivable?(f, x) AND derivable?(g, f(x))
                  IMPLIES deriv(g o f, x) = deriv(g, f(x)) * deriv(f, x)


  ff : VAR { f | derivable?(f) }
  gg : VAR { g | derivable?(g) }

  deriv_comp_fun     : LEMMA deriv(gg o ff) = (deriv(gg) o ff) * deriv(ff)


  comp_derivable_fun : LEMMA derivable?(f) AND derivable?(g) 
                                       IMPLIES derivable?(LAMBDA (x: T1): g(f(x)))

  chain_rule         : LEMMA deriv(LAMBDA (x: T1): gg(ff(x))) =
                               (LAMBDA (x: T1): deriv(gg)(ff(x))) * deriv(ff)

END chain_rule