src/HOL/TLA/Memory/MemoryImplementation.thy

   (* the predicate S describes the states of the implementation.
      slight simplification: two "histState" parameters instead of a
      (one- or two-element) set.
      NB: The second conjunct of the definition in the paper is taken care of by
      the type definitions. The last conjunct is asserted separately as the memory
-     invariant MemInv, proved in Memory.ML. *)
+     invariant MemInv, proved in Memory.thy. *)
   S :: "histType => bool => bool => bool => mClkState => rpcState => histState => histState => PrIds => stpred"
       "S rmhist ecalling ccalling rcalling cs rs hs1 hs2 p == PRED
                 Calling memCh p = #ecalling
               & Calling crCh p  = #ccalling
               & (#ccalling --> arg<crCh!p> = MClkRelayArg<arg<memCh!p>>)

                            (mm!l, rtrner rmCh!p, ires!p))"
 
 (*
     The main theorem is theorem "Implementation" at the end of this file,
     which shows that the composition of a reliable memory, an RPC component, and
-    a memory clerk implements an unreliable memory. The files "MIsafe.ML" and
-    "MIlive.ML" contain lower-level lemmas for the safety and liveness parts.
+    a memory clerk implements an unreliable memory. The files "MIsafe.thy" and
+    "MIlive.thy" contain lower-level lemmas for the safety and liveness parts.
 
     Steps are (roughly) numbered as in the hand proof.
 *)
 
 (* --------------------------- automatic prover --------------------------- *)
 
 declare if_weak_cong [cong del]
 
