SSL open_sets.pvs

open_sets[T: TYPE FROM real]: THEORY
BEGIN

   AUTO_REWRITE+ member

   x,y: VAR T
   S,S1,S2: VAR set[T]
   open_ball?(x,S): bool = (EXISTS (delta: posreal): 
                                (FORALL y: abs(x-y) < delta IMPLIES S(y)))
   
   r: VAR posreal
   open_ball(x,r): set[T] = {y: T | abs(x-y) < r}
   
   open_ball?_lem: LEMMA open_ball?(x,S) IFF
                           EXISTS r: subset?(open_ball(x,r),S) 
   
   open?(S): bool = FORALL (x: (S)): open_ball?(x,S)
   
   open?_lem: LEMMA open?(S) AND S(x) IMPLIES open_ball?(x,S)
   
   closed?(S): bool = open?(complement(S))

   Open  : TYPE = (open?)      %% = {S: set[T] | open?(S)}
   Closed: TYPE = (closed?)    %% = {S: set[T] | closed?(S)}

   IMPORTING reals@intervals_real[T]

   above_intv(a:T)(x) : MACRO bool = x > a
   below_intv(a:T)(x) : MACRO bool = x < a

   a,b: VAR T

%   Open_empty        : LEMMA {x: Open_interval(a,a) | TRUE} = emptyset[T]

   open_intv_open     : LEMMA a < b IMPLIES open?(open_intv(a,b))

   above_intv_open    : LEMMA open?(above_intv(a))  
   below_intv_open    : LEMMA open?(below_intv(a))  

   union_open         : LEMMA open?(S1) AND open?(S2) IMPLIES
                                 open?(union(S1,S2))

   closed_intv_closed : LEMMA a < b IMPLIES closed?(closed_intv(a,b))


END open_sets