%%% Real Intervals %%%
RealInt : THEORY
BEGIN

  RealInt : TYPE = [# lb: real,
               ub: real,
       bounded_below: bool,
       bounded_above: bool,
       closed_below: bool,
       closed_above: bool #]

  I   : VAR RealInt
  x,y : VAR real

  contains?(I)(x): bool =
    (I`bounded_below IMPLIES
      (IF I`closed_below THEN I`lb<=x ELSE I`lb<x ENDIF)) AND
    (I`bounded_above IMPLIES
      (IF I`closed_above THEN x<=I`ub ELSE x<I`ub ENDIF))


  mk_realint(x,y:real,bb,ba,cb,ca:bool) : MACRO RealInt =
    (# lb:=x,ub:=y,bounded_below:=bb,bounded_above:=ba,closed_below:=cb,closed_above:=ca #)

  ;##(x,I) : bool = contains?(I)(x)

  RealInf : DATATYPE WITH SUBTYPES Inf,nInf,RealN 
  BEGIN
    oo  : inf? : Inf
    ninf(get_inf:Inf) : ninf? : nInf
    open(get_real:real) : open? : RealN 
  END RealInf

  rx,ry : VAR RealInf

  ;-(i:Inf) : nInf = ninf(oo)

  ;[||](x,ry) : RealInt = 
    LET y = IF open?(ry) THEN get_real(ry) ELSIF ninf?(ry) THEN x-1 ELSE x+1 ENDIF IN
    mk_realint(x,y,TRUE,open?(ry),TRUE,FALSE)

  ;[||](rx,y) : RealInt = 
    LET x = IF open?(rx) THEN get_real(rx) ELSIF inf?(rx) THEN y+1 ELSE y-1 ENDIF IN
    mk_realint(x,y,open?(rx),TRUE,FALSE,TRUE)

  ;[||](rx,ry) : RealInt = 
    LET x = IF open?(rx) THEN get_real(rx) 
            ELSIF open?(ry) THEN 
              IF inf?(rx) THEN get_real(ry)+1
              ELSE get_real(ry)-1 
              ENDIF
            ELSE -1 ENDIF,
        y = IF open?(ry) THEN get_real(ry) 
            ELSIF open?(rx) THEN 
              IF ninf?(ry) THEN get_real(rx)-1
              ELSE get_real(rx)+1 
              ENDIF
            ELSE 1 ENDIF IN
    mk_realint(x,y,open?(rx),open?(ry),FALSE,FALSE)

  z : VAR real

  in_ninf_inf : LEMMA
    z ## [| -oo, oo |]

  in_ninf_open : LEMMA
    z ## [| -oo, open(y) |] IFF z < y

  in_open_inf : LEMMA
    z ## [| open(x), oo |] IFF z > x

  in_open_open : LEMMA
    z ## [| open(x), open(y) |] IFF x < z AND z < y

  in_ninf_close : LEMMA
    z ## [| -oo, y |] IFF z <= y

  in_close_inf : LEMMA
    z ## [| x, oo |] IFF z >= x

END RealInt