author  lcp 
Thu, 08 Dec 1994 11:26:25 +0100  
changeset 761  04320c295500 
parent 670  ff4c6691de9d 
child 922  196ca0973a6d 
permissions  rwrr 
0  1 
(* Title: tactic 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1991 University of Cambridge 

5 

6 
Tactics 

7 
*) 

8 

9 
signature TACTIC = 

10 
sig 

11 
structure Tactical: TACTICAL and Net: NET 

12 
local open Tactical Tactical.Thm Net 

13 
in 

14 
val ares_tac: thm list > int > tactic 

15 
val asm_rewrite_goal_tac: 

214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
191
diff
changeset

16 
bool*bool > (meta_simpset > tactic) > meta_simpset > int > tactic 
0  17 
val assume_tac: int > tactic 
18 
val atac: int >tactic 

670  19 
val bimatch_from_nets_tac: 
20 
(int*(bool*thm)) net * (int*(bool*thm)) net > int > tactic 

0  21 
val bimatch_tac: (bool*thm)list > int > tactic 
670  22 
val biresolve_from_nets_tac: 
23 
(int*(bool*thm)) net * (int*(bool*thm)) net > int > tactic 

0  24 
val biresolve_tac: (bool*thm)list > int > tactic 
25 
val build_net: thm list > (int*thm) net 

670  26 
val build_netpair: (int*(bool*thm)) net * (int*(bool*thm)) net > 
27 
(bool*thm)list > (int*(bool*thm)) net * (int*(bool*thm)) net 

0  28 
val compose_inst_tac: (string*string)list > (bool*thm*int) > int > tactic 
29 
val compose_tac: (bool * thm * int) > int > tactic 

30 
val cut_facts_tac: thm list > int > tactic 

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

31 
val cut_inst_tac: (string*string)list > thm > int > tactic 
0  32 
val dmatch_tac: thm list > int > tactic 
33 
val dresolve_tac: thm list > int > tactic 

34 
val dres_inst_tac: (string*string)list > thm > int > tactic 

35 
val dtac: thm > int >tactic 

36 
val etac: thm > int >tactic 

37 
val eq_assume_tac: int > tactic 

38 
val ematch_tac: thm list > int > tactic 

39 
val eresolve_tac: thm list > int > tactic 

40 
val eres_inst_tac: (string*string)list > thm > int > tactic 

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

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

43 
val flexflex_tac: tactic 

44 
val fold_goals_tac: thm list > tactic 

45 
val fold_tac: thm list > tactic 

46 
val forward_tac: thm list > int > tactic 

47 
val forw_inst_tac: (string*string)list > thm > int > tactic 

48 
val is_fact: thm > bool 

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

50 
val lift_inst_rule: thm * int * (string*string)list * thm > thm 

51 
val make_elim: thm > thm 

52 
val match_from_net_tac: (int*thm) net > int > tactic 

53 
val match_tac: thm list > int > tactic 

54 
val metacut_tac: thm > int > tactic 

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

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

57 
val net_match_tac: thm list > int > tactic 

58 
val net_resolve_tac: thm list > int > tactic 

59 
val PRIMITIVE: (thm > thm) > tactic 

60 
val PRIMSEQ: (thm > thm Sequence.seq) > tactic 

61 
val prune_params_tac: tactic 

62 
val rename_tac: string > int > tactic 

63 
val rename_last_tac: string > string list > int > tactic 

64 
val resolve_from_net_tac: (int*thm) net > int > tactic 

65 
val resolve_tac: thm list > int > tactic 

66 
val res_inst_tac: (string*string)list > thm > int > tactic 

67 
val rewrite_goals_tac: thm list > tactic 

68 
val rewrite_tac: thm list > tactic 

69 
val rewtac: thm > tactic 

70 
val rtac: thm > int > tactic 

71 
val rule_by_tactic: tactic > thm > thm 

439  72 
val subgoal_tac: string > int > tactic 
73 
val subgoals_tac: string list > int > tactic 

0  74 
val subgoals_of_brl: bool * thm > int 
75 
val trace_goalno_tac: (int > tactic) > int > tactic 

76 
end 

77 
end; 

78 

79 

