author  paulson 
Fri, 28 Feb 1997 15:46:41 +0100  
changeset 2688  889a1cbd1aca 
parent 2672  85d7e800d754 
child 2814  a318f7f3a65c 
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 

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

64 
val orderlist: (int * 'a) list > 'a list 
0  65 
val PRIMITIVE: (thm > thm) > tactic 
66 
val PRIMSEQ: (thm > thm Sequence.seq) > tactic 

67 
val prune_params_tac: tactic 

68 
val rename_tac: string > int > tactic 

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

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

73 
val rewrite_goals_tac: thm list > tactic 

74 
val rewrite_tac: thm list > tactic 

75 
val rewtac: thm > tactic 

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

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

0  81 
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

82 
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

83 
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

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

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

89 

1501  90 
structure Tactic : TACTIC = 
0  91 
struct 
92 

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

95 
case Sequence.pull(tac i st) of 

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

100 

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

103 
local 

104 
fun string_of (a,0) = a 

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

106 
in 

107 
fun freeze_thaw th = 

108 
let val fth = freezeT th 

2688  109 
val vary = variant (add_term_names (#prop(rep_thm fth), [])) 
2029  110 
val {prop,sign,...} = rep_thm fth 
111 
fun mk_inst (Var(v,T)) = 

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

2688  113 
cterm_of sign (Free(vary (string_of v), T))) 
2029  114 
val insts = map mk_inst (term_vars prop) 
115 
fun thaw th' = 

116 
th' > forall_intr_list (map #2 insts) 

117 
> forall_elim_list (map #1 insts) 

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

119 
end; 

120 

121 

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

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

124 
DOES NOT WORK FOR TYPE VARIABLES.*) 

125 
fun defer_tac i state = 

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

127 
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

128 
val hyp::hyps' = List.drop(hyps, i1) 
2029  129 
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

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

133 
end 

134 
handle _ => Sequence.null; 

135 

0  136 

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

1501  138 
fun rule_by_tactic tac rl = 
2688  139 
let val (st, thaw) = freeze_thaw (zero_var_indexes rl) 
140 
in case Sequence.pull (tac st) of 

1460  141 
None => raise THM("rule_by_tactic", 0, [rl]) 
2688  142 
 Some(st',_) => Thm.varifyT (thaw st') 
143 
end; 

0  144 

145 
(*** Basic tactics ***) 

146 

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

1501  148 
fun PRIMSEQ thmfun st = thmfun st handle THM _ => Sequence.null; 
0  149 

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

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

152 

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

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

155 

156 
(*Solve subgoal i by assumption*) 

157 
fun assume_tac i = PRIMSEQ (assumption i); 

158 

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

160 
fun eq_assume_tac i = PRIMITIVE (eq_assumption i); 

161 

162 
(** Resolution/matching tactics **) 

163 

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

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

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

167 

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

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

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

171 

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

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

174 

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

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

177 

178 
(*Resolution with elimination rules only*) 

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

180 

181 
(*Forward reasoning using destruction rules.*) 

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

183 

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

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

186 

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

1460  188 
fun rtac rl = resolve_tac [rl]; 
189 
fun etac rl = eresolve_tac [rl]; 

190 
fun dtac rl = dresolve_tac [rl]; 

0  191 
val atac = assume_tac; 
192 

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

194 
fun ares_tac rules = assume_tac ORELSE' resolve_tac rules; 

195 

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

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

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

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

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

201 

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

203 
val flexflex_tac = PRIMSEQ flexflex_rule; 

204 

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

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

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

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

212 
and inc = maxidx+1 

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

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

215 
fun liftterm t = list_abs_free (params, 

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

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

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

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

227 
val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts 
0  228 
in instantiate (map lifttvar Tinsts, map liftpair insts) 
1501  229 
(lift_rule (st,i) rule) 
0  230 
end; 
231 

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

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

235 
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

236 
fun term_lift_inst_rule (st, i, Tinsts, insts, rule) = 
1966  237 
let val {maxidx,sign,...} = rep_thm st 
238 
val (_, _, Bi, _) = dest_state(st,i) 

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

240 
val paramTs = map #2 params 

241 
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

242 
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

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

244 
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

245 
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

246 
in instantiate (map liftTpair Tinsts, map liftpair insts) 
1966  247 
(lift_rule (st,i) rule) 
248 
end; 

0  249 

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

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

252 

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

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

1501  255 
STATE ( fn st => 
256 
compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule), 

1460  257 
nsubgoal) i 
258 
handle TERM (msg,_) => (writeln msg; no_tac) 

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

0  260 

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

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

264 

2029  265 
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

266 
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

267 
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

268 
goals. 
761  269 
*) 
0  270 
fun res_inst_tac sinsts rule i = 
271 
compose_inst_tac sinsts (false, rule, nprems_of rule) i; 

272 

1501  273 
(*eresolve elimination version*) 
0  274 
fun eres_inst_tac sinsts rule i = 
275 
compose_inst_tac sinsts (true, rule, nprems_of rule) i; 

276 

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

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

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

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

281 
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

282 
val revcut_rl' = 
1460  283 
instantiate ([], [(cvar("V",0), cvar("V",maxidx+1)), 
284 
(cvar("W",0), cvar("W",maxidx+1))]) revcut_rl 

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

287 
in th end 

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

289 

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

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

291 
fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule); 
0  292 

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

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

294 
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

295 

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

