author  wenzelm 
Wed, 29 May 2013 18:25:11 +0200  
changeset 52223  5bb6ae8acb87 
parent 52087  f3075fc4f5f6 
child 58837  e84d900cd287 
permissions  rwrr 
10805  1 
(* Title: Pure/tactic.ML 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

0  3 

29276  4 
Fundamental tactics. 
0  5 
*) 
6 

11774  7 
signature BASIC_TACTIC = 
8 
sig 

23223  9 
val trace_goalno_tac: (int > tactic) > int > tactic 
36546  10 
val rule_by_tactic: Proof.context > tactic > thm > thm 
23223  11 
val assume_tac: int > tactic 
12 
val eq_assume_tac: int > tactic 

13 
val compose_tac: (bool * thm * int) > int > tactic 

14 
val make_elim: thm > thm 

15 
val biresolve_tac: (bool * thm) list > int > tactic 

16 
val resolve_tac: thm list > int > tactic 

17 
val eresolve_tac: thm list > int > tactic 

18 
val forward_tac: thm list > int > tactic 

19 
val dresolve_tac: thm list > int > tactic 

20 
val atac: int > tactic 

21 
val rtac: thm > int > tactic 

31251  22 
val dtac: thm > int > tactic 
23 
val etac: thm > int > tactic 

24 
val ftac: thm > int > tactic 

23223  25 
val ares_tac: thm list > int > tactic 
26 
val solve_tac: thm list > int > tactic 

27 
val bimatch_tac: (bool * thm) list > int > tactic 

28 
val match_tac: thm list > int > tactic 

29 
val ematch_tac: thm list > int > tactic 

30 
val dmatch_tac: thm list > int > tactic 

31 
val flexflex_tac: tactic 

32 
val distinct_subgoal_tac: int > tactic 

33 
val distinct_subgoals_tac: tactic 

46704  34 
val cut_tac: thm > int > tactic 
23223  35 
val cut_rules_tac: thm list > int > tactic 
36 
val cut_facts_tac: thm list > int > tactic 

37 
val filter_thms: (term * term > bool) > int * term * thm list > thm list 

