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