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