## Diff of /thys/TLA/State.thy [000000] .. [f01853]  Maximize  Restore

### Switch to side-by-side view

--- a
+++ b/thys/TLA/State.thy
@@ -0,0 +1,208 @@
+(*  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>
+*)
+
+header {* 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 @{text world} class to enable
+  use with the @{text 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'' @{text basevars}, which is defined here.
+*}
+
+definition stvars    :: "'a statefun \<Rightarrow> bool"
+where basevars_def:  "stvars \<equiv> surj"
+
+syntax
+  "PRED"    :: "lift \<Rightarrow> 'a"                          ("PRED _")
+  "_stvars" :: "lift \<Rightarrow> bool"                        ("basevars _")
+
+translations
+  "PRED P"   \<rightharpoonup>  "(P::state => _)"
+  "_stvars"  \<rightleftharpoons>  "CONST stvars"
+
+text {*
+  Base variables may be assigned arbitrary (type-correct) values.
+  In the following lemma, note that @{text 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 \<Longrightarrow> \<exists>u. vs u = c"
+proof (unfold basevars_def surj_def)
+  assume "\<forall>y. \<exists>x. y = vs x"
+  then obtain x where "c = vs x" by blast
+  thus "\<exists>u. vs u = c" by blast
+qed
+
+lemma baseE:
+  assumes H1: "basevars v" and H2:"\<And>x. v x = c \<Longrightarrow> 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: "\<And>x. v (first x) = c \<Longrightarrow> 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 \<in> 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 \<in> range y" by auto
+qed
+
+lemma base_pair: "basevars (x,y) \<Longrightarrow> basevars x \<and> 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 @{text basevars}. The following theorem can sometimes
+  be useful because it gives a trivial solution for @{text basevars} premises.
+*}
+
+lemma unit_base: "basevars (v::state \<Rightarrow> unit)"
+  by (auto simp: basevars_def)
+
+text {*
+  A pair of the form @{text "(x,x)"} will generally not satisfy the predicate
+  @{text basevars} -- except for pathological cases such as @{text "x::unit"}.
+*}
+lemma
+  fixes x :: "state \<Rightarrow> bool"
+  assumes h1: "basevars (x,x)"
+  shows "False"
+proof -
+  from h1 have "\<exists>u. (LIFT (x,x)) u = (False,True)" by (rule basevars)
+  thus False by auto
+qed
+
+lemma
+  fixes x :: "state \<Rightarrow> nat"
+  assumes h1: "basevars (x,x)"
+  shows "False"
+proof -
+  from h1 have "\<exists>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 @{text c} at the successor state for the base variables of the
+  specification. This rule is intended for reasoning about standard TLA
+  specifications, where @{text Enabled} is applied to actions, not arbitrary
+  pre-formulas.
+*}
+lemma base_enabled:
+  assumes h1: "basevars vs"
+  and h2: "\<And>u. vs (first u) = c \<Longrightarrow> ((first s) ## u) \<Turnstile> F"
+  shows "s \<Turnstile> Enabled F"
+using h1 proof (rule first_baseE)
+  fix t
+  assume "vs (first t) = c"
+  hence "((first s) ## t) \<Turnstile> F" by (rule h2)
+  thus "s \<Turnstile> 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 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 \<Rightarrow> temporal) \<Rightarrow> temporal"       (binder "Eex " 10)
+  AAll       :: "('a statefun \<Rightarrow> temporal) \<Rightarrow> temporal"       (binder "Aall " 10)
+
+syntax
+ "_EEx"     :: "[idts, lift] \<Rightarrow> lift"                ("(3EEX _./ _)" [0,10] 10)
+  "_AAll"    :: "[idts, lift] \<Rightarrow> lift"                ("(3AALL _./ _)" [0,10] 10)
+
+translations
+  "_EEx v A"  ==   "Eex v. A"
+  "_AAll v A" ==   "Aall v. A"
+
+syntax (xsymbols)
+  "_EEx"     :: "[idts, lift] => lift"                ("(3\<exists>\<exists> _./ _)" [0,10] 10)
+  "_AAll"    :: "[idts, lift] => lift"                ("(3\<forall>\<forall> _./ _)" [0,10] 10)
+
+axiomatization where
+     eexI: "\<turnstile> F x \<longrightarrow> (\<exists>\<exists> x. F x)"
+and  eexE: "\<lbrakk>s \<Turnstile> (\<exists>\<exists> x. F x) ; basevars vs; (!! x. \<lbrakk> basevars (x,vs); s \<Turnstile> F x \<rbrakk> \<Longrightarrow> s \<Turnstile> G)\<rbrakk>
+            \<Longrightarrow> (s \<Turnstile> G)"
+and  all_def: "\<turnstile> (\<forall>\<forall> x. F x) = (\<not>(\<exists>\<exists> x. \<not>(F x)))"
+and  eexSTUT: "STUTINV F x \<Longrightarrow> STUTINV (\<exists>\<exists> x. F x)"
+and  history: "\<turnstile> (I \<and> \<box>[A]_v) = (\<exists>\<exists> h. (\$h = ha) \<and> I \<and> \<box>[A \<and> h\$=hb]_(h,v))"
+
+lemmas eexI_unl = eexI[unlift_rule] --{* @{text "w \<Turnstile> F x \<Longrightarrow> w \<Turnstile> (\<exists>\<exists> x. F x)"} *}
+
+text {*
+  @{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