Theory State
section ‹Representing state in TLA*›
theory State
imports Liveness
begin
text‹
We adopt the hidden state appraoch, as used in the existing
Isabelle/HOL TLA embedding \<^cite>‹"Merz98"›. This approach is also used
in \<^cite>‹"Ehmety01"›.
Here, a state space is defined by its projections, and everything else is
unknown. Thus, a variable is a projection of the state space, and has the same
type as a state function. Moreover, strong typing is achieved, since the projection
function may have any result type. To achieve this, the state space is represented
by an undefined type, which is an instance of the ‹world› class to enable
use with the ‹Intensional› theory.
›
typedecl state
instance state :: world ..
type_synonym 'a statefun = "(state,'a) stfun"
type_synonym statepred = "bool statefun"
type_synonym 'a tempfun = "(state,'a) formfun"
type_synonym temporal = "state formula"
text ‹
Formalizing type state would require formulas to be tagged with
their underlying state space and would result in a system that is
much harder to use. (Unlike Hoare logic or Unity, TLA has quantification
over state variables, and therefore one usually works with different
state spaces within a single specification.) Instead, state is just
an anonymous type whose only purpose is to provide Skolem constants.
Moreover, we do not define a type of state variables separate from that
of arbitrary state functions, again in order to simplify the definition
of flexible quantification later on. Nevertheless, we need to distinguish
state variables, mainly to define the enabledness of actions. The user
identifies (tuples of) ``base'' state variables in a specification via the
``meta predicate'' ‹basevars›, which is defined here.
›
definition stvars :: "'a statefun ⇒ bool"
where basevars_def: "stvars ≡ surj"
syntax
"PRED" :: "lift ⇒ 'a" ("PRED _")
"_stvars" :: "lift ⇒ bool" ("basevars _")
translations
"PRED P" ⇀ "(P::state => _)"
"_stvars" ⇌ "CONST stvars"
text ‹
Base variables may be assigned arbitrary (type-correct) values.
In the following lemma, note that ‹vs› may be a tuple of variables.
The correct identification of base variables is up to the user who must
take care not to introduce an inconsistency. For example, @{term "basevars (x,x)"}
would definitely be inconsistent.
›
lemma basevars: "basevars vs ⟹ ∃u. vs u = c"
proof (unfold basevars_def surj_def)
assume "∀y. ∃x. y = vs x"
then obtain x where "c = vs x" by blast
thus "∃u. vs u = c" by blast
qed
lemma baseE:
assumes H1: "basevars v" and H2:"⋀x. v x = c ⟹ Q"
shows "Q"
using H1[THEN basevars] H2 by auto
text ‹A variant written for sequences rather than single states.›
lemma first_baseE:
assumes H1: "basevars v" and H2: "⋀x. v (first x) = c ⟹ Q"
shows "Q"
using H1[THEN basevars] H2 by (force simp: first_def)
lemma base_pair1:
assumes h: "basevars (x,y)"
shows "basevars x"
proof (auto simp: basevars_def)
fix c
from h[THEN basevars] obtain s where "(LIFT (x,y)) s = (c, arbitrary)" by auto
thus "c ∈ range x" by auto
qed
lemma base_pair2:
assumes h: "basevars (x,y)"
shows "basevars y"
proof (auto simp: basevars_def)
fix d
from h[THEN basevars] obtain s where "(LIFT (x,y)) s = (arbitrary, d)" by auto
thus "d ∈ range y" by auto
qed
lemma base_pair: "basevars (x,y) ⟹ basevars x ∧ basevars y"
by (auto elim: base_pair1 base_pair2)
text ‹
Since the @{typ unit} type has just one value, any state function of unit type
satisfies the predicate ‹basevars›. The following theorem can sometimes
be useful because it gives a trivial solution for ‹basevars› premises.
›
lemma unit_base: "basevars (v::state ⇒ unit)"
by (auto simp: basevars_def)
text ‹
A pair of the form ‹(x,x)› will generally not satisfy the predicate
‹basevars› -- except for pathological cases such as ‹x::unit›.
›
lemma
fixes x :: "state ⇒ bool"
assumes h1: "basevars (x,x)"
shows "False"
proof -
from h1 have "∃u. (LIFT (x,x)) u = (False,True)" by (rule basevars)
thus False by auto
qed
lemma
fixes x :: "state ⇒ nat"
assumes h1: "basevars (x,x)"
shows "False"
proof -
from h1 have "∃u. (LIFT (x,x)) u = (0,1)" by (rule basevars)
thus False by auto
qed
text ‹
The following theorem reduces the reasoning about the existence of a
state sequence satisfiyng an enabledness predicate to finding a suitable
value ‹c› at the successor state for the base variables of the
specification. This rule is intended for reasoning about standard TLA
specifications, where ‹Enabled› is applied to actions, not arbitrary
pre-formulas.
›
lemma base_enabled:
assumes h1: "basevars vs"
and h2: "⋀u. vs (first u) = c ⟹ ((first s) ## u) ⊨ F"
shows "s ⊨ Enabled F"
using h1 proof (rule first_baseE)
fix t
assume "vs (first t) = c"
hence "((first s) ## t) ⊨ F" by (rule h2)
thus "s ⊨ Enabled F" unfolding enabled_def by blast
qed
subsection "Temporal Quantifiers"
text‹
In \<^cite>‹"Lamport94"›, Lamport gives a stuttering invariant definition
of quantification over (flexible) variables. It relies on similarity
of two sequences (as supported in our @{theory TLA.Sequence} theory), and
equivalence of two sequences up to a variable (the bound variable).
However, sequence equaivalence up to a variable, requires state
equaivalence up to a variable. Our state representation above does not
support this, hence we cannot encode Lamport's definition in our theory.
Thus, we need to axiomatise quantification over (flexible) variables.
Note that with a state representation supporting this, our theory should
allow such an encoding.
›
consts
EEx :: "('a statefun ⇒ temporal) ⇒ temporal" (binder "Eex " 10)
AAll :: "('a statefun ⇒ temporal) ⇒ temporal" (binder "Aall " 10)
syntax
"_EEx" :: "[idts, lift] => lift" ("(3∃∃ _./ _)" [0,10] 10)
"_AAll" :: "[idts, lift] => lift" ("(3∀∀ _./ _)" [0,10] 10)
translations
"_EEx v A" == "Eex v. A"
"_AAll v A" == "Aall v. A"
axiomatization where
eexI: "⊢ F x ⟶ (∃∃ x. F x)"
and eexE: "⟦s ⊨ (∃∃ x. F x) ; basevars vs; (!! x. ⟦ basevars (x,vs); s ⊨ F x ⟧ ⟹ s ⊨ G)⟧
⟹ (s ⊨ G)"
and all_def: "⊢ (∀∀ x. F x) = (¬(∃∃ x. ¬(F x)))"
and eexSTUT: "STUTINV F x ⟹ STUTINV (∃∃ x. F x)"
and history: "⊢ (I ∧ □[A]_v) = (∃∃ h. ($h = ha) ∧ I ∧ □[A ∧ h$=hb]_(h,v))"
lemmas eexI_unl = eexI[unlift_rule]
text ‹
‹tla_defs› can be used to unfold TLA definitions into lowest predicate level.
This is particularly useful for reasoning about enabledness of formulas.
›
lemmas tla_defs = unch_def before_def after_def first_def second_def suffix_def
tail_def nexts_def app_def angle_actrans_def actrans_def
end