author  paulson 
Tue, 04 Feb 1997 10:33:58 +0100  
changeset 2580  e3f680709487 
parent 2228  f381c1a98209 
child 2672  85d7e800d754 
permissions  rwrr 
1460  1 
(* Title: tactic 
0  2 
ID: $Id$ 
1460  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1991 University of Cambridge 
5 

6 
Tactics 

7 
*) 

8 

9 
signature TACTIC = 

1501  10 
sig 
0  11 
val ares_tac: thm list > int > tactic 
12 
val asm_rewrite_goal_tac: 

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

13 
bool*bool > (meta_simpset > tactic) > meta_simpset > int > tactic 
0  14 
val assume_tac: int > tactic 
15 
val atac: int >tactic 

670  16 
val bimatch_from_nets_tac: 
1501  17 
(int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net > int > tactic 
0  18 
val bimatch_tac: (bool*thm)list > int > tactic 
670  19 
val biresolve_from_nets_tac: 
1501  20 
(int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net > int > tactic 
0  21 
val biresolve_tac: (bool*thm)list > int > tactic 
1501  22 
val build_net: thm list > (int*thm) Net.net 
23 
val build_netpair: (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net > 

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

0  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 
2029  29 
val defer_tac : int > tactic 
0  30 
val dmatch_tac: thm list > int > tactic 
31 
val dresolve_tac: thm list > int > tactic 

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

33 
val dtac: thm > int >tactic 

34 
val etac: thm > int >tactic 

35 
val eq_assume_tac: int > tactic 

36 
val ematch_tac: thm list > int > tactic 

37 
val eresolve_tac: thm list > int > tactic 

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

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

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

41 
val flexflex_tac: tactic 

42 
val fold_goals_tac: thm list > tactic 

43 
val fold_tac: thm list > tactic 

44 
val forward_tac: thm list > int > tactic 

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

2029  46 
val freeze_thaw: thm > thm * (thm > thm) 
1077
c2df11ae8b55
Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents:
952
diff
changeset

47 
val insert_tagged_brl: ('a*(bool*thm)) * 
1501  48 
(('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) > 
49 
('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net 

1801  50 
val delete_tagged_brl: (bool*thm) * 
51 
((int*(bool*thm))Net.net * (int*(bool*thm))Net.net) > 

52 
(int*(bool*thm))Net.net * (int*(bool*thm))Net.net 

0  53 
val is_fact: thm > bool 
54 
val lessb: (bool * thm) * (bool * thm) > bool 

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

56 
val make_elim: thm > thm 

1501  57 
val match_from_net_tac: (int*thm) Net.net > int > tactic 
0  58 
val match_tac: thm list > int > tactic 
59 
val metacut_tac: thm > int > tactic 

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

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

62 
val net_match_tac: thm list > int > tactic 

63 
val net_resolve_tac: thm list > int > tactic 

64 
val PRIMITIVE: (thm > thm) > tactic 

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

66 
val prune_params_tac: tactic 

67 
val rename_tac: string > int > tactic 

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

1501  69 
val resolve_from_net_tac: (int*thm) Net.net > int > tactic 
0  70 
val resolve_tac: thm list > int > tactic 
71 
val res_inst_tac: (string*string)list > thm > int > tactic 

72 
val rewrite_goals_tac: thm list > tactic 

73 
val rewrite_tac: thm list > tactic 

74 
val rewtac: thm > tactic 

1209  75 
val rotate_tac: int > int > tactic 
0  76 
val rtac: thm > int > tactic 
77 
val rule_by_tactic: tactic > thm > thm 

439  78 
val subgoal_tac: string > int > tactic 
79 
val subgoals_tac: string list > int > tactic 

0  80 
val subgoals_of_brl: bool * thm > int 
1975
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset

81 
val term_lift_inst_rule: 
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset

82 
thm * int * (indexname*typ)list * ((indexname*typ)*term)list * thm 
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset

83 
> thm 
1955
5309416236b6
Added thin_tac to signature; previous change was useless
paulson
parents:
1951
diff
changeset

84 
val thin_tac: string > int > tactic 
0  85 
val trace_goalno_tac: (int > tactic) > int > tactic 
1501  86 
end; 
0  87 

88 

1501  89 
structure Tactic : TACTIC = 
0  90 
struct 
91 

1501  92 
(*Discover which goal is chosen: SOMEGOAL(trace_goalno_tac tac) *) 
93 
fun trace_goalno_tac tac i st = 

94 
case Sequence.pull(tac i st) of 

1460  95 
None => Sequence.null 
0  96 
 seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); 
1501  97 
Sequence.seqof(fn()=> seqcell)); 
0  98 

99 

2029  100 
(*Convert all Vars in a theorem to Frees. Also return a function for 
101 
reversing that operation. DOES NOT WORK FOR TYPE VARIABLES.*) 

102 
local 

103 
fun string_of (a,0) = a 

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

105 
in 

106 
fun freeze_thaw th = 

107 
let val fth = freezeT th 

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

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

110 
(cterm_of sign (Var(v,T)), 

111 
cterm_of sign (Free(string_of v, T))) 

112 
val insts = map mk_inst (term_vars prop) 

113 
fun thaw th' = 

114 
th' > forall_intr_list (map #2 insts) 

115 
> forall_elim_list (map #1 insts) 

116 
in (instantiate ([],insts) fth, thaw) end; 

117 
end; 

118 

119 

120 
(*Rotates the given subgoal to be the last. Useful when replaying 

121 
an old proof script, when the proof of an early subgoal fails. 

122 
DOES NOT WORK FOR TYPE VARIABLES.*) 

123 
fun defer_tac i state = 

124 
let val (state',thaw) = freeze_thaw state 

125 
val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state')) 

2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2228
diff
changeset

126 
val hyp::hyps' = List.drop(hyps, i1) 
2029  127 
in implies_intr hyp (implies_elim_list state' (map assume hyps)) 
2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2228
diff
changeset

128 
> implies_intr_list (List.take(hyps, i1) @ hyps') 
2029  129 
> thaw 
130 
> Sequence.single 

131 
end 

132 
handle _ => Sequence.null; 

133 

0  134 

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

1501  136 
fun rule_by_tactic tac rl = 
2029  137 
case rl > standard > freeze_thaw > #1 > tac > Sequence.pull of 
1460  138 
None => raise THM("rule_by_tactic", 0, [rl]) 
0  139 
 Some(rl',_) => standard rl'; 
140 

141 
(*** Basic tactics ***) 

142 

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

1501  144 
fun PRIMSEQ thmfun st = thmfun st handle THM _ => Sequence.null; 
0  145 

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

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

148 

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

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

151 

152 
(*Solve subgoal i by assumption*) 

153 
fun assume_tac i = PRIMSEQ (assumption i); 

154 

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

156 
fun eq_assume_tac i = PRIMITIVE (eq_assumption i); 

157 

158 
(** Resolution/matching tactics **) 

159 

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

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

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

163 

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

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

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

167 

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

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

170 

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

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

173 

174 
(*Resolution with elimination rules only*) 

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

176 

177 
(*Forward reasoning using destruction rules.*) 

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

179 

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

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

182 

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

1460  184 
fun rtac rl = resolve_tac [rl]; 
185 
fun etac rl = eresolve_tac [rl]; 

186 
fun dtac rl = dresolve_tac [rl]; 

0  187 
val atac = assume_tac; 
188 

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

190 
fun ares_tac rules = assume_tac ORELSE' resolve_tac rules; 

191 

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

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

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

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

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

197 

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

199 
val flexflex_tac = PRIMSEQ flexflex_rule; 

200 

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

1501  202 
fun lift_inst_rule (st, i, sinsts, rule) = 
203 
let val {maxidx,sign,...} = rep_thm st 

204 
val (_, _, Bi, _) = dest_state(st,i) 

1460  205 
val params = Logic.strip_params Bi (*params of subgoal i*) 
0  206 
val params = rev(rename_wrt_term Bi params) (*as they are printed*) 
207 
val paramTs = map #2 params 

208 
and inc = maxidx+1 

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

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

211 
fun liftterm t = list_abs_free (params, 

1460  212 
Logic.incr_indexes(paramTs,inc) t) 
0  213 
(*Lifts instantiation pair over params*) 
230  214 
fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct) 
0  215 
fun lifttvar((a,i),ctyp) = 
1460  216 
let val {T,sign} = rep_ctyp ctyp 
217 
in ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end 

1501  218 
val rts = types_sorts rule and (types,sorts) = types_sorts st 
0  219 
fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1)  sm => sm) 
220 
 types'(ixn) = types ixn; 

949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
947
diff
changeset

221 
val used = add_term_tvarnames 
1501  222 
(#prop(rep_thm st) $ #prop(rep_thm rule),[]) 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
947
diff
changeset

223 
val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts 
0  224 
in instantiate (map lifttvar Tinsts, map liftpair insts) 
1501  225 
(lift_rule (st,i) rule) 
0  226 
end; 
227 

1966  228 
(*Like lift_inst_rule but takes cterms, not strings. 
229 
The cterms must be functions of the parameters of the subgoal, 

230 
i.e. they are assumed to be lifted already! 

231 
Also: types of Vars must be fully instantiated already *) 

1975
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset

232 
fun term_lift_inst_rule (st, i, Tinsts, insts, rule) = 
1966  233 
let val {maxidx,sign,...} = rep_thm st 
234 
val (_, _, Bi, _) = dest_state(st,i) 

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

236 
val paramTs = map #2 params 

237 
and inc = maxidx+1 

1975
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset

238 
fun liftvar ((a,j), T) = Var((a, j+inc), paramTs> incr_tvar inc T) 
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset

239 
(*lift only Var, not term, which must be lifted already*) 
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset

240 
fun liftpair (v,t) = (cterm_of sign (liftvar v), cterm_of sign t) 
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset

241 
fun liftTpair((a,i),T) = ((a,i+inc), ctyp_of sign (incr_tvar inc T)) 
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset

242 
in instantiate (map liftTpair Tinsts, map liftpair insts) 
1966  243 
(lift_rule (st,i) rule) 
244 
end; 

0  245 

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

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

248 

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

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

1501  251 
STATE ( fn st => 
252 
compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule), 

1460  253 
nsubgoal) i 
254 
handle TERM (msg,_) => (writeln msg; no_tac) 

255 
 THM (msg,_,_) => (writeln msg; no_tac) ); 

0  256 

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

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

260 

2029  261 
The type checker is instructed not to freeze flexible type vars that 
952
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

262 
were introduced during type inference and still remain in the term at the 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

263 
end. This increases flexibility but can introduce schematic type vars in 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

264 
goals. 
761  265 
*) 
0  266 
fun res_inst_tac sinsts rule i = 
267 
compose_inst_tac sinsts (false, rule, nprems_of rule) i; 

268 

1501  269 
(*eresolve elimination version*) 
0  270 
fun eres_inst_tac sinsts rule i = 
271 
compose_inst_tac sinsts (true, rule, nprems_of rule) i; 

272 

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

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

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

276 
let val {maxidx,...} = rep_thm rl 
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
761
diff
changeset

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

278 
val revcut_rl' = 
1460  279 
instantiate ([], [(cvar("V",0), cvar("V",maxidx+1)), 
280 
(cvar("W",0), cvar("W",maxidx+1))]) revcut_rl 

0  281 
val arg = (false, rl, nprems_of rl) 
282 
val [th] = Sequence.list_of_s (bicompose false arg 1 revcut_rl') 

283 
in th end 

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

285 

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

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

287 
fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule); 
0  288 

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

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

290 
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

291 

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

292 
(*dresolve tactic applies a RULE to replace an assumption*) 
0  293 
fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule); 
294 

1951  295 
(*Deletion of an assumption*) 
296 
fun thin_tac s = eres_inst_tac [("V",s)] thin_rl; 

297 

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

298 
(*** Applications of cut_rl ***) 
0  299 

300 
(*Used by metacut_tac*) 

301 
fun bires_cut_tac arg i = 

1460  302 
resolve_tac [cut_rl] i THEN biresolve_tac arg (i+1) ; 
0  303 

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

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

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

307 

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

309 
fun is_fact rl = 

310 
case prems_of rl of 

1460  311 
[] => true  _::_ => false; 
0  312 

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

314 
fun cut_facts_tac ths i = 

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

316 

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

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

319 

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

322 

0  323 

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

325 

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

1460  327 
using the predicate could(subgoal,concl). 
0  328 
Resulting list is no longer than "limit"*) 
329 
fun filter_thms could (limit, prem, ths) = 

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

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

1460  332 
 filtr (limit, th::ths) = 
333 
if limit=0 then [] 

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

335 
else filtr(limit,ths) 

0  336 
in filtr(limit,ths) end; 
337 

338 

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

340 

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

342 

343 
(*insert tags*) 

344 
fun taglist k [] = [] 

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

346 

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

348 
fun untaglist [] = [] 

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

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

351 
if k=k' then untaglist rest 

352 
else x :: untaglist rest; 

353 

354 
(*return list elements in original order*) 

2228
f381c1a98209
Etaexpansion of a function definition, for value polymorphism
paulson
parents:
2145
diff
changeset

355 
fun orderlist kbrls = untaglist (sort (fn(x,y)=> #1 x < #1 y) kbrls); 
0  356 

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

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

358 
fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) = 
0  359 
if eres then 
1460  360 
case prems_of th of 
361 
prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false)) 

362 
 [] => error"insert_tagged_brl: elimination rule with no premises" 

0  363 
else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet); 
364 

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

670  366 
fun build_netpair netpair brls = 
1077
c2df11ae8b55
Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents:
952
diff
changeset

367 
foldr insert_tagged_brl (taglist 1 brls, netpair); 
0  368 

1801  369 
(*delete one kbrl from the pair of nets; 
370 
we don't know the value of k, so we use 0 and ignore it in the comparison*) 

371 
local 

372 
fun eq_kbrl ((k,(eres,th)), (k',(eres',th'))) = eq_thm (th,th') 

373 
in 

374 
fun delete_tagged_brl (brl as (eres,th), (inet,enet)) = 

375 
if eres then 

376 
case prems_of th of 

377 
prem::_ => (inet, Net.delete_term ((prem, (0,brl)), enet, eq_kbrl)) 

378 
 [] => error"delete_brl: elimination rule with no premises" 

379 
else (Net.delete_term ((concl_of th, (0,brl)), inet, eq_kbrl), enet); 

380 
end; 

381 

382 

0  383 
(*biresolution using a pair of nets rather than rules*) 
384 
fun biresolution_from_nets_tac match (inet,enet) = 

385 
SUBGOAL 

386 
(fn (prem,i) => 

387 
let val hyps = Logic.strip_assums_hyp prem 

388 
and concl = Logic.strip_assums_concl prem 

389 
val kbrls = Net.unify_term inet concl @ 

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

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

392 

393 
(*versions taking prebuilt nets*) 

394 
val biresolve_from_nets_tac = biresolution_from_nets_tac false; 

395 
val bimatch_from_nets_tac = biresolution_from_nets_tac true; 

396 

397 
(*fast versions using nets internally*) 

670  398 
val net_biresolve_tac = 
399 
biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty); 

400 

401 
val net_bimatch_tac = 

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

0  403 

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

405 

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

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

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

409 

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

411 
fun build_net rls = 

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

413 

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

415 
fun filt_resolution_from_net_tac match pred net = 

416 
SUBGOAL 

417 
(fn (prem,i) => 

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

419 
in 

1460  420 
if pred krls 
0  421 
then PRIMSEQ 
1460  422 
(biresolution match (map (pair false) (orderlist krls)) i) 
0  423 
else no_tac 
424 
end); 

425 

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

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

428 
fun filt_resolve_tac rules maxr = 

429 
let fun pred krls = length krls <= maxr 

430 
in filt_resolution_from_net_tac false pred (build_net rules) end; 

431 

432 
(*versions taking prebuilt nets*) 

433 
val resolve_from_net_tac = filt_resolution_from_net_tac false (K true); 

434 
val match_from_net_tac = filt_resolution_from_net_tac true (K true); 

435 

436 
(*fast versions using nets internally*) 

437 
val net_resolve_tac = resolve_from_net_tac o build_net; 

438 
val net_match_tac = match_from_net_tac o build_net; 

439 

440 

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

442 

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

444 
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

445 
 subgoals_of_brl (false,rule) = nprems_of rule; 
0  446 

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

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

449 

450 

451 
(*** MetaRewriting Tactics ***) 

452 

453 
fun result1 tacf mss thm = 

1501  454 
case Sequence.pull(tacf mss thm) of 
0  455 
None => None 
456 
 Some(thm,_) => Some(thm); 

457 

2145  458 
(*Rewrite subgoal i only. SELECT_GOAL avoids inefficiencies in goals_conv.*) 
459 
fun asm_rewrite_goal_tac mode prover_tac mss = 

460 
SELECT_GOAL 

461 
(PRIMITIVE 

462 
(rewrite_goal_rule mode (result1 prover_tac) mss 1)); 

0  463 

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

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

465 
fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs); 
0  466 

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

468 
fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs); 
0  469 

1460  470 
fun rewtac def = rewrite_goals_tac [def]; 
0  471 

472 

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

474 

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

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

476 
fun term_depth (Abs(a,T,t)) = 1 + term_depth t 
2145  477 
 term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t) 
