Quelle  proper_arith.pvs

proper_arith : THEORY
BEGIN

%
% The comparison and arithmetic operators defined in this theory require operands to be non-empty 
% (and in the case of division a non-zero divisor). The PVS's type-checker will generate TCCs that enforces
% these properties. 
%
% The theory symbols_as_proper defines the symbols +,-,*,/,^ using the functions in this theory
%

  IMPORTING interval

  x,y : VAR real
  X,Y : VAR ProperInterval
  n   : VAR nat

  NzInterval     : TYPE = { X | Zeroless?(X) }
  PosInterval    : TYPE = { X | Pos?(X) }
  NegInterval    : TYPE = { X | Neg?(X) }
  NonNegInterval : TYPE = { X | NonNeg?(X) }

  proper_Lt(X,x) : bool =
    Lt(X,x)

  proper_Le(X,x) : bool =
    Le(X,x)

  proper_Gt(X,x) : bool =
    Gt(X,x)

  proper_Ge(X,x) : bool =
    Ge(X,x)

  proper_Add(X,Y) : ProperInterval =
    Add(X,Y)    

  proper_Sub(X,Y) : ProperInterval =
    Sub(X,Y)

  proper_Neg(X) : ProperInterval =
    Neg(X)

  proper_Mult(X,Y) : ProperInterval = 
    Mult(X,Y)

  YNz : VAR NzInterval
  ynz : VAR nzreal

  proper_Div(X,YNz) : ProperInterval =
    Div(X,YNz)

  proper_Pow(X,n) : ProperInterval = 
    Pow(X,n)

  proper_Abs(X) : ProperInterval =
    Abs(X)

  proper_Sq(X) : ProperInterval =
    Sq(X)

END proper_arith