Quelle  Liveness.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 "Liveness"

theory Liveness
imports Rules
begin

text‹This theory derives proof rules for liveness properties.›

definition enabled :: "'a formula ==> 'a formula"
where "enabled F ≡ λ s. ∃ t. ((first s) ## t) ⊨ F"

syntax "_Enabled" :: "lift ==> lift" (‹(Enabled _)› [90] 90)

translations "_Enabled" ⇌ "CONST enabled"

definition WeakF :: "('a::world) formula ==> ('a,'b) stfun ==> 'a formula"
where "WeakF F v ≡ TEMP ♢◻Enabled ⟨F⟩_v ⟶ ◻♢⟨F⟩_v"

definition StrongF :: "('a::world) formula ==> ('a,'b) stfun ==> 'a formula"
where "StrongF F v ≡ TEMP ◻♢Enabled ⟨F⟩_v ⟶ ◻♢⟨F⟩_v"

text‹
 Lamport's TLA defines the above notions for actions.
 In \tlastar{}, (pre-)formulas generalise TLA's actions and the above
 definition is the natural generalisation of enabledness to pre-formulas.
 In particular, we have chosen to define ‹enabled› such that it
 yields itself a temporal formula, although its value really just depends
 on the first state of the sequence it is evaluated over.
 Then, the definitions of weak and strong fairness are exactly as in TLA.
 ›

