--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Fri Jun 26 15:55:44 2015 +0200
@@ -63,7 +63,7 @@
definition
(* the environment action *)
ENext :: "PrIds \<Rightarrow> action"
- where "ENext p = ACT (\<exists>l. #l : #MemLoc & Call memCh p #(read l))"
+ where "ENext p = ACT (\<exists>l. #l \<in> #MemLoc \<and> Call memCh p #(read l))"
definition
@@ -74,7 +74,7 @@
definition
HNext :: "histType \<Rightarrow> PrIds \<Rightarrow> action"
where "HNext rmhist p = ACT (rmhist!p)$ =
- (if (MemReturn rmCh ires p | RPCFail crCh rmCh rst p)
+ (if (MemReturn rmCh ires p \<or> RPCFail crCh rmCh rst p)
then #histB
else if (MClkReply memCh crCh cst p)
then #histA
@@ -83,7 +83,7 @@
definition
HistP :: "histType \<Rightarrow> PrIds \<Rightarrow> temporal"
where "HistP rmhist p = (TEMP Init HInit rmhist p
- & \<box>[HNext rmhist p]_(c p,r p,m p, rmhist!p))"
+ \<and> \<box>[HNext rmhist p]_(c p,r p,m p, rmhist!p))"
definition
Hist :: "histType \<Rightarrow> temporal"
@@ -92,40 +92,40 @@
definition
(* the implementation *)
IPImp :: "PrIds \<Rightarrow> temporal"
- where "IPImp p = (TEMP ( Init \<not>Calling memCh p & \<box>[ENext p]_(e p)
- & MClkIPSpec memCh crCh cst p
- & RPCIPSpec crCh rmCh rst p
- & RPSpec rmCh mm ires p
- & (\<forall>l. #l : #MemLoc \<longrightarrow> MSpec rmCh mm ires l)))"
+ where "IPImp p = (TEMP ( Init \<not>Calling memCh p \<and> \<box>[ENext p]_(e p)
+ \<and> MClkIPSpec memCh crCh cst p
+ \<and> RPCIPSpec crCh rmCh rst p
+ \<and> RPSpec rmCh mm ires p
+ \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec rmCh mm ires l)))"
definition
ImpInit :: "PrIds \<Rightarrow> stpred"
where "ImpInit p = PRED ( \<not>Calling memCh p
- & MClkInit crCh cst p
- & RPCInit rmCh rst p
- & PInit ires p)"
+ \<and> MClkInit crCh cst p
+ \<and> RPCInit rmCh rst p
+ \<and> PInit ires p)"
definition
ImpNext :: "PrIds \<Rightarrow> action"
where "ImpNext p = (ACT [ENext p]_(e p)
- & [MClkNext memCh crCh cst p]_(c p)
- & [RPCNext crCh rmCh rst p]_(r p)
- & [RNext rmCh mm ires p]_(m p))"
+ \<and> [MClkNext memCh crCh cst p]_(c p)
+ \<and> [RPCNext crCh rmCh rst p]_(r p)
+ \<and> [RNext rmCh mm ires p]_(m p))"
definition
ImpLive :: "PrIds \<Rightarrow> temporal"
where "ImpLive p = (TEMP WF(MClkFwd memCh crCh cst p)_(c p)
- & SF(MClkReply memCh crCh cst p)_(c p)
- & WF(RPCNext crCh rmCh rst p)_(r p)
- & WF(RNext rmCh mm ires p)_(m p)
- & WF(MemReturn rmCh ires p)_(m p))"
+ \<and> SF(MClkReply memCh crCh cst p)_(c p)
+ \<and> WF(RPCNext crCh rmCh rst p)_(r p)
+ \<and> WF(RNext rmCh mm ires p)_(m p)
+ \<and> WF(MemReturn rmCh ires p)_(m p))"
definition
Implementation :: "temporal"
- where "Implementation = (TEMP ( (\<forall>p. Init (\<not>Calling memCh p) & \<box>[ENext p]_(e p))
- & MClkISpec memCh crCh cst
- & RPCISpec crCh rmCh rst
- & IRSpec rmCh mm ires))"
+ where "Implementation = (TEMP ( (\<forall>p. Init (\<not>Calling memCh p) \<and> \<box>[ENext p]_(e p))
+ \<and> MClkISpec memCh crCh cst
+ \<and> RPCISpec crCh rmCh rst
+ \<and> IRSpec rmCh mm ires))"
definition
(* the predicate S describes the states of the implementation.
@@ -137,17 +137,17 @@
S :: "histType \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> mClkState \<Rightarrow> rpcState \<Rightarrow> histState \<Rightarrow> histState \<Rightarrow> PrIds \<Rightarrow> stpred"
where "S rmhist ecalling ccalling rcalling cs rs hs1 hs2 p = (PRED
Calling memCh p = #ecalling
- & Calling crCh p = #ccalling
- & (#ccalling \<longrightarrow> arg<crCh!p> = MClkRelayArg<arg<memCh!p>>)
- & (\<not> #ccalling & cst!p = #clkB \<longrightarrow> MVOKBARF<res<crCh!p>>)
- & Calling rmCh p = #rcalling
- & (#rcalling \<longrightarrow> arg<rmCh!p> = RPCRelayArg<arg<crCh!p>>)
- & (\<not> #rcalling \<longrightarrow> ires!p = #NotAResult)
- & (\<not> #rcalling & rst!p = #rpcB \<longrightarrow> MVOKBA<res<rmCh!p>>)
- & cst!p = #cs
- & rst!p = #rs
- & (rmhist!p = #hs1 | rmhist!p = #hs2)
- & MVNROKBA<ires!p>)"
+ \<and> Calling crCh p = #ccalling
+ \<and> (#ccalling \<longrightarrow> arg<crCh!p> = MClkRelayArg<arg<memCh!p>>)
+ \<and> (\<not> #ccalling \<and> cst!p = #clkB \<longrightarrow> MVOKBARF<res<crCh!p>>)
+ \<and> Calling rmCh p = #rcalling
+ \<and> (#rcalling \<longrightarrow> arg<rmCh!p> = RPCRelayArg<arg<crCh!p>>)
+ \<and> (\<not> #rcalling \<longrightarrow> ires!p = #NotAResult)
+ \<and> (\<not> #rcalling \<and> rst!p = #rpcB \<longrightarrow> MVOKBA<res<rmCh!p>>)
+ \<and> cst!p = #cs
+ \<and> rst!p = #rs
+ \<and> (rmhist!p = #hs1 \<or> rmhist!p = #hs2)
+ \<and> MVNROKBA<ires!p>)"
definition
(* predicates S1 -- S6 define special instances of S *)
@@ -177,8 +177,8 @@
definition
(* The invariant asserts that the system is always in one of S1 - S6, for every p *)
ImpInv :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred"
- where "ImpInv rmhist p = (PRED (S1 rmhist p | S2 rmhist p | S3 rmhist p
- | S4 rmhist p | S5 rmhist p | S6 rmhist p))"
+ where "ImpInv rmhist p = (PRED (S1 rmhist p \<or> S2 rmhist p \<or> S3 rmhist p
+ \<or> S4 rmhist p \<or> S5 rmhist p \<or> S6 rmhist p))"
definition
resbar :: "histType \<Rightarrow> resType" (* refinement mapping *)
@@ -241,9 +241,9 @@
section "History variable"
-lemma HistoryLemma: "\<turnstile> Init(\<forall>p. ImpInit p) & \<box>(\<forall>p. ImpNext p)
+lemma HistoryLemma: "\<turnstile> Init(\<forall>p. ImpInit p) \<and> \<box>(\<forall>p. ImpNext p)
\<longrightarrow> (\<exists>\<exists>rmhist. Init(\<forall>p. HInit rmhist p)
- & \<box>(\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)))"
+ \<and> \<box>(\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)))"
apply clarsimp
apply (rule historyI)
apply assumption+
@@ -299,21 +299,21 @@
by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def S6_def)
*)
-lemma S2_excl: "\<turnstile> S2 rmhist p \<longrightarrow> S2 rmhist p & \<not>S1 rmhist p"
+lemma S2_excl: "\<turnstile> S2 rmhist p \<longrightarrow> S2 rmhist p \<and> \<not>S1 rmhist p"
by (auto simp: S_def S1_def S2_def)
-lemma S3_excl: "\<turnstile> S3 rmhist p \<longrightarrow> S3 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p"
+lemma S3_excl: "\<turnstile> S3 rmhist p \<longrightarrow> S3 rmhist p \<and> \<not>S1 rmhist p \<and> \<not>S2 rmhist p"
by (auto simp: S_def S1_def S2_def S3_def)
-lemma S4_excl: "\<turnstile> S4 rmhist p \<longrightarrow> S4 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p & \<not>S3 rmhist p"
+lemma S4_excl: "\<turnstile> S4 rmhist p \<longrightarrow> S4 rmhist p \<and> \<not>S1 rmhist p \<and> \<not>S2 rmhist p \<and> \<not>S3 rmhist p"
by (auto simp: S_def S1_def S2_def S3_def S4_def)
-lemma S5_excl: "\<turnstile> S5 rmhist p \<longrightarrow> S5 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p
- & \<not>S3 rmhist p & \<not>S4 rmhist p"
+lemma S5_excl: "\<turnstile> S5 rmhist p \<longrightarrow> S5 rmhist p \<and> \<not>S1 rmhist p \<and> \<not>S2 rmhist p
+ \<and> \<not>S3 rmhist p \<and> \<not>S4 rmhist p"
by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def)
-lemma S6_excl: "\<turnstile> S6 rmhist p \<longrightarrow> S6 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p
- & \<not>S3 rmhist p & \<not>S4 rmhist p & \<not>S5 rmhist p"
+lemma S6_excl: "\<turnstile> S6 rmhist p \<longrightarrow> S6 rmhist p \<and> \<not>S1 rmhist p \<and> \<not>S2 rmhist p
+ \<and> \<not>S3 rmhist p \<and> \<not>S4 rmhist p \<and> \<not>S5 rmhist p"
by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def S6_def)
@@ -331,24 +331,24 @@
(* ------------------------------ State S1 ---------------------------------------- *)
-lemma S1Env: "\<turnstile> ENext p & $(S1 rmhist p) & unchanged (c p, r p, m p, rmhist!p)
+lemma S1Env: "\<turnstile> ENext p \<and> $(S1 rmhist p) \<and> unchanged (c p, r p, m p, rmhist!p)
\<longrightarrow> (S2 rmhist p)$"
by (force simp: ENext_def Call_def c_def r_def m_def
caller_def rtrner_def MVNROKBA_def S_def S1_def S2_def Calling_def)
-lemma S1ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) & $(S1 rmhist p) \<longrightarrow> unchanged (c p)"
+lemma S1ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S1 rmhist p) \<longrightarrow> unchanged (c p)"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] dest!: MClkidle [temp_use] simp: S_def S1_def)
-lemma S1RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) & $(S1 rmhist p) \<longrightarrow> unchanged (r p)"
+lemma S1RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $(S1 rmhist p) \<longrightarrow> unchanged (r p)"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] dest!: RPCidle [temp_use] simp: S_def S1_def)
-lemma S1MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) & $(S1 rmhist p) \<longrightarrow> unchanged (m p)"
+lemma S1MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S1 rmhist p) \<longrightarrow> unchanged (m p)"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] dest!: Memoryidle [temp_use] simp: S_def S1_def)
-lemma S1Hist: "\<turnstile> [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S1 rmhist p)
+lemma S1Hist: "\<turnstile> [HNext rmhist p]_(c p,r p,m p,rmhist!p) \<and> $(S1 rmhist p)
\<longrightarrow> unchanged (rmhist!p)"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def}, @{thm S_def},
@{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def},
@@ -357,26 +357,26 @@
(* ------------------------------ State S2 ---------------------------------------- *)
-lemma S2EnvUnch: "\<turnstile> [ENext p]_(e p) & $(S2 rmhist p) \<longrightarrow> unchanged (e p)"
+lemma S2EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S2 rmhist p) \<longrightarrow> unchanged (e p)"
by (auto dest!: Envbusy [temp_use] simp: S_def S2_def)
-lemma S2Clerk: "\<turnstile> MClkNext memCh crCh cst p & $(S2 rmhist p) \<longrightarrow> MClkFwd memCh crCh cst p"
+lemma S2Clerk: "\<turnstile> MClkNext memCh crCh cst p \<and> $(S2 rmhist p) \<longrightarrow> MClkFwd memCh crCh cst p"
by (auto simp: MClkNext_def MClkRetry_def MClkReply_def S_def S2_def)
-lemma S2Forward: "\<turnstile> $(S2 rmhist p) & MClkFwd memCh crCh cst p
- & unchanged (e p, r p, m p, rmhist!p)
+lemma S2Forward: "\<turnstile> $(S2 rmhist p) \<and> MClkFwd memCh crCh cst p
+ \<and> unchanged (e p, r p, m p, rmhist!p)
\<longrightarrow> (S3 rmhist p)$"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
@{thm Call_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def},
@{thm rtrner_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1 *})
-lemma S2RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) & $(S2 rmhist p) \<longrightarrow> unchanged (r p)"
+lemma S2RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $(S2 rmhist p) \<longrightarrow> unchanged (r p)"
by (auto simp: S_def S2_def dest!: RPCidle [temp_use])
-lemma S2MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) & $(S2 rmhist p) \<longrightarrow> unchanged (m p)"
+lemma S2MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S2 rmhist p) \<longrightarrow> unchanged (m p)"
by (auto simp: S_def S2_def dest!: Memoryidle [temp_use])
-lemma S2Hist: "\<turnstile> [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S2 rmhist p)
+lemma S2Hist: "\<turnstile> [HNext rmhist p]_(c p,r p,m p,rmhist!p) \<and> $(S2 rmhist p)
\<longrightarrow> unchanged (rmhist!p)"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
@@ -384,61 +384,61 @@
(* ------------------------------ State S3 ---------------------------------------- *)
-lemma S3EnvUnch: "\<turnstile> [ENext p]_(e p) & $(S3 rmhist p) \<longrightarrow> unchanged (e p)"
+lemma S3EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S3 rmhist p) \<longrightarrow> unchanged (e p)"
by (auto dest!: Envbusy [temp_use] simp: S_def S3_def)
-lemma S3ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) & $(S3 rmhist p) \<longrightarrow> unchanged (c p)"
+lemma S3ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S3 rmhist p) \<longrightarrow> unchanged (c p)"
by (auto dest!: MClkbusy [temp_use] simp: square_def S_def S3_def)
lemma S3LegalRcvArg: "\<turnstile> S3 rmhist p \<longrightarrow> IsLegalRcvArg<arg<crCh!p>>"
by (auto simp: IsLegalRcvArg_def MClkRelayArg_def S_def S3_def)
-lemma S3RPC: "\<turnstile> RPCNext crCh rmCh rst p & $(S3 rmhist p)
- \<longrightarrow> RPCFwd crCh rmCh rst p | RPCFail crCh rmCh rst p"
+lemma S3RPC: "\<turnstile> RPCNext crCh rmCh rst p \<and> $(S3 rmhist p)
+ \<longrightarrow> RPCFwd crCh rmCh rst p \<or> RPCFail crCh rmCh rst p"
apply clarsimp
apply (frule S3LegalRcvArg [action_use])
apply (auto simp: RPCNext_def RPCReject_def RPCReply_def S_def S3_def)
done
-lemma S3Forward: "\<turnstile> RPCFwd crCh rmCh rst p & HNext rmhist p & $(S3 rmhist p)
- & unchanged (e p, c p, m p)
- \<longrightarrow> (S4 rmhist p)$ & unchanged (rmhist!p)"
+lemma S3Forward: "\<turnstile> RPCFwd crCh rmCh rst p \<and> HNext rmhist p \<and> $(S3 rmhist p)
+ \<and> unchanged (e p, c p, m p)
+ \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCFwd_def},
@{thm HNext_def}, @{thm MemReturn_def}, @{thm RPCFail_def},
@{thm MClkReply_def}, @{thm Return_def}, @{thm Call_def}, @{thm e_def},
@{thm c_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
@{thm S3_def}, @{thm S4_def}, @{thm Calling_def}]) [] [] 1 *})
-lemma S3Fail: "\<turnstile> RPCFail crCh rmCh rst p & $(S3 rmhist p) & HNext rmhist p
- & unchanged (e p, c p, m p)
+lemma S3Fail: "\<turnstile> RPCFail crCh rmCh rst p \<and> $(S3 rmhist p) \<and> HNext rmhist p
+ \<and> unchanged (e p, c p, m p)
\<longrightarrow> (S6 rmhist p)$"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def},
@{thm RPCFail_def}, @{thm Return_def}, @{thm e_def}, @{thm c_def},
@{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm MVOKBARF_def},
@{thm S_def}, @{thm S3_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
-lemma S3MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) & $(S3 rmhist p) \<longrightarrow> unchanged (m p)"
+lemma S3MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S3 rmhist p) \<longrightarrow> unchanged (m p)"
by (auto simp: S_def S3_def dest!: Memoryidle [temp_use])
-lemma S3Hist: "\<turnstile> HNext rmhist p & $(S3 rmhist p) & unchanged (r p) \<longrightarrow> unchanged (rmhist!p)"
+lemma S3Hist: "\<turnstile> HNext rmhist p \<and> $(S3 rmhist p) \<and> unchanged (r p) \<longrightarrow> unchanged (rmhist!p)"
by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def
Return_def r_def rtrner_def S_def S3_def Calling_def)
(* ------------------------------ State S4 ---------------------------------------- *)
-lemma S4EnvUnch: "\<turnstile> [ENext p]_(e p) & $(S4 rmhist p) \<longrightarrow> unchanged (e p)"
+lemma S4EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S4 rmhist p) \<longrightarrow> unchanged (e p)"
by (auto simp: S_def S4_def dest!: Envbusy [temp_use])
-lemma S4ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) & $(S4 rmhist p) \<longrightarrow> unchanged (c p)"
+lemma S4ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S4 rmhist p) \<longrightarrow> unchanged (c p)"
by (auto simp: S_def S4_def dest!: MClkbusy [temp_use])
-lemma S4RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) & $(S4 rmhist p) \<longrightarrow> unchanged (r p)"
+lemma S4RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $(S4 rmhist p) \<longrightarrow> unchanged (r p)"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] dest!: RPCbusy [temp_use] simp: S_def S4_def)
-lemma S4ReadInner: "\<turnstile> ReadInner rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
- & HNext rmhist p & $(MemInv mm l)
- \<longrightarrow> (S4 rmhist p)$ & unchanged (rmhist!p)"
+lemma S4ReadInner: "\<turnstile> ReadInner rmCh mm ires p l \<and> $(S4 rmhist p) \<and> unchanged (e p, c p, r p)
+ \<and> HNext rmhist p \<and> $(MemInv mm l)
+ \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm ReadInner_def},
@{thm GoodRead_def}, @{thm BadRead_def}, @{thm HNext_def}, @{thm MemReturn_def},
@{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
@@ -446,68 +446,68 @@
@{thm MVNROKBA_def}, @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def},
@{thm Calling_def}, @{thm MemInv_def}]) [] [] 1 *})
-lemma S4Read: "\<turnstile> Read rmCh mm ires p & $(S4 rmhist p) & unchanged (e p, c p, r p)
- & HNext rmhist p & (\<forall>l. $MemInv mm l)
- \<longrightarrow> (S4 rmhist p)$ & unchanged (rmhist!p)"
+lemma S4Read: "\<turnstile> Read rmCh mm ires p \<and> $(S4 rmhist p) \<and> unchanged (e p, c p, r p)
+ \<and> HNext rmhist p \<and> (\<forall>l. $MemInv mm l)
+ \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
by (auto simp: Read_def dest!: S4ReadInner [temp_use])
-lemma S4WriteInner: "\<turnstile> WriteInner rmCh mm ires p l v & $(S4 rmhist p) & unchanged (e p, c p, r p) & HNext rmhist p
- \<longrightarrow> (S4 rmhist p)$ & unchanged (rmhist!p)"
+lemma S4WriteInner: "\<turnstile> WriteInner rmCh mm ires p l v \<and> $(S4 rmhist p) \<and> unchanged (e p, c p, r p) \<and> HNext rmhist p
+ \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm WriteInner_def},
@{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm HNext_def}, @{thm MemReturn_def},
@{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
@{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def}, @{thm MVNROKBA_def},
@{thm S_def}, @{thm S4_def}, @{thm WrRequest_def}, @{thm Calling_def}]) [] [] 1 *})
-lemma S4Write: "\<turnstile> Write rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
- & (HNext rmhist p)
- \<longrightarrow> (S4 rmhist p)$ & unchanged (rmhist!p)"
+lemma S4Write: "\<turnstile> Write rmCh mm ires p l \<and> $(S4 rmhist p) \<and> unchanged (e p, c p, r p)
+ \<and> (HNext rmhist p)
+ \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
by (auto simp: Write_def dest!: S4WriteInner [temp_use])
-lemma WriteS4: "\<turnstile> $ImpInv rmhist p & Write rmCh mm ires p l \<longrightarrow> $S4 rmhist p"
+lemma WriteS4: "\<turnstile> $ImpInv rmhist p \<and> Write rmCh mm ires p l \<longrightarrow> $S4 rmhist p"
by (auto simp: Write_def WriteInner_def ImpInv_def
WrRequest_def S_def S1_def S2_def S3_def S4_def S5_def S6_def)
-lemma S4Return: "\<turnstile> MemReturn rmCh ires p & $S4 rmhist p & unchanged (e p, c p, r p)
- & HNext rmhist p
+lemma S4Return: "\<turnstile> MemReturn rmCh ires p \<and> $S4 rmhist p \<and> unchanged (e p, c p, r p)
+ \<and> HNext rmhist p
\<longrightarrow> (S5 rmhist p)$"
by (auto simp: HNext_def MemReturn_def Return_def e_def c_def r_def
rtrner_def caller_def MVNROKBA_def MVOKBA_def S_def S4_def S5_def Calling_def)
-lemma S4Hist: "\<turnstile> HNext rmhist p & $S4 rmhist p & (m p)$ = $(m p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
+lemma S4Hist: "\<turnstile> HNext rmhist p \<and> $S4 rmhist p \<and> (m p)$ = $(m p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def
Return_def m_def rtrner_def S_def S4_def Calling_def)
(* ------------------------------ State S5 ---------------------------------------- *)
-lemma S5EnvUnch: "\<turnstile> [ENext p]_(e p) & $(S5 rmhist p) \<longrightarrow> unchanged (e p)"
+lemma S5EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S5 rmhist p) \<longrightarrow> unchanged (e p)"
by (auto simp: S_def S5_def dest!: Envbusy [temp_use])
-lemma S5ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) & $(S5 rmhist p) \<longrightarrow> unchanged (c p)"
+lemma S5ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S5 rmhist p) \<longrightarrow> unchanged (c p)"
by (auto simp: S_def S5_def dest!: MClkbusy [temp_use])
-lemma S5RPC: "\<turnstile> RPCNext crCh rmCh rst p & $(S5 rmhist p)
- \<longrightarrow> RPCReply crCh rmCh rst p | RPCFail crCh rmCh rst p"
+lemma S5RPC: "\<turnstile> RPCNext crCh rmCh rst p \<and> $(S5 rmhist p)
+ \<longrightarrow> RPCReply crCh rmCh rst p \<or> RPCFail crCh rmCh rst p"
by (auto simp: RPCNext_def RPCReject_def RPCFwd_def S_def S5_def)
-lemma S5Reply: "\<turnstile> RPCReply crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
+lemma S5Reply: "\<turnstile> RPCReply crCh rmCh rst p \<and> $(S5 rmhist p) \<and> unchanged (e p, c p, m p,rmhist!p)
\<longrightarrow> (S6 rmhist p)$"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
@{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, @{thm MVOKBA_def},
@{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
@{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
-lemma S5Fail: "\<turnstile> RPCFail crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
+lemma S5Fail: "\<turnstile> RPCFail crCh rmCh rst p \<and> $(S5 rmhist p) \<and> unchanged (e p, c p, m p,rmhist!p)
\<longrightarrow> (S6 rmhist p)$"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
@{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def},
@{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def},
@{thm S_def}, @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
-lemma S5MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) & $(S5 rmhist p) \<longrightarrow> unchanged (m p)"
+lemma S5MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S5 rmhist p) \<longrightarrow> unchanged (m p)"
by (auto simp: S_def S5_def dest!: Memoryidle [temp_use])
-lemma S5Hist: "\<turnstile> [HNext rmhist p]_(c p, r p, m p, rmhist!p) & $(S5 rmhist p)
+lemma S5Hist: "\<turnstile> [HNext rmhist p]_(c p, r p, m p, rmhist!p) \<and> $(S5 rmhist p)
\<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
@@ -515,36 +515,36 @@
(* ------------------------------ State S6 ---------------------------------------- *)
-lemma S6EnvUnch: "\<turnstile> [ENext p]_(e p) & $(S6 rmhist p) \<longrightarrow> unchanged (e p)"
+lemma S6EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S6 rmhist p) \<longrightarrow> unchanged (e p)"
by (auto simp: S_def S6_def dest!: Envbusy [temp_use])
-lemma S6Clerk: "\<turnstile> MClkNext memCh crCh cst p & $(S6 rmhist p)
- \<longrightarrow> MClkRetry memCh crCh cst p | MClkReply memCh crCh cst p"
+lemma S6Clerk: "\<turnstile> MClkNext memCh crCh cst p \<and> $(S6 rmhist p)
+ \<longrightarrow> MClkRetry memCh crCh cst p \<or> MClkReply memCh crCh cst p"
by (auto simp: MClkNext_def MClkFwd_def S_def S6_def)
-lemma S6Retry: "\<turnstile> MClkRetry memCh crCh cst p & HNext rmhist p & $S6 rmhist p
- & unchanged (e p,r p,m p)
- \<longrightarrow> (S3 rmhist p)$ & unchanged (rmhist!p)"
+lemma S6Retry: "\<turnstile> MClkRetry memCh crCh cst p \<and> HNext rmhist p \<and> $S6 rmhist p
+ \<and> unchanged (e p,r p,m p)
+ \<longrightarrow> (S3 rmhist p)$ \<and> unchanged (rmhist!p)"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def},
@{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm Call_def}, @{thm Return_def},
@{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
@{thm S_def}, @{thm S6_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1 *})
-lemma S6Reply: "\<turnstile> MClkReply memCh crCh cst p & HNext rmhist p & $S6 rmhist p
- & unchanged (e p,r p,m p)
+lemma S6Reply: "\<turnstile> MClkReply memCh crCh cst p \<and> HNext rmhist p \<and> $S6 rmhist p
+ \<and> unchanged (e p,r p,m p)
\<longrightarrow> (S1 rmhist p)$"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def},
@{thm MemReturn_def}, @{thm RPCFail_def}, @{thm Return_def}, @{thm MClkReply_def},
@{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
@{thm S_def}, @{thm S6_def}, @{thm S1_def}, @{thm Calling_def}]) [] [] 1 *})
-lemma S6RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) & $S6 rmhist p \<longrightarrow> unchanged (r p)"
+lemma S6RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $S6 rmhist p \<longrightarrow> unchanged (r p)"
by (auto simp: S_def S6_def dest!: RPCidle [temp_use])
-lemma S6MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) & $(S6 rmhist p) \<longrightarrow> unchanged (m p)"
+lemma S6MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S6 rmhist p) \<longrightarrow> unchanged (m p)"
by (auto simp: S_def S6_def dest!: Memoryidle [temp_use])
-lemma S6Hist: "\<turnstile> HNext rmhist p & $S6 rmhist p & (c p)$ = $(c p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
+lemma S6Hist: "\<turnstile> HNext rmhist p \<and> $S6 rmhist p \<and> (c p)$ = $(c p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
by (auto simp: HNext_def MClkReply_def Return_def c_def rtrner_def S_def S6_def Calling_def)
@@ -554,7 +554,7 @@
(* ========== Step 1.1 ================================================= *)
(* The implementation's initial condition implies the state predicate S1 *)
-lemma Step1_1: "\<turnstile> ImpInit p & HInit rmhist p \<longrightarrow> S1 rmhist p"
+lemma Step1_1: "\<turnstile> ImpInit p \<and> HInit rmhist p \<longrightarrow> S1 rmhist p"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] simp: MVNROKBA_def
MClkInit_def RPCInit_def PInit_def HInit_def ImpInit_def S_def S1_def)
@@ -562,9 +562,9 @@
(* ========== Step 1.2 ================================================== *)
(* Figure 16 is a predicate-action diagram for the implementation. *)
-lemma Step1_2_1: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
- & \<not>unchanged (e p, c p, r p, m p, rmhist!p) & $S1 rmhist p
- \<longrightarrow> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"
+lemma Step1_2_1: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p
+ \<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) \<and> $S1 rmhist p
+ \<longrightarrow> (S2 rmhist p)$ \<and> ENext p \<and> unchanged (c p, r p, m p)"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
(map (temp_elim @{context})
[@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1 *})
@@ -572,10 +572,10 @@
apply (auto elim!: squareE [temp_use] intro!: S1Env [temp_use])
done
-lemma Step1_2_2: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
- & \<not>unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p
- \<longrightarrow> (S3 rmhist p)$ & MClkFwd memCh crCh cst p
- & unchanged (e p, r p, m p, rmhist!p)"
+lemma Step1_2_2: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p
+ \<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) \<and> $S2 rmhist p
+ \<longrightarrow> (S3 rmhist p)$ \<and> MClkFwd memCh crCh cst p
+ \<and> unchanged (e p, r p, m p, rmhist!p)"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
(map (temp_elim @{context})
[@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1 *})
@@ -583,10 +583,10 @@
apply (auto elim!: squareE [temp_use] intro!: S2Clerk [temp_use] S2Forward [temp_use])
done
-lemma Step1_2_3: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
- & \<not>unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p
- \<longrightarrow> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p))
- | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
+lemma Step1_2_3: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p
+ \<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) \<and> $S3 rmhist p
+ \<longrightarrow> ((S4 rmhist p)$ \<and> RPCFwd crCh rmCh rst p \<and> unchanged (e p, c p, m p, rmhist!p))
+ \<or> ((S6 rmhist p)$ \<and> RPCFail crCh rmCh rst p \<and> unchanged (e p, c p, m p))"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
(map (temp_elim @{context}) [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1 *})
apply (tactic {* action_simp_tac @{context} []
@@ -595,12 +595,12 @@
apply (auto dest!: S3Hist [temp_use])
done
-lemma Step1_2_4: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
- & \<not>unchanged (e p, c p, r p, m p, rmhist!p)
- & $S4 rmhist p & (\<forall>l. $(MemInv mm l))
- \<longrightarrow> ((S4 rmhist p)$ & Read rmCh mm ires p & unchanged (e p, c p, r p, rmhist!p))
- | ((S4 rmhist p)$ & (\<exists>l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p))
- | ((S5 rmhist p)$ & MemReturn rmCh ires p & unchanged (e p, c p, r p))"
+lemma Step1_2_4: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p
+ \<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p)
+ \<and> $S4 rmhist p \<and> (\<forall>l. $(MemInv mm l))
+ \<longrightarrow> ((S4 rmhist p)$ \<and> Read rmCh mm ires p \<and> unchanged (e p, c p, r p, rmhist!p))
+ \<or> ((S4 rmhist p)$ \<and> (\<exists>l. Write rmCh mm ires p l) \<and> unchanged (e p, c p, r p, rmhist!p))
+ \<or> ((S5 rmhist p)$ \<and> MemReturn rmCh ires p \<and> unchanged (e p, c p, r p))"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
(map (temp_elim @{context}) [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm RNext_def}]) []
@@ -609,10 +609,10 @@
apply (auto dest!: S4Hist [temp_use])
done
-lemma Step1_2_5: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
- & \<not>unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p
- \<longrightarrow> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p))
- | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
+lemma Step1_2_5: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p
+ \<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) \<and> $S5 rmhist p
+ \<longrightarrow> ((S6 rmhist p)$ \<and> RPCReply crCh rmCh rst p \<and> unchanged (e p, c p, m p))
+ \<or> ((S6 rmhist p)$ \<and> RPCFail crCh rmCh rst p \<and> unchanged (e p, c p, m p))"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
(map (temp_elim @{context}) [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1 *})
apply (tactic {* action_simp_tac @{context} [] [@{thm squareE}, temp_elim @{context} @{thm S5RPC}] 1 *})
@@ -620,10 +620,10 @@
apply (auto elim!: squareE [temp_use] dest!: S5Reply [temp_use] S5Fail [temp_use])
done
-lemma Step1_2_6: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
- & \<not>unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p
- \<longrightarrow> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p))
- | ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))"
+lemma Step1_2_6: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p
+ \<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) \<and> $S6 rmhist p
+ \<longrightarrow> ((S1 rmhist p)$ \<and> MClkReply memCh crCh cst p \<and> unchanged (e p, r p, m p))
+ \<or> ((S3 rmhist p)$ \<and> MClkRetry memCh crCh cst p \<and> unchanged (e p,r p,m p,rmhist!p))"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
(map (temp_elim @{context}) [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1 *})
apply (tactic {* action_simp_tac @{context} []
@@ -648,20 +648,20 @@
section "Step simulation (Step 1.4)"
-lemma Step1_4_1: "\<turnstile> ENext p & $S1 rmhist p & (S2 rmhist p)$ & unchanged (c p, r p, m p)
+lemma Step1_4_1: "\<turnstile> ENext p \<and> $S1 rmhist p \<and> (S2 rmhist p)$ \<and> unchanged (c p, r p, m p)
\<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] simp: c_def r_def m_def resbar_def)
-lemma Step1_4_2: "\<turnstile> MClkFwd memCh crCh cst p & $S2 rmhist p & (S3 rmhist p)$
- & unchanged (e p, r p, m p, rmhist!p)
+lemma Step1_4_2: "\<turnstile> MClkFwd memCh crCh cst p \<and> $S2 rmhist p \<and> (S3 rmhist p)$
+ \<and> unchanged (e p, r p, m p, rmhist!p)
\<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
by (tactic {* action_simp_tac
(@{context} addsimps [@{thm MClkFwd_def}, @{thm e_def}, @{thm r_def}, @{thm m_def},
@{thm resbar_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}]) [] [] 1 *})
-lemma Step1_4_3a: "\<turnstile> RPCFwd crCh rmCh rst p & $S3 rmhist p & (S4 rmhist p)$
- & unchanged (e p, c p, m p, rmhist!p)
+lemma Step1_4_3a: "\<turnstile> RPCFwd crCh rmCh rst p \<and> $S3 rmhist p \<and> (S4 rmhist p)$
+ \<and> unchanged (e p, c p, m p, rmhist!p)
\<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
apply clarsimp
apply (drule S3_excl [temp_use] S4_excl [temp_use])+
@@ -669,8 +669,8 @@
@{thm c_def}, @{thm m_def}, @{thm resbar_def}, @{thm S_def}, @{thm S3_def}]) [] [] 1 *})
done
-lemma Step1_4_3b: "\<turnstile> RPCFail crCh rmCh rst p & $S3 rmhist p & (S6 rmhist p)$
- & unchanged (e p, c p, m p)
+lemma Step1_4_3b: "\<turnstile> RPCFail crCh rmCh rst p \<and> $S3 rmhist p \<and> (S6 rmhist p)$
+ \<and> unchanged (e p, c p, m p)
\<longrightarrow> MemFail memCh (resbar rmhist) p"
apply clarsimp
apply (drule S6_excl [temp_use])
@@ -679,8 +679,8 @@
apply (auto simp: Return_def)
done
-lemma Step1_4_4a1: "\<turnstile> $S4 rmhist p & (S4 rmhist p)$ & ReadInner rmCh mm ires p l
- & unchanged (e p, c p, r p, rmhist!p) & $MemInv mm l
+lemma Step1_4_4a1: "\<turnstile> $S4 rmhist p \<and> (S4 rmhist p)$ \<and> ReadInner rmCh mm ires p l
+ \<and> unchanged (e p, c p, r p, rmhist!p) \<and> $MemInv mm l
\<longrightarrow> ReadInner memCh mm (resbar rmhist) p l"
apply clarsimp
apply (drule S4_excl [temp_use])+
@@ -693,13 +693,13 @@
[] [@{thm impE}, @{thm MemValNotAResultE}]) *})
done
-lemma Step1_4_4a: "\<turnstile> Read rmCh mm ires p & $S4 rmhist p & (S4 rmhist p)$
- & unchanged (e p, c p, r p, rmhist!p) & (\<forall>l. $(MemInv mm l))
+lemma Step1_4_4a: "\<turnstile> Read rmCh mm ires p \<and> $S4 rmhist p \<and> (S4 rmhist p)$
+ \<and> unchanged (e p, c p, r p, rmhist!p) \<and> (\<forall>l. $(MemInv mm l))
\<longrightarrow> Read memCh mm (resbar rmhist) p"
by (force simp: Read_def elim!: Step1_4_4a1 [temp_use])
-lemma Step1_4_4b1: "\<turnstile> $S4 rmhist p & (S4 rmhist p)$ & WriteInner rmCh mm ires p l v
- & unchanged (e p, c p, r p, rmhist!p)
+lemma Step1_4_4b1: "\<turnstile> $S4 rmhist p \<and> (S4 rmhist p)$ \<and> WriteInner rmCh mm ires p l v
+ \<and> unchanged (e p, c p, r p, rmhist!p)
\<longrightarrow> WriteInner memCh mm (resbar rmhist) p l v"
apply clarsimp
apply (drule S4_excl [temp_use])+
@@ -712,13 +712,13 @@
@{thm S4_def}, @{thm WrRequest_def}]) [] []) *})
done
-lemma Step1_4_4b: "\<turnstile> Write rmCh mm ires p l & $S4 rmhist p & (S4 rmhist p)$
- & unchanged (e p, c p, r p, rmhist!p)
+lemma Step1_4_4b: "\<turnstile> Write rmCh mm ires p l \<and> $S4 rmhist p \<and> (S4 rmhist p)$
+ \<and> unchanged (e p, c p, r p, rmhist!p)
\<longrightarrow> Write memCh mm (resbar rmhist) p l"
by (force simp: Write_def elim!: Step1_4_4b1 [temp_use])
-lemma Step1_4_4c: "\<turnstile> MemReturn rmCh ires p & $S4 rmhist p & (S5 rmhist p)$
- & unchanged (e p, c p, r p)
+lemma Step1_4_4c: "\<turnstile> MemReturn rmCh ires p \<and> $S4 rmhist p \<and> (S5 rmhist p)$
+ \<and> unchanged (e p, c p, r p)
\<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm e_def},
@{thm c_def}, @{thm r_def}, @{thm resbar_def}]) [] [] 1 *})
@@ -727,8 +727,8 @@
apply (auto elim!: squareE [temp_use] simp: MemReturn_def Return_def)
done
-lemma Step1_4_5a: "\<turnstile> RPCReply crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$
- & unchanged (e p, c p, m p)
+lemma Step1_4_5a: "\<turnstile> RPCReply crCh rmCh rst p \<and> $S5 rmhist p \<and> (S6 rmhist p)$
+ \<and> unchanged (e p, c p, m p)
\<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
apply clarsimp
apply (drule S5_excl [temp_use] S6_excl [temp_use])+
@@ -736,8 +736,8 @@
apply (auto simp: RPCReply_def Return_def S5_def S_def dest!: MVOKBAnotRF [temp_use])
done
-lemma Step1_4_5b: "\<turnstile> RPCFail crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$
- & unchanged (e p, c p, m p)
+lemma Step1_4_5b: "\<turnstile> RPCFail crCh rmCh rst p \<and> $S5 rmhist p \<and> (S6 rmhist p)$
+ \<and> unchanged (e p, c p, m p)
\<longrightarrow> MemFail memCh (resbar rmhist) p"
apply clarsimp
apply (drule S6_excl [temp_use])
@@ -745,8 +745,8 @@
apply (auto simp: S5_def S_def)
done
-lemma Step1_4_6a: "\<turnstile> MClkReply memCh crCh cst p & $S6 rmhist p & (S1 rmhist p)$
- & unchanged (e p, r p, m p)
+lemma Step1_4_6a: "\<turnstile> MClkReply memCh crCh cst p \<and> $S6 rmhist p \<and> (S1 rmhist p)$
+ \<and> unchanged (e p, r p, m p)
\<longrightarrow> MemReturn memCh (resbar rmhist) p"
apply clarsimp
apply (drule S6_excl [temp_use])+
@@ -758,8 +758,8 @@
[@{thm MClkReplyVal_def}, @{thm S6_def}, @{thm S_def}]) [] [@{thm MVOKBARFnotNR}]) *})
done
-lemma Step1_4_6b: "\<turnstile> MClkRetry memCh crCh cst p & $S6 rmhist p & (S3 rmhist p)$
- & unchanged (e p, r p, m p, rmhist!p)
+lemma Step1_4_6b: "\<turnstile> MClkRetry memCh crCh cst p \<and> $S6 rmhist p \<and> (S3 rmhist p)$
+ \<and> unchanged (e p, r p, m p, rmhist!p)
\<longrightarrow> MemFail memCh (resbar rmhist) p"
apply clarsimp
apply (drule S3_excl [temp_use])+
@@ -825,7 +825,7 @@
(* turn into (unsafe, looping!) introduction rule *)
lemmas unchanged_safeI = impI [THEN unchanged_safe [action_use]]
-lemma S1safe: "\<turnstile> $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S1safe: "\<turnstile> $S1 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
\<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
apply clarsimp
apply (rule unchanged_safeI)
@@ -833,7 +833,7 @@
apply (auto dest!: Step1_2_1 [temp_use] Step1_4_1 [temp_use])
done
-lemma S2safe: "\<turnstile> $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S2safe: "\<turnstile> $S2 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
\<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
apply clarsimp
apply (rule unchanged_safeI)
@@ -841,7 +841,7 @@
apply (auto dest!: Step1_2_2 [temp_use] Step1_4_2 [temp_use])
done
-lemma S3safe: "\<turnstile> $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S3safe: "\<turnstile> $S3 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
\<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
apply clarsimp
apply (rule unchanged_safeI)
@@ -849,8 +849,8 @@
apply (auto simp: square_def UNext_def dest!: Step1_4_3a [temp_use] Step1_4_3b [temp_use])
done
-lemma S4safe: "\<turnstile> $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- & (\<forall>l. $(MemInv mm l))
+lemma S4safe: "\<turnstile> $S4 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+ \<and> (\<forall>l. $(MemInv mm l))
\<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
apply clarsimp
apply (rule unchanged_safeI)
@@ -859,7 +859,7 @@
dest!: Step1_4_4a [temp_use] Step1_4_4b [temp_use] Step1_4_4c [temp_use])
done
-lemma S5safe: "\<turnstile> $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S5safe: "\<turnstile> $S5 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
\<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
apply clarsimp
apply (rule unchanged_safeI)
@@ -867,7 +867,7 @@
apply (auto simp: square_def UNext_def dest!: Step1_4_5a [temp_use] Step1_4_5b [temp_use])
done
-lemma S6safe: "\<turnstile> $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S6safe: "\<turnstile> $S6 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
\<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
apply clarsimp
apply (rule unchanged_safeI)
@@ -889,8 +889,8 @@
(* ------------------------------ State S1 ------------------------------ *)
-lemma S1_successors: "\<turnstile> $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- \<longrightarrow> (S1 rmhist p)$ | (S2 rmhist p)$"
+lemma S1_successors: "\<turnstile> $S1 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+ \<longrightarrow> (S1 rmhist p)$ \<or> (S2 rmhist p)$"
apply split_idle
apply (auto dest!: Step1_2_1 [temp_use])
done
@@ -923,18 +923,18 @@
(* ------------------------------ State S2 ------------------------------ *)
-lemma S2_successors: "\<turnstile> $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- \<longrightarrow> (S2 rmhist p)$ | (S3 rmhist p)$"
+lemma S2_successors: "\<turnstile> $S2 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+ \<longrightarrow> (S2 rmhist p)$ \<or> (S3 rmhist p)$"
apply split_idle
apply (auto dest!: Step1_2_2 [temp_use])
done
-lemma S2MClkFwd_successors: "\<turnstile> ($S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
- & <MClkFwd memCh crCh cst p>_(c p)
+lemma S2MClkFwd_successors: "\<turnstile> ($S2 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+ \<and> <MClkFwd memCh crCh cst p>_(c p)
\<longrightarrow> (S3 rmhist p)$"
by (auto simp: angle_def dest!: Step1_2_2 [temp_use])
-lemma S2MClkFwd_enabled: "\<turnstile> $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S2MClkFwd_enabled: "\<turnstile> $S2 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
\<longrightarrow> $Enabled (<MClkFwd memCh crCh cst p>_(c p))"
apply (auto simp: c_def intro!: MClkFwd_ch_enabled [temp_use] MClkFwd_enabled [temp_use])
apply (cut_tac MI_base)
@@ -942,26 +942,26 @@
apply (simp_all add: S_def S2_def)
done
-lemma S2_live: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
- & WF(MClkFwd memCh crCh cst p)_(c p)
+lemma S2_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+ \<and> WF(MClkFwd memCh crCh cst p)_(c p)
\<longrightarrow> (S2 rmhist p \<leadsto> S3 rmhist p)"
by (rule WF1 S2_successors S2MClkFwd_successors S2MClkFwd_enabled)+
(* ------------------------------ State S3 ------------------------------ *)
-lemma S3_successors: "\<turnstile> $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- \<longrightarrow> (S3 rmhist p)$ | (S4 rmhist p | S6 rmhist p)$"
+lemma S3_successors: "\<turnstile> $S3 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+ \<longrightarrow> (S3 rmhist p)$ \<or> (S4 rmhist p \<or> S6 rmhist p)$"
apply split_idle
apply (auto dest!: Step1_2_3 [temp_use])
done
-lemma S3RPC_successors: "\<turnstile> ($S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
- & <RPCNext crCh rmCh rst p>_(r p)
- \<longrightarrow> (S4 rmhist p | S6 rmhist p)$"
+lemma S3RPC_successors: "\<turnstile> ($S3 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+ \<and> <RPCNext crCh rmCh rst p>_(r p)
+ \<longrightarrow> (S4 rmhist p \<or> S6 rmhist p)$"
apply (auto simp: angle_def dest!: Step1_2_3 [temp_use])
done
-lemma S3RPC_enabled: "\<turnstile> $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S3RPC_enabled: "\<turnstile> $S3 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
\<longrightarrow> $Enabled (<RPCNext crCh rmCh rst p>_(r p))"
apply (auto simp: r_def intro!: RPCFail_Next_enabled [temp_use] RPCFail_enabled [temp_use])
apply (cut_tac MI_base)
@@ -969,39 +969,39 @@
apply (simp_all add: S_def S3_def)
done
-lemma S3_live: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
- & WF(RPCNext crCh rmCh rst p)_(r p)
- \<longrightarrow> (S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p)"
+lemma S3_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+ \<and> WF(RPCNext crCh rmCh rst p)_(r p)
+ \<longrightarrow> (S3 rmhist p \<leadsto> S4 rmhist p \<or> S6 rmhist p)"
by (rule WF1 S3_successors S3RPC_successors S3RPC_enabled)+
(* ------------- State S4 -------------------------------------------------- *)
-lemma S4_successors: "\<turnstile> $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- & (\<forall>l. $MemInv mm l)
- \<longrightarrow> (S4 rmhist p)$ | (S5 rmhist p)$"
+lemma S4_successors: "\<turnstile> $S4 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+ \<and> (\<forall>l. $MemInv mm l)
+ \<longrightarrow> (S4 rmhist p)$ \<or> (S5 rmhist p)$"
apply split_idle
apply (auto dest!: Step1_2_4 [temp_use])
done
(* --------- State S4a: S4 /\ (ires p = NotAResult) ------------------------ *)
-lemma S4a_successors: "\<turnstile> $(S4 rmhist p & ires!p = #NotAResult)
- & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (\<forall>l. $MemInv mm l)
- \<longrightarrow> (S4 rmhist p & ires!p = #NotAResult)$
- | ((S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p)$"
+lemma S4a_successors: "\<turnstile> $(S4 rmhist p \<and> ires!p = #NotAResult)
+ \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p,rmhist!p) \<and> (\<forall>l. $MemInv mm l)
+ \<longrightarrow> (S4 rmhist p \<and> ires!p = #NotAResult)$
+ \<or> ((S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p)$"
apply split_idle
apply (auto dest!: Step1_2_4 [temp_use])
done
-lemma S4aRNext_successors: "\<turnstile> ($(S4 rmhist p & ires!p = #NotAResult)
- & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (\<forall>l. $MemInv mm l))
- & <RNext rmCh mm ires p>_(m p)
- \<longrightarrow> ((S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p)$"
+lemma S4aRNext_successors: "\<turnstile> ($(S4 rmhist p \<and> ires!p = #NotAResult)
+ \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p,rmhist!p) \<and> (\<forall>l. $MemInv mm l))
+ \<and> <RNext rmCh mm ires p>_(m p)
+ \<longrightarrow> ((S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p)$"
by (auto simp: angle_def
dest!: Step1_2_4 [temp_use] ReadResult [temp_use] WriteResult [temp_use])
-lemma S4aRNext_enabled: "\<turnstile> $(S4 rmhist p & ires!p = #NotAResult)
- & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (\<forall>l. $MemInv mm l)
+lemma S4aRNext_enabled: "\<turnstile> $(S4 rmhist p \<and> ires!p = #NotAResult)
+ \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> (\<forall>l. $MemInv mm l)
\<longrightarrow> $Enabled (<RNext rmCh mm ires p>_(m p))"
apply (auto simp: m_def intro!: RNext_enabled [temp_use])
apply (cut_tac MI_base)
@@ -1009,30 +1009,30 @@
apply (simp add: S_def S4_def)
done
-lemma S4a_live: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- & (\<forall>l. $MemInv mm l)) & WF(RNext rmCh mm ires p)_(m p)
- \<longrightarrow> (S4 rmhist p & ires!p = #NotAResult
- \<leadsto> (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p)"
+lemma S4a_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+ \<and> (\<forall>l. $MemInv mm l)) \<and> WF(RNext rmCh mm ires p)_(m p)
+ \<longrightarrow> (S4 rmhist p \<and> ires!p = #NotAResult
+ \<leadsto> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p)"
by (rule WF1 S4a_successors S4aRNext_successors S4aRNext_enabled)+
(* ---------- State S4b: S4 /\ (ires p # NotAResult) --------------------------- *)
-lemma S4b_successors: "\<turnstile> $(S4 rmhist p & ires!p \<noteq> #NotAResult)
- & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (\<forall>l. $MemInv mm l)
- \<longrightarrow> (S4 rmhist p & ires!p \<noteq> #NotAResult)$ | (S5 rmhist p)$"
+lemma S4b_successors: "\<turnstile> $(S4 rmhist p \<and> ires!p \<noteq> #NotAResult)
+ \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> (\<forall>l. $MemInv mm l)
+ \<longrightarrow> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult)$ \<or> (S5 rmhist p)$"
apply (split_idle simp: m_def)
apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use])
done
-lemma S4bReturn_successors: "\<turnstile> ($(S4 rmhist p & ires!p \<noteq> #NotAResult)
- & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- & (\<forall>l. $MemInv mm l)) & <MemReturn rmCh ires p>_(m p)
+lemma S4bReturn_successors: "\<turnstile> ($(S4 rmhist p \<and> ires!p \<noteq> #NotAResult)
+ \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+ \<and> (\<forall>l. $MemInv mm l)) \<and> <MemReturn rmCh ires p>_(m p)
\<longrightarrow> (S5 rmhist p)$"
by (force simp: angle_def dest!: Step1_2_4 [temp_use] dest: ReturnNotReadWrite [temp_use])
-lemma S4bReturn_enabled: "\<turnstile> $(S4 rmhist p & ires!p \<noteq> #NotAResult)
- & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- & (\<forall>l. $MemInv mm l)
+lemma S4bReturn_enabled: "\<turnstile> $(S4 rmhist p \<and> ires!p \<noteq> #NotAResult)
+ \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+ \<and> (\<forall>l. $MemInv mm l)
\<longrightarrow> $Enabled (<MemReturn rmCh ires p>_(m p))"
apply (auto simp: m_def intro!: MemReturn_enabled [temp_use])
apply (cut_tac MI_base)
@@ -1040,25 +1040,25 @@
apply (simp add: S_def S4_def)
done
-lemma S4b_live: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (\<forall>l. $MemInv mm l))
- & WF(MemReturn rmCh ires p)_(m p)
- \<longrightarrow> (S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p)"
+lemma S4b_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> (\<forall>l. $MemInv mm l))
+ \<and> WF(MemReturn rmCh ires p)_(m p)
+ \<longrightarrow> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p)"
by (rule WF1 S4b_successors S4bReturn_successors S4bReturn_enabled)+
(* ------------------------------ State S5 ------------------------------ *)
-lemma S5_successors: "\<turnstile> $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- \<longrightarrow> (S5 rmhist p)$ | (S6 rmhist p)$"
+lemma S5_successors: "\<turnstile> $S5 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+ \<longrightarrow> (S5 rmhist p)$ \<or> (S6 rmhist p)$"
apply split_idle
apply (auto dest!: Step1_2_5 [temp_use])
done
-lemma S5RPC_successors: "\<turnstile> ($S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
- & <RPCNext crCh rmCh rst p>_(r p)
+lemma S5RPC_successors: "\<turnstile> ($S5 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+ \<and> <RPCNext crCh rmCh rst p>_(r p)
\<longrightarrow> (S6 rmhist p)$"
by (auto simp: angle_def dest!: Step1_2_5 [temp_use])
-lemma S5RPC_enabled: "\<turnstile> $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S5RPC_enabled: "\<turnstile> $S5 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
\<longrightarrow> $Enabled (<RPCNext crCh rmCh rst p>_(r p))"
apply (auto simp: r_def intro!: RPCFail_Next_enabled [temp_use] RPCFail_enabled [temp_use])
apply (cut_tac MI_base)
@@ -1066,27 +1066,27 @@
apply (simp_all add: S_def S5_def)
done
-lemma S5_live: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
- & WF(RPCNext crCh rmCh rst p)_(r p)
+lemma S5_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+ \<and> WF(RPCNext crCh rmCh rst p)_(r p)
\<longrightarrow> (S5 rmhist p \<leadsto> S6 rmhist p)"
by (rule WF1 S5_successors S5RPC_successors S5RPC_enabled)+
(* ------------------------------ State S6 ------------------------------ *)
-lemma S6_successors: "\<turnstile> $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- \<longrightarrow> (S1 rmhist p)$ | (S3 rmhist p)$ | (S6 rmhist p)$"
+lemma S6_successors: "\<turnstile> $S6 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+ \<longrightarrow> (S1 rmhist p)$ \<or> (S3 rmhist p)$ \<or> (S6 rmhist p)$"
apply split_idle
apply (auto dest!: Step1_2_6 [temp_use])
done
lemma S6MClkReply_successors:
- "\<turnstile> ($S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
- & <MClkReply memCh crCh cst p>_(c p)
+ "\<turnstile> ($S6 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+ \<and> <MClkReply memCh crCh cst p>_(c p)
\<longrightarrow> (S1 rmhist p)$"
by (auto simp: angle_def dest!: Step1_2_6 [temp_use] MClkReplyNotRetry [temp_use])
lemma MClkReplyS6:
- "\<turnstile> $ImpInv rmhist p & <MClkReply memCh crCh cst p>_(c p) \<longrightarrow> $S6 rmhist p"
+ "\<turnstile> $ImpInv rmhist p \<and> <MClkReply memCh crCh cst p>_(c p) \<longrightarrow> $S6 rmhist p"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def},
@{thm MClkReply_def}, @{thm Return_def}, @{thm ImpInv_def}, @{thm S_def},
@{thm S1_def}, @{thm S2_def}, @{thm S3_def}, @{thm S4_def}, @{thm S5_def}]) [] [] 1 *})
@@ -1099,8 +1099,8 @@
addsimps [@{thm S_def}, @{thm S6_def}]) [] []) *})
done
-lemma S6_live: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & $(ImpInv rmhist p))
- & SF(MClkReply memCh crCh cst p)_(c p) & \<box>\<diamond>(S6 rmhist p)
+lemma S6_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> $(ImpInv rmhist p))
+ \<and> SF(MClkReply memCh crCh cst p)_(c p) \<and> \<box>\<diamond>(S6 rmhist p)
\<longrightarrow> \<box>\<diamond>(S1 rmhist p)"
apply clarsimp
apply (subgoal_tac "sigma \<Turnstile> \<box>\<diamond> (<MClkReply memCh crCh cst p>_ (c p))")
@@ -1116,25 +1116,25 @@
(* --------------- aggregate leadsto properties----------------------------- *)
lemma S5S6LeadstoS6: "sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p
- \<Longrightarrow> sigma \<Turnstile> (S5 rmhist p | S6 rmhist p) \<leadsto> S6 rmhist p"
+ \<Longrightarrow> sigma \<Turnstile> (S5 rmhist p \<or> S6 rmhist p) \<leadsto> S6 rmhist p"
by (auto intro!: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
-lemma S4bS5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
+lemma S4bS5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk>
- \<Longrightarrow> sigma \<Turnstile> (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p | S6 rmhist p
+ \<Longrightarrow> sigma \<Turnstile> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p \<or> S6 rmhist p
\<leadsto> S6 rmhist p"
by (auto intro!: LatticeDisjunctionIntro [temp_use]
S5S6LeadstoS6 [temp_use] intro: LatticeTransitivity [temp_use])
-lemma S4S5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S4 rmhist p & ires!p = #NotAResult
- \<leadsto> (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p;
- sigma \<Turnstile> S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
+lemma S4S5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S4 rmhist p \<and> ires!p = #NotAResult
+ \<leadsto> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p;
+ sigma \<Turnstile> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk>
- \<Longrightarrow> sigma \<Turnstile> S4 rmhist p | S5 rmhist p | S6 rmhist p \<leadsto> S6 rmhist p"
- apply (subgoal_tac "sigma \<Turnstile> (S4 rmhist p & ires!p = #NotAResult) |
- (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p | S6 rmhist p \<leadsto> S6 rmhist p")
- apply (erule_tac G = "PRED ((S4 rmhist p & ires!p = #NotAResult) |
- (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p | S6 rmhist p)" in
+ \<Longrightarrow> sigma \<Turnstile> S4 rmhist p \<or> S5 rmhist p \<or> S6 rmhist p \<leadsto> S6 rmhist p"
+ apply (subgoal_tac "sigma \<Turnstile> (S4 rmhist p \<and> ires!p = #NotAResult) \<or>
+ (S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p \<or> S6 rmhist p \<leadsto> S6 rmhist p")
+ apply (erule_tac G = "PRED ((S4 rmhist p \<and> ires!p = #NotAResult) \<or>
+ (S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p \<or> S6 rmhist p)" in
LatticeTransitivity [temp_use])
apply (force simp: Init_defs intro!: ImplLeadsto_gen [temp_use] necT [temp_use])
apply (rule LatticeDisjunctionIntro [temp_use])
@@ -1144,12 +1144,12 @@
apply (auto intro!: S4bS5S6LeadstoS6 [temp_use])
done
-lemma S3S4S5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p;
- sigma \<Turnstile> S4 rmhist p & ires!p = #NotAResult
- \<leadsto> (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p;
- sigma \<Turnstile> S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
+lemma S3S4S5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S3 rmhist p \<leadsto> S4 rmhist p \<or> S6 rmhist p;
+ sigma \<Turnstile> S4 rmhist p \<and> ires!p = #NotAResult
+ \<leadsto> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p;
+ sigma \<Turnstile> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk>
- \<Longrightarrow> sigma \<Turnstile> S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p \<leadsto> S6 rmhist p"
+ \<Longrightarrow> sigma \<Turnstile> S3 rmhist p \<or> S4 rmhist p \<or> S5 rmhist p \<or> S6 rmhist p \<leadsto> S6 rmhist p"
apply (rule LatticeDisjunctionIntro [temp_use])
apply (erule LatticeTriangle2 [temp_use])
apply (rule S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]])
@@ -1158,12 +1158,12 @@
done
lemma S2S3S4S5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S2 rmhist p \<leadsto> S3 rmhist p;
- sigma \<Turnstile> S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p;
- sigma \<Turnstile> S4 rmhist p & ires!p = #NotAResult
- \<leadsto> S4 rmhist p & ires!p \<noteq> #NotAResult | S5 rmhist p;
- sigma \<Turnstile> S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
+ sigma \<Turnstile> S3 rmhist p \<leadsto> S4 rmhist p \<or> S6 rmhist p;
+ sigma \<Turnstile> S4 rmhist p \<and> ires!p = #NotAResult
+ \<leadsto> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<or> S5 rmhist p;
+ sigma \<Turnstile> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk>
- \<Longrightarrow> sigma \<Turnstile> S2 rmhist p | S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p
+ \<Longrightarrow> sigma \<Turnstile> S2 rmhist p \<or> S3 rmhist p \<or> S4 rmhist p \<or> S5 rmhist p \<or> S6 rmhist p
\<leadsto> S6 rmhist p"
apply (rule LatticeDisjunctionIntro [temp_use])
apply (rule LatticeTransitivity [temp_use])
@@ -1175,10 +1175,10 @@
lemma NotS1LeadstoS6: "\<lbrakk> sigma \<Turnstile> \<box>ImpInv rmhist p;
sigma \<Turnstile> S2 rmhist p \<leadsto> S3 rmhist p;
- sigma \<Turnstile> S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p;
- sigma \<Turnstile> S4 rmhist p & ires!p = #NotAResult
- \<leadsto> S4 rmhist p & ires!p \<noteq> #NotAResult | S5 rmhist p;
- sigma \<Turnstile> S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
+ sigma \<Turnstile> S3 rmhist p \<leadsto> S4 rmhist p \<or> S6 rmhist p;
+ sigma \<Turnstile> S4 rmhist p \<and> ires!p = #NotAResult
+ \<leadsto> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<or> S5 rmhist p;
+ sigma \<Turnstile> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk>
\<Longrightarrow> sigma \<Turnstile> \<not>S1 rmhist p \<leadsto> S6 rmhist p"
apply (rule S2S3S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]])
@@ -1207,8 +1207,8 @@
lemma Step1_5_1a: "\<turnstile> IPImp p \<longrightarrow> (\<forall>l. \<box>$MemInv mm l)"
by (auto simp: IPImp_def box_stp_act [temp_use] intro!: MemoryInvariantAll [temp_use])
-lemma Step1_5_1b: "\<turnstile> Init(ImpInit p & HInit rmhist p) & \<box>(ImpNext p)
- & \<box>[HNext rmhist p]_(c p, r p, m p, rmhist!p) & \<box>(\<forall>l. $MemInv mm l)
+lemma Step1_5_1b: "\<turnstile> Init(ImpInit p \<and> HInit rmhist p) \<and> \<box>(ImpNext p)
+ \<and> \<box>[HNext rmhist p]_(c p, r p, m p, rmhist!p) \<and> \<box>(\<forall>l. $MemInv mm l)
\<longrightarrow> \<box>ImpInv rmhist p"
apply invariant
apply (auto simp: Init_def ImpInv_def box_stp_act [temp_use]
@@ -1218,26 +1218,26 @@
done
(*** Initialization ***)
-lemma Step1_5_2a: "\<turnstile> Init(ImpInit p & HInit rmhist p) \<longrightarrow> Init(PInit (resbar rmhist) p)"
+lemma Step1_5_2a: "\<turnstile> Init(ImpInit p \<and> HInit rmhist p) \<longrightarrow> Init(PInit (resbar rmhist) p)"
by (auto simp: Init_def intro!: Step1_1 [temp_use] Step1_3 [temp_use])
(*** step simulation ***)
-lemma Step1_5_2b: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)
- & $ImpInv rmhist p & (\<forall>l. $MemInv mm l))
+lemma Step1_5_2b: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p)
+ \<and> $ImpInv rmhist p \<and> (\<forall>l. $MemInv mm l))
\<longrightarrow> \<box>[UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
by (auto simp: ImpInv_def elim!: STL4E [temp_use]
dest!: S1safe [temp_use] S2safe [temp_use] S3safe [temp_use] S4safe [temp_use]
S5safe [temp_use] S6safe [temp_use])
(*** Liveness ***)
-lemma GoodImpl: "\<turnstile> IPImp p & HistP rmhist p
- \<longrightarrow> Init(ImpInit p & HInit rmhist p)
- & \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
- & \<box>(\<forall>l. $MemInv mm l) & \<box>($ImpInv rmhist p)
- & ImpLive p"
+lemma GoodImpl: "\<turnstile> IPImp p \<and> HistP rmhist p
+ \<longrightarrow> Init(ImpInit p \<and> HInit rmhist p)
+ \<and> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p))
+ \<and> \<box>(\<forall>l. $MemInv mm l) \<and> \<box>($ImpInv rmhist p)
+ \<and> ImpLive p"
apply clarsimp
- apply (subgoal_tac "sigma \<Turnstile> Init (ImpInit p & HInit rmhist p) & \<box> (ImpNext p) &
- \<box>[HNext rmhist p]_ (c p, r p, m p, rmhist!p) & \<box> (\<forall>l. $MemInv mm l)")
+ apply (subgoal_tac "sigma \<Turnstile> Init (ImpInit p \<and> HInit rmhist p) \<and> \<box> (ImpNext p) \<and>
+ \<box>[HNext rmhist p]_ (c p, r p, m p, rmhist!p) \<and> \<box> (\<forall>l. $MemInv mm l)")
apply (auto simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite]
dest!: Step1_5_1b [temp_use])
apply (force simp: IPImp_def MClkIPSpec_def RPCIPSpec_def RPSpec_def
@@ -1251,9 +1251,9 @@
done
(* The implementation is infinitely often in state S1... *)
-lemma Step1_5_3a: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
- & \<box>(\<forall>l. $MemInv mm l)
- & \<box>($ImpInv rmhist p) & ImpLive p
+lemma Step1_5_3a: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p))
+ \<and> \<box>(\<forall>l. $MemInv mm l)
+ \<and> \<box>($ImpInv rmhist p) \<and> ImpLive p
\<longrightarrow> \<box>\<diamond>S1 rmhist p"
apply (clarsimp simp: ImpLive_def)
apply (rule S1Infinite)
@@ -1264,18 +1264,18 @@
done
(* ... and therefore satisfies the fairness requirements of the specification *)
-lemma Step1_5_3b: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
- & \<box>(\<forall>l. $MemInv mm l) & \<box>($ImpInv rmhist p) & ImpLive p
+lemma Step1_5_3b: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p))
+ \<and> \<box>(\<forall>l. $MemInv mm l) \<and> \<box>($ImpInv rmhist p) \<and> ImpLive p
\<longrightarrow> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
by (auto intro!: RNext_fair [temp_use] Step1_5_3a [temp_use])
-lemma Step1_5_3c: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
- & \<box>(\<forall>l. $MemInv mm l) & \<box>($ImpInv rmhist p) & ImpLive p
+lemma Step1_5_3c: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p))
+ \<and> \<box>(\<forall>l. $MemInv mm l) \<and> \<box>($ImpInv rmhist p) \<and> ImpLive p
\<longrightarrow> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
by (auto intro!: Return_fair [temp_use] Step1_5_3a [temp_use])
(* QED step of step 1 *)
-lemma Step1: "\<turnstile> IPImp p & HistP rmhist p --> UPSpec memCh mm (resbar rmhist) p"
+lemma Step1: "\<turnstile> IPImp p \<and> HistP rmhist p \<longrightarrow> UPSpec memCh mm (resbar rmhist) p"
by (auto simp: UPSpec_def split_box_conj [temp_use]
dest!: GoodImpl [temp_use] intro!: Step1_5_2a [temp_use] Step1_5_2b [temp_use]
Step1_5_3b [temp_use] Step1_5_3c [temp_use])
@@ -1283,10 +1283,10 @@
(* ------------------------------ Step 2 ------------------------------ *)
section "Step 2"
-lemma Step2_2a: "\<turnstile> Write rmCh mm ires p l & ImpNext p
- & [HNext rmhist p]_(c p, r p, m p, rmhist!p)
- & $ImpInv rmhist p
- \<longrightarrow> (S4 rmhist p)$ & unchanged (e p, c p, r p, rmhist!p)"
+lemma Step2_2a: "\<turnstile> Write rmCh mm ires p l \<and> ImpNext p
+ \<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p)
+ \<and> $ImpInv rmhist p
+ \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (e p, c p, r p, rmhist!p)"
apply clarsimp
apply (drule WriteS4 [action_use])
apply assumption
@@ -1297,9 +1297,9 @@
done
lemma Step2_2: "\<turnstile> (\<forall>p. ImpNext p)
- & (\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
- & (\<forall>p. $ImpInv rmhist p)
- & [\<exists>q. Write rmCh mm ires q l]_(mm!l)
+ \<and> (\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
+ \<and> (\<forall>p. $ImpInv rmhist p)
+ \<and> [\<exists>q. Write rmCh mm ires q l]_(mm!l)
\<longrightarrow> [\<exists>q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
apply (auto intro!: squareCI elim!: squareE)
apply (assumption | rule exI Step1_4_4b [action_use])+
@@ -1308,13 +1308,13 @@
done
lemma Step2_lemma: "\<turnstile> \<box>( (\<forall>p. ImpNext p)
- & (\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
- & (\<forall>p. $ImpInv rmhist p)
- & [\<exists>q. Write rmCh mm ires q l]_(mm!l))
+ \<and> (\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
+ \<and> (\<forall>p. $ImpInv rmhist p)
+ \<and> [\<exists>q. Write rmCh mm ires q l]_(mm!l))
\<longrightarrow> \<box>[\<exists>q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
by (force elim!: STL4E [temp_use] dest!: Step2_2 [temp_use])
-lemma Step2: "\<turnstile> #l : #MemLoc & (\<forall>p. IPImp p & HistP rmhist p)
+lemma Step2: "\<turnstile> #l \<in> #MemLoc \<and> (\<forall>p. IPImp p \<and> HistP rmhist p)
\<longrightarrow> MSpec memCh mm (resbar rmhist) l"
apply (auto simp: MSpec_def)
apply (force simp: IPImp_def MSpec_def)
@@ -1334,7 +1334,7 @@
(* Implementation of internal specification by combination of implementation
and history variable with explicit refinement mapping
*)
-lemma Impl_IUSpec: "\<turnstile> Implementation & Hist rmhist \<longrightarrow> IUSpec memCh mm (resbar rmhist)"
+lemma Impl_IUSpec: "\<turnstile> Implementation \<and> Hist rmhist \<longrightarrow> IUSpec memCh mm (resbar rmhist)"
by (auto simp: IUSpec_def Implementation_def IPImp_def MClkISpec_def
RPCISpec_def IRSpec_def Hist_def intro!: Step1 [temp_use] Step2 [temp_use])