% 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