296 
(*dresolve tactic applies a RULE to replace an assumption*) 
0  297 
fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule); 
298 

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

301 

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

302 
(*** Applications of cut_rl ***) 
0  303 

304 
(*Used by metacut_tac*) 

305 
fun bires_cut_tac arg i = 

1460  306 
resolve_tac [cut_rl] i THEN biresolve_tac arg (i+1) ; 
0  307 

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

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

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

311 

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

313 
fun is_fact rl = 

314 
case prems_of rl of 

1460  315 
[] => true  _::_ => false; 
0  316 

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

318 
fun cut_facts_tac ths i = 

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

320 

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

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

323 

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

326 

0  327 

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

329 

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

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

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

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

1460  336 
 filtr (limit, th::ths) = 
337 
if limit=0 then [] 

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

339 
else filtr(limit,ths) 

0  340 
in filtr(limit,ths) end; 
341 

342 

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

344 

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

346 

347 
(*insert tags*) 

348 
fun taglist k [] = [] 

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

350 

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

352 
fun untaglist [] = [] 

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

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

355 
if k=k' then untaglist rest 

356 
else x :: untaglist rest; 

357 

358 
(*return list elements in original order*) 

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

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

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

362 
fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) = 
0  363 
if eres then 
1460  364 
case prems_of th of 
365 
prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false)) 

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

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

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

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

371 
foldr insert_tagged_brl (taglist 1 brls, netpair); 
0  372 

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

375 
local 

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

377 
in 

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

379 
if eres then 

380 
case prems_of th of 

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

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

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

384 
end; 

385 

386 

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

389 
SUBGOAL 

390 
(fn (prem,i) => 

391 
let val hyps = Logic.strip_assums_hyp prem 

392 
and concl = Logic.strip_assums_concl prem 

393 
val kbrls = Net.unify_term inet concl @ 

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

394 
List.concat (map (Net.unify_term enet) hyps) 
0  395 
in PRIMSEQ (biresolution match (orderlist kbrls) i) end); 
396 

397 
(*versions taking prebuilt nets*) 

398 
val biresolve_from_nets_tac = biresolution_from_nets_tac false; 

399 
val bimatch_from_nets_tac = biresolution_from_nets_tac true; 

400 

401 
(*fast versions using nets internally*) 

670  402 
val net_biresolve_tac = 
403 
biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty); 

404 

405 
val net_bimatch_tac = 

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

0  407 

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

409 

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

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

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

413 

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

415 
fun build_net rls = 

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

417 

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

419 
fun filt_resolution_from_net_tac match pred net = 

420 
SUBGOAL 

421 
(fn (prem,i) => 

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

423 
in 

1460  424 
if pred krls 
0  425 
then PRIMSEQ 
1460  426 
(biresolution match (map (pair false) (orderlist krls)) i) 
0  427 
else no_tac 
428 
end); 

429 

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

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

432 
fun filt_resolve_tac rules maxr = 

433 
let fun pred krls = length krls <= maxr 

434 
in filt_resolution_from_net_tac false pred (build_net rules) end; 

435 

436 
(*versions taking prebuilt nets*) 

437 
val resolve_from_net_tac = filt_resolution_from_net_tac false (K true); 

438 
val match_from_net_tac = filt_resolution_from_net_tac true (K true); 

439 

440 
(*fast versions using nets internally*) 

441 
val net_resolve_tac = resolve_from_net_tac o build_net; 

442 
val net_match_tac = match_from_net_tac o build_net; 

443 

444 

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

446 

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

448 
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

449 
 subgoals_of_brl (false,rule) = nprems_of rule; 
0  450 

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

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

453 

454 

455 
(*** MetaRewriting Tactics ***) 

456 

457 
fun result1 tacf mss thm = 

1501  458 
case Sequence.pull(tacf mss thm) of 
0  459 
None => None 
460 
 Some(thm,_) => Some(thm); 

461 

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

464 
SELECT_GOAL 

465 
(PRIMITIVE 

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

0  467 

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

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

469 
fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs); 
0  470 

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

472 
fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs); 
0  473 

1460  474 
fun rewtac def = rewrite_goals_tac [def]; 
0  475 

476 

1501  477 
(*** 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

478 

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

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

480 
fun term_depth (Abs(a,T,t)) = 1 + term_depth t 
2145  481 
 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

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

483 

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

484 
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

485 

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

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

487 
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

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

489 
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

490 
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

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

492 

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

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

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

495 

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

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

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

498 

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

499 

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

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

501 
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

502 
separated by blanks ***) 
0  503 

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

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

506 
fun rename_tac str i = 

507 
let val cs = explode str 

508 
in 

509 
if !Logic.auto_rename 

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

1460  511 
Logic.auto_rename := false) 
0  512 
else (); 
513 
case #2 (take_prefix (is_letdig orf is_blank) cs) of 

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

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

516 
end; 

517 

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

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

522 
in if Syntax.is_identifier a 

523 
then PRIMITIVE (rename_params_rule (names,i)) 

524 
else all_tac 

525 
end; 

526 

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

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

530 
val prune_params_tac = rewrite_goals_tac [triv_forall_equality]; 

0  531 

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

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

534 
fun rotate_tac 0 i = all_tac 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2580
diff
changeset

535 
 rotate_tac k i = PRIMITIVE (rotate_rule k i); 
1209  536 

0  537 
end; 
1501  538 

539 
open Tactic; 