src/Pure/tactic.ML
author wenzelm
Sat Apr 12 17:00:35 2008 +0200 (2008-04-12)
changeset 26626 c6231d64d264
parent 26424 a6cad32a27b0
child 27158 113a32dd0b14
permissions -rw-r--r--
rep_cterm/rep_thm: no longer dereference theory_ref;
     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 Lexicon.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
   267     val thy = Thm.theory_of_thm st
   268     val cert = Thm.cterm_of thy
   269     val certT = Thm.ctyp_of thy
   270     val maxidx = Thm.maxidx_of st
   271     val paramTs = map #2 (params_of_state i st)
   272     val inc = maxidx+1
   273     fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
   274     (*lift only Var, not term, which must be lifted already*)
   275     fun liftpair (v,t) = (cert (liftvar v), cert t)
   276     fun liftTpair (((a, i), S), T) =
   277       (certT (TVar ((a, i + inc), S)),
   278        certT (Logic.incr_tvar inc T))
   279 in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
   280                      (Thm.lift_rule (Thm.cprem_of st i) rule)
   281 end;
   282 
   283 (*** Resolve after lifting and instantation; may refer to parameters of the
   284      subgoal.  Fails if "i" is out of range.  ***)
   285 
   286 (*compose version: arguments are as for bicompose.*)
   287 fun gen_compose_inst_tac instf sinsts (bires_flg, rule, nsubgoal) i st =
   288   if i > nprems_of st then no_tac st
   289   else st |>
   290     (compose_tac (bires_flg, instf (st, i, sinsts, rule), nsubgoal) i
   291      handle TERM (msg,_)   => (warning msg;  no_tac)
   292           | THM  (msg,_,_) => (warning msg;  no_tac));
   293 
   294 val compose_inst_tac = gen_compose_inst_tac lift_inst_rule;
   295 val compose_inst_tac' = gen_compose_inst_tac lift_inst_rule';
   296 
   297 (*"Resolve" version.  Note: res_inst_tac cannot behave sensibly if the
   298   terms that are substituted contain (term or type) unknowns from the
   299   goal, because it is unable to instantiate goal unknowns at the same time.
   300 
   301   The type checker is instructed not to freeze flexible type vars that
   302   were introduced during type inference and still remain in the term at the
   303   end.  This increases flexibility but can introduce schematic type vars in
   304   goals.
   305 *)
   306 fun res_inst_tac sinsts rule i =
   307     compose_inst_tac sinsts (false, rule, nprems_of rule) i;
   308 
   309 fun res_inst_tac' sinsts rule i =
   310     compose_inst_tac' sinsts (false, rule, nprems_of rule) i;
   311 
   312 (*eresolve elimination version*)
   313 fun eres_inst_tac sinsts rule i =
   314     compose_inst_tac sinsts (true, rule, nprems_of rule) i;
   315 
   316 fun eres_inst_tac' sinsts rule i =
   317     compose_inst_tac' sinsts (true, rule, nprems_of rule) i;
   318 
   319 (*For forw_inst_tac and dres_inst_tac.  Preserve Var indexes of rl;
   320   increment revcut_rl instead.*)
   321 fun make_elim_preserve rl =
   322   let val maxidx = Thm.maxidx_of rl
   323       val thy = Thm.theory_of_thm rl
   324       fun cvar ixn = cterm_of thy (Var(ixn,propT));
   325       val revcut_rl' =
   326           instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
   327                              (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
   328       val arg = (false, rl, nprems_of rl)
   329       val [th] = Seq.list_of (bicompose false arg 1 revcut_rl')
   330   in  th  end
   331   handle Bind => raise THM("make_elim_preserve", 1, [rl]);
   332 
   333 (*instantiate and cut -- for a FACT, anyway...*)
   334 fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule);
   335 
   336 (*forward tactic applies a RULE to an assumption without deleting it*)
   337 fun forw_inst_tac sinsts rule = cut_inst_tac sinsts rule THEN' assume_tac;
   338 
   339 (*dresolve tactic applies a RULE to replace an assumption*)
   340 fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule);
   341 
   342 (*instantiate variables in the whole state*)
   343 val instantiate_tac = PRIMITIVE o read_instantiate;
   344 
   345 val instantiate_tac' = PRIMITIVE o Drule.read_instantiate';
   346 
   347 (*Deletion of an assumption*)
   348 fun thin_tac s = eres_inst_tac [("V",s)] thin_rl;
   349 
   350 (*** Applications of cut_rl ***)
   351 
   352 (*Used by metacut_tac*)
   353 fun bires_cut_tac arg i =
   354     resolve_tac [cut_rl] i  THEN  biresolve_tac arg (i+1) ;
   355 
   356 (*The conclusion of the rule gets assumed in subgoal i,
   357   while subgoal i+1,... are the premises of the rule.*)
   358 fun metacut_tac rule = bires_cut_tac [(false,rule)];
   359 
   360 (*"Cut" a list of rules into the goal.  Their premises will become new
   361   subgoals.*)
   362 fun cut_rules_tac ths i = EVERY (map (fn th => metacut_tac th i) ths);
   363 
   364 (*As above, but inserts only facts (unconditional theorems);
   365   generates no additional subgoals. *)
   366 fun cut_facts_tac ths = cut_rules_tac (filter Thm.no_prems ths);
   367 
   368 (*Introduce the given proposition as a lemma and subgoal*)
   369 fun subgoal_tac sprop =
   370   DETERM o res_inst_tac [("psi", sprop)] cut_rl THEN' SUBGOAL (fn (prop, _) =>
   371     let val concl' = Logic.strip_assums_concl prop in
   372       if null (term_tvars concl') then ()
   373       else warning"Type variables in new subgoal: add a type constraint?";
   374       all_tac
   375   end);
   376 
   377 (*Introduce a list of lemmas and subgoals*)
   378 fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops);
   379 
   380 
   381 (**** Indexing and filtering of theorems ****)
   382 
   383 (*Returns the list of potentially resolvable theorems for the goal "prem",
   384         using the predicate  could(subgoal,concl).
   385   Resulting list is no longer than "limit"*)
   386 fun filter_thms could (limit, prem, ths) =
   387   let val pb = Logic.strip_assums_concl prem;   (*delete assumptions*)
   388       fun filtr (limit, []) = []
   389         | filtr (limit, th::ths) =
   390             if limit=0 then  []
   391             else if could(pb, concl_of th)  then th :: filtr(limit-1, ths)
   392             else filtr(limit,ths)
   393   in  filtr(limit,ths)  end;
   394 
   395 
   396 (*** biresolution and resolution using nets ***)
   397 
   398 (** To preserve the order of the rules, tag them with increasing integers **)
   399 
   400 (*insert tags*)
   401 fun taglist k [] = []
   402   | taglist k (x::xs) = (k,x) :: taglist (k+1) xs;
   403 
   404 (*remove tags and suppress duplicates -- list is assumed sorted!*)
   405 fun untaglist [] = []
   406   | untaglist [(k:int,x)] = [x]
   407   | untaglist ((k,x) :: (rest as (k',x')::_)) =
   408       if k=k' then untaglist rest
   409       else    x :: untaglist rest;
   410 
   411 (*return list elements in original order*)
   412 fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls);
   413 
   414 (*insert one tagged brl into the pair of nets*)
   415 fun insert_tagged_brl (kbrl as (k, (eres, th))) (inet, enet) =
   416   if eres then
   417     (case try Thm.major_prem_of th of
   418       SOME prem => (inet, Net.insert_term (K false) (prem, kbrl) enet)
   419     | NONE => error "insert_tagged_brl: elimination rule with no premises")
   420   else (Net.insert_term (K false) (concl_of th, kbrl) inet, enet);
   421 
   422 (*build a pair of nets for biresolution*)
   423 fun build_netpair netpair brls =
   424     fold_rev insert_tagged_brl (taglist 1 brls) netpair;
   425 
   426 (*delete one kbrl from the pair of nets*)
   427 fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
   428 
   429 fun delete_tagged_brl (brl as (eres, th)) (inet, enet) =
   430   (if eres then
   431     (case try Thm.major_prem_of th of
   432       SOME prem => (inet, Net.delete_term eq_kbrl (prem, ((), brl)) enet)
   433     | NONE => (inet, enet))  (*no major premise: ignore*)
   434   else (Net.delete_term eq_kbrl (Thm.concl_of th, ((), brl)) inet, enet))
   435   handle Net.DELETE => (inet,enet);
   436 
   437 
   438 (*biresolution using a pair of nets rather than rules.
   439     function "order" must sort and possibly filter the list of brls.
   440     boolean "match" indicates matching or unification.*)
   441 fun biresolution_from_nets_tac order match (inet,enet) =
   442   SUBGOAL
   443     (fn (prem,i) =>
   444       let val hyps = Logic.strip_assums_hyp prem
   445           and concl = Logic.strip_assums_concl prem
   446           val kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps
   447       in PRIMSEQ (biresolution match (order kbrls) i) end);
   448 
   449 (*versions taking pre-built nets.  No filtering of brls*)
   450 val biresolve_from_nets_tac = biresolution_from_nets_tac orderlist false;
   451 val bimatch_from_nets_tac   = biresolution_from_nets_tac orderlist true;
   452 
   453 (*fast versions using nets internally*)
   454 val net_biresolve_tac =
   455     biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty);
   456 
   457 val net_bimatch_tac =
   458     bimatch_from_nets_tac o build_netpair(Net.empty,Net.empty);
   459 
   460 (*** Simpler version for resolve_tac -- only one net, and no hyps ***)
   461 
   462 (*insert one tagged rl into the net*)
   463 fun insert_krl (krl as (k,th)) =
   464   Net.insert_term (K false) (concl_of th, krl);
   465 
   466 (*build a net of rules for resolution*)
   467 fun build_net rls =
   468   fold_rev insert_krl (taglist 1 rls) Net.empty;
   469 
   470 (*resolution using a net rather than rules; pred supports filt_resolve_tac*)
   471 fun filt_resolution_from_net_tac match pred net =
   472   SUBGOAL
   473     (fn (prem,i) =>
   474       let val krls = Net.unify_term net (Logic.strip_assums_concl prem)
   475       in
   476          if pred krls
   477          then PRIMSEQ
   478                 (biresolution match (map (pair false) (orderlist krls)) i)
   479          else no_tac
   480       end);
   481 
   482 (*Resolve the subgoal using the rules (making a net) unless too flexible,
   483    which means more than maxr rules are unifiable.      *)
   484 fun filt_resolve_tac rules maxr =
   485     let fun pred krls = length krls <= maxr
   486     in  filt_resolution_from_net_tac false pred (build_net rules)  end;
   487 
   488 (*versions taking pre-built nets*)
   489 val resolve_from_net_tac = filt_resolution_from_net_tac false (K true);
   490 val match_from_net_tac = filt_resolution_from_net_tac true (K true);
   491 
   492 (*fast versions using nets internally*)
   493 val net_resolve_tac = resolve_from_net_tac o build_net;
   494 val net_match_tac = match_from_net_tac o build_net;
   495 
   496 
   497 (*** For Natural Deduction using (bires_flg, rule) pairs ***)
   498 
   499 (*The number of new subgoals produced by the brule*)
   500 fun subgoals_of_brl (true,rule)  = nprems_of rule - 1
   501   | subgoals_of_brl (false,rule) = nprems_of rule;
   502 
   503 (*Less-than test: for sorting to minimize number of new subgoals*)
   504 fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2;
   505 
   506 
   507 (*** Renaming of parameters in a subgoal
   508      Names may contain letters, digits or primes and must be
   509      separated by blanks ***)
   510 
   511 fun rename_params_tac xs i =
   512   case Library.find_first (not o Syntax.is_identifier) xs of
   513       SOME x => error ("Not an identifier: " ^ x)
   514     | NONE => 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 end;
   564 
   565 structure BasicTactic: BASIC_TACTIC = Tactic;
   566 open BasicTactic;