author  lcp 
Fri, 10 Dec 1993 10:36:39 +0100  
changeset 191  fe5d88d4c7e1 
parent 69  e7588b53d6b0 
child 214  ed6a3e2b1a33 
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: 

16 
(meta_simpset > tactic) > meta_simpset > int > tactic 

17 
val assume_tac: int > tactic 

18 
val atac: int >tactic 

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

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

21 
val biresolve_from_nets_tac: (int*(bool*thm)) net * (int*(bool*thm)) net > int > tactic 

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

23 
val build_net: thm list > (int*thm) net 

24 
val build_netpair: (bool*thm)list > (int*(bool*thm)) net * (int*(bool*thm)) net 

25 
val compose_inst_tac: (string*string)list > (bool*thm*int) > int > tactic 

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

27 
val cut_facts_tac: thm list > int > tactic 

28 
val dmatch_tac: thm list > int > tactic 

29 
val dresolve_tac: thm list > int > tactic 

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

31 
val dtac: thm > int >tactic 

32 
val etac: thm > int >tactic 

33 
val eq_assume_tac: int > tactic 

34 
val ematch_tac: thm list > int > tactic 

35 
val eresolve_tac: thm list > int > tactic 

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

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

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

39 
val flexflex_tac: tactic 

40 
val fold_goals_tac: thm list > tactic 

41 
val fold_tac: thm list > tactic 

42 
val forward_tac: thm list > int > tactic 

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

44 
val is_fact: thm > bool 

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

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

47 
val make_elim: thm > thm 

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

49 
val match_tac: thm list > int > tactic 

50 
val metacut_tac: thm > int > tactic 

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

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

53 
val net_match_tac: thm list > int > tactic 

54 
val net_resolve_tac: thm list > int > tactic 

55 
val PRIMITIVE: (thm > thm) > tactic 

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

57 
val prune_params_tac: tactic 

58 
val rename_tac: string > int > tactic 

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

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

61 
val resolve_tac: thm list > int > tactic 

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

63 
val rewrite_goals_tac: thm list > tactic 

64 
val rewrite_tac: thm list > tactic 

65 
val rewtac: thm > tactic 

66 
val rtac: thm > int > tactic 

67 
val rule_by_tactic: tactic > thm > thm 

68 
val subgoals_of_brl: bool * thm > int 

69 
val subgoal_tac: string > int > tactic 

70 
val trace_goalno_tac: (int > tactic) > int > tactic 

71 
end 

72 
end; 

73 

74 

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

76 
Tactical: TACTICAL and Net: NET 

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

78 
struct 

79 
structure Tactical = Tactical; 

80 
structure Thm = Tactical.Thm; 

81 
structure Net = Net; 

82 
structure Sequence = Thm.Sequence; 

83 
structure Sign = Thm.Sign; 

84 
local open Tactical Tactical.Thm Drule 

85 
in 

86 

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

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

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

90 
None => Sequence.null 

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

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

93 

94 
fun string_of (a,0) = a 

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

96 

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

98 
fun freeze th = 

99 
let val fth = freezeT th 

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

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

102 
(Sign.cterm_of sign (Var(v,T)), 

103 
Sign.cterm_of sign (Free(string_of v, T))) 

104 
val insts = map mk_inst (term_vars prop) 

105 
in instantiate ([],insts) fth end; 

106 

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

108 
fun rule_by_tactic (Tactic tf) rl = 

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

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

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

112 

113 
(*** Basic tactics ***) 

114 

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

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

117 
handle THM _ => Sequence.null); 

118 

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

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

121 

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

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

124 

125 
(*Solve subgoal i by assumption*) 

126 
fun assume_tac i = PRIMSEQ (assumption i); 

127 

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

129 
fun eq_assume_tac i = PRIMITIVE (eq_assumption i); 

130 

131 
(** Resolution/matching tactics **) 

132 

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

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

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

136 

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

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

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

140 

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

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

143 

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

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

146 

147 
(*Resolution with elimination rules only*) 

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

149 

150 
(*Forward reasoning using destruction rules.*) 

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

152 

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

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

155 

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

157 
fun rtac rl = resolve_tac [rl]; 

158 
fun etac rl = eresolve_tac [rl]; 

159 
fun dtac rl = dresolve_tac [rl]; 

160 
val atac = assume_tac; 

161 

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

163 
fun ares_tac rules = assume_tac ORELSE' resolve_tac rules; 

164 

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

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

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

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

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

170 

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

172 
val flexflex_tac = PRIMSEQ flexflex_rule; 

173 

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

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

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

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

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

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

180 
val paramTs = map #2 params 

181 
and inc = maxidx+1 

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

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

184 
fun liftterm t = list_abs_free (params, 

185 
Logic.incr_indexes(paramTs,inc) t) 

186 
(*Lifts instantiation pair over params*) 

187 
fun liftpair (cv,ct) = (Sign.cfun liftvar cv, Sign.cfun liftterm ct) 

188 
fun lifttvar((a,i),ctyp) = 

189 
let val {T,sign} = Sign.rep_ctyp ctyp 

190 
in ((a,i+inc), Sign.ctyp_of sign (incr_tvar inc T)) end 

191 
val rts = types_sorts rule and (types,sorts) = types_sorts state 

192 
fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1)  sm => sm) 

193 
 types'(ixn) = types ixn; 

194 
val (Tinsts,insts) = Sign.read_insts sign rts (types',sorts) sinsts 

195 
in instantiate (map lifttvar Tinsts, map liftpair insts) 

196 
(lift_rule (state,i) rule) 

197 
end; 

198 

199 

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

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

202 

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

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

205 
STATE ( fn state => 

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

207 
nsubgoal) i 

208 
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

209 
 THM (msg,_,_) => (writeln msg; no_tac) ); 
