Finite Sets

spec
     Elem =
     sort
          Elem
end

spec
     GenerateFiniteSet [Elem with sort Elem] =
free
{
     type
           FinSet[Elem]::= {} | set(Elem) |
                           __ union __ (FinSet[Elem];FinSet[Elem])
     op
           __ union __: FinSet[Elem] * FinSet[Elem] -> FinSet[Elem],
                        assoc, comm, idem, unit {}
}
%%     intended system of representatives:
%%     {} and
%%     set(x1) union ... union set(xn),
%%     where n >= 1, xi in Elem, xi =/= xj for i =/= j, and
%%     x1 < x2 < ...< xn (< is an arbitrary order on Elem)
end

spec
     FiniteSet [Elem with sort Elem] =
     GenerateFiniteSet [Elem]
     with sort FinSet[Elem] , ops {}, set, __ union __
then
     preds
           __  elemOf __:    Elem * FinSet[Elem];
           __ isSubsetOf __: FinSet[Elem] * FinSet[Elem]
     ops
           add:                Elem * FinSet[Elem] -> FinSet[Elem];
           __ without __:      FinSet[Elem] * Elem -> FinSet[Elem];
           __ intersection __,
           __ - __,
           __ symmDiff __:     FinSet[Elem] * FinSet[Elem] -> FinSet[Elem]
     vars
          x,y : Elem; S,T,U,V:FinSet[Elem]
     %%          x  elemOf S:
     .          not x  elemOf {}
     .          x  elemOf set(y) <=> (x=y)
     .          x  elemOf (S union T) <=> (x  elemOf S) \/ (x  elemOf T)
     %%          S isSubsetOf T:
     .          {} isSubsetOf S
     .          set(x) isSubsetOf S <=> x  elemOf S
     .          (S union T) isSubsetOf U <=> S isSubsetOf U /\ T isSubsetOf U
     %%          add(x,S):
     .          add(x,S) = set(x) union S
     %%          S without x:
     .          {} without x = {}
     .          set(y) without x = set(y) if not x = y
     .          set(y) without x = {} if x = y
     .          (S union T) without x = (S without x) union (T without x)
     %%          S intersection T:
     .          {} intersection S = {}
     .          set(x) intersection S = {} if not x  elemOf S
     .          set(x) intersection S = set(x) if x  elemOf S
     .          (S union T) intersection U = ( S intersection U ) union (T
          intersection U)
     %%          S - T:
     .          {} - S = {}
     .          set(x) - S = set(x) if not x  elemOf S
     .          set(x) - S = {} if x  elemOf S
     .          (S union T) - U = (S - U ) union (T - U)
     %%          S symmDiff T:
     .          S symmDiff T = (S - T) union (T - S)

then
     %%cons
     ops
           __ intersection __: FinSet[Elem] * FinSet[Elem] -> FinSet[Elem],
                               assoc, comm, idem;
           __ symmDiff __ :    FinSet[Elem] * FinSet[Elem] -> FinSet[Elem],
                               comm;
     vars
          x: Elem; S,T: FinSet[Elem]
     .          S isSubsetOf T <=> ( forall x: Elem . x  elemOf S => x  elemOf T )

end

view
     PartialOrder_in_FiniteSet [Elem]:
PartialOrder
     to FiniteSet [Elem] =
     sort
          Elem |-> FinSet[Elem] ,
     pred
          __ <= __ |-> __ isSubsetOf __
end

spec
     FinitePowerSet3
     [FiniteSet [Elem with sort Elem]
      with preds __  elemOf __,__ isSubsetOf __,
           ops __ union __, __ intersection __, add, __ without __, __ -
           __, __ symmDiff __ ]
     [op X: FinSet[Elem]] =
     sorts
           FinitePowerSet[X]= { Y: FinSet[Elem] . Y isSubsetOf X };
           Elem[X] =          {x : Elem . x  elemOf X }
     preds
           __  elemOf __ :   Elem[X] * FinitePowerSet[X];
           __ isSubsetOf __: FinitePowerSet[X] * FinitePowerSet[X]
     ops
           {}:                 FinitePowerSet[X];
           set :               Elem[X] -> FinitePowerSet[X];
           add:                Elem[X] × FinitePowerSet[X] ->
                               FinitePowerSet[X];
           __ union __,
           __ intersection __,
           __ - __,
           __ symmDiff __:     FinitePowerSet[X] * FinitePowerSet[X]
                               -> FinitePowerSet[X]
     %%          These predicates and operations
     %%          are determined by overloading.end

view
     DefineBooleanAlgebra_in_FinitePowerSet
     [FiniteSet[Elem]] [op X: FinSet[Elem]]:
DefineBooleanAlgebra
     to
FinitePowerSet
     [FiniteSet[Elem]] [ op X: FinSet[Elem]] =
     sort
          Elem |-> FinitePowerSet[X],
     ops
           0 |-> {},
           1 |-> X,
           __ cap __ |-> __ intersection __,
           __ cup __ |-> __ union __
end