src/HOL/TLA/Memory/MemoryImplementation.thy
changeset 39159 0dec18004e75
parent 36866 426d5781bb25
child 41589 bbd861837ebc
     1.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -255,10 +255,10 @@
     1.4    apply (rule historyI)
     1.5        apply assumption+
     1.6    apply (rule MI_base)
     1.7 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "HInit_def"]) [] [] 1 *})
     1.8 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HInit_def}]) [] [] 1 *})
     1.9     apply (erule fun_cong)
    1.10 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def"])
    1.11 -    [thm "busy_squareI"] [] 1 *})
    1.12 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def}])
    1.13 +    [@{thm busy_squareI}] [] 1 *})
    1.14    apply (erule fun_cong)
    1.15    done
    1.16  
    1.17 @@ -346,22 +346,22 @@
    1.18      caller_def rtrner_def MVNROKBA_def S_def S1_def S2_def Calling_def)
    1.19  
    1.20  lemma S1ClerkUnch: "|- [MClkNext memCh crCh cst p]_(c p) & $(S1 rmhist p) --> unchanged (c p)"
    1.21 -  by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use (thm "MClkidle")]
    1.22 -    addsimps2 [thm "S_def", thm "S1_def"]) *})
    1.23 +  by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use @{thm MClkidle}]
    1.24 +    addsimps2 [@{thm S_def}, @{thm S1_def}]) *})
    1.25  
    1.26  lemma S1RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S1 rmhist p) --> unchanged (r p)"
    1.27 -  by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use (thm "RPCidle")]
    1.28 -    addsimps2 [thm "S_def", thm "S1_def"]) *})
    1.29 +  by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use @{thm RPCidle}]
    1.30 +    addsimps2 [@{thm S_def}, @{thm S1_def}]) *})
    1.31  
    1.32  lemma S1MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S1 rmhist p) --> unchanged (m p)"
    1.33 -  by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use (thm "Memoryidle")]
    1.34 -    addsimps2 [thm "S_def", thm "S1_def"]) *})
    1.35 +  by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use @{thm Memoryidle}]
    1.36 +    addsimps2 [@{thm S_def}, @{thm S1_def}]) *})
    1.37  
    1.38  lemma S1Hist: "|- [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S1 rmhist p)
    1.39           --> unchanged (rmhist!p)"
    1.40 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def", thm "S_def",
    1.41 -    thm "S1_def", thm "MemReturn_def", thm "RPCFail_def", thm "MClkReply_def",
    1.42 -    thm "Return_def"]) [] [temp_use (thm "squareE")] 1 *})
    1.43 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def}, @{thm S_def},
    1.44 +    @{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def},
    1.45 +    @{thm Return_def}]) [] [temp_use @{thm squareE}] 1 *})
    1.46  
    1.47  
    1.48  (* ------------------------------ State S2 ---------------------------------------- *)
    1.49 @@ -375,9 +375,9 @@
    1.50  lemma S2Forward: "|- $(S2 rmhist p) & MClkFwd memCh crCh cst p
    1.51           & unchanged (e p, r p, m p, rmhist!p)
    1.52           --> (S3 rmhist p)$"
    1.53 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "MClkFwd_def",
    1.54 -    thm "Call_def", thm "e_def", thm "r_def", thm "m_def", thm "caller_def",
    1.55 -    thm "rtrner_def", thm "S_def", thm "S2_def", thm "S3_def", thm "Calling_def"]) [] [] 1 *})
    1.56 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm MClkFwd_def},
    1.57 +    @{thm Call_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def},
    1.58 +    @{thm rtrner_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1 *})
    1.59  
    1.60  lemma S2RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S2 rmhist p) --> unchanged (r p)"
    1.61    by (auto simp: S_def S2_def dest!: RPCidle [temp_use])
    1.62 @@ -387,8 +387,8 @@
    1.63  
    1.64  lemma S2Hist: "|- [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S2 rmhist p)
    1.65           --> unchanged (rmhist!p)"
    1.66 -  by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "HNext_def", thm "MemReturn_def",
    1.67 -    thm "RPCFail_def", thm "MClkReply_def", thm "Return_def", thm "S_def", thm "S2_def"]) *})
    1.68 +  by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm HNext_def}, @{thm MemReturn_def},
    1.69 +    @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm S_def}, @{thm S2_def}]) *})
    1.70  
    1.71  (* ------------------------------ State S3 ---------------------------------------- *)
    1.72  
    1.73 @@ -411,19 +411,19 @@
    1.74  lemma S3Forward: "|- RPCFwd crCh rmCh rst p & HNext rmhist p & $(S3 rmhist p)
    1.75           & unchanged (e p, c p, m p)
    1.76           --> (S4 rmhist p)$ & unchanged (rmhist!p)"
    1.77 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCFwd_def",
    1.78 -    thm "HNext_def", thm "MemReturn_def", thm "RPCFail_def",
    1.79 -    thm "MClkReply_def", thm "Return_def", thm "Call_def", thm "e_def",
    1.80 -    thm "c_def", thm "m_def", thm "caller_def", thm "rtrner_def", thm "S_def",
    1.81 -    thm "S3_def", thm "S4_def", thm "Calling_def"]) [] [] 1 *})
    1.82 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCFwd_def},
    1.83 +    @{thm HNext_def}, @{thm MemReturn_def}, @{thm RPCFail_def},
    1.84 +    @{thm MClkReply_def}, @{thm Return_def}, @{thm Call_def}, @{thm e_def},
    1.85 +    @{thm c_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
    1.86 +    @{thm S3_def}, @{thm S4_def}, @{thm Calling_def}]) [] [] 1 *})
    1.87  
    1.88  lemma S3Fail: "|- RPCFail crCh rmCh rst p & $(S3 rmhist p) & HNext rmhist p
    1.89           & unchanged (e p, c p, m p)
    1.90           --> (S6 rmhist p)$"
    1.91 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def",
    1.92 -    thm "RPCFail_def", thm "Return_def", thm "e_def", thm "c_def",
    1.93 -    thm "m_def", thm "caller_def", thm "rtrner_def", thm "MVOKBARF_def",
    1.94 -    thm "S_def", thm "S3_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *})
    1.95 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def},
    1.96 +    @{thm RPCFail_def}, @{thm Return_def}, @{thm e_def}, @{thm c_def},
    1.97 +    @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm MVOKBARF_def},
    1.98 +    @{thm S_def}, @{thm S3_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
    1.99  
   1.100  lemma S3MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S3 rmhist p) --> unchanged (m p)"
   1.101    by (auto simp: S_def S3_def dest!: Memoryidle [temp_use])
   1.102 @@ -441,18 +441,18 @@
   1.103    by (auto simp: S_def S4_def dest!: MClkbusy [temp_use])
   1.104  
   1.105  lemma S4RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S4 rmhist p) --> unchanged (r p)"
   1.106 -  by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "S_def", thm "S4_def"]
   1.107 -    addSDs2 [temp_use (thm "RPCbusy")]) *})
   1.108 +  by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm S_def}, @{thm S4_def}]
   1.109 +    addSDs2 [temp_use @{thm RPCbusy}]) *})
   1.110  
   1.111  lemma S4ReadInner: "|- ReadInner rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
   1.112           & HNext rmhist p & $(MemInv mm l)
   1.113           --> (S4 rmhist p)$ & unchanged (rmhist!p)"
   1.114 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "ReadInner_def",
   1.115 -    thm "GoodRead_def", thm "BadRead_def", thm "HNext_def", thm "MemReturn_def",
   1.116 -    thm "RPCFail_def", thm "MClkReply_def", thm "Return_def", thm "e_def",
   1.117 -    thm "c_def", thm "r_def", thm "rtrner_def", thm "caller_def",
   1.118 -    thm "MVNROKBA_def", thm "S_def", thm "S4_def", thm "RdRequest_def",
   1.119 -    thm "Calling_def", thm "MemInv_def"]) [] [] 1 *})
   1.120 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ReadInner_def},
   1.121 +    @{thm GoodRead_def}, @{thm BadRead_def}, @{thm HNext_def}, @{thm MemReturn_def},
   1.122 +    @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
   1.123 +    @{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def},
   1.124 +    @{thm MVNROKBA_def}, @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def},
   1.125 +    @{thm Calling_def}, @{thm MemInv_def}]) [] [] 1 *})
   1.126  
   1.127  lemma S4Read: "|- Read rmCh mm ires p & $(S4 rmhist p) & unchanged (e p, c p, r p)
   1.128           & HNext rmhist p & (!l. $MemInv mm l)
   1.129 @@ -461,11 +461,11 @@
   1.130  
   1.131  lemma S4WriteInner: "|- WriteInner rmCh mm ires p l v & $(S4 rmhist p) & unchanged (e p, c p, r p)           & HNext rmhist p
   1.132           --> (S4 rmhist p)$ & unchanged (rmhist!p)"
   1.133 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "WriteInner_def",
   1.134 -    thm "GoodWrite_def", thm "BadWrite_def", thm "HNext_def", thm "MemReturn_def",
   1.135 -    thm "RPCFail_def", thm "MClkReply_def", thm "Return_def", thm "e_def",
   1.136 -    thm "c_def", thm "r_def", thm "rtrner_def", thm "caller_def", thm "MVNROKBA_def",
   1.137 -    thm "S_def", thm "S4_def", thm "WrRequest_def", thm "Calling_def"]) [] [] 1 *})
   1.138 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm WriteInner_def},
   1.139 +    @{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm HNext_def}, @{thm MemReturn_def},
   1.140 +    @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
   1.141 +    @{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def}, @{thm MVNROKBA_def},
   1.142 +    @{thm S_def}, @{thm S4_def}, @{thm WrRequest_def}, @{thm Calling_def}]) [] [] 1 *})
   1.143  
   1.144  lemma S4Write: "|- Write rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
   1.145           & (HNext rmhist p)
   1.146 @@ -500,26 +500,26 @@
   1.147  
   1.148  lemma S5Reply: "|- RPCReply crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
   1.149         --> (S6 rmhist p)$"
   1.150 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCReply_def",
   1.151 -    thm "Return_def", thm "e_def", thm "c_def", thm "m_def", thm "MVOKBA_def",
   1.152 -    thm "MVOKBARF_def", thm "caller_def", thm "rtrner_def", thm "S_def",
   1.153 -    thm "S5_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *})
   1.154 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCReply_def},
   1.155 +    @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, @{thm MVOKBA_def},
   1.156 +    @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
   1.157 +    @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
   1.158  
   1.159  lemma S5Fail: "|- RPCFail crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
   1.160           --> (S6 rmhist p)$"
   1.161 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCFail_def",
   1.162 -    thm "Return_def", thm "e_def", thm "c_def", thm "m_def",
   1.163 -    thm "MVOKBARF_def", thm "caller_def", thm "rtrner_def",
   1.164 -    thm "S_def", thm "S5_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *})
   1.165 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCFail_def},
   1.166 +    @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def},
   1.167 +    @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def},
   1.168 +    @{thm S_def}, @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
   1.169  
   1.170  lemma S5MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S5 rmhist p) --> unchanged (m p)"
   1.171    by (auto simp: S_def S5_def dest!: Memoryidle [temp_use])
   1.172  
   1.173  lemma S5Hist: "|- [HNext rmhist p]_(c p, r p, m p, rmhist!p) & $(S5 rmhist p)
   1.174           --> (rmhist!p)$ = $(rmhist!p)"
   1.175 -  by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "HNext_def",
   1.176 -    thm "MemReturn_def", thm "RPCFail_def", thm "MClkReply_def", thm "Return_def",
   1.177 -    thm "S_def", thm "S5_def"]) *})
   1.178 +  by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm HNext_def},
   1.179 +    @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def},
   1.180 +    @{thm S_def}, @{thm S5_def}]) *})
   1.181  
   1.182  (* ------------------------------ State S6 ---------------------------------------- *)
   1.183  
   1.184 @@ -533,18 +533,18 @@
   1.185  lemma S6Retry: "|- MClkRetry memCh crCh cst p & HNext rmhist p & $S6 rmhist p
   1.186           & unchanged (e p,r p,m p)
   1.187           --> (S3 rmhist p)$ & unchanged (rmhist!p)"
   1.188 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def",
   1.189 -    thm "MClkReply_def", thm "MClkRetry_def", thm "Call_def", thm "Return_def",
   1.190 -    thm "e_def", thm "r_def", thm "m_def", thm "caller_def", thm "rtrner_def",
   1.191 -    thm "S_def", thm "S6_def", thm "S3_def", thm "Calling_def"]) [] [] 1 *})
   1.192 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def},
   1.193 +    @{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm Call_def}, @{thm Return_def},
   1.194 +    @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
   1.195 +    @{thm S_def}, @{thm S6_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1 *})
   1.196  
   1.197  lemma S6Reply: "|- MClkReply memCh crCh cst p & HNext rmhist p & $S6 rmhist p
   1.198           & unchanged (e p,r p,m p)
   1.199           --> (S1 rmhist p)$"
   1.200 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def",
   1.201 -    thm "MemReturn_def", thm "RPCFail_def", thm "Return_def", thm "MClkReply_def",
   1.202 -    thm "e_def", thm "r_def", thm "m_def", thm "caller_def", thm "rtrner_def",
   1.203 -    thm "S_def", thm "S6_def", thm "S1_def", thm "Calling_def"]) [] [] 1 *})
   1.204 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def},
   1.205 +    @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm Return_def}, @{thm MClkReply_def},
   1.206 +    @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
   1.207 +    @{thm S_def}, @{thm S6_def}, @{thm S1_def}, @{thm Calling_def}]) [] [] 1 *})
   1.208  
   1.209  lemma S6RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $S6 rmhist p --> unchanged (r p)"
   1.210    by (auto simp: S_def S6_def dest!: RPCidle [temp_use])
   1.211 @@ -563,9 +563,9 @@
   1.212  (* The implementation's initial condition implies the state predicate S1 *)
   1.213  
   1.214  lemma Step1_1: "|- ImpInit p & HInit rmhist p --> S1 rmhist p"
   1.215 -  by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "MVNROKBA_def",
   1.216 -    thm "MClkInit_def", thm "RPCInit_def", thm "PInit_def", thm "HInit_def",
   1.217 -    thm "ImpInit_def", thm "S_def", thm "S1_def"]) *})
   1.218 +  by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm MVNROKBA_def},
   1.219 +    @{thm MClkInit_def}, @{thm RPCInit_def}, @{thm PInit_def}, @{thm HInit_def},
   1.220 +    @{thm ImpInit_def}, @{thm S_def}, @{thm S1_def}]) *})
   1.221  
   1.222  (* ========== Step 1.2 ================================================== *)
   1.223  (* Figure 16 is a predicate-action diagram for the implementation. *)
   1.224 @@ -573,29 +573,29 @@
   1.225  lemma Step1_2_1: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
   1.226           & ~unchanged (e p, c p, r p, m p, rmhist!p)  & $S1 rmhist p
   1.227           --> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"
   1.228 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
   1.229 -      (map temp_elim [thm "S1ClerkUnch", thm "S1RPCUnch", thm "S1MemUnch", thm "S1Hist"]) 1 *})
   1.230 -   apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use (thm "S1Env")]) *})
   1.231 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
   1.232 +      (map temp_elim [@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1 *})
   1.233 +   apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use @{thm S1Env}]) *})
   1.234    done
   1.235  
   1.236  lemma Step1_2_2: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
   1.237           & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p
   1.238           --> (S3 rmhist p)$ & MClkFwd memCh crCh cst p
   1.239               & unchanged (e p, r p, m p, rmhist!p)"
   1.240 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
   1.241 -    (map temp_elim [thm "S2EnvUnch", thm "S2RPCUnch", thm "S2MemUnch", thm "S2Hist"]) 1 *})
   1.242 -   apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use (thm "S2Clerk"),
   1.243 -     temp_use (thm "S2Forward")]) *})
   1.244 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
   1.245 +    (map temp_elim [@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1 *})
   1.246 +   apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use @{thm S2Clerk},
   1.247 +     temp_use @{thm S2Forward}]) *})
   1.248    done
   1.249  
   1.250  lemma Step1_2_3: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
   1.251           & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p
   1.252           --> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p))
   1.253               | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
   1.254 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
   1.255 -    (map temp_elim [thm "S3EnvUnch", thm "S3ClerkUnch", thm "S3MemUnch"]) 1 *})
   1.256 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
   1.257 +    (map temp_elim [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1 *})
   1.258    apply (tactic {* action_simp_tac @{simpset} []
   1.259 -    (thm "squareE" :: map temp_elim [thm "S3RPC", thm "S3Forward", thm "S3Fail"]) 1 *})
   1.260 +    (@{thm squareE} :: map temp_elim [@{thm S3RPC}, @{thm S3Forward}, @{thm S3Fail}]) 1 *})
   1.261     apply (auto dest!: S3Hist [temp_use])
   1.262    done
   1.263  
   1.264 @@ -605,10 +605,10 @@
   1.265           --> ((S4 rmhist p)$ & Read rmCh mm ires p & unchanged (e p, c p, r p, rmhist!p))
   1.266               | ((S4 rmhist p)$ & (? l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p))
   1.267               | ((S5 rmhist p)$ & MemReturn rmCh ires p & unchanged (e p, c p, r p))"
   1.268 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
   1.269 -    (map temp_elim [thm "S4EnvUnch", thm "S4ClerkUnch", thm "S4RPCUnch"]) 1 *})
   1.270 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "RNext_def"]) []
   1.271 -    (thm "squareE" :: map temp_elim [thm "S4Read", thm "S4Write", thm "S4Return"]) 1 *})
   1.272 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
   1.273 +    (map temp_elim [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
   1.274 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RNext_def}]) []
   1.275 +    (@{thm squareE} :: map temp_elim [@{thm S4Read}, @{thm S4Write}, @{thm S4Return}]) 1 *})
   1.276    apply (auto dest!: S4Hist [temp_use])
   1.277    done
   1.278  
   1.279 @@ -616,21 +616,21 @@
   1.280                & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p
   1.281           --> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p))
   1.282               | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
   1.283 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
   1.284 -    (map temp_elim [thm "S5EnvUnch", thm "S5ClerkUnch", thm "S5MemUnch", thm "S5Hist"]) 1 *})
   1.285 -  apply (tactic {* action_simp_tac @{simpset} [] [thm "squareE", temp_elim (thm "S5RPC")] 1 *})
   1.286 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
   1.287 +    (map temp_elim [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1 *})
   1.288 +  apply (tactic {* action_simp_tac @{simpset} [] [@{thm squareE}, temp_elim @{thm S5RPC}] 1 *})
   1.289     apply (tactic {* auto_tac (MI_fast_css addSDs2
   1.290 -     [temp_use (thm "S5Reply"), temp_use (thm "S5Fail")]) *})
   1.291 +     [temp_use @{thm S5Reply}, temp_use @{thm S5Fail}]) *})
   1.292    done
   1.293  
   1.294  lemma Step1_2_6: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
   1.295                & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p
   1.296           --> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p))
   1.297               | ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))"
   1.298 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
   1.299 -    (map temp_elim [thm "S6EnvUnch", thm "S6RPCUnch", thm "S6MemUnch"]) 1 *})
   1.300 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
   1.301 +    (map temp_elim [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1 *})
   1.302    apply (tactic {* action_simp_tac @{simpset} []
   1.303 -    (thm "squareE" :: map temp_elim [thm "S6Clerk", thm "S6Retry", thm "S6Reply"]) 1 *})
   1.304 +    (@{thm squareE} :: map temp_elim [@{thm S6Clerk}, @{thm S6Retry}, @{thm S6Reply}]) 1 *})
   1.305       apply (auto dest: S6Hist [temp_use])
   1.306    done
   1.307  
   1.308 @@ -641,8 +641,8 @@
   1.309  section "Initialization (Step 1.3)"
   1.310  
   1.311  lemma Step1_3: "|- S1 rmhist p --> PInit (resbar rmhist) p"
   1.312 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "resbar_def",
   1.313 -    thm "PInit_def", thm "S_def", thm "S1_def"]) [] [] 1 *})
   1.314 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm resbar_def},
   1.315 +    @{thm PInit_def}, @{thm S_def}, @{thm S1_def}]) [] [] 1 *})
   1.316  
   1.317  (* ----------------------------------------------------------------------
   1.318     Step 1.4: Implementation's next-state relation simulates specification's
   1.319 @@ -653,23 +653,23 @@
   1.320  
   1.321  lemma Step1_4_1: "|- ENext p & $S1 rmhist p & (S2 rmhist p)$ & unchanged (c p, r p, m p)
   1.322           --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   1.323 -  by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "c_def", thm "r_def",
   1.324 -    thm "m_def", thm "resbar_def"]) *})
   1.325 +  by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm c_def}, @{thm r_def},
   1.326 +    @{thm m_def}, @{thm resbar_def}]) *})
   1.327  
   1.328  lemma Step1_4_2: "|- MClkFwd memCh crCh cst p & $S2 rmhist p & (S3 rmhist p)$
   1.329           & unchanged (e p, r p, m p, rmhist!p)
   1.330           --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   1.331    by (tactic {* action_simp_tac
   1.332 -    (@{simpset} addsimps [thm "MClkFwd_def", thm "e_def", thm "r_def", thm "m_def",
   1.333 -    thm "resbar_def", thm "S_def", thm "S2_def", thm "S3_def"]) [] [] 1 *})
   1.334 +    (@{simpset} addsimps [@{thm MClkFwd_def}, @{thm e_def}, @{thm r_def}, @{thm m_def},
   1.335 +    @{thm resbar_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}]) [] [] 1 *})
   1.336  
   1.337  lemma Step1_4_3a: "|- RPCFwd crCh rmCh rst p & $S3 rmhist p & (S4 rmhist p)$
   1.338           & unchanged (e p, c p, m p, rmhist!p)
   1.339           --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   1.340    apply clarsimp
   1.341    apply (drule S3_excl [temp_use] S4_excl [temp_use])+
   1.342 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
   1.343 -    thm "c_def", thm "m_def", thm "resbar_def", thm "S_def", thm "S3_def"]) [] [] 1 *})
   1.344 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def},
   1.345 +    @{thm c_def}, @{thm m_def}, @{thm resbar_def}, @{thm S_def}, @{thm S3_def}]) [] [] 1 *})
   1.346    done
   1.347  
   1.348  lemma Step1_4_3b: "|- RPCFail crCh rmCh rst p & $S3 rmhist p & (S6 rmhist p)$
   1.349 @@ -687,13 +687,13 @@
   1.350           --> ReadInner memCh mm (resbar rmhist) p l"
   1.351    apply clarsimp
   1.352    apply (drule S4_excl [temp_use])+
   1.353 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ReadInner_def",
   1.354 -    thm "GoodRead_def", thm "BadRead_def", thm "e_def", thm "c_def", thm "m_def"]) [] [] 1 *})
   1.355 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ReadInner_def},
   1.356 +    @{thm GoodRead_def}, @{thm BadRead_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}]) [] [] 1 *})
   1.357       apply (auto simp: resbar_def)
   1.358         apply (tactic {* ALLGOALS (action_simp_tac
   1.359 -                (@{simpset} addsimps [thm "RPCRelayArg_def", thm "MClkRelayArg_def",
   1.360 -                  thm "S_def", thm "S4_def", thm "RdRequest_def", thm "MemInv_def"])
   1.361 -                [] [thm "impE", thm "MemValNotAResultE"]) *})
   1.362 +                (@{simpset} addsimps [@{thm RPCRelayArg_def}, @{thm MClkRelayArg_def},
   1.363 +                  @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def}, @{thm MemInv_def}])
   1.364 +                [] [@{thm impE}, @{thm MemValNotAResultE}]) *})
   1.365    done
   1.366  
   1.367  lemma Step1_4_4a: "|- Read rmCh mm ires p & $S4 rmhist p & (S4 rmhist p)$
   1.368 @@ -707,12 +707,12 @@
   1.369    apply clarsimp
   1.370    apply (drule S4_excl [temp_use])+
   1.371    apply (tactic {* action_simp_tac (@{simpset} addsimps
   1.372 -    [thm "WriteInner_def", thm "GoodWrite_def", thm "BadWrite_def", thm "e_def",
   1.373 -    thm "c_def", thm "m_def"]) [] [] 1 *})
   1.374 +    [@{thm WriteInner_def}, @{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm e_def},
   1.375 +    @{thm c_def}, @{thm m_def}]) [] [] 1 *})
   1.376       apply (auto simp: resbar_def)
   1.377      apply (tactic {* ALLGOALS (action_simp_tac (@{simpset} addsimps
   1.378 -      [thm "RPCRelayArg_def", thm "MClkRelayArg_def", thm "S_def",
   1.379 -      thm "S4_def", thm "WrRequest_def"]) [] []) *})
   1.380 +      [@{thm RPCRelayArg_def}, @{thm MClkRelayArg_def}, @{thm S_def},
   1.381 +      @{thm S4_def}, @{thm WrRequest_def}]) [] []) *})
   1.382    done
   1.383  
   1.384  lemma Step1_4_4b: "|- Write rmCh mm ires p l & $S4 rmhist p & (S4 rmhist p)$
   1.385 @@ -723,10 +723,10 @@
   1.386  lemma Step1_4_4c: "|- MemReturn rmCh ires p & $S4 rmhist p & (S5 rmhist p)$
   1.387           & unchanged (e p, c p, r p)
   1.388           --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   1.389 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
   1.390 -    thm "c_def", thm "r_def", thm "resbar_def"]) [] [] 1 *})
   1.391 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def},
   1.392 +    @{thm c_def}, @{thm r_def}, @{thm resbar_def}]) [] [] 1 *})
   1.393    apply (drule S4_excl [temp_use] S5_excl [temp_use])+
   1.394 -  apply (tactic {* auto_tac (MI_fast_css addsimps2 [thm "MemReturn_def", thm "Return_def"]) *})
   1.395 +  apply (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm MemReturn_def}, @{thm Return_def}]) *})
   1.396    done
   1.397  
   1.398  lemma Step1_4_5a: "|- RPCReply crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$
   1.399 @@ -752,12 +752,12 @@
   1.400           --> MemReturn memCh (resbar rmhist) p"
   1.401    apply clarsimp
   1.402    apply (drule S6_excl [temp_use])+
   1.403 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
   1.404 -    thm "r_def", thm "m_def", thm "MClkReply_def", thm "MemReturn_def",
   1.405 -    thm "Return_def", thm "resbar_def"]) [] [] 1 *})
   1.406 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def},
   1.407 +    @{thm r_def}, @{thm m_def}, @{thm MClkReply_def}, @{thm MemReturn_def},
   1.408 +    @{thm Return_def}, @{thm resbar_def}]) [] [] 1 *})
   1.409      apply simp_all (* simplify if-then-else *)
   1.410      apply (tactic {* ALLGOALS (action_simp_tac (@{simpset} addsimps
   1.411 -      [thm "MClkReplyVal_def", thm "S6_def", thm "S_def"]) [] [thm "MVOKBARFnotNR"]) *})
   1.412 +      [@{thm MClkReplyVal_def}, @{thm S6_def}, @{thm S_def}]) [] [@{thm MVOKBARFnotNR}]) *})
   1.413    done
   1.414  
   1.415  lemma Step1_4_6b: "|- MClkRetry memCh crCh cst p & $S6 rmhist p & (S3 rmhist p)$
   1.416 @@ -765,8 +765,8 @@
   1.417           --> MemFail memCh (resbar rmhist) p"
   1.418    apply clarsimp
   1.419    apply (drule S3_excl [temp_use])+
   1.420 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def", thm "r_def",
   1.421 -    thm "m_def", thm "MClkRetry_def", thm "MemFail_def", thm "resbar_def"]) [] [] 1 *})
   1.422 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def}, @{thm r_def},
   1.423 +    @{thm m_def}, @{thm MClkRetry_def}, @{thm MemFail_def}, @{thm resbar_def}]) [] [] 1 *})
   1.424     apply (auto simp: S6_def S_def)
   1.425    done
   1.426  
   1.427 @@ -816,7 +816,7 @@
   1.428  lemma unchanged_safe: "|- (~unchanged (e p, c p, r p, m p, rmhist!p)
   1.429               --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p))
   1.430           --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   1.431 -  apply (tactic {* split_idle_tac @{context} [thm "square_def"] 1 *})
   1.432 +  apply (tactic {* split_idle_tac @{context} [@{thm square_def}] 1 *})
   1.433    apply force
   1.434    done
   1.435  (* turn into (unsafe, looping!) introduction rule *)
   1.436 @@ -898,15 +898,15 @@
   1.437  
   1.438  lemma S1_RNextdisabled: "|- S1 rmhist p -->
   1.439           ~Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
   1.440 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def",
   1.441 -    thm "S_def", thm "S1_def"]) [notI] [thm "enabledE", temp_elim (thm "Memoryidle")] 1 *})
   1.442 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm angle_def},
   1.443 +    @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{thm Memoryidle}] 1 *})
   1.444    apply force
   1.445    done
   1.446  
   1.447  lemma S1_Returndisabled: "|- S1 rmhist p -->
   1.448           ~Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
   1.449 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def", thm "MemReturn_def",
   1.450 -    thm "Return_def", thm "S_def", thm "S1_def"]) [notI] [thm "enabledE"] 1 *})
   1.451 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm angle_def}, @{thm MemReturn_def},
   1.452 +    @{thm Return_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1 *})
   1.453  
   1.454  lemma RNext_fair: "|- []<>S1 rmhist p
   1.455           --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
   1.456 @@ -986,7 +986,7 @@
   1.457           & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l)
   1.458           --> (S4 rmhist p & ires!p = #NotAResult)$
   1.459               | ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$"
   1.460 -  apply (tactic {* split_idle_tac @{context} [thm "m_def"] 1 *})
   1.461 +  apply (tactic {* split_idle_tac @{context} [@{thm m_def}] 1 *})
   1.462    apply (auto dest!: Step1_2_4 [temp_use])
   1.463    done
   1.464  
   1.465 @@ -1017,7 +1017,7 @@
   1.466  lemma S4b_successors: "|- $(S4 rmhist p & ires!p ~= #NotAResult)
   1.467           & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l)
   1.468           --> (S4 rmhist p & ires!p ~= #NotAResult)$ | (S5 rmhist p)$"
   1.469 -  apply (tactic {* split_idle_tac @{context} [thm "m_def"] 1 *})
   1.470 +  apply (tactic {* split_idle_tac @{context} [@{thm m_def}] 1 *})
   1.471    apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use])
   1.472    done
   1.473  
   1.474 @@ -1084,16 +1084,16 @@
   1.475  
   1.476  lemma MClkReplyS6:
   1.477    "|- $ImpInv rmhist p & <MClkReply memCh crCh cst p>_(c p) --> $S6 rmhist p"
   1.478 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def",
   1.479 -    thm "MClkReply_def", thm "Return_def", thm "ImpInv_def", thm "S_def",
   1.480 -    thm "S1_def", thm "S2_def", thm "S3_def", thm "S4_def", thm "S5_def"]) [] [] 1 *})
   1.481 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm angle_def},
   1.482 +    @{thm MClkReply_def}, @{thm Return_def}, @{thm ImpInv_def}, @{thm S_def},
   1.483 +    @{thm S1_def}, @{thm S2_def}, @{thm S3_def}, @{thm S4_def}, @{thm S5_def}]) [] [] 1 *})
   1.484  
   1.485  lemma S6MClkReply_enabled: "|- S6 rmhist p --> Enabled (<MClkReply memCh crCh cst p>_(c p))"
   1.486    apply (auto simp: c_def intro!: MClkReply_enabled [temp_use])
   1.487       apply (cut_tac MI_base)
   1.488       apply (blast dest: base_pair)
   1.489      apply (tactic {* ALLGOALS (action_simp_tac (@{simpset}
   1.490 -      addsimps [thm "S_def", thm "S6_def"]) [] []) *})
   1.491 +      addsimps [@{thm S_def}, @{thm S6_def}]) [] []) *})
   1.492    done
   1.493  
   1.494  lemma S6_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & $(ImpInv rmhist p))
   1.495 @@ -1104,7 +1104,7 @@
   1.496     apply (erule InfiniteEnsures)
   1.497      apply assumption
   1.498     apply (tactic {* action_simp_tac @{simpset} []
   1.499 -     (map temp_elim [thm "MClkReplyS6", thm "S6MClkReply_successors"]) 1 *})
   1.500 +     (map temp_elim [@{thm MClkReplyS6}, @{thm S6MClkReply_successors}]) 1 *})
   1.501    apply (auto simp: SF_def)
   1.502    apply (erule contrapos_np)
   1.503    apply (auto intro!: S6MClkReply_enabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use])
   1.504 @@ -1191,7 +1191,7 @@
   1.505        ==> sigma |= []<>S1 rmhist p"
   1.506    apply (rule classical)
   1.507    apply (tactic {* asm_lr_simp_tac (@{simpset} addsimps
   1.508 -    [temp_use (thm "NotBox"), temp_rewrite (thm "NotDmd")]) 1 *})
   1.509 +    [temp_use @{thm NotBox}, temp_rewrite @{thm NotDmd}]) 1 *})
   1.510    apply (auto elim!: leadsto_infinite [temp_use] mp dest!: DBImplBD [temp_use])
   1.511    done
   1.512