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