Quelle  State.thy

(*  Title:       A Definitional Encoding of TLA in Isabelle/HOL
    Authors:     Gudmund Grov <ggrov at inf.ed.ac.uk>
                 Stephan Merz <Stephan.Merz at loria.fr>
    Year:        2011
    Maintainer:  Gudmund Grov <ggrov at inf.ed.ac.uk>
*)

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 "w ⊨ F x ==> w ⊨ (∃∃ x. F x)"}›

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