deriv_real_vect_def [T: TYPE FROM real, n: posnat ] : THEORY
%------------------------------------------------------------------------------
% Derivatives of Vector-Valued Functions
%
%    Author:  Rick Butler     NASA Langley Research Center
%
%  This is the point-wise version.  Users should probably rely primarily on
%  the theory deriv_real_vect.
%------------------------------------------------------------------------------
BEGIN

  ASSUMING

    IMPORTING analysis@deriv_domain_def

    deriv_domain     : ASSUMPTION deriv_domain?[T]

    not_one_element  : ASSUMPTION not_one_element?[T]

  ENDASSUMING


  CONVERSION+ singleton

  IMPORTING analysis@derivatives[T]  

  IMPORTING vectors@vectors[n], vect_fun_ops

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

  const_vfun(a) : MACRO [T -> Vector[n]] = (LAMBDA x : (LAMBDA (i: below(n)): a))

  derivable?(f, x) : bool = FORALL (i: below[n]): derivable?(LAMBDA (t:T): f(t)(i),x)

  deriv(f, (x0 : { x | derivable?(f, x) })) : Vector[n] = 
                (LAMBDA (i: below(n)): deriv(LAMBDA (t:T): f(t)(i), x0 ))
 
  sum_derivable      : LEMMA derivable?(f1, x) AND derivable?(f2, x)
                             IMPLIES derivable?(f1 + f2, x)

  diff_derivable     : LEMMA derivable?(f1, x) AND derivable?(f2, x)
                             IMPLIES derivable?(f1 - f2, x)

  neg_derivable      : LEMMA derivable?(f, x) IMPLIES derivable?(- f, x)

  scal_derivable     : LEMMA derivable?(f, x) IMPLIES derivable?(b * f, x)

  const_derivable    : LEMMA derivable?(const_vfun(b), x)

  deriv_sum         : LEMMA derivable?(f1, x) AND derivable?(f2, x) IMPLIES
                         deriv(f1 + f2, x) = deriv(f1, x) + deriv(f2, x)

  deriv_neg         : LEMMA derivable?(f, x) IMPLIES 
                         deriv(- f, x) = - deriv(f, x)

  deriv_diff        : LEMMA derivable?(f1, x) AND derivable?(f2, x) IMPLIES
                            deriv(f1 - f2, x) = deriv(f1, x) - deriv(f2, x)

  deriv_const        : LEMMA deriv(const_vfun(b), x) = zero[n]

  deriv_scal         : LEMMA derivable?(f, x) IMPLIES deriv(b * f, x) = b * deriv(f, x)

END deriv_real_vect_def