Go backward to C.8 More on Functions Go up to C Logic Evaluator Definitions Go forward to C.10 Equivalence Relations

C.9 Real Functions

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

read real;
read function;

// is B upper/lower bound of s in first n members of sequence s?
pred isUpperBound(B, s, n) <=> 
  forall(i in nat(0, n): <=R(apply(s, i), B));
pred isLowerBound(B, s, n) <=>
  forall(i in nat(0, n): <=R(B, apply(s, i)));

// supremum/infimum of s considering only the first n members
fun sup(s, n) = 
  such(U in range(s):
    and(isUpperBound(U, s, n),
      forall(U' in range(s):
        implies(isUpperBound(U', s, n), <=R(U, U')))), U);
fun inf(s, n) = 
  such(L in range(s):
    and(isLowerBound(L, s, n),
      forall(L' in range(s): 
        implies(isLowerBound(L', s, n), <=R(L', L)))), L);

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