Quelle  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)

%   IMPORTING finite_sets@finite_sets

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


END doubletons