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