Impressum vect2_fun_ops.pvs

vect2_fun_ops: THEORY
%------------------------------------------%
%  Operations on functions : [Vect2 -> real]  %
%------------------------------------------%
BEGIN
  IMPORTING vectors_2D

  f, f1, f2: VAR [Vect2 -> real]
  f3        : VAR [Vect2 -> nzreal]
  a         : VAR real
  x, y      : VAR Vect2

  const_fun(a) : [Vect2 -> real] = LAMBDA x : a ;

  +(f1, f2) : [Vect2 -> real] = LAMBDA x : f1(x) + f2(x);
 
  -(f1)     : [Vect2 -> real] = LAMBDA x : -f1(x);

  *(f1, f2) : [Vect2 -> real] = LAMBDA x : f1(x) * f2(x);

  *(a, f1)  : [Vect2 -> real] = LAMBDA x : a * f1(x);

  -(f1, f2) : [Vect2 -> real] = LAMBDA x : f1(x) - f2(x);

  /(f1, f3) : [Vect2 -> real] = LAMBDA x : f1(x) / f3(x);

  /(a, f3)  : [Vect2 -> real] = LAMBDA x : a / f3(x);

  inv(f3)   : [Vect2 -> real] = 1 / f3;

  abs(f1)   : [Vect2 -> nnreal] = LAMBDA x : abs(f1(x));

  n: VAR nat
  ^(f,n)    : [Vect2 -> real] =  (LAMBDA (v:Vect2): f(v)^n)

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

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

  div_function     : LEMMA f1 / f3 = f1 * (1 /f3)

  scal_function    : LEMMA a * f1 = const_fun(a) * f1

  scaldiv_function : LEMMA a / f3 = const_fun(a) / f3

  negneg_function  : LEMMA - (- f1) = f1


END vect2_fun_ops