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