38 
val biresolution_from_nets_tac: ('a list > (bool * thm) list) > 

39 
bool > 'a Net.net * 'a Net.net > int > tactic 

40 
val biresolve_from_nets_tac: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net > 

41 
int > tactic 

42 
val bimatch_from_nets_tac: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net > 

43 
int > tactic 

44 
val net_biresolve_tac: (bool * thm) list > int > tactic 

45 
val net_bimatch_tac: (bool * thm) list > int > tactic 

46 
val filt_resolve_tac: thm list > int > int > tactic 

47 
val resolve_from_net_tac: (int * thm) Net.net > int > tactic 

48 
val match_from_net_tac: (int * thm) Net.net > int > tactic 

49 
val net_resolve_tac: thm list > int > tactic 

50 
val net_match_tac: thm list > int > tactic 

51 
val subgoals_of_brl: bool * thm > int 

52 
val lessb: (bool * thm) * (bool * thm) > bool 

27243
d549b5b0f344
removed obsolete global instantiation tactics (cf. Isar/rule_insts.ML);
wenzelm
parents:
27209
diff
changeset

53 
val rename_tac: string list > int > tactic 
23223  54 
val rotate_tac: int > int > tactic 
55 
val defer_tac: int > tactic 

49865  56 
val prefer_tac: int > tactic 
23223  57 
val filter_prems_tac: (term > bool) > int > tactic 
11774  58 
end; 
0  59 

11774  60 
signature TACTIC = 
61 
sig 

62 
include BASIC_TACTIC 

23223  63 
val insert_tagged_brl: 'a * (bool * thm) > 
64 
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net > 

65 
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net 

66 
val build_netpair: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net > 

67 
(bool * thm) list > (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net 

68 
val delete_tagged_brl: bool * thm > 

69 
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net > 

70 
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net 

71 
val eq_kbrl: ('a * (bool * thm)) * ('a * (bool * thm)) > bool 

32971  72 
val build_net: thm list > (int * thm) Net.net 
11774  73 
end; 
0  74 

11774  75 
structure Tactic: TACTIC = 
0  76 
struct 
77 

1501  78 
(*Discover which goal is chosen: SOMEGOAL(trace_goalno_tac tac) *) 
10817  79 
fun trace_goalno_tac tac i st = 
4270  80 
case Seq.pull(tac i st) of 
15531  81 
NONE => Seq.empty 
12262  82 
 seqcell => (tracing ("Subgoal " ^ string_of_int i ^ " selected"); 
10805  83 
Seq.make(fn()=> seqcell)); 
0  84 

85 
(*Makes a rule by applying a tactic to an existing rule*) 

36546  86 
fun rule_by_tactic ctxt tac rl = 
19925
3f9341831812
eliminated freeze/varify in favour of Variable.import/export/trade;
wenzelm
parents:
19743
diff
changeset

87 
let 
52087
f3075fc4f5f6
more precise treatment of theory vs. Proof.context;
wenzelm
parents:
51602
diff
changeset

88 
val thy = Proof_Context.theory_of ctxt; 
36546  89 
val ctxt' = Variable.declare_thm rl ctxt; 
52087
f3075fc4f5f6
more precise treatment of theory vs. Proof.context;
wenzelm
parents:
51602
diff
changeset

90 
val ((_, [st]), ctxt'') = Variable.import true [Thm.transfer thy rl] ctxt'; 
19925
3f9341831812
eliminated freeze/varify in favour of Variable.import/export/trade;
wenzelm
parents:
19743
diff
changeset

91 
in 
3f9341831812
eliminated freeze/varify in favour of Variable.import/export/trade;
wenzelm
parents:
19743
diff
changeset

92 
(case Seq.pull (tac st) of 
3f9341831812
eliminated freeze/varify in favour of Variable.import/export/trade;
wenzelm
parents:
19743
diff
changeset

93 
NONE => raise THM ("rule_by_tactic", 0, [rl]) 
36546  94 
 SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt'' ctxt') st')) 
2688  95 
end; 
10817  96 

19925
3f9341831812
eliminated freeze/varify in favour of Variable.import/export/trade;
wenzelm
parents:
19743
diff
changeset

97 

0  98 
(*** Basic tactics ***) 
99 

100 
(*** The following fail if the goal number is out of range: 

101 
thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *) 

102 

103 
(*Solve subgoal i by assumption*) 

31945  104 
fun assume_tac i = PRIMSEQ (Thm.assumption i); 
0  105 

106 
(*Solve subgoal i by assumption, using no unification*) 

31945  107 
fun eq_assume_tac i = PRIMITIVE (Thm.eq_assumption i); 
0  108 

23223  109 

0  110 
(** Resolution/matching tactics **) 
111 

112 
(*The composition rule/state: no lifting or var renaming. 

31945  113 
The arg = (bires_flg, orule, m); see Thm.bicompose for explanation.*) 
52223
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
52087
diff
changeset

114 
fun compose_tac arg i = 
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
52087
diff
changeset

115 
PRIMSEQ (Thm.bicompose {flatten = true, match = false, incremented = false} arg i); 
0  116 

117 
(*Converts a "destruct" rule like P&Q==>P to an "elimination" rule 

118 
like [ P&Q; P==>R ] ==> R *) 

119 
fun make_elim rl = zero_var_indexes (rl RS revcut_rl); 

120 

121 
(*Attack subgoal i by resolution, using flags to indicate elimination rules*) 

31945  122 
fun biresolve_tac brules i = PRIMSEQ (Thm.biresolution false brules i); 
0  123 

124 
(*Resolution: the simple case, works for introduction rules*) 

125 
fun resolve_tac rules = biresolve_tac (map (pair false) rules); 

126 

127 
(*Resolution with elimination rules only*) 

128 
fun eresolve_tac rules = biresolve_tac (map (pair true) rules); 

129 

130 
(*Forward reasoning using destruction rules.*) 

131 
fun forward_tac rls = resolve_tac (map make_elim rls) THEN' assume_tac; 

132 

133 
(*Like forward_tac, but deletes the assumption after use.*) 

134 
fun dresolve_tac rls = eresolve_tac (map make_elim rls); 

135 

136 
(*Shorthand versions: for resolution with a single theorem*) 

7491  137 
val atac = assume_tac; 
138 
fun rtac rl = resolve_tac [rl]; 

139 
fun dtac rl = dresolve_tac [rl]; 

1460  140 
fun etac rl = eresolve_tac [rl]; 
7491  141 
fun ftac rl = forward_tac [rl]; 
0  142 

143 
(*Use an assumption or some rules ... A popular combination!*) 

144 
fun ares_tac rules = assume_tac ORELSE' resolve_tac rules; 

145 

5263  146 
fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac; 
147 

0  148 
(*Matching tactics  as above, but forbid updating of state*) 
31945  149 
fun bimatch_tac brules i = PRIMSEQ (Thm.biresolution true brules i); 
0  150 
fun match_tac rules = bimatch_tac (map (pair false) rules); 
151 
fun ematch_tac rules = bimatch_tac (map (pair true) rules); 

152 
fun dmatch_tac rls = ematch_tac (map make_elim rls); 

153 

154 
(*Smash all flexflex disagreement pairs in the proof state.*) 

36944  155 
val flexflex_tac = PRIMSEQ Thm.flexflex_rule; 
0  156 

19056
6ac9dfe98e54
sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;
wenzelm
parents:
18977
diff
changeset

157 
(*Remove duplicate subgoals.*) 
50081  158 
val permute_tac = PRIMITIVE oo Thm.permute_prems; 
22560
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

159 
fun distinct_tac (i, k) = 
50081  160 
permute_tac 0 (i  1) THEN 
161 
permute_tac 1 (k  1) THEN 

51602
4c7fdc00bd59
tuned  Drule.comp_no_flatten includes Drule.incr_indexes already (NB: result should be deterministic by construction);
wenzelm
parents:
50239
diff
changeset

162 
PRIMITIVE (fn st => Drule.comp_no_flatten (st, 0) 1 Drule.distinct_prems_rl) THEN 
50081  163 
permute_tac 1 (1  k) THEN 
164 
permute_tac 0 (1  i); 

22560
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

165 

f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

166 
fun distinct_subgoal_tac i st = 
33957  167 
(case drop (i  1) (Thm.prems_of st) of 
22560
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

168 
[] => no_tac st 
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

169 
 A :: Bs => 
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

170 
st > EVERY (fold (fn (B, k) => 
23223  171 
if A aconv B then cons (distinct_tac (i, k)) else I) (Bs ~~ (1 upto length Bs)) [])); 
22560
f19ddf96c323
now exports distinct_subgoal_tac (needed by MetisAPI)
paulson
parents:
22360
diff
changeset

172 

10817  173 
fun distinct_subgoals_tac state = 
19056
6ac9dfe98e54
sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;
wenzelm
parents:
18977
diff
changeset

174 
let 
6ac9dfe98e54
sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;
wenzelm
parents:
18977
diff
changeset

175 
val goals = Thm.prems_of state; 
6ac9dfe98e54
sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;
wenzelm
parents:
18977
diff
changeset

176 
val dups = distinct (eq_fst (op aconv)) (goals ~~ (1 upto length goals)); 
6ac9dfe98e54
sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;
wenzelm
parents:
18977
diff
changeset

177 
in EVERY (rev (map (distinct_subgoal_tac o snd) dups)) state end; 
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset

178 

1951  179 

270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

180 
(*** Applications of cut_rl ***) 
0  181 

182 
(*The conclusion of the rule gets assumed in subgoal i, 

183 
while subgoal i+1,... are the premises of the rule.*) 

46704  184 
fun cut_tac rule i = rtac cut_rl i THEN rtac rule (i + 1); 
0  185 

13650
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13559
diff
changeset

186 
(*"Cut" a list of rules into the goal. Their premises will become new 
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13559
diff
changeset

187 
subgoals.*) 
46704  188 
fun cut_rules_tac ths i = EVERY (map (fn th => cut_tac th i) ths); 
13650
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13559
diff
changeset

189 

31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13559
diff
changeset

190 
(*As above, but inserts only facts (unconditional theorems); 
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13559
diff
changeset

191 
generates no additional subgoals. *) 
20232  192 
fun cut_facts_tac ths = cut_rules_tac (filter Thm.no_prems ths); 
0  193 

194 

195 
(**** Indexing and filtering of theorems ****) 

196 

197 
(*Returns the list of potentially resolvable theorems for the goal "prem", 

10805  198 
using the predicate could(subgoal,concl). 
0  199 
Resulting list is no longer than "limit"*) 
200 
fun filter_thms could (limit, prem, ths) = 

201 
let val pb = Logic.strip_assums_concl prem; (*delete assumptions*) 

202 
fun filtr (limit, []) = [] 

10805  203 
 filtr (limit, th::ths) = 
204 
if limit=0 then [] 

205 
else if could(pb, concl_of th) then th :: filtr(limit1, ths) 

206 
else filtr(limit,ths) 

0  207 
in filtr(limit,ths) end; 
208 

209 

210 
(*** biresolution and resolution using nets ***) 

211 

212 
(** To preserve the order of the rules, tag them with increasing integers **) 

213 

214 
(*insert one tagged brl into the pair of nets*) 

23178  215 
fun insert_tagged_brl (kbrl as (k, (eres, th))) (inet, enet) = 
12320  216 
if eres then 
217 
(case try Thm.major_prem_of th of 

16809  218 
SOME prem => (inet, Net.insert_term (K false) (prem, kbrl) enet) 
15531  219 
 NONE => error "insert_tagged_brl: elimination rule with no premises") 
16809  220 
else (Net.insert_term (K false) (concl_of th, kbrl) inet, enet); 
0  221 

222 
(*build a pair of nets for biresolution*) 

10817  223 
fun build_netpair netpair brls = 
30558
2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
29276
diff
changeset

224 
fold_rev insert_tagged_brl (tag_list 1 brls) netpair; 
0  225 

12320  226 
(*delete one kbrl from the pair of nets*) 
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
21708
diff
changeset

227 
fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th') 
16809  228 

23178  229 
fun delete_tagged_brl (brl as (eres, th)) (inet, enet) = 
13925  230 
(if eres then 
12320  231 
(case try Thm.major_prem_of th of 
16809  232 
SOME prem => (inet, Net.delete_term eq_kbrl (prem, ((), brl)) enet) 
15531  233 
 NONE => (inet, enet)) (*no major premise: ignore*) 
16809  234 
else (Net.delete_term eq_kbrl (Thm.concl_of th, ((), brl)) inet, enet)) 
13925  235 
handle Net.DELETE => (inet,enet); 
1801  236 

237 

10817  238 
(*biresolution using a pair of nets rather than rules. 
3706
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset

239 
function "order" must sort and possibly filter the list of brls. 
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset

240 
boolean "match" indicates matching or unification.*) 
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset

241 
fun biresolution_from_nets_tac order match (inet,enet) = 
0  242 
SUBGOAL 
243 
(fn (prem,i) => 

244 
let val hyps = Logic.strip_assums_hyp prem 

10817  245 
and concl = Logic.strip_assums_concl prem 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19473
diff
changeset

246 
val kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps 
31945  247 
in PRIMSEQ (Thm.biresolution match (order kbrls) i) end); 
0  248 

3706
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset

249 
(*versions taking prebuilt nets. No filtering of brls*) 
30558
2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
29276
diff
changeset

250 
val biresolve_from_nets_tac = biresolution_from_nets_tac order_list false; 
2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
29276
diff
changeset

251 
val bimatch_from_nets_tac = biresolution_from_nets_tac order_list true; 
0  252 

253 
(*fast versions using nets internally*) 

670  254 
val net_biresolve_tac = 
255 
biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty); 

