Quelle  Cont.pvs   Sprache: PVS

%------------------------------------------------------------------------------
% Continuations
%
% 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
%------------------------------------------------------------------------------

Cont[V:TYPE+]: THEORY

BEGIN

  IMPORTING State[V],
            orders@lift_props[State],
            scott@partial_function_props[State,State]

  s,s1,s2: VAR State

  Cont: TYPE+ = LiftPartialFunction[State,State] CONTAINING (LAMBDA s: bottom)

  x:       VAR V
  f:       VAR [State->int]
  c,c1,c2: VAR Cont
  p:       VAR pred[State]

  sq_le(c1,c2):bool = FORALL (s1,s2): c1(s1) = up(s2) IMPLIES c2(s1) = up(s2)

  sq_le_def: LEMMA sq_le(c1,c2) IFF
                   subset?[[State,State]](graph(c1),graph(c2))      % NN 4.8

  partial_order_sq_le: JUDGEMENT sq_le HAS_TYPE (partial_order?[Cont])

  IMPORTING orders@directed_orders[Cont],
            orders@bounded_order_props[Cont,(sq_le)]

  D: VAR set[Cont]

  lub_graph: LEMMA empty?(D) OR directed?(sq_le)(D) IMPLIES
     least_upper_bound?(from_graph(Union(image(graph,D))),D,sq_le)

  sq_le_dcpo:  JUDGEMENT
                sq_le HAS_TYPE (directed_complete_partial_order?[Cont])
  sq_le_pdcpo: JUDGEMENT
                sq_le HAS_TYPE (pointed_directed_complete_partial_order?[Cont])

  sq_le_bottom: LEMMA sq_le((LAMBDA s: bottom),c)

  sq_le_least:  LEMMA least?(fullset[Cont],sq_le)(LAMBDA s: bottom)

  conditional(p,c1,c2):Cont
    = (LAMBDA s: IF p(s) THEN c1(s) ELSE c2(s) ENDIF)

  sq_le_conditional: LEMMA sq_le(c,conditional(p,c1,c2)) IFF
    (FORALL s1,s2: (    p(s1) AND c(s1) = up(s2) IMPLIES c1(s1) = up(s2)) AND
                   (NOT p(s1) AND c(s1) = up(s2) IMPLIES c2(s1) = up(s2)))

  assign(x,f):Cont = (LAMBDA s: up(assign(x,f)(s)))

  IMPORTING scott@scott_continuity[Cont,Cont,(sq_le),(sq_le)]

  apply_continuous: LEMMA scott_continuous?(LAMBDA c: c o c1)

END Cont