misc tuning and modernization;
authorwenzelm
Sat Feb 01 17:56:03 2014 +0100 (2014-02-01)
changeset 55228901a6696cdd8
parent 55227 653de351d21c
child 55229 08f2ebb65078
misc tuning and modernization;
src/Sequents/ILL.thy
src/Sequents/LK.thy
src/Sequents/LK/Hard_Quantifiers.thy
src/Sequents/LK/Nat.thy
src/Sequents/LK0.thy
src/Sequents/Sequents.thy
src/Sequents/Washing.thy
src/Sequents/prover.ML
src/Sequents/simpdata.ML
     1.1 --- a/src/Sequents/ILL.thy	Sat Feb 01 00:32:32 2014 +0000
     1.2 +++ b/src/Sequents/ILL.thy	Sat Feb 01 17:56:03 2014 +0100
     1.3 @@ -126,23 +126,25 @@
     1.4  
     1.5  
     1.6  ML {*
     1.7 -val lazy_cs = empty_pack
     1.8 -  add_safes [@{thm tensl}, @{thm conjr}, @{thm disjl}, @{thm promote0},
     1.9 -    @{thm context2}, @{thm context3}]
    1.10 -  add_unsafes [@{thm identity}, @{thm zerol}, @{thm conjll}, @{thm conjlr},
    1.11 -    @{thm disjrl}, @{thm disjrr}, @{thm impr}, @{thm tensr}, @{thm impl},
    1.12 -    @{thm derelict}, @{thm weaken}, @{thm promote1}, @{thm promote2},
    1.13 -    @{thm context1}, @{thm context4a}, @{thm context4b}];
    1.14 -
    1.15 -fun prom_tac n =
    1.16 -  REPEAT (resolve_tac [@{thm promote0}, @{thm promote1}, @{thm promote2}] n)
    1.17 +  val lazy_pack =
    1.18 +    Cla.put_pack Cla.empty_pack @{context}
    1.19 +    |> fold_rev Cla.add_safe @{thms tensl conjr disjl promote0 context2 context3}
    1.20 +    |> fold_rev Cla.add_unsafe @{thms
    1.21 +      identity zerol conjll conjlr
    1.22 +      disjrl disjrr impr tensr impl
    1.23 +      derelict weaken promote1 promote2
    1.24 +      context1 context4a context4b}
    1.25 +    |> Cla.get_pack;
    1.26 +  
    1.27 +  fun promote_tac i =
    1.28 +    REPEAT (resolve_tac @{thms promote0 promote1 promote2} i);
    1.29  *}
    1.30  
    1.31 -method_setup best_lazy =
    1.32 -  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac lazy_cs))) *}
    1.33 -  "lazy classical reasoning"
    1.34 +method_setup best_lazy = {*
    1.35 +  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack lazy_pack ctxt)))
    1.36 +*} "lazy classical reasoning"
    1.37  
    1.38 -lemma aux_impl: "$F, $G |- A ==> $F, !(A -o B), $G |- B"
    1.39 +lemma aux_impl: "$F, $G |- A \<Longrightarrow> $F, !(A -o B), $G |- B"
    1.40    apply (rule derelict)
    1.41    apply (rule impl)
    1.42    apply (rule_tac [2] identity)
    1.43 @@ -150,7 +152,7 @@
    1.44    apply assumption
    1.45    done
    1.46  
    1.47 -lemma conj_lemma: " $F, !A, !B, $G |- C ==> $F, !(A && B), $G |- C"
    1.48 +lemma conj_lemma: " $F, !A, !B, $G |- C \<Longrightarrow> $F, !(A && B), $G |- C"
    1.49    apply (rule contract)
    1.50    apply (rule_tac A = " (!A) >< (!B) " in cut)
    1.51    apply (rule_tac [2] tensr)
    1.52 @@ -170,13 +172,13 @@
    1.53    apply (rule context1)
    1.54    done
    1.55  
    1.56 -lemma impr_contract: "!A, !A, $G |- B ==> $G |- (!A) -o B"
    1.57 +lemma impr_contract: "!A, !A, $G |- B \<Longrightarrow> $G |- (!A) -o B"
    1.58    apply (rule impr)
    1.59    apply (rule contract)
    1.60    apply assumption
    1.61    done
    1.62  
    1.63 -lemma impr_contr_der: "A, !A, $G |- B ==> $G |- (!A) -o B"
    1.64 +lemma impr_contr_der: "A, !A, $G |- B \<Longrightarrow> $G |- (!A) -o B"
    1.65    apply (rule impr)
    1.66    apply (rule contract)
    1.67    apply (rule derelict)
    1.68 @@ -207,7 +209,7 @@
    1.69    apply (rule context1)
    1.70    done
    1.71  
    1.72 -lemma mp_rule1: "$F, B, $G, $H |- C ==> $F, A, $G, A -o B, $H |- C"
    1.73 +lemma mp_rule1: "$F, B, $G, $H |- C \<Longrightarrow> $F, A, $G, A -o B, $H |- C"
    1.74    apply (rule_tac A = "B" in cut)
    1.75    apply (rule_tac [2] ll_mp)
    1.76    prefer 2 apply (assumption)
    1.77 @@ -216,7 +218,7 @@
    1.78    apply (rule context1)
    1.79    done
    1.80  
    1.81 -lemma mp_rule2: "$F, B, $G, $H |- C ==> $F, A -o B, $G, A, $H |- C"
    1.82 +lemma mp_rule2: "$F, B, $G, $H |- C \<Longrightarrow> $F, A -o B, $G, A, $H |- C"
    1.83    apply (rule_tac A = "B" in cut)
    1.84    apply (rule_tac [2] ll_mp)
    1.85    prefer 2 apply (assumption)
    1.86 @@ -228,7 +230,7 @@
    1.87  lemma or_to_and: "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))"
    1.88    by best_lazy
    1.89  
    1.90 -lemma o_a_rule: "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C ==>  
    1.91 +lemma o_a_rule: "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C \<Longrightarrow>
    1.92            $F, !((!(A ++ B)) -o 0), $G |- C"
    1.93    apply (rule cut)
    1.94    apply (rule_tac [2] or_to_and)
    1.95 @@ -256,7 +258,7 @@
    1.96    apply best_lazy
    1.97    done
    1.98  
    1.99 -lemma a_not_a_rule: "$J1, !A -o 0, $J2 |- B ==> $J1, !A -o (!A -o 0), $J2 |- B"
   1.100 +lemma a_not_a_rule: "$J1, !A -o 0, $J2 |- B \<Longrightarrow> $J1, !A -o (!A -o 0), $J2 |- B"
   1.101    apply (rule_tac A = "!A -o 0" in cut)
   1.102    apply (rule_tac [2] a_not_a)
   1.103    prefer 2 apply (assumption)
   1.104 @@ -264,20 +266,25 @@
   1.105    done
   1.106  
   1.107  ML {*
   1.108 -val safe_cs = lazy_cs add_safes [@{thm conj_lemma}, @{thm ll_mp}, @{thm contrad1},
   1.109 -                                 @{thm contrad2}, @{thm mp_rule1}, @{thm mp_rule2}, @{thm o_a_rule},
   1.110 -                                 @{thm a_not_a_rule}]
   1.111 -                      add_unsafes [@{thm aux_impl}];
   1.112 +  val safe_pack =
   1.113 +    Cla.put_pack lazy_pack @{context}
   1.114 +    |> fold_rev Cla.add_safe @{thms conj_lemma ll_mp contrad1
   1.115 +        contrad2 mp_rule1 mp_rule2 o_a_rule a_not_a_rule}
   1.116 +    |> Cla.add_unsafe @{thm aux_impl}
   1.117 +    |> Cla.get_pack;
   1.118  
   1.119 -val power_cs = safe_cs add_unsafes [@{thm impr_contr_der}];
   1.120 +  val power_pack =
   1.121 +    Cla.put_pack safe_pack @{context}
   1.122 +    |> Cla.add_unsafe @{thm impr_contr_der}
   1.123 +    |> Cla.get_pack;
   1.124  *}
   1.125  
   1.126  
   1.127  method_setup best_safe =
   1.128 -  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac safe_cs))) *}
   1.129 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack safe_pack ctxt))) *}
   1.130  
   1.131  method_setup best_power =
   1.132 -  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac power_cs))) *}
   1.133 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack power_pack ctxt))) *}
   1.134  
   1.135  
   1.136  (* Some examples from Troelstra and van Dalen *)
     2.1 --- a/src/Sequents/LK.thy	Sat Feb 01 00:32:32 2014 +0000
     2.2 +++ b/src/Sequents/LK.thy	Sat Feb 01 17:56:03 2014 +0100
     2.3 @@ -35,8 +35,7 @@
     2.4    "|- P & ~P <-> False"
     2.5    "|- ~P & P <-> False"
     2.6    "|- (P & Q) & R <-> P & (Q & R)"
     2.7 -  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
     2.8 -  done
     2.9 +  by (fast add!: subst)+
    2.10  
    2.11  lemma disj_simps:
    2.12    "|- P | True <-> True"
    2.13 @@ -46,14 +45,12 @@
    2.14    "|- P | P <-> P"
    2.15    "|- P | P | Q <-> P | Q"
    2.16    "|- (P | Q) | R <-> P | (Q | R)"
    2.17 -  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
    2.18 -  done
    2.19 +  by (fast add!: subst)+
    2.20  
    2.21  lemma not_simps:
    2.22    "|- ~ False <-> True"
    2.23    "|- ~ True <-> False"
    2.24 -  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
    2.25 -  done
    2.26 +  by (fast add!: subst)+
    2.27  
    2.28  lemma imp_simps:
    2.29    "|- (P --> False) <-> ~P"
    2.30 @@ -62,8 +59,7 @@
    2.31    "|- (True --> P) <-> P"
    2.32    "|- (P --> P) <-> True"
    2.33    "|- (P --> ~P) <-> ~P"
    2.34 -  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
    2.35 -  done
    2.36 +  by (fast add!: subst)+
    2.37  
    2.38  lemma iff_simps:
    2.39    "|- (True <-> P) <-> P"
    2.40 @@ -71,8 +67,7 @@
    2.41    "|- (P <-> P) <-> True"
    2.42    "|- (False <-> P) <-> ~P"
    2.43    "|- (P <-> False) <-> ~P"
    2.44 -  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
    2.45 -  done
    2.46 +  by (fast add!: subst)+
    2.47  
    2.48  lemma quant_simps:
    2.49    "!!P. |- (ALL x. P) <-> P"
    2.50 @@ -81,8 +76,7 @@
    2.51    "!!P. |- (EX x. P) <-> P"
    2.52    "!!P. |- (EX x. x=t & P(x)) <-> P(t)"
    2.53    "!!P. |- (EX x. t=x & P(x)) <-> P(t)"
    2.54 -  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
    2.55 -  done
    2.56 +  by (fast add!: subst)+
    2.57  
    2.58  
    2.59  subsection {* Miniscoping: pushing quantifiers in *}
    2.60 @@ -101,8 +95,7 @@
    2.61    "!!P Q. |- (EX x. P | Q(x)) <-> P | (EX x. Q(x))"
    2.62    "!!P Q. |- (EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q"
    2.63    "!!P Q. |- (EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"
    2.64 -  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
    2.65 -  done
    2.66 +  by (fast add!: subst)+
    2.67  
    2.68  text {*universal miniscoping*}
    2.69  lemma all_simps:
    2.70 @@ -112,27 +105,25 @@
    2.71    "!!P Q. |- (ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"
    2.72    "!!P Q. |- (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q"
    2.73    "!!P Q. |- (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"
    2.74 -  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
    2.75 -  done
    2.76 +  by (fast add!: subst)+
    2.77  
    2.78  text {*These are NOT supplied by default!*}
    2.79  lemma distrib_simps:
    2.80    "|- P & (Q | R) <-> P&Q | P&R"
    2.81    "|- (Q | R) & P <-> Q&P | R&P"
    2.82    "|- (P | Q --> R) <-> (P --> R) & (Q --> R)"
    2.83 -  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
    2.84 -  done
    2.85 +  by (fast add!: subst)+
    2.86  
    2.87  lemma P_iff_F: "|- ~P ==> |- (P <-> False)"
    2.88    apply (erule thinR [THEN cut])
    2.89 -  apply (tactic {* fast_tac LK_pack 1 *})
    2.90 +  apply fast
    2.91    done
    2.92  
    2.93  lemmas iff_reflection_F = P_iff_F [THEN iff_reflection]
    2.94  
    2.95  lemma P_iff_T: "|- P ==> |- (P <-> True)"
    2.96    apply (erule thinR [THEN cut])
    2.97 -  apply (tactic {* fast_tac LK_pack 1 *})
    2.98 +  apply fast
    2.99    done
   2.100  
   2.101  lemmas iff_reflection_T = P_iff_T [THEN iff_reflection]
   2.102 @@ -144,23 +135,20 @@
   2.103    "|- ~ ~ P <-> P"
   2.104    "|- (~P --> P) <-> P"
   2.105    "|- (~P <-> ~Q) <-> (P<->Q)"
   2.106 -  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
   2.107 -  done
   2.108 +  by (fast add!: subst)+
   2.109  
   2.110  
   2.111  subsection {* Named rewrite rules *}
   2.112  
   2.113  lemma conj_commute: "|- P&Q <-> Q&P"
   2.114    and conj_left_commute: "|- P&(Q&R) <-> Q&(P&R)"
   2.115 -  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
   2.116 -  done
   2.117 +  by (fast add!: subst)+
   2.118  
   2.119  lemmas conj_comms = conj_commute conj_left_commute
   2.120  
   2.121  lemma disj_commute: "|- P|Q <-> Q|P"
   2.122    and disj_left_commute: "|- P|(Q|R) <-> Q|(P|R)"
   2.123 -  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
   2.124 -  done
   2.125 +  by (fast add!: subst)+
   2.126  
   2.127  lemmas disj_comms = disj_commute disj_left_commute
   2.128  
   2.129 @@ -181,20 +169,19 @@
   2.130    and de_Morgan_conj: "|- (~(P & Q)) <-> (~P | ~Q)"
   2.131  
   2.132    and not_iff: "|- ~(P <-> Q) <-> (P <-> ~Q)"
   2.133 -  apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
   2.134 -  done
   2.135 +  by (fast add!: subst)+
   2.136  
   2.137  lemma imp_cong:
   2.138    assumes p1: "|- P <-> P'"
   2.139      and p2: "|- P' ==> |- Q <-> Q'"
   2.140    shows "|- (P-->Q) <-> (P'-->Q')"
   2.141    apply (tactic {* lemma_tac @{thm p1} 1 *})
   2.142 -  apply (tactic {* safe_tac LK_pack 1 *})
   2.143 +  apply safe
   2.144     apply (tactic {*
   2.145       REPEAT (rtac @{thm cut} 1 THEN
   2.146         DEPTH_SOLVE_1
   2.147           (resolve_tac [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
   2.148 -           safe_tac LK_pack 1) *})
   2.149 +           Cla.safe_tac @{context} 1) *})
   2.150    done
   2.151  
   2.152  lemma conj_cong:
   2.153 @@ -202,17 +189,16 @@
   2.154      and p2: "|- P' ==> |- Q <-> Q'"
   2.155    shows "|- (P&Q) <-> (P'&Q')"
   2.156    apply (tactic {* lemma_tac @{thm p1} 1 *})
   2.157 -  apply (tactic {* safe_tac LK_pack 1 *})
   2.158 +  apply safe
   2.159     apply (tactic {*
   2.160       REPEAT (rtac @{thm cut} 1 THEN
   2.161         DEPTH_SOLVE_1
   2.162           (resolve_tac [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
   2.163 -           safe_tac LK_pack 1) *})
   2.164 +           Cla.safe_tac @{context} 1) *})
   2.165    done
   2.166  
   2.167  lemma eq_sym_conv: "|- (x=y) <-> (y=x)"
   2.168 -  apply (tactic {* fast_tac (LK_pack add_safes @{thms subst}) 1 *})
   2.169 -  done
   2.170 +  by (fast add!: subst)
   2.171  
   2.172  ML_file "simpdata.ML"
   2.173  setup {* map_theory_simpset (put_simpset LK_ss) *}
   2.174 @@ -229,17 +215,17 @@
   2.175     apply (tactic {* simp_tac (@{context} addsimps @{thms if_P}) 2 *})
   2.176    apply (rule_tac P = "~Q" in cut)
   2.177     apply (tactic {* simp_tac (@{context} addsimps @{thms if_not_P}) 2 *})
   2.178 -  apply (tactic {* fast_tac LK_pack 1 *})
   2.179 +  apply fast
   2.180    done
   2.181  
   2.182  lemma if_cancel: "|- (if P then x else x) = x"
   2.183    apply (tactic {* lemma_tac @{thm split_if} 1 *})
   2.184 -  apply (tactic {* fast_tac LK_pack 1 *})
   2.185 +  apply fast
   2.186    done
   2.187  
   2.188  lemma if_eq_cancel: "|- (if x=y then y else x) = x"
   2.189    apply (tactic {* lemma_tac @{thm split_if} 1 *})
   2.190 -  apply (tactic {* safe_tac LK_pack 1 *})
   2.191 +  apply safe
   2.192    apply (rule symL)
   2.193    apply (rule basic)
   2.194    done
     3.1 --- a/src/Sequents/LK/Hard_Quantifiers.thy	Sat Feb 01 00:32:32 2014 +0000
     3.2 +++ b/src/Sequents/LK/Hard_Quantifiers.thy	Sat Feb 01 17:56:03 2014 +0100
     3.3 @@ -73,7 +73,7 @@
     3.4  lemma "|- ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &   
     3.5       ~(EX x. P(x)) --> (EX x. Q(x)) & (ALL x. Q(x)|R(x) --> S(x))   
     3.6      --> (EX x. P(x)&R(x))"
     3.7 -  by (tactic "pc_tac LK_pack 1")
     3.8 +  by pc
     3.9  
    3.10  text "Problem 25"
    3.11  lemma "|- (EX x. P(x)) &   
    3.12 @@ -87,7 +87,7 @@
    3.13  lemma "|- ((EX x. p(x)) <-> (EX x. q(x))) &        
    3.14        (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))    
    3.15    --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))"
    3.16 -  by (tactic "pc_tac LK_pack 1")
    3.17 +  by pc
    3.18  
    3.19  text "Problem 27"
    3.20  lemma "|- (EX x. P(x) & ~Q(x)) &    
    3.21 @@ -95,20 +95,20 @@
    3.22                (ALL x. M(x) & L(x) --> P(x)) &    
    3.23                ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))   
    3.24            --> (ALL x. M(x) --> ~L(x))"
    3.25 -  by (tactic "pc_tac LK_pack 1")
    3.26 +  by pc
    3.27  
    3.28  text "Problem 28.  AMENDED"
    3.29  lemma "|- (ALL x. P(x) --> (ALL x. Q(x))) &    
    3.30          ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &   
    3.31          ((EX x. S(x)) --> (ALL x. L(x) --> M(x)))   
    3.32      --> (ALL x. P(x) & L(x) --> M(x))"
    3.33 -  by (tactic "pc_tac LK_pack 1")
    3.34 +  by pc
    3.35  
    3.36  text "Problem 29.  Essentially the same as Principia Mathematica *11.71"
    3.37  lemma "|- (EX x. P(x)) & (EX y. Q(y))   
    3.38      --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->      
    3.39           (ALL x y. P(x) & Q(y) --> R(x) & S(y)))"
    3.40 -  by (tactic "pc_tac LK_pack 1")
    3.41 +  by pc
    3.42  
    3.43  text "Problem 30"
    3.44  lemma "|- (ALL x. P(x) | Q(x) --> ~ R(x)) &  
    3.45 @@ -161,7 +161,7 @@
    3.46          (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) &  
    3.47          ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))   
    3.48      --> (ALL x. EX y. R(x,y))"
    3.49 -  by (tactic "pc_tac LK_pack 1")
    3.50 +  by pc
    3.51  
    3.52  text "Problem 38"
    3.53  lemma "|- (ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) -->         
    3.54 @@ -169,7 +169,7 @@
    3.55           (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) &     
    3.56                   (~p(a) | ~(EX y. p(y) & r(x,y)) |                           
    3.57                   (EX z. EX w. p(z) & r(x,w) & r(w,z))))"
    3.58 -  by (tactic "pc_tac LK_pack 1")
    3.59 +  by pc
    3.60  
    3.61  text "Problem 39"
    3.62  lemma "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
    3.63 @@ -215,7 +215,7 @@
    3.64  
    3.65  text "Problem 48"
    3.66  lemma "|- (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
    3.67 -  by (tactic {* fast_tac (LK_pack add_safes @{thms subst}) 1 *})
    3.68 +  by (fast add!: subst)
    3.69  
    3.70  text "Problem 50"
    3.71  lemma "|- (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))"
    3.72 @@ -224,16 +224,16 @@
    3.73  text "Problem 51"
    3.74  lemma "|- (EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->   
    3.75           (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"
    3.76 -  by (tactic {* fast_tac (LK_pack add_safes @{thms subst}) 1 *})
    3.77 +  by (fast add!: subst)
    3.78  
    3.79  text "Problem 52"  (*Almost the same as 51. *)
    3.80  lemma "|- (EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->
    3.81           (EX w. ALL y. EX z. (ALL x. P(x,y) <-> x=z) <-> y=w)"
    3.82 -  by (tactic {* fast_tac (LK_pack add_safes @{thms subst}) 1 *})
    3.83 +  by (fast add!: subst)
    3.84  
    3.85  text "Problem 56"
    3.86  lemma "|- (ALL x.(EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
    3.87 -  by (tactic {* best_tac (LK_pack add_unsafes [@{thm symL}, @{thm subst}]) 1 *})
    3.88 +  by (best add: symL subst)
    3.89    (*requires tricker to orient the equality properly*)
    3.90  
    3.91  text "Problem 57"
    3.92 @@ -243,7 +243,7 @@
    3.93  
    3.94  text "Problem 58!"
    3.95  lemma "|- (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))"
    3.96 -  by (tactic {* fast_tac (LK_pack add_safes @{thms subst}) 1 *})
    3.97 +  by (fast add!: subst)
    3.98  
    3.99  text "Problem 59"
   3.100  (*Unification works poorly here -- the abstraction %sobj prevents efficient
     4.1 --- a/src/Sequents/LK/Nat.thy	Sat Feb 01 00:32:32 2014 +0000
     4.2 +++ b/src/Sequents/LK/Nat.thy	Sat Feb 01 17:56:03 2014 +0100
     4.3 @@ -37,7 +37,7 @@
     4.4  lemma Suc_n_not_n: "|- Suc(k) ~= k"
     4.5    apply (rule_tac n = k in induct)
     4.6    apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms Suc_neq_0}) 1 *})
     4.7 -  apply (tactic {* fast_tac (LK_pack add_safes @{thms Suc_inject_rule}) 1 *})
     4.8 +  apply (fast add!: Suc_inject_rule)
     4.9    done
    4.10  
    4.11  lemma add_0: "|- 0+n = n"
     5.1 --- a/src/Sequents/LK0.thy	Sat Feb 01 00:32:32 2014 +0000
     5.2 +++ b/src/Sequents/LK0.thy	Sat Feb 01 17:56:03 2014 +0100
     5.3 @@ -162,13 +162,13 @@
     5.4  
     5.5  
     5.6  (** If-and-only-if rules **)
     5.7 -lemma iffR: 
     5.8 +lemma iffR:
     5.9      "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
    5.10    apply (unfold iff_def)
    5.11    apply (assumption | rule conjR impR)+
    5.12    done
    5.13  
    5.14 -lemma iffL: 
    5.15 +lemma iffL:
    5.16      "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
    5.17    apply (unfold iff_def)
    5.18    apply (assumption | rule conjL impL basic)+
    5.19 @@ -210,28 +210,44 @@
    5.20  
    5.21  (*The rules of LK*)
    5.22  
    5.23 -ML {*
    5.24 -val prop_pack = empty_pack add_safes
    5.25 -                [@{thm basic}, @{thm refl}, @{thm TrueR}, @{thm FalseL},
    5.26 -                 @{thm conjL}, @{thm conjR}, @{thm disjL}, @{thm disjR}, @{thm impL}, @{thm impR},
    5.27 -                 @{thm notL}, @{thm notR}, @{thm iffL}, @{thm iffR}];
    5.28 +lemmas [safe] =
    5.29 +  iffR iffL
    5.30 +  notR notL
    5.31 +  impR impL
    5.32 +  disjR disjL
    5.33 +  conjR conjL
    5.34 +  FalseL TrueR
    5.35 +  refl basic
    5.36 +ML {* val prop_pack = Cla.get_pack @{context} *}
    5.37 +
    5.38 +lemmas [safe] = exL allR
    5.39 +lemmas [unsafe] = the_equality exR_thin allL_thin
    5.40 +ML {* val LK_pack = Cla.get_pack @{context} *}
    5.41  
    5.42 -val LK_pack = prop_pack add_safes   [@{thm allR}, @{thm exL}]
    5.43 -                        add_unsafes [@{thm allL_thin}, @{thm exR_thin}, @{thm the_equality}];
    5.44 +ML {*
    5.45 +  val LK_dup_pack =
    5.46 +    Cla.put_pack prop_pack @{context}
    5.47 +    |> fold_rev Cla.add_safe @{thms allR exL}
    5.48 +    |> fold_rev Cla.add_unsafe @{thms allL exR the_equality}
    5.49 +    |> Cla.get_pack;
    5.50 +*}
    5.51  
    5.52 -val LK_dup_pack = prop_pack add_safes   [@{thm allR}, @{thm exL}]
    5.53 -                            add_unsafes [@{thm allL}, @{thm exR}, @{thm the_equality}];
    5.54 +ML {*
    5.55 +  fun lemma_tac th i =
    5.56 +    rtac (@{thm thinR} RS @{thm cut}) i THEN
    5.57 +    REPEAT (rtac @{thm thinL} i) THEN
    5.58 +    rtac th i;
    5.59 +*}
    5.60  
    5.61  
    5.62 -fun lemma_tac th i =
    5.63 -    rtac (@{thm thinR} RS @{thm cut}) i THEN REPEAT (rtac @{thm thinL} i) THEN rtac th i;
    5.64 -*}
    5.65 +method_setup fast_prop =
    5.66 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.fast_tac (Cla.put_pack prop_pack ctxt))) *}
    5.67  
    5.68 -method_setup fast_prop = {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac prop_pack))) *}
    5.69 -method_setup fast = {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_pack))) *}
    5.70 -method_setup fast_dup = {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_dup_pack))) *}
    5.71 -method_setup best = {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_pack))) *}
    5.72 -method_setup best_dup = {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_dup_pack))) *}
    5.73 +method_setup fast_dup =
    5.74 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.fast_tac (Cla.put_pack LK_dup_pack ctxt))) *}
    5.75 +
    5.76 +method_setup best_dup =
    5.77 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack LK_dup_pack ctxt))) *}
    5.78  
    5.79  
    5.80  lemma mp_R:
    5.81 @@ -239,7 +255,7 @@
    5.82      and minor: "$H |- $E, $F, P"
    5.83    shows "$H |- $E, Q, $F"
    5.84    apply (rule thinRS [THEN cut], rule major)
    5.85 -  apply (tactic "step_tac LK_pack 1")
    5.86 +  apply step
    5.87    apply (rule thinR, rule minor)
    5.88    done
    5.89  
    5.90 @@ -248,7 +264,7 @@
    5.91      and minor: "$H, $G, Q |- $E"
    5.92    shows "$H, P, $G |- $E"
    5.93    apply (rule thinL [THEN cut], rule major)
    5.94 -  apply (tactic "step_tac LK_pack 1")
    5.95 +  apply step
    5.96    apply (rule thinL, rule minor)
    5.97    done
    5.98  
    5.99 @@ -301,10 +317,10 @@
   5.100  (** Equality **)
   5.101  
   5.102  lemma sym: "|- a=b --> b=a"
   5.103 -  by (tactic {* safe_tac (LK_pack add_safes [@{thm subst}]) 1 *})
   5.104 +  by (safe add!: subst)
   5.105  
   5.106  lemma trans: "|- a=b --> b=c --> a=c"
   5.107 -  by (tactic {* safe_tac (LK_pack add_safes [@{thm subst}]) 1 *})
   5.108 +  by (safe add!: subst)
   5.109  
   5.110  (* Symmetry of equality in hypotheses *)
   5.111  lemmas symL = sym [THEN L_of_imp]
     6.1 --- a/src/Sequents/Sequents.thy	Sat Feb 01 00:32:32 2014 +0000
     6.2 +++ b/src/Sequents/Sequents.thy	Sat Feb 01 17:56:03 2014 +0100
     6.3 @@ -7,6 +7,7 @@
     6.4  
     6.5  theory Sequents
     6.6  imports Pure
     6.7 +keywords "print_pack" :: diag
     6.8  begin
     6.9  
    6.10  setup Pure_Thy.old_appl_syntax_setup
    6.11 @@ -15,7 +16,8 @@
    6.12  
    6.13  typedecl o
    6.14  
    6.15 -(* Sequences *)
    6.16 +
    6.17 +subsection {* Sequences *}
    6.18  
    6.19  typedecl
    6.20   seq'
    6.21 @@ -25,7 +27,7 @@
    6.22   Seq1'         :: "o=>seq'"
    6.23  
    6.24  
    6.25 -(* concrete syntax *)
    6.26 +subsection {* Concrete syntax *}
    6.27  
    6.28  nonterminal seq and seqobj and seqcont
    6.29  
    6.30 @@ -141,6 +143,9 @@
    6.31  
    6.32  parse_translation {* [(@{syntax_const "_Side"}, K side_tr)] *}
    6.33  
    6.34 +
    6.35 +subsection {* Proof tools *}
    6.36 +
    6.37  ML_file "prover.ML"
    6.38  
    6.39  end
     7.1 --- a/src/Sequents/Washing.thy	Sat Feb 01 00:32:32 2014 +0000
     7.2 +++ b/src/Sequents/Washing.thy	Sat Feb 01 17:56:03 2014 +0100
     7.3 @@ -40,19 +40,16 @@
     7.4  (* a load of dirty clothes and two dollars gives you clean clothes *)
     7.5  
     7.6  lemma "dollar , dollar , dirty |- clean"
     7.7 -  apply (tactic {* best_tac (lazy_cs add_safes (@{thms changeI} @ @{thms load1I} @ @{thms washI} @ @{thms dryI})) 1 *})
     7.8 -  done
     7.9 +  by (tactic {* Cla.best_tac (Cla.put_pack lazy_pack @{context} |> fold Cla.add_safe @{thms changeI load1I washI dryI}) 1 *})
    7.10  
    7.11  (* order of premises doesn't matter *)
    7.12  
    7.13  lemma "dollar , dirty , dollar |- clean"
    7.14 -  apply (tactic {* best_tac (lazy_cs add_safes (@{thms changeI} @ @{thms load1I} @ @{thms washI} @ @{thms dryI})) 1 *})
    7.15 -  done
    7.16 +  by (tactic {* Cla.best_tac (Cla.put_pack lazy_pack @{context} |> fold Cla.add_safe @{thms changeI load1I washI dryI}) 1 *})
    7.17  
    7.18  (* alternative formulation *)
    7.19  
    7.20  lemma "dollar , dollar |- dirty -o clean"
    7.21 -  apply (tactic {* best_tac (lazy_cs add_safes (@{thms changeI} @ @{thms load1I} @ @{thms washI} @ @{thms dryI})) 1 *})
    7.22 -  done
    7.23 +  by (tactic {* Cla.best_tac (Cla.put_pack lazy_pack @{context} |> fold Cla.add_safe @{thms changeI load1I washI dryI}) 1 *})
    7.24  
    7.25  end
     8.1 --- a/src/Sequents/prover.ML	Sat Feb 01 00:32:32 2014 +0000
     8.2 +++ b/src/Sequents/prover.ML	Sat Feb 01 17:56:03 2014 +0100
     8.3 @@ -5,54 +5,114 @@
     8.4  Simple classical reasoner for the sequent calculus, based on "theorem packs".
     8.5  *)
     8.6  
     8.7 +signature CLA =
     8.8 +sig
     8.9 +  type pack
    8.10 +  val empty_pack: pack
    8.11 +  val get_pack: Proof.context -> pack
    8.12 +  val put_pack: pack -> Proof.context -> Proof.context
    8.13 +  val pretty_pack: Proof.context -> Pretty.T
    8.14 +  val add_safe: thm -> Proof.context -> Proof.context
    8.15 +  val add_unsafe: thm -> Proof.context -> Proof.context
    8.16 +  val safe_add: attribute
    8.17 +  val unsafe_add: attribute
    8.18 +  val method: (Proof.context -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
    8.19 +  val trace: bool Config.T
    8.20 +  val forms_of_seq: term -> term list
    8.21 +  val safe_tac: Proof.context -> int -> tactic
    8.22 +  val step_tac: Proof.context -> int -> tactic
    8.23 +  val pc_tac: Proof.context -> int -> tactic
    8.24 +  val fast_tac: Proof.context -> int -> tactic
    8.25 +  val best_tac: Proof.context -> int -> tactic
    8.26 +end;
    8.27  
    8.28 -(*Higher precedence than := facilitates use of references*)
    8.29 -infix 4 add_safes add_unsafes;
    8.30 -
    8.31 -structure Cla =
    8.32 +structure Cla: CLA =
    8.33  struct
    8.34  
    8.35 -datatype pack = Pack of thm list * thm list;
    8.36 -
    8.37 -val trace = Unsynchronized.ref false;
    8.38 +(** rule declarations **)
    8.39  
    8.40  (*A theorem pack has the form  (safe rules, unsafe rules)
    8.41    An unsafe rule is incomplete or introduces variables in subgoals,
    8.42    and is tried only when the safe rules are not applicable.  *)
    8.43  
    8.44 -fun less (rl1,rl2) = (nprems_of rl1) < (nprems_of rl2);
    8.45 +fun less (rl1, rl2) = Thm.nprems_of rl1 < Thm.nprems_of rl2;
    8.46 +val sort_rules = sort (make_ord less);
    8.47  
    8.48 -val empty_pack = Pack([],[]);
    8.49 +datatype pack = Pack of thm list * thm list;
    8.50 +
    8.51 +val empty_pack = Pack ([], []);
    8.52  
    8.53 -fun warn_duplicates [] = []
    8.54 -  | warn_duplicates dups =
    8.55 -      (warning (cat_lines ("Ignoring duplicate theorems:" ::
    8.56 -          map Display.string_of_thm_without_context dups));
    8.57 -       dups);
    8.58 +structure Pack = Generic_Data
    8.59 +(
    8.60 +  type T = pack;
    8.61 +  val empty = empty_pack;
    8.62 +  val extend = I;
    8.63 +  fun merge (Pack (safes, unsafes), Pack (safes', unsafes')) =
    8.64 +    Pack
    8.65 +     (sort_rules (Thm.merge_thms (safes, safes')),
    8.66 +      sort_rules (Thm.merge_thms (unsafes, unsafes')));
    8.67 +);
    8.68  
    8.69 -fun (Pack(safes,unsafes)) add_safes ths   = 
    8.70 -    let val dups = warn_duplicates (inter Thm.eq_thm_prop ths safes)
    8.71 -        val ths' = subtract Thm.eq_thm_prop dups ths
    8.72 -    in
    8.73 -        Pack(sort (make_ord less) (ths'@safes), unsafes)
    8.74 -    end;
    8.75 +val put_pack = Context.proof_map o Pack.put;
    8.76 +val get_pack = Pack.get o Context.Proof;
    8.77 +fun get_rules ctxt = let val Pack rules = get_pack ctxt in rules end;
    8.78 +
    8.79 +
    8.80 +(* print pack *)
    8.81  
    8.82 -fun (Pack(safes,unsafes)) add_unsafes ths = 
    8.83 -    let val dups = warn_duplicates (inter Thm.eq_thm_prop unsafes ths)
    8.84 -        val ths' = subtract Thm.eq_thm_prop dups ths
    8.85 -    in
    8.86 -        Pack(safes, sort (make_ord less) (ths'@unsafes))
    8.87 -    end;
    8.88 +fun pretty_pack ctxt =
    8.89 +  let val (safes, unsafes) = get_rules ctxt in
    8.90 +    Pretty.chunks
    8.91 +     [Pretty.big_list "safe rules:" (map (Display.pretty_thm ctxt) safes),
    8.92 +      Pretty.big_list "unsafe rules:" (map (Display.pretty_thm ctxt) unsafes)]
    8.93 +  end;
    8.94  
    8.95 -fun merge_pack (Pack(safes,unsafes), Pack(safes',unsafes')) =
    8.96 -        Pack(sort (make_ord less) (safes@safes'), 
    8.97 -             sort (make_ord less) (unsafes@unsafes'));
    8.98 +val _ =
    8.99 +  Outer_Syntax.command @{command_spec "print_pack"} "print pack of classical rules"
   8.100 +    (Scan.succeed (Toplevel.keep (Pretty.writeln o pretty_pack o Toplevel.context_of)));
   8.101  
   8.102  
   8.103 -fun print_pack (Pack(safes,unsafes)) =
   8.104 -  writeln (cat_lines
   8.105 -   (["Safe rules:"] @ map Display.string_of_thm_without_context safes @
   8.106 -    ["Unsafe rules:"] @ map Display.string_of_thm_without_context unsafes));
   8.107 +(* declare rules *)
   8.108 +
   8.109 +fun add_rule which th context = context |> Pack.map (fn Pack rules =>
   8.110 +  Pack (rules |> which (fn ths =>
   8.111 +    if member Thm.eq_thm_prop ths th then
   8.112 +      let
   8.113 +        val ctxt = Context.proof_of context;
   8.114 +        val _ =
   8.115 +          if Context_Position.is_visible ctxt then
   8.116 +            warning ("Ignoring duplicate theorems:\n" ^ Display.string_of_thm ctxt th)
   8.117 +          else ();
   8.118 +      in ths end
   8.119 +    else sort_rules (th :: ths))));
   8.120 +
   8.121 +val add_safe = Context.proof_map o add_rule apfst;
   8.122 +val add_unsafe = Context.proof_map o add_rule apsnd;
   8.123 +
   8.124 +
   8.125 +(* attributes *)
   8.126 +
   8.127 +val safe_add = Thm.declaration_attribute (add_rule apfst);
   8.128 +val unsafe_add = Thm.declaration_attribute (add_rule apsnd);
   8.129 +
   8.130 +val _ = Theory.setup
   8.131 +  (Attrib.setup @{binding safe} (Scan.succeed safe_add) "" #>
   8.132 +   Attrib.setup @{binding unsafe} (Scan.succeed unsafe_add) "");
   8.133 +
   8.134 +
   8.135 +(* proof method syntax *)
   8.136 +
   8.137 +fun method tac =
   8.138 +  Method.sections
   8.139 +   [Args.$$$ "add" -- Args.bang_colon >> K (I, safe_add),
   8.140 +    Args.$$$ "add" -- Args.colon >> K (I, unsafe_add)]
   8.141 +  >> K (SIMPLE_METHOD' o tac);
   8.142 +
   8.143 +
   8.144 +(** tactics **)
   8.145 +
   8.146 +val trace = Attrib.setup_config_bool @{binding cla_trace} (K false);
   8.147 +
   8.148  
   8.149  (*Returns the list of all formulas in the sequent*)
   8.150  fun forms_of_seq (Const(@{const_name "SeqO'"},_) $ P $ u) = P :: forms_of_seq u
   8.151 @@ -65,11 +125,10 @@
   8.152    -- checks that each concl formula looks like some subgoal formula.
   8.153    It SHOULD check order as well, using recursion rather than forall/exists*)
   8.154  fun could_res (seqp,seqc) =
   8.155 -      forall (fn Qc => exists (fn Qp => Term.could_unify (Qp,Qc)) 
   8.156 +      forall (fn Qc => exists (fn Qp => Term.could_unify (Qp,Qc))
   8.157                                (forms_of_seq seqp))
   8.158               (forms_of_seq seqc);
   8.159  
   8.160 -
   8.161  (*Tests whether two sequents or pairs of sequents could be resolved*)
   8.162  fun could_resolve_seq (prem,conc) =
   8.163    case (prem,conc) of
   8.164 @@ -102,7 +161,7 @@
   8.165    The list of rules is partitioned into 0, 1, 2 premises.
   8.166    The resulting tactic, gtac, tries to resolve with rules.
   8.167    If successful, it recursively applies nextac to the new subgoals only.
   8.168 -  Else fails.  (Treatment of goals due to Ph. de Groote) 
   8.169 +  Else fails.  (Treatment of goals due to Ph. de Groote)
   8.170    Bind (RESOLVE_THEN rules) to a variable: it preprocesses the rules. *)
   8.171  
   8.172  (*Takes rule lists separated in to 0, 1, 2, >2 premises.
   8.173 @@ -112,7 +171,7 @@
   8.174  fun RESOLVE_THEN rules =
   8.175    let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules;
   8.176        fun tac nextac i state = state |>
   8.177 -             (filseq_resolve_tac rls0 9999 i 
   8.178 +             (filseq_resolve_tac rls0 9999 i
   8.179                ORELSE
   8.180                (DETERM(filseq_resolve_tac rls1 9999 i) THEN  TRY(nextac i))
   8.181                ORELSE
   8.182 @@ -123,50 +182,54 @@
   8.183  
   8.184  
   8.185  (*repeated resolution applied to the designated goal*)
   8.186 -fun reresolve_tac rules = 
   8.187 -  let val restac = RESOLVE_THEN rules;  (*preprocessing done now*)
   8.188 -      fun gtac i = restac gtac i
   8.189 -  in  gtac  end; 
   8.190 +fun reresolve_tac rules =
   8.191 +  let
   8.192 +    val restac = RESOLVE_THEN rules;  (*preprocessing done now*)
   8.193 +    fun gtac i = restac gtac i;
   8.194 +  in gtac end;
   8.195  
   8.196  (*tries the safe rules repeatedly before the unsafe rules. *)
   8.197 -fun repeat_goal_tac (Pack(safes,unsafes)) = 
   8.198 -  let val restac  =    RESOLVE_THEN safes
   8.199 -      and lastrestac = RESOLVE_THEN unsafes;
   8.200 -      fun gtac i = restac gtac i  
   8.201 -                   ORELSE  (if !trace then
   8.202 -                                (print_tac "" THEN lastrestac gtac i)
   8.203 -                            else lastrestac gtac i)
   8.204 -  in  gtac  end; 
   8.205 +fun repeat_goal_tac ctxt =
   8.206 +  let
   8.207 +    val (safes, unsafes) = get_rules ctxt;
   8.208 +    val restac = RESOLVE_THEN safes;
   8.209 +    val lastrestac = RESOLVE_THEN unsafes;
   8.210 +    fun gtac i =
   8.211 +      restac gtac i ORELSE
   8.212 +       (if Config.get ctxt trace then print_tac "" THEN lastrestac gtac i
   8.213 +        else lastrestac gtac i)
   8.214 +  in gtac end;
   8.215  
   8.216  
   8.217  (*Tries safe rules only*)
   8.218 -fun safe_tac (Pack(safes,unsafes)) = reresolve_tac safes;
   8.219 -
   8.220 -val safe_goal_tac = safe_tac;   (*backwards compatibility*)
   8.221 +fun safe_tac ctxt = reresolve_tac (#1 (get_rules ctxt));
   8.222  
   8.223  (*Tries a safe rule or else a unsafe rule.  Single-step for tracing. *)
   8.224 -fun step_tac (pack as Pack(safes,unsafes)) =
   8.225 -    safe_tac pack  ORELSE'
   8.226 -    filseq_resolve_tac unsafes 9999;
   8.227 +fun step_tac ctxt =
   8.228 +  safe_tac ctxt ORELSE' filseq_resolve_tac (#2 (get_rules ctxt)) 9999;
   8.229  
   8.230  
   8.231  (* Tactic for reducing a goal, using Predicate Calculus rules.
   8.232     A decision procedure for Propositional Calculus, it is incomplete
   8.233 -   for Predicate-Calculus because of allL_thin and exR_thin.  
   8.234 +   for Predicate-Calculus because of allL_thin and exR_thin.
   8.235     Fails if it can do nothing.      *)
   8.236 -fun pc_tac pack = SELECT_GOAL (DEPTH_SOLVE (repeat_goal_tac pack 1));
   8.237 +fun pc_tac ctxt = SELECT_GOAL (DEPTH_SOLVE (repeat_goal_tac ctxt 1));
   8.238  
   8.239  
   8.240 -(*The following two tactics are analogous to those provided by 
   8.241 +(*The following two tactics are analogous to those provided by
   8.242    Provers/classical.  In fact, pc_tac is usually FASTER than fast_tac!*)
   8.243 -fun fast_tac pack =
   8.244 -  SELECT_GOAL (DEPTH_SOLVE (step_tac pack 1));
   8.245 +fun fast_tac ctxt =
   8.246 +  SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
   8.247 +
   8.248 +fun best_tac ctxt  =
   8.249 +  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1));
   8.250  
   8.251 -fun best_tac pack  = 
   8.252 -  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) 
   8.253 -               (step_tac pack 1));
   8.254 +val _ = Theory.setup
   8.255 +  (Method.setup @{binding safe} (method safe_tac) "" #>
   8.256 +   Method.setup @{binding step} (method step_tac) "" #>
   8.257 +   Method.setup @{binding pc} (method pc_tac) "" #>
   8.258 +   Method.setup @{binding fast} (method fast_tac) "" #>
   8.259 +   Method.setup @{binding best} (method best_tac) "");
   8.260  
   8.261  end;
   8.262  
   8.263 -
   8.264 -open Cla;
     9.1 --- a/src/Sequents/simpdata.ML	Sat Feb 01 00:32:32 2014 +0000
     9.2 +++ b/src/Sequents/simpdata.ML	Sat Feb 01 17:56:03 2014 +0100
     9.3 @@ -14,7 +14,7 @@
     9.4  fun atomize r =
     9.5   case concl_of r of
     9.6     Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) =>
     9.7 -     (case (forms_of_seq a, forms_of_seq c) of
     9.8 +     (case (Cla.forms_of_seq a, Cla.forms_of_seq c) of
     9.9          ([], [p]) =>
    9.10            (case p of
    9.11                 Const(@{const_name imp},_)$_$_ => atomize(r RS @{thm mp_R})
    9.12 @@ -28,18 +28,17 @@
    9.13   | _ => [r];
    9.14  
    9.15  (*Make meta-equalities.*)
    9.16 -fun mk_meta_eq th = case concl_of th of
    9.17 +fun mk_meta_eq ctxt th = case concl_of th of
    9.18      Const("==",_)$_$_           => th
    9.19    | Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) =>
    9.20 -        (case (forms_of_seq a, forms_of_seq c) of
    9.21 +        (case (Cla.forms_of_seq a, Cla.forms_of_seq c) of
    9.22               ([], [p]) =>
    9.23                   (case p of
    9.24                        (Const(@{const_name equal},_)$_$_)   => th RS @{thm eq_reflection}
    9.25                      | (Const(@{const_name iff},_)$_$_) => th RS @{thm iff_reflection}
    9.26                      | (Const(@{const_name Not},_)$_)      => th RS @{thm iff_reflection_F}
    9.27                      | _                       => th RS @{thm iff_reflection_T})
    9.28 -           | _ => error ("addsimps: unable to use theorem\n" ^
    9.29 -                         Display.string_of_thm_without_context th));
    9.30 +           | _ => error ("addsimps: unable to use theorem\n" ^ Display.string_of_thm ctxt th));
    9.31  
    9.32  (*Replace premises x=y, X<->Y by X==Y*)
    9.33  fun mk_meta_prems ctxt =
    9.34 @@ -48,7 +47,7 @@
    9.35  
    9.36  (*Congruence rules for = or <-> (instead of ==)*)
    9.37  fun mk_meta_cong ctxt rl =
    9.38 -  Drule.zero_var_indexes (mk_meta_eq (mk_meta_prems ctxt rl))
    9.39 +  Drule.zero_var_indexes (mk_meta_eq ctxt (mk_meta_prems ctxt rl))
    9.40      handle THM _ =>
    9.41        error("Premises and conclusion of congruence rules must use =-equality or <->");
    9.42  
    9.43 @@ -71,7 +70,7 @@
    9.44    setSSolver (mk_solver "safe" safe_solver)
    9.45    setSolver (mk_solver "unsafe" unsafe_solver)
    9.46    |> Simplifier.set_subgoaler asm_simp_tac
    9.47 -  |> Simplifier.set_mksimps (K (map mk_meta_eq o atomize o gen_all))
    9.48 +  |> Simplifier.set_mksimps (fn ctxt => map (mk_meta_eq ctxt) o atomize o gen_all)
    9.49    |> Simplifier.set_mkcong mk_meta_cong
    9.50    |> simpset_of;
    9.51