Go up to C Logic Evaluator Definitions Go 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 $
// ----------------------------------------------------------------