256 

257 
val net_bimatch_tac = 

258 
bimatch_from_nets_tac o build_netpair(Net.empty,Net.empty); 

0  259 

260 
(*** Simpler version for resolve_tac  only one net, and no hyps ***) 

261 

262 
(*insert one tagged rl into the net*) 

23178  263 
fun insert_krl (krl as (k,th)) = 
264 
Net.insert_term (K false) (concl_of th, krl); 

0  265 

266 
(*build a net of rules for resolution*) 

10817  267 
fun build_net rls = 
30558
2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
29276
diff
changeset

268 
fold_rev insert_krl (tag_list 1 rls) Net.empty; 
0  269 

270 
(*resolution using a net rather than rules; pred supports filt_resolve_tac*) 

271 
fun filt_resolution_from_net_tac match pred net = 

272 
SUBGOAL 

273 
(fn (prem,i) => 

274 
let val krls = Net.unify_term net (Logic.strip_assums_concl prem) 

10817  275 
in 
276 
if pred krls 

0  277 
then PRIMSEQ 
31945  278 
(Thm.biresolution match (map (pair false) (order_list krls)) i) 
0  279 
else no_tac 
280 
end); 

281 

282 
(*Resolve the subgoal using the rules (making a net) unless too flexible, 

283 
which means more than maxr rules are unifiable. *) 

