SSL doubletons.pvs

doubletons[T: TYPE]: THEORY

BEGIN

   x,y,z: VAR T

   dbl(x,y): set[T] = {t: T | t = x OR t = y}

   S: VAR set[T]

   doubleton?(S): bool = (EXISTS x,y: x /= y AND S = dbl(x,y))

   doubleton: TYPE = {S | EXISTS x,y: x /= y AND S = dbl(x,y)}

   Dbl: TYPE = doubleton

   dbl_comm: LEMMA dbl(x,y) = dbl(y,x)

   D: VAR doubleton

   doubleton_irreflexive  : LEMMA NOT doubleton?(dbl(x,x))

   doubleton_nonempty     : LEMMA nonempty?(D)

   doubleton_rest_nonempty: LEMMA nonempty?(rest(D))

   dbl_choose             : LEMMA choose(dbl(x,y)) = x or choose(dbl(x,y)) = y

   dbl_rest_choose        : LEMMA x /= y IMPLIES
                                  (choose(dbl(x,y)) /= choose(rest(dbl(x,y)))) AND 
                                  (choose(rest(dbl(x,y))) = x 
                                      OR choose(rest(dbl(x,y))) = y)

   dbl_to_pair(D) : {(x,y) | D = dbl(x,y)}

   dbl_def        : LEMMA dbl(PROJ_1(dbl_to_pair(D)), PROJ_2(dbl_to_pair(D))) = D

   dbl_in         : LEMMA D = dbl(x,y) IMPLIES D(x) AND D(y)
   
   dbl_not_in     : LEMMA D = dbl(x,y) AND z /= x AND z /= y IMPLIES NOT D(z)

   dbl_to_pair_lem        : LEMMA x /= y IMPLIES
                                   dbl_to_pair(dbl(x,y)) = (x,y) OR
                                   dbl_to_pair(dbl(x,y)) = (y,x) 

   dbl_to_pair_inverse_l  : LEMMA dbl(dbl_to_pair(D)) = D

   dbl_proj               : LEMMA D(PROJ_1(dbl_to_pair(D))) AND
                                  D(PROJ_2(dbl_to_pair(D)))
   v: VAR T
   proj_dbl: LEMMA (PROJ_1(dbl_to_pair(D)) = v OR PROJ_2(dbl_to_pair(D)) = v)
                    IMPLIES D(v)

   dbl_eq: LEMMA dbl(x,y) = dbl(v,z) IMPLIES
                        (x = v AND y = z) OR (x = z AND y = v)

   finite_dbl: LEMMA is_finite(dbl(x,y))

   e: VAR doubleton
   finite_doubleton: LEMMA is_finite(e)

   card_dbl: LEMMA x /= y IMPLIES card(dbl(x,y)) = 2

   JUDGEMENT dbl(x,y) HAS_TYPE finite_set[T]



   AUTO_REWRITE+ doubleton_irreflexive   % NOT doubleton?(dbl(x,x))
   AUTO_REWRITE+ doubleton_nonempty      % nonempty?(D)  
   AUTO_REWRITE+ dbl_def                 % dbl(PROJ_1(dbl_to_pair(D)), 
                                         %     PROJ_2(dbl_to_pair(D))) = D

   AUTO_REWRITE+ dbl_to_pair_inverse_l   % dbl(dbl_to_pair(D)) = D
   AUTO_REWRITE+ dbl_proj                

   AUTO_REWRITE+ finite_dbl
   AUTO_REWRITE+ finite_doubleton

%  ------------- The following two cause wierd PVS bug -------

   AUTO_REWRITE+ dbl_in                  % D = dbl(x,y) IMPLIES D(x) AND D(y)
   AUTO_REWRITE+ dbl_not_in              % D = dbl(x,y) AND z /= x AND z /= y 





  rev(fs: finseq[T]): finseq[T] = (# length := length(fs),
                                  seq := (LAMBDA (i: below(length(fs))): seq(fs)(length(fs)-1-i))
                             #)
  


END doubletons