% <pre> small theory of transition relations

transitions [states: TYPE+, 
             INIT: pred[states],
             REL: pred [ [states, states] ]
            ]: THEORY
BEGIN

  % To prove that a property P is an invariant, we prove it is *inductive*
  % This is similar to Amir Pnueli's rule for Universal Invariance
  % Except that we strengthen the actual property rather than have an auxiliary

  indinv(P: pred[states]): bool =
    (FORALL (s: states): INIT(s) => P(s))
      AND (FORALL (pre, post: states): P(pre) AND REL(pre, post) => P(post))

  s, t: VAR states

  REACHABLE(s): INDUCTIVE bool =
     INIT(s) OR (EXISTS t: REACHABLE(t) AND REL(t,s))

  P: VAR pred[states]

  invariant(P): bool = FORALL s: REACHABLE(s) => P(s)

  indinv_is_invariant: LEMMA indinv(P) => invariant(P)

  invariant_closed_on_reachable: LEMMA invariant(P) =>
     FORALL t: (EXISTS s: REACHABLE(s) AND P(s) AND REL(s, t)) => P(t)

END transitions