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