header {* 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 ∧ \<box>[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: "\<turnstile> Enabled ⟨m1⟩_(x,y)"
proof (clarify)
fix s
show "s \<Turnstile> Enabled ⟨m1⟩_(x,y)"
by (rule base_enabled[OF bvar]) (auto simp: m1_def tla_defs)
qed
lemma (in Firstprogram) enabled_m2: "\<turnstile> Enabled ⟨m2⟩_(x,y)"
proof (clarify)
fix s
show "s \<Turnstile> 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 ∧ \<box>[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 @{text I} is an inductive invariant of specification @{text psi}.
*}
lemma (in Secondprogram) psiI: "\<turnstile> psi --> \<box>I"
proof -
have init: "\<turnstile> initPsi --> I" by (auto simp: initPsi_def I_def)
have "|~ I ∧ Unchanged vars --> oI" by (auto simp: I_def vars_def tla_defs)
moreover
have "|~ I ∧ n1 --> oI" by (auto simp: I_def Sact2_defs tla_defs)
moreover
have "|~ I ∧ n2 --> oI" by (auto simp: I_def Sact2_defs tla_defs)
ultimately have step: "|~ I ∧ [n1 ∨ n2]_vars --> oI" by (force simp: actrans_def)
from init step have goal: "\<turnstile> initPsi ∧ \<box>[n1 ∨ n2]_vars --> \<box>I" by (rule invmono)
have "\<turnstile> initPsi ∧ \<box>[n1 ∨ n2]_vars ∧ Live2 ==> \<turnstile> initPsi ∧ \<box>[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: "\<turnstile> psi --> init ∧ \<box>[m1 ∨ m2]_(x,y)"
proof -
have "\<turnstile> initPsi ∧ \<box>I ∧ \<box>[n1 ∨ n2]_vars --> init ∧ \<box>[m1 ∨ m2]_(x,y)"
proof (rule refinement1)
show "\<turnstile> initPsi --> init" by (auto simp: initPsi_def init_def)
next
show "|~ I ∧ oI ∧ [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: "\<turnstile> $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 \<Turnstile> Enabled alpha1"
by (intro base_enabled[OF bvar2]) (auto simp: Sact2_defs tla_defs vars_def)
qed
lemma (in Secondprogram) enab_beta1: "\<turnstile> $pc1 = #b --> Enabled beta1"
proof (clarsimp simp: tla_defs)
fix s :: "state seq"
assume "pc1 (s 0) = b"
thus "s \<Turnstile> Enabled beta1"
by (intro base_enabled[OF bvar2]) (auto simp: Sact2_defs tla_defs vars_def)
qed
lemma (in Secondprogram) enab_gamma1: "\<turnstile> $pc1 = #g --> Enabled gamma1"
proof (clarsimp simp: tla_defs)
fix s :: "state seq"
assume "pc1 (s 0) = g"
thus "s \<Turnstile> Enabled gamma1"
by (intro base_enabled[OF bvar2]) (auto simp: Sact2_defs tla_defs vars_def)
qed
lemma (in Secondprogram) enab_n1:
"\<turnstile> Enabled ⟨n1⟩_vars = ($pc1 = #a --> # 0 < $sem)"
unfolding n1_ch[int_rewrite] proof (rule int_iffI)
show "\<turnstile> Enabled n1 --> $pc1 = #a --> # 0 < $sem"
by (auto elim!: enabledE simp: Sact2_defs tla_defs)
next
show "\<turnstile> ($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 \<Turnstile> 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: "\<turnstile> $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 \<Turnstile> Enabled alpha2"
by (intro base_enabled[OF bvar2]) (auto simp: Sact2_defs tla_defs vars_def)
qed
lemma (in Secondprogram) enab_beta2: "\<turnstile> $pc2 = #b --> Enabled beta2"
proof (clarsimp simp: tla_defs)
fix s :: "state seq"
assume "pc2 (s 0) = b"
thus "s \<Turnstile> Enabled beta2"
by (intro base_enabled[OF bvar2]) (auto simp: Sact2_defs tla_defs vars_def)
qed
lemma (in Secondprogram) enab_gamma2: "\<turnstile> $pc2 = #g --> Enabled gamma2"
proof (clarsimp simp: tla_defs)
fix s :: "state seq"
assume "pc2 (s 0) = g"
thus "s \<Turnstile> Enabled gamma2"
by (intro base_enabled[OF bvar2]) (auto simp: Sact2_defs tla_defs vars_def)
qed
lemma (in Secondprogram) enab_n2:
"\<turnstile> Enabled ⟨n2⟩_vars = ($pc2 = #a --> # 0 < $sem)"
unfolding n2_ch[int_rewrite] proof (rule int_iffI)
show "\<turnstile> Enabled n2 --> $pc2 = #a --> # 0 < $sem"
by (auto elim!: enabledE simp: Sact2_defs tla_defs)
next
show "\<turnstile> ($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 \<Turnstile> 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 @{text SF2} to prove that @{text psi} implements strong fairness
for the abstract action @{text m1}. Since strong fairness implies weak fairness,
it follows that @{text psi} refines the liveness condition of @{text phi}.
*}
lemma (in Secondprogram) psi_fair_m1: "\<turnstile> psi --> SF(m1)_(x,y)"
proof -
have "\<turnstile> \<box>[n1 ∨ n2]_vars ∧ SF(n1)_vars ∧ \<box>(I ∧ SF(n2)_vars) --> SF(m1)_(x,y)"
proof (rule SF2)
txt {*
Rule @{text SF2} requires us to choose a helpful action (whose effect implies
@{text "⟨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 @{text beta1} and the persistent condition is @{text "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 ∧ o($pc1 = #b) ∧ ⟨(n1 ∨ n2) ∧ n1⟩_vars --> beta1"
by (auto simp: n1_def alpha1_def beta1_def gamma1_def tla_defs)
next
show "\<turnstile> $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 "\<turnstile> \<box>[(n1 ∨ n2) ∧ ¬ beta1]_vars
∧ SF(n1)_vars ∧ \<box>(I ∧ SF(n2)_vars) ∧ \<box>\<diamond>Enabled ⟨m1⟩_(x, y)
--> \<diamond>\<box>($pc1 = #b)"
proof -
have "\<turnstile> \<box>\<box>[(n1 ∨ n2) ∧ ¬ beta1]_vars --> \<box>($pc1 = #b --> \<box>($pc1 = #b))"
proof (rule STL4)
have "|~ $pc1 = #b ∧ [(n1 ∨ n2) ∧ ¬ beta1]_vars --> o($pc1 = #b)"
by (auto simp: Sact2_defs vars_def tla_defs)
from this[THEN INV1]
show "\<turnstile> \<box>[(n1 ∨ n2) ∧ ¬ beta1]_vars --> $pc1 = #b --> \<box>($pc1 = #b)" by auto
qed
hence 1: "\<turnstile> \<box>[(n1 ∨ n2) ∧ ¬ beta1]_vars --> \<diamond>($pc1 = #b) --> \<diamond>\<box>($pc1 = #b)"
by (force intro: E31[unlift_rule])
have "\<turnstile> \<box>[(n1 ∨ n2) ∧ ¬ beta1]_vars ∧ SF(n1)_vars ∧ \<box>(I ∧ SF(n2)_vars)
--> \<diamond>($pc1 = #b)"
proof -
txt {*
The plan of the proof is to show that from any state where @{text "pc1 = g"}
one eventually reaches @{text "pc1 = a"}, from where one eventually reaches
@{text "pc1 = b"}. The result follows by combining leadsto properties.
*}
let ?F = "LIFT (\<box>[(n1 ∨ n2) ∧ ¬ beta1]_vars ∧ SF(n1)_vars ∧ \<box>(I ∧ SF(n2)_vars))"
txt {*
Showing that @{text "pc1 = g"} leads to @{text "pc1 = a"} is a simple
application of rule @{text SF1} because the first process completely
controls this transition.
*}
have ga: "\<turnstile> ?F --> ($pc1 = #g \<leadsto> $pc1 = #a)"
proof (rule SF1)
show "|~ $pc1 = #g ∧ [(n1 ∨ n2) ∧ ¬ beta1]_vars --> o($pc1 = #g) ∨ o($pc1 = #a)"
by (auto simp: Sact2_defs vars_def tla_defs)
next
show "|~ $pc1 = #g ∧ ⟨((n1 ∨ n2) ∧ ¬ beta1) ∧ n1⟩_vars --> o($pc1 = #a)"
by (auto simp: Sact2_defs vars_def tla_defs)
next
show "|~ $pc1 = #g ∧ Unchanged vars --> o($pc1 = #g)"
by (auto simp: vars_def tla_defs)
next
have "\<turnstile> $pc1 = #g --> Enabled ⟨n1⟩_vars"
unfolding enab_n1[int_rewrite] by (auto simp: tla_defs)
hence "\<turnstile> \<box>($pc1 = #g) --> Enabled ⟨n1⟩_vars"
by (rule lift_imp_trans[OF ax1])
hence "\<turnstile> \<box>($pc1 = #g) --> \<diamond>Enabled ⟨n1⟩_vars"
by (rule lift_imp_trans[OF _ E3])
thus "\<turnstile> \<box>($pc1 = #g) ∧ \<box>[(n1 ∨ n2) ∧ ¬ beta1]_vars ∧ \<box>(I ∧ SF(n2)_vars)
--> \<diamond>Enabled ⟨n1⟩_vars"
by auto
qed
txt {*
The proof that @{text "pc1 = a"} leads to @{text "pc1 = b"} follows
the same basic schema. However, showing that @{text n1} is eventually
enabled requires reasoning about the second process, which must liberate
the critical section.
*}
have ab: "\<turnstile> ?F --> ($pc1 = #a \<leadsto> $pc1 = #b)"
proof (rule SF1)
show "|~ $pc1 = #a ∧ [(n1 ∨ n2) ∧ ¬ beta1]_vars --> o($pc1 = #a) ∨ o($pc1 = #b)"
by (auto simp: Sact2_defs vars_def tla_defs)
next
show "|~ $pc1 = #a ∧ ⟨((n1 ∨ n2) ∧ ¬ beta1) ∧ n1⟩_vars --> o($pc1 = #b)"
by (auto simp: Sact2_defs vars_def tla_defs)
next
show "|~ $pc1 = #a ∧ Unchanged vars --> o($pc1 = #a)"
by (auto simp: vars_def tla_defs)
next
txt {* We establish a suitable leadsto-chain. *}
let ?G = "LIFT \<box>[(n1 ∨ n2) ∧ ¬ beta1]_vars ∧ SF(n2)_vars ∧ \<box>($pc1 = #a ∧ I)"
have "\<turnstile> ?G --> \<diamond>($pc2 = #a ∧ $pc1 = #a ∧ I)"
proof -
txt {* Rule @{text SF1} takes us from @{text "pc2 = b"} to @{text "pc2 = g"}. *}
have bg2: "\<turnstile> ?G --> ($pc2 = #b \<leadsto> $pc2 = #g)"
proof (rule SF1)
show "|~ $pc2 = #b ∧ [(n1 ∨ n2) ∧ ¬beta1]_vars --> o($pc2 = #b) ∨ o($pc2 = #g)"
by (auto simp: Sact2_defs vars_def tla_defs)
next
show "|~ $pc2 = #b ∧ ⟨((n1 ∨ n2) ∧ ¬beta1) ∧ n2⟩_vars --> o($pc2 = #g)"
by (auto simp: Sact2_defs vars_def tla_defs)
next
show "|~ $pc2 = #b ∧ Unchanged vars --> o($pc2 = #b)"
by (auto simp: vars_def tla_defs)
next
have "\<turnstile> $pc2 = #b --> Enabled ⟨n2⟩_vars"
unfolding enab_n2[int_rewrite] by (auto simp: tla_defs)
hence "\<turnstile> \<box>($pc2 = #b) --> Enabled ⟨n2⟩_vars"
by (rule lift_imp_trans[OF ax1])
hence "\<turnstile> \<box>($pc2 = #b) --> \<diamond>Enabled ⟨n2⟩_vars"
by (rule lift_imp_trans[OF _ E3])
thus "\<turnstile> \<box>($pc2 = #b) ∧ \<box>[(n1 ∨ n2) ∧ ¬beta1]_vars ∧ \<box>($pc1 = #a ∧ I)
--> \<diamond>Enabled ⟨n2⟩_vars"
by auto
qed
txt {* Similarly, @{text "pc2 = b"} leads to @{text "pc2 = g"}. *}
have ga2: "\<turnstile> ?G --> ($pc2 = #g \<leadsto> $pc2 = #a)"
proof (rule SF1)
show "|~ $pc2 = #g ∧ [(n1 ∨ n2) ∧ ¬beta1]_vars --> o($pc2 = #g) ∨ o($pc2 = #a)"
by (auto simp: Sact2_defs vars_def tla_defs)
next
show "|~ $pc2 = #g ∧ ⟨((n1 ∨ n2) ∧ ¬beta1) ∧ n2⟩_vars --> o($pc2 = #a)"
by (auto simp: n2_def alpha2_def beta2_def gamma2_def vars_def tla_defs)
next
show "|~ $pc2 = #g ∧ Unchanged vars --> o($pc2 = #g)"
by (auto simp: vars_def tla_defs)
next
have "\<turnstile> $pc2 = #g --> Enabled ⟨n2⟩_vars"
unfolding enab_n2[int_rewrite] by (auto simp: tla_defs)
hence "\<turnstile> \<box>($pc2 = #g) --> Enabled ⟨n2⟩_vars"
by (rule lift_imp_trans[OF ax1])
hence "\<turnstile> \<box>($pc2 = #g) --> \<diamond>Enabled ⟨n2⟩_vars"
by (rule lift_imp_trans[OF _ E3])
thus "\<turnstile> \<box>($pc2 = #g) ∧ \<box>[(n1 ∨ n2) ∧ ¬beta1]_vars ∧ \<box>($pc1 = #a ∧ I)
--> \<diamond>Enabled ⟨n2⟩_vars"
by auto
qed
with bg2 have "\<turnstile> ?G --> ($pc2 = #b \<leadsto> $pc2 = #a)"
by (force elim: LT13[unlift_rule])
with ga2 have "\<turnstile> ?G --> ($pc2 = #a ∨ $pc2 = #b ∨ $pc2 = #g) \<leadsto> ($pc2 = #a)"
unfolding LT17[int_rewrite] LT1[int_rewrite] by force
moreover
have "\<turnstile> $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 "\<turnstile> (($pc2 = #a ∨ $pc2 = #b ∨ $pc2 = #g) \<leadsto> $pc2 = #a) --> \<diamond>($pc2 = #a)"
by (rule fmp[OF _ LT4])
ultimately
have "\<turnstile> ?G --> \<diamond>($pc2 = #a)" by force
thus ?thesis by (auto intro!: SE3[unlift_rule])
qed
moreover
have "\<turnstile> \<diamond>($pc2 = #a ∧ $pc1 = #a ∧ I) --> \<diamond>Enabled ⟨n1⟩_vars"
unfolding enab_n1[int_rewrite] by (rule STL4_eve) (auto simp: I_def tla_defs)
ultimately
show "\<turnstile> \<box>($pc1 = #a) ∧ \<box>[(n1 ∨ n2) ∧ ¬ beta1]_vars ∧ \<box>(I ∧ SF(n2)_vars)
--> \<diamond>Enabled ⟨n1⟩_vars"
by (force simp: STL5[int_rewrite])
qed
from ga ab have "\<turnstile> ?F --> ($pc1 = #g \<leadsto> $pc1 = #b)"
by (force elim: LT13[unlift_rule])
with ab have "\<turnstile> ?F --> (($pc1 = #a ∨ $pc1 = #b ∨ $pc1 = #g) \<leadsto> $pc1 = #b)"
unfolding LT17[int_rewrite] LT1[int_rewrite] by force
moreover
have "\<turnstile> $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 "\<turnstile> (($pc1 = #a ∨ $pc1 = #b ∨ $pc1 = #g) \<leadsto> $pc1 = #b) --> \<diamond>($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 @{text psi} implements strong fairness
for the abstract action @{text m1}. The proof is obtained by copy and paste
from the previous one.
*}
lemma (in Secondprogram) psi_fair_m2: "\<turnstile> psi --> SF(m2)_(x,y)"
proof -
have "\<turnstile> \<box>[n1 ∨ n2]_vars ∧ SF(n2)_vars ∧ \<box>(I ∧ SF(n1)_vars) --> SF(m2)_(x,y)"
proof (rule SF2)
txt {*
Rule @{text SF2} requires us to choose a helpful action (whose effect implies
@{text "⟨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 @{text beta2} and the persistent condition is @{text "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 ∧ o($pc2 = #b) ∧ ⟨(n1 ∨ n2) ∧ n2⟩_vars --> beta2"
by (auto simp: n2_def alpha2_def beta2_def gamma2_def tla_defs)
next
show "\<turnstile> $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 "\<turnstile> \<box>[(n1 ∨ n2) ∧ ¬ beta2]_vars
∧ SF(n2)_vars ∧ \<box>(I ∧ SF(n1)_vars) ∧ \<box>\<diamond>Enabled ⟨m2⟩_(x, y)
--> \<diamond>\<box>($pc2 = #b)"
proof -
have "\<turnstile> \<box>\<box>[(n1 ∨ n2) ∧ ¬ beta2]_vars --> \<box>($pc2 = #b --> \<box>($pc2 = #b))"
proof (rule STL4)
have "|~ $pc2 = #b ∧ [(n1 ∨ n2) ∧ ¬ beta2]_vars --> o($pc2 = #b)"
by (auto simp: Sact2_defs vars_def tla_defs)
from this[THEN INV1]
show "\<turnstile> \<box>[(n1 ∨ n2) ∧ ¬ beta2]_vars --> $pc2 = #b --> \<box>($pc2 = #b)" by auto
qed
hence 1: "\<turnstile> \<box>[(n1 ∨ n2) ∧ ¬ beta2]_vars --> \<diamond>($pc2 = #b) --> \<diamond>\<box>($pc2 = #b)"
by (force intro: E31[unlift_rule])
have "\<turnstile> \<box>[(n1 ∨ n2) ∧ ¬ beta2]_vars ∧ SF(n2)_vars ∧ \<box>(I ∧ SF(n1)_vars)
--> \<diamond>($pc2 = #b)"
proof -
txt {*
The plan of the proof is to show that from any state where @{text "pc2 = g"}
one eventually reaches @{text "pc2 = a"}, from where one eventually reaches
@{text "pc2 = b"}. The result follows by combining leadsto properties.
*}
let ?F = "LIFT (\<box>[(n1 ∨ n2) ∧ ¬ beta2]_vars ∧ SF(n2)_vars ∧ \<box>(I ∧ SF(n1)_vars))"
txt {*
Showing that @{text "pc2 = g"} leads to @{text "pc2 = a"} is a simple
application of rule @{text SF1} because the second process completely
controls this transition.
*}
have ga: "\<turnstile> ?F --> ($pc2 = #g \<leadsto> $pc2 = #a)"
proof (rule SF1)
show "|~ $pc2 = #g ∧ [(n1 ∨ n2) ∧ ¬ beta2]_vars --> o($pc2 = #g) ∨ o($pc2 = #a)"
by (auto simp: Sact2_defs vars_def tla_defs)
next
show "|~ $pc2 = #g ∧ ⟨((n1 ∨ n2) ∧ ¬ beta2) ∧ n2⟩_vars --> o($pc2 = #a)"
by (auto simp: n2_def alpha2_def beta2_def gamma2_def vars_def tla_defs)
next
show "|~ $pc2 = #g ∧ Unchanged vars --> o($pc2 = #g)"
by (auto simp: vars_def tla_defs)
next
have "\<turnstile> $pc2 = #g --> Enabled ⟨n2⟩_vars"
unfolding enab_n2[int_rewrite] by (auto simp: tla_defs)
hence "\<turnstile> \<box>($pc2 = #g) --> Enabled ⟨n2⟩_vars"
by (rule lift_imp_trans[OF ax1])
hence "\<turnstile> \<box>($pc2 = #g) --> \<diamond>Enabled ⟨n2⟩_vars"
by (rule lift_imp_trans[OF _ E3])
thus "\<turnstile> \<box>($pc2 = #g) ∧ \<box>[(n1 ∨ n2) ∧ ¬ beta2]_vars ∧ \<box>(I ∧ SF(n1)_vars)
--> \<diamond>Enabled ⟨n2⟩_vars"
by auto
qed
txt {*
The proof that @{text "pc2 = a"} leads to @{text "pc2 = b"} follows
the same basic schema. However, showing that @{text n2} is eventually
enabled requires reasoning about the second process, which must liberate
the critical section.
*}
have ab: "\<turnstile> ?F --> ($pc2 = #a \<leadsto> $pc2 = #b)"
proof (rule SF1)
show "|~ $pc2 = #a ∧ [(n1 ∨ n2) ∧ ¬ beta2]_vars --> o($pc2 = #a) ∨ o($pc2 = #b)"
by (auto simp: Sact2_defs vars_def tla_defs)
next
show "|~ $pc2 = #a ∧ ⟨((n1 ∨ n2) ∧ ¬ beta2) ∧ n2⟩_vars --> o($pc2 = #b)"
by (auto simp: n2_def alpha2_def beta2_def gamma2_def vars_def tla_defs)
next
show "|~ $pc2 = #a ∧ Unchanged vars --> o($pc2 = #a)"
by (auto simp: vars_def tla_defs)
next
txt {* We establish a suitable leadsto-chain. *}
let ?G = "LIFT \<box>[(n1 ∨ n2) ∧ ¬ beta2]_vars ∧ SF(n1)_vars ∧ \<box>($pc2 = #a ∧ I)"
have "\<turnstile> ?G --> \<diamond>($pc1 = #a ∧ $pc2 = #a ∧ I)"
proof -
txt {* Rule @{text SF1} takes us from @{text "pc1 = b"} to @{text "pc1 = g"}. *}
have bg1: "\<turnstile> ?G --> ($pc1 = #b \<leadsto> $pc1 = #g)"
proof (rule SF1)
show "|~ $pc1 = #b ∧ [(n1 ∨ n2) ∧ ¬beta2]_vars --> o($pc1 = #b) ∨ o($pc1 = #g)"
by (auto simp: Sact2_defs vars_def tla_defs)
next
show "|~ $pc1 = #b ∧ ⟨((n1 ∨ n2) ∧ ¬beta2) ∧ n1⟩_vars --> o($pc1 = #g)"
by (auto simp: n1_def alpha1_def beta1_def gamma1_def vars_def tla_defs)
next
show "|~ $pc1 = #b ∧ Unchanged vars --> o($pc1 = #b)"
by (auto simp: vars_def tla_defs)
next
have "\<turnstile> $pc1 = #b --> Enabled ⟨n1⟩_vars"
unfolding enab_n1[int_rewrite] by (auto simp: tla_defs)
hence "\<turnstile> \<box>($pc1 = #b) --> Enabled ⟨n1⟩_vars"
by (rule lift_imp_trans[OF ax1])
hence "\<turnstile> \<box>($pc1 = #b) --> \<diamond>Enabled ⟨n1⟩_vars"
by (rule lift_imp_trans[OF _ E3])
thus "\<turnstile> \<box>($pc1 = #b) ∧ \<box>[(n1 ∨ n2) ∧ ¬beta2]_vars ∧ \<box>($pc2 = #a ∧ I)
--> \<diamond>Enabled ⟨n1⟩_vars"
by auto
qed
txt {* Similarly, @{text "pc1 = b"} leads to @{text "pc1 = g"}. *}
have ga1: "\<turnstile> ?G --> ($pc1 = #g \<leadsto> $pc1 = #a)"
proof (rule SF1)
show "|~ $pc1 = #g ∧ [(n1 ∨ n2) ∧ ¬beta2]_vars --> o($pc1 = #g) ∨ o($pc1 = #a)"
by (auto simp: Sact2_defs vars_def tla_defs)
next
show "|~ $pc1 = #g ∧ ⟨((n1 ∨ n2) ∧ ¬beta2) ∧ n1⟩_vars --> o($pc1 = #a)"
by (auto simp: n1_def alpha1_def beta1_def gamma1_def vars_def tla_defs)
next
show "|~ $pc1 = #g ∧ Unchanged vars --> o($pc1 = #g)"
by (auto simp: vars_def tla_defs)
next
have "\<turnstile> $pc1 = #g --> Enabled ⟨n1⟩_vars"
unfolding enab_n1[int_rewrite] by (auto simp: tla_defs)
hence "\<turnstile> \<box>($pc1 = #g) --> Enabled ⟨n1⟩_vars"
by (rule lift_imp_trans[OF ax1])
hence "\<turnstile> \<box>($pc1 = #g) --> \<diamond>Enabled ⟨n1⟩_vars"
by (rule lift_imp_trans[OF _ E3])
thus "\<turnstile> \<box>($pc1 = #g) ∧ \<box>[(n1 ∨ n2) ∧ ¬beta2]_vars ∧ \<box>($pc2 = #a ∧ I)
--> \<diamond>Enabled ⟨n1⟩_vars"
by auto
qed
with bg1 have "\<turnstile> ?G --> ($pc1 = #b \<leadsto> $pc1 = #a)"
by (force elim: LT13[unlift_rule])
with ga1 have "\<turnstile> ?G --> ($pc1 = #a ∨ $pc1 = #b ∨ $pc1 = #g) \<leadsto> ($pc1 = #a)"
unfolding LT17[int_rewrite] LT1[int_rewrite] by force
moreover
have "\<turnstile> $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 "\<turnstile> (($pc1 = #a ∨ $pc1 = #b ∨ $pc1 = #g) \<leadsto> $pc1 = #a) --> \<diamond>($pc1 = #a)"
by (rule fmp[OF _ LT4])
ultimately
have "\<turnstile> ?G --> \<diamond>($pc1 = #a)" by force
thus ?thesis by (auto intro!: SE3[unlift_rule])
qed
moreover
have "\<turnstile> \<diamond>($pc1 = #a ∧ $pc2 = #a ∧ I) --> \<diamond>Enabled ⟨n2⟩_vars"
unfolding enab_n2[int_rewrite] by (rule STL4_eve) (auto simp: I_def tla_defs)
ultimately
show "\<turnstile> \<box>($pc2 = #a) ∧ \<box>[(n1 ∨ n2) ∧ ¬ beta2]_vars ∧ \<box>(I ∧ SF(n1)_vars)
--> \<diamond>Enabled ⟨n2⟩_vars"
by (force simp: STL5[int_rewrite])
qed
from ga ab have "\<turnstile> ?F --> ($pc2 = #g \<leadsto> $pc2 = #b)"
by (force elim: LT13[unlift_rule])
with ab have "\<turnstile> ?F --> (($pc2 = #a ∨ $pc2 = #b ∨ $pc2 = #g) \<leadsto> $pc2 = #b)"
unfolding LT17[int_rewrite] LT1[int_rewrite] by force
moreover
have "\<turnstile> $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 "\<turnstile> (($pc2 = #a ∨ $pc2 = #b ∨ $pc2 = #g) \<leadsto> $pc2 = #b) --> \<diamond>($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 @{text psi}
implements @{text phi}.
*}
theorem (in Secondprogram) impl: "\<turnstile> 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