80 
functor TacticFun (structure Logic: LOGIC and Drule: DRULE and 

81 
Tactical: TACTICAL and Net: NET 

82 
sharing Drule.Thm = Tactical.Thm) : TACTIC = 

83 
struct 

84 
structure Tactical = Tactical; 

85 
structure Thm = Tactical.Thm; 

86 
structure Net = Net; 

87 
structure Sequence = Thm.Sequence; 

88 
structure Sign = Thm.Sign; 

89 
local open Tactical Tactical.Thm Drule 

90 
in 

91 

92 
(*Discover what goal is chosen: SOMEGOAL(trace_goalno_tac tac) *) 

93 
fun trace_goalno_tac tf i = Tactic (fn state => 

94 
case Sequence.pull(tapply(tf i, state)) of 

95 
None => Sequence.null 

96 
 seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); 

97 
Sequence.seqof(fn()=> seqcell))); 

98 

99 
fun string_of (a,0) = a 

100 
 string_of (a,i) = a ^ "_" ^ string_of_int i; 

101 

102 
(*convert all Vars in a theorem to Frees  export??*) 

103 
fun freeze th = 

104 
let val fth = freezeT th 

105 
val {prop,sign,...} = rep_thm fth 

106 
fun mk_inst (Var(v,T)) = 

230  107 
(cterm_of sign (Var(v,T)), 
108 
cterm_of sign (Free(string_of v, T))) 

0  109 
val insts = map mk_inst (term_vars prop) 
110 
in instantiate ([],insts) fth end; 

111 

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

113 
fun rule_by_tactic (Tactic tf) rl = 

114 
case Sequence.pull(tf (freeze (standard rl))) of 

115 
None => raise THM("rule_by_tactic", 0, [rl]) 

116 
 Some(rl',_) => standard rl'; 

117 

118 
(*** Basic tactics ***) 

119 

120 
(*Makes a tactic whose effect on a state is given by thmfun: thm>thm seq.*) 

121 
fun PRIMSEQ thmfun = Tactic (fn state => thmfun state 

122 
handle THM _ => Sequence.null); 

123 

124 
(*Makes a tactic whose effect on a state is given by thmfun: thm>thm.*) 

125 
fun PRIMITIVE thmfun = PRIMSEQ (Sequence.single o thmfun); 

126 

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

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

129 

130 
(*Solve subgoal i by assumption*) 

131 
fun assume_tac i = PRIMSEQ (assumption i); 

132 

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

134 
fun eq_assume_tac i = PRIMITIVE (eq_assumption i); 

135 

136 
(** Resolution/matching tactics **) 

137 

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

139 
The arg = (bires_flg, orule, m) ; see bicompose for explanation.*) 

140 
fun compose_tac arg i = PRIMSEQ (bicompose false arg i); 

141 

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

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

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

145 

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

147 
fun biresolve_tac brules i = PRIMSEQ (biresolution false brules i); 

148 

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

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

151 

152 
(*Resolution with elimination rules only*) 

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

154 

155 
(*Forward reasoning using destruction rules.*) 

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

157 

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

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

160 

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

162 
fun rtac rl = resolve_tac [rl]; 

163 
fun etac rl = eresolve_tac [rl]; 

164 
fun dtac rl = dresolve_tac [rl]; 

165 
val atac = assume_tac; 

166 

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

168 
fun ares_tac rules = assume_tac ORELSE' resolve_tac rules; 

169 

170 
(*Matching tactics  as above, but forbid updating of state*) 

171 
fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i); 

172 
fun match_tac rules = bimatch_tac (map (pair false) rules); 

173 
fun ematch_tac rules = bimatch_tac (map (pair true) rules); 

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

175 

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

177 
val flexflex_tac = PRIMSEQ flexflex_rule; 

178 

179 
(*Lift and instantiate a rule wrt the given state and subgoal number *) 

180 
fun lift_inst_rule (state, i, sinsts, rule) = 

181 
let val {maxidx,sign,...} = rep_thm state 

182 
val (_, _, Bi, _) = dest_state(state,i) 

183 
val params = Logic.strip_params Bi (*params of subgoal i*) 

184 
val params = rev(rename_wrt_term Bi params) (*as they are printed*) 

185 
val paramTs = map #2 params 

