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 flex-flex 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)
|
|
209 |
| THM _ => no_tac );
|
|
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(limit-1, 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 pre-built 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 pre-built 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 |
(*Less-than 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 |
(*** Meta-Rewriting 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 |
|
|
379 |
(*Rewrite or fold throughout proof state. *)
|
|
380 |
fun rewrite_tac thms = PRIMITIVE(rewrite_rule thms);
|
|
381 |
fun fold_tac rths = rewrite_tac (map symmetric rths);
|
|
382 |
|
|
383 |
(*Rewrite subgoals only, not main goal. *)
|
|
384 |
fun rewrite_goals_tac thms = PRIMITIVE (rewrite_goals_rule thms);
|
|
385 |
fun fold_goals_tac rths = rewrite_goals_tac (map symmetric rths);
|
|
386 |
|
|
387 |
fun rewtac rth = rewrite_goals_tac [rth];
|
|
388 |
|
|
389 |
|
|
390 |
(** Renaming of parameters in a subgoal
|
|
391 |
Names may contain letters, digits or primes and must be
|
|
392 |
separated by blanks **)
|
|
393 |
|
|
394 |
(*Calling this will generate the warning "Same as previous level" since
|
|
395 |
it affects nothing but the names of bound variables!*)
|
|
396 |
fun rename_tac str i =
|
|
397 |
let val cs = explode str
|
|
398 |
in
|
|
399 |
if !Logic.auto_rename
|
|
400 |
then (writeln"Note: setting Logic.auto_rename := false";
|
|
401 |
Logic.auto_rename := false)
|
|
402 |
else ();
|
|
403 |
case #2 (take_prefix (is_letdig orf is_blank) cs) of
|
|
404 |
[] => PRIMITIVE (rename_params_rule (scanwords is_letdig cs, i))
|
|
405 |
| c::_ => error ("Illegal character: " ^ c)
|
|
406 |
end;
|
|
407 |
|
|
408 |
(*Rename recent parameters using names generated from (a) and the suffixes,
|
|
409 |
provided the string (a), which represents a term, is an identifier. *)
|
|
410 |
fun rename_last_tac a sufs i =
|
|
411 |
let val names = map (curry op^ a) sufs
|
|
412 |
in if Syntax.is_identifier a
|
|
413 |
then PRIMITIVE (rename_params_rule (names,i))
|
|
414 |
else all_tac
|
|
415 |
end;
|
|
416 |
|
|
417 |
(*Prunes all redundant parameters from the proof state by rewriting*)
|
|
418 |
val prune_params_tac = rewrite_tac [triv_forall_equality];
|
|
419 |
|
|
420 |
end;
|
|
421 |
end;
|