Quelle  congruence.pvs

%------------------------------------------------------------------------------
% The Equivalence of a Direct and Continuation Semantics
%
% All references are to HR and F Nielson "Semantics with Applications:
% A Formal Introduction", John Wiley & Sons, 1992. (revised edition
% available: http://www.daimi.au.dk/~hrn )
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
%     Version 1.0            25/12/07  Initial Version
%------------------------------------------------------------------------------

congruence[V:TYPE+]: THEORY

BEGIN

  IMPORTING direct[V], continuation[V],
            scott@admissible[Cont,sq_le],
            scott@admissible[(scott_continuous?[Cont,Cont,sq_le,sq_le]),
                             (continuous_pointwise(sq_le,sq_le))]

  s:   VAR State
  c:   VAR Cont
  S:   VAR Stm
  phi: VAR scott_continuous[Cont,Cont,(sq_le),(sq_le)]
  psi: VAR Cont

  P(phi,psi):bool = FORALL c: phi(c) = c o psi

  P_bottom: LEMMA P(LAMBDA c: LAMBDA s: bottom[State], LAMBDA s: bottom[State])

  IMPORTING
  orders@product_orders[(scott_continuous?[Cont,Cont,(sq_le),(sq_le)]),Cont],
  scott@scott_continuity[[(scott_continuous?[Cont,Cont,(sq_le),(sq_le)]),Cont],
                         bool,(continuous_pointwise(sq_le,sq_le)*sq_le),when],
  scott@dual_fixpoints[(scott_continuous?[Cont,Cont,(sq_le),(sq_le)]),Cont,
                       continuous_pointwise(sq_le,sq_le),sq_le]

  admissible_P: LEMMA admissible_pred?(P)

  continuation_direct: LEMMA P(continuation.SS(S),direct.SS(S))      % N&N 4.74

END congruence