vect_fun_ops  [T: TYPE, n: posnat ] : THEORY
%------------------------------------------%
%  Operations on functions : [ T -> Vect[n]]  %
%------------------------------------------%
BEGIN

   IMPORTING vectors@vectors[n]

   f, f1, f2: VAR [T -> Vector[n]]
   h: VAR [T -> real]
   x : VAR T
   a,b : VAR real

   +(f1, f2) : MACRO [T -> Vector[n]]  = LAMBDA x : f1(x) + f2(x);
   -(f1)     : MACRO [T -> Vector[n]]  = LAMBDA x : -f1(x);
   -(f1, f2) : MACRO [T -> Vector[n]]  = LAMBDA x : f1(x) - f2(x);
   *(b,f1)   : MACRO [T -> Vector[n]]  = LAMBDA x : b*f1(x);                %% scalar product
   *(h,f)    : MACRO [T -> Vector[n]]   = LAMBDA (t:T): h(t)*f(t);
   *(f1,f2)  : MACRO [T -> real]       = LAMBDA x : f1(x)*f2(x);            %% dot product
 
  const_vfun(a) : MACRO [T -> Vector[n]] = (LAMBDA x : (LAMBDA (i: below(n)): a))

  %------------------
  %  Rewrite rules
  %------------------

  diff_function    : LEMMA f1 - f2 = f1 + (- f2)
  negneg_function  : LEMMA - (- f1) = f1

END vect_fun_ops