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