0  210 

211 
(*Resolve version*) 

212 
fun res_inst_tac sinsts rule i = 

213 
compose_inst_tac sinsts (false, rule, nprems_of rule) i; 

214 

215 
(*eresolve (elimination) version*) 

216 
fun eres_inst_tac sinsts rule i = 

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

218 

219 
(*For forw_inst_tac and dres_inst_tac: preserve Var indexes of rl. 

220 
Fails if rl's major premise contains !! or ==> ; it should not anyway!*) 

221 
fun make_elim_preserve rl = 

222 
let val revcut_rl' = lift_rule (rl,1) revcut_rl 

223 
val arg = (false, rl, nprems_of rl) 

224 
val [th] = Sequence.list_of_s (bicompose false arg 1 revcut_rl') 

225 
in th end 

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

227 

228 
(*forward version*) 

229 
fun forw_inst_tac sinsts rule = 

230 
res_inst_tac sinsts (make_elim_preserve rule) THEN' assume_tac; 

231 

232 
(*dresolve version*) 

233 
fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule); 

234 

235 
(*** Applications of cut_rl  forward reasoning ***) 

236 

237 
(*Used by metacut_tac*) 

238 
fun bires_cut_tac arg i = 

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

240 

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

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

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

244 

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

246 
fun is_fact rl = 

247 
case prems_of rl of 

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

249 

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

251 
fun cut_facts_tac ths i = 

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

253 

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

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

256 

257 

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

259 

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

261 
using the predicate could(subgoal,concl). 

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

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

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

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

266 
 filtr (limit, th::ths) = 

267 
if limit=0 then [] 

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

269 
else filtr(limit,ths) 

270 
in filtr(limit,ths) end; 

271 

272 

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

274 

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

276 

277 
(*insert tags*) 

278 
fun taglist k [] = [] 

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

280 

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

282 
fun untaglist [] = [] 

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

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

285 
if k=k' then untaglist rest 

286 
else x :: untaglist rest; 

287 

288 
(*return list elements in original order*) 

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

290 

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

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

293 
if eres then 

294 
case prems_of th of 

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

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

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

298 

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

300 
fun build_netpair brls = 

301 
foldr insert_kbrl (taglist 1 brls, (Net.empty,Net.empty)); 

302 

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

304 
fun biresolution_from_nets_tac match (inet,enet) = 

305 
SUBGOAL 

306 
(fn (prem,i) => 

307 
let val hyps = Logic.strip_assums_hyp prem 

308 
and concl = Logic.strip_assums_concl prem 

309 
val kbrls = Net.unify_term inet concl @ 

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

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

312 

313 
(*versions taking prebuilt nets*) 

314 
val biresolve_from_nets_tac = biresolution_from_nets_tac false; 

315 
val bimatch_from_nets_tac = biresolution_from_nets_tac true; 

316 

317 
(*fast versions using nets internally*) 

318 
val net_biresolve_tac = biresolve_from_nets_tac o build_netpair; 

319 
val net_bimatch_tac = bimatch_from_nets_tac o build_netpair; 

320 

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

322 

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

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

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

326 

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

328 
fun build_net rls = 

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

330 

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

332 
fun filt_resolution_from_net_tac match pred net = 

333 
SUBGOAL 

334 
(fn (prem,i) => 

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

336 
in 

337 
if pred krls 

338 
then PRIMSEQ 

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

340 
else no_tac 

341 
end); 

342 

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

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

345 
fun filt_resolve_tac rules maxr = 

346 
let fun pred krls = length krls <= maxr 

347 
in filt_resolution_from_net_tac false pred (build_net rules) end; 

348 

349 
(*versions taking prebuilt nets*) 

350 
val resolve_from_net_tac = filt_resolution_from_net_tac false (K true); 

351 
val match_from_net_tac = filt_resolution_from_net_tac true (K true); 

352 

353 
(*fast versions using nets internally*) 

354 
val net_resolve_tac = resolve_from_net_tac o build_net; 

355 
val net_match_tac = match_from_net_tac o build_net; 

356 

357 

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

359 

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

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

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

363 

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

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

366 

367 

368 
(*** MetaRewriting Tactics ***) 

369 

370 
fun result1 tacf mss thm = 

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

372 
None => None 

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

374 

375 
(*Rewrite subgoal i only *) 

376 
fun asm_rewrite_goal_tac prover_tac mss i = 

377 
PRIMITIVE(rewrite_goal_rule (result1 prover_tac) mss i); 

378 

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

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

380 
fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs); 
0  381 

382 
(*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

383 
fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs); 
0  384 

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

385 
fun rewtac def = rewrite_goals_tac [def]; 
0  386 

387 

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

388 
(*** 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

389 

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

390 
(*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

391 
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

392 
 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

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

394 

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

395 
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

396 

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

397 
(*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

398 
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

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

400 
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

401 
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

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

403 

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

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

405 
(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

406 

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

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

408 
(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

409 

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

410 

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

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

412 
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

413 
separated by blanks ***) 
0  414 

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

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

417 
fun rename_tac str i = 

418 
let val cs = explode str 

419 
in 

420 
if !Logic.auto_rename 

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

422 
Logic.auto_rename := false) 

423 
else (); 

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

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

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

427 
end; 

428 

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

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

431 
fun rename_last_tac a sufs i = 

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

433 
in if Syntax.is_identifier a 

434 
then PRIMITIVE (rename_params_rule (names,i)) 

435 
else all_tac 

436 
end; 

437 

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

439 
val prune_params_tac = rewrite_tac [triv_forall_equality]; 

440 

441 
end; 

442 
end; 