69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

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

479 

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

480 
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

481 

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

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

483 
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

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

485 
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

486 
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

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

488 

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

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

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

491 

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

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

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

494 

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

495 

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

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

497 
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

498 
separated by blanks ***) 
0  499 

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

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

502 
fun rename_tac str i = 

503 
let val cs = explode str 

504 
in 

505 
if !Logic.auto_rename 

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

1460  507 
Logic.auto_rename := false) 
0  508 
else (); 
509 
case #2 (take_prefix (is_letdig orf is_blank) cs) of 

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

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

512 
end; 

513 

1501  514 
(*Rename recent parameters using names generated from a and the suffixes, 
515 
provided the string a, which represents a term, is an identifier. *) 

0  516 
fun rename_last_tac a sufs i = 
517 
let val names = map (curry op^ a) sufs 

518 
in if Syntax.is_identifier a 

519 
then PRIMITIVE (rename_params_rule (names,i)) 

520 
else all_tac 

521 
end; 

522 

2043  523 
(*Prunes all redundant parameters from the proof state by rewriting. 
524 
DOES NOT rewrite main goal, where quantification over an unused bound 

525 
variable is sometimes done to avoid the need for cut_facts_tac.*) 

526 
val prune_params_tac = rewrite_goals_tac [triv_forall_equality]; 

0  527 

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

1209  530 
fun rotate_tac n = 
531 
let fun rot(n) = EVERY'(replicate n (dtac asm_rl)); 

532 
in if n >= 0 then rot n 

533 
else SUBGOAL (fn (t,i) => rot(length(Logic.strip_assums_hyp t)+n) i) 

534 
end; 

535 

0  536 
end; 
1501  537 

538 
open Tactic; 