Theory Semantics

(*  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 ‹Semantics› 

theory Semantics
imports Sequence Intensional
begin

text ‹
  This theory mechanises a \emph{shallow} embedding of \tlastar{} using the
  ‹Sequence› and ‹Intensional› theories. A shallow embedding
  represents \tlastar{} using Isabelle/HOL predicates, while a \emph{deep}
  embedding would represent \tlastar{} formulas and pre-formulas as mutually
  inductive datatypes\footnote{See e.g. \<^cite>‹"Wildmoser04"› for a discussion
  about deep vs. shallow embeddings in Isabelle/HOL.}.  
  The choice of a shallow over a deep embedding is motivated by the following 
  factors: a shallow embedding is usually less involved, and existing Isabelle
  theories and tools can be applied more directly to enhance automation; due to
  the lifting in the ‹Intensional› theory, a shallow embedding can reuse
  standard logical operators, whilst a deep embedding requires a different
  set of operators for both formulas and pre-formulas. Finally, since our 
  target is system verification rather than proving meta-properties of \tlastar{},
  which requires a deep embedding, a shallow embedding is more fit for purpose.
›

subsection "Types of Formulas"

text ‹
  To mechanise the \tlastar{} semantics, the following
  type abbreviations are used:
›

type_synonym ('a,'b) formfun = "'a seq ⇒ 'b"
type_synonym 'a formula = "('a,bool) formfun"
type_synonym ('a,'b) stfun = "'a ⇒ 'b"
type_synonym 'a stpred = "('a,bool) stfun"

instance 
 "fun" :: (type,type) world ..

instance
 "prod" :: (type,type) world ..

text ‹
  Pair and function are instantiated to be of type class world.
  This allows use of the lifted intensional logic for formulas, and 
  standard logical connectives can therefore be used.
›

subsection "Semantics of TLA*"

text ‹The semantics of \tlastar{} is defined.›

definition always :: "('a::world) formula ⇒ 'a formula" 
where "always F ≡ λ s. ∀ n. (s |⇩s n) ⊨ F"

definition nexts :: "('a::world) formula ⇒ 'a formula" 
where "nexts F ≡ λ s. (tail s) ⊨ F"

definition before :: "('a::world,'b) stfun ⇒ ('a,'b) formfun"
where "before f ≡ λ s. (first s) ⊨ f"

definition after :: "('a::world,'b) stfun ⇒ ('a,'b) formfun"
where "after f ≡ λ s. (second s) ⊨ f" 

definition unch  :: "('a::world,'b) stfun ⇒ 'a formula" 
where "unch v ≡ λ s. s ⊨ (after v) = (before v)"

definition action :: "('a::world) formula ⇒ ('a,'b) stfun ⇒ 'a formula"
where "action P v ≡ λ s. ∀ i. ((s |⇩s i) ⊨ P) ∨ ((s |⇩s i) ⊨ unch v)"

subsubsection "Concrete Syntax"

text‹This is the concrete syntax for the (abstract) operators above.›

