Quelle  admissible.pvs

%------------------------------------------------------------------------------
% Admissible Predicates
%
%     Author: David Lester, Manchester University, NIA, Universite Perpignan
%
% If a predicate is "admissible" then we have an induction principle for
% fixpoints (fixpoint_induction).
%
%     Version 1.0            1/11/06  Initial Version
%------------------------------------------------------------------------------

admissible[T:TYPE+, (IMPORTING orders@directed_orders[T])
          <=:(pointed_directed_complete_partial_order?[T])]: THEORY

BEGIN

  IMPORTING fixpoints[T,<=]

  x:   VAR T
  D:   VAR set[T]
  q:   VAR pred[T]
  phi: VAR (increasing?[T,T,<=,<=])

% An admissible predicate is a lub-preserving function between T and the
% special two-point pointed DCPO: TRUE < FALSE, that is also TRUE for bottom.

  IMPORTING scott[bool,when], scott_continuity[T,bool,<=,when]

  admissible_pred?(p:pred[T]):bool
   = FORALL D: empty?(D) OR directed?(D) => (FORALL (x:(D)): p(x)) => p(lub(D))

  admissible_pred: TYPE+ = (admissible_pred?) CONTAINING (LAMBDA x: TRUE)

  p: VAR admissible_pred

  fixpoint_induction: LEMMA (FORALL x: p(x) => p(phi(x))) => p(fix(phi))

END admissible