src/Pure/tactic.ML
author wenzelm
Sun Jun 03 23:16:51 2007 +0200 (2007-06-03)
changeset 23223 7791128b39a9
parent 23178 07ba6b58b3d2
child 23492 60cf5cf30b81
permissions -rw-r--r--
cleaned up signature;
     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 trace_goalno_tac: (int -> tactic) -> int -> tactic
    12   val rule_by_tactic: tactic -> thm -> thm
    13   val assume_tac: int -> tactic
    14   val eq_assume_tac: int -> tactic
    15   val compose_tac: (bool * thm * int) -> int -> tactic
    16   val make_elim: thm -> thm
    17   val biresolve_tac: (bool * thm) list -> int -> tactic
    18   val resolve_tac: thm list -> int -> tactic
    19   val eresolve_tac: thm list -> int -> tactic
    20   val forward_tac: thm list -> int -> tactic
    21   val dresolve_tac: thm list -> int -> tactic
    22   val atac: int -> tactic
    23   val rtac: thm -> int -> tactic
    24   val dtac: thm -> int ->tactic
    25   val etac: thm -> int ->tactic
    26   val ftac: thm -> int ->tactic
    27   val datac: thm -> int -> int -> tactic
    28   val eatac: thm -> int -> int -> tactic
    29   val fatac: thm -> int -> int -> tactic
    30   val ares_tac: thm list -> int -> tactic
    31   val solve_tac: thm list -> int -> tactic
    32   val bimatch_tac: (bool * thm) list -> int -> tactic
    33   val match_tac: thm list -> int -> tactic
    34   val ematch_tac: thm list -> int -> tactic
    35   val dmatch_tac: thm list -> int -> tactic
    36   val flexflex_tac: tactic
    37   val distinct_subgoal_tac: int -> tactic
    38   val distinct_subgoals_tac: tactic
    39   val lift_inst_rule: thm * int * (string*string)list * thm -> thm
    40   val term_lift_inst_rule:
    41     thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm -> thm
    42   val compose_inst_tac: (string * string) list -> (bool * thm * int) -> int -> tactic
    43   val res_inst_tac: (string * string) list -> thm -> int -> tactic
    44   val eres_inst_tac: (string * string) list -> thm -> int -> tactic
    45   val cut_inst_tac: (string * string) list -> thm -> int -> tactic
    46   val forw_inst_tac: (string * string) list -> thm -> int -> tactic
    47   val dres_inst_tac: (string * string) list -> thm -> int -> tactic
    48   val instantiate_tac: (string * string) list -> tactic
    49   val thin_tac: string -> int -> tactic
    50   val metacut_tac: thm -> int -> tactic
    51   val cut_rules_tac: thm list -> int -> tactic
    52   val cut_facts_tac: thm list -> int -> tactic
    53   val subgoal_tac: string -> int -> tactic
    54   val subgoals_tac: string list -> int -> tactic
    55   val filter_thms: (term * term -> bool) -> int * term * thm list -> thm list
    56   val biresolution_from_nets_tac: ('a list -> (bool * thm) list) ->
    57     bool -> 'a Net.net * 'a Net.net -> int -> tactic
    58   val biresolve_from_nets_tac: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net ->
    59     int -> tactic
    60   val bimatch_from_nets_tac: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net ->
    61     int -> tactic
    62   val net_biresolve_tac: (bool * thm) list -> int -> tactic
    63   val net_bimatch_tac: (bool * thm) list -> int -> tactic
    64   val build_net: thm list -> (int * thm) Net.net
    65   val filt_resolve_tac: thm list -> int -> int -> tactic
    66   val resolve_from_net_tac: (int * thm) Net.net -> int -> tactic
    67   val match_from_net_tac: (int * thm) Net.net -> int -> tactic
    68   val net_resolve_tac: thm list -> int -> tactic
    69   val net_match_tac: thm list -> int -> tactic
    70   val subgoals_of_brl: bool * thm -> int
    71   val lessb: (bool * thm) * (bool * thm) -> bool
    72   val rename_params_tac: string list -> int -> tactic
    73   val rename_tac: string -> int -> tactic
    74   val rename_last_tac: string -> string list -> int -> tactic
    75   val rotate_tac: int -> int -> tactic
    76   val defer_tac: int -> tactic
    77   val filter_prems_tac: (term -> bool) -> int -> tactic
    78 end;
    79 
    80 signature TACTIC =
    81 sig
    82   include BASIC_TACTIC
    83   val innermost_params: int -> thm -> (string * typ) list
    84   val lift_inst_rule': thm * int * (indexname * string) list * thm -> thm
    85   val compose_inst_tac': (indexname * string) list -> (bool * thm * int) -> int -> tactic
    86   val res_inst_tac': (indexname * string) list -> thm -> int -> tactic
    87   val eres_inst_tac': (indexname * string) list -> thm -> int -> tactic
    88   val make_elim_preserve: thm -> thm
    89   val instantiate_tac': (indexname * string) list -> tactic
    90   val untaglist: (int * 'a) list -> 'a list
    91   val orderlist: (int * 'a) list -> 'a list
    92   val insert_tagged_brl: 'a * (bool * thm) ->
    93     ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
    94       ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
    95   val build_netpair: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net ->
    96     (bool * thm) list -> (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net
    97   val delete_tagged_brl: bool * thm ->
    98     ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
    99       ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
   100   val eq_kbrl: ('a * (bool * thm)) * ('a * (bool * thm)) -> bool
   101 end;
   102 
   103 structure Tactic: TACTIC =
   104 struct
   105 
   106 (*Discover which goal is chosen:  SOMEGOAL(trace_goalno_tac tac) *)
   107 fun trace_goalno_tac tac i st =
   108     case Seq.pull(tac i st) of
   109         NONE    => Seq.empty
   110       | seqcell => (tracing ("Subgoal " ^ string_of_int i ^ " selected");
   111                          Seq.make(fn()=> seqcell));
   112 
   113 (*Makes a rule by applying a tactic to an existing rule*)
   114 fun rule_by_tactic tac rl =
   115   let
   116     val ctxt = Variable.thm_context rl;
   117     val ((_, [st]), ctxt') = Variable.import_thms true [rl] ctxt;
   118   in
   119     (case Seq.pull (tac st) of
   120       NONE => raise THM ("rule_by_tactic", 0, [rl])
   121     | SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt' ctxt) st'))
   122   end;
   123 
   124 
   125 (*** Basic tactics ***)
   126 
   127 (*** The following fail if the goal number is out of range:
   128      thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
   129 
   130 (*Solve subgoal i by assumption*)
   131 fun assume_tac i = PRIMSEQ (assumption i);
   132 
   133 (*Solve subgoal i by assumption, using no unification*)
   134 fun eq_assume_tac i = PRIMITIVE (eq_assumption i);
   135 
   136 
   137 (** Resolution/matching tactics **)
   138 
   139 (*The composition rule/state: no lifting or var renaming.
   140   The arg = (bires_flg, orule, m) ;  see bicompose for explanation.*)
   141 fun compose_tac arg i = PRIMSEQ (bicompose false arg i);
   142 
   143 (*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
   144   like [| P&Q; P==>R |] ==> R *)
   145 fun make_elim rl = zero_var_indexes (rl RS revcut_rl);
   146 
   147 (*Attack subgoal i by resolution, using flags to indicate elimination rules*)
   148 fun biresolve_tac brules i = PRIMSEQ (biresolution false brules i);
   149 
   150 (*Resolution: the simple case, works for introduction rules*)
   151 fun resolve_tac rules = biresolve_tac (map (pair false) rules);
   152 
   153 (*Resolution with elimination rules only*)
   154 fun eresolve_tac rules = biresolve_tac (map (pair true) rules);
   155 
   156 (*Forward reasoning using destruction rules.*)
   157 fun forward_tac rls = resolve_tac (map make_elim rls) THEN' assume_tac;
   158 
   159 (*Like forward_tac, but deletes the assumption after use.*)
   160 fun dresolve_tac rls = eresolve_tac (map make_elim rls);
   161 
   162 (*Shorthand versions: for resolution with a single theorem*)
   163 val atac    =   assume_tac;
   164 fun rtac rl =  resolve_tac [rl];
   165 fun dtac rl = dresolve_tac [rl];
   166 fun etac rl = eresolve_tac [rl];
   167 fun ftac rl =  forward_tac [rl];
   168 fun datac thm j = EVERY' (dtac thm::replicate j atac);
   169 fun eatac thm j = EVERY' (etac thm::replicate j atac);
   170 fun fatac thm j = EVERY' (ftac thm::replicate j atac);
   171 
   172 (*Use an assumption or some rules ... A popular combination!*)
   173 fun ares_tac rules = assume_tac  ORELSE'  resolve_tac rules;
   174 
   175 fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac;
   176 
   177 (*Matching tactics -- as above, but forbid updating of state*)
   178 fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i);
   179 fun match_tac rules  = bimatch_tac (map (pair false) rules);
   180 fun ematch_tac rules = bimatch_tac (map (pair true) rules);
   181 fun dmatch_tac rls   = ematch_tac (map make_elim rls);
   182 
   183 (*Smash all flex-flex disagreement pairs in the proof state.*)
   184 val flexflex_tac = PRIMSEQ flexflex_rule;
   185 
   186 (*Remove duplicate subgoals.*)
   187 val perm_tac = PRIMITIVE oo Thm.permute_prems;
   188 
   189 fun distinct_tac (i, k) =
   190   perm_tac 0 (i - 1) THEN
   191   perm_tac 1 (k - 1) THEN
   192   DETERM (PRIMSEQ (fn st =>
   193     Thm.compose_no_flatten false (st, 0) 1
   194       (Drule.incr_indexes st Drule.distinct_prems_rl))) THEN
   195   perm_tac 1 (1 - k) THEN
   196   perm_tac 0 (1 - i);
   197 
   198 fun distinct_subgoal_tac i st =
   199   (case Library.drop (i - 1, Thm.prems_of st) of
   200     [] => no_tac st
   201   | A :: Bs =>
   202       st |> EVERY (fold (fn (B, k) =>
   203         if A aconv B then cons (distinct_tac (i, k)) else I) (Bs ~~ (1 upto length Bs)) []));
   204 
   205 fun distinct_subgoals_tac state =
   206   let
   207     val goals = Thm.prems_of state;
   208     val dups = distinct (eq_fst (op aconv)) (goals ~~ (1 upto length goals));
   209   in EVERY (rev (map (distinct_subgoal_tac o snd) dups)) state end;
   210 
   211 (*Determine print names of goal parameters (reversed)*)
   212 fun innermost_params i st =
   213   let val (_, _, Bi, _) = dest_state (st, i)
   214   in rename_wrt_term Bi (Logic.strip_params Bi) end;
   215 
   216 (*params of subgoal i as they are printed*)
   217 fun params_of_state i st = rev (innermost_params i st);
   218 
   219 (*read instantiations with respect to subgoal i of proof state st*)
   220 fun read_insts_in_state (st, i, sinsts, rule) =
   221   let val thy = Thm.theory_of_thm st
   222       and params = params_of_state i st
   223       and rts = types_sorts rule and (types,sorts) = types_sorts st
   224       fun types'(a, ~1) = (case AList.lookup (op =) params a of NONE => types (a, ~1) | sm => sm)
   225         | types' ixn = types ixn;
   226       val used = Drule.add_used rule (Drule.add_used st []);
   227   in read_insts thy rts (types',sorts) used sinsts end;
   228 
   229 (*Lift and instantiate a rule wrt the given state and subgoal number *)
   230 fun lift_inst_rule' (st, i, sinsts, rule) =
   231 let val (Tinsts,insts) = read_insts_in_state (st, i, sinsts, rule)
   232     and {maxidx,...} = rep_thm st
   233     and params = params_of_state i st
   234     val paramTs = map #2 params
   235     and inc = maxidx+1
   236     fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
   237       | liftvar t = raise TERM("Variable expected", [t]);
   238     fun liftterm t = list_abs_free (params,
   239                                     Logic.incr_indexes(paramTs,inc) t)
   240     (*Lifts instantiation pair over params*)
   241     fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
   242     val lifttvar = pairself (ctyp_fun (Logic.incr_tvar inc))
   243 in Drule.instantiate (map lifttvar Tinsts, map liftpair insts)
   244                      (Thm.lift_rule (Thm.cprem_of st i) rule)
   245 end;
   246 
   247 fun lift_inst_rule (st, i, sinsts, rule) = lift_inst_rule'
   248   (st, i, map (apfst Syntax.read_indexname) sinsts, rule);
   249 
   250 (*
   251 Like lift_inst_rule but takes terms, not strings, where the terms may contain
   252 Bounds referring to parameters of the subgoal.
   253 
   254 insts: [...,(vj,tj),...]
   255 
   256 The tj may contain references to parameters of subgoal i of the state st
   257 in the form of Bound k, i.e. the tj may be subterms of the subgoal.
   258 To saturate the lose bound vars, the tj are enclosed in abstractions
   259 corresponding to the parameters of subgoal i, thus turning them into
   260 functions. At the same time, the types of the vj are lifted.
   261 
   262 NB: the types in insts must be correctly instantiated already,
   263     i.e. Tinsts is not applied to insts.
   264 *)
   265 fun term_lift_inst_rule (st, i, Tinsts, insts, rule) =
   266 let val {maxidx,thy,...} = rep_thm st
   267     val paramTs = map #2 (params_of_state i st)
   268     and inc = maxidx+1
   269     fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
   270     (*lift only Var, not term, which must be lifted already*)
   271     fun liftpair (v,t) = (cterm_of thy (liftvar v), cterm_of thy t)
   272     fun liftTpair (((a, i), S), T) =
   273       (ctyp_of thy (TVar ((a, i + inc), S)),
   274        ctyp_of thy (Logic.incr_tvar inc T))
   275 in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
   276                      (Thm.lift_rule (Thm.cprem_of st i) rule)
   277 end;
   278 
   279 (*** Resolve after lifting and instantation; may refer to parameters of the
   280      subgoal.  Fails if "i" is out of range.  ***)
   281 
   282 (*compose version: arguments are as for bicompose.*)
   283 fun gen_compose_inst_tac instf sinsts (bires_flg, rule, nsubgoal) i st =
   284   if i > nprems_of st then no_tac st
   285   else st |>
   286     (compose_tac (bires_flg, instf (st, i, sinsts, rule), nsubgoal) i
   287      handle TERM (msg,_)   => (warning msg;  no_tac)
   288           | THM  (msg,_,_) => (warning msg;  no_tac));
   289 
   290 val compose_inst_tac = gen_compose_inst_tac lift_inst_rule;
   291 val compose_inst_tac' = gen_compose_inst_tac lift_inst_rule';
   292 
   293 (*"Resolve" version.  Note: res_inst_tac cannot behave sensibly if the
   294   terms that are substituted contain (term or type) unknowns from the
   295   goal, because it is unable to instantiate goal unknowns at the same time.
   296 
   297   The type checker is instructed not to freeze flexible type vars that
   298   were introduced during type inference and still remain in the term at the
   299   end.  This increases flexibility but can introduce schematic type vars in
   300   goals.
   301 *)
   302 fun res_inst_tac sinsts rule i =
   303     compose_inst_tac sinsts (false, rule, nprems_of rule) i;
   304 
   305 fun res_inst_tac' sinsts rule i =
   306     compose_inst_tac' sinsts (false, rule, nprems_of rule) i;
   307 
   308 (*eresolve elimination version*)
   309 fun eres_inst_tac sinsts rule i =
   310     compose_inst_tac sinsts (true, rule, nprems_of rule) i;
   311 
   312 fun eres_inst_tac' sinsts rule i =
   313     compose_inst_tac' sinsts (true, rule, nprems_of rule) i;
   314 
   315 (*For forw_inst_tac and dres_inst_tac.  Preserve Var indexes of rl;
   316   increment revcut_rl instead.*)
   317 fun make_elim_preserve rl =
   318   let val {maxidx,...} = rep_thm rl
   319       fun cvar ixn = cterm_of ProtoPure.thy (Var(ixn,propT));
   320       val revcut_rl' =
   321           instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
   322                              (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
   323       val arg = (false, rl, nprems_of rl)
   324       val [th] = Seq.list_of (bicompose false arg 1 revcut_rl')
   325   in  th  end
   326   handle Bind => raise THM("make_elim_preserve", 1, [rl]);
   327 
   328 (*instantiate and cut -- for a FACT, anyway...*)
   329 fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule);
   330 
   331 (*forward tactic applies a RULE to an assumption without deleting it*)
   332 fun forw_inst_tac sinsts rule = cut_inst_tac sinsts rule THEN' assume_tac;
   333 
   334 (*dresolve tactic applies a RULE to replace an assumption*)
   335 fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule);
   336 
   337 (*instantiate variables in the whole state*)
   338 val instantiate_tac = PRIMITIVE o read_instantiate;
   339 
   340 val instantiate_tac' = PRIMITIVE o Drule.read_instantiate';
   341 
   342 (*Deletion of an assumption*)
   343 fun thin_tac s = eres_inst_tac [("V",s)] thin_rl;
   344 
   345 (*** Applications of cut_rl ***)
   346 
   347 (*Used by metacut_tac*)
   348 fun bires_cut_tac arg i =
   349     resolve_tac [cut_rl] i  THEN  biresolve_tac arg (i+1) ;
   350 
   351 (*The conclusion of the rule gets assumed in subgoal i,
   352   while subgoal i+1,... are the premises of the rule.*)
   353 fun metacut_tac rule = bires_cut_tac [(false,rule)];
   354 
   355 (*"Cut" a list of rules into the goal.  Their premises will become new
   356   subgoals.*)
   357 fun cut_rules_tac ths i = EVERY (map (fn th => metacut_tac th i) ths);
   358 
   359 (*As above, but inserts only facts (unconditional theorems);
   360   generates no additional subgoals. *)
   361 fun cut_facts_tac ths = cut_rules_tac (filter Thm.no_prems ths);
   362 
   363 (*Introduce the given proposition as a lemma and subgoal*)
   364 fun subgoal_tac sprop =
   365   DETERM o res_inst_tac [("psi", sprop)] cut_rl THEN' SUBGOAL (fn (prop, _) =>
   366     let val concl' = Logic.strip_assums_concl prop in
   367       if null (term_tvars concl') then ()
   368       else warning"Type variables in new subgoal: add a type constraint?";
   369       all_tac
   370   end);
   371 
   372 (*Introduce a list of lemmas and subgoals*)
   373 fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops);
   374 
   375 
   376 (**** Indexing and filtering of theorems ****)
   377 
   378 (*Returns the list of potentially resolvable theorems for the goal "prem",
   379         using the predicate  could(subgoal,concl).
   380   Resulting list is no longer than "limit"*)
   381 fun filter_thms could (limit, prem, ths) =
   382   let val pb = Logic.strip_assums_concl prem;   (*delete assumptions*)
   383       fun filtr (limit, []) = []
   384         | filtr (limit, th::ths) =
   385             if limit=0 then  []
   386             else if could(pb, concl_of th)  then th :: filtr(limit-1, ths)
   387             else filtr(limit,ths)
   388   in  filtr(limit,ths)  end;
   389 
   390 
   391 (*** biresolution and resolution using nets ***)
   392 
   393 (** To preserve the order of the rules, tag them with increasing integers **)
   394 
   395 (*insert tags*)
   396 fun taglist k [] = []
   397   | taglist k (x::xs) = (k,x) :: taglist (k+1) xs;
   398 
   399 (*remove tags and suppress duplicates -- list is assumed sorted!*)
   400 fun untaglist [] = []
   401   | untaglist [(k:int,x)] = [x]
   402   | untaglist ((k,x) :: (rest as (k',x')::_)) =
   403       if k=k' then untaglist rest
   404       else    x :: untaglist rest;
   405 
   406 (*return list elements in original order*)
   407 fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls);
   408 
   409 (*insert one tagged brl into the pair of nets*)
   410 fun insert_tagged_brl (kbrl as (k, (eres, th))) (inet, enet) =
   411   if eres then
   412     (case try Thm.major_prem_of th of
   413       SOME prem => (inet, Net.insert_term (K false) (prem, kbrl) enet)
   414     | NONE => error "insert_tagged_brl: elimination rule with no premises")
   415   else (Net.insert_term (K false) (concl_of th, kbrl) inet, enet);
   416 
   417 (*build a pair of nets for biresolution*)
   418 fun build_netpair netpair brls =
   419     fold_rev insert_tagged_brl (taglist 1 brls) netpair;
   420 
   421 (*delete one kbrl from the pair of nets*)
   422 fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
   423 
   424 fun delete_tagged_brl (brl as (eres, th)) (inet, enet) =
   425   (if eres then
   426     (case try Thm.major_prem_of th of
   427       SOME prem => (inet, Net.delete_term eq_kbrl (prem, ((), brl)) enet)
   428     | NONE => (inet, enet))  (*no major premise: ignore*)
   429   else (Net.delete_term eq_kbrl (Thm.concl_of th, ((), brl)) inet, enet))
   430   handle Net.DELETE => (inet,enet);
   431 
   432 
   433 (*biresolution using a pair of nets rather than rules.
   434     function "order" must sort and possibly filter the list of brls.
   435     boolean "match" indicates matching or unification.*)
   436 fun biresolution_from_nets_tac order match (inet,enet) =
   437   SUBGOAL
   438     (fn (prem,i) =>
   439       let val hyps = Logic.strip_assums_hyp prem
   440           and concl = Logic.strip_assums_concl prem
   441           val kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps
   442       in PRIMSEQ (biresolution match (order kbrls) i) end);
   443 
   444 (*versions taking pre-built nets.  No filtering of brls*)
   445 val biresolve_from_nets_tac = biresolution_from_nets_tac orderlist false;
   446 val bimatch_from_nets_tac   = biresolution_from_nets_tac orderlist true;
   447 
   448 (*fast versions using nets internally*)
   449 val net_biresolve_tac =
   450     biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty);
   451 
   452 val net_bimatch_tac =
   453     bimatch_from_nets_tac o build_netpair(Net.empty,Net.empty);
   454 
   455 (*** Simpler version for resolve_tac -- only one net, and no hyps ***)
   456 
   457 (*insert one tagged rl into the net*)
   458 fun insert_krl (krl as (k,th)) =
   459   Net.insert_term (K false) (concl_of th, krl);
   460 
   461 (*build a net of rules for resolution*)
   462 fun build_net rls =
   463   fold_rev insert_krl (taglist 1 rls) Net.empty;
   464 
   465 (*resolution using a net rather than rules; pred supports filt_resolve_tac*)
   466 fun filt_resolution_from_net_tac match pred net =
   467   SUBGOAL
   468     (fn (prem,i) =>
   469       let val krls = Net.unify_term net (Logic.strip_assums_concl prem)
   470       in
   471          if pred krls
   472          then PRIMSEQ
   473                 (biresolution match (map (pair false) (orderlist krls)) i)
   474          else no_tac
   475       end);
   476 
   477 (*Resolve the subgoal using the rules (making a net) unless too flexible,
   478    which means more than maxr rules are unifiable.      *)
   479 fun filt_resolve_tac rules maxr =
   480     let fun pred krls = length krls <= maxr
   481     in  filt_resolution_from_net_tac false pred (build_net rules)  end;
   482 
   483 (*versions taking pre-built nets*)
   484 val resolve_from_net_tac = filt_resolution_from_net_tac false (K true);
   485 val match_from_net_tac = filt_resolution_from_net_tac true (K true);
   486 
   487 (*fast versions using nets internally*)
   488 val net_resolve_tac = resolve_from_net_tac o build_net;
   489 val net_match_tac = match_from_net_tac o build_net;
   490 
   491 
   492 (*** For Natural Deduction using (bires_flg, rule) pairs ***)
   493 
   494 (*The number of new subgoals produced by the brule*)
   495 fun subgoals_of_brl (true,rule)  = nprems_of rule - 1
   496   | subgoals_of_brl (false,rule) = nprems_of rule;
   497 
   498 (*Less-than test: for sorting to minimize number of new subgoals*)
   499 fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2;
   500 
   501 
   502 (*** Renaming of parameters in a subgoal
   503      Names may contain letters, digits or primes and must be
   504      separated by blanks ***)
   505 
   506 fun rename_params_tac xs i =
   507   case Library.find_first (not o Syntax.is_identifier) xs of
   508       SOME x => error ("Not an identifier: " ^ x)
   509     | NONE =>
   510        (if !Logic.auto_rename
   511          then (warning "Resetting Logic.auto_rename";
   512              Logic.auto_rename := false)
   513         else (); PRIMITIVE (rename_params_rule (xs, i)));
   514 
   515 (*scan a list of characters into "words" composed of "letters" (recognized by
   516   is_let) and separated by any number of non-"letters"*)
   517 fun scanwords is_let cs =
   518   let fun scan1 [] = []
   519         | scan1 cs =
   520             let val (lets, rest) = take_prefix is_let cs
   521             in implode lets :: scanwords is_let rest end;
   522   in scan1 (#2 (take_prefix (not o is_let) cs)) end;
   523 
   524 fun rename_tac str i =
   525   let val cs = Symbol.explode str in
   526   case #2 (take_prefix (Symbol.is_letdig orf Symbol.is_blank) cs) of
   527       [] => rename_params_tac (scanwords Symbol.is_letdig cs) i
   528     | c::_ => error ("Illegal character: " ^ c)
   529   end;
   530 
   531 (*Rename recent parameters using names generated from a and the suffixes,
   532   provided the string a, which represents a term, is an identifier. *)
   533 fun rename_last_tac a sufs i =
   534   let val names = map (curry op^ a) sufs
   535   in  if Syntax.is_identifier a
   536       then PRIMITIVE (rename_params_rule (names,i))
   537       else all_tac
   538   end;
   539 
   540 (*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
   541   right to left if n is positive, and from left to right if n is negative.*)
   542 fun rotate_tac 0 i = all_tac
   543   | rotate_tac k i = PRIMITIVE (rotate_rule k i);
   544 
   545 (*Rotates the given subgoal to be the last.*)
   546 fun defer_tac i = PRIMITIVE (permute_prems (i-1) 1);
   547 
   548 (* remove premises that do not satisfy p; fails if all prems satisfy p *)
   549 fun filter_prems_tac p =
   550   let fun Then NONE tac = SOME tac
   551         | Then (SOME tac) tac' = SOME(tac THEN' tac');
   552       fun thins H (tac,n) =
   553         if p H then (tac,n+1)
   554         else (Then tac (rotate_tac n THEN' etac thin_rl),0);
   555   in SUBGOAL(fn (subg,n) =>
   556        let val Hs = Logic.strip_assums_hyp subg
   557        in case fst(fold thins Hs (NONE,0)) of
   558             NONE => no_tac | SOME tac => tac n
   559        end)
   560   end;
   561 
   562 end;
   563 
   564 structure BasicTactic: BASIC_TACTIC = Tactic;
   565 open BasicTactic;