author  lcp 
Fri, 24 Jun 1994 10:45:02 +0200  
changeset 439  ad3f46c13f1e 
parent 270  d506ea00c825 
child 670  ff4c6691de9d 
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 

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 

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

28 
val cut_inst_tac: (string*string)list > thm > int > tactic 
0  29 
val dmatch_tac: thm list > int > tactic 
30 
val dresolve_tac: thm list > int > tactic 

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

32 
val dtac: thm > int >tactic 

33 
val etac: thm > int >tactic 

34 
val eq_assume_tac: int > tactic 

35 
val ematch_tac: thm list > int > tactic 

36 
val eresolve_tac: thm list > int > tactic 

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

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

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

40 
val flexflex_tac: tactic 

41 
val fold_goals_tac: thm list > tactic 

42 
val fold_tac: thm list > tactic 

43 
val forward_tac: thm list > int > tactic 

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

45 
val is_fact: thm > bool 

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

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

48 
val make_elim: thm > thm 

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

50 
val match_tac: thm list > int > tactic 

51 
val metacut_tac: thm > int > tactic 

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

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

54 
val net_match_tac: thm list > int > tactic 

55 
val net_resolve_tac: thm list > int > tactic 

56 
val PRIMITIVE: (thm > thm) > tactic 

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

58 
val prune_params_tac: tactic 

59 
val rename_tac: string > int > tactic 

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

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

62 
val resolve_tac: thm list > int > tactic 

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

64 
val rewrite_goals_tac: thm list > tactic 

65 
val rewrite_tac: thm list > tactic 

66 
val rewtac: thm > tactic 

67 
val rtac: thm > int > tactic 

68 
val rule_by_tactic: tactic > thm > thm 

439  69 
val subgoal_tac: string > int > tactic 
70 
val subgoals_tac: string list > int > tactic 

0  71 
val subgoals_of_brl: bool * thm > int 
72 
val trace_goalno_tac: (int > tactic) > int > tactic 

73 
end 

74 
end; 

75 

76 

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

78 
Tactical: TACTICAL and Net: NET 

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

80 
struct 

81 
structure Tactical = Tactical; 

82 
structure Thm = Tactical.Thm; 

83 
structure Net = Net; 

84 
structure Sequence = Thm.Sequence; 

85 
structure Sign = Thm.Sign; 

86 
local open Tactical Tactical.Thm Drule 

87 
in 

88 

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

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

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

92 
None => Sequence.null 

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

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

95 

96 
fun string_of (a,0) = a 

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

98 

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

100 
fun freeze th = 

101 
let val fth = freezeT th 

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

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

230  104 
(cterm_of sign (Var(v,T)), 
105 
cterm_of sign (Free(string_of v, T))) 

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

108 

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

110 
fun rule_by_tactic (Tactic tf) rl = 

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

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

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

114 

115 
(*** Basic tactics ***) 

116 

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

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

119 
handle THM _ => Sequence.null); 

120 

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

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

123 

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

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

126 

127 
(*Solve subgoal i by assumption*) 

128 
fun assume_tac i = PRIMSEQ (assumption i); 

129 

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

131 
fun eq_assume_tac i = PRIMITIVE (eq_assumption i); 

132 

133 
(** Resolution/matching tactics **) 

134 

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

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

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

138 

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

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

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

142 

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

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

145 

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

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

148 

149 
(*Resolution with elimination rules only*) 

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

151 

152 
(*Forward reasoning using destruction rules.*) 

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

154 

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

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

157 

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

159 
fun rtac rl = resolve_tac [rl]; 

160 
fun etac rl = eresolve_tac [rl]; 

161 
fun dtac rl = dresolve_tac [rl]; 

162 
val atac = assume_tac; 

163 

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

165 
fun ares_tac rules = assume_tac ORELSE' resolve_tac rules; 

166 

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

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

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

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

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

172 

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

174 
val flexflex_tac = PRIMSEQ flexflex_rule; 

175 

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

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

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

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

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

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

182 
val paramTs = map #2 params 

183 
and inc = maxidx+1 

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

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

186 
fun liftterm t = list_abs_free (params, 

187 
Logic.incr_indexes(paramTs,inc) t) 

188 
(*Lifts instantiation pair over params*) 

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

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

195 
 types'(ixn) = types ixn; 

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

199 
end; 

200 

201 

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

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

204 

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

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

207 
STATE ( fn state => 

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

209 
nsubgoal) i 

210 
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

211 
 THM (msg,_,_) => (writeln msg; no_tac) ); 
0  212 

213 
(*Resolve version*) 

214 
fun res_inst_tac sinsts rule i = 

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

216 

217 
(*eresolve (elimination) version*) 

