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