src/Pure/tactic.ML
author paulson
Fri Jun 14 12:27:11 1996 +0200 (1996-06-14)
changeset 1801 927a31ba4346
parent 1501 bb7f99a0a6f0
child 1951 f2b8005bdc6e
permissions -rw-r--r--
Added delete function for brls
     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 (*** Applications of cut_rl ***)
   251 
   252 (*Used by metacut_tac*)
   253 fun bires_cut_tac arg i =
   254     resolve_tac [cut_rl] i  THEN  biresolve_tac arg (i+1) ;
   255 
   256 (*The conclusion of the rule gets assumed in subgoal i,
   257   while subgoal i+1,... are the premises of the rule.*)
   258 fun metacut_tac rule = bires_cut_tac [(false,rule)];
   259 
   260 (*Recognizes theorems that are not rules, but simple propositions*)
   261 fun is_fact rl =
   262     case prems_of rl of
   263 	[] => true  |  _::_ => false;
   264 
   265 (*"Cut" all facts from theorem list into the goal as assumptions. *)
   266 fun cut_facts_tac ths i =
   267     EVERY (map (fn th => metacut_tac th i) (filter is_fact ths));
   268 
   269 (*Introduce the given proposition as a lemma and subgoal*)
   270 fun subgoal_tac sprop = res_inst_tac [("psi", sprop)] cut_rl;
   271 
   272 (*Introduce a list of lemmas and subgoals*)
   273 fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops);
   274 
   275 
   276 (**** Indexing and filtering of theorems ****)
   277 
   278 (*Returns the list of potentially resolvable theorems for the goal "prem",
   279 	using the predicate  could(subgoal,concl).
   280   Resulting list is no longer than "limit"*)
   281 fun filter_thms could (limit, prem, ths) =
   282   let val pb = Logic.strip_assums_concl prem;   (*delete assumptions*)
   283       fun filtr (limit, []) = []
   284 	| filtr (limit, th::ths) =
   285 	    if limit=0 then  []
   286 	    else if could(pb, concl_of th)  then th :: filtr(limit-1, ths)
   287 	    else filtr(limit,ths)
   288   in  filtr(limit,ths)  end;
   289 
   290 
   291 (*** biresolution and resolution using nets ***)
   292 
   293 (** To preserve the order of the rules, tag them with increasing integers **)
   294 
   295 (*insert tags*)
   296 fun taglist k [] = []
   297   | taglist k (x::xs) = (k,x) :: taglist (k+1) xs;
   298 
   299 (*remove tags and suppress duplicates -- list is assumed sorted!*)
   300 fun untaglist [] = []
   301   | untaglist [(k:int,x)] = [x]
   302   | untaglist ((k,x) :: (rest as (k',x')::_)) =
   303       if k=k' then untaglist rest
   304       else    x :: untaglist rest;
   305 
   306 (*return list elements in original order*)
   307 val orderlist = untaglist o sort (fn(x,y)=> #1 x < #1 y); 
   308 
   309 (*insert one tagged brl into the pair of nets*)
   310 fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) =
   311     if eres then 
   312 	case prems_of th of
   313 	    prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false))
   314 	  | [] => error"insert_tagged_brl: elimination rule with no premises"
   315     else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet);
   316 
   317 (*build a pair of nets for biresolution*)
   318 fun build_netpair netpair brls = 
   319     foldr insert_tagged_brl (taglist 1 brls, netpair);
   320 
   321 (*delete one kbrl from the pair of nets;
   322   we don't know the value of k, so we use 0 and ignore it in the comparison*)
   323 local
   324   fun eq_kbrl ((k,(eres,th)), (k',(eres',th'))) = eq_thm (th,th')
   325 in
   326 fun delete_tagged_brl (brl as (eres,th), (inet,enet)) =
   327     if eres then 
   328 	case prems_of th of
   329 	    prem::_ => (inet, Net.delete_term ((prem, (0,brl)), enet, eq_kbrl))
   330 	  | [] => error"delete_brl: elimination rule with no premises"
   331     else (Net.delete_term ((concl_of th, (0,brl)), inet, eq_kbrl), enet);
   332 end;
   333 
   334 
   335 (*biresolution using a pair of nets rather than rules*)
   336 fun biresolution_from_nets_tac match (inet,enet) =
   337   SUBGOAL
   338     (fn (prem,i) =>
   339       let val hyps = Logic.strip_assums_hyp prem
   340           and concl = Logic.strip_assums_concl prem 
   341           val kbrls = Net.unify_term inet concl @
   342                       flat (map (Net.unify_term enet) hyps)
   343       in PRIMSEQ (biresolution match (orderlist kbrls) i) end);
   344 
   345 (*versions taking pre-built nets*)
   346 val biresolve_from_nets_tac = biresolution_from_nets_tac false;
   347 val bimatch_from_nets_tac = biresolution_from_nets_tac true;
   348 
   349 (*fast versions using nets internally*)
   350 val net_biresolve_tac =
   351     biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty);
   352 
   353 val net_bimatch_tac =
   354     bimatch_from_nets_tac o build_netpair(Net.empty,Net.empty);
   355 
   356 (*** Simpler version for resolve_tac -- only one net, and no hyps ***)
   357 
   358 (*insert one tagged rl into the net*)
   359 fun insert_krl (krl as (k,th), net) =
   360     Net.insert_term ((concl_of th, krl), net, K false);
   361 
   362 (*build a net of rules for resolution*)
   363 fun build_net rls = 
   364     foldr insert_krl (taglist 1 rls, Net.empty);
   365 
   366 (*resolution using a net rather than rules; pred supports filt_resolve_tac*)
   367 fun filt_resolution_from_net_tac match pred net =
   368   SUBGOAL
   369     (fn (prem,i) =>
   370       let val krls = Net.unify_term net (Logic.strip_assums_concl prem)
   371       in 
   372 	 if pred krls  
   373          then PRIMSEQ
   374 		(biresolution match (map (pair false) (orderlist krls)) i)
   375          else no_tac
   376       end);
   377 
   378 (*Resolve the subgoal using the rules (making a net) unless too flexible,
   379    which means more than maxr rules are unifiable.      *)
   380 fun filt_resolve_tac rules maxr = 
   381     let fun pred krls = length krls <= maxr
   382     in  filt_resolution_from_net_tac false pred (build_net rules)  end;
   383 
   384 (*versions taking pre-built nets*)
   385 val resolve_from_net_tac = filt_resolution_from_net_tac false (K true);
   386 val match_from_net_tac = filt_resolution_from_net_tac true (K true);
   387 
   388 (*fast versions using nets internally*)
   389 val net_resolve_tac = resolve_from_net_tac o build_net;
   390 val net_match_tac = match_from_net_tac o build_net;
   391 
   392 
   393 (*** For Natural Deduction using (bires_flg, rule) pairs ***)
   394 
   395 (*The number of new subgoals produced by the brule*)
   396 fun subgoals_of_brl (true,rule)  = nprems_of rule - 1
   397   | subgoals_of_brl (false,rule) = nprems_of rule;
   398 
   399 (*Less-than test: for sorting to minimize number of new subgoals*)
   400 fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2;
   401 
   402 
   403 (*** Meta-Rewriting Tactics ***)
   404 
   405 fun result1 tacf mss thm =
   406   case Sequence.pull(tacf mss thm) of
   407     None => None
   408   | Some(thm,_) => Some(thm);
   409 
   410 (*Rewrite subgoal i only *)
   411 fun asm_rewrite_goal_tac mode prover_tac mss i =
   412       PRIMITIVE(rewrite_goal_rule mode (result1 prover_tac) mss i);
   413 
   414 (*Rewrite throughout proof state. *)
   415 fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
   416 
   417 (*Rewrite subgoals only, not main goal. *)
   418 fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
   419 
   420 fun rewtac def = rewrite_goals_tac [def];
   421 
   422 
   423 (*** for folding definitions, handling critical pairs ***)
   424 
   425 (*The depth of nesting in a term*)
   426 fun term_depth (Abs(a,T,t)) = 1 + term_depth t
   427   | term_depth (f$t) = 1 + max [term_depth f, term_depth t]
   428   | term_depth _ = 0;
   429 
   430 val lhs_of_thm = #1 o Logic.dest_equals o #prop o rep_thm;
   431 
   432 (*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
   433   Returns longest lhs first to avoid folding its subexpressions.*)
   434 fun sort_lhs_depths defs =
   435   let val keylist = make_keylist (term_depth o lhs_of_thm) defs
   436       val keys = distinct (sort op> (map #2 keylist))
   437   in  map (keyfilter keylist) keys  end;
   438 
   439 fun fold_tac defs = EVERY 
   440     (map rewrite_tac (sort_lhs_depths (map symmetric defs)));
   441 
   442 fun fold_goals_tac defs = EVERY 
   443     (map rewrite_goals_tac (sort_lhs_depths (map symmetric defs)));
   444 
   445 
   446 (*** Renaming of parameters in a subgoal
   447      Names may contain letters, digits or primes and must be
   448      separated by blanks ***)
   449 
   450 (*Calling this will generate the warning "Same as previous level" since
   451   it affects nothing but the names of bound variables!*)
   452 fun rename_tac str i = 
   453   let val cs = explode str 
   454   in  
   455   if !Logic.auto_rename 
   456   then (writeln"Note: setting Logic.auto_rename := false"; 
   457 	Logic.auto_rename := false)
   458   else ();
   459   case #2 (take_prefix (is_letdig orf is_blank) cs) of
   460       [] => PRIMITIVE (rename_params_rule (scanwords is_letdig cs, i))
   461     | c::_ => error ("Illegal character: " ^ c)
   462   end;
   463 
   464 (*Rename recent parameters using names generated from a and the suffixes,
   465   provided the string a, which represents a term, is an identifier. *)
   466 fun rename_last_tac a sufs i = 
   467   let val names = map (curry op^ a) sufs
   468   in  if Syntax.is_identifier a
   469       then PRIMITIVE (rename_params_rule (names,i))
   470       else all_tac
   471   end;
   472 
   473 (*Prunes all redundant parameters from the proof state by rewriting*)
   474 val prune_params_tac = rewrite_tac [triv_forall_equality];
   475 
   476 (*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
   477   right to left if n is positive, and from left to right if n is negative.*)
   478 fun rotate_tac n =
   479   let fun rot(n) = EVERY'(replicate n (dtac asm_rl));
   480   in if n >= 0 then rot n
   481      else SUBGOAL (fn (t,i) => rot(length(Logic.strip_assums_hyp t)+n) i)
   482   end;
   483 
   484 end;
   485 
   486 open Tactic;