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