218 
fun eres_inst_tac sinsts rule i = 

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

220 

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

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

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

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

225 
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

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

227 
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

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

231 
in th end 

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

233 

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

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

235 
fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule); 
0  236 

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

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

238 
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

239 

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

240 
(*dresolve tactic applies a RULE to replace an assumption*) 
0  241 
fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule); 
242 

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

243 
(*** Applications of cut_rl ***) 
0  244 

245 
(*Used by metacut_tac*) 

246 
fun bires_cut_tac arg i = 

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

248 

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

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

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

252 

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

254 
fun is_fact rl = 

255 
case prems_of rl of 

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

257 

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

259 
fun cut_facts_tac ths i = 

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

261 

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

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

264 

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

267 

0  268 

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

270 

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

272 
using the predicate could(subgoal,concl). 

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

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

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

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

277 
 filtr (limit, th::ths) = 

278 
if limit=0 then [] 

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

280 
else filtr(limit,ths) 

281 
in filtr(limit,ths) end; 

282 

283 

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

285 

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

287 

288 
(*insert tags*) 

289 
fun taglist k [] = [] 

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

291 

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

293 
fun untaglist [] = [] 

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

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

296 
if k=k' then untaglist rest 

297 
else x :: untaglist rest; 

298 

299 
(*return list elements in original order*) 

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

301 

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

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

304 
if eres then 

305 
case prems_of th of 

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

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

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

309 

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

311 
fun build_netpair brls = 

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

313 

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

315 
fun biresolution_from_nets_tac match (inet,enet) = 

316 
SUBGOAL 

317 
(fn (prem,i) => 

318 
let val hyps = Logic.strip_assums_hyp prem 

319 
and concl = Logic.strip_assums_concl prem 

320 
val kbrls = Net.unify_term inet concl @ 

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

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

323 

324 
(*versions taking prebuilt nets*) 

325 
val biresolve_from_nets_tac = biresolution_from_nets_tac false; 

326 
val bimatch_from_nets_tac = biresolution_from_nets_tac true; 

327 

328 
(*fast versions using nets internally*) 

329 
val net_biresolve_tac = biresolve_from_nets_tac o build_netpair; 

330 
val net_bimatch_tac = bimatch_from_nets_tac o build_netpair; 

331 

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

333 

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

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

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

337 

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

339 
fun build_net rls = 

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

341 

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

343 
fun filt_resolution_from_net_tac match pred net = 

344 
SUBGOAL 

345 
(fn (prem,i) => 

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

347 
in 

348 
if pred krls 

349 
then PRIMSEQ 

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

351 
else no_tac 

352 
end); 

353 

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

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

356 
fun filt_resolve_tac rules maxr = 

357 
let fun pred krls = length krls <= maxr 

358 
in filt_resolution_from_net_tac false pred (build_net rules) end; 

359 

360 
(*versions taking prebuilt nets*) 

361 
val resolve_from_net_tac = filt_resolution_from_net_tac false (K true); 

362 
val match_from_net_tac = filt_resolution_from_net_tac true (K true); 

363 

364 
(*fast versions using nets internally*) 

365 
val net_resolve_tac = resolve_from_net_tac o build_net; 

366 
val net_match_tac = match_from_net_tac o build_net; 

367 

368 

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

370 

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

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

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

374 

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

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

377 

378 

379 
(*** MetaRewriting Tactics ***) 

380 

381 
fun result1 tacf mss thm = 

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

383 
None => None 

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

385 

386 
(*Rewrite subgoal i only *) 

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

387 
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

388 
PRIMITIVE(rewrite_goal_rule mode (result1 prover_tac) mss i); 
0  389 

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

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

391 
fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs); 
0  392 

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

394 
fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs); 
0  395 

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

396 
fun rewtac def = rewrite_goals_tac [def]; 
0  397 

398 

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

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

400 

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

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

402 
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

403 
 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

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

405 

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

406 
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

407 

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

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

409 
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

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

411 
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

412 
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

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

414 

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

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

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

417 

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

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

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

420 

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

421 

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

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

423 
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

424 
separated by blanks ***) 
0  425 

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

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

428 
fun rename_tac str i = 

429 
let val cs = explode str 

430 
in 

431 
if !Logic.auto_rename 

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

433 
Logic.auto_rename := false) 

434 
else (); 

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

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

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

438 
end; 

439 

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

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

442 
fun rename_last_tac a sufs i = 

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

444 
in if Syntax.is_identifier a 

445 
then PRIMITIVE (rename_params_rule (names,i)) 

446 
else all_tac 

447 
end; 

448 

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

450 
val prune_params_tac = rewrite_tac [triv_forall_equality]; 

451 

452 
end; 

453 
end; 