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