proper method_setup;
authorwenzelm
Fri May 13 14:25:35 2011 +0200 (2011-05-13)
changeset 42787dd3ab25eb9d1
parent 42786 06a38b936342
child 42788 9984232a0c68
proper method_setup;
src/HOL/TLA/TLA.thy
     1.1 --- a/src/HOL/TLA/TLA.thy	Fri May 13 14:16:46 2011 +0200
     1.2 +++ b/src/HOL/TLA/TLA.thy	Fri May 13 14:25:35 2011 +0200
     1.3 @@ -310,6 +310,11 @@
     1.4                           eres_inst_tac ctxt [(("'a", 0), "state * state")] @{thm box_thin} i])
     1.5  *}
     1.6  
     1.7 +method_setup merge_box = {* Scan.succeed (K (SIMPLE_METHOD' merge_box_tac)) *} ""
     1.8 +method_setup merge_temp_box = {* Scan.succeed (SIMPLE_METHOD' o merge_temp_box_tac) *} ""
     1.9 +method_setup merge_stp_box = {* Scan.succeed (SIMPLE_METHOD' o merge_stp_box_tac) *} ""
    1.10 +method_setup merge_act_box = {* Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac) *} ""
    1.11 +
    1.12  (* rewrite rule to push universal quantification through box:
    1.13        (sigma |= [](! x. F x)) = (! x. (sigma |= []F x))
    1.14  *)
    1.15 @@ -317,8 +322,7 @@
    1.16  
    1.17  lemma DmdOr: "|- (<>(F | G)) = (<>F | <>G)"
    1.18    apply (auto simp add: dmd_def split_box_conj [try_rewrite])
    1.19 -  apply (erule contrapos_np, tactic "merge_box_tac 1",
    1.20 -    fastsimp elim!: STL4E [temp_use])+
    1.21 +  apply (erule contrapos_np, merge_box, fastsimp elim!: STL4E [temp_use])+
    1.22    done
    1.23  
    1.24  lemma exT: "|- (EX x. <>(F x)) = (<>(EX x. F x))"
    1.25 @@ -328,7 +332,7 @@
    1.26  
    1.27  lemma STL4Edup: "!!sigma. [| sigma |= []A; sigma |= []F; |- F & []A --> G |] ==> sigma |= []G"
    1.28    apply (erule dup_boxE)
    1.29 -  apply (tactic "merge_box_tac 1")
    1.30 +  apply merge_box
    1.31    apply (erule STL4E)
    1.32    apply assumption
    1.33    done
    1.34 @@ -338,7 +342,7 @@
    1.35    apply (unfold dmd_def)
    1.36    apply auto
    1.37    apply (erule notE)
    1.38 -  apply (tactic "merge_box_tac 1")
    1.39 +  apply merge_box
    1.40    apply (fastsimp elim!: STL4E [temp_use])
    1.41    done
    1.42  
    1.43 @@ -349,7 +353,7 @@
    1.44    shows "sigma |= []<>H"
    1.45    apply (insert 1 2)
    1.46    apply (erule_tac F = G in dup_boxE)
    1.47 -  apply (tactic "merge_box_tac 1")
    1.48 +  apply merge_box
    1.49    apply (fastsimp elim!: STL4E [temp_use] DmdImpl2 [temp_use] intro!: 3 [temp_use])
    1.50    done
    1.51  
    1.52 @@ -359,7 +363,7 @@
    1.53    apply (unfold dmd_def)
    1.54    apply clarsimp
    1.55    apply (erule dup_boxE)
    1.56 -  apply (tactic "merge_box_tac 1")
    1.57 +  apply merge_box
    1.58    apply (erule contrapos_np)
    1.59    apply (fastsimp elim!: STL4E [temp_use])
    1.60    done
    1.61 @@ -368,14 +372,14 @@
    1.62  lemma BoxDmd_simple: "|- []F & <>G --> <>(F & G)"
    1.63    apply (unfold dmd_def)
    1.64    apply clarsimp
    1.65 -  apply (tactic "merge_box_tac 1")
    1.66 +  apply merge_box
    1.67    apply (fastsimp elim!: notE STL4E [temp_use])
    1.68    done
    1.69  
    1.70  lemma BoxDmd2_simple: "|- []F & <>G --> <>(G & F)"
    1.71    apply (unfold dmd_def)
    1.72    apply clarsimp
    1.73 -  apply (tactic "merge_box_tac 1")
    1.74 +  apply merge_box
    1.75    apply (fastsimp elim!: notE STL4E [temp_use])
    1.76    done
    1.77  
    1.78 @@ -610,7 +614,7 @@
    1.79  lemma unless: "|- []($P --> P` | Q`) --> (stable P) | <>Q"
    1.80    apply (unfold dmd_def)
    1.81    apply (clarsimp dest!: BoxPrime [temp_use])
    1.82 -  apply (tactic "merge_box_tac 1")
    1.83 +  apply merge_box
    1.84    apply (erule contrapos_np)
    1.85    apply (fastsimp elim!: Stable [temp_use])
    1.86    done
    1.87 @@ -840,7 +844,7 @@
    1.88    apply (unfold leadsto_def)
    1.89    apply clarsimp
    1.90    apply (erule dup_boxE) (* [][] (Init G --> H) *)
    1.91 -  apply (tactic "merge_box_tac 1")
    1.92 +  apply merge_box
    1.93    apply (clarsimp elim!: STL4E [temp_use])
    1.94    apply (rule dup_dmdD)
    1.95    apply (subgoal_tac "sigmaa |= <>Init G")
    1.96 @@ -862,7 +866,7 @@
    1.97  lemma LatticeDisjunctionIntro: "|- (F ~> H) & (G ~> H) --> (F | G ~> H)"
    1.98    apply (unfold leadsto_def)
    1.99    apply clarsimp
   1.100 -  apply (tactic "merge_box_tac 1")
   1.101 +  apply merge_box
   1.102    apply (auto simp: Init_simps elim!: STL4E [temp_use])
   1.103    done
   1.104  
   1.105 @@ -943,7 +947,7 @@
   1.106    apply (clarsimp dest!: BoxSFI [temp_use])
   1.107    apply (erule (2) ensures [temp_use])
   1.108    apply (erule_tac F = F in dup_boxE)
   1.109 -  apply (tactic "merge_temp_box_tac @{context} 1")
   1.110 +  apply merge_temp_box
   1.111    apply (erule STL4Edup)
   1.112    apply assumption
   1.113    apply (clarsimp simp: SF_def)
   1.114 @@ -962,7 +966,7 @@
   1.115    apply (clarsimp dest!: BoxWFI [temp_use] BoxDmdBox [temp_use, THEN iffD2]
   1.116      simp: WF_def [where A = M])
   1.117    apply (erule_tac F = F in dup_boxE)
   1.118 -  apply (tactic "merge_temp_box_tac @{context} 1")
   1.119 +  apply merge_temp_box
   1.120    apply (erule STL4Edup)
   1.121     apply assumption
   1.122    apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
   1.123 @@ -971,7 +975,7 @@
   1.124     apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
   1.125    apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
   1.126    apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
   1.127 -  apply (tactic "merge_act_box_tac @{context} 1")
   1.128 +  apply merge_act_box
   1.129    apply (frule 4 [temp_use])
   1.130       apply assumption+
   1.131    apply (drule STL6 [temp_use])
   1.132 @@ -980,7 +984,7 @@
   1.133    apply (erule_tac V = "sigmaa |= []F" in thin_rl)
   1.134    apply (drule BoxWFI [temp_use])
   1.135    apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE)
   1.136 -  apply (tactic "merge_temp_box_tac @{context} 1")
   1.137 +  apply merge_temp_box
   1.138    apply (erule DmdImpldup)
   1.139     apply assumption
   1.140    apply (auto simp: split_box_conj [try_rewrite] STL3 [try_rewrite]
   1.141 @@ -1000,7 +1004,7 @@
   1.142    apply (clarsimp dest!: BoxSFI [temp_use] simp: 2 [try_rewrite] SF_def [where A = M])
   1.143    apply (erule_tac F = F in dup_boxE)
   1.144    apply (erule_tac F = "TEMP <>Enabled (<M>_g) " in dup_boxE)
   1.145 -  apply (tactic "merge_temp_box_tac @{context} 1")
   1.146 +  apply merge_temp_box
   1.147    apply (erule STL4Edup)
   1.148     apply assumption
   1.149    apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
   1.150 @@ -1009,14 +1013,14 @@
   1.151     apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
   1.152    apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
   1.153    apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
   1.154 -  apply (tactic "merge_act_box_tac @{context} 1")
   1.155 +  apply merge_act_box
   1.156    apply (frule 4 [temp_use])
   1.157       apply assumption+
   1.158    apply (erule_tac V = "sigmaa |= []F" in thin_rl)
   1.159    apply (drule BoxSFI [temp_use])
   1.160    apply (erule_tac F = "TEMP <>Enabled (<M>_g)" in dup_boxE)
   1.161    apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE)
   1.162 -  apply (tactic "merge_temp_box_tac @{context} 1")
   1.163 +  apply merge_temp_box
   1.164    apply (erule DmdImpldup)
   1.165     apply assumption
   1.166    apply (auto simp: split_box_conj [try_rewrite] STL3 [try_rewrite]
   1.167 @@ -1149,7 +1153,7 @@
   1.168    apply (rule conjI)
   1.169     prefer 2
   1.170     apply (insert 2)
   1.171 -   apply (tactic "merge_box_tac 1")
   1.172 +   apply merge_box
   1.173     apply (force elim!: STL4E [temp_use] 5 [temp_use])
   1.174    apply (insert 1)
   1.175    apply (force simp: Init_defs elim!: 4 [temp_use])