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