src/Pure/tactic.ML
author wenzelm
Thu Oct 25 02:12:10 2001 +0200 (2001-10-25)
changeset 11929 a77ad6c86564
parent 11774 3bc4f67d7fe1
child 11961 e5911a25d094
permissions -rw-r--r--
innermost_params;
     1 (*  Title:      Pure/tactic.ML
     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 BASIC_TACTIC =
    10 sig
    11   val ares_tac          : thm list -> int -> tactic
    12   val asm_rewrite_goal_tac: bool*bool*bool ->
    13     (MetaSimplifier.meta_simpset -> tactic) -> MetaSimplifier.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 biresolution_from_nets_tac:
    20         ('a list -> (bool * thm) list) ->
    21         bool -> 'a Net.net * 'a Net.net -> int -> tactic
    22   val biresolve_from_nets_tac:
    23       (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
    24   val biresolve_tac     : (bool*thm)list -> int -> tactic
    25   val build_net : thm list -> (int*thm) Net.net
    26   val build_netpair:    (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net ->
    27       (bool*thm)list -> (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net
    28   val compose_inst_tac  : (string*string)list -> (bool*thm*int) ->
    29                           int -> tactic
    30   val compose_tac       : (bool * thm * int) -> int -> tactic
    31   val cut_facts_tac     : thm list -> int -> tactic
    32   val cut_inst_tac      : (string*string)list -> thm -> int -> tactic
    33   val datac             : thm -> int -> int -> tactic
    34   val defer_tac         : int -> tactic
    35   val distinct_subgoals_tac     : tactic
    36   val dmatch_tac        : thm list -> int -> tactic
    37   val dresolve_tac      : thm list -> int -> tactic
    38   val dres_inst_tac     : (string*string)list -> thm -> int -> tactic
    39   val dtac              : thm -> int ->tactic
    40   val eatac             : thm -> int -> int -> tactic
    41   val etac              : thm -> int ->tactic
    42   val eq_assume_tac     : int -> tactic
    43   val ematch_tac        : thm list -> int -> tactic
    44   val eresolve_tac      : thm list -> int -> tactic
    45   val eres_inst_tac     : (string*string)list -> thm -> int -> tactic
    46   val fatac             : thm -> int -> int -> tactic
    47   val filter_prems_tac  : (term -> bool) -> int -> tactic
    48   val filter_thms       : (term*term->bool) -> int*term*thm list -> thm list
    49   val filt_resolve_tac  : thm list -> int -> int -> tactic
    50   val flexflex_tac      : tactic
    51   val fold_goals_tac    : thm list -> tactic
    52   val fold_rule         : thm list -> thm -> thm
    53   val fold_tac          : thm list -> tactic
    54   val forward_tac       : thm list -> int -> tactic
    55   val forw_inst_tac     : (string*string)list -> thm -> int -> tactic
    56   val ftac              : thm -> int ->tactic
    57   val insert_tagged_brl : ('a*(bool*thm)) *
    58                           (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) ->
    59                           ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net
    60   val delete_tagged_brl : (bool*thm) *
    61                          ((int*(bool*thm))Net.net * (int*(bool*thm))Net.net) ->
    62                     (int*(bool*thm))Net.net * (int*(bool*thm))Net.net
    63   val is_fact           : thm -> bool
    64   val lessb             : (bool * thm) * (bool * thm) -> bool
    65   val lift_inst_rule    : thm * int * (string*string)list * thm -> thm
    66   val make_elim         : thm -> thm
    67   val match_from_net_tac        : (int*thm) Net.net -> int -> tactic
    68   val match_tac : thm list -> int -> tactic
    69   val metacut_tac       : thm -> int -> tactic
    70   val net_bimatch_tac   : (bool*thm) list -> int -> tactic
    71   val net_biresolve_tac : (bool*thm) list -> int -> tactic
    72   val net_match_tac     : thm list -> int -> tactic
    73   val net_resolve_tac   : thm list -> int -> tactic
    74   val norm_hhf          : thm -> thm
    75   val norm_hhf_tac      : int -> tactic
    76   val PRIMITIVE         : (thm -> thm) -> tactic
    77   val PRIMSEQ           : (thm -> thm Seq.seq) -> tactic
    78   val prune_params_tac  : tactic
    79   val rename_params_tac : string list -> int -> tactic
    80   val rename_tac        : string -> int -> tactic
    81   val rename_last_tac   : string -> string list -> int -> tactic
    82   val resolve_from_net_tac      : (int*thm) Net.net -> int -> tactic
    83   val resolve_tac       : thm list -> int -> tactic
    84   val res_inst_tac      : (string*string)list -> thm -> int -> tactic
    85   val rewrite_goal_tac  : thm list -> int -> tactic
    86   val rewrite_goals_rule: thm list -> thm -> thm
    87   val rewrite_rule      : thm list -> thm -> thm
    88   val rewrite_goals_tac : thm list -> tactic
    89   val rewrite_tac       : thm list -> tactic
    90   val rewtac            : thm -> tactic
    91   val rotate_tac        : int -> int -> tactic
    92   val rtac              : thm -> int -> tactic
    93   val rule_by_tactic    : tactic -> thm -> thm
    94   val solve_tac         : thm list -> int -> tactic
    95   val subgoal_tac       : string -> int -> tactic
    96   val subgoals_tac      : string list -> int -> tactic
    97   val subgoals_of_brl   : bool * thm -> int
    98   val term_lift_inst_rule       :
    99       thm * int * (indexname*typ)list * ((indexname*typ)*term)list  * thm
   100       -> thm
   101   val instantiate_tac   : (string * string) list -> tactic
   102   val thin_tac          : string -> int -> tactic
   103   val trace_goalno_tac  : (int -> tactic) -> int -> tactic
   104 end;
   105 
   106 signature TACTIC =
   107 sig
   108   include BASIC_TACTIC
   109   val innermost_params: int -> thm -> (string * typ) list
   110   val untaglist: (int * 'a) list -> 'a list
   111   val orderlist: (int * 'a) list -> 'a list
   112   val rewrite: bool -> thm list -> cterm -> thm
   113   val rewrite_cterm: bool -> thm list -> cterm -> cterm
   114   val simplify: bool -> thm list -> thm -> thm
   115 end;
   116 
   117 structure Tactic: TACTIC =
   118 struct
   119 
   120 (*Discover which goal is chosen:  SOMEGOAL(trace_goalno_tac tac) *)
   121 fun trace_goalno_tac tac i st =
   122     case Seq.pull(tac i st) of
   123         None    => Seq.empty
   124       | seqcell => (writeln ("Subgoal " ^ string_of_int i ^ " selected");
   125                          Seq.make(fn()=> seqcell));
   126 
   127 (*Makes a rule by applying a tactic to an existing rule*)
   128 fun rule_by_tactic tac rl =
   129   let val (st, thaw) = freeze_thaw (zero_var_indexes rl)
   130   in case Seq.pull (tac st)  of
   131         None        => raise THM("rule_by_tactic", 0, [rl])
   132       | Some(st',_) => Thm.varifyT (thaw st')
   133   end;
   134 
   135 (*** Basic tactics ***)
   136 
   137 (*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
   138 fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Seq.empty;
   139 
   140 (*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
   141 fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun);
   142 
   143 (*** The following fail if the goal number is out of range:
   144      thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
   145 
   146 (*Solve subgoal i by assumption*)
   147 fun assume_tac i = PRIMSEQ (assumption i);
   148 
   149 (*Solve subgoal i by assumption, using no unification*)
   150 fun eq_assume_tac i = PRIMITIVE (eq_assumption i);
   151 
   152 (** Resolution/matching tactics **)
   153 
   154 (*The composition rule/state: no lifting or var renaming.
   155   The arg = (bires_flg, orule, m) ;  see bicompose for explanation.*)
   156 fun compose_tac arg i = PRIMSEQ (bicompose false arg i);
   157 
   158 (*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
   159   like [| P&Q; P==>R |] ==> R *)
   160 fun make_elim rl = zero_var_indexes (rl RS revcut_rl);
   161 
   162 (*Attack subgoal i by resolution, using flags to indicate elimination rules*)
   163 fun biresolve_tac brules i = PRIMSEQ (biresolution false brules i);
   164 
   165 (*Resolution: the simple case, works for introduction rules*)
   166 fun resolve_tac rules = biresolve_tac (map (pair false) rules);
   167 
   168 (*Resolution with elimination rules only*)
   169 fun eresolve_tac rules = biresolve_tac (map (pair true) rules);
   170 
   171 (*Forward reasoning using destruction rules.*)
   172 fun forward_tac rls = resolve_tac (map make_elim rls) THEN' assume_tac;
   173 
   174 (*Like forward_tac, but deletes the assumption after use.*)
   175 fun dresolve_tac rls = eresolve_tac (map make_elim rls);
   176 
   177 (*Shorthand versions: for resolution with a single theorem*)
   178 val atac    =   assume_tac;
   179 fun rtac rl =  resolve_tac [rl];
   180 fun dtac rl = dresolve_tac [rl];
   181 fun etac rl = eresolve_tac [rl];
   182 fun ftac rl =  forward_tac [rl];
   183 fun datac thm j = EVERY' (dtac thm::replicate j atac);
   184 fun eatac thm j = EVERY' (etac thm::replicate j atac);
   185 fun fatac thm j = EVERY' (ftac thm::replicate j atac);
   186 
   187 (*Use an assumption or some rules ... A popular combination!*)
   188 fun ares_tac rules = assume_tac  ORELSE'  resolve_tac rules;
   189 
   190 fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac;
   191 
   192 (*Matching tactics -- as above, but forbid updating of state*)
   193 fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i);
   194 fun match_tac rules  = bimatch_tac (map (pair false) rules);
   195 fun ematch_tac rules = bimatch_tac (map (pair true) rules);
   196 fun dmatch_tac rls   = ematch_tac (map make_elim rls);
   197 
   198 (*Smash all flex-flex disagreement pairs in the proof state.*)
   199 val flexflex_tac = PRIMSEQ flexflex_rule;
   200 
   201 
   202 (*Remove duplicate subgoals.  By Mark Staples*)
   203 local
   204 fun cterm_aconv (a,b) = #t (rep_cterm a) aconv #t (rep_cterm b);
   205 in
   206 fun distinct_subgoals_tac state =
   207     let val (frozth,thawfn) = freeze_thaw state
   208         val froz_prems = cprems_of frozth
   209         val assumed = implies_elim_list frozth (map assume froz_prems)
   210         val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems)
   211                                         assumed;
   212     in  Seq.single (thawfn implied)  end
   213 end;
   214 
   215 
   216 (*Determine print names of goal parameters (reversed)*)
   217 fun innermost_params i st =
   218   let val (_, _, Bi, _) = dest_state (st, i)
   219   in rename_wrt_term Bi (Logic.strip_params Bi) end;
   220 
   221 (*Lift and instantiate a rule wrt the given state and subgoal number *)
   222 fun lift_inst_rule (st, i, sinsts, rule) =
   223 let val {maxidx,sign,...} = rep_thm st
   224     val (_, _, Bi, _) = dest_state(st,i)
   225     val params = Logic.strip_params Bi          (*params of subgoal i*)
   226     val params = rev(rename_wrt_term Bi params) (*as they are printed*)
   227     val paramTs = map #2 params
   228     and inc = maxidx+1
   229     fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> incr_tvar inc T)
   230       | liftvar t = raise TERM("Variable expected", [t]);
   231     fun liftterm t = list_abs_free (params,
   232                                     Logic.incr_indexes(paramTs,inc) t)
   233     (*Lifts instantiation pair over params*)
   234     fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
   235     fun lifttvar((a,i),ctyp) =
   236         let val {T,sign} = rep_ctyp ctyp
   237         in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
   238     val rts = types_sorts rule and (types,sorts) = types_sorts st
   239     fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
   240       | types'(ixn) = types ixn;
   241     val used = add_term_tvarnames
   242                   (#prop(rep_thm st) $ #prop(rep_thm rule),[])
   243     val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts
   244 in Drule.instantiate (map lifttvar Tinsts, map liftpair insts)
   245                      (lift_rule (st,i) rule)
   246 end;
   247 
   248 (*
   249 Like lift_inst_rule but takes terms, not strings, where the terms may contain
   250 Bounds referring to parameters of the subgoal.
   251 
   252 insts: [...,(vj,tj),...]
   253 
   254 The tj may contain references to parameters of subgoal i of the state st
   255 in the form of Bound k, i.e. the tj may be subterms of the subgoal.
   256 To saturate the lose bound vars, the tj are enclosed in abstractions
   257 corresponding to the parameters of subgoal i, thus turning them into
   258 functions. At the same time, the types of the vj are lifted.
   259 
   260 NB: the types in insts must be correctly instantiated already,
   261     i.e. Tinsts is not applied to insts.
   262 *)
   263 fun term_lift_inst_rule (st, i, Tinsts, insts, rule) =
   264 let val {maxidx,sign,...} = rep_thm st
   265     val (_, _, Bi, _) = dest_state(st,i)
   266     val params = Logic.strip_params Bi          (*params of subgoal i*)
   267     val paramTs = map #2 params
   268     and inc = maxidx+1
   269     fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> incr_tvar inc T)
   270     (*lift only Var, not term, which must be lifted already*)
   271     fun liftpair (v,t) = (cterm_of sign (liftvar v), cterm_of sign t)
   272     fun liftTpair((a,i),T) = ((a,i+inc), ctyp_of sign (incr_tvar inc T))
   273 in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
   274                      (lift_rule (st,i) rule)
   275 end;
   276 
   277 (*** Resolve after lifting and instantation; may refer to parameters of the
   278      subgoal.  Fails if "i" is out of range.  ***)
   279 
   280 (*compose version: arguments are as for bicompose.*)
   281 fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i st =
   282   if i > nprems_of st then no_tac st
   283   else st |>
   284     (compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule), nsubgoal) i
   285      handle TERM (msg,_)   => (writeln msg;  no_tac)
   286           | THM  (msg,_,_) => (writeln msg;  no_tac));
   287 
   288 (*"Resolve" version.  Note: res_inst_tac cannot behave sensibly if the
   289   terms that are substituted contain (term or type) unknowns from the
   290   goal, because it is unable to instantiate goal unknowns at the same time.
   291 
   292   The type checker is instructed not to freeze flexible type vars that
   293   were introduced during type inference and still remain in the term at the
   294   end.  This increases flexibility but can introduce schematic type vars in
   295   goals.
   296 *)
   297 fun res_inst_tac sinsts rule i =
   298     compose_inst_tac sinsts (false, rule, nprems_of rule) i;
   299 
   300 (*eresolve elimination version*)
   301 fun eres_inst_tac sinsts rule i =
   302     compose_inst_tac sinsts (true, rule, nprems_of rule) i;
   303 
   304 (*For forw_inst_tac and dres_inst_tac.  Preserve Var indexes of rl;
   305   increment revcut_rl instead.*)
   306 fun make_elim_preserve rl =
   307   let val {maxidx,...} = rep_thm rl
   308       fun cvar ixn = cterm_of (Theory.sign_of ProtoPure.thy) (Var(ixn,propT));
   309       val revcut_rl' =
   310           instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
   311                              (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
   312       val arg = (false, rl, nprems_of rl)
   313       val [th] = Seq.list_of (bicompose false arg 1 revcut_rl')
   314   in  th  end
   315   handle Bind => raise THM("make_elim_preserve", 1, [rl]);
   316 
   317 (*instantiate and cut -- for a FACT, anyway...*)
   318 fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule);
   319 
   320 (*forward tactic applies a RULE to an assumption without deleting it*)
   321 fun forw_inst_tac sinsts rule = cut_inst_tac sinsts rule THEN' assume_tac;
   322 
   323 (*dresolve tactic applies a RULE to replace an assumption*)
   324 fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule);
   325 
   326 (*instantiate variables in the whole state*)
   327 val instantiate_tac = PRIMITIVE o read_instantiate;
   328 
   329 (*Deletion of an assumption*)
   330 fun thin_tac s = eres_inst_tac [("V",s)] thin_rl;
   331 
   332 (*** Applications of cut_rl ***)
   333 
   334 (*Used by metacut_tac*)
   335 fun bires_cut_tac arg i =
   336     resolve_tac [cut_rl] i  THEN  biresolve_tac arg (i+1) ;
   337 
   338 (*The conclusion of the rule gets assumed in subgoal i,
   339   while subgoal i+1,... are the premises of the rule.*)
   340 fun metacut_tac rule = bires_cut_tac [(false,rule)];
   341 
   342 (*Recognizes theorems that are not rules, but simple propositions*)
   343 fun is_fact rl =
   344     case prems_of rl of
   345         [] => true  |  _::_ => false;
   346 
   347 (*"Cut" all facts from theorem list into the goal as assumptions. *)
   348 fun cut_facts_tac ths i =
   349     EVERY (map (fn th => metacut_tac th i) (filter is_fact ths));
   350 
   351 (*Introduce the given proposition as a lemma and subgoal*)
   352 fun subgoal_tac sprop i st =
   353   let val st'    = Seq.hd (res_inst_tac [("psi", sprop)] cut_rl i st)
   354       val concl' = Logic.strip_assums_concl (List.nth(prems_of st', i))
   355   in
   356       if null (term_tvars concl') then ()
   357       else warning"Type variables in new subgoal: add a type constraint?";
   358       Seq.single st'
   359   end;
   360 
   361 (*Introduce a list of lemmas and subgoals*)
   362 fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops);
   363 
   364 
   365 (**** Indexing and filtering of theorems ****)
   366 
   367 (*Returns the list of potentially resolvable theorems for the goal "prem",
   368         using the predicate  could(subgoal,concl).
   369   Resulting list is no longer than "limit"*)
   370 fun filter_thms could (limit, prem, ths) =
   371   let val pb = Logic.strip_assums_concl prem;   (*delete assumptions*)
   372       fun filtr (limit, []) = []
   373         | filtr (limit, th::ths) =
   374             if limit=0 then  []
   375             else if could(pb, concl_of th)  then th :: filtr(limit-1, ths)
   376             else filtr(limit,ths)
   377   in  filtr(limit,ths)  end;
   378 
   379 
   380 (*** biresolution and resolution using nets ***)
   381 
   382 (** To preserve the order of the rules, tag them with increasing integers **)
   383 
   384 (*insert tags*)
   385 fun taglist k [] = []
   386   | taglist k (x::xs) = (k,x) :: taglist (k+1) xs;
   387 
   388 (*remove tags and suppress duplicates -- list is assumed sorted!*)
   389 fun untaglist [] = []
   390   | untaglist [(k:int,x)] = [x]
   391   | untaglist ((k,x) :: (rest as (k',x')::_)) =
   392       if k=k' then untaglist rest
   393       else    x :: untaglist rest;
   394 
   395 (*return list elements in original order*)
   396 fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls);
   397 
   398 (*insert one tagged brl into the pair of nets*)
   399 fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) =
   400     if eres then
   401         case prems_of th of
   402             prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false))
   403           | [] => error"insert_tagged_brl: elimination rule with no premises"
   404     else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet);
   405 
   406 (*build a pair of nets for biresolution*)
   407 fun build_netpair netpair brls =
   408     foldr insert_tagged_brl (taglist 1 brls, netpair);
   409 
   410 (*delete one kbrl from the pair of nets;
   411   we don't know the value of k, so we use 0 and ignore it in the comparison*)
   412 local
   413   fun eq_kbrl ((k,(eres,th)), (k',(eres',th'))) = eq_thm (th,th')
   414 in
   415 fun delete_tagged_brl (brl as (eres,th), (inet,enet)) =
   416     if eres then
   417         case prems_of th of
   418             prem::_ => (inet, Net.delete_term ((prem, (0,brl)), enet, eq_kbrl))
   419           | []      => (inet,enet)     (*no major premise: ignore*)
   420     else (Net.delete_term ((concl_of th, (0,brl)), inet, eq_kbrl), enet);
   421 end;
   422 
   423 
   424 (*biresolution using a pair of nets rather than rules.
   425     function "order" must sort and possibly filter the list of brls.
   426     boolean "match" indicates matching or unification.*)
   427 fun biresolution_from_nets_tac order match (inet,enet) =
   428   SUBGOAL
   429     (fn (prem,i) =>
   430       let val hyps = Logic.strip_assums_hyp prem
   431           and concl = Logic.strip_assums_concl prem
   432           val kbrls = Net.unify_term inet concl @
   433                       List.concat (map (Net.unify_term enet) hyps)
   434       in PRIMSEQ (biresolution match (order kbrls) i) end);
   435 
   436 (*versions taking pre-built nets.  No filtering of brls*)
   437 val biresolve_from_nets_tac = biresolution_from_nets_tac orderlist false;
   438 val bimatch_from_nets_tac   = biresolution_from_nets_tac orderlist true;
   439 
   440 (*fast versions using nets internally*)
   441 val net_biresolve_tac =
   442     biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty);
   443 
   444 val net_bimatch_tac =
   445     bimatch_from_nets_tac o build_netpair(Net.empty,Net.empty);
   446 
   447 (*** Simpler version for resolve_tac -- only one net, and no hyps ***)
   448 
   449 (*insert one tagged rl into the net*)
   450 fun insert_krl (krl as (k,th), net) =
   451     Net.insert_term ((concl_of th, krl), net, K false);
   452 
   453 (*build a net of rules for resolution*)
   454 fun build_net rls =
   455     foldr insert_krl (taglist 1 rls, Net.empty);
   456 
   457 (*resolution using a net rather than rules; pred supports filt_resolve_tac*)
   458 fun filt_resolution_from_net_tac match pred net =
   459   SUBGOAL
   460     (fn (prem,i) =>
   461       let val krls = Net.unify_term net (Logic.strip_assums_concl prem)
   462       in
   463          if pred krls
   464          then PRIMSEQ
   465                 (biresolution match (map (pair false) (orderlist krls)) i)
   466          else no_tac
   467       end);
   468 
   469 (*Resolve the subgoal using the rules (making a net) unless too flexible,
   470    which means more than maxr rules are unifiable.      *)
   471 fun filt_resolve_tac rules maxr =
   472     let fun pred krls = length krls <= maxr
   473     in  filt_resolution_from_net_tac false pred (build_net rules)  end;
   474 
   475 (*versions taking pre-built nets*)
   476 val resolve_from_net_tac = filt_resolution_from_net_tac false (K true);
   477 val match_from_net_tac = filt_resolution_from_net_tac true (K true);
   478 
   479 (*fast versions using nets internally*)
   480 val net_resolve_tac = resolve_from_net_tac o build_net;
   481 val net_match_tac = match_from_net_tac o build_net;
   482 
   483 
   484 (*** For Natural Deduction using (bires_flg, rule) pairs ***)
   485 
   486 (*The number of new subgoals produced by the brule*)
   487 fun subgoals_of_brl (true,rule)  = nprems_of rule - 1
   488   | subgoals_of_brl (false,rule) = nprems_of rule;
   489 
   490 (*Less-than test: for sorting to minimize number of new subgoals*)
   491 fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2;
   492 
   493 
   494 (*** Meta-Rewriting Tactics ***)
   495 
   496 fun result1 tacf mss thm =
   497   apsome fst (Seq.pull (tacf mss thm));
   498 
   499 val simple_prover =
   500   result1 (fn mss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_mss mss)));
   501 
   502 val rewrite = MetaSimplifier.rewrite_aux simple_prover;
   503 val rewrite_cterm = (#2 o Thm.dest_comb o #prop o Thm.crep_thm) ooo rewrite;
   504 val simplify = MetaSimplifier.simplify_aux simple_prover;
   505 val rewrite_rule = simplify true;
   506 val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
   507 
   508 (*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
   509 fun asm_rewrite_goal_tac mode prover_tac mss =
   510   SELECT_GOAL
   511     (PRIMITIVE (MetaSimplifier.rewrite_goal_rule mode (result1 prover_tac) mss 1));
   512 
   513 fun rewrite_goal_tac rews =
   514   asm_rewrite_goal_tac (true, false, false) (K no_tac) (MetaSimplifier.mss_of rews);
   515 
   516 (*Rewrite throughout proof state. *)
   517 fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
   518 
   519 (*Rewrite subgoals only, not main goal. *)
   520 fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
   521 fun rewtac def = rewrite_goals_tac [def];
   522 
   523 fun norm_hhf th =
   524   (if Logic.is_norm_hhf (#prop (Thm.rep_thm th)) then th else rewrite_rule [Drule.norm_hhf_eq] th)
   525   |> Drule.forall_elim_vars_safe;
   526 
   527 val norm_hhf_tac = SUBGOAL (fn (t, i) =>
   528   if Logic.is_norm_hhf t then all_tac
   529   else rewrite_goal_tac [Drule.norm_hhf_eq] i);
   530 
   531 
   532 (*** for folding definitions, handling critical pairs ***)
   533 
   534 (*The depth of nesting in a term*)
   535 fun term_depth (Abs(a,T,t)) = 1 + term_depth t
   536   | term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t)
   537   | term_depth _ = 0;
   538 
   539 val lhs_of_thm = #1 o Logic.dest_equals o #prop o rep_thm;
   540 
   541 (*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
   542   Returns longest lhs first to avoid folding its subexpressions.*)
   543 fun sort_lhs_depths defs =
   544   let val keylist = make_keylist (term_depth o lhs_of_thm) defs
   545       val keys = distinct (sort (rev_order o int_ord) (map #2 keylist))
   546   in  map (keyfilter keylist) keys  end;
   547 
   548 val rev_defs = sort_lhs_depths o map symmetric;
   549 
   550 fun fold_rule defs thm = foldl (fn (th, ds) => rewrite_rule ds th) (thm, rev_defs defs);
   551 fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs));
   552 fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
   553 
   554 
   555 (*** Renaming of parameters in a subgoal
   556      Names may contain letters, digits or primes and must be
   557      separated by blanks ***)
   558 
   559 (*Calling this will generate the warning "Same as previous level" since
   560   it affects nothing but the names of bound variables!*)
   561 fun rename_params_tac xs i =
   562   (if !Logic.auto_rename
   563     then (warning "Resetting Logic.auto_rename";
   564         Logic.auto_rename := false)
   565    else (); PRIMITIVE (rename_params_rule (xs, i)));
   566 
   567 fun rename_tac str i =
   568   let val cs = Symbol.explode str in
   569   case #2 (take_prefix (Symbol.is_letdig orf Symbol.is_blank) cs) of
   570       [] => rename_params_tac (scanwords Symbol.is_letdig cs) i
   571     | c::_ => error ("Illegal character: " ^ c)
   572   end;
   573 
   574 (*Rename recent parameters using names generated from a and the suffixes,
   575   provided the string a, which represents a term, is an identifier. *)
   576 fun rename_last_tac a sufs i =
   577   let val names = map (curry op^ a) sufs
   578   in  if Syntax.is_identifier a
   579       then PRIMITIVE (rename_params_rule (names,i))
   580       else all_tac
   581   end;
   582 
   583 (*Prunes all redundant parameters from the proof state by rewriting.
   584   DOES NOT rewrite main goal, where quantification over an unused bound
   585     variable is sometimes done to avoid the need for cut_facts_tac.*)
   586 val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
   587 
   588 (*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
   589   right to left if n is positive, and from left to right if n is negative.*)
   590 fun rotate_tac 0 i = all_tac
   591   | rotate_tac k i = PRIMITIVE (rotate_rule k i);
   592 
   593 (*Rotates the given subgoal to be the last.*)
   594 fun defer_tac i = PRIMITIVE (permute_prems (i-1) 1);
   595 
   596 (* remove premises that do not satisfy p; fails if all prems satisfy p *)
   597 fun filter_prems_tac p =
   598   let fun Then None tac = Some tac
   599         | Then (Some tac) tac' = Some(tac THEN' tac');
   600       fun thins ((tac,n),H) =
   601         if p H then (tac,n+1)
   602         else (Then tac (rotate_tac n THEN' etac thin_rl),0);
   603   in SUBGOAL(fn (subg,n) =>
   604        let val Hs = Logic.strip_assums_hyp subg
   605        in case fst(foldl thins ((None,0),Hs)) of
   606             None => no_tac | Some tac => tac n
   607        end)
   608   end;
   609 
   610 end;
   611 
   612 structure BasicTactic: BASIC_TACTIC = Tactic;
   613 open BasicTactic;