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