186 
and inc = maxidx+1 

187 
fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs> incr_tvar inc T) 

188 
 liftvar t = raise TERM("Variable expected", [t]); 

189 
fun liftterm t = list_abs_free (params, 

190 
Logic.incr_indexes(paramTs,inc) t) 

191 
(*Lifts instantiation pair over params*) 

230  192 
fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct) 
0  193 
fun lifttvar((a,i),ctyp) = 
230  194 
let val {T,sign} = rep_ctyp ctyp 
195 
in ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end 

0  196 
val rts = types_sorts rule and (types,sorts) = types_sorts state 
197 
fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1)  sm => sm) 

198 
 types'(ixn) = types ixn; 

230  199 
val (Tinsts,insts) = read_insts sign rts (types',sorts) sinsts 
0  200 
in instantiate (map lifttvar Tinsts, map liftpair insts) 
201 
(lift_rule (state,i) rule) 

202 
end; 

203 

204 

205 
(*** Resolve after lifting and instantation; may refer to parameters of the 

206 
subgoal. Fails if "i" is out of range. ***) 

207 

208 
(*compose version: arguments are as for bicompose.*) 

209 
fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i = 

210 
STATE ( fn state => 

211 
compose_tac (bires_flg, lift_inst_rule (state, i, sinsts, rule), 

212 
nsubgoal) i 

213 
handle TERM (msg,_) => (writeln msg; no_tac) 

191
fe5d88d4c7e1
Pure/tactic/compose_inst_tac: when catching exception THM, prints the
lcp
parents:
69
diff
changeset

214 
 THM (msg,_,_) => (writeln msg; no_tac) ); 
0  215 

761  216 
(*"Resolve" version. Note: res_inst_tac cannot behave sensibly if the 
217 
terms that are substituted contain (term or type) unknowns from the 

218 
goal, because it is unable to instantiate goal unknowns at the same time. 

219 

220 
The type checker freezes all flexible type vars that were introduced during 

221 
type inference and still remain in the term at the end. This avoids the 

222 
introduction of flexible type vars in goals and other places where they 

223 
could cause complications. If you really want a flexible type var, you 

224 
have to put it in yourself as a constraint. 

225 

226 
This policy breaks down when a list of substitutions is type checked: later 

227 
pairs may force type instantiations in earlier pairs, which is impossible, 

228 
because the type vars in the earlier pairs are already frozen. 

229 
*) 

0  230 
fun res_inst_tac sinsts rule i = 
231 
compose_inst_tac sinsts (false, rule, nprems_of rule) i; 

232 

233 
(*eresolve (elimination) version*) 

234 
fun eres_inst_tac sinsts rule i = 

235 
compose_inst_tac sinsts (true, rule, nprems_of rule) i; 

236 

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

237 
(*For forw_inst_tac and dres_inst_tac. Preserve Var indexes of rl; 
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

238 
increment revcut_rl instead.*) 
0  239 
fun make_elim_preserve rl = 
270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

240 
let val {maxidx,...} = rep_thm rl 
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

241 
fun cvar ixn = cterm_of Sign.pure (Var(ixn,propT)); 
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

242 
val revcut_rl' = 
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

243 
instantiate ([], [(cvar("V",0), cvar("V",maxidx+1)), 
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

244 
(cvar("W",0), cvar("W",maxidx+1))]) revcut_rl 
0  245 
val arg = (false, rl, nprems_of rl) 
246 
val [th] = Sequence.list_of_s (bicompose false arg 1 revcut_rl') 

247 
in th end 

248 
handle Bind => raise THM("make_elim_preserve", 1, [rl]); 

249 

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

250 
(*instantiate and cut  for a FACT, anyway...*) 
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

251 
fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule); 
0  252 

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

253 
(*forward tactic applies a RULE to an assumption without deleting it*) 
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

254 
fun forw_inst_tac sinsts rule = cut_inst_tac sinsts rule THEN' assume_tac; 
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

255 

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

256 
(*dresolve tactic applies a RULE to replace an assumption*) 
0  257 
fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule); 
258 

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

259 
(*** Applications of cut_rl ***) 
0  260 

261 
(*Used by metacut_tac*) 

262 
fun bires_cut_tac arg i = 