-ML {* val MI_css = (claset(), simpset()) *}
+ML {* val MI_css = (@{claset}, @{simpset}) *}
 
 (* A more aggressive variant that tries to solve subgoals by assumption
    or contradiction during the simplification.
    THIS IS UNSAFE, BECAUSE IT DOESN'T RECORD THE CHOICES!!
    (but it can be a lot faster than MI_css)

 ML {*
 val MI_fast_css =
   let
     val (cs,ss) = MI_css
   in
-    (cs addSEs [temp_use (thm "squareE")],
+    (cs addSEs [temp_use @{thm squareE}],
       ss addSSolver (mk_solver "" (fn thms => assume_tac ORELSE' (etac notE))))
   end;
 
 val temp_elim = make_elim o temp_use;
 *}

 
 (* Frequently needed abbreviation: distinguish between idling and non-idling
    steps of the implementation, and try to solve the idling case by simplification
 *)
 ML {*
-local
-  val actionI = thm "actionI";
-  val action_rews = thms "action_rews";
-  val Step1_4_7 = thm "Step1_4_7";
-in
-fun split_idle_tac simps i =
-    EVERY [TRY (rtac actionI i),
+fun split_idle_tac ss simps i =
+    EVERY [TRY (rtac @{thm actionI} i),
            case_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i,
-           rewrite_goals_tac action_rews,
-           forward_tac [temp_use Step1_4_7] i,
-           asm_full_simp_tac (simpset() addsimps simps) i
+           rewrite_goals_tac @{thms action_rews},
+           forward_tac [temp_use @{thm Step1_4_7}] i,
+           asm_full_simp_tac (ss addsimps simps) i
           ]
-end
 *}
 (* ----------------------------------------------------------------------
    Combine steps 1.2 and 1.4 to prove that the implementation satisfies
    the specification's next-state relation.
 *)

 (* Steps that leave all variables unchanged are safe, so I may assume
    that some variable changes in the proof that a step is safe. *)
 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 [thm "square_def"] 1 *})
+  apply (tactic {* split_idle_tac @{simpset} [thm "square_def"] 1 *})
   apply force
   done
 (* turn into (unsafe, looping!) introduction rule *)
 lemmas unchanged_safeI = impI [THEN unchanged_safe [action_use], standard]
 

 
 (* ------------------------------ State S1 ------------------------------ *)
 
 lemma S1_successors: "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
          --> (S1 rmhist p)$ | (S2 rmhist p)$"
-  apply (tactic "split_idle_tac [] 1")
+  apply (tactic "split_idle_tac @{simpset} [] 1")
   apply (auto dest!: Step1_2_1 [temp_use])
   done
 
 (* Show that the implementation can satisfy the high-level fairness requirements
    by entering the state S1 infinitely often.

 
 (* ------------------------------ State S2 ------------------------------ *)
 
 lemma S2_successors: "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
          --> (S2 rmhist p)$ | (S3 rmhist p)$"
-  apply (tactic "split_idle_tac [] 1")
+  apply (tactic "split_idle_tac @{simpset} [] 1")
   apply (auto dest!: Step1_2_2 [temp_use])
   done
 
 lemma S2MClkFwd_successors: "|- ($S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
          & <MClkFwd memCh crCh cst p>_(c p)

 
 (* ------------------------------ State S3 ------------------------------ *)
 
 lemma S3_successors: "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
          --> (S3 rmhist p)$ | (S4 rmhist p | S6 rmhist p)$"
-  apply (tactic "split_idle_tac [] 1")
+  apply (tactic "split_idle_tac @{simpset} [] 1")
   apply (auto dest!: Step1_2_3 [temp_use])
   done
 
 lemma S3RPC_successors: "|- ($S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
          & <RPCNext crCh rmCh rst p>_(r p)

 (* ------------- State S4 -------------------------------------------------- *)
 
 lemma S4_successors: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
         & (ALL l. $MemInv mm l)
         --> (S4 rmhist p)$ | (S5 rmhist p)$"
-  apply (tactic "split_idle_tac [] 1")
+  apply (tactic "split_idle_tac @{simpset} [] 1")
   apply (auto dest!: Step1_2_4 [temp_use])
   done
 
 (* --------- State S4a: S4 /\ (ires p = NotAResult) ------------------------ *)
 
 lemma S4a_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)$
              | ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$"
-  apply (tactic {* split_idle_tac [thm "m_def"] 1 *})
+  apply (tactic {* split_idle_tac @{simpset} [thm "m_def"] 1 *})
   apply (auto dest!: Step1_2_4 [temp_use])
   done
 
 lemma S4aRNext_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))

 (* ---------- State S4b: S4 /\ (ires p # NotAResult) --------------------------- *)
 
 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 [thm "m_def"] 1 *})
+  apply (tactic {* split_idle_tac @{simpset} [thm "m_def"] 1 *})
   apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use])
   done
 
 lemma S4bReturn_successors: "|- ($(S4 rmhist p & ires!p ~= #NotAResult)
          & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)

 
 (* ------------------------------ State S5 ------------------------------ *)
 
 lemma S5_successors: "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
          --> (S5 rmhist p)$ | (S6 rmhist p)$"
-  apply (tactic "split_idle_tac [] 1")
+  apply (tactic "split_idle_tac @{simpset} [] 1")
   apply (auto dest!: Step1_2_5 [temp_use])
   done
 
 lemma S5RPC_successors: "|- ($S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
          & <RPCNext crCh rmCh rst p>_(r p)

 
 (* ------------------------------ State S6 ------------------------------ *)
 
 lemma S6_successors: "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
          --> (S1 rmhist p)$ | (S3 rmhist p)$ | (S6 rmhist p)$"
-  apply (tactic "split_idle_tac [] 1")
+  apply (tactic "split_idle_tac @{simpset} [] 1")
   apply (auto dest!: Step1_2_6 [temp_use])
   done
 
 lemma S6MClkReply_successors:
   "|- ($S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))

          & $ImpInv rmhist p
          --> (S4 rmhist p)$ & unchanged (e p, c p, r p, rmhist!p)"
   apply clarsimp
   apply (drule WriteS4 [action_use])
    apply assumption
-  apply (tactic "split_idle_tac [] 1")
+  apply (tactic "split_idle_tac @{simpset} [] 1")
   apply (auto simp: ImpNext_def dest!: S4EnvUnch [temp_use] S4ClerkUnch [temp_use]
     S4RPCUnch [temp_use])
      apply (auto simp: square_def dest: S4Write [temp_use])
   done