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