SIGNATURE SetByPred[data]

-- sets represented by predicates
-- this makes infinite sets possible, but many functions from Set are not
-- computable ({}? # arb exist? ...) or need further information (incl
-- excl % ...) and are therefore not available

-- Parameter
SORT data

-- the type itself
TYPE set == asSet(cF: data -> bool)
-- cF is the characteristic function of the set 
-- x in S <=> cF(x) = true

-- constant sets
FUN {}        : set                     -- the empty set

FUN U : set                             -- the universal set
-- x in U = true 

-- combining sets
FUN + - *     : set ** set -> set       -- union/diff./intersection

FUN ~ : set -> set                      -- complement
-- x in S <=> ~ (x in ~(S))

-- information about a set
FUN in        : data ** set -> bool     -- membership