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