src/Pure/tactic.ML
author paulson
Thu Nov 06 10:28:20 1997 +0100 (1997-11-06)
changeset 4178 e64ff1c1bc70
parent 3991 4cb2f2422695
child 4213 cef5ef41e70d
permissions -rw-r--r--
subgoal_tac displays a warning if the new subgoal has type variables
     1 (*  Title: 	Pure/tactic.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 
     6 Tactics 
     7 *)
     8 
     9 signature TACTIC =
    10   sig
    11   val ares_tac		: thm list -> int -> tactic
    12   val asm_rewrite_goal_tac:
    13         bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic
    14   val assume_tac	: int -> tactic
    15   val atac	: int ->tactic
    16   val bimatch_from_nets_tac: 
    17       (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
    18   val bimatch_tac	: (bool*thm)list -> int -> tactic
    19   val biresolution_from_nets_tac: 
    20 	('a list -> (bool * thm) list) ->
    21 	bool -> 'a Net.net * 'a Net.net -> int -> tactic
    22   val biresolve_from_nets_tac: 
    23       (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
    24   val biresolve_tac	: (bool*thm)list -> int -> tactic
    25   val build_net	: thm list -> (int*thm) Net.net
    26   val build_netpair:    (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net ->
    27       (bool*thm)list -> (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net
    28   val compose_inst_tac	: (string*string)list -> (bool*thm*int) -> 
    29                           int -> tactic
    30   val compose_tac	: (bool * thm * int) -> int -> tactic 
    31   val cut_facts_tac	: thm list -> int -> tactic
    32   val cut_inst_tac	: (string*string)list -> thm -> int -> tactic   
    33   val defer_tac 	: int -> tactic
    34   val distinct_subgoals_tac	: tactic
    35   val dmatch_tac	: thm list -> int -> tactic
    36   val dresolve_tac	: thm list -> int -> tactic
    37   val dres_inst_tac	: (string*string)list -> thm -> int -> tactic   
    38   val dtac		: thm -> int ->tactic
    39   val etac		: thm -> int ->tactic
    40   val eq_assume_tac	: int -> tactic   
    41   val ematch_tac	: thm list -> int -> tactic
    42   val eresolve_tac	: thm list -> int -> tactic
    43   val eres_inst_tac	: (string*string)list -> thm -> int -> tactic   
    44   val filter_thms	: (term*term->bool) -> int*term*thm list -> thm list
    45   val filt_resolve_tac	: thm list -> int -> int -> tactic
    46   val flexflex_tac	: tactic
    47   val fold_goals_tac	: thm list -> tactic
    48   val fold_tac		: thm list -> tactic
    49   val forward_tac	: thm list -> int -> tactic   
    50   val forw_inst_tac	: (string*string)list -> thm -> int -> tactic
    51   val freeze_thaw	: thm -> thm * (thm -> thm)
    52   val insert_tagged_brl : ('a*(bool*thm)) * 
    53                           (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) ->
    54                           ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net
    55   val delete_tagged_brl	: (bool*thm) * 
    56                          ((int*(bool*thm))Net.net * (int*(bool*thm))Net.net) ->
    57                     (int*(bool*thm))Net.net * (int*(bool*thm))Net.net
    58   val is_fact		: thm -> bool
    59   val lessb		: (bool * thm) * (bool * thm) -> bool
    60   val lift_inst_rule	: thm * int * (string*string)list * thm -> thm
    61   val make_elim		: thm -> thm
    62   val match_from_net_tac	: (int*thm) Net.net -> int -> tactic
    63   val match_tac	: thm list -> int -> tactic
    64   val metacut_tac	: thm -> int -> tactic   
    65   val net_bimatch_tac	: (bool*thm) list -> int -> tactic
    66   val net_biresolve_tac	: (bool*thm) list -> int -> tactic
    67   val net_match_tac	: thm list -> int -> tactic
    68   val net_resolve_tac	: thm list -> int -> tactic
    69   val orderlist		: (int * 'a) list -> 'a list
    70   val PRIMITIVE		: (thm -> thm) -> tactic  
    71   val PRIMSEQ		: (thm -> thm Sequence.seq) -> tactic  
    72   val prune_params_tac	: tactic
    73   val rename_tac	: string -> int -> tactic
    74   val rename_last_tac	: string -> string list -> int -> tactic
    75   val resolve_from_net_tac	: (int*thm) Net.net -> int -> tactic
    76   val resolve_tac	: thm list -> int -> tactic
    77   val res_inst_tac	: (string*string)list -> thm -> int -> tactic   
    78   val rewrite_goals_rule: thm list -> thm -> thm
    79   val rewrite_rule	: thm list -> thm -> thm
    80   val rewrite_goals_tac	: thm list -> tactic
    81   val rewrite_tac	: thm list -> tactic
    82   val rewtac		: thm -> tactic
    83   val rotate_tac	: int -> int -> tactic
    84   val rtac		: thm -> int -> tactic
    85   val rule_by_tactic	: tactic -> thm -> thm
    86   val subgoal_tac	: string -> int -> tactic
    87   val subgoals_tac	: string list -> int -> tactic
    88   val subgoals_of_brl	: bool * thm -> int
    89   val term_lift_inst_rule	:
    90       thm * int * (indexname*typ)list * ((indexname*typ)*term)list  * thm
    91       -> thm
    92   val thin_tac		: string -> int -> tactic
    93   val trace_goalno_tac	: (int -> tactic) -> int -> tactic
    94   end;
    95 
    96 
    97 structure Tactic : TACTIC = 
    98 struct
    99 
   100 (*Discover which goal is chosen:  SOMEGOAL(trace_goalno_tac tac) *)
   101 fun trace_goalno_tac tac i st =  
   102     case Sequence.pull(tac i st) of
   103 	None    => Sequence.null
   104       | seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); 
   105     			 Sequence.seqof(fn()=> seqcell));
   106 
   107 
   108 (*Convert all Vars in a theorem to Frees.  Also return a function for 
   109   reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.
   110   Similar code in type/freeze_thaw*)
   111 fun freeze_thaw th =
   112   let val fth = freezeT th
   113       val {prop,sign,...} = rep_thm fth
   114       val used = add_term_names (prop, [])
   115       and vars = term_vars prop
   116       fun newName (Var(ix,_), (pairs,used)) = 
   117 	    let val v = variant used (string_of_indexname ix)
   118 	    in  ((ix,v)::pairs, v::used)  end;
   119       val (alist, _) = foldr newName (vars, ([], used))
   120       fun mk_inst (Var(v,T)) = 
   121 	  (cterm_of sign (Var(v,T)),
   122 	   cterm_of sign (Free(the (assoc(alist,v)), T)))
   123       val insts = map mk_inst vars
   124       fun thaw th' = 
   125 	  th' |> forall_intr_list (map #2 insts)
   126 	      |> forall_elim_list (map #1 insts)
   127   in  (instantiate ([],insts) fth, thaw)  end;
   128 
   129 
   130 (*Rotates the given subgoal to be the last.  Useful when re-playing
   131   an old proof script, when the proof of an early subgoal fails.
   132   DOES NOT WORK FOR TYPE VARIABLES.*)
   133 fun defer_tac i state = 
   134     let val (state',thaw) = freeze_thaw state
   135 	val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state'))
   136 	val hyp::hyps' = List.drop(hyps, i-1)
   137     in  implies_intr hyp (implies_elim_list state' (map assume hyps)) 
   138         |> implies_intr_list (List.take(hyps, i-1) @ hyps')
   139         |> thaw
   140         |> Sequence.single
   141     end
   142     handle _ => Sequence.null;
   143 
   144 
   145 (*Makes a rule by applying a tactic to an existing rule*)
   146 fun rule_by_tactic tac rl =
   147   let val (st, thaw) = freeze_thaw (zero_var_indexes rl)
   148   in case Sequence.pull (tac st)  of
   149 	None        => raise THM("rule_by_tactic", 0, [rl])
   150       | Some(st',_) => Thm.varifyT (thaw st')
   151   end;
   152  
   153 (*** Basic tactics ***)
   154 
   155 (*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
   156 fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Sequence.null;
   157 
   158 (*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
   159 fun PRIMITIVE thmfun = PRIMSEQ (Sequence.single o thmfun);
   160 
   161 (*** The following fail if the goal number is out of range:
   162      thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
   163 
   164 (*Solve subgoal i by assumption*)
   165 fun assume_tac i = PRIMSEQ (assumption i);
   166 
   167 (*Solve subgoal i by assumption, using no unification*)
   168 fun eq_assume_tac i = PRIMITIVE (eq_assumption i);
   169 
   170 (** Resolution/matching tactics **)
   171 
   172 (*The composition rule/state: no lifting or var renaming.
   173   The arg = (bires_flg, orule, m) ;  see bicompose for explanation.*)
   174 fun compose_tac arg i = PRIMSEQ (bicompose false arg i);
   175 
   176 (*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
   177   like [| P&Q; P==>R |] ==> R *)
   178 fun make_elim rl = zero_var_indexes (rl RS revcut_rl);
   179 
   180 (*Attack subgoal i by resolution, using flags to indicate elimination rules*)
   181 fun biresolve_tac brules i = PRIMSEQ (biresolution false brules i);
   182 
   183 (*Resolution: the simple case, works for introduction rules*)
   184 fun resolve_tac rules = biresolve_tac (map (pair false) rules);
   185 
   186 (*Resolution with elimination rules only*)
   187 fun eresolve_tac rules = biresolve_tac (map (pair true) rules);
   188 
   189 (*Forward reasoning using destruction rules.*)
   190 fun forward_tac rls = resolve_tac (map make_elim rls) THEN' assume_tac;
   191 
   192 (*Like forward_tac, but deletes the assumption after use.*)
   193 fun dresolve_tac rls = eresolve_tac (map make_elim rls);
   194 
   195 (*Shorthand versions: for resolution with a single theorem*)
   196 fun rtac rl = resolve_tac [rl];
   197 fun etac rl = eresolve_tac [rl];
   198 fun dtac rl = dresolve_tac [rl];
   199 val atac = assume_tac;
   200 
   201 (*Use an assumption or some rules ... A popular combination!*)
   202 fun ares_tac rules = assume_tac  ORELSE'  resolve_tac rules;
   203 
   204 (*Matching tactics -- as above, but forbid updating of state*)
   205 fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i);
   206 fun match_tac rules  = bimatch_tac (map (pair false) rules);
   207 fun ematch_tac rules = bimatch_tac (map (pair true) rules);
   208 fun dmatch_tac rls   = ematch_tac (map make_elim rls);
   209 
   210 (*Smash all flex-flex disagreement pairs in the proof state.*)
   211 val flexflex_tac = PRIMSEQ flexflex_rule;
   212 
   213 
   214 (*Remove duplicate subgoals.  By Mark Staples*)
   215 local
   216 fun cterm_aconv (a,b) = #t (rep_cterm a) aconv #t (rep_cterm b);
   217 in
   218 fun distinct_subgoals_tac state = 
   219     let val (frozth,thawfn) = freeze_thaw state
   220 	val froz_prems = cprems_of frozth
   221 	val assumed = implies_elim_list frozth (map assume froz_prems)
   222 	val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems)
   223 					assumed;
   224     in  Sequence.single (thawfn implied)  end
   225 end; 
   226 
   227 
   228 (*Lift and instantiate a rule wrt the given state and subgoal number *)
   229 fun lift_inst_rule (st, i, sinsts, rule) =
   230 let val {maxidx,sign,...} = rep_thm st
   231     val (_, _, Bi, _) = dest_state(st,i)
   232     val params = Logic.strip_params Bi	        (*params of subgoal i*)
   233     val params = rev(rename_wrt_term Bi params) (*as they are printed*)
   234     val paramTs = map #2 params
   235     and inc = maxidx+1
   236     fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> incr_tvar inc T)
   237       | liftvar t = raise TERM("Variable expected", [t]);
   238     fun liftterm t = list_abs_free (params, 
   239 				    Logic.incr_indexes(paramTs,inc) t)
   240     (*Lifts instantiation pair over params*)
   241     fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
   242     fun lifttvar((a,i),ctyp) =
   243 	let val {T,sign} = rep_ctyp ctyp
   244 	in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
   245     val rts = types_sorts rule and (types,sorts) = types_sorts st
   246     fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
   247       | types'(ixn) = types ixn;
   248     val used = add_term_tvarnames
   249                   (#prop(rep_thm st) $ #prop(rep_thm rule),[])
   250     val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts
   251 in instantiate (map lifttvar Tinsts, map liftpair insts)
   252                (lift_rule (st,i) rule)
   253 end;
   254 
   255 (*
   256 Like lift_inst_rule but takes terms, not strings, where the terms may contain
   257 Bounds referring to parameters of the subgoal.
   258 
   259 insts: [...,(vj,tj),...]
   260 
   261 The tj may contain references to parameters of subgoal i of the state st
   262 in the form of Bound k, i.e. the tj may be subterms of the subgoal.
   263 To saturate the lose bound vars, the tj are enclosed in abstractions
   264 corresponding to the parameters of subgoal i, thus turning them into
   265 functions. At the same time, the types of the vj are lifted.
   266 
   267 NB: the types in insts must be correctly instantiated already,
   268     i.e. Tinsts is not applied to insts.
   269 *)
   270 fun term_lift_inst_rule (st, i, Tinsts, insts, rule) =
   271 let val {maxidx,sign,...} = rep_thm st
   272     val (_, _, Bi, _) = dest_state(st,i)
   273     val params = Logic.strip_params Bi          (*params of subgoal i*)
   274     val paramTs = map #2 params
   275     and inc = maxidx+1
   276     fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> incr_tvar inc T)
   277     (*lift only Var, not term, which must be lifted already*)
   278     fun liftpair (v,t) = (cterm_of sign (liftvar v), cterm_of sign t)
   279     fun liftTpair((a,i),T) = ((a,i+inc), ctyp_of sign (incr_tvar inc T))
   280 in instantiate (map liftTpair Tinsts, map liftpair insts)
   281                (lift_rule (st,i) rule)
   282 end;
   283 
   284 (*** Resolve after lifting and instantation; may refer to parameters of the
   285      subgoal.  Fails if "i" is out of range.  ***)
   286 
   287 (*compose version: arguments are as for bicompose.*)
   288 fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i st = st |>
   289   (compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule), nsubgoal) i
   290    handle TERM (msg,_)   => (writeln msg;  no_tac)
   291 	| THM  (msg,_,_) => (writeln msg;  no_tac));
   292 
   293 (*"Resolve" version.  Note: res_inst_tac cannot behave sensibly if the
   294   terms that are substituted contain (term or type) unknowns from the
   295   goal, because it is unable to instantiate goal unknowns at the same time.
   296 
   297   The type checker is instructed not to freeze flexible type vars that
   298   were introduced during type inference and still remain in the term at the
   299   end.  This increases flexibility but can introduce schematic type vars in
   300   goals.
   301 *)
   302 fun res_inst_tac sinsts rule i =
   303     compose_inst_tac sinsts (false, rule, nprems_of rule) i;
   304 
   305 (*eresolve elimination version*)
   306 fun eres_inst_tac sinsts rule i =
   307     compose_inst_tac sinsts (true, rule, nprems_of rule) i;
   308 
   309 (*For forw_inst_tac and dres_inst_tac.  Preserve Var indexes of rl;
   310   increment revcut_rl instead.*)
   311 fun make_elim_preserve rl = 
   312   let val {maxidx,...} = rep_thm rl
   313       fun cvar ixn = cterm_of (sign_of ProtoPure.thy) (Var(ixn,propT));
   314       val revcut_rl' = 
   315 	  instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
   316 			     (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
   317       val arg = (false, rl, nprems_of rl)
   318       val [th] = Sequence.list_of_s (bicompose false arg 1 revcut_rl')
   319   in  th  end
   320   handle Bind => raise THM("make_elim_preserve", 1, [rl]);
   321 
   322 (*instantiate and cut -- for a FACT, anyway...*)
   323 fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule);
   324 
   325 (*forward tactic applies a RULE to an assumption without deleting it*)
   326 fun forw_inst_tac sinsts rule = cut_inst_tac sinsts rule THEN' assume_tac;
   327 
   328 (*dresolve tactic applies a RULE to replace an assumption*)
   329 fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule);
   330 
   331 (*Deletion of an assumption*)
   332 fun thin_tac s = eres_inst_tac [("V",s)] thin_rl;
   333 
   334 (*** Applications of cut_rl ***)
   335 
   336 (*Used by metacut_tac*)
   337 fun bires_cut_tac arg i =
   338     resolve_tac [cut_rl] i  THEN  biresolve_tac arg (i+1) ;
   339 
   340 (*The conclusion of the rule gets assumed in subgoal i,
   341   while subgoal i+1,... are the premises of the rule.*)
   342 fun metacut_tac rule = bires_cut_tac [(false,rule)];
   343 
   344 (*Recognizes theorems that are not rules, but simple propositions*)
   345 fun is_fact rl =
   346     case prems_of rl of
   347 	[] => true  |  _::_ => false;
   348 
   349 (*"Cut" all facts from theorem list into the goal as assumptions. *)
   350 fun cut_facts_tac ths i =
   351     EVERY (map (fn th => metacut_tac th i) (filter is_fact ths));
   352 
   353 (*Introduce the given proposition as a lemma and subgoal*)
   354 fun subgoal_tac sprop i st = 
   355   let val st'    = Sequence.hd (res_inst_tac [("psi", sprop)] cut_rl i st)
   356       val concl' = Logic.strip_assums_concl (List.nth(prems_of st', i))
   357   in  
   358       if null (term_tvars concl') then ()
   359       else warning"Type variables in new subgoal: add a type constraint?";
   360       Sequence.single st'
   361   end;
   362 
   363 (*Introduce a list of lemmas and subgoals*)
   364 fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops);
   365 
   366 
   367 (**** Indexing and filtering of theorems ****)
   368 
   369 (*Returns the list of potentially resolvable theorems for the goal "prem",
   370 	using the predicate  could(subgoal,concl).
   371   Resulting list is no longer than "limit"*)
   372 fun filter_thms could (limit, prem, ths) =
   373   let val pb = Logic.strip_assums_concl prem;   (*delete assumptions*)
   374       fun filtr (limit, []) = []
   375 	| filtr (limit, th::ths) =
   376 	    if limit=0 then  []
   377 	    else if could(pb, concl_of th)  then th :: filtr(limit-1, ths)
   378 	    else filtr(limit,ths)
   379   in  filtr(limit,ths)  end;
   380 
   381 
   382 (*** biresolution and resolution using nets ***)
   383 
   384 (** To preserve the order of the rules, tag them with increasing integers **)
   385 
   386 (*insert tags*)
   387 fun taglist k [] = []
   388   | taglist k (x::xs) = (k,x) :: taglist (k+1) xs;
   389 
   390 (*remove tags and suppress duplicates -- list is assumed sorted!*)
   391 fun untaglist [] = []
   392   | untaglist [(k:int,x)] = [x]
   393   | untaglist ((k,x) :: (rest as (k',x')::_)) =
   394       if k=k' then untaglist rest
   395       else    x :: untaglist rest;
   396 
   397 (*return list elements in original order*)
   398 fun orderlist kbrls = untaglist (sort (fn(x,y)=> #1 x < #1 y) kbrls); 
   399 
   400 (*insert one tagged brl into the pair of nets*)
   401 fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) =
   402     if eres then 
   403 	case prems_of th of
   404 	    prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false))
   405 	  | [] => error"insert_tagged_brl: elimination rule with no premises"
   406     else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet);
   407 
   408 (*build a pair of nets for biresolution*)
   409 fun build_netpair netpair brls = 
   410     foldr insert_tagged_brl (taglist 1 brls, netpair);
   411 
   412 (*delete one kbrl from the pair of nets;
   413   we don't know the value of k, so we use 0 and ignore it in the comparison*)
   414 local
   415   fun eq_kbrl ((k,(eres,th)), (k',(eres',th'))) = eq_thm (th,th')
   416 in
   417 fun delete_tagged_brl (brl as (eres,th), (inet,enet)) =
   418     if eres then 
   419 	case prems_of th of
   420 	    prem::_ => (inet, Net.delete_term ((prem, (0,brl)), enet, eq_kbrl))
   421 	  | []      => (inet,enet)     (*no major premise: ignore*)
   422     else (Net.delete_term ((concl_of th, (0,brl)), inet, eq_kbrl), enet);
   423 end;
   424 
   425 
   426 (*biresolution using a pair of nets rather than rules.  
   427     function "order" must sort and possibly filter the list of brls.
   428     boolean "match" indicates matching or unification.*)
   429 fun biresolution_from_nets_tac order match (inet,enet) =
   430   SUBGOAL
   431     (fn (prem,i) =>
   432       let val hyps = Logic.strip_assums_hyp prem
   433           and concl = Logic.strip_assums_concl prem 
   434           val kbrls = Net.unify_term inet concl @
   435                       List.concat (map (Net.unify_term enet) hyps)
   436       in PRIMSEQ (biresolution match (order kbrls) i) end);
   437 
   438 (*versions taking pre-built nets.  No filtering of brls*)
   439 val biresolve_from_nets_tac = biresolution_from_nets_tac orderlist false;
   440 val bimatch_from_nets_tac   = biresolution_from_nets_tac orderlist true;
   441 
   442 (*fast versions using nets internally*)
   443 val net_biresolve_tac =
   444     biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty);
   445 
   446 val net_bimatch_tac =
   447     bimatch_from_nets_tac o build_netpair(Net.empty,Net.empty);
   448 
   449 (*** Simpler version for resolve_tac -- only one net, and no hyps ***)
   450 
   451 (*insert one tagged rl into the net*)
   452 fun insert_krl (krl as (k,th), net) =
   453     Net.insert_term ((concl_of th, krl), net, K false);
   454 
   455 (*build a net of rules for resolution*)
   456 fun build_net rls = 
   457     foldr insert_krl (taglist 1 rls, Net.empty);
   458 
   459 (*resolution using a net rather than rules; pred supports filt_resolve_tac*)
   460 fun filt_resolution_from_net_tac match pred net =
   461   SUBGOAL
   462     (fn (prem,i) =>
   463       let val krls = Net.unify_term net (Logic.strip_assums_concl prem)
   464       in 
   465 	 if pred krls  
   466          then PRIMSEQ
   467 		(biresolution match (map (pair false) (orderlist krls)) i)
   468          else no_tac
   469       end);
   470 
   471 (*Resolve the subgoal using the rules (making a net) unless too flexible,
   472    which means more than maxr rules are unifiable.      *)
   473 fun filt_resolve_tac rules maxr = 
   474     let fun pred krls = length krls <= maxr
   475     in  filt_resolution_from_net_tac false pred (build_net rules)  end;
   476 
   477 (*versions taking pre-built nets*)
   478 val resolve_from_net_tac = filt_resolution_from_net_tac false (K true);
   479 val match_from_net_tac = filt_resolution_from_net_tac true (K true);
   480 
   481 (*fast versions using nets internally*)
   482 val net_resolve_tac = resolve_from_net_tac o build_net;
   483 val net_match_tac = match_from_net_tac o build_net;
   484 
   485 
   486 (*** For Natural Deduction using (bires_flg, rule) pairs ***)
   487 
   488 (*The number of new subgoals produced by the brule*)
   489 fun subgoals_of_brl (true,rule)  = nprems_of rule - 1
   490   | subgoals_of_brl (false,rule) = nprems_of rule;
   491 
   492 (*Less-than test: for sorting to minimize number of new subgoals*)
   493 fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2;
   494 
   495 
   496 (*** Meta-Rewriting Tactics ***)
   497 
   498 fun result1 tacf mss thm =
   499   apsome fst (Sequence.pull (tacf mss thm));
   500 
   501 val simple_prover =
   502   result1 (fn mss => ALLGOALS (resolve_tac (prems_of_mss mss)));
   503 
   504 val rewrite_rule = Drule.rewrite_rule_aux simple_prover;
   505 val rewrite_goals_rule = Drule.rewrite_goals_rule_aux simple_prover;
   506 
   507 
   508 (*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
   509 fun asm_rewrite_goal_tac mode prover_tac mss =
   510       SELECT_GOAL 
   511         (PRIMITIVE
   512 	   (rewrite_goal_rule mode (result1 prover_tac) mss 1));
   513 
   514 (*Rewrite throughout proof state. *)
   515 fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
   516 
   517 (*Rewrite subgoals only, not main goal. *)
   518 fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
   519 
   520 fun rewtac def = rewrite_goals_tac [def];
   521 
   522 
   523 (*** for folding definitions, handling critical pairs ***)
   524 
   525 (*The depth of nesting in a term*)
   526 fun term_depth (Abs(a,T,t)) = 1 + term_depth t
   527   | term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t)
   528   | term_depth _ = 0;
   529 
   530 val lhs_of_thm = #1 o Logic.dest_equals o #prop o rep_thm;
   531 
   532 (*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
   533   Returns longest lhs first to avoid folding its subexpressions.*)
   534 fun sort_lhs_depths defs =
   535   let val keylist = make_keylist (term_depth o lhs_of_thm) defs
   536       val keys = distinct (sort op> (map #2 keylist))
   537   in  map (keyfilter keylist) keys  end;
   538 
   539 fun fold_tac defs = EVERY 
   540     (map rewrite_tac (sort_lhs_depths (map symmetric defs)));
   541 
   542 fun fold_goals_tac defs = EVERY 
   543     (map rewrite_goals_tac (sort_lhs_depths (map symmetric defs)));
   544 
   545 
   546 (*** Renaming of parameters in a subgoal
   547      Names may contain letters, digits or primes and must be
   548      separated by blanks ***)
   549 
   550 (*Calling this will generate the warning "Same as previous level" since
   551   it affects nothing but the names of bound variables!*)
   552 fun rename_tac str i = 
   553   let val cs = explode str 
   554   in  
   555   if !Logic.auto_rename 
   556   then (writeln"Note: setting Logic.auto_rename := false"; 
   557 	Logic.auto_rename := false)
   558   else ();
   559   case #2 (take_prefix (is_letdig orf is_blank) cs) of
   560       [] => PRIMITIVE (rename_params_rule (scanwords is_letdig cs, i))
   561     | c::_ => error ("Illegal character: " ^ c)
   562   end;
   563 
   564 (*Rename recent parameters using names generated from a and the suffixes,
   565   provided the string a, which represents a term, is an identifier. *)
   566 fun rename_last_tac a sufs i = 
   567   let val names = map (curry op^ a) sufs
   568   in  if Syntax.is_identifier a
   569       then PRIMITIVE (rename_params_rule (names,i))
   570       else all_tac
   571   end;
   572 
   573 (*Prunes all redundant parameters from the proof state by rewriting.
   574   DOES NOT rewrite main goal, where quantification over an unused bound
   575     variable is sometimes done to avoid the need for cut_facts_tac.*)
   576 val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
   577 
   578 (*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
   579   right to left if n is positive, and from left to right if n is negative.*)
   580 fun rotate_tac 0 i = all_tac
   581   | rotate_tac k i = PRIMITIVE (rotate_rule k i);
   582 
   583 end;
   584 
   585 open Tactic;