abs_props.pvs   Interaktion und
PortierbarkeitPVS

%
%
% Purpose : extra properties of absolute value
%
%

abs_props: THEORY

BEGIN

  IMPORTING minmax_ineq

  x, y: VAR real
  nny: VAR nnreal

  abs_max: LEMMA
    abs(x) = max(-x,x)

  abs_add: LEMMA
    x*y >= 0 IMPLIES abs(x+y) = abs(x) + abs(y)

  abs_le_nonneg: LEMMA
    abs(x) <= nny IFF -nny <= x AND x <= nny

  abs_diff_commutes: LEMMA abs(x-y) = abs(y-x)  % from hacks

END abs_props