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