Quelle  vect_fun_ops_rv.pvs

vect_fun_ops_rv  [T: TYPE] : THEORY
%------------------------------------------%
%  Operations on functions : [ T -> Vect2]  %
%------------------------------------------%
BEGIN

   IMPORTING vectors@vectors_2D

   f, f1, f2: VAR [T -> Vect2]
   x : VAR T
   a,b : VAR real
   r: VAR [T -> real]
   v: VAR Vect2
   

   +(f1, f2) : MACRO [T -> Vect2]  = LAMBDA x : f1(x) + f2(x);
   -(f1)     : MACRO [T -> Vect2]  = LAMBDA x : -f1(x);
   -(f1, f2) : MACRO [T -> Vect2]  = LAMBDA x : f1(x) - f2(x);
   *(b,f1)   : MACRO [T -> Vect2]  = LAMBDA x : b*f1(x);            %% scalar product
   *(r,f)  : [T -> Vect2]          = LAMBDA (t:T): r(t)*f(t);
   *(f1,f2)  : MACRO [T -> real]   = LAMBDA x : f1(x)*f2(x);        %% dot product
 
   const_vfun(a) : MACRO [T -> Vect2] = (LAMBDA x : (a,a))
   const_vfun(v) : [T -> Vect2] = (LAMBDA x : v) ;

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

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

END vect_fun_ops_rv