% W.H. Hesselink
% First version 6th August 2003. Last modification 11 October 2006

programs [state: TYPE]: THEORY 
BEGIN

   program: TYPE = pred[[state, lift[state]]]
   prog, body, progA, progB: VAR program 
   x, y, z: VAR state 
   yy, zz: VAR lift[state]

% prog(x, yy) means: if prog starts in x it may result in yy,
% where yy = bottom means nontermination

   guard, inv, p0, p1, pre, post: VAR pred[state]
   n, i: VAR nat
   t: VAR int
   vf: VAR [state -> int]

   AND (p0, p1): pred[state] = {x | p0 (x) AND p1(x)}
   NOT (p0): pred[state] = {x | NOT p0 (x)}

% NOTE that these functions AND and NOT are lifted versions of the boolean 
% operators with the same names. Therefore you may have to expand them at 
% unexpected points! Moreover, this AND can serve as an infix operator.

   ifThenElse (guard, progA, progB): program =
      { (x, yy) |
         IF guard (x) THEN progA (x,yy) ELSE progB (x, yy) ENDIF } ;
      
   ^ (progA, progB): program =   % sequential composition (infix)
      { (x, yy) |
         yy = bottom and progA (x, yy) 
         OR (EXISTS (z): progA (x, up(z)) and progB (z, yy)) }
      
   while (guard, body): program =
      { (x, yy) | EXISTS (ss: sequence[state]):
         ss(0) = x and 
         ((EXISTS (n): 
             (FORALL (i): i< n implies 
                guard (ss (i)) and body (ss(i), up(ss(i+1))) )
             and ((not guard (ss(n)) and yy = up (ss (n)))
                  or (guard (ss(n)) and body (ss (n), bottom) 
                      and yy = bottom ) ) )
          or (yy = bottom and 
              FORALL (i): guard (ss (i)) and 
                          body (ss(i), up(ss(i+1))) ) )  }

   tcHoare (pre, prog, post): bool = % total correctness Hoare triple
      (FORALL (x): pre (x) IMPLIES 
         NOT prog (x, bottom) AND 
         FORALL (y): prog (x, up (y)) IMPLIES post (y) ) 

   up_injective: LEMMA (up (x) = up (y) IMPLIES x = y)

   tcHoareWeakening: LEMMA
      tcHoare (p0, prog, p1) AND subset?(pre, p0) AND subset?(p1, post) 
      IMPLIES tcHoare (pre, prog, post)

   tcHoareComposition: LEMMA
      tcHoare (pre, progA, p0) AND tcHoare (p0, progB, post)
      IMPLIES tcHoare (pre, progA ^ progB, post)

   isVariant (vf, inv, guard, body): bool =
      (FORALL (x): inv (x) AND guard (x) IMPLIES 
         vf (x) >= 0 AND 
         FORALL (y): body (x, up (y)) IMPLIES vf (y) < vf (x) ) 

   whileTheorem: THEOREM
      tcHoare (inv and guard, body, inv) 
      AND isVariant (vf, inv, guard, body)
      IMPLIES tcHoare (inv, while (guard, body), inv and not (guard))

% A special theory for deterministic, terminating programs: "commands"

   command: TYPE = [state -> state]
   com, comA, comB: VAR command 

   lift (com): program = { (x, yy) | yy = up (com (x)) }

   tcHoare (pre, com, post): bool = 
      (FORALL (x): pre (x) IMPLIES post (com (x))) 

   com_prog_tcHoare: LEMMA
      tcHoare (pre, com, post) IMPLIES tcHoare (pre, lift (com), post)

   isVariant (vf, inv, guard, com): bool =
      (FORALL (x): inv (x) AND guard (x) IMPLIES 
         vf (x) >= 0 AND vf (com (x)) < vf (x) ) 

   com_prog_isVariant: LEMMA
      isVariant (vf, inv, guard, com) IMPLIES 
      isVariant (vf, inv, guard, lift (com))

   ifThenElse (guard, comA, comB): command =
      {x | IF guard (x) THEN comA (x) ELSE comB (x) ENDIF } ;

   ^ (comA, comB): command = comB o comA  
   % Sequential composition, see prelude. Note the reversal.

   com_prog_ifThenElse: LEMMA 
      lift (ifThenElse (guard, comA, comB)) = 
         ifThenElse (guard, lift (comA), lift (comB))

   com_prog_composition: LEMMA 
      lift (comA ^ comB) = lift (comA) ^ lift (comB)

% Conditional correctness allows nontermination

   ccHoare (pre, prog, post): boolean =
      (FORALL (x, y): pre (x) AND prog (x, up (y)) IMPLIES post (y)) 

   ccHoare_implied: LEMMA
      tcHoare (pre, prog, post) IMPLIES ccHoare (pre, prog, post)

   com_prog_ccHoare: LEMMA
      tcHoare (pre, com, post) IMPLIES ccHoare (pre, lift (com), post)

   ccHoareWeakening: LEMMA
      ccHoare (p0, prog, p1) AND subset?(pre, p0) AND subset?(p1, post) 
      IMPLIES ccHoare (pre, prog, post)

   mixedHoareConjunction: LEMMA
      tcHoare (pre, prog, post) AND ccHoare (p0, prog, p1) 
      IMPLIES tcHoare (pre AND p0, prog, post AND p1)

   ccHoareComposition: LEMMA
      ccHoare (pre, progA, p0) AND ccHoare (p0, progB, post)
      IMPLIES ccHoare (pre, progA ^ progB, post)

   ccWhileTheorem: THEOREM
      ccHoare (inv and guard, body, inv)
      IMPLIES ccHoare (inv, while (guard, body), inv and not guard)

   boundedBy (vf, t): pred[state] = {x | vf (x) <= t}

   isVariant_implied: LEMMA   
      (FORALL (x): inv (x) AND guard (x) IMPLIES vf (x) >= 0) AND 
      (FORALL (n): ccHoare (inv AND guard AND boundedBy (vf, n), 
                            body, boundedBy (vf, n - 1) ) )
      IMPLIES isVariant (vf, inv, guard, body) 
END programs