FDL > PVS > Prelude > sets : Theory

PVS-2.4 prelude.pvs

 sets provides the polymorphic set type, along with the usual set
 operations.  It is important to bear in mind that a set is just
 a predicate.

sets [T:TYPE] : THEORY
BEGIN

set : TYPE = setof[T]

x: VAR T

y: VAR T

a: VAR set

b: VAR set

c: VAR set

p: VAR PRED[T]

member(x, a): bool = a(x);

empty?(a): bool = FORALL x : NOT member(x, a);

emptyset: set = {x | FALSE};

nonempty?(a): bool = NOT empty?(a);

full?(a): bool = FORALL x : member(x, a);

fullset: set = {x | TRUE};

subset?(a, b): bool = FORALL x : member(x, a) = > member(x, b);

strict subset?(a, b): bool = subset?(a, b) & (a /= b);

union(a, b): set = {x | member(x, a) OR member(x, b)};

intersection(a, b): set = {x | member(x, a) AND member(x, b)};

disjoint?(a, b): bool = empty?(intersection(a, b));

complement(a): set = {x | NOT member(x, a)};

difference(a, b): set = {x | member(x, a) AND (NOT member(x, b))};

symmetric difference(a, b): set = union(difference(a, b), difference(b, a));

every(p)(a): bool = FORALL (x:(a) ) : p(x);

every(p, a): bool = FORALL (x:(a) ) : p(x);

some(p)(a): bool = EXISTS (x:(a) ) : p(x);

some(p, a): bool = EXISTS (x:(a) ) : p(x);

singleton?(a): bool = EXISTS (x:(a) ) : FORALL (y:(a) ) : x = y;

%%(TCC) singleton_TCC1: OBLIGATION

singleton(x): (singleton?) = {y | y = x};

%%(TCC) add_TCC1: OBLIGATION

add(x, a): (nonempty?) = {y | (x = y) OR member(y, a)};

remove(x, a): set = {y | (x /= y) AND member(y, a)};

%%(TCC) choose_TCC1: OBLIGATION

%%(TCC) choose_TCC2: OBLIGATION

choose((p:(nonempty?) )): (p) = epsilon(p);

%%(TCC) the_TCC1: OBLIGATION

%%(TCC) the_TCC2: OBLIGATION

the((p:(singleton?) )): (p) = epsilon(p);

%%(TCC) rest_TCC1: OBLIGATION

rest(a): set = IF empty?(a) THEN a ELSE remove(choose(a), a) ENDIF;

%%(TCC) nonempty_singleton: OBLIGATION

nonempty singleton: JUDGEMENT (singleton?) SUBTYPE_OF (nonempty?)

%%(TCC) nonempty_union1: OBLIGATION

nonempty union1: JUDGEMENT union((a:(nonempty?) ), (b:set)) HAS_TYPE (nonempty?)

%%(TCC) nonempty_union2: OBLIGATION

nonempty union2: JUDGEMENT union((a:set), (b:(nonempty?) )) HAS_TYPE (nonempty?)

END sets