Quelle  real_fun_ops.pvs

real_fun_ops  [ T : TYPE ] : THEORY
%------------------------------------------%
%  Operations on functions : [ T -> real]  %
%------------------------------------------%
BEGIN

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

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


  +(f1, f2) : [T -> real] = LAMBDA x : f1(x) + f2(x);
  -(f1)     : [T -> real] = LAMBDA x : -f1(x);
  *(f1, f2) : [T -> real] = LAMBDA x : f1(x) * f2(x);
  *(a, f1)  : [T -> real] = LAMBDA x : a * f1(x);
  -(f1, f2) : [T -> real] = LAMBDA x : f1(x) - f2(x);
  /(f1, f3) : [T -> real] = LAMBDA x : f1(x) / f3(x);
  /(a, f3)  : [T -> real] = LAMBDA x : a / f3(x);
  inv(f3)   : [T -> real] = 1 / f3;
  abs(f1)   : [T -> nonneg_real] = LAMBDA x : abs(f1(x));

  n: VAR nat
  ^(f,n)    : [T -> real] =  (LAMBDA (t:T): f(t)^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 real_fun_ops