src/Pure/tctical.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5997 4d00bbd3d3ac
child 6041 684ec6a1d802
permissions -rw-r--r--
tidying
     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   (writeln "** Press RETURN to continue:";
   202    if TextIO.inputLine TextIO.stdIn = "\n" then Seq.single st
   203    else (writeln "Goodbye";  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" => (writeln "Exiting now";  raise (TRACE_EXIT st))
   220      | "quit\n" => raise TRACE_QUIT
   221      | _     => (writeln
   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                  writeln "** 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
   331         val t = List.nth(prems_of st, i-1)
   332         fun diff st' = (*true if subgoal still exists and is same as old one*)
   333 	    not (nprems_of st' >= j
   334 		 andalso
   335 		 Pattern.aeconv (t,
   336 				 List.nth(prems_of st', nprems_of st' - j)))
   337     in  Seq.filter diff (tac i st)  end
   338     handle Subscript => Seq.empty  (*no subgoal i*);
   339 
   340 fun ALLGOALS_RANGE tac (i:int) j st =
   341   if i > j then all_tac st
   342   else (tac j THEN ALLGOALS_RANGE tac i (j - 1)) st;
   343 
   344 fun (tac1 THEN_ALL_NEW tac2) i st =
   345   st |> (tac1 i THEN (fn st' => ALLGOALS_RANGE tac2 i (i + nprems_of st' - nprems_of st) st'));
   346 
   347 
   348 (*** SELECT_GOAL ***)
   349 
   350 (*Tactical for restricting the effect of a tactic to subgoal i.
   351   Works by making a new state from subgoal i, applying tac to it, and
   352   composing the resulting metathm with the original state.
   353   The "main goal" of the new state will not be atomic, some tactics may fail!
   354   DOES NOT work if tactic affects the main goal other than by instantiation.*)
   355 
   356 (*SELECT_GOAL optimization: replace the conclusion by a variable X,
   357   to avoid copying.  Proof states have X==concl as an assuption.*)
   358 
   359 val prop_equals = cterm_of (sign_of ProtoPure.thy) 
   360                     (Const("==", propT-->propT-->propT));
   361 
   362 fun mk_prop_equals(t,u) = capply (capply prop_equals t) u;
   363 
   364 (*Like trivial but returns [ct==X] ct==>X instead of ct==>ct, if possible.
   365   It is paired with a function to undo the transformation.  If ct contains
   366   Vars then it returns ct==>ct.*)
   367 
   368 fun eq_trivial ct =
   369   let val xfree = cterm_of (sign_of ProtoPure.thy)
   370                            (Free (gensym"EQ_TRIVIAL_", propT))
   371       val ct_eq_x = mk_prop_equals (ct, xfree)
   372       and refl_ct = reflexive ct
   373       fun restore th = 
   374           implies_elim 
   375             (forall_elim ct (forall_intr xfree (implies_intr ct_eq_x th)))
   376             refl_ct
   377   in  (equal_elim
   378          (combination (combination refl_implies refl_ct) (assume ct_eq_x))
   379          (Drule.mk_triv_goal ct),
   380        restore)
   381   end  (*Fails if there are Vars or TVars*)
   382     handle THM _ => (Drule.mk_triv_goal ct, I);
   383 
   384 
   385 (*Does the work of SELECT_GOAL. *)
   386 fun select tac st i =
   387   let val (eq_cprem, restore) = (*we hope maxidx goes to ~1*)
   388 	  eq_trivial (adjust_maxidx (List.nth(cprems_of st, i-1)))
   389       fun next st' = 
   390 	  let val np' = nprems_of st'
   391               (*rename the ?A in rev_triv_goal*)
   392 	      val {maxidx,...} = rep_thm st'
   393               val ct = cterm_of (sign_of ProtoPure.thy)
   394 		                (Var(("A",maxidx+1), propT))
   395 	      val rev_triv_goal' = instantiate' [] [Some ct] Drule.rev_triv_goal
   396               fun bic th = bicompose false (false, th, np')
   397           in  bic (Seq.hd (bic (restore st') 1 rev_triv_goal')) i st  end 
   398   in  Seq.flat (Seq.map next (tac eq_cprem))
   399   end;
   400 
   401 fun SELECT_GOAL tac i st = 
   402   let val np = nprems_of st
   403   in  if 1<=i andalso i<=np then 
   404           (*If only one subgoal, then just apply tactic*)
   405 	  if np=1 then tac st else select tac st i
   406       else Seq.empty
   407   end;
   408 
   409 
   410 (*Strips assumptions in goal yielding  ( [x1,...,xm], [H1,...,Hn], B )
   411     H1,...,Hn are the hypotheses;  x1...xm are variants of the parameters. 
   412   Main difference from strip_assums concerns parameters: 
   413     it replaces the bound variables by free variables.  *)
   414 fun strip_context_aux (params, Hs, Const("==>", _) $ H $ B) = 
   415         strip_context_aux (params, H::Hs, B)
   416   | strip_context_aux (params, Hs, Const("all",_)$Abs(a,T,t)) =
   417         let val (b,u) = variant_abs(a,T,t)
   418         in  strip_context_aux ((b,T)::params, Hs, u)  end
   419   | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
   420 
   421 fun strip_context A = strip_context_aux ([],[],A);
   422 
   423 
   424 (**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
   425        METAHYPS (fn prems => tac prems) i
   426 
   427 converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new
   428 proof state A==>A, supplying A1,...,An as meta-level assumptions (in
   429 "prems").  The parameters x1,...,xm become free variables.  If the
   430 resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An)
   431 then it is lifted back into the original context, yielding k subgoals.
   432 
   433 Replaces unknowns in the context by Frees having the prefix METAHYP_
   434 New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm.
   435 DOES NOT HANDLE TYPE UNKNOWNS.
   436 ****)
   437 
   438 local 
   439 
   440   (*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
   441     Instantiates distinct free variables by terms of same type.*)
   442   fun free_instantiate ctpairs = 
   443       forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs);
   444 
   445   fun free_of s ((a,i), T) =
   446         Free(s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i),
   447              T)
   448 
   449   fun mk_inst (var as Var(v,T))  = (var,  free_of "METAHYP1_" (v,T))
   450 in
   451 
   452 fun metahyps_aux_tac tacf (prem,i) state = 
   453   let val {sign,maxidx,...} = rep_thm state
   454       val cterm = cterm_of sign
   455       (*find all vars in the hyps -- should find tvars also!*)
   456       val hyps_vars = foldr add_term_vars (Logic.strip_assums_hyp prem, [])
   457       val insts = map mk_inst hyps_vars
   458       (*replace the hyps_vars by Frees*)
   459       val prem' = subst_atomic insts prem
   460       val (params,hyps,concl) = strip_context prem'
   461       val fparams = map Free params
   462       val cparams = map cterm fparams
   463       and chyps = map cterm hyps
   464       val hypths = map assume chyps
   465       fun swap_ctpair (t,u) = (cterm u, cterm t)
   466       (*Subgoal variables: make Free; lift type over params*)
   467       fun mk_subgoal_inst concl_vars (var as Var(v,T)) = 
   468           if var mem concl_vars 
   469           then (var, true, free_of "METAHYP2_" (v,T))
   470           else (var, false,
   471                 free_of "METAHYP2_" (v, map #2 params --->T))
   472       (*Instantiate subgoal vars by Free applied to params*)
   473       fun mk_ctpair (t,in_concl,u) = 
   474           if in_concl then (cterm t,  cterm u)
   475           else (cterm t,  cterm (list_comb (u,fparams)))
   476       (*Restore Vars with higher type and index*)
   477       fun mk_subgoal_swap_ctpair 
   478                 (t as Var((a,i),_), in_concl, u as Free(_,U)) = 
   479           if in_concl then (cterm u, cterm t)
   480           else (cterm u, cterm(Var((a, i+maxidx), U)))
   481       (*Embed B in the original context of params and hyps*)
   482       fun embed B = list_all_free (params, Logic.list_implies (hyps, B))
   483       (*Strip the context using elimination rules*)
   484       fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
   485       (*Embed an ff pair in the original params*)
   486       fun embed_ff(t,u) = Logic.mk_flexpair (list_abs_free (params, t), 
   487                                              list_abs_free (params, u))
   488       (*Remove parameter abstractions from the ff pairs*)
   489       fun elim_ff ff = flexpair_abs_elim_list cparams ff
   490       (*A form of lifting that discharges assumptions.*)
   491       fun relift st = 
   492         let val prop = #prop(rep_thm st)
   493             val subgoal_vars = (*Vars introduced in the subgoals*)
   494                   foldr add_term_vars (Logic.strip_imp_prems prop, [])
   495             and concl_vars = add_term_vars (Logic.strip_imp_concl prop, [])
   496             val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
   497             val st' = instantiate ([], map mk_ctpair subgoal_insts) st
   498             val emBs = map (cterm o embed) (prems_of st')
   499             and ffs = map (cterm o embed_ff) (tpairs_of st')
   500             val Cth  = implies_elim_list st' 
   501                             (map (elim_ff o assume) ffs @
   502                              map (elim o assume) emBs)
   503         in  (*restore the unknowns to the hypotheses*)
   504             free_instantiate (map swap_ctpair insts @
   505                               map mk_subgoal_swap_ctpair subgoal_insts)
   506                 (*discharge assumptions from state in same order*)
   507                 (implies_intr_list (ffs@emBs)
   508                   (forall_intr_list cparams (implies_intr_list chyps Cth)))
   509         end
   510       val subprems = map (forall_elim_vars 0) hypths
   511       and st0 = trivial (cterm concl)
   512       (*function to replace the current subgoal*)
   513       fun next st = bicompose false (false, relift st, nprems_of st)
   514                     i state
   515   in  Seq.flat (Seq.map next (tacf subprems st0))
   516   end;
   517 end;
   518 
   519 fun METAHYPS tacf = SUBGOAL (metahyps_aux_tac tacf);
   520 
   521 end;
   522 
   523 open Tactical;