--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Mon Sep 06 19:13:10 2010 +0200
@@ -255,10 +255,10 @@
apply (rule historyI)
apply assumption+
apply (rule MI_base)
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "HInit_def"]) [] [] 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HInit_def}]) [] [] 1 *})
apply (erule fun_cong)
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def"])
- [thm "busy_squareI"] [] 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def}])
+ [@{thm busy_squareI}] [] 1 *})
apply (erule fun_cong)
done
@@ -346,22 +346,22 @@
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)"
- by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use (thm "MClkidle")]
- addsimps2 [thm "S_def", thm "S1_def"]) *})
+ by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use @{thm MClkidle}]
+ addsimps2 [@{thm S_def}, @{thm S1_def}]) *})
lemma S1RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S1 rmhist p) --> unchanged (r p)"
- by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use (thm "RPCidle")]
- addsimps2 [thm "S_def", thm "S1_def"]) *})
+ by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use @{thm RPCidle}]
+ addsimps2 [@{thm S_def}, @{thm S1_def}]) *})
lemma S1MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S1 rmhist p) --> unchanged (m p)"
- by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use (thm "Memoryidle")]
- addsimps2 [thm "S_def", thm "S1_def"]) *})
+ by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use @{thm Memoryidle}]
+ addsimps2 [@{thm S_def}, @{thm S1_def}]) *})
lemma S1Hist: "|- [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S1 rmhist p)
--> unchanged (rmhist!p)"
- by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def", thm "S_def",
- thm "S1_def", thm "MemReturn_def", thm "RPCFail_def", thm "MClkReply_def",
- thm "Return_def"]) [] [temp_use (thm "squareE")] 1 *})
+ by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def}, @{thm S_def},
+ @{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def},
+ @{thm Return_def}]) [] [temp_use @{thm squareE}] 1 *})
(* ------------------------------ State S2 ---------------------------------------- *)
@@ -375,9 +375,9 @@
lemma S2Forward: "|- $(S2 rmhist p) & MClkFwd memCh crCh cst p
& unchanged (e p, r p, m p, rmhist!p)
--> (S3 rmhist p)$"
- by (tactic {* action_simp_tac (@{simpset} 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 *})
+ by (tactic {* action_simp_tac (@{simpset} 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: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S2 rmhist p) --> unchanged (r p)"
by (auto simp: S_def S2_def dest!: RPCidle [temp_use])
@@ -387,8 +387,8 @@
lemma S2Hist: "|- [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S2 rmhist p)
--> unchanged (rmhist!p)"
- by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "HNext_def", thm "MemReturn_def",
- thm "RPCFail_def", thm "MClkReply_def", thm "Return_def", thm "S_def", thm "S2_def"]) *})
+ by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm HNext_def}, @{thm MemReturn_def},
+ @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm S_def}, @{thm S2_def}]) *})
(* ------------------------------ State S3 ---------------------------------------- *)
@@ -411,19 +411,19 @@
lemma S3Forward: "|- RPCFwd crCh rmCh rst p & HNext rmhist p & $(S3 rmhist p)
& unchanged (e p, c p, m p)
--> (S4 rmhist p)$ & unchanged (rmhist!p)"
- by (tactic {* action_simp_tac (@{simpset} 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 *})
+ by (tactic {* action_simp_tac (@{simpset} 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: "|- RPCFail crCh rmCh rst p & $(S3 rmhist p) & HNext rmhist p
& unchanged (e p, c p, m p)
--> (S6 rmhist p)$"
- by (tactic {* action_simp_tac (@{simpset} 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 *})
+ by (tactic {* action_simp_tac (@{simpset} 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: "|- [RNext rmCh mm ires p]_(m p) & $(S3 rmhist p) --> unchanged (m p)"
by (auto simp: S_def S3_def dest!: Memoryidle [temp_use])
@@ -441,18 +441,18 @@
by (auto simp: S_def S4_def dest!: MClkbusy [temp_use])
lemma S4RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S4 rmhist p) --> unchanged (r p)"
- by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "S_def", thm "S4_def"]
- addSDs2 [temp_use (thm "RPCbusy")]) *})
+ by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm S_def}, @{thm S4_def}]
+ addSDs2 [temp_use @{thm RPCbusy}]) *})
lemma S4ReadInner: "|- ReadInner rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
& HNext rmhist p & $(MemInv mm l)
--> (S4 rmhist p)$ & unchanged (rmhist!p)"
- by (tactic {* action_simp_tac (@{simpset} 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 "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 *})
+ by (tactic {* action_simp_tac (@{simpset} 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 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 *})
lemma S4Read: "|- Read rmCh mm ires p & $(S4 rmhist p) & unchanged (e p, c p, r p)
& HNext rmhist p & (!l. $MemInv mm l)
@@ -461,11 +461,11 @@
lemma S4WriteInner: "|- WriteInner rmCh mm ires p l v & $(S4 rmhist p) & unchanged (e p, c p, r p) & HNext rmhist p
--> (S4 rmhist p)$ & unchanged (rmhist!p)"
- by (tactic {* action_simp_tac (@{simpset} 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 *})
+ by (tactic {* action_simp_tac (@{simpset} 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: "|- Write rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
& (HNext rmhist p)
@@ -500,26 +500,26 @@
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 (@{simpset} 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 *})
+ by (tactic {* action_simp_tac (@{simpset} 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: "|- 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 (@{simpset} 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 *})
+ by (tactic {* action_simp_tac (@{simpset} 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: "|- [RNext rmCh mm ires p]_(m p) & $(S5 rmhist p) --> unchanged (m p)"
by (auto simp: S_def S5_def dest!: Memoryidle [temp_use])
lemma S5Hist: "|- [HNext rmhist p]_(c p, r p, m p, rmhist!p) & $(S5 rmhist p)
--> (rmhist!p)$ = $(rmhist!p)"
- by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "HNext_def",
- thm "MemReturn_def", thm "RPCFail_def", thm "MClkReply_def", thm "Return_def",
- thm "S_def", thm "S5_def"]) *})
+ by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm HNext_def},
+ @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def},
+ @{thm S_def}, @{thm S5_def}]) *})
(* ------------------------------ State S6 ---------------------------------------- *)
@@ -533,18 +533,18 @@
lemma S6Retry: "|- MClkRetry memCh crCh cst p & HNext rmhist p & $S6 rmhist p
& unchanged (e p,r p,m p)
--> (S3 rmhist p)$ & unchanged (rmhist!p)"
- by (tactic {* action_simp_tac (@{simpset} 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 *})
+ by (tactic {* action_simp_tac (@{simpset} 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: "|- MClkReply memCh crCh cst p & HNext rmhist p & $S6 rmhist p
& unchanged (e p,r p,m p)
--> (S1 rmhist p)$"
- by (tactic {* action_simp_tac (@{simpset} 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 *})
+ by (tactic {* action_simp_tac (@{simpset} 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: "|- [RPCNext crCh rmCh rst p]_(r p) & $S6 rmhist p --> unchanged (r p)"
by (auto simp: S_def S6_def dest!: RPCidle [temp_use])
@@ -563,9 +563,9 @@
(* The implementation's initial condition implies the state predicate S1 *)
lemma Step1_1: "|- ImpInit p & HInit rmhist p --> S1 rmhist p"
- by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "MVNROKBA_def",
- thm "MClkInit_def", thm "RPCInit_def", thm "PInit_def", thm "HInit_def",
- thm "ImpInit_def", thm "S_def", thm "S1_def"]) *})
+ by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm MVNROKBA_def},
+ @{thm MClkInit_def}, @{thm RPCInit_def}, @{thm PInit_def}, @{thm HInit_def},
+ @{thm ImpInit_def}, @{thm S_def}, @{thm S1_def}]) *})
(* ========== Step 1.2 ================================================== *)
(* Figure 16 is a predicate-action diagram for the implementation. *)
@@ -573,29 +573,29 @@
lemma Step1_2_1: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
& ~unchanged (e p, c p, r p, m p, rmhist!p) & $S1 rmhist p
--> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
- (map temp_elim [thm "S1ClerkUnch", thm "S1RPCUnch", thm "S1MemUnch", thm "S1Hist"]) 1 *})
- apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use (thm "S1Env")]) *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
+ (map temp_elim [@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1 *})
+ apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use @{thm S1Env}]) *})
done
lemma Step1_2_2: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
& ~unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p
--> (S3 rmhist p)$ & MClkFwd memCh crCh cst p
& unchanged (e p, r p, m p, rmhist!p)"
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
- (map temp_elim [thm "S2EnvUnch", thm "S2RPCUnch", thm "S2MemUnch", thm "S2Hist"]) 1 *})
- apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use (thm "S2Clerk"),
- temp_use (thm "S2Forward")]) *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
+ (map temp_elim [@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1 *})
+ apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use @{thm S2Clerk},
+ temp_use @{thm S2Forward}]) *})
done
lemma Step1_2_3: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
& ~unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p
--> ((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))"
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
- (map temp_elim [thm "S3EnvUnch", thm "S3ClerkUnch", thm "S3MemUnch"]) 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
+ (map temp_elim [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1 *})
apply (tactic {* action_simp_tac @{simpset} []
- (thm "squareE" :: map temp_elim [thm "S3RPC", thm "S3Forward", thm "S3Fail"]) 1 *})
+ (@{thm squareE} :: map temp_elim [@{thm S3RPC}, @{thm S3Forward}, @{thm S3Fail}]) 1 *})
apply (auto dest!: S3Hist [temp_use])
done
@@ -605,10 +605,10 @@
--> ((S4 rmhist p)$ & Read rmCh mm ires p & unchanged (e p, c p, r p, rmhist!p))
| ((S4 rmhist p)$ & (? 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))"
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
- (map temp_elim [thm "S4EnvUnch", thm "S4ClerkUnch", thm "S4RPCUnch"]) 1 *})
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "RNext_def"]) []
- (thm "squareE" :: map temp_elim [thm "S4Read", thm "S4Write", thm "S4Return"]) 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
+ (map temp_elim [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RNext_def}]) []
+ (@{thm squareE} :: map temp_elim [@{thm S4Read}, @{thm S4Write}, @{thm S4Return}]) 1 *})
apply (auto dest!: S4Hist [temp_use])
done
@@ -616,21 +616,21 @@
& ~unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p
--> ((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))"
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
- (map temp_elim [thm "S5EnvUnch", thm "S5ClerkUnch", thm "S5MemUnch", thm "S5Hist"]) 1 *})
- apply (tactic {* action_simp_tac @{simpset} [] [thm "squareE", temp_elim (thm "S5RPC")] 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
+ (map temp_elim [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1 *})
+ apply (tactic {* action_simp_tac @{simpset} [] [@{thm squareE}, temp_elim @{thm S5RPC}] 1 *})
apply (tactic {* auto_tac (MI_fast_css addSDs2
- [temp_use (thm "S5Reply"), temp_use (thm "S5Fail")]) *})
+ [temp_use @{thm S5Reply}, temp_use @{thm S5Fail}]) *})
done
lemma Step1_2_6: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
& ~unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p
--> ((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))"
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
- (map temp_elim [thm "S6EnvUnch", thm "S6RPCUnch", thm "S6MemUnch"]) 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
+ (map temp_elim [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1 *})
apply (tactic {* action_simp_tac @{simpset} []
- (thm "squareE" :: map temp_elim [thm "S6Clerk", thm "S6Retry", thm "S6Reply"]) 1 *})
+ (@{thm squareE} :: map temp_elim [@{thm S6Clerk}, @{thm S6Retry}, @{thm S6Reply}]) 1 *})
apply (auto dest: S6Hist [temp_use])
done
@@ -641,8 +641,8 @@
section "Initialization (Step 1.3)"
lemma Step1_3: "|- S1 rmhist p --> PInit (resbar rmhist) p"
- by (tactic {* action_simp_tac (@{simpset} addsimps [thm "resbar_def",
- thm "PInit_def", thm "S_def", thm "S1_def"]) [] [] 1 *})
+ by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm resbar_def},
+ @{thm PInit_def}, @{thm S_def}, @{thm S1_def}]) [] [] 1 *})
(* ----------------------------------------------------------------------
Step 1.4: Implementation's next-state relation simulates specification's
@@ -653,23 +653,23 @@
lemma Step1_4_1: "|- ENext p & $S1 rmhist p & (S2 rmhist p)$ & unchanged (c p, r p, m p)
--> unchanged (rtrner memCh!p, resbar rmhist!p)"
- by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "c_def", thm "r_def",
- thm "m_def", thm "resbar_def"]) *})
+ by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm c_def}, @{thm r_def},
+ @{thm m_def}, @{thm resbar_def}]) *})
lemma Step1_4_2: "|- MClkFwd memCh crCh cst p & $S2 rmhist p & (S3 rmhist p)$
& unchanged (e p, r p, m p, rmhist!p)
--> unchanged (rtrner memCh!p, resbar rmhist!p)"
by (tactic {* action_simp_tac
- (@{simpset} 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 *})
+ (@{simpset} 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: "|- RPCFwd crCh rmCh rst p & $S3 rmhist p & (S4 rmhist p)$
& unchanged (e p, c p, m p, rmhist!p)
--> unchanged (rtrner memCh!p, resbar rmhist!p)"
apply clarsimp
apply (drule S3_excl [temp_use] S4_excl [temp_use])+
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
- thm "c_def", thm "m_def", thm "resbar_def", thm "S_def", thm "S3_def"]) [] [] 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def},
+ @{thm c_def}, @{thm m_def}, @{thm resbar_def}, @{thm S_def}, @{thm S3_def}]) [] [] 1 *})
done
lemma Step1_4_3b: "|- RPCFail crCh rmCh rst p & $S3 rmhist p & (S6 rmhist p)$
@@ -687,13 +687,13 @@
--> ReadInner memCh mm (resbar rmhist) p l"
apply clarsimp
apply (drule S4_excl [temp_use])+
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ReadInner_def",
- thm "GoodRead_def", thm "BadRead_def", thm "e_def", thm "c_def", thm "m_def"]) [] [] 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ReadInner_def},
+ @{thm GoodRead_def}, @{thm BadRead_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}]) [] [] 1 *})
apply (auto simp: resbar_def)
apply (tactic {* ALLGOALS (action_simp_tac
- (@{simpset} addsimps [thm "RPCRelayArg_def", thm "MClkRelayArg_def",
- thm "S_def", thm "S4_def", thm "RdRequest_def", thm "MemInv_def"])
- [] [thm "impE", thm "MemValNotAResultE"]) *})
+ (@{simpset} addsimps [@{thm RPCRelayArg_def}, @{thm MClkRelayArg_def},
+ @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def}, @{thm MemInv_def}])
+ [] [@{thm impE}, @{thm MemValNotAResultE}]) *})
done
lemma Step1_4_4a: "|- Read rmCh mm ires p & $S4 rmhist p & (S4 rmhist p)$
@@ -707,12 +707,12 @@
apply clarsimp
apply (drule S4_excl [temp_use])+
apply (tactic {* action_simp_tac (@{simpset} addsimps
- [thm "WriteInner_def", thm "GoodWrite_def", thm "BadWrite_def", thm "e_def",
- thm "c_def", thm "m_def"]) [] [] 1 *})
+ [@{thm WriteInner_def}, @{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm e_def},
+ @{thm c_def}, @{thm m_def}]) [] [] 1 *})
apply (auto simp: resbar_def)
apply (tactic {* ALLGOALS (action_simp_tac (@{simpset} addsimps
- [thm "RPCRelayArg_def", thm "MClkRelayArg_def", thm "S_def",
- thm "S4_def", thm "WrRequest_def"]) [] []) *})
+ [@{thm RPCRelayArg_def}, @{thm MClkRelayArg_def}, @{thm S_def},
+ @{thm S4_def}, @{thm WrRequest_def}]) [] []) *})
done
lemma Step1_4_4b: "|- Write rmCh mm ires p l & $S4 rmhist p & (S4 rmhist p)$
@@ -723,10 +723,10 @@
lemma Step1_4_4c: "|- MemReturn rmCh ires p & $S4 rmhist p & (S5 rmhist p)$
& unchanged (e p, c p, r p)
--> unchanged (rtrner memCh!p, resbar rmhist!p)"
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
- thm "c_def", thm "r_def", thm "resbar_def"]) [] [] 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def},
+ @{thm c_def}, @{thm r_def}, @{thm resbar_def}]) [] [] 1 *})
apply (drule S4_excl [temp_use] S5_excl [temp_use])+
- apply (tactic {* auto_tac (MI_fast_css addsimps2 [thm "MemReturn_def", thm "Return_def"]) *})
+ apply (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm MemReturn_def}, @{thm Return_def}]) *})
done
lemma Step1_4_5a: "|- RPCReply crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$
@@ -752,12 +752,12 @@
--> MemReturn memCh (resbar rmhist) p"
apply clarsimp
apply (drule S6_excl [temp_use])+
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
- thm "r_def", thm "m_def", thm "MClkReply_def", thm "MemReturn_def",
- thm "Return_def", thm "resbar_def"]) [] [] 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def},
+ @{thm r_def}, @{thm m_def}, @{thm MClkReply_def}, @{thm MemReturn_def},
+ @{thm Return_def}, @{thm resbar_def}]) [] [] 1 *})
apply simp_all (* simplify if-then-else *)
apply (tactic {* ALLGOALS (action_simp_tac (@{simpset} addsimps
- [thm "MClkReplyVal_def", thm "S6_def", thm "S_def"]) [] [thm "MVOKBARFnotNR"]) *})
+ [@{thm MClkReplyVal_def}, @{thm S6_def}, @{thm S_def}]) [] [@{thm MVOKBARFnotNR}]) *})
done
lemma Step1_4_6b: "|- MClkRetry memCh crCh cst p & $S6 rmhist p & (S3 rmhist p)$
@@ -765,8 +765,8 @@
--> MemFail memCh (resbar rmhist) p"
apply clarsimp
apply (drule S3_excl [temp_use])+
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def", thm "r_def",
- thm "m_def", thm "MClkRetry_def", thm "MemFail_def", thm "resbar_def"]) [] [] 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def}, @{thm r_def},
+ @{thm m_def}, @{thm MClkRetry_def}, @{thm MemFail_def}, @{thm resbar_def}]) [] [] 1 *})
apply (auto simp: S6_def S_def)
done
@@ -816,7 +816,7 @@
lemma unchanged_safe: "|- (~unchanged (e p, c p, r p, m p, rmhist!p)
--> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p))
--> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
- apply (tactic {* split_idle_tac @{context} [thm "square_def"] 1 *})
+ apply (tactic {* split_idle_tac @{context} [@{thm square_def}] 1 *})
apply force
done
(* turn into (unsafe, looping!) introduction rule *)
@@ -898,15 +898,15 @@
lemma S1_RNextdisabled: "|- S1 rmhist p -->
~Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
- apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def",
- thm "S_def", thm "S1_def"]) [notI] [thm "enabledE", temp_elim (thm "Memoryidle")] 1 *})
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm angle_def},
+ @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{thm Memoryidle}] 1 *})
apply force
done
lemma S1_Returndisabled: "|- S1 rmhist p -->
~Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
- by (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def", thm "MemReturn_def",
- thm "Return_def", thm "S_def", thm "S1_def"]) [notI] [thm "enabledE"] 1 *})
+ by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm angle_def}, @{thm MemReturn_def},
+ @{thm Return_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)"
@@ -986,7 +986,7 @@
& ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l)
--> (S4 rmhist p & ires!p = #NotAResult)$
| ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$"
- apply (tactic {* split_idle_tac @{context} [thm "m_def"] 1 *})
+ apply (tactic {* split_idle_tac @{context} [@{thm m_def}] 1 *})
apply (auto dest!: Step1_2_4 [temp_use])
done
@@ -1017,7 +1017,7 @@
lemma S4b_successors: "|- $(S4 rmhist p & ires!p ~= #NotAResult)
& ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l)
--> (S4 rmhist p & ires!p ~= #NotAResult)$ | (S5 rmhist p)$"
- apply (tactic {* split_idle_tac @{context} [thm "m_def"] 1 *})
+ apply (tactic {* split_idle_tac @{context} [@{thm m_def}] 1 *})
apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use])
done
@@ -1084,16 +1084,16 @@
lemma MClkReplyS6:
"|- $ImpInv rmhist p & <MClkReply memCh crCh cst p>_(c p) --> $S6 rmhist p"
- by (tactic {* action_simp_tac (@{simpset} 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 *})
+ by (tactic {* action_simp_tac (@{simpset} 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 *})
lemma S6MClkReply_enabled: "|- S6 rmhist p --> Enabled (<MClkReply memCh crCh cst p>_(c p))"
apply (auto simp: c_def intro!: MClkReply_enabled [temp_use])
apply (cut_tac MI_base)
apply (blast dest: base_pair)
apply (tactic {* ALLGOALS (action_simp_tac (@{simpset}
- addsimps [thm "S_def", thm "S6_def"]) [] []) *})
+ addsimps [@{thm S_def}, @{thm S6_def}]) [] []) *})
done
lemma S6_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & $(ImpInv rmhist p))
@@ -1104,7 +1104,7 @@
apply (erule InfiniteEnsures)
apply assumption
apply (tactic {* action_simp_tac @{simpset} []
- (map temp_elim [thm "MClkReplyS6", thm "S6MClkReply_successors"]) 1 *})
+ (map temp_elim [@{thm MClkReplyS6}, @{thm S6MClkReply_successors}]) 1 *})
apply (auto simp: SF_def)
apply (erule contrapos_np)
apply (auto intro!: S6MClkReply_enabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use])
@@ -1191,7 +1191,7 @@
==> sigma |= []<>S1 rmhist p"
apply (rule classical)
apply (tactic {* asm_lr_simp_tac (@{simpset} addsimps
- [temp_use (thm "NotBox"), temp_rewrite (thm "NotDmd")]) 1 *})
+ [temp_use @{thm NotBox}, temp_rewrite @{thm NotDmd}]) 1 *})
apply (auto elim!: leadsto_infinite [temp_use] mp dest!: DBImplBD [temp_use])
done