--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Wed Mar 19 22:50:42 2008 +0100
@@ -220,9 +220,9 @@
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"])
+ apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def"])
[thm "busy_squareI"] [] 1 *})
apply (erule fun_cong)
done
@@ -324,7 +324,7 @@
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",
+ 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 *})
@@ -340,7 +340,7 @@
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",
+ 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 *})
@@ -376,7 +376,7 @@
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",
+ 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",
@@ -385,7 +385,7 @@
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",
+ 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 *})
@@ -412,7 +412,7 @@
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",
+ 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",
@@ -426,7 +426,7 @@
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",
+ 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",
@@ -465,14 +465,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 (simpset () addsimps [thm "RPCReply_def",
+ 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",
+ 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 *})
@@ -498,7 +498,7 @@
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",
+ 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 *})
@@ -506,7 +506,7 @@
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",
+ 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 *})
@@ -538,7 +538,7 @@
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"]) []
+ 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
@@ -547,7 +547,7 @@
& ~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"]) []
+ 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")]) *})
@@ -557,9 +557,9 @@
& ~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"]) []
+ 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()) []
+ apply (tactic {* action_simp_tac @{simpset} []
(thm "squareE" :: map temp_elim [thm "S3RPC", thm "S3Forward", thm "S3Fail"]) 1 *})
apply (auto dest!: S3Hist [temp_use])
done
@@ -570,9 +570,9 @@
--> ((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"]) []
+ 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"]) []
+ 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
@@ -581,9 +581,9 @@
& ~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"]) []
+ 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} [] [thm "squareE", temp_elim (thm "S5RPC")] 1 *})
apply (tactic {* auto_tac (MI_fast_css addSDs2
[temp_use (thm "S5Reply"), temp_use (thm "S5Fail")]) *})
done
@@ -592,9 +592,9 @@
& ~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"]) []
+ 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()) []
+ apply (tactic {* action_simp_tac @{simpset} []
(thm "squareE" :: map temp_elim [thm "S6Clerk", thm "S6Retry", thm "S6Reply"]) 1 *})
apply (auto dest: S6Hist [temp_use])
done
@@ -606,7 +606,7 @@
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",
+ by (tactic {* action_simp_tac (@{simpset} addsimps [thm "resbar_def",
thm "PInit_def", thm "S_def", thm "S1_def"]) [] [] 1 *})
(* ----------------------------------------------------------------------
@@ -625,7 +625,7 @@
& 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",
+ (@{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)$
@@ -633,7 +633,7 @@
--> 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",
+ 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
@@ -652,11 +652,11 @@
--> 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",
+ 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",
+ (@{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
@@ -671,11 +671,11 @@
--> WriteInner memCh mm (resbar rmhist) p l v"
apply clarsimp
apply (drule S4_excl [temp_use])+
- apply (tactic {* action_simp_tac (simpset () addsimps
+ 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 *})
apply (auto simp: resbar_def)
- apply (tactic {* ALLGOALS (action_simp_tac (simpset () addsimps
+ apply (tactic {* ALLGOALS (action_simp_tac (@{simpset} addsimps
[thm "RPCRelayArg_def", thm "MClkRelayArg_def", thm "S_def",
thm "S4_def", thm "WrRequest_def"]) [] []) *})
done
@@ -688,7 +688,7 @@
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",
+ 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"]) *})
@@ -717,11 +717,11 @@
--> MemReturn memCh (resbar rmhist) p"
apply clarsimp
apply (drule S6_excl [temp_use])+
- apply (tactic {* action_simp_tac (simpset () addsimps [thm "e_def",
+ 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
+ apply (tactic {* ALLGOALS (action_simp_tac (@{simpset} addsimps
[thm "MClkReplyVal_def", thm "S6_def", thm "S_def"]) [] [thm "MVOKBARFnotNR"]) *})
done
@@ -730,7 +730,7 @@
--> 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",
+ 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
@@ -862,14 +862,14 @@
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",
+ 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",
+ 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
@@ -1048,7 +1048,7 @@
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",
+ 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 *})
@@ -1056,7 +1056,7 @@
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 ()
+ apply (tactic {* ALLGOALS (action_simp_tac (@{simpset}
addsimps [thm "S_def", thm "S6_def"]) [] []) *})
done
@@ -1067,7 +1067,7 @@
apply (subgoal_tac "sigma |= []<> (<MClkReply memCh crCh cst p>_ (c p))")
apply (erule InfiniteEnsures)
apply assumption
- apply (tactic {* action_simp_tac (simpset()) []
+ apply (tactic {* action_simp_tac @{simpset} []
(map temp_elim [thm "MClkReplyS6", thm "S6MClkReply_successors"]) 1 *})
apply (auto simp: SF_def)
apply (erule contrapos_np)
@@ -1154,7 +1154,7 @@
sigma |= []<>S6 rmhist p --> []<>S1 rmhist p |]
==> sigma |= []<>S1 rmhist p"
apply (rule classical)
- apply (tactic {* asm_lr_simp_tac (simpset() addsimps
+ apply (tactic {* asm_lr_simp_tac (@{simpset} addsimps
[temp_use (thm "NotBox"), temp_rewrite (thm "NotDmd")]) 1 *})
apply (auto elim!: leadsto_infinite [temp_use] mp dest!: DBImplBD [temp_use])
done