syntax
 "_always" :: "lift ⇒ lift" (‹(□_)› [90] 90) 
 "_nexts" :: "lift ⇒ lift" (‹(○_)› [90] 90) 
 "_action" :: "[lift,lift] ⇒ lift" (‹(□[_]'_(_))› [20,1000] 90)
 "_before"    :: "lift ⇒ lift"  (‹($_)› [100] 99)
 "_after"     :: "lift ⇒ lift"  (‹(_$)› [100] 99)
 "_prime"     :: "lift ⇒ lift"  (‹(_`)› [100] 99)  
 "_unch"     :: "lift ⇒ lift"  (‹(Unchanged _)› [100] 99) 
 "TEMP"  :: "lift ⇒ 'b" (‹(TEMP _)›)

syntax (ASCII)
 "_always" :: "lift ⇒ lift" (‹([]_)› [90] 90)
 "_nexts" :: "lift ⇒ lift" (‹(Next _)› [90] 90)
 "_action" :: "[lift,lift] ⇒ lift" (‹([][_]'_(_))› [20,1000] 90)

translations
 "_always" ⇌ "CONST always"
 "_nexts" ⇌ "CONST nexts"
 "_action" ⇌ "CONST action"
 "_before"    ⇌ "CONST before" 
 "_after"     ⇌ "CONST after" 
 "_prime"     ⇀ "CONST after"
 "_unch"     ⇌ "CONST unch" 
 "TEMP F" ⇀ "(F:: (nat ⇒ _) ⇒ _)"


subsection "Abbreviations"

text ‹Some standard temporal abbreviations, with their concrete syntax.›

definition actrans :: "('a::world) formula ⇒ ('a,'b) stfun ⇒ 'a formula"
where "actrans P v ≡ TEMP(P ∨ unch v)"

definition eventually :: "('a::world) formula ⇒ 'a formula"
where "eventually F ≡ LIFT(¬□(¬F))"

definition angle_action :: "('a::world) formula ⇒ ('a,'b) stfun ⇒ 'a formula"
where "angle_action P v ≡ LIFT(¬□[¬P]_v)"

definition angle_actrans :: "('a::world) formula ⇒ ('a,'b) stfun ⇒ 'a formula"
where "angle_actrans P v ≡ TEMP (¬ actrans (LIFT(¬P)) v)"

definition leadsto :: "('a::world) formula ⇒ 'a formula ⇒ 'a formula"
where "leadsto P Q ≡ LIFT □(P ⟶ eventually Q)"

subsubsection "Concrete Syntax"

syntax (ASCII)
  "_actrans" :: "[lift,lift] ⇒ lift" (‹([_]'_(_))›  [20,1000] 90)
  "_eventually" :: "lift ⇒ lift" (‹(<>_)› [90] 90)
  "_angle_action" :: "[lift,lift] ⇒ lift" (‹(<><_>'_(_))› [20,1000] 90)
  "_angle_actrans" :: "[lift,lift] ⇒ lift" (‹(<_>'_(_))› [20,1000] 90)
  "_leadsto" :: "[lift,lift] ⇒ lift" (‹(_ ~> _)› [26,25] 25)

syntax
  "_eventually" :: "lift ⇒ lift" (‹(◇_)› [90] 90)
  "_angle_action" :: "[lift,lift] ⇒ lift" (‹(◇⟨_⟩'_(_))› [20,1000] 90)
  "_angle_actrans" :: "[lift,lift] ⇒ lift" (‹(⟨_⟩'_(_))› [20,1000] 90)
  "_leadsto" :: "[lift,lift] ⇒ lift" (‹(_ ↝ _)› [26,25] 25)

translations 
  "_actrans" ⇌ "CONST actrans"
  "_eventually" ⇌ "CONST eventually"
  "_angle_action" ⇌ "CONST angle_action"
  "_angle_actrans" ⇌ "CONST angle_actrans"
  "_leadsto" ⇌ "CONST leadsto"


subsection "Properties of Operators"

text ‹The following lemmas show that these operators have the expected semantics.›

lemma eventually_defs: "(w ⊨ ◇ F) = (∃ n. (w |⇩s n) ⊨ F)"
  by (simp add: eventually_def always_def)

lemma angle_action_defs: "(w ⊨ ◇⟨P⟩_v) = (∃ i. ((w |⇩s i) ⊨ P) ∧ ((w |⇩s i) ⊨ v$ ≠ $v))"
  by (simp add: angle_action_def action_def unch_def)

lemma unch_defs: "(w ⊨ Unchanged v) = (((second w) ⊨ v) = ((first w) ⊨ v))"
  by (simp add: unch_def before_def nexts_def after_def tail_def suffix_def first_def second_def)

lemma linalw:
  assumes h1: "a ≤ b" and h2: "(w |⇩s a) ⊨ □A"
  shows "(w |⇩s b) ⊨ □A"
proof (clarsimp simp: always_def)
  fix n
  from h1 obtain k where g1: "b = a + k" by (auto simp: le_iff_add)
  with h2 show "(w |⇩s b |⇩s n) ⊨ A" by (auto simp: always_def suffix_plus ac_simps)
qed

subsection "Invariance Under Stuttering"

text ‹
  A key feature of \tlastar{} is that specification at different abstraction
  levels can be compared. The soundness of this relies on the stuttering invariance 
  of formulas. Since the embedding is shallow, it cannot be shown that a generic 
  \tlastar{} formula is stuttering invariant. However, this section will show that 
  each operator is stuttering invariant or preserves stuttering invariance in an
  appropriate sense, which can be used to show stuttering invariance
  for given specifications. 

  Formula ‹F› is stuttering invariant if for any two similar behaviours
  (i.e., sequences of states), ‹F› holds in one iff it holds in the other.
  The definition is generalised to arbitrary expressions, and not just predicates.
›

definition stutinv :: "('a,'b) formfun ⇒ bool"
where "stutinv F ≡ ∀ σ τ. σ ≈ τ ⟶ (σ ⊨ F) = (τ ⊨ F)"

text‹
  The requirement for stuttering invariance is too strong for pre-formulas. 
  For example, an action formula specifies a relation between the first two states
  of a behaviour, and will rarely be satisfied by a stuttering step. This is why
  pre-formulas are ``protected'' by (square or angle) brackets in \tlastar{}:
  the only place a pre-formula ‹P› can be used is inside an action:
  ‹□[P]_v›.
  To show that ‹□[P]_v› is stuttering invariant, is must be shown that a 
  slightly weaker predicate holds for @{term P}. For example, if @{term P} contains 
  a term of the form ‹○○Q›, then it is not a well-formed pre-formula, thus 
  ‹□[P]_v› is not stuttering invariant. This weaker version of
  stuttering invariance has been named \emph{near stuttering invariance}.
›

definition nstutinv :: "('a,'b) formfun ⇒ bool"
where "nstutinv P ≡ ∀ σ τ. (first σ = first τ) ∧ (tail σ) ≈ (tail τ) ⟶ (σ ⊨ P) = (τ ⊨ P)"

syntax
  "_stutinv" :: "lift ⇒ bool" (‹(STUTINV _)› [40] 40)
  "_nstutinv" :: "lift ⇒ bool" (‹(NSTUTINV _)› [40] 40)

translations
  "_stutinv" ⇌ "CONST stutinv"
  "_nstutinv" ⇌ "CONST nstutinv"


text ‹
  Predicate @{term "stutinv F"} formalises stuttering invariance for
  formula @{term F}. That is if two sequences are similar @{term "s ≈ t"} (equal up
  to stuttering) then the validity of @{term F} under both @{term s} and @{term t}
  are equivalent. Predicate @{term "nstutinv P"} should be read as \emph{nearly
  stuttering invariant} -- and is required for some stuttering invariance proofs.
›

lemma stutinv_strictly_stronger: 
  assumes h: "STUTINV F" shows "NSTUTINV F"
  unfolding nstutinv_def
proof (clarify)
  fix s t :: "nat ⇒ 'a"
  assume a1: "first s = first t" and a2: "(tail s) ≈ (tail t)"
  have "s ≈ t"
  proof -
    have tg1: "(first s) ## (tail s) = s" by (rule seq_app_first_tail)
    have tg2: "(first t) ## (tail t) = t" by (rule seq_app_first_tail)
    with a1 have tg2': "(first s) ## (tail t) = t" by simp
    from a2 have "(first s) ## (tail s) ≈ (first s) ## (tail t)" by (rule app_seqsimilar)
    with tg1 tg2' show ?thesis by simp
  qed
  with h show "(s ⊨ F) = (t ⊨ F)" by (simp add: stutinv_def)
qed

subsubsection "Properties of @{term stutinv}"

text ‹
  This subsection proves stuttering invariance, preservation of stuttering invariance
  and introduction of stuttering invariance for different formulas. 
  First, state predicates are stuttering invariant.
›

theorem stut_before: "STUTINV $F"
proof (clarsimp simp: stutinv_def)
  fix s t :: "'a seq"
  assume a1: "s ≈ t"
  hence "(first s) = (first t)" by (rule sim_first)
  thus "(s ⊨ $F) = (t ⊨ $F)" by (simp add: before_def)
qed

lemma nstut_after: "NSTUTINV F$"
proof (clarsimp simp: nstutinv_def)
  fix s t :: "'a seq"
  assume a1: "tail s ≈ tail t"
  thus "(s ⊨ F$) = (t ⊨ F$)" by (simp add: after_def tail_sim_second)
qed

text‹The always operator preserves stuttering invariance.›

theorem stut_always: assumes H:"STUTINV F" shows "STUTINV □F"
proof (clarsimp simp: stutinv_def)
  fix s t :: "'a seq"
  assume a2: "s ≈ t"
  show "(s ⊨ (□ F)) = (t ⊨ (□ F))"
  proof 
    assume a1: "t ⊨ □ F"
    show "s ⊨ □ F"
    proof (clarsimp simp: always_def)
      fix n
      from a2[THEN sim_step] obtain m where m: "s |⇩s n ≈ t |⇩s m" by blast
      from a1 have "(t |⇩s m) ⊨ F" by (simp add: always_def)
      with H m show "(s |⇩s n) ⊨ F" by (simp add: stutinv_def)
    qed
  next
    assume a1: "s ⊨ (□ F)"
    show "t ⊨ (□ F)"
    proof (clarsimp simp: always_def)
      fix n
      from a2[THEN seqsim_sym, THEN sim_step] obtain m where m: "t |⇩s n ≈ s |⇩s m" by blast
      from a1 have "(s |⇩s m) ⊨ F" by (simp add: always_def)
      with H m show "(t |⇩s n) ⊨ F" by (simp add: stutinv_def)
    qed
  qed
qed

text ‹
  Assuming that formula @{term P} is nearly suttering invariant
  then ‹□[P]_v› will be stuttering invariant.
›

lemma stut_action_lemma:
  assumes H: "NSTUTINV P" and st: "s ≈ t" and P: "t ⊨ □[P]_v"
  shows "s ⊨ □[P]_v"
proof (clarsimp simp: action_def)
  fix n
  assume "¬ ((s |⇩s n) ⊨ Unchanged v)"
  hence v: "v (s (Suc n)) ≠ v (s n)" 
    by (simp add: unch_defs first_def second_def suffix_def)
  from st[THEN sim_step] obtain m where
    a2': "s |⇩s n ≈ t |⇩s m 
          ∧ (s |⇩s Suc n ≈ t |⇩s Suc m ∨ s |⇩s Suc n ≈ t |⇩s m)" ..
  hence g1: "(s |⇩s n ≈ t |⇩s m)" by simp
  hence g1'': "first (s |⇩s n) = first (t |⇩s m)" by (simp add: sim_first)
  hence g1': "s n = t m" by (simp add: suffix_def first_def)
  from a2' have g2: "s |⇩s Suc n ≈ t |⇩s Suc m ∨ s |⇩s Suc n ≈ t |⇩s m" by simp
  from P have a1': "((t |⇩s m) ⊨ P) ∨ ((t |⇩s m) ⊨ Unchanged v)" by (simp add: action_def)
  from g2 show "(s |⇩s n) ⊨ P"
  proof
    assume "s |⇩s Suc n ≈ t |⇩s m"
    hence "first (s |⇩s Suc n) = first (t |⇩s m)" by (simp add: sim_first)
    hence "s (Suc n) = t m" by (simp add: suffix_def first_def)
    with g1' v show ?thesis by simp  ― ‹by contradiction›
  next
    assume a3: "s |⇩s Suc n ≈ t |⇩s Suc m"
    hence "first (s |⇩s Suc n) = first (t |⇩s Suc m)" by (simp add: sim_first)
    hence a3': "s (Suc n) = t (Suc m)" by (simp add: suffix_def first_def)
    from a1' show ?thesis
    proof
      assume "(t |⇩s m) ⊨ Unchanged v"
      hence "v (t (Suc m)) = v (t m)"
        by (simp add: unch_defs first_def second_def suffix_def)
      with g1' a3' v show ?thesis by simp  ― ‹again, by contradiction›
    next
      assume a4: "(t |⇩s m) ⊨ P"
      from a3 have "tail (s |⇩s n) ≈ tail (t |⇩s m)" by (simp add: tail_def suffix_plus)
      with H g1'' a4 show ?thesis by (auto simp: nstutinv_def)
    qed
  qed
qed

theorem stut_action: assumes H: "NSTUTINV P" shows "STUTINV □[P]_v"
proof (clarsimp simp: stutinv_def)
  fix s t :: "'a seq"
  assume st: "s ≈ t"
  show "(s ⊨ □[P]_v) = (t ⊨ □[P]_v)"
  proof
    assume "t ⊨ □[P]_v"
    with H st show "s ⊨ □[P]_v" by (rule stut_action_lemma)
  next
    assume "s ⊨ □[P]_v"
    with H st[THEN seqsim_sym] show "t ⊨ □[P]_v" by (rule stut_action_lemma)
  qed
qed

text ‹
  The lemmas below shows that propositional and predicate operators 
  preserve stuttering invariance.
›

lemma stut_and: "⟦STUTINV F;STUTINV G⟧ ⟹ STUTINV (F ∧ G)"
  by (simp add: stutinv_def)

lemma stut_or: "⟦STUTINV F;STUTINV G⟧ ⟹ STUTINV (F ∨ G)"
  by (simp add: stutinv_def)

lemma stut_imp: "⟦STUTINV F;STUTINV G⟧ ⟹ STUTINV (F ⟶ G)"
  by (simp add: stutinv_def)

lemma stut_eq: "⟦STUTINV F;STUTINV G⟧ ⟹ STUTINV (F = G)"
  by (simp add: stutinv_def)

lemma stut_noteq: "⟦STUTINV F;STUTINV G⟧ ⟹ STUTINV (F ≠ G)"
  by (simp add: stutinv_def)

lemma stut_not: "STUTINV F ⟹ STUTINV (¬ F)"
  by (simp add: stutinv_def)

lemma stut_all: "(⋀x. STUTINV (F x)) ⟹ STUTINV (∀ x. F x)"
  by (simp add: stutinv_def)

lemma stut_ex: "(⋀x. STUTINV (F x)) ⟹ STUTINV (∃ x. F x)"
  by (simp add: stutinv_def)

lemma stut_const: "STUTINV #c"
  by (simp add: stutinv_def)

lemma stut_fun1: "STUTINV X ⟹ STUTINV (f <X>)"
  by (simp add: stutinv_def)

lemma stut_fun2: "⟦STUTINV X;STUTINV Y⟧ ⟹ STUTINV (f <X,Y>)"
  by (simp add: stutinv_def)

lemma stut_fun3: "⟦STUTINV X;STUTINV Y;STUTINV Z⟧ ⟹ STUTINV (f <X,Y,Z>)"
  by (simp add: stutinv_def)

lemma stut_fun4: "⟦STUTINV X;STUTINV Y;STUTINV Z; STUTINV W⟧ ⟹ STUTINV (f <X,Y,Z,W>)"
  by (simp add: stutinv_def)

lemma stut_plus: "⟦STUTINV x;STUTINV y⟧ ⟹ STUTINV (x+y)"
  by (simp add: stutinv_def)

subsubsection "Properties of @{term nstutinv}"

text ‹
  This subsection shows analogous properties about near stuttering
  invariance.

  If a formula @{term F} is stuttering invariant then ‹○F› is
  nearly stuttering invariant.
›

lemma nstut_nexts: assumes H: "STUTINV F" shows "NSTUTINV ○F"
using H by (simp add: stutinv_def nstutinv_def nexts_def)

text ‹
  The lemmas below shows that propositional and predicate operators 
  preserves near stuttering invariance.
›

lemma nstut_and: "⟦NSTUTINV F;NSTUTINV G⟧ ⟹ NSTUTINV (F ∧ G)"
  by (auto simp: nstutinv_def)

lemma nstut_or: "⟦NSTUTINV F;NSTUTINV G⟧ ⟹ NSTUTINV (F ∨ G)"
  by (auto simp: nstutinv_def)

lemma nstut_imp: "⟦NSTUTINV F;NSTUTINV G⟧ ⟹ NSTUTINV (F ⟶ G)"
  by (auto simp: nstutinv_def)

lemma nstut_eq: "⟦NSTUTINV F; NSTUTINV G⟧ ⟹ NSTUTINV (F = G)"
  by (force simp: nstutinv_def)

lemma nstut_not: "NSTUTINV F ⟹ NSTUTINV (¬ F)"
  by (auto simp: nstutinv_def)

lemma nstut_noteq: "⟦NSTUTINV F; NSTUTINV G⟧ ⟹ NSTUTINV (F ≠ G)"
  by (simp add: nstut_eq nstut_not)

lemma nstut_all: "(⋀x. NSTUTINV (F x)) ⟹ NSTUTINV (∀ x. F x)"
  by (auto simp: nstutinv_def)

lemma nstut_ex: "(⋀x. NSTUTINV (F x)) ⟹ NSTUTINV (∃ x. F x)"
  by (auto simp: nstutinv_def)

lemma nstut_const: "NSTUTINV #c"
  by (auto simp: nstutinv_def)

lemma nstut_fun1: "NSTUTINV X ⟹ NSTUTINV (f <X>)"
  by (force simp: nstutinv_def)

lemma nstut_fun2: "⟦NSTUTINV X; NSTUTINV Y⟧ ⟹ NSTUTINV (f <X,Y>)"
  by (force simp: nstutinv_def)

lemma nstut_fun3: "⟦NSTUTINV X; NSTUTINV Y; NSTUTINV Z⟧ ⟹ NSTUTINV (f <X,Y,Z>)"
  by (force simp: nstutinv_def)

lemma nstut_fun4: "⟦NSTUTINV X; NSTUTINV Y; NSTUTINV Z; NSTUTINV W⟧ ⟹ NSTUTINV (f <X,Y,Z,W>)"
  by (force simp: nstutinv_def)

lemma nstut_plus: "⟦NSTUTINV x;NSTUTINV y⟧ ⟹ NSTUTINV (x+y)"
  by (simp add: nstut_fun2)

subsubsection "Abbreviations"

text ‹
  We show the obvious fact that the same properties holds for abbreviated
  operators.
›

lemmas nstut_before = stut_before[THEN stutinv_strictly_stronger]

lemma nstut_unch: "NSTUTINV (Unchanged v)"
proof (unfold unch_def)
  have g1: "NSTUTINV v$" by (rule nstut_after)
  have "NSTUTINV $v" by (rule stut_before[THEN stutinv_strictly_stronger])
  with g1 show "NSTUTINV (v$ = $v)" by (rule nstut_eq)
qed

text‹
  Formulas ‹[P]_v› are not \tlastar{} formulas by themselves,
  but we need to reason about them when they appear wrapped
  inside ‹□[-]_v›. We only require that it preserves nearly
  stuttering invariance. Observe that ‹[P]_v› trivially holds for
  a stuttering step, so it cannot be stuttering invariant.
›

lemma nstut_actrans: "NSTUTINV P ⟹ NSTUTINV [P]_v"
  by (simp add: actrans_def nstut_unch nstut_or)

lemma stut_eventually: "STUTINV F ⟹ STUTINV ◇F"
  by (simp add: eventually_def stut_not stut_always)

lemma stut_leadsto: "⟦STUTINV F; STUTINV G⟧ ⟹ STUTINV (F ↝ G)"
  by (simp add: leadsto_def stut_always stut_eventually stut_imp)

lemma stut_angle_action: "NSTUTINV P ⟹ STUTINV ◇⟨P⟩_v"
  by (simp add: angle_action_def nstut_not stut_action stut_not)

lemma nstut_angle_acttrans: "NSTUTINV P ⟹ NSTUTINV ⟨P⟩_v"
  by (simp add: angle_actrans_def nstut_not nstut_actrans)

lemmas stutinvs = stut_before stut_always stut_action
  stut_and stut_or stut_imp stut_eq stut_noteq stut_not
  stut_all stut_ex stut_eventually stut_leadsto stut_angle_action stut_const 
  stut_fun1 stut_fun2 stut_fun3 stut_fun4

lemmas nstutinvs =  nstut_after nstut_nexts nstut_actrans
  nstut_unch nstut_and nstut_or nstut_imp nstut_eq nstut_noteq nstut_not
  nstut_all nstut_ex nstut_angle_acttrans stutinv_strictly_stronger 
  nstut_fun1 nstut_fun2 nstut_fun3 nstut_fun4 stutinvs[THEN stutinv_strictly_stronger]

lemmas bothstutinvs = stutinvs nstutinvs

end