Go up to C Logic Evaluator DefinitionsGo forward to C.2 Relations and Functions

C.1 Sets

```// ----------------------------------------------------------------
// \$Id: evaluator.tex,v 1.7 1999/09/29 12:28:26 schreine Exp \$
// some set-theoretic notions
//
// (c) 1999, Wolfgang Schreiner, see file COPYRIGHT
// http://www.risc.uni-linz.ac.at/software/formal
// ----------------------------------------------------------------

// singleton set
fun {}(x) =
join(x, {});

// A is a subset of B iff every element of A is also in B
pred isSubset(A: Set, B: Set) <=>
forall(x in A: in(x, B));

// two sets are equal if each is a subset of the other
pred equals(A: Set, B: Set) <=>
and(isSubset(A, B), isSubset(B, A));

// the intersection of two sets
fun **(A: Set, B: Set) =
set(x in A: in(x, B), x);

// the difference of two sets
fun --(A: Set, B: Set) =
set(x in A: not(in(x, B)), x);

// the union of two sets
fun ++(A: Set, B: Set) =
reduce(join, A, B);

// the union of all sets n A
fun ++(A: Set) =
reduce(++, A, {});

// the product of two sets A and B
fun x(A: Set, B: Set) =
set(a in A, b in B: true, tuple(a, b));

// cardinality of S is determined by iteration over the elements
fun count(e, i: Nat) = +(i, 1);
fun #(S: Set) = reduce(count, S, 0);

// the union of S and of e joined to all elements of S
fun combine(e, S: Set) =
++(S, set(x in S: true, join(e, x)));

// the set of all subsets of S
fun Powerset(S: Set) =
reduce(combine, S, {}({}));

// alternative recursive definition
fun PowersetR(S: Set) recursive #(S) =
if (=(S, {}), join({}, {}),
let(e = such(x in S: true, x):
combine(e, Powerset(--(S, {}(e))))));

// ----------------------------------------------------------------
// \$Id: evaluator.tex,v 1.7 1999/09/29 12:28:26 schreine Exp \$
// ----------------------------------------------------------------
```

Author: Wolfgang Schreiner
Last Modification: October 4, 1999