263 
resolve_tac [cut_rl] i THEN biresolve_tac arg (i+1) ; 

264 

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

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

267 
fun metacut_tac rule = bires_cut_tac [(false,rule)]; 

268 

269 
(*Recognizes theorems that are not rules, but simple propositions*) 

270 
fun is_fact rl = 

271 
case prems_of rl of 

272 
[] => true  _::_ => false; 

273 

274 
(*"Cut" all facts from theorem list into the goal as assumptions. *) 

275 
fun cut_facts_tac ths i = 

276 
EVERY (map (fn th => metacut_tac th i) (filter is_fact ths)); 

277 

278 
(*Introduce the given proposition as a lemma and subgoal*) 

279 
fun subgoal_tac sprop = res_inst_tac [("psi", sprop)] cut_rl; 

280 

439  281 
(*Introduce a list of lemmas and subgoals*) 
282 
fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops); 

283 

0  284 

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

286 

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

288 
using the predicate could(subgoal,concl). 

289 
Resulting list is no longer than "limit"*) 

290 
fun filter_thms could (limit, prem, ths) = 

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

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

293 
 filtr (limit, th::ths) = 

294 
if limit=0 then [] 

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

296 
else filtr(limit,ths) 

297 
in filtr(limit,ths) end; 

298 

299 

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

301 

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

303 

304 
(*insert tags*) 

305 
fun taglist k [] = [] 

306 
 taglist k (x::xs) = (k,x) :: taglist (k+1) xs; 

307 

308 
(*remove tags and suppress duplicates  list is assumed sorted!*) 

309 
fun untaglist [] = [] 

310 
 untaglist [(k:int,x)] = [x] 

311 
 untaglist ((k,x) :: (rest as (k',x')::_)) = 

312 
if k=k' then untaglist rest 

313 
else x :: untaglist rest; 

314 

315 
(*return list elements in original order*) 

316 
val orderlist = untaglist o sort (fn(x,y)=> #1 x < #1 y); 

317 

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

319 
fun insert_kbrl (kbrl as (k,(eres,th)), (inet,enet)) = 

320 
if eres then 

321 
case prems_of th of 

322 
prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false)) 

323 
 [] => error"insert_kbrl: elimination rule with no premises" 

324 
else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet); 

325 

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

670  327 
fun build_netpair netpair brls = 
328 
foldr insert_kbrl (taglist 1 brls, netpair); 

0  329 

330 
(*biresolution using a pair of nets rather than rules*) 

331 
fun biresolution_from_nets_tac match (inet,enet) = 

332 
SUBGOAL 

333 
(fn (prem,i) => 

334 
let val hyps = Logic.strip_assums_hyp prem 

335 
and concl = Logic.strip_assums_concl prem 

336 
val kbrls = Net.unify_term inet concl @ 

337 
flat (map (Net.unify_term enet) hyps) 

338 
in PRIMSEQ (biresolution match (orderlist kbrls) i) end); 

339 

340 
(*versions taking prebuilt nets*) 

341 
val biresolve_from_nets_tac = biresolution_from_nets_tac false; 

342 
val bimatch_from_nets_tac = biresolution_from_nets_tac true; 

343 

344 
(*fast versions using nets internally*) 

670  345 
val net_biresolve_tac = 
346 
biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty); 

347 

348 
val net_bimatch_tac = 

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

0  350 

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

352 

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

354 
fun insert_krl (krl as (k,th), net) = 

355 
Net.insert_term ((concl_of th, krl), net, K false); 

356 

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

358 
fun build_net rls = 

359 
foldr insert_krl (taglist 1 rls, Net.empty); 

360 

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

362 
fun filt_resolution_from_net_tac match pred net = 

363 
SUBGOAL 

364 
(fn (prem,i) => 

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

366 
in 

367 
if pred krls 

368 
then PRIMSEQ 

369 
(biresolution match (map (pair false) (orderlist krls)) i) 

370 
else no_tac 

371 
end); 

372 

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

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

375 
fun filt_resolve_tac rules maxr = 

376 
let fun pred krls = length krls <= maxr 

377 
in filt_resolution_from_net_tac false pred (build_net rules) end; 

378 

