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