Go backward to C.9 Real Functions Go up to C Logic Evaluator Definitions Go forward to C.11 Modular Arithmetic

C.10 Equivalence Relations

// ----------------------------------------------------------------
// $Id: evaluator.tex,v 1.7 1999/09/29 12:28:26 schreine Exp $
// equivalence relations
//
// (c) 1999, Wolfgang Schreiner, see file COPYRIGHT
// http://www.risc.uni-linz.ac.at/software/formal
// ----------------------------------------------------------------
read relation;

// R is reflexive on S
pred isReflexive(R: Relation, S) <=>
  forall(x in S: in(tuple(x, x), R));

// R is symmetric on S
pred isSymmetric(R: Relation, S) <=>
  forall(t in R: in(tuple(.1(t), .0(t)), R));

// R is transitive on S
pred isTransitive(R: Relation, S) <=>
  forall(s in R, t in R: 
    implies(=(.1(s), .0(t)), in(tuple(.0(s), .1(t)), R))); 

// R is equivalence relation on S
pred isEquivalence(R: Relation, S) <=>
  and(isRelation(R, S, S), isReflexive(R, S),
      isSymmetric(R, S), isTransitive(R, S));

// class [x]_R
fun [](x, R: Relation) =
  set(y in range(R): in(tuple(x, y), R), y);

// quotient set S/R
fun /(S, R: Relation) = set(x in S: true, [](x, R));

// D is partition on S
pred isPartition(D, S) <=>
  and(forall(x in D: not(=(x, {}))),
      forall(x in D, y in D: or(=(x, y), =(**(x, y), {}))),
      =(++(D), S));

// induced relation ~D
fun ~(D) = 
  ++(set(d in D: true, set(x in d, y in d: true, tuple(x, y))));

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