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