Theory Inc

(*  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 ‹Lamport's Inc example›

theory Inc
imports State   
begin

text‹
  This example illustrates use of the embedding by mechanising
  the running example of Lamports original TLA paper \<^cite>‹"Lamport94"›.
›

datatype pcount = a | b | g

locale Firstprogram =
  fixes x :: "state ⇒ nat"
  and y :: "state ⇒ nat"
  and init :: "temporal"
  and m1  :: "temporal"
  and m2 :: "temporal"
  and phi :: "temporal"
  and Live :: "temporal"
  defines "init ≡ TEMP $x = # 0 ∧ $y = # 0"
  and "m1 ≡ TEMP x` = Suc<$x> ∧ y` = $y"
  and "m2 ≡ TEMP y` = Suc<$y> ∧ x` = $x"
  and "Live ≡ TEMP WF(m1)_(x,y) ∧ WF(m2)_(x,y)"
  and "phi ≡ TEMP (init ∧ □[m1 ∨ m2]_(x,y) ∧ Live)"
  assumes bvar: "basevars (x,y)"

lemma (in Firstprogram) "STUTINV phi"
  by (auto simp: phi_def init_def m1_def m2_def Live_def stutinvs nstutinvs livestutinv)

lemma (in Firstprogram) enabled_m1: "⊢ Enabled ⟨m1⟩_(x,y)"
proof (clarify)
  fix s
  show "s ⊨ Enabled ⟨m1⟩_(x,y)"
    by (rule base_enabled[OF bvar]) (auto simp: m1_def tla_defs)
qed

lemma (in Firstprogram) enabled_m2: "⊢ Enabled ⟨m2⟩_(x,y)"
proof (clarify)
  fix s
  show "s ⊨ Enabled ⟨m2⟩_(x,y)"
    by (rule base_enabled[OF bvar]) (auto simp: m2_def tla_defs)
qed

locale Secondprogram = Firstprogram +
  fixes sem :: "state ⇒ nat" 
  and pc1 :: "state ⇒ pcount"
  and pc2 :: "state ⇒ pcount"
  and vars
  and initPsi :: "temporal"
  and alpha1 :: "temporal"
  and alpha2 :: "temporal"
  and beta1 :: "temporal"
  and beta2 :: "temporal"
  and gamma1 :: "temporal"
  and gamma2 :: "temporal"
  and n1 :: "temporal"
  and n2 :: "temporal"
  and Live2 :: "temporal"
  and psi :: "temporal"
  and I :: "temporal"
  defines "vars ≡ LIFT (x,y,sem,pc1,pc2)" 
  and "initPsi ≡ TEMP $pc1 = # a ∧ $pc2 = # a ∧ $x = # 0 ∧ $y = # 0 ∧ $sem = # 1"
  and "alpha1 ≡ TEMP $pc1 =#a ∧ # 0 < $sem ∧ pc1$ = #b ∧ sem$ = $sem - # 1 ∧ Unchanged (x,y,pc2)" 
  and "alpha2 ≡ TEMP $pc2 =#a ∧ # 0 < $sem ∧ pc2` = #b ∧ sem$ = $sem - # 1 ∧ Unchanged (x,y,pc1)" 
  and "beta1 ≡ TEMP $pc1 =#b ∧ pc1` = #g ∧ x` = Suc<$x> ∧ Unchanged (y,sem,pc2)" 
  and "beta2 ≡ TEMP $pc2 =#b ∧ pc2` = #g ∧ y` = Suc<$y> ∧ Unchanged (x,sem,pc1)" 
  and "gamma1 ≡ TEMP $pc1 =#g ∧ pc1` = #a ∧ sem` = Suc<$sem> ∧ Unchanged (x,y,pc2)"
  and "gamma2 ≡ TEMP $pc2 =#g ∧ pc2` = #a ∧ sem` = Suc<$sem> ∧ Unchanged (x,y,pc1)"
  and "n1 ≡ TEMP (alpha1 ∨ beta1 ∨ gamma1)"
  and "n2 ≡ TEMP (alpha2 ∨ beta2 ∨ gamma2)"
  and "Live2 ≡ TEMP SF(n1)_vars ∧ SF(n2)_vars"
  and "psi ≡ TEMP (initPsi ∧ □[n1 ∨ n2]_vars ∧ Live2)"
  and "I ≡ TEMP ($sem = # 1 ∧ $pc1 = #a ∧ $pc2 = # a)
               ∨   ($sem = # 0 ∧ (($pc1 = #a ∧ $pc2 ∈ {#b , #g}) 
                                ∨ ($pc2 = #a ∧ $pc1 ∈ {#b , #g})))"
  assumes bvar2: "basevars vars"

lemmas  (in Secondprogram) Sact2_defs = n1_def n2_def alpha1_def beta1_def gamma1_def alpha2_def beta2_def gamma2_def

text ‹
  Proving invariants is the basis of every effort of system verification.
  We show that ‹I› is an inductive invariant of specification ‹psi›.
›
lemma (in Secondprogram) psiI: "⊢ psi ⟶ □I"
proof -
  have init: "⊢ initPsi ⟶ I" by (auto simp: initPsi_def I_def)
  have "|~ I ∧ Unchanged vars ⟶ ○I" by (auto simp: I_def vars_def tla_defs)
  moreover
  have "|~ I ∧ n1 ⟶ ○I" by (auto simp: I_def Sact2_defs tla_defs)
  moreover
  have "|~ I ∧ n2 ⟶ ○I" by (auto simp: I_def Sact2_defs tla_defs)
  ultimately have step: "|~ I ∧ [n1 ∨ n2]_vars ⟶ ○I" by (force simp: actrans_def)
  from init step have goal: "⊢ initPsi ∧ □[n1 ∨ n2]_vars ⟶ □I" by (rule invmono)
  have "⊢ initPsi ∧ □[n1 ∨ n2]_vars ∧ Live2 ==> ⊢ initPsi ∧ □[n1 ∨ n2]_vars"
   by auto
  with goal show ?thesis unfolding psi_def by auto
qed

text ‹
  Using this invariant we now prove step simulation, i.e. the safety part of
  the refinement proof.
›

theorem (in Secondprogram) step_simulation: "⊢ psi ⟶ init ∧ □[m1 ∨ m2]_(x,y)"
proof -
  have "⊢ initPsi ∧ □I ∧ □[n1 ∨ n2]_vars ⟶ init ∧ □[m1 ∨ m2]_(x,y)"
  proof (rule refinement1)
    show "⊢ initPsi ⟶ init" by (auto simp: initPsi_def init_def)
  next
    show "|~ I ∧ ○I ∧ [n1 ∨ n2]_vars ⟶ [m1 ∨ m2]_(x,y)"
      by (auto simp: I_def m1_def m2_def vars_def Sact2_defs tla_defs)
  qed
  with psiI show ?thesis unfolding psi_def by force
qed

text ‹
  Liveness proofs require computing the enabledness conditions of actions.
  The first lemma below shows that all steps are visible, i.e. they change
  at least one variable.
›
lemma  (in Secondprogram) n1_ch: "|~ ⟨n1⟩_vars = n1"
proof -
  have "|~ n1 ⟶ ⟨n1⟩_vars" by (auto simp: Sact2_defs tla_defs vars_def)
  thus ?thesis by (auto simp: angle_actrans_sem[int_rewrite])
qed

lemma (in Secondprogram) enab_alpha1: "⊢ $pc1 = #a ⟶ # 0 < $sem ⟶ Enabled alpha1"
proof (clarsimp simp: tla_defs)
  fix s :: "state seq"
  assume "pc1 (s 0) = a" and "0 < sem (s 0)"
  thus "s ⊨ Enabled alpha1"
    by (intro base_enabled[OF bvar2]) (auto simp: Sact2_defs tla_defs vars_def)
qed

lemma (in Secondprogram) enab_beta1: "⊢ $pc1 = #b ⟶ Enabled beta1"
proof (clarsimp simp: tla_defs)
  fix s :: "state seq"
  assume "pc1 (s 0) = b"
  thus "s ⊨ Enabled beta1"
    by (intro base_enabled[OF bvar2]) (auto simp: Sact2_defs tla_defs vars_def)
qed

lemma (in Secondprogram) enab_gamma1: "⊢ $pc1 = #g ⟶ Enabled gamma1"
proof (clarsimp simp: tla_defs)
  fix s :: "state seq"
  assume "pc1 (s 0) = g"
  thus "s ⊨ Enabled gamma1"
    by (intro base_enabled[OF bvar2]) (auto simp: Sact2_defs tla_defs vars_def)
qed

lemma (in Secondprogram) enab_n1:
  "⊢ Enabled ⟨n1⟩_vars = ($pc1 = #a ⟶ # 0 < $sem)"
unfolding n1_ch[int_rewrite] proof (rule int_iffI)
  show "⊢ Enabled n1 ⟶ $pc1 = #a ⟶ # 0 < $sem"
    by (auto elim!: enabledE simp: Sact2_defs tla_defs)
next
  show "⊢ ($pc1 = #a ⟶ # 0 < $sem) ⟶ Enabled n1"
  proof (clarsimp simp: tla_defs)
    fix s :: "state seq"
    assume "pc1 (s 0) = a ⟶ 0 < sem (s 0)"
    thus "s ⊨ Enabled n1"
      using enab_alpha1[unlift_rule]
            enab_beta1[unlift_rule]
            enab_gamma1[unlift_rule]
      by (cases "pc1 (s 0)") (force simp: n1_def Enabled_disj[int_rewrite] tla_defs)+
  qed
qed

text ‹
  The analogous properties for the second process are obtained by copy and paste.
›
lemma  (in Secondprogram) n2_ch: "|~ ⟨n2⟩_vars = n2"
proof -
  have "|~ n2 ⟶ ⟨n2⟩_vars" by (auto simp: Sact2_defs tla_defs vars_def)
  thus ?thesis by (auto simp: angle_actrans_sem[int_rewrite])
qed

lemma (in Secondprogram) enab_alpha2: "⊢ $pc2 = #a ⟶ # 0 < $sem ⟶ Enabled alpha2"
proof (clarsimp simp: tla_defs)
  fix s :: "state seq"
  assume "pc2 (s 0) = a" and "0 < sem (s 0)"
  thus "s ⊨ Enabled alpha2"
    by (intro base_enabled[OF bvar2]) (auto simp: Sact2_defs tla_defs vars_def)
qed

lemma (in Secondprogram) enab_beta2: "⊢ $pc2 = #b ⟶ Enabled beta2"
proof (clarsimp simp: tla_defs)
  fix s :: "state seq"
  assume "pc2 (s 0) = b"
  thus "s ⊨ Enabled beta2"
    by (intro base_enabled[OF bvar2]) (auto simp: Sact2_defs tla_defs vars_def)
qed

lemma (in Secondprogram) enab_gamma2: "⊢ $pc2 = #g ⟶ Enabled gamma2"
proof (clarsimp simp: tla_defs)
  fix s :: "state seq"
  assume "pc2 (s 0) = g"
  thus "s ⊨ Enabled gamma2"
    by (intro base_enabled[OF bvar2]) (auto simp: Sact2_defs tla_defs vars_def)
qed

lemma (in Secondprogram) enab_n2:
  "⊢ Enabled ⟨n2⟩_vars = ($pc2 = #a ⟶ # 0 < $sem)"
unfolding n2_ch[int_rewrite] proof (rule int_iffI)
  show "⊢ Enabled n2 ⟶ $pc2 = #a ⟶ # 0 < $sem"
    by (auto elim!: enabledE simp: Sact2_defs tla_defs)
next
  show "⊢ ($pc2 = #a ⟶ # 0 < $sem) ⟶ Enabled n2"
  proof (clarsimp simp: tla_defs)
    fix s :: "state seq"
    assume "pc2 (s 0) = a ⟶ 0 < sem (s 0)"
    thus "s ⊨ Enabled n2"
      using enab_alpha2[unlift_rule]
            enab_beta2[unlift_rule]
            enab_gamma2[unlift_rule]
      by (cases "pc2 (s 0)") (force simp: n2_def Enabled_disj[int_rewrite] tla_defs)+
  qed
qed

text ‹
  We use rule ‹SF2› to prove that ‹psi› implements strong fairness
  for the abstract action ‹m1›. Since strong fairness implies weak fairness,
  it follows that ‹psi› refines the liveness condition of ‹phi›.
›

lemma (in Secondprogram) psi_fair_m1: "⊢ psi ⟶ SF(m1)_(x,y)"
proof -
  have "⊢ □[n1 ∨ n2]_vars ∧ SF(n1)_vars ∧ □(I ∧ SF(n2)_vars) ⟶ SF(m1)_(x,y)"
  proof (rule SF2)
    txt ‹
      Rule ‹SF2› requires us to choose a helpful action (whose effect implies
      ‹⟨m1⟩_(x,y)›) and a persistent condition, which will eventually remain
      true if the helpful action is never executed. In our case, the helpful action
      is ‹beta1› and the persistent condition is ‹pc1 = b›.
›
    show "|~ ⟨(n1 ∨ n2) ∧ beta1⟩_vars ⟶ ⟨m1⟩_(x,y)"
      by (auto simp: beta1_def m1_def vars_def tla_defs)
  next
    show "|~ $pc1 = #b ∧ ○($pc1 = #b) ∧ ⟨(n1 ∨ n2) ∧ n1⟩_vars ⟶ beta1"
      by (auto simp: n1_def alpha1_def beta1_def gamma1_def tla_defs)
  next
    show "⊢ $pc1 = #b ∧ Enabled ⟨m1⟩_(x, y) ⟶ Enabled ⟨n1⟩_vars"
      unfolding enab_n1[int_rewrite] by auto
  next
    txt ‹
      The difficult part of the proof is showing that the persistent condition
      will eventually always be true if the helpful action is never executed.
      We show that (1) whenever the condition becomes true it remains so and
      (2) eventually the condition must be true.
›
    show "⊢ □[(n1 ∨ n2) ∧ ¬ beta1]_vars
            ∧ SF(n1)_vars ∧ □(I ∧ SF(n2)_vars) ∧ □◇Enabled ⟨m1⟩_(x, y)
            ⟶ ◇□($pc1 = #b)"
    proof -
      have "⊢ □□[(n1 ∨ n2) ∧ ¬ beta1]_vars ⟶ □($pc1 = #b ⟶ □($pc1 = #b))"
      proof (rule STL4)
        have "|~ $pc1 = #b ∧ [(n1 ∨ n2) ∧ ¬ beta1]_vars ⟶ ○($pc1 = #b)"
          by (auto simp: Sact2_defs vars_def tla_defs)
        from this[THEN INV1]
        show "⊢ □[(n1 ∨ n2) ∧ ¬ beta1]_vars ⟶ $pc1 = #b ⟶ □($pc1 = #b)" by auto
      qed
      hence 1: "⊢ □[(n1 ∨ n2) ∧ ¬ beta1]_vars ⟶ ◇($pc1 = #b) ⟶ ◇□($pc1 = #b)"
        by (force intro: E31[unlift_rule])
      have "⊢ □[(n1 ∨ n2) ∧ ¬ beta1]_vars ∧ SF(n1)_vars ∧ □(I ∧ SF(n2)_vars)
              ⟶ ◇($pc1 = #b)"
      proof -
        txt ‹
          The plan of the proof is to show that from any state where ‹pc1 = g›
          one eventually reaches ‹pc1 = a›, from where one eventually reaches
          ‹pc1 = b›. The result follows by combining leadsto properties.
›
        let ?F = "LIFT (□[(n1 ∨ n2) ∧ ¬ beta1]_vars ∧ SF(n1)_vars ∧ □(I ∧ SF(n2)_vars))"
        txt ‹
          Showing that ‹pc1 = g› leads to ‹pc1 = a› is a simple
          application of rule ‹SF1› because the first process completely
          controls this transition.
›
        have ga: "⊢ ?F ⟶ ($pc1 = #g ↝ $pc1 = #a)"
        proof (rule SF1)
          show "|~ $pc1 = #g ∧ [(n1 ∨ n2) ∧ ¬ beta1]_vars ⟶ ○($pc1 = #g) ∨ ○($pc1 = #a)"
            by (auto simp: Sact2_defs vars_def tla_defs)
        next
          show "|~ $pc1 = #g ∧ ⟨((n1 ∨ n2) ∧ ¬ beta1) ∧ n1⟩_vars ⟶ ○($pc1 = #a)"
            by (auto simp: Sact2_defs vars_def tla_defs)
        next
          show "|~ $pc1 = #g ∧ Unchanged vars ⟶ ○($pc1 = #g)"
            by (auto simp: vars_def tla_defs)
        next
          have "⊢ $pc1 = #g ⟶ Enabled ⟨n1⟩_vars"
            unfolding enab_n1[int_rewrite] by (auto simp: tla_defs)
          hence "⊢ □($pc1 = #g) ⟶ Enabled ⟨n1⟩_vars"
            by (rule lift_imp_trans[OF ax1])
          hence "⊢ □($pc1 = #g) ⟶ ◇Enabled ⟨n1⟩_vars"
            by (rule lift_imp_trans[OF _ E3])
          thus "⊢ □($pc1 = #g) ∧ □[(n1 ∨ n2) ∧ ¬ beta1]_vars ∧ □(I ∧ SF(n2)_vars)
                  ⟶ ◇Enabled ⟨n1⟩_vars"
            by auto
        qed
        txt ‹
          The proof that ‹pc1 = a› leads to ‹pc1 = b› follows
          the same basic schema. However, showing that ‹n1› is eventually
          enabled requires reasoning about the second process, which must liberate
          the critical section.
›
        have ab: "⊢ ?F ⟶ ($pc1 = #a ↝ $pc1 = #b)"
        proof (rule SF1)
          show "|~ $pc1 = #a ∧ [(n1 ∨ n2) ∧ ¬ beta1]_vars ⟶ ○($pc1 = #a) ∨ ○($pc1 = #b)"
            by (auto simp: Sact2_defs vars_def tla_defs)
        next
          show "|~ $pc1 = #a ∧ ⟨((n1 ∨ n2) ∧ ¬ beta1) ∧ n1⟩_vars ⟶ ○($pc1 = #b)"
            by (auto simp: Sact2_defs vars_def tla_defs)
        next
          show "|~ $pc1 = #a ∧ Unchanged vars ⟶ ○($pc1 = #a)"
            by (auto simp: vars_def tla_defs)
        next
          txt ‹We establish a suitable leadsto-chain.›
          let ?G = "LIFT □[(n1 ∨ n2) ∧ ¬ beta1]_vars ∧ SF(n2)_vars ∧ □($pc1 = #a ∧ I)"
          have "⊢ ?G ⟶ ◇($pc2 = #a ∧ $pc1 = #a ∧ I)"
          proof -
            txt ‹Rule ‹SF1› takes us from ‹pc2 = b› to ‹pc2 = g›.›
            have bg2: "⊢ ?G ⟶ ($pc2 = #b ↝ $pc2 = #g)"
            proof (rule SF1)
              show "|~ $pc2 = #b ∧ [(n1 ∨ n2) ∧ ¬beta1]_vars ⟶ ○($pc2 = #b) ∨ ○($pc2 = #g)"
                by (auto simp: Sact2_defs vars_def tla_defs)
            next
              show "|~ $pc2 = #b ∧ ⟨((n1 ∨ n2) ∧ ¬beta1) ∧ n2⟩_vars ⟶ ○($pc2 = #g)"
                by (auto simp: Sact2_defs vars_def tla_defs)
            next
              show "|~ $pc2 = #b ∧ Unchanged vars ⟶ ○($pc2 = #b)"
                by (auto simp: vars_def tla_defs)
            next
              have "⊢ $pc2 = #b ⟶ Enabled ⟨n2⟩_vars"
                unfolding enab_n2[int_rewrite] by (auto simp: tla_defs)
              hence "⊢ □($pc2 = #b) ⟶ Enabled ⟨n2⟩_vars"
                by (rule lift_imp_trans[OF ax1])
              hence "⊢ □($pc2 = #b) ⟶ ◇Enabled ⟨n2⟩_vars"
                by (rule lift_imp_trans[OF _ E3])
              thus "⊢ □($pc2 = #b) ∧ □[(n1 ∨ n2) ∧ ¬beta1]_vars ∧ □($pc1 = #a ∧ I)
                      ⟶ ◇Enabled ⟨n2⟩_vars"
                by auto
            qed
            txt ‹Similarly, ‹pc2 = b› leads to ‹pc2 = g›.›
            have ga2: "⊢ ?G ⟶ ($pc2 = #g ↝ $pc2 = #a)"
            proof (rule SF1)
              show "|~ $pc2 = #g ∧ [(n1 ∨ n2) ∧ ¬beta1]_vars ⟶ ○($pc2 = #g) ∨ ○($pc2 = #a)"
                by (auto simp: Sact2_defs vars_def tla_defs)
            next
              show "|~ $pc2 = #g ∧ ⟨((n1 ∨ n2) ∧ ¬beta1) ∧ n2⟩_vars ⟶ ○($pc2 = #a)"
                by (auto simp: n2_def alpha2_def beta2_def gamma2_def vars_def tla_defs)
            next
              show "|~ $pc2 = #g ∧ Unchanged vars ⟶ ○($pc2 = #g)"
                by (auto simp: vars_def tla_defs)
            next
              have "⊢ $pc2 = #g ⟶ Enabled ⟨n2⟩_vars"
                unfolding enab_n2[int_rewrite] by (auto simp: tla_defs)
              hence "⊢ □($pc2 = #g) ⟶ Enabled ⟨n2⟩_vars"
                by (rule lift_imp_trans[OF ax1])
              hence "⊢ □($pc2 = #g) ⟶ ◇Enabled ⟨n2⟩_vars"
                by (rule lift_imp_trans[OF _ E3])
              thus "⊢ □($pc2 = #g) ∧ □[(n1 ∨ n2) ∧ ¬beta1]_vars ∧ □($pc1 = #a ∧ I)
                      ⟶ ◇Enabled ⟨n2⟩_vars"
                by auto
            qed
            with bg2 have "⊢ ?G ⟶ ($pc2 = #b ↝ $pc2 = #a)"
              by (force elim: LT13[unlift_rule])
            with ga2 have "⊢ ?G ⟶ ($pc2 = #a ∨ $pc2 = #b ∨ $pc2 = #g) ↝ ($pc2 = #a)"
              unfolding LT17[int_rewrite] LT1[int_rewrite] by force
            moreover
            have "⊢ $pc2 = #a ∨ $pc2 = #b ∨ $pc2 = #g"
            proof (clarsimp simp: tla_defs)
              fix s :: "state seq"
              assume "pc2 (s 0) ≠ a" and "pc2 (s 0) ≠ g"
              thus "pc2 (s 0) = b" by (cases "pc2 (s 0)") auto
            qed
            hence "⊢ (($pc2 = #a ∨ $pc2 = #b ∨ $pc2 = #g) ↝ $pc2 = #a) ⟶ ◇($pc2 = #a)"
              by (rule fmp[OF _ LT4])
            ultimately
            have "⊢ ?G ⟶ ◇($pc2 = #a)" by force
            thus ?thesis by (auto intro!: SE3[unlift_rule])
          qed
          moreover
          have "⊢ ◇($pc2 = #a ∧ $pc1 = #a ∧ I) ⟶ ◇Enabled ⟨n1⟩_vars"
            unfolding enab_n1[int_rewrite] by (rule STL4_eve) (auto simp: I_def tla_defs)
          ultimately
          show "⊢ □($pc1 = #a) ∧ □[(n1 ∨ n2) ∧ ¬ beta1]_vars ∧ □(I ∧ SF(n2)_vars)
                  ⟶ ◇Enabled ⟨n1⟩_vars"
            by (force simp: STL5[int_rewrite])
        qed
        from ga ab have "⊢ ?F ⟶ ($pc1 = #g ↝ $pc1 = #b)"
          by (force elim: LT13[unlift_rule])
        with ab have "⊢ ?F ⟶ (($pc1 = #a ∨ $pc1 = #b ∨ $pc1 = #g) ↝ $pc1 = #b)"
          unfolding LT17[int_rewrite] LT1[int_rewrite] by force
        moreover
        have "⊢ $pc1 = #a ∨ $pc1 = #b ∨ $pc1 = #g"
        proof (clarsimp simp: tla_defs)
          fix s :: "state seq"
          assume "pc1 (s 0) ≠ a" and "pc1 (s 0) ≠ g"
          thus "pc1 (s 0) = b" by (cases "pc1 (s 0)", auto)
        qed
        hence "⊢ (($pc1 = #a ∨ $pc1 = #b ∨ $pc1 = #g) ↝ $pc1 = #b) ⟶ ◇($pc1 = #b)"
          by (rule fmp[OF _ LT4])
        ultimately show ?thesis by (rule lift_imp_trans)
      qed
      with 1 show ?thesis by force
    qed
  qed
  with psiI show ?thesis unfolding psi_def Live2_def STL5[int_rewrite] by force
qed

text ‹
  In the same way we prove that ‹psi› implements strong fairness
  for the abstract action ‹m1›. The proof is obtained by copy and paste
  from the previous one.
›

lemma (in Secondprogram) psi_fair_m2: "⊢ psi ⟶ SF(m2)_(x,y)"
proof -
  have "⊢ □[n1 ∨ n2]_vars ∧ SF(n2)_vars ∧ □(I ∧ SF(n1)_vars) ⟶ SF(m2)_(x,y)"
  proof (rule SF2)
    txt ‹
      Rule ‹SF2› requires us to choose a helpful action (whose effect implies
      ‹⟨m2⟩_(x,y)›) and a persistent condition, which will eventually remain
      true if the helpful action is never executed. In our case, the helpful action
      is ‹beta2› and the persistent condition is ‹pc2 = b›.
›
    show "|~ ⟨(n1 ∨ n2) ∧ beta2⟩_vars ⟶ ⟨m2⟩_(x,y)"
      by (auto simp: beta2_def m2_def vars_def tla_defs)
  next
    show "|~ $pc2 = #b ∧ ○($pc2 = #b) ∧ ⟨(n1 ∨ n2) ∧ n2⟩_vars ⟶ beta2"
      by (auto simp: n2_def alpha2_def beta2_def gamma2_def tla_defs)
  next
    show "⊢ $pc2 = #b ∧ Enabled ⟨m2⟩_(x, y) ⟶ Enabled ⟨n2⟩_vars"
      unfolding enab_n2[int_rewrite] by auto
  next
    txt ‹
      The difficult part of the proof is showing that the persistent condition
      will eventually always be true if the helpful action is never executed.
      We show that (1) whenever the condition becomes true it remains so and
      (2) eventually the condition must be true.
›
    show "⊢ □[(n1 ∨ n2) ∧ ¬ beta2]_vars
            ∧ SF(n2)_vars ∧ □(I ∧ SF(n1)_vars) ∧ □◇Enabled ⟨m2⟩_(x, y)
            ⟶ ◇□($pc2 = #b)"
    proof -
      have "⊢ □□[(n1 ∨ n2) ∧ ¬ beta2]_vars ⟶ □($pc2 = #b ⟶ □($pc2 = #b))"
      proof (rule STL4)
        have "|~ $pc2 = #b ∧ [(n1 ∨ n2) ∧ ¬ beta2]_vars ⟶ ○($pc2 = #b)"
          by (auto simp: Sact2_defs vars_def tla_defs)
        from this[THEN INV1]
        show "⊢ □[(n1 ∨ n2) ∧ ¬ beta2]_vars ⟶ $pc2 = #b ⟶ □($pc2 = #b)" by auto
      qed
      hence 1: "⊢ □[(n1 ∨ n2) ∧ ¬ beta2]_vars ⟶ ◇($pc2 = #b) ⟶ ◇□($pc2 = #b)"
        by (force intro: E31[unlift_rule])
      have "⊢ □[(n1 ∨ n2) ∧ ¬ beta2]_vars ∧ SF(n2)_vars ∧ □(I ∧ SF(n1)_vars)
              ⟶ ◇($pc2 = #b)"
      proof -
        txt ‹
          The plan of the proof is to show that from any state where ‹pc2 = g›
          one eventually reaches ‹pc2 = a›, from where one eventually reaches
          ‹pc2 = b›. The result follows by combining leadsto properties.
›
        let ?F = "LIFT (□[(n1 ∨ n2) ∧ ¬ beta2]_vars ∧ SF(n2)_vars ∧ □(I ∧ SF(n1)_vars))"
        txt ‹
          Showing that ‹pc2 = g› leads to ‹pc2 = a› is a simple
          application of rule ‹SF1› because the second process completely
          controls this transition.
›
        have ga: "⊢ ?F ⟶ ($pc2 = #g ↝ $pc2 = #a)"
        proof (rule SF1)
          show "|~ $pc2 = #g ∧ [(n1 ∨ n2) ∧ ¬ beta2]_vars ⟶ ○($pc2 = #g) ∨ ○($pc2 = #a)"
            by (auto simp: Sact2_defs vars_def tla_defs)
        next
          show "|~ $pc2 = #g ∧ ⟨((n1 ∨ n2) ∧ ¬ beta2) ∧ n2⟩_vars ⟶ ○($pc2 = #a)"
            by (auto simp: n2_def alpha2_def beta2_def gamma2_def vars_def tla_defs)
        next
          show "|~ $pc2 = #g ∧ Unchanged vars ⟶ ○($pc2 = #g)"
            by (auto simp: vars_def tla_defs)
        next
          have "⊢ $pc2 = #g ⟶ Enabled ⟨n2⟩_vars"
            unfolding enab_n2[int_rewrite] by (auto simp: tla_defs)
          hence "⊢ □($pc2 = #g) ⟶ Enabled ⟨n2⟩_vars"
            by (rule lift_imp_trans[OF ax1])
          hence "⊢ □($pc2 = #g) ⟶ ◇Enabled ⟨n2⟩_vars"
            by (rule lift_imp_trans[OF _ E3])
          thus "⊢ □($pc2 = #g) ∧ □[(n1 ∨ n2) ∧ ¬ beta2]_vars ∧ □(I ∧ SF(n1)_vars)
                  ⟶ ◇Enabled ⟨n2⟩_vars"
            by auto
        qed
        txt ‹
          The proof that ‹pc2 = a› leads to ‹pc2 = b› follows
          the same basic schema. However, showing that ‹n2› is eventually
          enabled requires reasoning about the second process, which must liberate
          the critical section.
›
        have ab: "⊢ ?F ⟶ ($pc2 = #a ↝ $pc2 = #b)"
        proof (rule SF1)
          show "|~ $pc2 = #a ∧ [(n1 ∨ n2) ∧ ¬ beta2]_vars ⟶ ○($pc2 = #a) ∨ ○($pc2 = #b)"
            by (auto simp: Sact2_defs vars_def tla_defs)
        next
          show "|~ $pc2 = #a ∧ ⟨((n1 ∨ n2) ∧ ¬ beta2) ∧ n2⟩_vars ⟶ ○($pc2 = #b)"
            by (auto simp: n2_def alpha2_def beta2_def gamma2_def vars_def tla_defs)
        next
          show "|~ $pc2 = #a ∧ Unchanged vars ⟶ ○($pc2 = #a)"
            by (auto simp: vars_def tla_defs)
        next
          txt ‹We establish a suitable leadsto-chain.›
          let ?G = "LIFT □[(n1 ∨ n2) ∧ ¬ beta2]_vars ∧ SF(n1)_vars ∧ □($pc2 = #a ∧ I)"
          have "⊢ ?G ⟶ ◇($pc1 = #a ∧ $pc2 = #a ∧ I)"
          proof -
            txt ‹Rule ‹SF1› takes us from ‹pc1 = b› to ‹pc1 = g›.›
            have bg1: "⊢ ?G ⟶ ($pc1 = #b ↝ $pc1 = #g)"
            proof (rule SF1)
              show "|~ $pc1 = #b ∧ [(n1 ∨ n2) ∧ ¬beta2]_vars ⟶ ○($pc1 = #b) ∨ ○($pc1 = #g)"
                by (auto simp: Sact2_defs vars_def tla_defs)
            next
              show "|~ $pc1 = #b ∧ ⟨((n1 ∨ n2) ∧ ¬beta2) ∧ n1⟩_vars ⟶ ○($pc1 = #g)"
                by (auto simp: n1_def alpha1_def beta1_def gamma1_def vars_def tla_defs)
            next
              show "|~ $pc1 = #b ∧ Unchanged vars ⟶ ○($pc1 = #b)"
                by (auto simp: vars_def tla_defs)
            next
              have "⊢ $pc1 = #b ⟶ Enabled ⟨n1⟩_vars"
                unfolding enab_n1[int_rewrite] by (auto simp: tla_defs)
              hence "⊢ □($pc1 = #b) ⟶ Enabled ⟨n1⟩_vars"
                by (rule lift_imp_trans[OF ax1])
              hence "⊢ □($pc1 = #b) ⟶ ◇Enabled ⟨n1⟩_vars"
                by (rule lift_imp_trans[OF _ E3])
              thus "⊢ □($pc1 = #b) ∧ □[(n1 ∨ n2) ∧ ¬beta2]_vars ∧ □($pc2 = #a ∧ I)
                      ⟶ ◇Enabled ⟨n1⟩_vars"
                by auto
            qed
            txt ‹Similarly, ‹pc1 = b› leads to ‹pc1 = g›.›
            have ga1: "⊢ ?G ⟶ ($pc1 = #g ↝ $pc1 = #a)"
            proof (rule SF1)
              show "|~ $pc1 = #g ∧ [(n1 ∨ n2) ∧ ¬beta2]_vars ⟶ ○($pc1 = #g) ∨ ○($pc1 = #a)"
                by (auto simp: Sact2_defs vars_def tla_defs)
            next
              show "|~ $pc1 = #g ∧ ⟨((n1 ∨ n2) ∧ ¬beta2) ∧ n1⟩_vars ⟶ ○($pc1 = #a)"
                by (auto simp: n1_def alpha1_def beta1_def gamma1_def vars_def tla_defs)
            next
              show "|~ $pc1 = #g ∧ Unchanged vars ⟶ ○($pc1 = #g)"
                by (auto simp: vars_def tla_defs)
            next
              have "⊢ $pc1 = #g ⟶ Enabled ⟨n1⟩_vars"
                unfolding enab_n1[int_rewrite] by (auto simp: tla_defs)
              hence "⊢ □($pc1 = #g) ⟶ Enabled ⟨n1⟩_vars"
                by (rule lift_imp_trans[OF ax1])
              hence "⊢ □($pc1 = #g) ⟶ ◇Enabled ⟨n1⟩_vars"
                by (rule lift_imp_trans[OF _ E3])
              thus "⊢ □($pc1 = #g) ∧ □[(n1 ∨ n2) ∧ ¬beta2]_vars ∧ □($pc2 = #a ∧ I)
                      ⟶ ◇Enabled ⟨n1⟩_vars"
                by auto
            qed
            with bg1 have "⊢ ?G ⟶ ($pc1 = #b ↝ $pc1 = #a)"
              by (force elim: LT13[unlift_rule])
            with ga1 have "⊢ ?G ⟶ ($pc1 = #a ∨ $pc1 = #b ∨ $pc1 = #g) ↝ ($pc1 = #a)"
              unfolding LT17[int_rewrite] LT1[int_rewrite] by force
            moreover
            have "⊢ $pc1 = #a ∨ $pc1 = #b ∨ $pc1 = #g"
            proof (clarsimp simp: tla_defs)
              fix s :: "state seq"
              assume "pc1 (s 0) ≠ a" and "pc1 (s 0) ≠ g"
              thus "pc1 (s 0) = b" by (cases "pc1 (s 0)") auto
            qed
            hence "⊢ (($pc1 = #a ∨ $pc1 = #b ∨ $pc1 = #g) ↝ $pc1 = #a) ⟶ ◇($pc1 = #a)"
              by (rule fmp[OF _ LT4])
            ultimately
            have "⊢ ?G ⟶ ◇($pc1 = #a)" by force
            thus ?thesis by (auto intro!: SE3[unlift_rule])
          qed
          moreover
          have "⊢ ◇($pc1 = #a ∧ $pc2 = #a ∧ I) ⟶ ◇Enabled ⟨n2⟩_vars"
            unfolding enab_n2[int_rewrite] by (rule STL4_eve) (auto simp: I_def tla_defs)
          ultimately
          show "⊢ □($pc2 = #a) ∧ □[(n1 ∨ n2) ∧ ¬ beta2]_vars ∧ □(I ∧ SF(n1)_vars)
                  ⟶ ◇Enabled ⟨n2⟩_vars"
            by (force simp: STL5[int_rewrite])
        qed
        from ga ab have "⊢ ?F ⟶ ($pc2 = #g ↝ $pc2 = #b)"
          by (force elim: LT13[unlift_rule])
        with ab have "⊢ ?F ⟶ (($pc2 = #a ∨ $pc2 = #b ∨ $pc2 = #g) ↝ $pc2 = #b)"
          unfolding LT17[int_rewrite] LT1[int_rewrite] by force
        moreover
        have "⊢ $pc2 = #a ∨ $pc2 = #b ∨ $pc2 = #g"
        proof (clarsimp simp: tla_defs)
          fix s :: "state seq"
          assume "pc2 (s 0) ≠ a" and "pc2 (s 0) ≠ g"
          thus "pc2 (s 0) = b" by (cases "pc2 (s 0)") auto
        qed
        hence "⊢ (($pc2 = #a ∨ $pc2 = #b ∨ $pc2 = #g) ↝ $pc2 = #b) ⟶ ◇($pc2 = #b)"
          by (rule fmp[OF _ LT4])
        ultimately show ?thesis by (rule lift_imp_trans)
      qed
      with 1 show ?thesis by force
    qed
  qed
  with psiI show ?thesis unfolding psi_def Live2_def STL5[int_rewrite] by force
qed

text ‹
  We can now prove the main theorem, which states that ‹psi›
  implements ‹phi›.
›

theorem (in Secondprogram) impl: "⊢ psi ⟶ phi"
  unfolding phi_def Live_def
  by (auto dest: step_simulation[unlift_rule]
                 lift_imp_trans[OF psi_fair_m1 SF_imp_WF, unlift_rule]
                 lift_imp_trans[OF psi_fair_m2 SF_imp_WF, unlift_rule])

end