% if <= is a complete lower semilattice on T and f is a monotone function from
% T to T, then f is a least fixed point of x iff f is the least prefixed point.
%
% Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace
% Date: Nov 2004

fixed_points[T: TYPE+]: THEORY

BEGIN

  IMPORTING minmax_orders[T]

  R: VAR pred[[T, T]]
  <=: VAR (complete_lower_semilattice?[T])
  x, y: VAR T
  f: VAR [T -> T]

  monotone?(R)(f): bool = FORALL x, y: R(x, y) => R(f(x), f(y))
  fixed_point?(f)(x): bool = (f(x) = x)
  prefixed_point?(R)(f)(x): bool = R(f(x), x)
  lfp?(R)(f)(x): bool = least?(fixed_point?(f), R)(x)

  prefixed_points_closed: LEMMA
    FORALL (f: (monotone?(<=))):
      prefixed_point?(<=)(f)(x) => prefixed_point?(<=)(f)(f(x))

  prefixed_points_lower_bounds: LEMMA
    FORALL (f: (monotone?(<=))):
      lower_bound?[T](x, prefixed_point?(<=)(f), <=) =>
        lower_bound?[T](f(x), prefixed_point?(<=)(f), <=)

  least_prefixed_point_is_fixed_point: LEMMA
    FORALL (f: (monotone?(<=))):
      greatest_lower_bound?[T](x, prefixed_point?(<=)(f), <=) =>
        fixed_point?(f)(x)

  least_fixed_point_le_prefixed_points: LEMMA
    FORALL (f: (monotone?(<=))):
      lfp?(<=)(f)(x) => lower_bound?[T](x, prefixed_point?(<=)(f), <=)

  least_prefixed_point: THEOREM
    FORALL (f: (monotone?(<=))):
      lfp?(<=)(f)(x) IFF greatest_lower_bound?[T](x, prefixed_point?(<=)(f), <=)

  least_fixed_point_exists: COROLLARY
    FORALL (f: (monotone?(<=))):
      nonempty?(lfp?(<=)(f))

  least_fixed_point_unique: COROLLARY
    FORALL (f: (monotone?(<=))):
      unique?(lfp?(<=)(f))

END fixed_points