Go backward to C.13 Rationals as Equivalence Classes Go up to C Logic Evaluator Definitions

C.14 Order Relations

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

read equiv;

// R is antisymmetric on S
pred isAntiSymmetric(R: Relation, S) <=>
  forall(x in S, y in S:
    implies(and(in(tuple(x, y), S), in(tuple(y, x), S)), =(x, y)));

// R is partial order on S
pred isPartialOrder(R: Relation, S) <=>
  and(isRelation(R, S, S),
      isReflexive(R, S),
      isAntiSymmetric(R, S),
      isTransitive(R, S));

// R is irreflexive on S
pred isIrreflexive(R: Relation, S) <=>
  forall(x in S: not(in(tuple(x, x), R)));

// R is partial order on S
pred isQuasiOrder(R: Relation, S) <=>
  and(isRelation(R, S, S),
      isIrreflexive(R, S),
      isAntiSymmetric(R, S),
      isTransitive(R, S));

// x and y are incomparable with respect to R
pred areIncomparable(x, y, R) <=>
  and(not(in(tuple(x, y), R)), not(in(tuple(y, x), R)));

// R is total order on S
pred isTotalOrder(R: Relation, S) <=>
  and(isRelation(R, S, S),
      not(exists(x in S, y in S: areIncomparable(x, y, R))));

// x is least/greatest element in S with respect to R
pred isLeast(x, S, R) <=>
  and(in(x, S), forall(y in S: in(tuple(x, y), R)));
pred isGreatest(x, S, R) <=>
  and(in(x, S), forall(y in S: in(tuple(y, x), R)));

// x is minimal/maximal element of S with respect to R
pred isMinimal(x, S, R) <=>
  and(in(x, S), forall(y in S: 
    implies(in(tuple(y, x), R), =(y, x))));
pred isMaximal(x, S, R) <=>
  and(in(x, S), forall(y in S: 
    implies(in(tuple(x, y), R), =(x, y))));

// x is lower/upper bound of S with respect to R
pred isLowerBound(x, S, R) <=>
  forall(y in S: in(tuple(x, y), R));
pred isUpperBound(x, S, R) <=>
  forall(y in S: in(tuple(y, x), R));

// x is infimum/supremum of S with respect to R
pred isInfimum(x, S, R) <=>
  and(isLowerBound(x, S, R),
      forall(y in domain(R): 
        implies(isLowerBound(y, S, R), in(tuple(y, x), R))));
pred isSupremum(x, S, R) <=>
  and(isUpperBound(x, S, R),
      forall(y in range(R): 
        implies(isUpperBound(y, S, R), in(tuple(x, y), R))));

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