# HG changeset patch
# User wenzelm
# Date 1305289535 -7200
# Node ID dd3ab25eb9d1d8d76e468db8953d1f6e959fbd00
# Parent  06a38b936342e61fd66ea29d065b93aac14c2bcd
proper method_setup;

diff -r 06a38b936342 -r dd3ab25eb9d1 src/HOL/TLA/TLA.thy
--- a/src/HOL/TLA/TLA.thy	Fri May 13 14:16:46 2011 +0200
+++ b/src/HOL/TLA/TLA.thy	Fri May 13 14:25:35 2011 +0200
@@ -310,6 +310,11 @@
                          eres_inst_tac ctxt [(("'a", 0), "state * state")] @{thm box_thin} i])
 *}
 
+method_setup merge_box = {* Scan.succeed (K (SIMPLE_METHOD' merge_box_tac)) *} ""
+method_setup merge_temp_box = {* Scan.succeed (SIMPLE_METHOD' o merge_temp_box_tac) *} ""
+method_setup merge_stp_box = {* Scan.succeed (SIMPLE_METHOD' o merge_stp_box_tac) *} ""
+method_setup merge_act_box = {* Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac) *} ""
+
 (* rewrite rule to push universal quantification through box:
       (sigma |= [](! x. F x)) = (! x. (sigma |= []F x))
 *)
@@ -317,8 +322,7 @@
 
 lemma DmdOr: "|- (<>(F | G)) = (<>F | <>G)"
   apply (auto simp add: dmd_def split_box_conj [try_rewrite])
-  apply (erule contrapos_np, tactic "merge_box_tac 1",
-    fastsimp elim!: STL4E [temp_use])+
+  apply (erule contrapos_np, merge_box, fastsimp elim!: STL4E [temp_use])+
   done
 
 lemma exT: "|- (EX x. <>(F x)) = (<>(EX x. F x))"
@@ -328,7 +332,7 @@
 
 lemma STL4Edup: "!!sigma. [| sigma |= []A; sigma |= []F; |- F & []A --> G |] ==> sigma |= []G"
   apply (erule dup_boxE)
-  apply (tactic "merge_box_tac 1")
+  apply merge_box
   apply (erule STL4E)
   apply assumption
   done
@@ -338,7 +342,7 @@
   apply (unfold dmd_def)
   apply auto
   apply (erule notE)
-  apply (tactic "merge_box_tac 1")
+  apply merge_box
   apply (fastsimp elim!: STL4E [temp_use])
   done
 
@@ -349,7 +353,7 @@
   shows "sigma |= []<>H"
   apply (insert 1 2)
   apply (erule_tac F = G in dup_boxE)
-  apply (tactic "merge_box_tac 1")
+  apply merge_box
   apply (fastsimp elim!: STL4E [temp_use] DmdImpl2 [temp_use] intro!: 3 [temp_use])
   done
 
@@ -359,7 +363,7 @@
   apply (unfold dmd_def)
   apply clarsimp
   apply (erule dup_boxE)
-  apply (tactic "merge_box_tac 1")
+  apply merge_box
   apply (erule contrapos_np)
   apply (fastsimp elim!: STL4E [temp_use])
   done
@@ -368,14 +372,14 @@
 lemma BoxDmd_simple: "|- []F & <>G --> <>(F & G)"
   apply (unfold dmd_def)
   apply clarsimp
-  apply (tactic "merge_box_tac 1")
+  apply merge_box
   apply (fastsimp elim!: notE STL4E [temp_use])
   done
 
 lemma BoxDmd2_simple: "|- []F & <>G --> <>(G & F)"
   apply (unfold dmd_def)
   apply clarsimp
-  apply (tactic "merge_box_tac 1")
+  apply merge_box
   apply (fastsimp elim!: notE STL4E [temp_use])
   done
 
@@ -610,7 +614,7 @@
 lemma unless: "|- []($P --> P` | Q`) --> (stable P) | <>Q"
   apply (unfold dmd_def)
   apply (clarsimp dest!: BoxPrime [temp_use])
-  apply (tactic "merge_box_tac 1")
+  apply merge_box
   apply (erule contrapos_np)
   apply (fastsimp elim!: Stable [temp_use])
   done
@@ -840,7 +844,7 @@
   apply (unfold leadsto_def)
   apply clarsimp
   apply (erule dup_boxE) (* [][] (Init G --> H) *)
-  apply (tactic "merge_box_tac 1")
+  apply merge_box
   apply (clarsimp elim!: STL4E [temp_use])
   apply (rule dup_dmdD)
   apply (subgoal_tac "sigmaa |= <>Init G")
@@ -862,7 +866,7 @@
 lemma LatticeDisjunctionIntro: "|- (F ~> H) & (G ~> H) --> (F | G ~> H)"
   apply (unfold leadsto_def)
   apply clarsimp
-  apply (tactic "merge_box_tac 1")
+  apply merge_box
   apply (auto simp: Init_simps elim!: STL4E [temp_use])
   done
 
@@ -943,7 +947,7 @@
   apply (clarsimp dest!: BoxSFI [temp_use])
   apply (erule (2) ensures [temp_use])
   apply (erule_tac F = F in dup_boxE)
-  apply (tactic "merge_temp_box_tac @{context} 1")
+  apply merge_temp_box
   apply (erule STL4Edup)
   apply assumption
   apply (clarsimp simp: SF_def)
@@ -962,7 +966,7 @@
   apply (clarsimp dest!: BoxWFI [temp_use] BoxDmdBox [temp_use, THEN iffD2]
     simp: WF_def [where A = M])
   apply (erule_tac F = F in dup_boxE)
-  apply (tactic "merge_temp_box_tac @{context} 1")
+  apply merge_temp_box
   apply (erule STL4Edup)
    apply assumption
   apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
@@ -971,7 +975,7 @@
    apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
   apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
   apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
-  apply (tactic "merge_act_box_tac @{context} 1")
+  apply merge_act_box
   apply (frule 4 [temp_use])
      apply assumption+
   apply (drule STL6 [temp_use])
@@ -980,7 +984,7 @@
   apply (erule_tac V = "sigmaa |= []F" in thin_rl)
   apply (drule BoxWFI [temp_use])
   apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE)
-  apply (tactic "merge_temp_box_tac @{context} 1")
+  apply merge_temp_box
   apply (erule DmdImpldup)
    apply assumption
   apply (auto simp: split_box_conj [try_rewrite] STL3 [try_rewrite]
@@ -1000,7 +1004,7 @@
   apply (clarsimp dest!: BoxSFI [temp_use] simp: 2 [try_rewrite] SF_def [where A = M])
   apply (erule_tac F = F in dup_boxE)
   apply (erule_tac F = "TEMP <>Enabled (<M>_g) " in dup_boxE)
-  apply (tactic "merge_temp_box_tac @{context} 1")
+  apply merge_temp_box
   apply (erule STL4Edup)
    apply assumption
   apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
@@ -1009,14 +1013,14 @@
    apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
   apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
   apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
-  apply (tactic "merge_act_box_tac @{context} 1")
+  apply merge_act_box
   apply (frule 4 [temp_use])
      apply assumption+
   apply (erule_tac V = "sigmaa |= []F" in thin_rl)
   apply (drule BoxSFI [temp_use])
   apply (erule_tac F = "TEMP <>Enabled (<M>_g)" in dup_boxE)
   apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE)
-  apply (tactic "merge_temp_box_tac @{context} 1")
+  apply merge_temp_box
   apply (erule DmdImpldup)
    apply assumption
   apply (auto simp: split_box_conj [try_rewrite] STL3 [try_rewrite]
@@ -1149,7 +1153,7 @@
   apply (rule conjI)
    prefer 2
    apply (insert 2)
-   apply (tactic "merge_box_tac 1")
+   apply merge_box
    apply (force elim!: STL4E [temp_use] 5 [temp_use])
   apply (insert 1)
   apply (force simp: Init_defs elim!: 4 [temp_use])