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