Quellcode-Bibliothek symbols_as_proper.pvs

symbols_as_proper : THEORY
BEGIN

  IMPORTING proper_arith

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

  ;<(X,x) : MACRO bool =
    proper_Lt(X,x)

  ;<=(X,x) : MACRO bool =
    proper_Le(X,x)

  ;>(X,x) : MACRO bool =
    proper_Gt(X,x)

  ;>=(X,x) : MACRO bool =
    proper_Ge(X,x)

  ;+(X,Y) : MACRO ProperInterval =
    proper_Add(X,Y)    

  ;+(x,Y) : MACRO ProperInterval =
    proper_Add([|x|],Y)

  ;+(X,y) : MACRO ProperInterval =
    proper_Add(X,[|y|])

  ;-(X,Y) : MACRO ProperInterval =
    proper_Sub(X,Y)

  ;-(x,Y) : MACRO ProperInterval =
   [|x|]-Y

  ;-(X,y) : MACRO ProperInterval =
   X-[|y|]

  ;-(X) : MACRO ProperInterval =
    proper_Neg(X)

  ;*(X,Y) : MACRO ProperInterval = 
    proper_Mult(X,Y)

  ;*(x,Y) : MACRO ProperInterval =
    [|x|]*Y

  ;*(X,y) : MACRO ProperInterval =
    X*[|y|]

  YNz : VAR NzInterval
  ynz : VAR nzreal

  ;/(X,YNz) : MACRO ProperInterval =
    proper_Div(X,YNz)

  ;/(x,YNz) : MACRO ProperInterval =
    [|x|]/YNz

  ;/(X,ynz) : MACRO ProperInterval =
    X/[|ynz|]

  ;^(X,n) : MACRO ProperInterval = 
    proper_Pow(X,n)

END symbols_as_proper