10817  284 
fun filt_resolve_tac rules maxr = 
0  285 
let fun pred krls = length krls <= maxr 
286 
in filt_resolution_from_net_tac false pred (build_net rules) end; 

287 

288 
(*versions taking prebuilt nets*) 

289 
val resolve_from_net_tac = filt_resolution_from_net_tac false (K true); 

290 
val match_from_net_tac = filt_resolution_from_net_tac true (K true); 

291 

292 
(*fast versions using nets internally*) 

293 
val net_resolve_tac = resolve_from_net_tac o build_net; 

294 
val net_match_tac = match_from_net_tac o build_net; 

295 

296 

297 
(*** For Natural Deduction using (bires_flg, rule) pairs ***) 

298 

299 
(*The number of new subgoals produced by the brule*) 

1077
c2df11ae8b55
Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents:
952
diff
changeset

300 
fun subgoals_of_brl (true,rule) = nprems_of rule  1 
c2df11ae8b55
Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents:
952
diff
changeset

301 
 subgoals_of_brl (false,rule) = nprems_of rule; 
0  302 

303 
(*Lessthan test: for sorting to minimize number of new subgoals*) 

304 
fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2; 

305 

306 

27243
d549b5b0f344
removed obsolete global instantiation tactics (cf. Isar/rule_insts.ML);
wenzelm
parents:
27209
diff
changeset

