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