syntax
 "_WF" :: "[lift,lift] ==> lift" (‹(WF'(_')'_(_))›  [20,1000] 90)
 "_SF" :: "[lift,lift] ==> lift" (‹(SF'(_')'_(_))›  [20,1000] 90)
 "_WFsp" :: "[lift,lift] ==> lift" (‹(WF '(_')'_(_))›  [20,1000] 90)
 "_SFsp" :: "[lift,lift] ==> lift" (‹(SF '(_')'_(_))›  [20,1000] 90)

translations
 "_WF" ⇌ "CONST WeakF"
 "_SF" ⇌ "CONST StrongF"
 "_WFsp" ⇀ "CONST WeakF"
 "_SFsp" ⇀ "CONST StrongF"


subsection "Properties of @{term enabled}"

theorem enabledI: "⊨ F ⟶ Enabled F"
proof (clarsimp)
  fix w
  assume "w ⊨ F"
  with seq_app_first_tail[of w] have "((first w) ## tail w) ⊨ F" by simp
  thus "w ⊨ Enabled F" by (auto simp: enabled_def)
qed

theorem enabledE:
  assumes "s ⊨ Enabled F" and "∧u. (first s ## u) ⊨ F ==> Q"
  shows "Q"
  using assms unfolding enabled_def by blast

lemma enabled_mono: 
  assumes "w ⊨ Enabled F" and "⊨ F ⟶ G" 
  shows "w ⊨ Enabled G"
  using assms[unlifted] unfolding enabled_def by blast

lemma Enabled_disj1: "⊨ Enabled F ⟶ Enabled (F ∨ G)"
  by (auto simp: enabled_def)

lemma  Enabled_disj2: "⊨ Enabled F ⟶ Enabled (G ∨ F)"
  by (auto simp: enabled_def)

lemma  Enabled_conj1: "⊨ Enabled (F ∧ G) ⟶ Enabled F"
  by (auto simp: enabled_def)

lemma  Enabled_conj2: "⊨ Enabled (G ∧ F) ⟶ Enabled F"
  by (auto simp: enabled_def)

lemma Enabled_disjD: "⊨ Enabled (F ∨ G) ⟶ Enabled F ∨ Enabled G"
  by (auto simp: enabled_def)

lemma Enabled_disj: "⊨ Enabled (F ∨ G) = (Enabled F ∨ Enabled G)"
  by (auto simp: enabled_def)

lemmas enabled_disj_rew = Enabled_disj[int_rewrite]

lemma Enabled_ex: "⊨ Enabled (∃ x. F x) = (∃ x. Enabled (F x))"
  by (force simp: enabled_def)

subsection "Fairness Properties" 

lemma WF_alt: "⊨ WF(A)_v = (◻♢¬Enabled ⟨A⟩_v ∨ ◻♢⟨A⟩_v)"
proof -
  have "⊨ WF(A)_v = (¬♢◻ Enabled ⟨A⟩_v ∨ ◻♢⟨A⟩_v)" by (auto simp: WeakF_def)
  thus ?thesis by (simp add: dualization_rew)
qed

lemma SF_alt: "⊨ SF(A)_v = (♢◻¬Enabled ⟨A⟩_v ∨ ◻♢⟨A⟩_v)"
proof -
  have "⊨ SF(A)_v = (¬◻♢ Enabled ⟨A⟩_v ∨ ◻♢⟨A⟩_v)" by (auto simp: StrongF_def)
  thus ?thesis by (simp add: dualization_rew)
qed

lemma alwaysWFI: "⊨ WF(A)_v ⟶ ◻WF(A)_v"
  unfolding WF_alt[int_rewrite] by (rule MM6)

theorem WF_always[simp_unl]: "⊨ ◻WF(A)_v = WF(A)_v"
  by (rule int_iffI[OF ax1 alwaysWFI])

theorem WF_eventually[simp_unl]: "⊨ ♢WF(A)_v = WF(A)_v"
proof -
  have 1: "⊨ ¬WF(A)_v = (♢◻Enabled ⟨A⟩_v ∧ ¬ ◻♢⟨A⟩_v)"
    by (auto simp: WeakF_def)
  have "⊨ ◻¬WF(A)_v = ¬WF(A)_v"
    by (simp add: 1[int_rewrite] STL5[int_rewrite] dualization_rew)
  thus ?thesis
    by (auto simp: eventually_def)
qed

lemma alwaysSFI: "⊨ SF(A)_v ⟶ ◻SF(A)_v"
proof -
  have "⊨ ◻♢◻¬Enabled ⟨A⟩_v ∨ ◻♢⟨A⟩_v ⟶ ◻(◻♢◻¬Enabled ⟨A⟩_v ∨ ◻♢⟨A⟩_v)"
    by (rule MM6)
  thus ?thesis unfolding SF_alt[int_rewrite] by simp
qed

theorem SF_always[simp_unl]: "⊨ ◻SF(A)_v = SF(A)_v"
  by (rule int_iffI[OF ax1 alwaysSFI])

theorem SF_eventually[simp_unl]: "⊨ ♢SF(A)_v = SF(A)_v"
proof -
  have 1: "⊨ ¬SF(A)_v = (◻♢Enabled ⟨A⟩_v ∧ ¬ ◻♢⟨A⟩_v)"
    by (auto simp: StrongF_def)
  have "⊨ ◻¬SF(A)_v = ¬SF(A)_v"
    by (simp add: 1[int_rewrite] STL5[int_rewrite] dualization_rew)
  thus ?thesis
    by (auto simp: eventually_def)
qed

theorem SF_imp_WF: "⊨ SF (A)_v ⟶ WF (A)_v"
  unfolding WeakF_def StrongF_def by (auto dest: E20[unlift_rule])

lemma enabled_WFSF: "⊨ ◻Enabled ⟨F⟩_v ⟶ (WF(F)_v = SF(F)_v)"
proof -
  have "⊨ ◻Enabled ⟨F⟩_v ⟶ ♢◻Enabled ⟨F⟩_v" by (rule E3)
  hence "⊨ ◻Enabled ⟨F⟩_v ⟶ WF(F)_v ⟶ SF(F)_v" by (auto simp: WeakF_def StrongF_def)
  moreover
  have "⊨ ◻Enabled ⟨F⟩_v ⟶ ◻♢Enabled ⟨F⟩_v" by (rule STL4[OF E3])
  hence "⊨ ◻Enabled ⟨F⟩_v ⟶ SF(F)_v ⟶ WF(F)_v" by (auto simp: WeakF_def StrongF_def)
  ultimately show ?thesis by force
qed

theorem WF1_general:
  assumes h1: "|~ P ∧ N ⟶ ◯P ∨ ◯Q"
      and h2: "|~ P ∧ N ∧ ⟨A⟩_v ⟶ ◯Q"
      and h3: "⊨ P ∧ N ⟶ Enabled ⟨A⟩_v"
      and h4: "|~ P ∧ Unchanged w ⟶ ◯P"
  shows "⊨ ◻N ∧ WF(A)_v ⟶ (P ↝ Q)"
proof -
  have "⊨ ◻(◻N ∧ WF(A)_v) ⟶ ◻(◻P ⟶ ♢⟨A⟩_v)"
  proof (rule STL4)
    have "⊨ ◻(P ∧ N) ⟶ ♢◻Enabled ⟨A⟩_v" by (rule lift_imp_trans[OF h3[THEN STL4] E3])
    hence "⊨ ◻P ∧ ◻N ∧ WF(A)_v ⟶ ◻♢⟨A⟩_v" by (auto simp: WeakF_def STL5[int_rewrite])
    with ax1[of "TEMP ♢⟨A⟩_v"] show "⊨ ◻N ∧ WF(A)_v ⟶ ◻P ⟶ ♢⟨A⟩_v" by force
  qed
  hence "⊨ ◻N ∧ WF(A)_v ⟶ ◻(◻P ⟶ ♢⟨A⟩_v)"
    by (simp add: STL5[int_rewrite])
  with AA22[OF h1 h2 h4] show ?thesis by force
qed

text ‹Lamport's version of the rule is derived as a special case.›

theorem WF1: 
  assumes h1: "|~ P ∧ [N]_v ⟶ ◯P ∨ ◯Q"
      and h2: "|~ P ∧ ⟨N ∧ A⟩_v ⟶ ◯Q"
      and h3: "⊨ P ⟶ Enabled ⟨A⟩_v"
      and h4: "|~ P ∧ Unchanged v ⟶ ◯P"
  shows "⊨ ◻[N]_v ∧ WF(A)_v ⟶ (P ↝ Q)"
proof -
  have "⊨ ◻◻[N]_v ∧ WF(A)_v ⟶ (P ↝ Q)"
  proof (rule WF1_general)
    from h1 T9[of N v] show "|~ P ∧ ◻[N]_v ⟶ ◯P ∨ ◯Q" by force
  next
    from T9[of N v] have "|~ P ∧ ◻[N]_v ∧ ⟨A⟩_v ⟶ P ∧ ⟨N ∧ A⟩_v"
      by (auto simp: actrans_def angle_actrans_def)
    from this h2 show "|~ P ∧ ◻[N]_v ∧ ⟨A⟩_v ⟶ ◯Q" by (rule pref_imp_trans)
  next
    from h3 T9[of N v] show "⊨ P ∧ ◻[N]_v ⟶ Enabled ⟨A⟩_v" by force
  qed (rule h4)
  thus ?thesis by simp
qed

text ‹
 The corresponding rule for strong fairness has an additional hypothesis
 ‹◻F›, which is typically a conjunction of other fairness properties
 used to prove that the helpful action eventually becomes enabled.
 ›

theorem SF1_general:
  assumes h1: "|~ P ∧ N ⟶ ◯P ∨ ◯Q"
      and h2: "|~ P ∧ N ∧ ⟨A⟩_v ⟶ ◯Q"
      and h3: "⊨ ◻P ∧ ◻N ∧ ◻F ⟶ ♢Enabled ⟨A⟩_v"
      and h4: "|~ P ∧ Unchanged w ⟶ ◯P"
  shows "⊨ ◻N ∧ SF(A)_v ∧ ◻F ⟶ (P ↝ Q)"
proof -
  have "⊨ ◻(◻N ∧ SF(A)_v ∧ ◻F) ⟶ ◻(◻P ⟶ ♢⟨A⟩_v)"
  proof (rule STL4)
    have "⊨ ◻(◻P ∧ ◻N ∧ ◻F) ⟶ ◻♢Enabled ⟨A⟩_v" by (rule STL4[OF h3])
    hence "⊨ ◻P ∧ ◻N ∧ ◻F ∧ SF(A)_v ⟶ ◻♢⟨A⟩_v" by (auto simp: StrongF_def STL5[int_rewrite])
    with ax1[of "TEMP ♢⟨A⟩_v"] show "⊨ ◻N ∧ SF(A)_v ∧ ◻F ⟶ ◻P ⟶ ♢⟨A⟩_v" by force
  qed
  hence "⊨ ◻N ∧ SF(A)_v ∧ ◻F ⟶ ◻(◻P ⟶ ♢⟨A⟩_v)"
    by (simp add: STL5[int_rewrite])
  with AA22[OF h1 h2 h4] show ?thesis by force
qed

theorem SF1:
  assumes h1: "|~ P ∧ [N]_v ⟶ ◯P ∨ ◯Q"
      and h2: "|~ P ∧ ⟨N ∧ A⟩_v ⟶ ◯Q"
      and h3: "⊨ ◻P ∧ ◻[N]_v ∧ ◻F ⟶ ♢Enabled ⟨A⟩_v"
      and h4: "|~ P ∧ Unchanged v ⟶ ◯P"
  shows "⊨ ◻[N]_v ∧ SF(A)_v ∧ ◻F ⟶ (P ↝ Q)"
proof -
  have "⊨ ◻◻[N]_v ∧ SF(A)_v ∧ ◻F ⟶ (P ↝ Q)"
  proof (rule SF1_general)
    from h1 T9[of N v] show "|~ P ∧ ◻[N]_v ⟶ ◯P ∨ ◯Q" by force
  next
    from T9[of N v] have "|~ P ∧ ◻[N]_v ∧ ⟨A⟩_v ⟶ P ∧ ⟨N ∧ A⟩_v"
      by (auto simp: actrans_def angle_actrans_def)
    from this h2 show "|~ P ∧ ◻[N]_v ∧ ⟨A⟩_v ⟶ ◯Q" by (rule pref_imp_trans)
  next
    from h3 show "⊨ ◻P ∧ ◻◻[N]_v ∧ ◻F ⟶ ♢Enabled ⟨A⟩_v" by simp
  qed (rule h4)
  thus ?thesis by simp
qed

text ‹
 Lamport proposes the following rule as an introduction rule for ‹WF› formulas.
 ›

theorem WF2:
  assumes h1: "|~ ⟨N ∧ B⟩_f ⟶ ⟨M⟩_g"
      and h2: "|~ P ∧ ◯P ∧ ⟨N ∧ A⟩_f ⟶ B"
      and h3: "⊨ P ∧ Enabled ⟨M⟩_g ⟶ Enabled ⟨A⟩_f"
      and h4: "⊨ ◻[N ∧ ¬B]_f ∧ WF(A)_f ∧ ◻F ∧ ♢◻Enabled ⟨M⟩_g ⟶ ♢◻P"
  shows "⊨ ◻[N]_f ∧ WF(A)_f ∧ ◻F ⟶ WF(M)_g"
proof -
  have "⊨ ◻[N]_f ∧ WF(A)_f ∧ ◻F ∧ ♢◻Enabled ⟨M⟩_g ∧ ¬◻♢⟨M⟩_g ⟶ ◻♢⟨M⟩_g"
  proof -
    have 1: "⊨ ◻[N]_f ∧ WF(A)_f ∧ ◻F ∧ ♢◻Enabled ⟨M⟩_g ∧ ¬◻♢⟨M⟩_g ⟶ ♢◻P"
    proof -
      have A: "⊨ ◻[N]_f ∧ WF(A)_f ∧ ◻F ∧ ♢◻Enabled ⟨M⟩_g ∧ ¬◻♢⟨M⟩_g ⟶
                 ◻(◻[N]_f ∧ WF(A)_f ∧ ◻F) ∧ ♢◻(♢◻Enabled ⟨M⟩_g ∧ ◻[¬M]_g)"
        unfolding STL6[int_rewrite] (* important to do this before STL5 is applied *)
        by (auto simp: STL5[int_rewrite] dualization_rew)
      have B: "⊨ ◻(◻[N]_f ∧ WF(A)_f ∧ ◻F) ∧ ♢◻(♢◻Enabled ⟨M⟩_g ∧ ◻[¬M]_g) ⟶
                 ♢((◻[N]_f ∧ WF(A)_f ∧ ◻F) ∧ ◻(♢◻Enabled ⟨M⟩_g ∧ ◻[¬M]_g))"
        by (rule SE2)
      from lift_imp_trans[OF A B]
      have "⊨ ◻[N]_f ∧ WF(A)_f ∧ ◻F ∧ ♢◻Enabled ⟨M⟩_g ∧ ¬◻♢⟨M⟩_g ⟶
              ♢((◻[N]_f ∧ WF(A)_f ∧ ◻F) ∧ (♢◻Enabled ⟨M⟩_g ∧ ◻[¬M]_g))"
        by (simp add: STL5[int_rewrite])
      moreover
      from h1 have "|~ [N]_f ⟶ [¬M]_g ⟶ [N ∧ ¬B]_f" by (auto simp: actrans_def angle_actrans_def)
      hence "⊨ ◻[[N]_f]_f ⟶ ◻[[¬M]_g ⟶ [N ∧ ¬B]_f]_f" by (rule M2)
      from lift_imp_trans[OF this ax4] have "⊨ ◻[N]_f ∧ ◻[¬M]_g ⟶ ◻[N ∧ ¬B]_f"
        by (force intro: T4[unlift_rule])
      with h4 have "⊨ (◻[N]_f ∧ WF(A)_f ∧ ◻F) ∧ (♢◻Enabled ⟨M⟩_g ∧ ◻[¬M]_g) ⟶ ♢◻P"
        by force
      from STL4_eve[OF this]
      have "⊨ ♢((◻[N]_f ∧ WF(A)_f ∧ ◻F) ∧ (♢◻Enabled ⟨M⟩_g ∧ ◻[¬M]_g)) ⟶ ♢◻P" by simp
      ultimately
      show ?thesis by (rule lift_imp_trans)
    qed
    have 2: "⊨ ◻[N]_f ∧ WF(A)_f ∧ ♢◻Enabled ⟨M⟩_g ∧ ♢◻P ⟶ ◻♢⟨M⟩_g"
    proof -
      have A: "⊨ ♢◻P ∧ ♢◻Enabled ⟨M⟩_g ∧ WF(A)_f ⟶ ◻♢⟨A⟩_f"
        using h3[THEN STL4, THEN STL4_eve] by (auto simp: STL6[int_rewrite] WeakF_def)
      have B: "⊨ ◻[N]_f ∧ ♢◻P ∧ ◻♢⟨A⟩_f ⟶ ◻♢⟨M⟩_g"
      proof -
        from M1[of P f] have "⊨ ◻P ∧ ◻♢⟨N ∧ A⟩_f ⟶ ◻♢⟨(P ∧ ◯P) ∧ (N ∧ A)⟩_f"
          by (force intro: AA29[unlift_rule])
        hence "⊨ ♢◻(◻P ∧ ◻♢⟨N ∧ A⟩_f) ⟶ ♢◻◻♢⟨(P ∧ ◯P) ∧ (N ∧ A)⟩_f"
          by (rule STL4_eve[OF STL4])
        hence "⊨ ♢◻P ∧ ◻♢⟨N ∧ A⟩_f ⟶ ◻♢⟨(P ∧ ◯P) ∧ (N ∧ A)⟩_f"
          by (simp add: STL6[int_rewrite])
        with AA29[of N f A]
        have B1: "⊨ ◻[N]_f ∧ ♢◻P ∧ ◻♢⟨A⟩_f ⟶ ◻♢⟨(P ∧ ◯P) ∧ (N ∧ A)⟩_f" by force
        from h2 have "|~ ⟨(P ∧ ◯P) ∧ (N ∧ A)⟩_f ⟶ ⟨N ∧ B⟩_f"
          by (auto simp: angle_actrans_sem[unlifted])
        from B1 this[THEN AA25, THEN STL4] have "⊨ ◻[N]_f ∧ ♢◻P ∧ ◻♢⟨A⟩_f ⟶ ◻♢⟨N ∧ B⟩_f"
          by (rule lift_imp_trans)
        moreover
        have "⊨ ◻♢⟨N ∧ B⟩_f ⟶ ◻♢⟨M⟩_g" by (rule h1[THEN AA25, THEN STL4])
        ultimately show ?thesis by (rule lift_imp_trans)
      qed
      from A B show ?thesis by force
    qed
    from 1 2 show ?thesis by force
  qed
  thus ?thesis by (auto simp: WeakF_def)
qed

text ‹
 Lamport proposes an analogous theorem for introducing strong fairness, and its
 proof is very similar, in fact, it was obtained by copy and paste, with minimal
 modifications.
 ›

theorem SF2:
  assumes h1: "|~ ⟨N ∧ B⟩_f ⟶ ⟨M⟩_g"
      and h2: "|~ P ∧ ◯P ∧ ⟨N ∧ A⟩_f ⟶ B"
      and h3: "⊨ P ∧ Enabled ⟨M⟩_g ⟶ Enabled ⟨A⟩_f"
      and h4: "⊨ ◻[N ∧ ¬B]_f ∧ SF(A)_f ∧ ◻F ∧ ◻♢Enabled ⟨M⟩_g ⟶ ♢◻P"
  shows "⊨ ◻[N]_f ∧ SF(A)_f ∧ ◻F ⟶ SF(M)_g"
proof -
  have "⊨ ◻[N]_f ∧ SF(A)_f ∧ ◻F ∧ ◻♢Enabled ⟨M⟩_g ∧ ¬◻♢⟨M⟩_g ⟶ ◻♢⟨M⟩_g"
  proof -
    have 1: "⊨ ◻[N]_f ∧ SF(A)_f ∧ ◻F ∧ ◻♢Enabled ⟨M⟩_g ∧ ¬◻♢⟨M⟩_g ⟶ ♢◻P"
    proof -
      have A: "⊨ ◻[N]_f ∧ SF(A)_f ∧ ◻F ∧ ◻♢Enabled ⟨M⟩_g ∧ ¬◻♢⟨M⟩_g ⟶
                 ◻(◻[N]_f ∧ SF(A)_f ∧ ◻F) ∧ ♢◻(◻♢Enabled ⟨M⟩_g ∧ ◻[¬M]_g)"
        unfolding STL6[int_rewrite] (* important to do this before STL5 is applied *)
        by (auto simp: STL5[int_rewrite] dualization_rew)
      have B: "⊨ ◻(◻[N]_f ∧ SF(A)_f ∧ ◻F) ∧ ♢◻(◻♢Enabled ⟨M⟩_g ∧ ◻[¬M]_g) ⟶
                 ♢((◻[N]_f ∧ SF(A)_f ∧ ◻F) ∧ ◻(◻♢Enabled ⟨M⟩_g ∧ ◻[¬M]_g))"
        by (rule SE2)
      from lift_imp_trans[OF A B]
      have "⊨ ◻[N]_f ∧ SF(A)_f ∧ ◻F ∧ ◻♢Enabled ⟨M⟩_g ∧ ¬◻♢⟨M⟩_g ⟶
              ♢((◻[N]_f ∧ SF(A)_f ∧ ◻F) ∧ (◻♢Enabled ⟨M⟩_g ∧ ◻[¬M]_g))"
        by (simp add: STL5[int_rewrite])
      moreover
      from h1 have "|~ [N]_f ⟶ [¬M]_g ⟶ [N ∧ ¬B]_f" by (auto simp: actrans_def angle_actrans_def)
      hence "⊨ ◻[[N]_f]_f ⟶ ◻[[¬M]_g ⟶ [N ∧ ¬B]_f]_f" by (rule M2)
      from lift_imp_trans[OF this ax4] have "⊨ ◻[N]_f ∧ ◻[¬M]_g ⟶ ◻[N ∧ ¬B]_f"
        by (force intro: T4[unlift_rule])
      with h4 have "⊨ (◻[N]_f ∧ SF(A)_f ∧ ◻F) ∧ (◻♢Enabled ⟨M⟩_g ∧ ◻[¬M]_g) ⟶ ♢◻P"
        by force
      from STL4_eve[OF this]
      have "⊨ ♢((◻[N]_f ∧ SF(A)_f ∧ ◻F) ∧ (◻♢Enabled ⟨M⟩_g ∧ ◻[¬M]_g)) ⟶ ♢◻P" by simp
      ultimately
      show ?thesis by (rule lift_imp_trans)
    qed
    have 2: "⊨ ◻[N]_f ∧ SF(A)_f ∧ ◻♢Enabled ⟨M⟩_g ∧ ♢◻P ⟶ ◻♢⟨M⟩_g"
    proof -
      have "⊨ ◻♢(P ∧ Enabled ⟨M⟩_g) ∧ SF(A)_f ⟶ ◻♢⟨A⟩_f"
        using h3[THEN STL4_eve, THEN STL4] by (auto simp: StrongF_def)
      with E28 have A: "⊨ ♢◻P ∧ ◻♢Enabled ⟨M⟩_g ∧ SF(A)_f ⟶ ◻♢⟨A⟩_f"
        by force
      have B: "⊨ ◻[N]_f ∧ ♢◻P ∧ ◻♢⟨A⟩_f ⟶ ◻♢⟨M⟩_g"
      proof -
        from M1[of P f] have "⊨ ◻P ∧ ◻♢⟨N ∧ A⟩_f ⟶ ◻♢⟨(P ∧ ◯P) ∧ (N ∧ A)⟩_f"
          by (force intro: AA29[unlift_rule])
        hence "⊨ ♢◻(◻P ∧ ◻♢⟨N ∧ A⟩_f) ⟶ ♢◻◻♢⟨(P ∧ ◯P) ∧ (N ∧ A)⟩_f"
          by (rule STL4_eve[OF STL4])
        hence "⊨ ♢◻P ∧ ◻♢⟨N ∧ A⟩_f ⟶ ◻♢⟨(P ∧ ◯P) ∧ (N ∧ A)⟩_f"
          by (simp add: STL6[int_rewrite])
        with AA29[of N f A]
        have B1: "⊨ ◻[N]_f ∧ ♢◻P ∧ ◻♢⟨A⟩_f ⟶ ◻♢⟨(P ∧ ◯P) ∧ (N ∧ A)⟩_f" by force
        from h2 have "|~ ⟨(P ∧ ◯P) ∧ (N ∧ A)⟩_f ⟶ ⟨N ∧ B⟩_f"
          by (auto simp: angle_actrans_sem[unlifted])
        from B1 this[THEN AA25, THEN STL4] have "⊨ ◻[N]_f ∧ ♢◻P ∧ ◻♢⟨A⟩_f ⟶ ◻♢⟨N ∧ B⟩_f"
          by (rule lift_imp_trans)
        moreover
        have "⊨ ◻♢⟨N ∧ B⟩_f ⟶ ◻♢⟨M⟩_g" by (rule h1[THEN AA25, THEN STL4])
        ultimately show ?thesis by (rule lift_imp_trans)
      qed
      from A B show ?thesis by force
    qed
    from 1 2 show ?thesis by force
  qed
  thus ?thesis by (auto simp: StrongF_def)
qed

text ‹This is the lattice rule from TLA›

theorem wf_leadsto:
  assumes h1: "wf r"
      and h2: "∧x. ⊨ F x ↝ (G ∨ (∃y. #((y,x) ∈ r) ∧ F y))"
  shows       "⊨ F x ↝ G"
using h1
proof (rule wf_induct)
  fix x
  assume ih: "∀y. (y, x) ∈ r ⟶ (⊨ F y ↝ G)"
  show "⊨ F x ↝ G"
  proof -
    from ih have "⊨ (∃y. #((y,x) ∈ r) ∧ F y) ↝ G"
      by (force simp: LT21[int_rewrite] LT33[int_rewrite])
    with h2 show ?thesis by (force intro: LT19[unlift_rule])
  qed
qed

subsection "Stuttering Invariance"

theorem stut_Enabled: "STUTINV Enabled ⟨F⟩_v"
  by (auto simp: enabled_def stutinv_def dest!: sim_first)

theorem stut_WF: "NSTUTINV F ==> STUTINV WF(F)_v"
  by (auto simp: WeakF_def stut_Enabled bothstutinvs)

theorem stut_SF: "NSTUTINV F ==> STUTINV SF(F)_v"
  by (auto simp: StrongF_def stut_Enabled bothstutinvs)

lemmas livestutinv = stut_WF stut_SF stut_Enabled

end