307 
(*Renaming of parameters in a subgoal*) 
d549b5b0f344
removed obsolete global instantiation tactics (cf. Isar/rule_insts.ML);
wenzelm
parents:
27209
diff
changeset

308 
fun rename_tac xs i = 
50239  309 
case Library.find_first (not o Symbol_Pos.is_identifier) xs of 
15531  310 
SOME x => error ("Not an identifier: " ^ x) 
31945  311 
 NONE => PRIMITIVE (Thm.rename_params_rule (xs, i)); 
9535  312 

1501  313 
(*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from 
314 
right to left if n is positive, and from left to right if n is negative.*) 

2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2580
diff
changeset

315 
fun rotate_tac 0 i = all_tac 
31945  316 
 rotate_tac k i = PRIMITIVE (Thm.rotate_rule k i); 
1209  317 

7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6979
diff
changeset

318 
(*Rotates the given subgoal to be the last.*) 
31945  319 
fun defer_tac i = PRIMITIVE (Thm.permute_prems (i  1) 1); 
7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6979
diff
changeset

320 

49865  321 
(*Rotates the given subgoal to be the first.*) 
322 
fun prefer_tac i = PRIMITIVE (Thm.permute_prems (i  1) 1 #> Thm.permute_prems 0 ~1); 

323 

5974  324 
(* remove premises that do not satisfy p; fails if all prems satisfy p *) 
325 
fun filter_prems_tac p = 

15531  326 
let fun Then NONE tac = SOME tac 
327 
 Then (SOME tac) tac' = SOME(tac THEN' tac'); 

19473  328 
fun thins H (tac,n) = 
5974  329 
if p H then (tac,n+1) 
330 
else (Then tac (rotate_tac n THEN' etac thin_rl),0); 

331 
in SUBGOAL(fn (subg,n) => 

332 
let val Hs = Logic.strip_assums_hyp subg 

19473  333 
in case fst(fold thins Hs (NONE,0)) of 
15531  334 
NONE => no_tac  SOME tac => tac n 
5974  335 
end) 
336 
end; 

337 

0  338 
end; 
1501  339 

32971  340 
structure Basic_Tactic: BASIC_TACTIC = Tactic; 
341 
open Basic_Tactic; 