src/HOL/TLA/Memory/MemoryImplementation.thy
changeset 54742 7a86358a3c0b
parent 51717 9e7d1c139569
child 58249 180f1b3508ed
     1.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -233,7 +233,7 @@
     1.4  
     1.5  setup {* map_theory_simpset (fn ctxt => ctxt addSSolver fast_solver) *}
     1.6  
     1.7 -ML {* val temp_elim = make_elim o temp_use *}
     1.8 +ML {* val temp_elim = make_elim oo temp_use *}
     1.9  
    1.10  
    1.11  
    1.12 @@ -352,7 +352,7 @@
    1.13           --> unchanged (rmhist!p)"
    1.14    by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def}, @{thm S_def},
    1.15      @{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def},
    1.16 -    @{thm Return_def}]) [] [temp_use @{thm squareE}] 1 *})
    1.17 +    @{thm Return_def}]) [] [temp_use @{context} @{thm squareE}] 1 *})
    1.18  
    1.19  
    1.20  (* ------------------------------ State S2 ---------------------------------------- *)
    1.21 @@ -566,7 +566,8 @@
    1.22           & ~unchanged (e p, c p, r p, m p, rmhist!p)  & $S1 rmhist p
    1.23           --> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"
    1.24    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
    1.25 -      (map temp_elim [@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1 *})
    1.26 +      (map (temp_elim @{context})
    1.27 +        [@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1 *})
    1.28     using [[fast_solver]]
    1.29     apply (auto elim!: squareE [temp_use] intro!: S1Env [temp_use])
    1.30    done
    1.31 @@ -576,7 +577,8 @@
    1.32           --> (S3 rmhist p)$ & MClkFwd memCh crCh cst p
    1.33               & unchanged (e p, r p, m p, rmhist!p)"
    1.34    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
    1.35 -    (map temp_elim [@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1 *})
    1.36 +    (map (temp_elim @{context})
    1.37 +      [@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1 *})
    1.38     using [[fast_solver]]
    1.39     apply (auto elim!: squareE [temp_use] intro!: S2Clerk [temp_use] S2Forward [temp_use])
    1.40    done
    1.41 @@ -586,9 +588,10 @@
    1.42           --> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p))
    1.43               | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
    1.44    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
    1.45 -    (map temp_elim [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1 *})
    1.46 +    (map (temp_elim @{context}) [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1 *})
    1.47    apply (tactic {* action_simp_tac @{context} []
    1.48 -    (@{thm squareE} :: map temp_elim [@{thm S3RPC}, @{thm S3Forward}, @{thm S3Fail}]) 1 *})
    1.49 +    (@{thm squareE} ::
    1.50 +      map (temp_elim @{context}) [@{thm S3RPC}, @{thm S3Forward}, @{thm S3Fail}]) 1 *})
    1.51     apply (auto dest!: S3Hist [temp_use])
    1.52    done
    1.53  
    1.54 @@ -599,9 +602,10 @@
    1.55               | ((S4 rmhist p)$ & (? l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p))
    1.56               | ((S5 rmhist p)$ & MemReturn rmCh ires p & unchanged (e p, c p, r p))"
    1.57    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
    1.58 -    (map temp_elim [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
    1.59 +    (map (temp_elim @{context}) [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
    1.60    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm RNext_def}]) []
    1.61 -    (@{thm squareE} :: map temp_elim [@{thm S4Read}, @{thm S4Write}, @{thm S4Return}]) 1 *})
    1.62 +    (@{thm squareE} ::
    1.63 +      map (temp_elim @{context}) [@{thm S4Read}, @{thm S4Write}, @{thm S4Return}]) 1 *})
    1.64    apply (auto dest!: S4Hist [temp_use])
    1.65    done
    1.66  
    1.67 @@ -610,8 +614,8 @@
    1.68           --> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p))
    1.69               | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
    1.70    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
    1.71 -    (map temp_elim [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1 *})
    1.72 -  apply (tactic {* action_simp_tac @{context} [] [@{thm squareE}, temp_elim @{thm S5RPC}] 1 *})
    1.73 +    (map (temp_elim @{context}) [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1 *})
    1.74 +  apply (tactic {* action_simp_tac @{context} [] [@{thm squareE}, temp_elim @{context} @{thm S5RPC}] 1 *})
    1.75     using [[fast_solver]]
    1.76     apply (auto elim!: squareE [temp_use] dest!: S5Reply [temp_use] S5Fail [temp_use])
    1.77    done
    1.78 @@ -621,9 +625,9 @@
    1.79           --> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p))
    1.80               | ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))"
    1.81    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
    1.82 -    (map temp_elim [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1 *})
    1.83 +    (map (temp_elim @{context}) [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1 *})
    1.84    apply (tactic {* action_simp_tac @{context} []
    1.85 -    (@{thm squareE} :: map temp_elim [@{thm S6Clerk}, @{thm S6Retry}, @{thm S6Reply}]) 1 *})
    1.86 +    (@{thm squareE} :: map (temp_elim @{context}) [@{thm S6Clerk}, @{thm S6Retry}, @{thm S6Reply}]) 1 *})
    1.87       apply (auto dest: S6Hist [temp_use])
    1.88    done
    1.89  
    1.90 @@ -795,8 +799,8 @@
    1.91    SELECT_GOAL
    1.92     (TRY (rtac @{thm actionI} 1) THEN
    1.93      Induct_Tacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" 1 THEN
    1.94 -    rewrite_goals_tac @{thms action_rews} THEN
    1.95 -    forward_tac [temp_use @{thm Step1_4_7}] 1 THEN
    1.96 +    rewrite_goals_tac ctxt @{thms action_rews} THEN
    1.97 +    forward_tac [temp_use ctxt @{thm Step1_4_7}] 1 THEN
    1.98      asm_full_simp_tac ctxt 1);
    1.99  *}
   1.100  
   1.101 @@ -898,7 +902,7 @@
   1.102  lemma S1_RNextdisabled: "|- S1 rmhist p -->
   1.103           ~Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
   1.104    apply (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def},
   1.105 -    @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{thm Memoryidle}] 1 *})
   1.106 +    @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{context} @{thm Memoryidle}] 1 *})
   1.107    apply force
   1.108    done
   1.109  
   1.110 @@ -1103,7 +1107,7 @@
   1.111     apply (erule InfiniteEnsures)
   1.112      apply assumption
   1.113     apply (tactic {* action_simp_tac @{context} []
   1.114 -     (map temp_elim [@{thm MClkReplyS6}, @{thm S6MClkReply_successors}]) 1 *})
   1.115 +     (map (temp_elim @{context}) [@{thm MClkReplyS6}, @{thm S6MClkReply_successors}]) 1 *})
   1.116    apply (auto simp: SF_def)
   1.117    apply (erule contrapos_np)
   1.118    apply (auto intro!: S6MClkReply_enabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use])
   1.119 @@ -1190,7 +1194,7 @@
   1.120        ==> sigma |= []<>S1 rmhist p"
   1.121    apply (rule classical)
   1.122    apply (tactic {* asm_lr_simp_tac (@{context} addsimps
   1.123 -    [temp_use @{thm NotBox}, temp_rewrite @{thm NotDmd}]) 1 *})
   1.124 +    [temp_use @{context} @{thm NotBox}, temp_rewrite @{context} @{thm NotDmd}]) 1 *})
   1.125    apply (auto elim!: leadsto_infinite [temp_use] mp dest!: DBImplBD [temp_use])
   1.126    done
   1.127