diff -r 5b946c81dfbf -r 324bc1ffba12 src/HOL/TLA/Memory/MemoryImplementation.thy --- 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: "\ $(Calling memCh p) \ \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: "\ ENext p \ $(S1 rmhist p) \ unchanged (c p, r p, m p, rmhist!p) \ (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: "\ [MClkNext memCh crCh cst p]_(c p) \ $(S1 rmhist p) \ unchanged (c p)" @@ -352,7 +352,7 @@ \ 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}, - @{thm Return_def}]) [] [temp_use @{context} @{thm squareE}] 1\) + @{thm AReturn_def}]) [] [temp_use @{context} @{thm squareE}] 1\) (* ------------------------------ State S2 ---------------------------------------- *) @@ -367,7 +367,7 @@ \ unchanged (e p, r p, m p, rmhist!p) \ (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 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\) lemma S2RPCUnch: "\ [RPCNext crCh rmCh rst p]_(r p) \ $(S2 rmhist p) \ unchanged (r p)" @@ -380,7 +380,7 @@ \ 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 @@ \ (S4 rmhist p)$ \ 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 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\) @@ -413,7 +413,7 @@ \ unchanged (e p, c p, m p) \ (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 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\) @@ -422,7 +422,7 @@ lemma S3Hist: "\ HNext rmhist p \ $(S3 rmhist p) \ unchanged (r p) \ 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 @@ \ (S4 rmhist p)$ \ 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}, + @{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\) @@ -455,7 +455,7 @@ \ (S4 rmhist p)$ \ 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 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\) @@ -471,12 +471,12 @@ lemma S4Return: "\ MemReturn rmCh ires p \ $S4 rmhist p \ unchanged (e p, c p, r p) \ HNext rmhist p \ (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: "\ HNext rmhist p \ $S4 rmhist p \ (m p)$ = $(m p) \ (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: "\ RPCReply crCh rmCh rst p \ $(S5 rmhist p) \ unchanged (e p, c p, m p,rmhist!p) \ (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 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\) lemma S5Fail: "\ RPCFail crCh rmCh rst p \ $(S5 rmhist p) \ unchanged (e p, c p, m p,rmhist!p) \ (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 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\) @@ -511,7 +511,7 @@ \ (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 @@ \ unchanged (e p,r p,m p) \ (S3 rmhist p)$ \ 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 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\) @@ -534,7 +534,7 @@ \ unchanged (e p,r p,m p) \ (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 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\) @@ -545,7 +545,7 @@ by (auto simp: S_def S6_def dest!: Memoryidle [temp_use]) lemma S6Hist: "\ HNext rmhist p \ $S6 rmhist p \ (c p)$ = $(c p) \ (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: "\ $S4 rmhist p \ (S4 rmhist p)$ \ ReadInner rmCh mm ires p l @@ -724,7 +724,7 @@ @{thm c_def}, @{thm r_def}, @{thm resbar_def}]) [] [] 1\) 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: "\ RPCReply crCh rmCh rst p \ $S5 rmhist p \ (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: "\ RPCFail crCh rmCh rst p \ $S5 rmhist p \ (S6 rmhist p)$ @@ -741,7 +741,7 @@ \ 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 \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\) + @{thm AReturn_def}, @{thm resbar_def}]) [] [] 1\) apply simp_all (* simplify if-then-else *) apply (tactic \ALLGOALS (action_simp_tac (@{context} addsimps [@{thm MClkReplyVal_def}, @{thm S6_def}, @{thm S_def}]) [] [@{thm MVOKBARFnotNR}])\) @@ -909,7 +909,7 @@ lemma S1_Returndisabled: "\ S1 rmhist p \ \Enabled (_(rtrner memCh!p, resbar rmhist!p))" by (tactic \action_simp_tac (@{context} addsimps [@{thm angle_def}, @{thm MemReturn_def}, - @{thm Return_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1\) + @{thm AReturn_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1\) lemma RNext_fair: "\ \\S1 rmhist p \ WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)" @@ -1088,7 +1088,7 @@ lemma MClkReplyS6: "\ $ImpInv rmhist p \ _(c p) \ $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 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\) lemma S6MClkReply_enabled: "\ S6 rmhist p \ Enabled (_(c p))"