379 
(*versions taking prebuilt nets*) 

380 
val resolve_from_net_tac = filt_resolution_from_net_tac false (K true); 

381 
val match_from_net_tac = filt_resolution_from_net_tac true (K true); 

382 

383 
(*fast versions using nets internally*) 

384 
val net_resolve_tac = resolve_from_net_tac o build_net; 

385 
val net_match_tac = match_from_net_tac o build_net; 

386 

387 

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

389 

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

391 
fun subgoals_of_brl (true,rule) = length (prems_of rule)  1 

392 
 subgoals_of_brl (false,rule) = length (prems_of rule); 

393 

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

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

396 

397 

398 
(*** MetaRewriting Tactics ***) 

399 

400 
fun result1 tacf mss thm = 

401 
case Sequence.pull(tapply(tacf mss,thm)) of 

402 
None => None 

403 
 Some(thm,_) => Some(thm); 

404 

405 
(*Rewrite subgoal i only *) 

214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
191
diff
changeset

406 
fun asm_rewrite_goal_tac mode prover_tac mss i = 
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
191
diff
changeset

407 
PRIMITIVE(rewrite_goal_rule mode (result1 prover_tac) mss i); 
0  408 

69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

409 
(*Rewrite throughout proof state. *) 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

410 
fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs); 
0  411 

412 
(*Rewrite subgoals only, not main goal. *) 

69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

413 
fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs); 
0  414 

69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

415 
fun rewtac def = rewrite_goals_tac [def]; 
0  416 

417 

69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

418 
(*** Tactic for folding definitions, handling critical pairs ***) 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

419 

e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

420 
(*The depth of nesting in a term*) 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

421 
fun term_depth (Abs(a,T,t)) = 1 + term_depth t 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

422 
 term_depth (f$t) = 1 + max [term_depth f, term_depth t] 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

423 
 term_depth _ = 0; 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

424 

e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

425 
val lhs_of_thm = #1 o Logic.dest_equals o #prop o rep_thm; 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

426 

e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

427 
(*folding should handle critical pairs! E.g. K == Inl(0), S == Inr(Inl(0)) 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

428 
Returns longest lhs first to avoid folding its subexpressions.*) 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

429 
fun sort_lhs_depths defs = 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

430 
let val keylist = make_keylist (term_depth o lhs_of_thm) defs 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

431 
val keys = distinct (sort op> (map #2 keylist)) 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

432 
in map (keyfilter keylist) keys end; 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

433 

e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

434 
fun fold_tac defs = EVERY 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

435 
(map rewrite_tac (sort_lhs_depths (map symmetric defs))); 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

436 

e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

437 
fun fold_goals_tac defs = EVERY 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

438 
(map rewrite_goals_tac (sort_lhs_depths (map symmetric defs))); 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

439 

e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

440 

e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

441 
(*** Renaming of parameters in a subgoal 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

442 
Names may contain letters, digits or primes and must be 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

443 
separated by blanks ***) 
0  444 

445 
(*Calling this will generate the warning "Same as previous level" since 

446 
it affects nothing but the names of bound variables!*) 

447 
fun rename_tac str i = 

448 
let val cs = explode str 

449 
in 

450 
if !Logic.auto_rename 

451 
then (writeln"Note: setting Logic.auto_rename := false"; 

452 
Logic.auto_rename := false) 

453 
else (); 

454 
case #2 (take_prefix (is_letdig orf is_blank) cs) of 

455 
[] => PRIMITIVE (rename_params_rule (scanwords is_letdig cs, i)) 

456 
 c::_ => error ("Illegal character: " ^ c) 

457 
end; 

458 

459 
(*Rename recent parameters using names generated from (a) and the suffixes, 

460 
provided the string (a), which represents a term, is an identifier. *) 

461 
fun rename_last_tac a sufs i = 

462 
let val names = map (curry op^ a) sufs 

463 
in if Syntax.is_identifier a 

464 
then PRIMITIVE (rename_params_rule (names,i)) 

465 
else all_tac 

466 
end; 

467 

468 
(*Prunes all redundant parameters from the proof state by rewriting*) 

469 
val prune_params_tac = rewrite_tac [triv_forall_equality]; 

470 

471 
end; 

472 
end; 