src/HOL/TLA/Memory/MemoryImplementation.thy
changeset 51717 9e7d1c139569
parent 45605 a89b4bc311a5
child 54742 7a86358a3c0b
     1.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -225,13 +225,13 @@
     1.4  *)
     1.5  ML {*
     1.6    val config_fast_solver = Attrib.setup_config_bool @{binding fast_solver} (K false);
     1.7 -  val fast_solver = mk_solver "fast_solver" (fn ss =>
     1.8 -    if Config.get (Simplifier.the_context ss) config_fast_solver
     1.9 +  val fast_solver = mk_solver "fast_solver" (fn ctxt =>
    1.10 +    if Config.get ctxt config_fast_solver
    1.11      then assume_tac ORELSE' (etac notE)
    1.12      else K no_tac);
    1.13  *}
    1.14  
    1.15 -declaration {* K (Simplifier.map_ss (fn ss => ss addSSolver fast_solver)) *}
    1.16 +setup {* map_theory_simpset (fn ctxt => ctxt addSSolver fast_solver) *}
    1.17  
    1.18  ML {* val temp_elim = make_elim o temp_use *}
    1.19  
    1.20 @@ -248,9 +248,9 @@
    1.21    apply (rule historyI)
    1.22        apply assumption+
    1.23    apply (rule MI_base)
    1.24 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HInit_def}]) [] [] 1 *})
    1.25 +  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm HInit_def}]) [] [] 1 *})
    1.26     apply (erule fun_cong)
    1.27 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def}])
    1.28 +  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def}])
    1.29      [@{thm busy_squareI}] [] 1 *})
    1.30    apply (erule fun_cong)
    1.31    done
    1.32 @@ -350,7 +350,7 @@
    1.33  
    1.34  lemma S1Hist: "|- [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S1 rmhist p)
    1.35           --> unchanged (rmhist!p)"
    1.36 -  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def}, @{thm S_def},
    1.37 +  by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def}, @{thm S_def},
    1.38      @{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def},
    1.39      @{thm Return_def}]) [] [temp_use @{thm squareE}] 1 *})
    1.40  
    1.41 @@ -366,7 +366,7 @@
    1.42  lemma S2Forward: "|- $(S2 rmhist p) & MClkFwd memCh crCh cst p
    1.43           & unchanged (e p, r p, m p, rmhist!p)
    1.44           --> (S3 rmhist p)$"
    1.45 -  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm MClkFwd_def},
    1.46 +  by (tactic {* action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
    1.47      @{thm Call_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def},
    1.48      @{thm rtrner_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1 *})
    1.49  
    1.50 @@ -403,7 +403,7 @@
    1.51  lemma S3Forward: "|- RPCFwd crCh rmCh rst p & HNext rmhist p & $(S3 rmhist p)
    1.52           & unchanged (e p, c p, m p)
    1.53           --> (S4 rmhist p)$ & unchanged (rmhist!p)"
    1.54 -  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCFwd_def},
    1.55 +  by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCFwd_def},
    1.56      @{thm HNext_def}, @{thm MemReturn_def}, @{thm RPCFail_def},
    1.57      @{thm MClkReply_def}, @{thm Return_def}, @{thm Call_def}, @{thm e_def},
    1.58      @{thm c_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
    1.59 @@ -412,7 +412,7 @@
    1.60  lemma S3Fail: "|- RPCFail crCh rmCh rst p & $(S3 rmhist p) & HNext rmhist p
    1.61           & unchanged (e p, c p, m p)
    1.62           --> (S6 rmhist p)$"
    1.63 -  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def},
    1.64 +  by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def},
    1.65      @{thm RPCFail_def}, @{thm Return_def}, @{thm e_def}, @{thm c_def},
    1.66      @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm MVOKBARF_def},
    1.67      @{thm S_def}, @{thm S3_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
    1.68 @@ -439,7 +439,7 @@
    1.69  lemma S4ReadInner: "|- ReadInner rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
    1.70           & HNext rmhist p & $(MemInv mm l)
    1.71           --> (S4 rmhist p)$ & unchanged (rmhist!p)"
    1.72 -  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ReadInner_def},
    1.73 +  by (tactic {* action_simp_tac (@{context} addsimps [@{thm ReadInner_def},
    1.74      @{thm GoodRead_def}, @{thm BadRead_def}, @{thm HNext_def}, @{thm MemReturn_def},
    1.75      @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
    1.76      @{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def},
    1.77 @@ -453,7 +453,7 @@
    1.78  
    1.79  lemma S4WriteInner: "|- WriteInner rmCh mm ires p l v & $(S4 rmhist p) & unchanged (e p, c p, r p)           & HNext rmhist p
    1.80           --> (S4 rmhist p)$ & unchanged (rmhist!p)"
    1.81 -  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm WriteInner_def},
    1.82 +  by (tactic {* action_simp_tac (@{context} addsimps [@{thm WriteInner_def},
    1.83      @{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm HNext_def}, @{thm MemReturn_def},
    1.84      @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
    1.85      @{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def}, @{thm MVNROKBA_def},
    1.86 @@ -492,14 +492,14 @@
    1.87  
    1.88  lemma S5Reply: "|- RPCReply crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
    1.89         --> (S6 rmhist p)$"
    1.90 -  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCReply_def},
    1.91 +  by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
    1.92      @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, @{thm MVOKBA_def},
    1.93      @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
    1.94      @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
    1.95  
    1.96  lemma S5Fail: "|- RPCFail crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
    1.97           --> (S6 rmhist p)$"
    1.98 -  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCFail_def},
    1.99 +  by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
   1.100      @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def},
   1.101      @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def},
   1.102      @{thm S_def}, @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
   1.103 @@ -525,7 +525,7 @@
   1.104  lemma S6Retry: "|- MClkRetry memCh crCh cst p & HNext rmhist p & $S6 rmhist p
   1.105           & unchanged (e p,r p,m p)
   1.106           --> (S3 rmhist p)$ & unchanged (rmhist!p)"
   1.107 -  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def},
   1.108 +  by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def},
   1.109      @{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm Call_def}, @{thm Return_def},
   1.110      @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
   1.111      @{thm S_def}, @{thm S6_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1 *})
   1.112 @@ -533,7 +533,7 @@
   1.113  lemma S6Reply: "|- MClkReply memCh crCh cst p & HNext rmhist p & $S6 rmhist p
   1.114           & unchanged (e p,r p,m p)
   1.115           --> (S1 rmhist p)$"
   1.116 -  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def},
   1.117 +  by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def},
   1.118      @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm Return_def}, @{thm MClkReply_def},
   1.119      @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
   1.120      @{thm S_def}, @{thm S6_def}, @{thm S1_def}, @{thm Calling_def}]) [] [] 1 *})
   1.121 @@ -565,7 +565,7 @@
   1.122  lemma Step1_2_1: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
   1.123           & ~unchanged (e p, c p, r p, m p, rmhist!p)  & $S1 rmhist p
   1.124           --> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"
   1.125 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
   1.126 +  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
   1.127        (map temp_elim [@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1 *})
   1.128     using [[fast_solver]]
   1.129     apply (auto elim!: squareE [temp_use] intro!: S1Env [temp_use])
   1.130 @@ -575,7 +575,7 @@
   1.131           & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p
   1.132           --> (S3 rmhist p)$ & MClkFwd memCh crCh cst p
   1.133               & unchanged (e p, r p, m p, rmhist!p)"
   1.134 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
   1.135 +  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
   1.136      (map temp_elim [@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1 *})
   1.137     using [[fast_solver]]
   1.138     apply (auto elim!: squareE [temp_use] intro!: S2Clerk [temp_use] S2Forward [temp_use])
   1.139 @@ -585,9 +585,9 @@
   1.140           & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p
   1.141           --> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p))
   1.142               | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
   1.143 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
   1.144 +  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
   1.145      (map temp_elim [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1 *})
   1.146 -  apply (tactic {* action_simp_tac @{simpset} []
   1.147 +  apply (tactic {* action_simp_tac @{context} []
   1.148      (@{thm squareE} :: map temp_elim [@{thm S3RPC}, @{thm S3Forward}, @{thm S3Fail}]) 1 *})
   1.149     apply (auto dest!: S3Hist [temp_use])
   1.150    done
   1.151 @@ -598,9 +598,9 @@
   1.152           --> ((S4 rmhist p)$ & Read rmCh mm ires p & unchanged (e p, c p, r p, rmhist!p))
   1.153               | ((S4 rmhist p)$ & (? l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p))
   1.154               | ((S5 rmhist p)$ & MemReturn rmCh ires p & unchanged (e p, c p, r p))"
   1.155 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
   1.156 +  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
   1.157      (map temp_elim [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
   1.158 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RNext_def}]) []
   1.159 +  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm RNext_def}]) []
   1.160      (@{thm squareE} :: map temp_elim [@{thm S4Read}, @{thm S4Write}, @{thm S4Return}]) 1 *})
   1.161    apply (auto dest!: S4Hist [temp_use])
   1.162    done
   1.163 @@ -609,9 +609,9 @@
   1.164                & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p
   1.165           --> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p))
   1.166               | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
   1.167 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
   1.168 +  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
   1.169      (map temp_elim [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1 *})
   1.170 -  apply (tactic {* action_simp_tac @{simpset} [] [@{thm squareE}, temp_elim @{thm S5RPC}] 1 *})
   1.171 +  apply (tactic {* action_simp_tac @{context} [] [@{thm squareE}, temp_elim @{thm S5RPC}] 1 *})
   1.172     using [[fast_solver]]
   1.173     apply (auto elim!: squareE [temp_use] dest!: S5Reply [temp_use] S5Fail [temp_use])
   1.174    done
   1.175 @@ -620,9 +620,9 @@
   1.176                & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p
   1.177           --> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p))
   1.178               | ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))"
   1.179 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
   1.180 +  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
   1.181      (map temp_elim [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1 *})
   1.182 -  apply (tactic {* action_simp_tac @{simpset} []
   1.183 +  apply (tactic {* action_simp_tac @{context} []
   1.184      (@{thm squareE} :: map temp_elim [@{thm S6Clerk}, @{thm S6Retry}, @{thm S6Reply}]) 1 *})
   1.185       apply (auto dest: S6Hist [temp_use])
   1.186    done
   1.187 @@ -634,7 +634,7 @@
   1.188  section "Initialization (Step 1.3)"
   1.189  
   1.190  lemma Step1_3: "|- S1 rmhist p --> PInit (resbar rmhist) p"
   1.191 -  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm resbar_def},
   1.192 +  by (tactic {* action_simp_tac (@{context} addsimps [@{thm resbar_def},
   1.193      @{thm PInit_def}, @{thm S_def}, @{thm S1_def}]) [] [] 1 *})
   1.194  
   1.195  (* ----------------------------------------------------------------------
   1.196 @@ -653,7 +653,7 @@
   1.197           & unchanged (e p, r p, m p, rmhist!p)
   1.198           --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   1.199    by (tactic {* action_simp_tac
   1.200 -    (@{simpset} addsimps [@{thm MClkFwd_def}, @{thm e_def}, @{thm r_def}, @{thm m_def},
   1.201 +    (@{context} addsimps [@{thm MClkFwd_def}, @{thm e_def}, @{thm r_def}, @{thm m_def},
   1.202      @{thm resbar_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}]) [] [] 1 *})
   1.203  
   1.204  lemma Step1_4_3a: "|- RPCFwd crCh rmCh rst p & $S3 rmhist p & (S4 rmhist p)$
   1.205 @@ -661,7 +661,7 @@
   1.206           --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   1.207    apply clarsimp
   1.208    apply (drule S3_excl [temp_use] S4_excl [temp_use])+
   1.209 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def},
   1.210 +  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm e_def},
   1.211      @{thm c_def}, @{thm m_def}, @{thm resbar_def}, @{thm S_def}, @{thm S3_def}]) [] [] 1 *})
   1.212    done
   1.213  
   1.214 @@ -680,11 +680,11 @@
   1.215           --> ReadInner memCh mm (resbar rmhist) p l"
   1.216    apply clarsimp
   1.217    apply (drule S4_excl [temp_use])+
   1.218 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ReadInner_def},
   1.219 +  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ReadInner_def},
   1.220      @{thm GoodRead_def}, @{thm BadRead_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}]) [] [] 1 *})
   1.221       apply (auto simp: resbar_def)
   1.222         apply (tactic {* ALLGOALS (action_simp_tac
   1.223 -                (@{simpset} addsimps [@{thm RPCRelayArg_def}, @{thm MClkRelayArg_def},
   1.224 +                (@{context} addsimps [@{thm RPCRelayArg_def}, @{thm MClkRelayArg_def},
   1.225                    @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def}, @{thm MemInv_def}])
   1.226                  [] [@{thm impE}, @{thm MemValNotAResultE}]) *})
   1.227    done
   1.228 @@ -699,11 +699,11 @@
   1.229           --> WriteInner memCh mm (resbar rmhist) p l v"
   1.230    apply clarsimp
   1.231    apply (drule S4_excl [temp_use])+
   1.232 -  apply (tactic {* action_simp_tac (@{simpset} addsimps
   1.233 +  apply (tactic {* action_simp_tac (@{context} addsimps
   1.234      [@{thm WriteInner_def}, @{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm e_def},
   1.235      @{thm c_def}, @{thm m_def}]) [] [] 1 *})
   1.236       apply (auto simp: resbar_def)
   1.237 -    apply (tactic {* ALLGOALS (action_simp_tac (@{simpset} addsimps
   1.238 +    apply (tactic {* ALLGOALS (action_simp_tac (@{context} addsimps
   1.239        [@{thm RPCRelayArg_def}, @{thm MClkRelayArg_def}, @{thm S_def},
   1.240        @{thm S4_def}, @{thm WrRequest_def}]) [] []) *})
   1.241    done
   1.242 @@ -716,7 +716,7 @@
   1.243  lemma Step1_4_4c: "|- MemReturn rmCh ires p & $S4 rmhist p & (S5 rmhist p)$
   1.244           & unchanged (e p, c p, r p)
   1.245           --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   1.246 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def},
   1.247 +  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm e_def},
   1.248      @{thm c_def}, @{thm r_def}, @{thm resbar_def}]) [] [] 1 *})
   1.249    apply (drule S4_excl [temp_use] S5_excl [temp_use])+
   1.250    using [[fast_solver]]
   1.251 @@ -746,11 +746,11 @@
   1.252           --> MemReturn memCh (resbar rmhist) p"
   1.253    apply clarsimp
   1.254    apply (drule S6_excl [temp_use])+
   1.255 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def},
   1.256 +  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm e_def},
   1.257      @{thm r_def}, @{thm m_def}, @{thm MClkReply_def}, @{thm MemReturn_def},
   1.258      @{thm Return_def}, @{thm resbar_def}]) [] [] 1 *})
   1.259      apply simp_all (* simplify if-then-else *)
   1.260 -    apply (tactic {* ALLGOALS (action_simp_tac (@{simpset} addsimps
   1.261 +    apply (tactic {* ALLGOALS (action_simp_tac (@{context} addsimps
   1.262        [@{thm MClkReplyVal_def}, @{thm S6_def}, @{thm S_def}]) [] [@{thm MVOKBARFnotNR}]) *})
   1.263    done
   1.264  
   1.265 @@ -759,7 +759,7 @@
   1.266           --> MemFail memCh (resbar rmhist) p"
   1.267    apply clarsimp
   1.268    apply (drule S3_excl [temp_use])+
   1.269 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def}, @{thm r_def},
   1.270 +  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm e_def}, @{thm r_def},
   1.271      @{thm m_def}, @{thm MClkRetry_def}, @{thm MemFail_def}, @{thm resbar_def}]) [] [] 1 *})
   1.272     apply (auto simp: S6_def S_def)
   1.273    done
   1.274 @@ -797,7 +797,7 @@
   1.275      Induct_Tacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" 1 THEN
   1.276      rewrite_goals_tac @{thms action_rews} THEN
   1.277      forward_tac [temp_use @{thm Step1_4_7}] 1 THEN
   1.278 -    asm_full_simp_tac (simpset_of ctxt) 1);
   1.279 +    asm_full_simp_tac ctxt 1);
   1.280  *}
   1.281  
   1.282  method_setup split_idle = {*
   1.283 @@ -897,14 +897,14 @@
   1.284  
   1.285  lemma S1_RNextdisabled: "|- S1 rmhist p -->
   1.286           ~Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
   1.287 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm angle_def},
   1.288 +  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def},
   1.289      @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{thm Memoryidle}] 1 *})
   1.290    apply force
   1.291    done
   1.292  
   1.293  lemma S1_Returndisabled: "|- S1 rmhist p -->
   1.294           ~Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
   1.295 -  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm angle_def}, @{thm MemReturn_def},
   1.296 +  by (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def}, @{thm MemReturn_def},
   1.297      @{thm Return_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1 *})
   1.298  
   1.299  lemma RNext_fair: "|- []<>S1 rmhist p
   1.300 @@ -1083,7 +1083,7 @@
   1.301  
   1.302  lemma MClkReplyS6:
   1.303    "|- $ImpInv rmhist p & <MClkReply memCh crCh cst p>_(c p) --> $S6 rmhist p"
   1.304 -  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm angle_def},
   1.305 +  by (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def},
   1.306      @{thm MClkReply_def}, @{thm Return_def}, @{thm ImpInv_def}, @{thm S_def},
   1.307      @{thm S1_def}, @{thm S2_def}, @{thm S3_def}, @{thm S4_def}, @{thm S5_def}]) [] [] 1 *})
   1.308  
   1.309 @@ -1091,7 +1091,7 @@
   1.310    apply (auto simp: c_def intro!: MClkReply_enabled [temp_use])
   1.311       apply (cut_tac MI_base)
   1.312       apply (blast dest: base_pair)
   1.313 -    apply (tactic {* ALLGOALS (action_simp_tac (@{simpset}
   1.314 +    apply (tactic {* ALLGOALS (action_simp_tac (@{context}
   1.315        addsimps [@{thm S_def}, @{thm S6_def}]) [] []) *})
   1.316    done
   1.317  
   1.318 @@ -1102,7 +1102,7 @@
   1.319    apply (subgoal_tac "sigma |= []<> (<MClkReply memCh crCh cst p>_ (c p))")
   1.320     apply (erule InfiniteEnsures)
   1.321      apply assumption
   1.322 -   apply (tactic {* action_simp_tac @{simpset} []
   1.323 +   apply (tactic {* action_simp_tac @{context} []
   1.324       (map temp_elim [@{thm MClkReplyS6}, @{thm S6MClkReply_successors}]) 1 *})
   1.325    apply (auto simp: SF_def)
   1.326    apply (erule contrapos_np)
   1.327 @@ -1189,7 +1189,7 @@
   1.328           sigma |= []<>S6 rmhist p --> []<>S1 rmhist p |]
   1.329        ==> sigma |= []<>S1 rmhist p"
   1.330    apply (rule classical)
   1.331 -  apply (tactic {* asm_lr_simp_tac (@{simpset} addsimps
   1.332 +  apply (tactic {* asm_lr_simp_tac (@{context} addsimps
   1.333      [temp_use @{thm NotBox}, temp_rewrite @{thm NotDmd}]) 1 *})
   1.334    apply (auto elim!: leadsto_infinite [temp_use] mp dest!: DBImplBD [temp_use])
   1.335    done