13 |
13 |
14 |
14 |
15 signature TACTICAL = |
15 signature TACTICAL = |
16 sig |
16 sig |
17 type tactic (* = thm -> thm Sequence.seq*) |
17 type tactic (* = thm -> thm Sequence.seq*) |
18 val all_tac : tactic |
18 val all_tac : tactic |
19 val ALLGOALS : (int -> tactic) -> tactic |
19 val ALLGOALS : (int -> tactic) -> tactic |
20 val APPEND : tactic * tactic -> tactic |
20 val APPEND : tactic * tactic -> tactic |
21 val APPEND' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
21 val APPEND' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
22 val CHANGED : tactic -> tactic |
22 val CHANGED : tactic -> tactic |
23 val COND : (thm -> bool) -> tactic -> tactic -> tactic |
23 val COND : (thm -> bool) -> tactic -> tactic -> tactic |
24 val DETERM : tactic -> tactic |
24 val DETERM : tactic -> tactic |
25 val EVERY : tactic list -> tactic |
25 val EVERY : tactic list -> tactic |
26 val EVERY' : ('a -> tactic) list -> 'a -> tactic |
26 val EVERY' : ('a -> tactic) list -> 'a -> tactic |
27 val EVERY1 : (int -> tactic) list -> tactic |
27 val EVERY1 : (int -> tactic) list -> tactic |
28 val FILTER : (thm -> bool) -> tactic -> tactic |
28 val FILTER : (thm -> bool) -> tactic -> tactic |
29 val FIRST : tactic list -> tactic |
29 val FIRST : tactic list -> tactic |
30 val FIRST' : ('a -> tactic) list -> 'a -> tactic |
30 val FIRST' : ('a -> tactic) list -> 'a -> tactic |
31 val FIRST1 : (int -> tactic) list -> tactic |
31 val FIRST1 : (int -> tactic) list -> tactic |
32 val FIRSTGOAL : (int -> tactic) -> tactic |
32 val FIRSTGOAL : (int -> tactic) -> tactic |
33 val goals_limit : int ref |
33 val goals_limit : int ref |
34 val INTLEAVE : tactic * tactic -> tactic |
34 val INTLEAVE : tactic * tactic -> tactic |
35 val INTLEAVE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
35 val INTLEAVE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
36 val METAHYPS : (thm list -> tactic) -> int -> tactic |
36 val METAHYPS : (thm list -> tactic) -> int -> tactic |
37 val no_tac : tactic |
37 val no_tac : tactic |
38 val ORELSE : tactic * tactic -> tactic |
38 val ORELSE : tactic * tactic -> tactic |
39 val ORELSE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
39 val ORELSE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
40 val pause_tac : tactic |
40 val pause_tac : tactic |
41 val print_tac : tactic |
41 val print_tac : tactic |
42 val REPEAT : tactic -> tactic |
42 val REPEAT : tactic -> tactic |
43 val REPEAT1 : tactic -> tactic |
43 val REPEAT1 : tactic -> tactic |
44 val REPEAT_DETERM_N : int -> tactic -> tactic |
44 val REPEAT_DETERM_N : int -> tactic -> tactic |
45 val REPEAT_DETERM : tactic -> tactic |
45 val REPEAT_DETERM : tactic -> tactic |
46 val REPEAT_DETERM1 : tactic -> tactic |
46 val REPEAT_DETERM1 : tactic -> tactic |
47 val REPEAT_DETERM_FIRST: (int -> tactic) -> tactic |
47 val REPEAT_DETERM_FIRST: (int -> tactic) -> tactic |
48 val REPEAT_DETERM_SOME: (int -> tactic) -> tactic |
48 val REPEAT_DETERM_SOME: (int -> tactic) -> tactic |
49 val REPEAT_FIRST : (int -> tactic) -> tactic |
49 val REPEAT_FIRST : (int -> tactic) -> tactic |
50 val REPEAT_SOME : (int -> tactic) -> tactic |
50 val REPEAT_SOME : (int -> tactic) -> tactic |
51 val SELECT_GOAL : tactic -> int -> tactic |
51 val SELECT_GOAL : tactic -> int -> tactic |
52 val SOMEGOAL : (int -> tactic) -> tactic |
52 val SOMEGOAL : (int -> tactic) -> tactic |
53 val STATE : (thm -> tactic) -> tactic |
53 val STATE : (thm -> tactic) -> tactic |
54 val strip_context : term -> (string * typ) list * term list * term |
54 val strip_context : term -> (string * typ) list * term list * term |
55 val SUBGOAL : ((term*int) -> tactic) -> int -> tactic |
55 val SUBGOAL : ((term*int) -> tactic) -> int -> tactic |
56 val suppress_tracing : bool ref |
56 val suppress_tracing : bool ref |
57 val THEN : tactic * tactic -> tactic |
57 val THEN : tactic * tactic -> tactic |
58 val THEN' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
58 val THEN' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
59 val THEN_ELSE : tactic * (tactic*tactic) -> tactic |
59 val THEN_ELSE : tactic * (tactic*tactic) -> tactic |
60 val traced_tac : (thm -> (thm * thm Sequence.seq) option) -> tactic |
60 val traced_tac : (thm -> (thm * thm Sequence.seq) option) -> tactic |
61 val tracify : bool ref -> tactic -> thm -> thm Sequence.seq |
61 val tracify : bool ref -> tactic -> thm -> thm Sequence.seq |
62 val trace_REPEAT : bool ref |
62 val trace_REPEAT : bool ref |
63 val TRY : tactic -> tactic |
63 val TRY : tactic -> tactic |
64 val TRYALL : (int -> tactic) -> tactic |
64 val TRYALL : (int -> tactic) -> tactic |
65 end; |
65 end; |
66 |
66 |
67 |
67 |
68 structure Tactical : TACTICAL = |
68 structure Tactical : TACTICAL = |
69 struct |
69 struct |
89 (*The tactical ORELSE uses the first tactic that returns a nonempty sequence. |
89 (*The tactical ORELSE uses the first tactic that returns a nonempty sequence. |
90 Like in LCF, ORELSE commits to either tac1 or tac2 immediately. |
90 Like in LCF, ORELSE commits to either tac1 or tac2 immediately. |
91 Does not backtrack to tac2 if tac1 was initially chosen. *) |
91 Does not backtrack to tac2 if tac1 was initially chosen. *) |
92 fun (tac1 ORELSE tac2) st = |
92 fun (tac1 ORELSE tac2) st = |
93 case Sequence.pull(tac1 st) of |
93 case Sequence.pull(tac1 st) of |
94 None => tac2 st |
94 None => tac2 st |
95 | sequencecell => Sequence.seqof(fn()=> sequencecell); |
95 | sequencecell => Sequence.seqof(fn()=> sequencecell); |
96 |
96 |
97 |
97 |
98 (*The tactical APPEND combines the results of two tactics. |
98 (*The tactical APPEND combines the results of two tactics. |
99 Like ORELSE, but allows backtracking on both tac1 and tac2. |
99 Like ORELSE, but allows backtracking on both tac1 and tac2. |
100 The tactic tac2 is not applied until needed.*) |
100 The tactic tac2 is not applied until needed.*) |
101 fun (tac1 APPEND tac2) st = |
101 fun (tac1 APPEND tac2) st = |
102 Sequence.append(tac1 st, |
102 Sequence.append(tac1 st, |
103 Sequence.seqof(fn()=> Sequence.pull (tac2 st))); |
103 Sequence.seqof(fn()=> Sequence.pull (tac2 st))); |
104 |
104 |
105 (*Like APPEND, but interleaves results of tac1 and tac2.*) |
105 (*Like APPEND, but interleaves results of tac1 and tac2.*) |
106 fun (tac1 INTLEAVE tac2) st = |
106 fun (tac1 INTLEAVE tac2) st = |
107 Sequence.interleave(tac1 st, |
107 Sequence.interleave(tac1 st, |
108 Sequence.seqof(fn()=> Sequence.pull (tac2 st))); |
108 Sequence.seqof(fn()=> Sequence.pull (tac2 st))); |
109 |
109 |
110 (*Conditional tactic. |
110 (*Conditional tactic. |
111 tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2) |
111 tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2) |
112 tac1 THEN tac2 = tac1 THEN_ELSE (tac2, no_tac) |
112 tac1 THEN tac2 = tac1 THEN_ELSE (tac2, no_tac) |
113 *) |
113 *) |
114 fun (tac THEN_ELSE (tac1, tac2)) st = |
114 fun (tac THEN_ELSE (tac1, tac2)) st = |
115 case Sequence.pull(tac st) of |
115 case Sequence.pull(tac st) of |
116 None => tac2 st (*failed; try tactic 2*) |
116 None => tac2 st (*failed; try tactic 2*) |
117 | seqcell => Sequence.flats (*succeeded; use tactic 1*) |
117 | seqcell => Sequence.flats (*succeeded; use tactic 1*) |
118 (Sequence.maps tac1 (Sequence.seqof(fn()=> seqcell))); |
118 (Sequence.maps tac1 (Sequence.seqof(fn()=> seqcell))); |
119 |
119 |
120 |
120 |
121 (*Versions for combining tactic-valued functions, as in |
121 (*Versions for combining tactic-valued functions, as in |
122 SOMEGOAL (resolve_tac rls THEN' assume_tac) *) |
122 SOMEGOAL (resolve_tac rls THEN' assume_tac) *) |
123 fun (tac1 THEN' tac2) x = tac1 x THEN tac2 x; |
123 fun (tac1 THEN' tac2) x = tac1 x THEN tac2 x; |
213 |
213 |
214 (*Extract from a tactic, a thm->thm seq function that handles tracing*) |
214 (*Extract from a tactic, a thm->thm seq function that handles tracing*) |
215 fun tracify flag tac st = |
215 fun tracify flag tac st = |
216 if !flag andalso not (!suppress_tracing) |
216 if !flag andalso not (!suppress_tracing) |
217 then (!print_goals_ref (!goals_limit) st; |
217 then (!print_goals_ref (!goals_limit) st; |
218 prs"** Press RETURN to continue: "; |
218 prs"** Press RETURN to continue: "; |
219 exec_trace_command flag (tac,st)) |
219 exec_trace_command flag (tac,st)) |
220 else tac st; |
220 else tac st; |
221 |
221 |
222 (*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*) |
222 (*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*) |
223 fun traced_tac seqf st = |
223 fun traced_tac seqf st = |
224 (suppress_tracing := false; |
224 (suppress_tracing := false; |
225 Sequence.seqof (fn()=> seqf st |
225 Sequence.seqof (fn()=> seqf st |
226 handle TRACE_EXIT st' => Some(st', Sequence.null))); |
226 handle TRACE_EXIT st' => Some(st', Sequence.null))); |
227 |
227 |
228 |
228 |
229 (*Deterministic REPEAT: only retains the first outcome; |
229 (*Deterministic REPEAT: only retains the first outcome; |
230 uses less space than REPEAT; tail recursive. |
230 uses less space than REPEAT; tail recursive. |
231 If non-negative, n bounds the number of repetitions.*) |
231 If non-negative, n bounds the number of repetitions.*) |
232 fun REPEAT_DETERM_N n tac = |
232 fun REPEAT_DETERM_N n tac = |
233 let val tac = tracify trace_REPEAT tac |
233 let val tac = tracify trace_REPEAT tac |
234 fun drep 0 st = Some(st, Sequence.null) |
234 fun drep 0 st = Some(st, Sequence.null) |
235 | drep n st = |
235 | drep n st = |
236 (case Sequence.pull(tac st) of |
236 (case Sequence.pull(tac st) of |
237 None => Some(st, Sequence.null) |
237 None => Some(st, Sequence.null) |
238 | Some(st',_) => drep (n-1) st') |
238 | Some(st',_) => drep (n-1) st') |
239 in traced_tac (drep n) end; |
239 in traced_tac (drep n) end; |
240 |
240 |
241 (*Allows any number of repetitions*) |
241 (*Allows any number of repetitions*) |
242 val REPEAT_DETERM = REPEAT_DETERM_N ~1; |
242 val REPEAT_DETERM = REPEAT_DETERM_N ~1; |
243 |
243 |
244 (*General REPEAT: maintains a stack of alternatives; tail recursive*) |
244 (*General REPEAT: maintains a stack of alternatives; tail recursive*) |
245 fun REPEAT tac = |
245 fun REPEAT tac = |
246 let val tac = tracify trace_REPEAT tac |
246 let val tac = tracify trace_REPEAT tac |
247 fun rep qs st = |
247 fun rep qs st = |
248 case Sequence.pull(tac st) of |
248 case Sequence.pull(tac st) of |
249 None => Some(st, Sequence.seqof(fn()=> repq qs)) |
249 None => Some(st, Sequence.seqof(fn()=> repq qs)) |
250 | Some(st',q) => rep (q::qs) st' |
250 | Some(st',q) => rep (q::qs) st' |
251 and repq [] = None |
251 and repq [] = None |
252 | repq(q::qs) = case Sequence.pull q of |
252 | repq(q::qs) = case Sequence.pull q of |
253 None => repq qs |
253 None => repq qs |
254 | Some(st,q) => rep (q::qs) st |
254 | Some(st,q) => rep (q::qs) st |
255 in traced_tac (rep []) end; |
255 in traced_tac (rep []) end; |
256 |
256 |
257 (*Repeat 1 or more times*) |
257 (*Repeat 1 or more times*) |
258 fun REPEAT_DETERM1 tac = DETERM tac THEN REPEAT_DETERM tac; |
258 fun REPEAT_DETERM1 tac = DETERM tac THEN REPEAT_DETERM tac; |
274 |
274 |
275 (*For n subgoals, performs tac(n) THEN ... THEN tac(1) |
275 (*For n subgoals, performs tac(n) THEN ... THEN tac(1) |
276 Essential to work backwards since tac(i) may add/delete subgoals at i. *) |
276 Essential to work backwards since tac(i) may add/delete subgoals at i. *) |
277 fun ALLGOALS tac st = |
277 fun ALLGOALS tac st = |
278 let fun doall 0 = all_tac |
278 let fun doall 0 = all_tac |
279 | doall n = tac(n) THEN doall(n-1) |
279 | doall n = tac(n) THEN doall(n-1) |
280 in doall(nprems_of st)st end; |
280 in doall(nprems_of st)st end; |
281 |
281 |
282 (*For n subgoals, performs tac(n) ORELSE ... ORELSE tac(1) *) |
282 (*For n subgoals, performs tac(n) ORELSE ... ORELSE tac(1) *) |
283 fun SOMEGOAL tac st = |
283 fun SOMEGOAL tac st = |
284 let fun find 0 = no_tac |
284 let fun find 0 = no_tac |
285 | find n = tac(n) ORELSE find(n-1) |
285 | find n = tac(n) ORELSE find(n-1) |
286 in find(nprems_of st)st end; |
286 in find(nprems_of st)st end; |
287 |
287 |
288 (*For n subgoals, performs tac(1) ORELSE ... ORELSE tac(n). |
288 (*For n subgoals, performs tac(1) ORELSE ... ORELSE tac(n). |
289 More appropriate than SOMEGOAL in some cases.*) |
289 More appropriate than SOMEGOAL in some cases.*) |
290 fun FIRSTGOAL tac st = |
290 fun FIRSTGOAL tac st = |
359 assume |> forall_elim_var 0 |> standard; |
359 assume |> forall_elim_var 0 |> standard; |
360 |
360 |
361 (* Prevent the subgoal's assumptions from becoming additional subgoals in the |
361 (* Prevent the subgoal's assumptions from becoming additional subgoals in the |
362 new proof state by enclosing them by a universal quantification *) |
362 new proof state by enclosing them by a universal quantification *) |
363 fun protect_subgoal st i = |
363 fun protect_subgoal st i = |
364 Sequence.hd (bicompose false (false,dummy_quant_rl,1) i st) |
364 Sequence.hd (bicompose false (false,dummy_quant_rl,1) i st) |
365 handle _ => error"SELECT_GOAL -- impossible error???"; |
365 handle _ => error"SELECT_GOAL -- impossible error???"; |
366 |
366 |
367 fun SELECT_GOAL tac i st = |
367 fun SELECT_GOAL tac i st = |
368 case (i, drop(i-1, prems_of st)) of |
368 case (i, drop(i-1, prems_of st)) of |
369 (_,[]) => Sequence.null |
369 (_,[]) => Sequence.null |
370 | (1,[_]) => tac st (*If i=1 and only one subgoal do nothing!*) |
370 | (1,[_]) => tac st (*If i=1 and only one subgoal do nothing!*) |
371 | (_, (Const("==>",_)$_$_) :: _) => select tac (protect_subgoal st i) i |
371 | (_, (Const("==>",_)$_$_) :: _) => select tac (protect_subgoal st i) i |
372 | (_, _::_) => select tac st i; |
372 | (_, _::_) => select tac st i; |
373 |
373 |
374 |
374 |
375 (*Strips assumptions in goal yielding ( [x1,...,xm], [H1,...,Hn], B ) |
375 (*Strips assumptions in goal yielding ( [x1,...,xm], [H1,...,Hn], B ) |
376 H1,...,Hn are the hypotheses; x1...xm are variants of the parameters. |
376 H1,...,Hn are the hypotheses; x1...xm are variants of the parameters. |
377 Main difference from strip_assums concerns parameters: |
377 Main difference from strip_assums concerns parameters: |
378 it replaces the bound variables by free variables. *) |
378 it replaces the bound variables by free variables. *) |
379 fun strip_context_aux (params, Hs, Const("==>", _) $ H $ B) = |
379 fun strip_context_aux (params, Hs, Const("==>", _) $ H $ B) = |
380 strip_context_aux (params, H::Hs, B) |
380 strip_context_aux (params, H::Hs, B) |
381 | strip_context_aux (params, Hs, Const("all",_)$Abs(a,T,t)) = |
381 | strip_context_aux (params, Hs, Const("all",_)$Abs(a,T,t)) = |
382 let val (b,u) = variant_abs(a,T,t) |
382 let val (b,u) = variant_abs(a,T,t) |
383 in strip_context_aux ((b,T)::params, Hs, u) end |
383 in strip_context_aux ((b,T)::params, Hs, u) end |
384 | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B); |
384 | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B); |
385 |
385 |
386 fun strip_context A = strip_context_aux ([],[],A); |
386 fun strip_context A = strip_context_aux ([],[],A); |
387 |
387 |
388 |
388 |
429 val hypths = map assume chyps |
429 val hypths = map assume chyps |
430 fun swap_ctpair (t,u) = (cterm u, cterm t) |
430 fun swap_ctpair (t,u) = (cterm u, cterm t) |
431 (*Subgoal variables: make Free; lift type over params*) |
431 (*Subgoal variables: make Free; lift type over params*) |
432 fun mk_subgoal_inst concl_vars (var as Var(v,T)) = |
432 fun mk_subgoal_inst concl_vars (var as Var(v,T)) = |
433 if var mem concl_vars |
433 if var mem concl_vars |
434 then (var, true, free_of "METAHYP2_" (v,T)) |
434 then (var, true, free_of "METAHYP2_" (v,T)) |
435 else (var, false, |
435 else (var, false, |
436 free_of "METAHYP2_" (v, map #2 params --->T)) |
436 free_of "METAHYP2_" (v, map #2 params --->T)) |
437 (*Instantiate subgoal vars by Free applied to params*) |
437 (*Instantiate subgoal vars by Free applied to params*) |
438 fun mk_ctpair (t,in_concl,u) = |
438 fun mk_ctpair (t,in_concl,u) = |
439 if in_concl then (cterm t, cterm u) |
439 if in_concl then (cterm t, cterm u) |
440 else (cterm t, cterm (list_comb (u,fparams))) |
440 else (cterm t, cterm (list_comb (u,fparams))) |
441 (*Restore Vars with higher type and index*) |
441 (*Restore Vars with higher type and index*) |
442 fun mk_subgoal_swap_ctpair |
442 fun mk_subgoal_swap_ctpair |
443 (t as Var((a,i),_), in_concl, u as Free(_,U)) = |
443 (t as Var((a,i),_), in_concl, u as Free(_,U)) = |
444 if in_concl then (cterm u, cterm t) |
444 if in_concl then (cterm u, cterm t) |
445 else (cterm u, cterm(Var((a, i+maxidx), U))) |
445 else (cterm u, cterm(Var((a, i+maxidx), U))) |
446 (*Embed B in the original context of params and hyps*) |
446 (*Embed B in the original context of params and hyps*) |
447 fun embed B = list_all_free (params, Logic.list_implies (hyps, B)) |
447 fun embed B = list_all_free (params, Logic.list_implies (hyps, B)) |
448 (*Strip the context using elimination rules*) |
448 (*Strip the context using elimination rules*) |
449 fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths |
449 fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths |
450 (*Embed an ff pair in the original params*) |
450 (*Embed an ff pair in the original params*) |
451 fun embed_ff(t,u) = Logic.mk_flexpair (list_abs_free (params, t), |
451 fun embed_ff(t,u) = Logic.mk_flexpair (list_abs_free (params, t), |
452 list_abs_free (params, u)) |
452 list_abs_free (params, u)) |
453 (*Remove parameter abstractions from the ff pairs*) |
453 (*Remove parameter abstractions from the ff pairs*) |
454 fun elim_ff ff = flexpair_abs_elim_list cparams ff |
454 fun elim_ff ff = flexpair_abs_elim_list cparams ff |
455 (*A form of lifting that discharges assumptions.*) |
455 (*A form of lifting that discharges assumptions.*) |
456 fun relift st = |
456 fun relift st = |
457 let val prop = #prop(rep_thm st) |
457 let val prop = #prop(rep_thm st) |
458 val subgoal_vars = (*Vars introduced in the subgoals*) |
458 val subgoal_vars = (*Vars introduced in the subgoals*) |
459 foldr add_term_vars (Logic.strip_imp_prems prop, []) |
459 foldr add_term_vars (Logic.strip_imp_prems prop, []) |
460 and concl_vars = add_term_vars (Logic.strip_imp_concl prop, []) |
460 and concl_vars = add_term_vars (Logic.strip_imp_concl prop, []) |
461 val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars |
461 val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars |
462 val st' = instantiate ([], map mk_ctpair subgoal_insts) st |
462 val st' = instantiate ([], map mk_ctpair subgoal_insts) st |
463 val emBs = map (cterm o embed) (prems_of st') |
463 val emBs = map (cterm o embed) (prems_of st') |
464 and ffs = map (cterm o embed_ff) (tpairs_of st') |
464 and ffs = map (cterm o embed_ff) (tpairs_of st') |
465 val Cth = implies_elim_list st' |
465 val Cth = implies_elim_list st' |
466 (map (elim_ff o assume) ffs @ |
466 (map (elim_ff o assume) ffs @ |
467 map (elim o assume) emBs) |
467 map (elim o assume) emBs) |
468 in (*restore the unknowns to the hypotheses*) |
468 in (*restore the unknowns to the hypotheses*) |
469 free_instantiate (map swap_ctpair insts @ |
469 free_instantiate (map swap_ctpair insts @ |
470 map mk_subgoal_swap_ctpair subgoal_insts) |
470 map mk_subgoal_swap_ctpair subgoal_insts) |
471 (*discharge assumptions from state in same order*) |
471 (*discharge assumptions from state in same order*) |
472 (implies_intr_list (ffs@emBs) |
472 (implies_intr_list (ffs@emBs) |
473 (forall_intr_list cparams (implies_intr_list chyps Cth))) |
473 (forall_intr_list cparams (implies_intr_list chyps Cth))) |
474 end |
474 end |
475 val subprems = map (forall_elim_vars 0) hypths |
475 val subprems = map (forall_elim_vars 0) hypths |
476 and st0 = trivial (cterm concl) |
476 and st0 = trivial (cterm concl) |
477 (*function to replace the current subgoal*) |
477 (*function to replace the current subgoal*) |
478 fun next st = bicompose false (false, relift st, nprems_of st) |
478 fun next st = bicompose false (false, relift st, nprems_of st) |
479 i state |
479 i state |
480 in Sequence.flats (Sequence.maps next (tacf subprems st0)) |
480 in Sequence.flats (Sequence.maps next (tacf subprems st0)) |
481 end; |
481 end; |
482 end; |
482 end; |
483 |
483 |
484 fun METAHYPS tacf = SUBGOAL (metahyps_aux_tac tacf); |
484 fun METAHYPS tacf = SUBGOAL (metahyps_aux_tac tacf); |