Impressum vect_fun_ops.pvs   Sprache: PVS

vect_fun_ops[n: posnat]: THEORY
%----------------------------------------------%
%  Operations on functions : [Vector -> real]  %
%----------------------------------------------%
BEGIN
  IMPORTING vectors[n]

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

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

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

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

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

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

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

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

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

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

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

  %------------------
  %  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 vect_fun_ops