# Theory Liveness

Up to index of Isabelle/HOL/TLA

theory Liveness
imports Rules
`(*  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 "Liveness"theory Livenessimports Rulesbegintext{* This theory derives proof rules for liveness properties.*}definition enabled :: "'a formula => 'a formula"where "enabled F ≡ λ s. ∃ t. ((first s) ## t) \<Turnstile> F"syntax "_Enabled" :: "lift => lift" ("(Enabled _)" [90] 90)translations "_Enabled" \<rightleftharpoons> "CONST enabled"definition WeakF :: "('a::world) formula => ('a,'b) stfun => 'a formula"where "WeakF F v ≡ TEMP \<diamond>\<box>Enabled ⟨F⟩_v --> \<box>\<diamond>⟨F⟩_v"definition StrongF :: "('a::world) formula => ('a,'b) stfun => 'a formula"where "StrongF F v ≡ TEMP \<box>\<diamond>Enabled ⟨F⟩_v --> \<box>\<diamond>⟨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 @{text 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" \<rightleftharpoons> "CONST WeakF" "_SF" \<rightleftharpoons> "CONST StrongF" "_WFsp" \<rightharpoonup> "CONST WeakF" "_SFsp" \<rightharpoonup> "CONST StrongF"subsection "Properties of @{term enabled}"theorem enabledI: "\<turnstile> F --> Enabled F"proof (clarsimp)  fix w  assume "w \<Turnstile> F"  with seq_app_first_tail[of w] have "((first w) ## tail w) \<Turnstile> F" by simp  thus "w \<Turnstile> Enabled F" by (auto simp: enabled_def)qedtheorem enabledE:  assumes "s \<Turnstile> Enabled F" and "!!u. (first s ## u) \<Turnstile> F ==> Q"  shows "Q"  using assms unfolding enabled_def by blastlemma enabled_mono:   assumes "w \<Turnstile> Enabled F" and "\<turnstile> F --> G"   shows "w \<Turnstile> Enabled G"  using assms[unlifted] unfolding enabled_def by blastlemma Enabled_disj1: "\<turnstile> Enabled F --> Enabled (F ∨ G)"  by (auto simp: enabled_def)lemma  Enabled_disj2: "\<turnstile> Enabled F --> Enabled (G ∨ F)"  by (auto simp: enabled_def)lemma  Enabled_conj1: "\<turnstile> Enabled (F ∧ G) --> Enabled F"  by (auto simp: enabled_def)lemma  Enabled_conj2: "\<turnstile> Enabled (G ∧ F) --> Enabled F"  by (auto simp: enabled_def)lemma Enabled_disjD: "\<turnstile> Enabled (F ∨ G) --> Enabled F ∨ Enabled G"  by (auto simp: enabled_def)lemma Enabled_disj: "\<turnstile> Enabled (F ∨ G) = (Enabled F ∨ Enabled G)"  by (auto simp: enabled_def)lemmas enabled_disj_rew = Enabled_disj[int_rewrite]lemma Enabled_ex: "\<turnstile> Enabled (∃ x. F x) = (∃ x. Enabled (F x))"  by (force simp: enabled_def)subsection "Fairness Properties" lemma WF_alt: "\<turnstile> WF(A)_v = (\<box>\<diamond>¬Enabled ⟨A⟩_v ∨ \<box>\<diamond>⟨A⟩_v)"proof -  have "\<turnstile> WF(A)_v = (¬\<diamond>\<box> Enabled ⟨A⟩_v ∨ \<box>\<diamond>⟨A⟩_v)" by (auto simp: WeakF_def)  thus ?thesis by (simp add: dualization_rew)qedlemma SF_alt: "\<turnstile> SF(A)_v = (\<diamond>\<box>¬Enabled ⟨A⟩_v ∨ \<box>\<diamond>⟨A⟩_v)"proof -  have "\<turnstile> SF(A)_v = (¬\<box>\<diamond> Enabled ⟨A⟩_v ∨ \<box>\<diamond>⟨A⟩_v)" by (auto simp: StrongF_def)  thus ?thesis by (simp add: dualization_rew)qedlemma alwaysWFI: "\<turnstile> WF(A)_v --> \<box>WF(A)_v"  unfolding WF_alt[int_rewrite] by (rule MM6)theorem WF_always[simp_unl]: "\<turnstile> \<box>WF(A)_v = WF(A)_v"  by (rule int_iffI[OF ax1 alwaysWFI])theorem WF_eventually[simp_unl]: "\<turnstile> \<diamond>WF(A)_v = WF(A)_v"proof -  have 1: "\<turnstile> ¬WF(A)_v = (\<diamond>\<box>Enabled ⟨A⟩_v ∧ ¬ \<box>\<diamond>⟨A⟩_v)"    by (auto simp: WeakF_def)  have "\<turnstile> \<box>¬WF(A)_v = ¬WF(A)_v"    by (simp add: 1[int_rewrite] STL5[int_rewrite] dualization_rew)  thus ?thesis    by (auto simp: eventually_def)qedlemma alwaysSFI: "\<turnstile> SF(A)_v --> \<box>SF(A)_v"proof -  have "\<turnstile> \<box>\<diamond>\<box>¬Enabled ⟨A⟩_v ∨ \<box>\<diamond>⟨A⟩_v --> \<box>(\<box>\<diamond>\<box>¬Enabled ⟨A⟩_v ∨ \<box>\<diamond>⟨A⟩_v)"    by (rule MM6)  thus ?thesis unfolding SF_alt[int_rewrite] by simpqedtheorem SF_always[simp_unl]: "\<turnstile> \<box>SF(A)_v = SF(A)_v"  by (rule int_iffI[OF ax1 alwaysSFI])theorem SF_eventually[simp_unl]: "\<turnstile> \<diamond>SF(A)_v = SF(A)_v"proof -  have 1: "\<turnstile> ¬SF(A)_v = (\<box>\<diamond>Enabled ⟨A⟩_v ∧ ¬ \<box>\<diamond>⟨A⟩_v)"    by (auto simp: StrongF_def)  have "\<turnstile> \<box>¬SF(A)_v = ¬SF(A)_v"    by (simp add: 1[int_rewrite] STL5[int_rewrite] dualization_rew)  thus ?thesis    by (auto simp: eventually_def)qedtheorem SF_imp_WF: "\<turnstile> SF (A)_v --> WF (A)_v"  unfolding WeakF_def StrongF_def by (auto dest: E20[unlift_rule])lemma enabled_WFSF: "\<turnstile> \<box>Enabled ⟨F⟩_v --> (WF(F)_v = SF(F)_v)"proof -  have "\<turnstile> \<box>Enabled ⟨F⟩_v --> \<diamond>\<box>Enabled ⟨F⟩_v" by (rule E3)  hence "\<turnstile> \<box>Enabled ⟨F⟩_v --> WF(F)_v --> SF(F)_v" by (auto simp: WeakF_def StrongF_def)  moreover  have "\<turnstile> \<box>Enabled ⟨F⟩_v --> \<box>\<diamond>Enabled ⟨F⟩_v" by (rule STL4[OF E3])  hence "\<turnstile> \<box>Enabled ⟨F⟩_v --> SF(F)_v --> WF(F)_v" by (auto simp: WeakF_def StrongF_def)  ultimately show ?thesis by forceqedtheorem WF1_general:  assumes h1: "|~ P ∧ N --> oP ∨ oQ"      and h2: "|~ P ∧ N ∧ ⟨A⟩_v --> oQ"      and h3: "\<turnstile> P ∧ N --> Enabled ⟨A⟩_v"      and h4: "|~ P ∧ Unchanged w --> oP"  shows "\<turnstile> \<box>N ∧ WF(A)_v --> (P \<leadsto> Q)"proof -  have "\<turnstile> \<box>(\<box>N ∧ WF(A)_v) --> \<box>(\<box>P --> \<diamond>⟨A⟩_v)"  proof (rule STL4)    have "\<turnstile> \<box>(P ∧ N) --> \<diamond>\<box>Enabled ⟨A⟩_v" by (rule lift_imp_trans[OF h3[THEN STL4] E3])    hence "\<turnstile> \<box>P ∧ \<box>N ∧ WF(A)_v --> \<box>\<diamond>⟨A⟩_v" by (auto simp: WeakF_def STL5[int_rewrite])    with ax1[of "TEMP \<diamond>⟨A⟩_v"] show "\<turnstile> \<box>N ∧ WF(A)_v --> \<box>P --> \<diamond>⟨A⟩_v" by force  qed  hence "\<turnstile> \<box>N ∧ WF(A)_v --> \<box>(\<box>P --> \<diamond>⟨A⟩_v)"    by (simp add: STL5[int_rewrite])  with AA22[OF h1 h2 h4] show ?thesis by forceqedtext {* Lamport's version of the rule is derived as a special case. *}theorem WF1:   assumes h1: "|~ P ∧ [N]_v --> oP ∨ oQ"      and h2: "|~ P ∧ ⟨N ∧ A⟩_v --> oQ"      and h3: "\<turnstile> P --> Enabled ⟨A⟩_v"      and h4: "|~ P ∧ Unchanged v --> oP"  shows "\<turnstile> \<box>[N]_v ∧ WF(A)_v --> (P \<leadsto> Q)"proof -  have "\<turnstile> \<box>\<box>[N]_v ∧ WF(A)_v --> (P \<leadsto> Q)"  proof (rule WF1_general)    from h1 T9[of N v] show "|~ P ∧ \<box>[N]_v --> oP ∨ oQ" by force  next    from T9[of N v] have "|~ P ∧ \<box>[N]_v ∧ ⟨A⟩_v --> P ∧ ⟨N ∧ A⟩_v"      by (auto simp: actrans_def angle_actrans_def)    from this h2 show "|~ P ∧ \<box>[N]_v ∧ ⟨A⟩_v --> oQ" by (rule pref_imp_trans)  next    from h3 T9[of N v] show "\<turnstile> P ∧ \<box>[N]_v --> Enabled ⟨A⟩_v" by force  qed (rule h4)  thus ?thesis by simpqedtext {*  The corresponding rule for strong fairness has an additional hypothesis  @{text "\<box>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 --> oP ∨ oQ"      and h2: "|~ P ∧ N ∧ ⟨A⟩_v --> oQ"      and h3: "\<turnstile> \<box>P ∧ \<box>N ∧ \<box>F --> \<diamond>Enabled ⟨A⟩_v"      and h4: "|~ P ∧ Unchanged w --> oP"  shows "\<turnstile> \<box>N ∧ SF(A)_v ∧ \<box>F --> (P \<leadsto> Q)"proof -  have "\<turnstile> \<box>(\<box>N ∧ SF(A)_v ∧ \<box>F) --> \<box>(\<box>P --> \<diamond>⟨A⟩_v)"  proof (rule STL4)    have "\<turnstile> \<box>(\<box>P ∧ \<box>N ∧ \<box>F) --> \<box>\<diamond>Enabled ⟨A⟩_v" by (rule STL4[OF h3])    hence "\<turnstile> \<box>P ∧ \<box>N ∧ \<box>F ∧ SF(A)_v --> \<box>\<diamond>⟨A⟩_v" by (auto simp: StrongF_def STL5[int_rewrite])    with ax1[of "TEMP \<diamond>⟨A⟩_v"] show "\<turnstile> \<box>N ∧ SF(A)_v ∧ \<box>F --> \<box>P --> \<diamond>⟨A⟩_v" by force  qed  hence "\<turnstile> \<box>N ∧ SF(A)_v ∧ \<box>F --> \<box>(\<box>P --> \<diamond>⟨A⟩_v)"    by (simp add: STL5[int_rewrite])  with AA22[OF h1 h2 h4] show ?thesis by forceqedtheorem SF1:  assumes h1: "|~ P ∧ [N]_v --> oP ∨ oQ"      and h2: "|~ P ∧ ⟨N ∧ A⟩_v --> oQ"      and h3: "\<turnstile> \<box>P ∧ \<box>[N]_v ∧ \<box>F --> \<diamond>Enabled ⟨A⟩_v"      and h4: "|~ P ∧ Unchanged v --> oP"  shows "\<turnstile> \<box>[N]_v ∧ SF(A)_v ∧ \<box>F --> (P \<leadsto> Q)"proof -  have "\<turnstile> \<box>\<box>[N]_v ∧ SF(A)_v ∧ \<box>F --> (P \<leadsto> Q)"  proof (rule SF1_general)    from h1 T9[of N v] show "|~ P ∧ \<box>[N]_v --> oP ∨ oQ" by force  next    from T9[of N v] have "|~ P ∧ \<box>[N]_v ∧ ⟨A⟩_v --> P ∧ ⟨N ∧ A⟩_v"      by (auto simp: actrans_def angle_actrans_def)    from this h2 show "|~ P ∧ \<box>[N]_v ∧ ⟨A⟩_v --> oQ" by (rule pref_imp_trans)  next    from h3 show "\<turnstile> \<box>P ∧ \<box>\<box>[N]_v ∧ \<box>F --> \<diamond>Enabled ⟨A⟩_v" by simp  qed (rule h4)  thus ?thesis by simpqedtext {*  Lamport proposes the following rule as an introduction rule for @{text WF} formulas.*}theorem WF2:  assumes h1: "|~ ⟨N ∧ B⟩_f --> ⟨M⟩_g"      and h2: "|~ P ∧ oP ∧ ⟨N ∧ A⟩_f --> B"      and h3: "\<turnstile> P ∧ Enabled ⟨M⟩_g --> Enabled ⟨A⟩_f"      and h4: "\<turnstile> \<box>[N ∧ ¬B]_f ∧ WF(A)_f ∧ \<box>F ∧ \<diamond>\<box>Enabled ⟨M⟩_g --> \<diamond>\<box>P"  shows "\<turnstile> \<box>[N]_f ∧ WF(A)_f ∧ \<box>F --> WF(M)_g"proof -  have "\<turnstile> \<box>[N]_f ∧ WF(A)_f ∧ \<box>F ∧ \<diamond>\<box>Enabled ⟨M⟩_g ∧ ¬\<box>\<diamond>⟨M⟩_g --> \<box>\<diamond>⟨M⟩_g"  proof -    have 1: "\<turnstile> \<box>[N]_f ∧ WF(A)_f ∧ \<box>F ∧ \<diamond>\<box>Enabled ⟨M⟩_g ∧ ¬\<box>\<diamond>⟨M⟩_g --> \<diamond>\<box>P"    proof -      have A: "\<turnstile> \<box>[N]_f ∧ WF(A)_f ∧ \<box>F ∧ \<diamond>\<box>Enabled ⟨M⟩_g ∧ ¬\<box>\<diamond>⟨M⟩_g -->                 \<box>(\<box>[N]_f ∧ WF(A)_f ∧ \<box>F) ∧ \<diamond>\<box>(\<diamond>\<box>Enabled ⟨M⟩_g ∧ \<box>[¬M]_g)"        unfolding STL6[int_rewrite] (* important to do this before STL5 is applied *)        by (auto simp: STL5[int_rewrite] dualization_rew)      have B: "\<turnstile> \<box>(\<box>[N]_f ∧ WF(A)_f ∧ \<box>F) ∧ \<diamond>\<box>(\<diamond>\<box>Enabled ⟨M⟩_g ∧ \<box>[¬M]_g) -->                 \<diamond>((\<box>[N]_f ∧ WF(A)_f ∧ \<box>F) ∧ \<box>(\<diamond>\<box>Enabled ⟨M⟩_g ∧ \<box>[¬M]_g))"        by (rule SE2)      from lift_imp_trans[OF A B]      have "\<turnstile> \<box>[N]_f ∧ WF(A)_f ∧ \<box>F ∧ \<diamond>\<box>Enabled ⟨M⟩_g ∧ ¬\<box>\<diamond>⟨M⟩_g -->              \<diamond>((\<box>[N]_f ∧ WF(A)_f ∧ \<box>F) ∧ (\<diamond>\<box>Enabled ⟨M⟩_g ∧ \<box>[¬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 "\<turnstile> \<box>[[N]_f]_f --> \<box>[[¬M]_g --> [N ∧ ¬B]_f]_f" by (rule M2)      from lift_imp_trans[OF this ax4] have "\<turnstile> \<box>[N]_f ∧ \<box>[¬M]_g --> \<box>[N ∧ ¬B]_f"        by (force intro: T4[unlift_rule])      with h4 have "\<turnstile> (\<box>[N]_f ∧ WF(A)_f ∧ \<box>F) ∧ (\<diamond>\<box>Enabled ⟨M⟩_g ∧ \<box>[¬M]_g) --> \<diamond>\<box>P"        by force      from STL4_eve[OF this]      have "\<turnstile> \<diamond>((\<box>[N]_f ∧ WF(A)_f ∧ \<box>F) ∧ (\<diamond>\<box>Enabled ⟨M⟩_g ∧ \<box>[¬M]_g)) --> \<diamond>\<box>P" by simp      ultimately      show ?thesis by (rule lift_imp_trans)    qed    have 2: "\<turnstile> \<box>[N]_f ∧ WF(A)_f ∧ \<diamond>\<box>Enabled ⟨M⟩_g ∧ \<diamond>\<box>P --> \<box>\<diamond>⟨M⟩_g"    proof -      have A: "\<turnstile> \<diamond>\<box>P ∧ \<diamond>\<box>Enabled ⟨M⟩_g ∧ WF(A)_f --> \<box>\<diamond>⟨A⟩_f"        using h3[THEN STL4, THEN STL4_eve] by (auto simp: STL6[int_rewrite] WeakF_def)      have B: "\<turnstile> \<box>[N]_f ∧ \<diamond>\<box>P ∧  \<box>\<diamond>⟨A⟩_f --> \<box>\<diamond>⟨M⟩_g"      proof -        from M1[of P f] have "\<turnstile> \<box>P ∧ \<box>\<diamond>⟨N ∧ A⟩_f --> \<box>\<diamond>⟨(P ∧ oP) ∧ (N ∧ A)⟩_f"          by (force intro: AA29[unlift_rule])        hence "\<turnstile> \<diamond>\<box>(\<box>P ∧ \<box>\<diamond>⟨N ∧ A⟩_f) --> \<diamond>\<box>\<box>\<diamond>⟨(P ∧ oP) ∧ (N ∧ A)⟩_f"          by (rule STL4_eve[OF STL4])        hence "\<turnstile> \<diamond>\<box>P ∧ \<box>\<diamond>⟨N ∧ A⟩_f --> \<box>\<diamond>⟨(P ∧ oP) ∧ (N ∧ A)⟩_f"          by (simp add: STL6[int_rewrite])        with AA29[of N f A]        have B1: "\<turnstile> \<box>[N]_f ∧ \<diamond>\<box>P ∧  \<box>\<diamond>⟨A⟩_f --> \<box>\<diamond>⟨(P ∧ oP) ∧ (N ∧ A)⟩_f" by force        from h2 have "|~ ⟨(P ∧ oP) ∧ (N ∧ A)⟩_f --> ⟨N ∧ B⟩_f"          by (auto simp: angle_actrans_sem[unlifted])        from B1 this[THEN AA25, THEN STL4] have "\<turnstile> \<box>[N]_f ∧ \<diamond>\<box>P ∧  \<box>\<diamond>⟨A⟩_f --> \<box>\<diamond>⟨N ∧ B⟩_f"          by (rule lift_imp_trans)        moreover        have "\<turnstile> \<box>\<diamond>⟨N ∧ B⟩_f --> \<box>\<diamond>⟨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)qedtext {*  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 ∧ oP ∧ ⟨N ∧ A⟩_f --> B"      and h3: "\<turnstile> P ∧ Enabled ⟨M⟩_g --> Enabled ⟨A⟩_f"      and h4: "\<turnstile> \<box>[N ∧ ¬B]_f ∧ SF(A)_f ∧ \<box>F ∧ \<box>\<diamond>Enabled ⟨M⟩_g --> \<diamond>\<box>P"  shows "\<turnstile> \<box>[N]_f ∧ SF(A)_f ∧ \<box>F --> SF(M)_g"proof -  have "\<turnstile> \<box>[N]_f ∧ SF(A)_f ∧ \<box>F ∧ \<box>\<diamond>Enabled ⟨M⟩_g ∧ ¬\<box>\<diamond>⟨M⟩_g --> \<box>\<diamond>⟨M⟩_g"  proof -    have 1: "\<turnstile> \<box>[N]_f ∧ SF(A)_f ∧ \<box>F ∧ \<box>\<diamond>Enabled ⟨M⟩_g ∧ ¬\<box>\<diamond>⟨M⟩_g --> \<diamond>\<box>P"    proof -      have A: "\<turnstile> \<box>[N]_f ∧ SF(A)_f ∧ \<box>F ∧ \<box>\<diamond>Enabled ⟨M⟩_g ∧ ¬\<box>\<diamond>⟨M⟩_g -->                 \<box>(\<box>[N]_f ∧ SF(A)_f ∧ \<box>F) ∧ \<diamond>\<box>(\<box>\<diamond>Enabled ⟨M⟩_g ∧ \<box>[¬M]_g)"        unfolding STL6[int_rewrite] (* important to do this before STL5 is applied *)        by (auto simp: STL5[int_rewrite] dualization_rew)      have B: "\<turnstile> \<box>(\<box>[N]_f ∧ SF(A)_f ∧ \<box>F) ∧ \<diamond>\<box>(\<box>\<diamond>Enabled ⟨M⟩_g ∧ \<box>[¬M]_g) -->                 \<diamond>((\<box>[N]_f ∧ SF(A)_f ∧ \<box>F) ∧ \<box>(\<box>\<diamond>Enabled ⟨M⟩_g ∧ \<box>[¬M]_g))"        by (rule SE2)      from lift_imp_trans[OF A B]      have "\<turnstile> \<box>[N]_f ∧ SF(A)_f ∧ \<box>F ∧ \<box>\<diamond>Enabled ⟨M⟩_g ∧ ¬\<box>\<diamond>⟨M⟩_g -->              \<diamond>((\<box>[N]_f ∧ SF(A)_f ∧ \<box>F) ∧ (\<box>\<diamond>Enabled ⟨M⟩_g ∧ \<box>[¬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 "\<turnstile> \<box>[[N]_f]_f --> \<box>[[¬M]_g --> [N ∧ ¬B]_f]_f" by (rule M2)      from lift_imp_trans[OF this ax4] have "\<turnstile> \<box>[N]_f ∧ \<box>[¬M]_g --> \<box>[N ∧ ¬B]_f"        by (force intro: T4[unlift_rule])      with h4 have "\<turnstile> (\<box>[N]_f ∧ SF(A)_f ∧ \<box>F) ∧ (\<box>\<diamond>Enabled ⟨M⟩_g ∧ \<box>[¬M]_g) --> \<diamond>\<box>P"        by force      from STL4_eve[OF this]      have "\<turnstile> \<diamond>((\<box>[N]_f ∧ SF(A)_f ∧ \<box>F) ∧ (\<box>\<diamond>Enabled ⟨M⟩_g ∧ \<box>[¬M]_g)) --> \<diamond>\<box>P" by simp      ultimately      show ?thesis by (rule lift_imp_trans)    qed    have 2: "\<turnstile> \<box>[N]_f ∧ SF(A)_f ∧ \<box>\<diamond>Enabled ⟨M⟩_g ∧ \<diamond>\<box>P --> \<box>\<diamond>⟨M⟩_g"    proof -      have "\<turnstile> \<box>\<diamond>(P ∧ Enabled ⟨M⟩_g) ∧ SF(A)_f --> \<box>\<diamond>⟨A⟩_f"        using h3[THEN STL4_eve, THEN STL4] by (auto simp: StrongF_def)      with E28 have A: "\<turnstile> \<diamond>\<box>P ∧ \<box>\<diamond>Enabled ⟨M⟩_g ∧ SF(A)_f --> \<box>\<diamond>⟨A⟩_f"        by force      have B: "\<turnstile> \<box>[N]_f ∧ \<diamond>\<box>P ∧  \<box>\<diamond>⟨A⟩_f --> \<box>\<diamond>⟨M⟩_g"      proof -        from M1[of P f] have "\<turnstile> \<box>P ∧ \<box>\<diamond>⟨N ∧ A⟩_f --> \<box>\<diamond>⟨(P ∧ oP) ∧ (N ∧ A)⟩_f"          by (force intro: AA29[unlift_rule])        hence "\<turnstile> \<diamond>\<box>(\<box>P ∧ \<box>\<diamond>⟨N ∧ A⟩_f) --> \<diamond>\<box>\<box>\<diamond>⟨(P ∧ oP) ∧ (N ∧ A)⟩_f"          by (rule STL4_eve[OF STL4])        hence "\<turnstile> \<diamond>\<box>P ∧ \<box>\<diamond>⟨N ∧ A⟩_f --> \<box>\<diamond>⟨(P ∧ oP) ∧ (N ∧ A)⟩_f"          by (simp add: STL6[int_rewrite])        with AA29[of N f A]        have B1: "\<turnstile> \<box>[N]_f ∧ \<diamond>\<box>P ∧  \<box>\<diamond>⟨A⟩_f --> \<box>\<diamond>⟨(P ∧ oP) ∧ (N ∧ A)⟩_f" by force        from h2 have "|~ ⟨(P ∧ oP) ∧ (N ∧ A)⟩_f --> ⟨N ∧ B⟩_f"          by (auto simp: angle_actrans_sem[unlifted])        from B1 this[THEN AA25, THEN STL4] have "\<turnstile> \<box>[N]_f ∧ \<diamond>\<box>P ∧  \<box>\<diamond>⟨A⟩_f --> \<box>\<diamond>⟨N ∧ B⟩_f"          by (rule lift_imp_trans)        moreover        have "\<turnstile> \<box>\<diamond>⟨N ∧ B⟩_f --> \<box>\<diamond>⟨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)qedtext {* This is the lattice rule from TLA *}theorem wf_leadsto:  assumes h1: "wf r"      and h2: "!!x. \<turnstile> F x \<leadsto> (G ∨ (∃y. #((y,x) ∈ r) ∧ F y))"  shows       "\<turnstile> F x \<leadsto> G"using h1proof (rule wf_induct)  fix x  assume ih: "∀y. (y, x) ∈ r --> (\<turnstile> F y \<leadsto> G)"  show "\<turnstile> F x \<leadsto> G"  proof -    from ih have "\<turnstile> (∃y. #((y,x) ∈ r) ∧ F y) \<leadsto> G"      by (force simp: LT21[int_rewrite] LT33[int_rewrite])    with h2 show ?thesis by (force intro: LT19[unlift_rule])  qedqedsubsection "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_Enabledend`