--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Mon Jan 11 21:21:02 2016 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Mon Jan 11 22:23:03 2016 +0100
@@ -320,7 +320,7 @@
(* ==================== Lemmas about the environment ============================== *)
lemma Envbusy: "\<turnstile> $(Calling memCh p) \<longrightarrow> \<not>ENext p"
- by (auto simp: ENext_def Call_def)
+ by (auto simp: ENext_def ACall_def)
(* ==================== Lemmas about the implementation's states ==================== *)
@@ -333,7 +333,7 @@
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
+ by (force simp: ENext_def ACall_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) \<and> $(S1 rmhist p) \<longrightarrow> unchanged (c p)"
@@ -352,7 +352,7 @@
\<longrightarrow> unchanged (rmhist!p)"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def}, @{thm S_def},
@{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def},
- @{thm Return_def}]) [] [temp_use @{context} @{thm squareE}] 1\<close>)
+ @{thm AReturn_def}]) [] [temp_use @{context} @{thm squareE}] 1\<close>)
(* ------------------------------ State S2 ---------------------------------------- *)
@@ -367,7 +367,7 @@
\<and> unchanged (e p, r p, m p, rmhist!p)
\<longrightarrow> (S3 rmhist p)$"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
- @{thm Call_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def},
+ @{thm ACall_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\<close>)
lemma S2RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $(S2 rmhist p) \<longrightarrow> unchanged (r p)"
@@ -380,7 +380,7 @@
\<longrightarrow> unchanged (rmhist!p)"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
- MClkReply_def Return_def S_def S2_def)
+ MClkReply_def AReturn_def S_def S2_def)
(* ------------------------------ State S3 ---------------------------------------- *)
@@ -405,7 +405,7 @@
\<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
by (tactic \<open>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 MClkReply_def}, @{thm AReturn_def}, @{thm ACall_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\<close>)
@@ -413,7 +413,7 @@
\<and> unchanged (e p, c p, m p)
\<longrightarrow> (S6 rmhist p)$"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def},
- @{thm RPCFail_def}, @{thm Return_def}, @{thm e_def}, @{thm c_def},
+ @{thm RPCFail_def}, @{thm AReturn_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\<close>)
@@ -422,7 +422,7 @@
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)
+ AReturn_def r_def rtrner_def S_def S3_def Calling_def)
(* ------------------------------ State S4 ---------------------------------------- *)
@@ -441,7 +441,7 @@
\<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
by (tactic \<open>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},
+ @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm AReturn_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 RdRequest_def},
@{thm Calling_def}, @{thm MemInv_def}]) [] [] 1\<close>)
@@ -455,7 +455,7 @@
\<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
by (tactic \<open>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 RPCFail_def}, @{thm MClkReply_def}, @{thm AReturn_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\<close>)
@@ -471,12 +471,12 @@
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
+ by (auto simp: HNext_def MemReturn_def AReturn_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 \<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)
+ AReturn_def m_def rtrner_def S_def S4_def Calling_def)
(* ------------------------------ State S5 ---------------------------------------- *)
@@ -493,14 +493,14 @@
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 \<open>action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
- @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, @{thm MVOKBA_def},
+ @{thm AReturn_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\<close>)
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 \<open>action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
- @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def},
+ @{thm AReturn_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\<close>)
@@ -511,7 +511,7 @@
\<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
- MClkReply_def Return_def S_def S5_def)
+ MClkReply_def AReturn_def S_def S5_def)
(* ------------------------------ State S6 ---------------------------------------- *)
@@ -526,7 +526,7 @@
\<and> unchanged (e p,r p,m p)
\<longrightarrow> (S3 rmhist p)$ \<and> unchanged (rmhist!p)"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def},
- @{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm Call_def}, @{thm Return_def},
+ @{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm ACall_def}, @{thm AReturn_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\<close>)
@@ -534,7 +534,7 @@
\<and> unchanged (e p,r p,m p)
\<longrightarrow> (S1 rmhist p)$"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def},
- @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm Return_def}, @{thm MClkReply_def},
+ @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm AReturn_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\<close>)
@@ -545,7 +545,7 @@
by (auto simp: S_def S6_def dest!: Memoryidle [temp_use])
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)
+ by (auto simp: HNext_def MClkReply_def AReturn_def c_def rtrner_def S_def S6_def Calling_def)
section "Correctness of predicate-action diagram"
@@ -676,7 +676,7 @@
apply (drule S6_excl [temp_use])
apply (auto simp: RPCFail_def MemFail_def e_def c_def m_def resbar_def)
apply (force simp: S3_def S_def)
- apply (auto simp: Return_def)
+ apply (auto simp: AReturn_def)
done
lemma Step1_4_4a1: "\<turnstile> $S4 rmhist p \<and> (S4 rmhist p)$ \<and> ReadInner rmCh mm ires p l
@@ -724,7 +724,7 @@
@{thm c_def}, @{thm r_def}, @{thm resbar_def}]) [] [] 1\<close>)
apply (drule S4_excl [temp_use] S5_excl [temp_use])+
using [[fast_solver]]
- apply (auto elim!: squareE [temp_use] simp: MemReturn_def Return_def)
+ apply (auto elim!: squareE [temp_use] simp: MemReturn_def AReturn_def)
done
lemma Step1_4_5a: "\<turnstile> RPCReply crCh rmCh rst p \<and> $S5 rmhist p \<and> (S6 rmhist p)$
@@ -733,7 +733,7 @@
apply clarsimp
apply (drule S5_excl [temp_use] S6_excl [temp_use])+
apply (auto simp: e_def c_def m_def resbar_def)
- apply (auto simp: RPCReply_def Return_def S5_def S_def dest!: MVOKBAnotRF [temp_use])
+ apply (auto simp: RPCReply_def AReturn_def S5_def S_def dest!: MVOKBAnotRF [temp_use])
done
lemma Step1_4_5b: "\<turnstile> RPCFail crCh rmCh rst p \<and> $S5 rmhist p \<and> (S6 rmhist p)$
@@ -741,7 +741,7 @@
\<longrightarrow> MemFail memCh (resbar rmhist) p"
apply clarsimp
apply (drule S6_excl [temp_use])
- apply (auto simp: e_def c_def m_def RPCFail_def Return_def MemFail_def resbar_def)
+ apply (auto simp: e_def c_def m_def RPCFail_def AReturn_def MemFail_def resbar_def)
apply (auto simp: S5_def S_def)
done
@@ -752,7 +752,7 @@
apply (drule S6_excl [temp_use])+
apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm e_def},
@{thm r_def}, @{thm m_def}, @{thm MClkReply_def}, @{thm MemReturn_def},
- @{thm Return_def}, @{thm resbar_def}]) [] [] 1\<close>)
+ @{thm AReturn_def}, @{thm resbar_def}]) [] [] 1\<close>)
apply simp_all (* simplify if-then-else *)
apply (tactic \<open>ALLGOALS (action_simp_tac (@{context} addsimps
[@{thm MClkReplyVal_def}, @{thm S6_def}, @{thm S_def}]) [] [@{thm MVOKBARFnotNR}])\<close>)
@@ -909,7 +909,7 @@
lemma S1_Returndisabled: "\<turnstile> S1 rmhist p \<longrightarrow>
\<not>Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm angle_def}, @{thm MemReturn_def},
- @{thm Return_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1\<close>)
+ @{thm AReturn_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1\<close>)
lemma RNext_fair: "\<turnstile> \<box>\<diamond>S1 rmhist p
\<longrightarrow> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
@@ -1088,7 +1088,7 @@
lemma MClkReplyS6:
"\<turnstile> $ImpInv rmhist p \<and> <MClkReply memCh crCh cst p>_(c p) \<longrightarrow> $S6 rmhist p"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm angle_def},
- @{thm MClkReply_def}, @{thm Return_def}, @{thm ImpInv_def}, @{thm S_def},
+ @{thm MClkReply_def}, @{thm AReturn_def}, @{thm ImpInv_def}, @{thm S_def},
@{thm S1_def}, @{thm S2_def}, @{thm S3_def}, @{thm S4_def}, @{thm S5_def}]) [] [] 1\<close>)
lemma S6MClkReply_enabled: "\<turnstile> S6 rmhist p \<longrightarrow> Enabled (<MClkReply memCh crCh cst p>_(c p))"