|
1 (* Title: tctical |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Tacticals |
|
7 *) |
|
8 |
|
9 infix 1 THEN THEN' THEN_BEST_FIRST; |
|
10 infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE'; |
|
11 |
|
12 |
|
13 signature TACTICAL = |
|
14 sig |
|
15 structure Thm : THM |
|
16 local open Thm in |
|
17 datatype tactic = Tactic of thm -> thm Sequence.seq |
|
18 val all_tac: tactic |
|
19 val ALLGOALS: (int -> tactic) -> tactic |
|
20 val APPEND: tactic * tactic -> tactic |
|
21 val APPEND': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
|
22 val BEST_FIRST: (thm -> bool) * (thm -> int) -> tactic -> tactic |
|
23 val BREADTH_FIRST: (thm -> bool) -> tactic -> tactic |
|
24 val CHANGED: tactic -> tactic |
|
25 val COND: (thm -> bool) -> tactic -> tactic -> tactic |
|
26 val DEPTH_FIRST: (thm -> bool) -> tactic -> tactic |
|
27 val DEPTH_SOLVE: tactic -> tactic |
|
28 val DEPTH_SOLVE_1: tactic -> tactic |
|
29 val DETERM: tactic -> tactic |
|
30 val EVERY: tactic list -> tactic |
|
31 val EVERY': ('a -> tactic) list -> 'a -> tactic |
|
32 val EVERY1: (int -> tactic) list -> tactic |
|
33 val FILTER: (thm -> bool) -> tactic -> tactic |
|
34 val FIRST: tactic list -> tactic |
|
35 val FIRST': ('a -> tactic) list -> 'a -> tactic |
|
36 val FIRST1: (int -> tactic) list -> tactic |
|
37 val FIRSTGOAL: (int -> tactic) -> tactic |
|
38 val goals_limit: int ref |
|
39 val has_fewer_prems: int -> thm -> bool |
|
40 val IF_UNSOLVED: tactic -> tactic |
|
41 val INTLEAVE: tactic * tactic -> tactic |
|
42 val INTLEAVE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
|
43 val METAHYPS: (thm list -> tactic) -> int -> tactic |
|
44 val no_tac: tactic |
|
45 val ORELSE: tactic * tactic -> tactic |
|
46 val ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
|
47 val pause_tac: tactic |
|
48 val print_tac: tactic |
|
49 val REPEAT1: tactic -> tactic |
|
50 val REPEAT: tactic -> tactic |
|
51 val REPEAT_DETERM: tactic -> tactic |
|
52 val REPEAT_FIRST: (int -> tactic) -> tactic |
|
53 val REPEAT_SOME: (int -> tactic) -> tactic |
|
54 val SELECT_GOAL: tactic -> int -> tactic |
|
55 val SOMEGOAL: (int -> tactic) -> tactic |
|
56 val STATE: (thm -> tactic) -> tactic |
|
57 val strip_context: term -> (string * typ) list * term list * term |
|
58 val SUBGOAL: ((term*int) -> tactic) -> int -> tactic |
|
59 val tapply: tactic * thm -> thm Sequence.seq |
|
60 val THEN: tactic * tactic -> tactic |
|
61 val THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
|
62 val THEN_BEST_FIRST: tactic * ((thm->bool) * (thm->int) * tactic) -> tactic |
|
63 val traced_tac: (thm -> (thm * thm Sequence.seq) option) -> tactic |
|
64 val tracify: bool ref -> tactic -> thm -> thm Sequence.seq |
|
65 val trace_BEST_FIRST: bool ref |
|
66 val trace_DEPTH_FIRST: bool ref |
|
67 val trace_REPEAT: bool ref |
|
68 val TRY: tactic -> tactic |
|
69 val TRYALL: (int -> tactic) -> tactic |
|
70 end |
|
71 end; |
|
72 |
|
73 |
|
74 functor TacticalFun (structure Logic: LOGIC and Drule: DRULE) : TACTICAL = |
|
75 struct |
|
76 structure Thm = Drule.Thm; |
|
77 structure Sequence = Thm.Sequence; |
|
78 structure Sign = Thm.Sign; |
|
79 local open Drule Thm |
|
80 in |
|
81 |
|
82 (**** Tactics ****) |
|
83 |
|
84 (*A tactic maps a proof tree to a sequence of proof trees: |
|
85 if length of sequence = 0 then the tactic does not apply; |
|
86 if length > 1 then backtracking on the alternatives can occur.*) |
|
87 |
|
88 datatype tactic = Tactic of thm -> thm Sequence.seq; |
|
89 |
|
90 fun tapply(Tactic tf, state) = tf (state); |
|
91 |
|
92 (*Makes a tactic from one that uses the components of the state.*) |
|
93 fun STATE tacfun = Tactic (fn state => tapply(tacfun state, state)); |
|
94 |
|
95 |
|
96 (*** LCF-style tacticals ***) |
|
97 |
|
98 (*the tactical THEN performs one tactic followed by another*) |
|
99 fun (Tactic tf1) THEN (Tactic tf2) = |
|
100 Tactic (fn state => Sequence.flats (Sequence.maps tf2 (tf1 state))); |
|
101 |
|
102 |
|
103 (*The tactical ORELSE uses the first tactic that returns a nonempty sequence. |
|
104 Like in LCF, ORELSE commits to either tac1 or tac2 immediately. |
|
105 Does not backtrack to tac2 if tac1 was initially chosen. *) |
|
106 fun (Tactic tf1) ORELSE (Tactic tf2) = |
|
107 Tactic (fn state => |
|
108 case Sequence.pull(tf1 state) of |
|
109 None => tf2 state |
|
110 | sequencecell => Sequence.seqof(fn()=> sequencecell)); |
|
111 |
|
112 |
|
113 (*The tactical APPEND combines the results of two tactics. |
|
114 Like ORELSE, but allows backtracking on both tac1 and tac2. |
|
115 The tactic tac2 is not applied until needed.*) |
|
116 fun (Tactic tf1) APPEND (Tactic tf2) = |
|
117 Tactic (fn state => Sequence.append(tf1 state, |
|
118 Sequence.seqof(fn()=> Sequence.pull (tf2 state)))); |
|
119 |
|
120 (*Like APPEND, but interleaves results of tac1 and tac2.*) |
|
121 fun (Tactic tf1) INTLEAVE (Tactic tf2) = |
|
122 Tactic (fn state => Sequence.interleave(tf1 state, |
|
123 Sequence.seqof(fn()=> Sequence.pull (tf2 state)))); |
|
124 |
|
125 (*Versions for combining tactic-valued functions, as in |
|
126 SOMEGOAL (resolve_tac rls THEN' assume_tac) *) |
|
127 fun tac1 THEN' tac2 = fn x => tac1 x THEN tac2 x; |
|
128 fun tac1 ORELSE' tac2 = fn x => tac1 x ORELSE tac2 x; |
|
129 fun tac1 APPEND' tac2 = fn x => tac1 x APPEND tac2 x; |
|
130 fun tac1 INTLEAVE' tac2 = fn x => tac1 x INTLEAVE tac2 x; |
|
131 |
|
132 (*passes all proofs through unchanged; identity of THEN*) |
|
133 val all_tac = Tactic (fn state => Sequence.single state); |
|
134 |
|
135 (*passes no proofs through; identity of ORELSE and APPEND*) |
|
136 val no_tac = Tactic (fn state => Sequence.null); |
|
137 |
|
138 |
|
139 (*Make a tactic deterministic by chopping the tail of the proof sequence*) |
|
140 fun DETERM (Tactic tf) = Tactic (fn state => |
|
141 case Sequence.pull (tf state) of |
|
142 None => Sequence.null |
|
143 | Some(x,_) => Sequence.cons(x, Sequence.null)); |
|
144 |
|
145 |
|
146 (*Conditional tactical: testfun controls which tactic to use next. |
|
147 Beware: due to eager evaluation, both thentac and elsetac are evaluated.*) |
|
148 fun COND testfun (Tactic thenf) (Tactic elsef) = Tactic (fn prf => |
|
149 if testfun prf then thenf prf else elsef prf); |
|
150 |
|
151 (*Do the tactic or else do nothing*) |
|
152 fun TRY tac = tac ORELSE all_tac; |
|
153 |
|
154 |
|
155 (*** List-oriented tactics ***) |
|
156 |
|
157 (* EVERY [tac1,...,tacn] equals tac1 THEN ... THEN tacn *) |
|
158 fun EVERY tacs = foldr (op THEN) (tacs, all_tac); |
|
159 |
|
160 (* EVERY' [tf1,...,tfn] i equals tf1 i THEN ... THEN tfn i *) |
|
161 fun EVERY' tfs = foldr (op THEN') (tfs, K all_tac); |
|
162 |
|
163 (*Apply every tactic to 1*) |
|
164 fun EVERY1 tfs = EVERY' tfs 1; |
|
165 |
|
166 (* FIRST [tac1,...,tacn] equals tac1 ORELSE ... ORELSE tacn *) |
|
167 fun FIRST tacs = foldr (op ORELSE) (tacs, no_tac); |
|
168 |
|
169 (* FIRST' [tf1,...,tfn] i equals tf1 i ORELSE ... ORELSE tfn i *) |
|
170 fun FIRST' tfs = foldr (op ORELSE') (tfs, K no_tac); |
|
171 |
|
172 (*Apply first tactic to 1*) |
|
173 fun FIRST1 tfs = FIRST' tfs 1; |
|
174 |
|
175 |
|
176 (*** Tracing tactics ***) |
|
177 |
|
178 (*Max number of goals to print -- set by user*) |
|
179 val goals_limit = ref 10; |
|
180 |
|
181 (*Print the current proof state and pass it on.*) |
|
182 val print_tac = Tactic (fn state => |
|
183 (print_goals (!goals_limit) state; Sequence.single state)); |
|
184 |
|
185 (*Pause until a line is typed -- if non-empty then fail. *) |
|
186 val pause_tac = Tactic (fn state => |
|
187 (prs"** Press RETURN to continue: "; |
|
188 if input(std_in,1) = "\n" then Sequence.single state |
|
189 else (prs"Goodbye\n"; Sequence.null))); |
|
190 |
|
191 exception TRACE_EXIT of thm |
|
192 and TRACE_QUIT; |
|
193 |
|
194 (*Handle all tracing commands for current state and tactic *) |
|
195 fun exec_trace_command flag (tf, state) = |
|
196 case input_line(std_in) of |
|
197 "\n" => tf state |
|
198 | "f\n" => Sequence.null |
|
199 | "o\n" => (flag:=false; tf state) |
|
200 | "x\n" => (prs"Exiting now\n"; raise (TRACE_EXIT state)) |
|
201 | "quit\n" => raise TRACE_QUIT |
|
202 | _ => (prs |
|
203 "Type RETURN to continue or...\n\ |
|
204 \ f - to fail here\n\ |
|
205 \ o - to switch tracing off\n\ |
|
206 \ x - to exit at this point\n\ |
|
207 \ quit - to abort this tracing run\n\ |
|
208 \** Well? " ; exec_trace_command flag (tf, state)); |
|
209 |
|
210 |
|
211 (*Extract from a tactic, a thm->thm seq function that handles tracing*) |
|
212 fun tracify flag (Tactic tf) state = |
|
213 if !flag then (print_goals (!goals_limit) state; |
|
214 prs"** Press RETURN to continue: "; |
|
215 exec_trace_command flag (tf,state)) |
|
216 else tf state; |
|
217 |
|
218 (*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*) |
|
219 fun traced_tac seqf = Tactic (fn st => |
|
220 Sequence.seqof (fn()=> seqf st |
|
221 handle TRACE_EXIT st' => Some(st', Sequence.null))); |
|
222 |
|
223 |
|
224 (*Tracing flags*) |
|
225 val trace_REPEAT= ref false |
|
226 and trace_DEPTH_FIRST = ref false |
|
227 and trace_BEST_FIRST = ref false; |
|
228 |
|
229 (*Deterministic REPEAT: only retains the first outcome; |
|
230 uses less space than REPEAT; tail recursive*) |
|
231 fun REPEAT_DETERM tac = |
|
232 let val tf = tracify trace_REPEAT tac |
|
233 fun drep st = |
|
234 case Sequence.pull(tf st) of |
|
235 None => Some(st, Sequence.null) |
|
236 | Some(st',_) => drep st' |
|
237 in traced_tac drep end; |
|
238 |
|
239 (*General REPEAT: maintains a stack of alternatives; tail recursive*) |
|
240 fun REPEAT tac = |
|
241 let val tf = tracify trace_REPEAT tac |
|
242 fun rep qs st = |
|
243 case Sequence.pull(tf st) of |
|
244 None => Some(st, Sequence.seqof(fn()=> repq qs)) |
|
245 | Some(st',q) => rep (q::qs) st' |
|
246 and repq [] = None |
|
247 | repq(q::qs) = case Sequence.pull q of |
|
248 None => repq qs |
|
249 | Some(st,q) => rep (q::qs) st |
|
250 in traced_tac (rep []) end; |
|
251 |
|
252 (*Repeat 1 or more times*) |
|
253 fun REPEAT1 tac = tac THEN REPEAT tac; |
|
254 |
|
255 |
|
256 (** Search tacticals **) |
|
257 |
|
258 (*Seaarches "satp" reports proof tree as satisfied*) |
|
259 fun DEPTH_FIRST satp tac = |
|
260 let val tf = tracify trace_DEPTH_FIRST tac |
|
261 fun depth [] = None |
|
262 | depth(q::qs) = |
|
263 case Sequence.pull q of |
|
264 None => depth qs |
|
265 | Some(st,stq) => |
|
266 if satp st then Some(st, Sequence.seqof(fn()=> depth(stq::qs))) |
|
267 else depth (tf st :: stq :: qs) |
|
268 in traced_tac (fn st => depth([Sequence.single st])) end; |
|
269 |
|
270 |
|
271 (*Predicate: Does the rule have fewer than n premises?*) |
|
272 fun has_fewer_prems n rule = (nprems_of rule < n); |
|
273 |
|
274 (*Apply a tactic if subgoals remain, else do nothing.*) |
|
275 val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac; |
|
276 |
|
277 (*Tactical to reduce the number of premises by 1. |
|
278 If no subgoals then it must fail! *) |
|
279 fun DEPTH_SOLVE_1 tac = STATE |
|
280 (fn state => |
|
281 (case nprems_of state of |
|
282 0 => no_tac |
|
283 | n => DEPTH_FIRST (has_fewer_prems n) tac)); |
|
284 |
|
285 (*Uses depth-first search to solve ALL subgoals*) |
|
286 val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1); |
|
287 |
|
288 (*** Best-first search ***) |
|
289 |
|
290 (*Insertion into priority queue of states *) |
|
291 fun insert (nth: int*thm, []) = [nth] |
|
292 | insert ((m,th), (n,th')::nths) = |
|
293 if n<m then (n,th') :: insert ((m,th), nths) |
|
294 else if n=m andalso eq_thm(th,th') |
|
295 then (n,th')::nths |
|
296 else (m,th)::(n,th')::nths; |
|
297 |
|
298 (*For creating output sequence*) |
|
299 fun some_of_list [] = None |
|
300 | some_of_list (x::l) = Some (x, Sequence.seqof (fn () => some_of_list l)); |
|
301 |
|
302 |
|
303 (* Best-first search for a state that satisfies satp (incl initial state) |
|
304 Function sizef estimates size of problem remaining (smaller means better). |
|
305 tactic tf0 sets up the initial priority queue, which is searched by tac. *) |
|
306 fun (Tactic tf0) THEN_BEST_FIRST (satp, sizef, tac) = |
|
307 let val tf = tracify trace_BEST_FIRST tac |
|
308 fun pairsize th = (sizef th, th); |
|
309 fun bfs (news,nprfs) = |
|
310 (case partition satp news of |
|
311 ([],nonsats) => next(foldr insert |
|
312 (map pairsize nonsats, nprfs)) |
|
313 | (sats,_) => some_of_list sats) |
|
314 and next [] = None |
|
315 | next ((n,prf)::nprfs) = |
|
316 (if !trace_BEST_FIRST |
|
317 then writeln("state size = " ^ string_of_int n ^ |
|
318 " queue length =" ^ string_of_int (length nprfs)) |
|
319 else (); |
|
320 bfs (Sequence.list_of_s (tf prf), nprfs)) |
|
321 fun tf st = bfs (Sequence.list_of_s (tf0 st), []) |
|
322 in traced_tac tf end; |
|
323 |
|
324 (*Ordinary best-first search, with no initial tactic*) |
|
325 fun BEST_FIRST (satp,sizef) tac = all_tac THEN_BEST_FIRST (satp,sizef,tac); |
|
326 |
|
327 (*Breadth-first search to satisfy satpred (including initial state) |
|
328 SLOW -- SHOULD NOT USE APPEND!*) |
|
329 fun BREADTH_FIRST satpred (Tactic tf) = |
|
330 let val tacf = Sequence.list_of_s o tf; |
|
331 fun bfs prfs = |
|
332 (case partition satpred prfs of |
|
333 ([],[]) => [] |
|
334 | ([],nonsats) => |
|
335 (prs("breadth=" ^ string_of_int(length nonsats) ^ "\n"); |
|
336 bfs (flat (map tacf nonsats))) |
|
337 | (sats,_) => sats) |
|
338 in Tactic (fn state => Sequence.s_of_list (bfs [state])) end; |
|
339 |
|
340 |
|
341 (** Filtering tacticals **) |
|
342 |
|
343 (*Returns all states satisfying the predicate*) |
|
344 fun FILTER pred (Tactic tf) = Tactic |
|
345 (fn state => Sequence.filters pred (tf state)); |
|
346 |
|
347 (*Returns all changed states*) |
|
348 fun CHANGED (Tactic tf) = |
|
349 Tactic (fn state => |
|
350 let fun diff st = not (eq_thm(state,st)) |
|
351 in Sequence.filters diff (tf state) |
|
352 end ); |
|
353 |
|
354 |
|
355 (*** Tacticals based on subgoal numbering ***) |
|
356 |
|
357 (*For n subgoals, performs tf(n) THEN ... THEN tf(1) |
|
358 Essential to work backwards since tf(i) may add/delete subgoals at i. *) |
|
359 fun ALLGOALS tf = |
|
360 let fun tac 0 = all_tac |
|
361 | tac n = tf(n) THEN tac(n-1) |
|
362 in Tactic(fn state => tapply(tac(nprems_of state), state)) end; |
|
363 |
|
364 (*For n subgoals, performs tf(n) ORELSE ... ORELSE tf(1) *) |
|
365 fun SOMEGOAL tf = |
|
366 let fun tac 0 = no_tac |
|
367 | tac n = tf(n) ORELSE tac(n-1) |
|
368 in Tactic(fn state => tapply(tac(nprems_of state), state)) end; |
|
369 |
|
370 (*For n subgoals, performs tf(1) ORELSE ... ORELSE tf(n). |
|
371 More appropriate than SOMEGOAL in some cases.*) |
|
372 fun FIRSTGOAL tf = |
|
373 let fun tac (i,n) = if i>n then no_tac else tf(i) ORELSE tac (i+1,n) |
|
374 in Tactic(fn state => tapply(tac(1, nprems_of state), state)) end; |
|
375 |
|
376 (*Repeatedly solve some using tf. *) |
|
377 fun REPEAT_SOME tf = REPEAT1 (SOMEGOAL (REPEAT1 o tf)); |
|
378 |
|
379 (*Repeatedly solve the first possible subgoal using tf. *) |
|
380 fun REPEAT_FIRST tf = REPEAT1 (FIRSTGOAL (REPEAT1 o tf)); |
|
381 |
|
382 (*For n subgoals, tries to apply tf to n,...1 *) |
|
383 fun TRYALL tf = ALLGOALS (TRY o tf); |
|
384 |
|
385 |
|
386 (*Make a tactic for subgoal i, if there is one. *) |
|
387 fun SUBGOAL goalfun i = Tactic(fn state => |
|
388 case drop(i-1, prems_of state) of |
|
389 [] => Sequence.null |
|
390 | prem::_ => tapply(goalfun (prem,i), state)); |
|
391 |
|
392 (*Tactical for restricting the effect of a tactic to subgoal i. |
|
393 Works by making a new state from subgoal i, applying tf to it, and |
|
394 composing the resulting metathm with the original state. |
|
395 The "main goal" of the new state will not be atomic, some tactics may fail! |
|
396 DOES NOT work if tactic affects the main goal other than by instantiation.*) |
|
397 |
|
398 (* (!!x. ?V) ==> ?V ; used by protect_subgoal.*) |
|
399 val dummy_quant_rl = |
|
400 standard (forall_elim_var 0 (assume |
|
401 (Sign.read_cterm Sign.pure ("!!x. PROP V",propT)))); |
|
402 |
|
403 (* Prevent the subgoal's assumptions from becoming additional subgoals in the |
|
404 new proof state by enclosing them by a universal quantification *) |
|
405 fun protect_subgoal state i = |
|
406 case Sequence.chop (1, bicompose false (false,dummy_quant_rl,1) i state) |
|
407 of |
|
408 ([state'],_) => state' |
|
409 | _ => error"SELECT_GOAL -- impossible error???"; |
|
410 |
|
411 (*Does the work of SELECT_GOAL. *) |
|
412 fun select (Tactic tf) state i = |
|
413 let val prem::_ = drop(i-1, prems_of state) |
|
414 val st0 = trivial (Sign.cterm_of (#sign(rep_thm state)) prem); |
|
415 fun next st = bicompose false (false, st, nprems_of st) i state |
|
416 in Sequence.flats (Sequence.maps next (tf st0)) |
|
417 end; |
|
418 |
|
419 (*If i=1 and there is only one subgoal then do nothing!*) |
|
420 fun SELECT_GOAL tac i = Tactic (fn state => |
|
421 case (i, drop(i-1, prems_of state)) of |
|
422 (_,[]) => Sequence.null |
|
423 | (1,[_]) => tapply(tac,state) |
|
424 | (_, (Const("==>",_)$_$_) :: _) => select tac (protect_subgoal state i) i |
|
425 | (_, _::_) => select tac state i); |
|
426 |
|
427 |
|
428 |
|
429 (*Strips assumptions in goal yielding ( [x1,...,xm], [H1,...,Hn], B ) |
|
430 H1,...,Hn are the hypotheses; x1...xm are variants of the parameters. |
|
431 Main difference from strip_assums concerns parameters: |
|
432 it replaces the bound variables by free variables. *) |
|
433 fun strip_context_aux (params, Hs, Const("==>", _) $ H $ B) = |
|
434 strip_context_aux (params, H::Hs, B) |
|
435 | strip_context_aux (params, Hs, Const("all",_)$Abs(a,T,t)) = |
|
436 let val (b,u) = variant_abs(a,T,t) |
|
437 in strip_context_aux ((b,T)::params, Hs, u) end |
|
438 | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B); |
|
439 |
|
440 fun strip_context A = strip_context_aux ([],[],A); |
|
441 |
|
442 |
|
443 (**** METAHYPS -- tactical for using hypotheses as meta-level assumptions |
|
444 METAHYPS (fn prems => tac (prems)) i |
|
445 |
|
446 converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new |
|
447 proof state A==>A, supplying A1,...,An as meta-level assumptions (in |
|
448 "prems"). The parameters x1,...,xm become free variables. If the |
|
449 resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An) |
|
450 then it is lifted back into the original context, yielding k subgoals. |
|
451 |
|
452 Replaces unknowns in the context by Frees having the prefix METAHYP_ |
|
453 New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm. |
|
454 DOES NOT HANDLE TYPE UNKNOWNS. |
|
455 ****) |
|
456 |
|
457 local |
|
458 open Logic |
|
459 |
|
460 (*Left-to-right replacements: ctpairs = [...,(vi,ti),...]. |
|
461 Instantiates distinct free variables by terms of same type.*) |
|
462 fun free_instantiate ctpairs = |
|
463 forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs); |
|
464 |
|
465 fun free_of s ((a,i), T) = |
|
466 Free(s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), |
|
467 T) |
|
468 |
|
469 fun mk_inst (var as Var(v,T)) = (var, free_of "METAHYP1_" (v,T)) |
|
470 in |
|
471 |
|
472 fun metahyps_aux_tac tacf (prem,i) = Tactic (fn state => |
|
473 let val {sign,maxidx,...} = rep_thm state |
|
474 val cterm = Sign.cterm_of sign |
|
475 (*find all vars in the hyps -- should find tvars also!*) |
|
476 val hyps_vars = foldr add_term_vars (strip_assums_hyp prem, []) |
|
477 val insts = map mk_inst hyps_vars |
|
478 (*replace the hyps_vars by Frees*) |
|
479 val prem' = subst_atomic insts prem |
|
480 val (params,hyps,concl) = strip_context prem' |
|
481 val fparams = map Free params |
|
482 val cparams = map cterm fparams |
|
483 and chyps = map cterm hyps |
|
484 val hypths = map assume chyps |
|
485 fun swap_ctpair (t,u) = (cterm u, cterm t) |
|
486 (*Subgoal variables: make Free; lift type over params*) |
|
487 fun mk_subgoal_inst concl_vars (var as Var(v,T)) = |
|
488 if var mem concl_vars |
|
489 then (var, true, free_of "METAHYP2_" (v,T)) |
|
490 else (var, false, |
|
491 free_of "METAHYP2_" (v, map #2 params --->T)) |
|
492 (*Instantiate subgoal vars by Free applied to params*) |
|
493 fun mk_ctpair (t,in_concl,u) = |
|
494 if in_concl then (cterm t, cterm u) |
|
495 else (cterm t, cterm (list_comb (u,fparams))) |
|
496 (*Restore Vars with higher type and index*) |
|
497 fun mk_subgoal_swap_ctpair |
|
498 (t as Var((a,i),_), in_concl, u as Free(_,U)) = |
|
499 if in_concl then (cterm u, cterm t) |
|
500 else (cterm u, cterm(Var((a, i+maxidx), U))) |
|
501 (*Embed B in the original context of params and hyps*) |
|
502 fun embed B = list_all_free (params, list_implies (hyps, B)) |
|
503 (*Strip the context using elimination rules*) |
|
504 fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths |
|
505 (*Embed an ff pair in the original params*) |
|
506 fun embed_ff(t,u) = |
|
507 mk_flexpair (list_abs_free (params, t), list_abs_free (params, u)) |
|
508 (*Remove parameter abstractions from the ff pairs*) |
|
509 fun elim_ff ff = flexpair_abs_elim_list cparams ff |
|
510 (*A form of lifting that discharges assumptions.*) |
|
511 fun relift st = |
|
512 let val prop = #prop(rep_thm st) |
|
513 val subgoal_vars = (*Vars introduced in the subgoals*) |
|
514 foldr add_term_vars (strip_imp_prems prop, []) |
|
515 and concl_vars = add_term_vars (strip_imp_concl prop, []) |
|
516 val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars |
|
517 val st' = instantiate ([], map mk_ctpair subgoal_insts) st |
|
518 val emBs = map (cterm o embed) (prems_of st') |
|
519 and ffs = map (cterm o embed_ff) (tpairs_of st') |
|
520 val Cth = implies_elim_list st' |
|
521 (map (elim_ff o assume) ffs @ |
|
522 map (elim o assume) emBs) |
|
523 in (*restore the unknowns to the hypotheses*) |
|
524 free_instantiate (map swap_ctpair insts @ |
|
525 map mk_subgoal_swap_ctpair subgoal_insts) |
|
526 (*discharge assumptions from state in same order*) |
|
527 (implies_intr_list (ffs@emBs) |
|
528 (forall_intr_list cparams (implies_intr_list chyps Cth))) |
|
529 end |
|
530 val subprems = map (forall_elim_vars 0) hypths |
|
531 and st0 = trivial (cterm concl) |
|
532 (*function to replace the current subgoal*) |
|
533 fun next st = bicompose false (false, relift st, nprems_of st) |
|
534 i state |
|
535 in Sequence.flats (Sequence.maps next (tapply(tacf subprems, st0))) |
|
536 end); |
|
537 end; |
|
538 |
|
539 fun METAHYPS tacf = SUBGOAL (metahyps_aux_tac tacf); |
|
540 |
|
541 end; |
|
542 end; |