// ---------------------------------------------------------------- // \$Id: set.txt,v 1.7 1999/07/13 06:39:49 schreine Exp \$ // some set-theoretic notions // // (c) 1999, Wolfgang Schreiner, see file COPYRIGHT // http://www.risc.uni-linz.ac.at/software/formal // ---------------------------------------------------------------- option silent = true; // 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 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)))))); option silent = false; // ---------------------------------------------------------------- // \$Id: set.txt,v 1.7 1999/07/13 06:39:49 schreine Exp \$ // ----------------------------------------------------------------