--- 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])