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