src/Pure/tactic.ML
author wenzelm
Thu Nov 10 20:57:11 2005 +0100 (2005-11-10)
changeset 18145 6757627acf59
parent 18034 5351a1538ea5
child 18209 6bcd9b2ca49b
permissions -rw-r--r--
renamed Thm.cgoal_of to Thm.cprem_of;
     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 end;
   102 
   103 signature TACTIC =
   104 sig
   105   include BASIC_TACTIC
   106   val innermost_params: int -> thm -> (string * typ) list
   107   val untaglist: (int * 'a) list -> 'a list
   108   val eq_kbrl: ('a * (bool * thm)) * ('a * (bool * thm)) -> bool
   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 smart_conjunction_tac: int -> tactic
   114   val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) ->
   115                           int -> tactic
   116   val lift_inst_rule'   : thm * int * (indexname * string) list * thm -> thm
   117   val eres_inst_tac'    : (indexname * string) list -> thm -> int -> tactic
   118   val res_inst_tac'     : (indexname * string) list -> thm -> int -> tactic
   119   val instantiate_tac'  : (indexname * string) list -> tactic
   120 end;
   121 
   122 structure Tactic: TACTIC =
   123 struct
   124 
   125 (*Discover which goal is chosen:  SOMEGOAL(trace_goalno_tac tac) *)
   126 fun trace_goalno_tac tac i st =
   127     case Seq.pull(tac i st) of
   128         NONE    => Seq.empty
   129       | seqcell => (tracing ("Subgoal " ^ string_of_int i ^ " selected");
   130                          Seq.make(fn()=> seqcell));
   131 
   132 (*Makes a rule by applying a tactic to an existing rule*)
   133 fun rule_by_tactic tac rl =
   134   let val (st, thaw) = freeze_thaw (zero_var_indexes rl)
   135   in case Seq.pull (tac st)  of
   136         NONE        => raise THM("rule_by_tactic", 0, [rl])
   137       | SOME(st',_) => Thm.varifyT (thaw st')
   138   end;
   139 
   140 (*** Basic tactics ***)
   141 
   142 (*** The following fail if the goal number is out of range:
   143      thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
   144 
   145 (*Solve subgoal i by assumption*)
   146 fun assume_tac i = PRIMSEQ (assumption i);
   147 
   148 (*Solve subgoal i by assumption, using no unification*)
   149 fun eq_assume_tac i = PRIMITIVE (eq_assumption i);
   150 
   151 (** Resolution/matching tactics **)
   152 
   153 (*The composition rule/state: no lifting or var renaming.
   154   The arg = (bires_flg, orule, m) ;  see bicompose for explanation.*)
   155 fun compose_tac arg i = PRIMSEQ (bicompose false arg i);
   156 
   157 (*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
   158   like [| P&Q; P==>R |] ==> R *)
   159 fun make_elim rl = zero_var_indexes (rl RS revcut_rl);
   160 
   161 (*Attack subgoal i by resolution, using flags to indicate elimination rules*)
   162 fun biresolve_tac brules i = PRIMSEQ (biresolution false brules i);
   163 
   164 (*Resolution: the simple case, works for introduction rules*)
   165 fun resolve_tac rules = biresolve_tac (map (pair false) rules);
   166 
   167 (*Resolution with elimination rules only*)
   168 fun eresolve_tac rules = biresolve_tac (map (pair true) rules);
   169 
   170 (*Forward reasoning using destruction rules.*)
   171 fun forward_tac rls = resolve_tac (map make_elim rls) THEN' assume_tac;
   172 
   173 (*Like forward_tac, but deletes the assumption after use.*)
   174 fun dresolve_tac rls = eresolve_tac (map make_elim rls);
   175 
   176 (*Shorthand versions: for resolution with a single theorem*)
   177 val atac    =   assume_tac;
   178 fun rtac rl =  resolve_tac [rl];
   179 fun dtac rl = dresolve_tac [rl];
   180 fun etac rl = eresolve_tac [rl];
   181 fun ftac rl =  forward_tac [rl];
   182 fun datac thm j = EVERY' (dtac thm::replicate j atac);
   183 fun eatac thm j = EVERY' (etac thm::replicate j atac);
   184 fun fatac thm j = EVERY' (ftac thm::replicate j atac);
   185 
   186 (*Use an assumption or some rules ... A popular combination!*)
   187 fun ares_tac rules = assume_tac  ORELSE'  resolve_tac rules;
   188 
   189 fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac;
   190 
   191 (*Matching tactics -- as above, but forbid updating of state*)
   192 fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i);
   193 fun match_tac rules  = bimatch_tac (map (pair false) rules);
   194 fun ematch_tac rules = bimatch_tac (map (pair true) rules);
   195 fun dmatch_tac rls   = ematch_tac (map make_elim rls);
   196 
   197 (*Smash all flex-flex disagreement pairs in the proof state.*)
   198 val flexflex_tac = PRIMSEQ flexflex_rule;
   199 
   200 
   201 (*Remove duplicate subgoals.  By Mark Staples*)
   202 local
   203 fun cterm_aconv (a,b) = term_of a aconv term_of b;
   204 in
   205 fun distinct_subgoals_tac state =
   206     let val (frozth,thawfn) = freeze_thaw state
   207         val froz_prems = cprems_of frozth
   208         val assumed = implies_elim_list frozth (map assume froz_prems)
   209         val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems)
   210                                         assumed;
   211     in  (*Applying Thm.varifyT to the result of thawfn would (re-)generalize
   212           all type variables that appear in the subgoals. Unfortunately, it
   213           would also break the function AxClass.intro_classes_tac, even in the
   214           trivial case where the type class has no axioms.*)
   215         Seq.single (thawfn implied)
   216     end
   217 end;
   218 
   219 
   220 (*Determine print names of goal parameters (reversed)*)
   221 fun innermost_params i st =
   222   let val (_, _, Bi, _) = dest_state (st, i)
   223   in rename_wrt_term Bi (Logic.strip_params Bi) end;
   224 
   225 (*params of subgoal i as they are printed*)
   226 fun params_of_state st i =
   227   let val (_, _, Bi, _) = dest_state(st,i)
   228       val params = Logic.strip_params Bi
   229   in rev(rename_wrt_term Bi params) end;
   230 
   231 (*read instantiations with respect to subgoal i of proof state st*)
   232 fun read_insts_in_state (st, i, sinsts, rule) =
   233   let val thy = Thm.theory_of_thm st
   234       and params = params_of_state st i
   235       and rts = types_sorts rule and (types,sorts) = types_sorts st
   236       fun types'(a, ~1) = (case AList.lookup (op =) params a of NONE => types (a, ~1) | sm => sm)
   237         | types' ixn = types ixn;
   238       val used = Drule.add_used rule (Drule.add_used st []);
   239   in read_insts thy rts (types',sorts) used sinsts end;
   240 
   241 (*Lift and instantiate a rule wrt the given state and subgoal number *)
   242 fun lift_inst_rule' (st, i, sinsts, rule) =
   243 let val (Tinsts,insts) = read_insts_in_state (st, i, sinsts, rule)
   244     and {maxidx,...} = rep_thm st
   245     and params = params_of_state st i
   246     val paramTs = map #2 params
   247     and inc = maxidx+1
   248     fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
   249       | liftvar t = raise TERM("Variable expected", [t]);
   250     fun liftterm t = list_abs_free (params,
   251                                     Logic.incr_indexes(paramTs,inc) t)
   252     (*Lifts instantiation pair over params*)
   253     fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
   254     val lifttvar = pairself (ctyp_fun (Logic.incr_tvar inc))
   255 in Drule.instantiate (map lifttvar Tinsts, map liftpair insts)
   256                      (Thm.lift_rule (Thm.cprem_of st i) rule)
   257 end;
   258 
   259 fun lift_inst_rule (st, i, sinsts, rule) = lift_inst_rule'
   260   (st, i, map (apfst Syntax.indexname) sinsts, rule);
   261 
   262 (*
   263 Like lift_inst_rule but takes terms, not strings, where the terms may contain
   264 Bounds referring to parameters of the subgoal.
   265 
   266 insts: [...,(vj,tj),...]
   267 
   268 The tj may contain references to parameters of subgoal i of the state st
   269 in the form of Bound k, i.e. the tj may be subterms of the subgoal.
   270 To saturate the lose bound vars, the tj are enclosed in abstractions
   271 corresponding to the parameters of subgoal i, thus turning them into
   272 functions. At the same time, the types of the vj are lifted.
   273 
   274 NB: the types in insts must be correctly instantiated already,
   275     i.e. Tinsts is not applied to insts.
   276 *)
   277 fun term_lift_inst_rule (st, i, Tinsts, insts, rule) =
   278 let val {maxidx,thy,...} = rep_thm st
   279     val paramTs = map #2 (params_of_state st i)
   280     and inc = maxidx+1
   281     fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
   282     (*lift only Var, not term, which must be lifted already*)
   283     fun liftpair (v,t) = (cterm_of thy (liftvar v), cterm_of thy t)
   284     fun liftTpair (((a, i), S), T) =
   285       (ctyp_of thy (TVar ((a, i + inc), S)),
   286        ctyp_of thy (Logic.incr_tvar inc T))
   287 in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
   288                      (Thm.lift_rule (Thm.cprem_of st i) rule)
   289 end;
   290 
   291 (*** Resolve after lifting and instantation; may refer to parameters of the
   292      subgoal.  Fails if "i" is out of range.  ***)
   293 
   294 (*compose version: arguments are as for bicompose.*)
   295 fun gen_compose_inst_tac instf sinsts (bires_flg, rule, nsubgoal) i st =
   296   if i > nprems_of st then no_tac st
   297   else st |>
   298     (compose_tac (bires_flg, instf (st, i, sinsts, rule), nsubgoal) i
   299      handle TERM (msg,_)   => (warning msg;  no_tac)
   300           | THM  (msg,_,_) => (warning msg;  no_tac));
   301 
   302 val compose_inst_tac = gen_compose_inst_tac lift_inst_rule;
   303 val compose_inst_tac' = gen_compose_inst_tac lift_inst_rule';
   304 
   305 (*"Resolve" version.  Note: res_inst_tac cannot behave sensibly if the
   306   terms that are substituted contain (term or type) unknowns from the
   307   goal, because it is unable to instantiate goal unknowns at the same time.
   308 
   309   The type checker is instructed not to freeze flexible type vars that
   310   were introduced during type inference and still remain in the term at the
   311   end.  This increases flexibility but can introduce schematic type vars in
   312   goals.
   313 *)
   314 fun res_inst_tac sinsts rule i =
   315     compose_inst_tac sinsts (false, rule, nprems_of rule) i;
   316 
   317 fun res_inst_tac' sinsts rule i =
   318     compose_inst_tac' sinsts (false, rule, nprems_of rule) i;
   319 
   320 (*eresolve elimination version*)
   321 fun eres_inst_tac sinsts rule i =
   322     compose_inst_tac sinsts (true, rule, nprems_of rule) i;
   323 
   324 fun eres_inst_tac' sinsts rule i =
   325     compose_inst_tac' sinsts (true, rule, nprems_of rule) i;
   326 
   327 (*For forw_inst_tac and dres_inst_tac.  Preserve Var indexes of rl;
   328   increment revcut_rl instead.*)
   329 fun make_elim_preserve rl =
   330   let val {maxidx,...} = rep_thm rl
   331       fun cvar ixn = cterm_of ProtoPure.thy (Var(ixn,propT));
   332       val revcut_rl' =
   333           instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
   334                              (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
   335       val arg = (false, rl, nprems_of rl)
   336       val [th] = Seq.list_of (bicompose false arg 1 revcut_rl')
   337   in  th  end
   338   handle Bind => raise THM("make_elim_preserve", 1, [rl]);
   339 
   340 (*instantiate and cut -- for a FACT, anyway...*)
   341 fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule);
   342 
   343 (*forward tactic applies a RULE to an assumption without deleting it*)
   344 fun forw_inst_tac sinsts rule = cut_inst_tac sinsts rule THEN' assume_tac;
   345 
   346 (*dresolve tactic applies a RULE to replace an assumption*)
   347 fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule);
   348 
   349 (*instantiate variables in the whole state*)
   350 val instantiate_tac = PRIMITIVE o read_instantiate;
   351 
   352 val instantiate_tac' = PRIMITIVE o Drule.read_instantiate';
   353 
   354 (*Deletion of an assumption*)
   355 fun thin_tac s = eres_inst_tac [("V",s)] thin_rl;
   356 
   357 (*** Applications of cut_rl ***)
   358 
   359 (*Used by metacut_tac*)
   360 fun bires_cut_tac arg i =
   361     resolve_tac [cut_rl] i  THEN  biresolve_tac arg (i+1) ;
   362 
   363 (*The conclusion of the rule gets assumed in subgoal i,
   364   while subgoal i+1,... are the premises of the rule.*)
   365 fun metacut_tac rule = bires_cut_tac [(false,rule)];
   366 
   367 (*Recognizes theorems that are not rules, but simple propositions*)
   368 fun is_fact rl =
   369     case prems_of rl of
   370         [] => true  |  _::_ => false;
   371 
   372 (*"Cut" a list of rules into the goal.  Their premises will become new
   373   subgoals.*)
   374 fun cut_rules_tac ths i = EVERY (map (fn th => metacut_tac th i) ths);
   375 
   376 (*As above, but inserts only facts (unconditional theorems);
   377   generates no additional subgoals. *)
   378 fun cut_facts_tac ths = cut_rules_tac  (List.filter is_fact ths);
   379 
   380 (*Introduce the given proposition as a lemma and subgoal*)
   381 fun subgoal_tac sprop =
   382   DETERM o res_inst_tac [("psi", sprop)] cut_rl THEN' SUBGOAL (fn (prop, _) =>
   383     let val concl' = Logic.strip_assums_concl prop in
   384       if null (term_tvars concl') then ()
   385       else warning"Type variables in new subgoal: add a type constraint?";
   386       all_tac
   387   end);
   388 
   389 (*Introduce a list of lemmas and subgoals*)
   390 fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops);
   391 
   392 
   393 (**** Indexing and filtering of theorems ****)
   394 
   395 (*Returns the list of potentially resolvable theorems for the goal "prem",
   396         using the predicate  could(subgoal,concl).
   397   Resulting list is no longer than "limit"*)
   398 fun filter_thms could (limit, prem, ths) =
   399   let val pb = Logic.strip_assums_concl prem;   (*delete assumptions*)
   400       fun filtr (limit, []) = []
   401         | filtr (limit, th::ths) =
   402             if limit=0 then  []
   403             else if could(pb, concl_of th)  then th :: filtr(limit-1, ths)
   404             else filtr(limit,ths)
   405   in  filtr(limit,ths)  end;
   406 
   407 
   408 (*** biresolution and resolution using nets ***)
   409 
   410 (** To preserve the order of the rules, tag them with increasing integers **)
   411 
   412 (*insert tags*)
   413 fun taglist k [] = []
   414   | taglist k (x::xs) = (k,x) :: taglist (k+1) xs;
   415 
   416 (*remove tags and suppress duplicates -- list is assumed sorted!*)
   417 fun untaglist [] = []
   418   | untaglist [(k:int,x)] = [x]
   419   | untaglist ((k,x) :: (rest as (k',x')::_)) =
   420       if k=k' then untaglist rest
   421       else    x :: untaglist rest;
   422 
   423 (*return list elements in original order*)
   424 fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls);
   425 
   426 (*insert one tagged brl into the pair of nets*)
   427 fun insert_tagged_brl (kbrl as (k, (eres, th)), (inet, enet)) =
   428   if eres then
   429     (case try Thm.major_prem_of th of
   430       SOME prem => (inet, Net.insert_term (K false) (prem, kbrl) enet)
   431     | NONE => error "insert_tagged_brl: elimination rule with no premises")
   432   else (Net.insert_term (K false) (concl_of th, kbrl) inet, enet);
   433 
   434 (*build a pair of nets for biresolution*)
   435 fun build_netpair netpair brls =
   436     foldr insert_tagged_brl netpair (taglist 1 brls);
   437 
   438 (*delete one kbrl from the pair of nets*)
   439 fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Drule.eq_thm_prop (th, th')
   440 
   441 fun delete_tagged_brl (brl as (eres, th), (inet, enet)) =
   442   (if eres then
   443     (case try Thm.major_prem_of th of
   444       SOME prem => (inet, Net.delete_term eq_kbrl (prem, ((), brl)) enet)
   445     | NONE => (inet, enet))  (*no major premise: ignore*)
   446   else (Net.delete_term eq_kbrl (Thm.concl_of th, ((), brl)) inet, enet))
   447   handle Net.DELETE => (inet,enet);
   448 
   449 
   450 (*biresolution using a pair of nets rather than rules.
   451     function "order" must sort and possibly filter the list of brls.
   452     boolean "match" indicates matching or unification.*)
   453 fun biresolution_from_nets_tac order match (inet,enet) =
   454   SUBGOAL
   455     (fn (prem,i) =>
   456       let val hyps = Logic.strip_assums_hyp prem
   457           and concl = Logic.strip_assums_concl prem
   458           val kbrls = Net.unify_term inet concl @
   459                       List.concat (map (Net.unify_term enet) hyps)
   460       in PRIMSEQ (biresolution match (order kbrls) i) end);
   461 
   462 (*versions taking pre-built nets.  No filtering of brls*)
   463 val biresolve_from_nets_tac = biresolution_from_nets_tac orderlist false;
   464 val bimatch_from_nets_tac   = biresolution_from_nets_tac orderlist true;
   465 
   466 (*fast versions using nets internally*)
   467 val net_biresolve_tac =
   468     biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty);
   469 
   470 val net_bimatch_tac =
   471     bimatch_from_nets_tac o build_netpair(Net.empty,Net.empty);
   472 
   473 (*** Simpler version for resolve_tac -- only one net, and no hyps ***)
   474 
   475 (*insert one tagged rl into the net*)
   476 fun insert_krl (krl as (k,th), net) =
   477     Net.insert_term (K false) (concl_of th, krl) net;
   478 
   479 (*build a net of rules for resolution*)
   480 fun build_net rls =
   481     foldr insert_krl Net.empty (taglist 1 rls);
   482 
   483 (*resolution using a net rather than rules; pred supports filt_resolve_tac*)
   484 fun filt_resolution_from_net_tac match pred net =
   485   SUBGOAL
   486     (fn (prem,i) =>
   487       let val krls = Net.unify_term net (Logic.strip_assums_concl prem)
   488       in
   489          if pred krls
   490          then PRIMSEQ
   491                 (biresolution match (map (pair false) (orderlist krls)) i)
   492          else no_tac
   493       end);
   494 
   495 (*Resolve the subgoal using the rules (making a net) unless too flexible,
   496    which means more than maxr rules are unifiable.      *)
   497 fun filt_resolve_tac rules maxr =
   498     let fun pred krls = length krls <= maxr
   499     in  filt_resolution_from_net_tac false pred (build_net rules)  end;
   500 
   501 (*versions taking pre-built nets*)
   502 val resolve_from_net_tac = filt_resolution_from_net_tac false (K true);
   503 val match_from_net_tac = filt_resolution_from_net_tac true (K true);
   504 
   505 (*fast versions using nets internally*)
   506 val net_resolve_tac = resolve_from_net_tac o build_net;
   507 val net_match_tac = match_from_net_tac o build_net;
   508 
   509 
   510 (*** For Natural Deduction using (bires_flg, rule) pairs ***)
   511 
   512 (*The number of new subgoals produced by the brule*)
   513 fun subgoals_of_brl (true,rule)  = nprems_of rule - 1
   514   | subgoals_of_brl (false,rule) = nprems_of rule;
   515 
   516 (*Less-than test: for sorting to minimize number of new subgoals*)
   517 fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2;
   518 
   519 
   520 (*** Meta-Rewriting Tactics ***)
   521 
   522 val simple_prover =
   523   SINGLE o (fn ss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_ss ss)));
   524 
   525 val rewrite = MetaSimplifier.rewrite_aux simple_prover;
   526 val simplify = MetaSimplifier.simplify_aux simple_prover;
   527 val rewrite_rule = simplify true;
   528 val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
   529 
   530 (*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
   531 fun asm_rewrite_goal_tac mode prover_tac ss =
   532   SELECT_GOAL
   533     (PRIMITIVE (MetaSimplifier.rewrite_goal_rule mode (SINGLE o prover_tac) ss 1));
   534 
   535 fun rewrite_goal_tac rews =
   536   let val ss = MetaSimplifier.empty_ss addsimps rews in
   537     fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
   538       (MetaSimplifier.theory_context (Thm.theory_of_thm st) ss) i st
   539   end;
   540 
   541 (*Rewrite throughout proof state. *)
   542 fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
   543 
   544 (*Rewrite subgoals only, not main goal. *)
   545 fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
   546 fun rewtac def = rewrite_goals_tac [def];
   547 
   548 val norm_hhf_tac =
   549   rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
   550   THEN' SUBGOAL (fn (t, i) =>
   551     if Drule.is_norm_hhf t then all_tac
   552     else rewrite_goal_tac [Drule.norm_hhf_eq] i);
   553 
   554 
   555 (*** for folding definitions, handling critical pairs ***)
   556 
   557 (*The depth of nesting in a term*)
   558 fun term_depth (Abs(a,T,t)) = 1 + term_depth t
   559   | term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t)
   560   | term_depth _ = 0;
   561 
   562 val lhs_of_thm = #1 o Logic.dest_equals o prop_of;
   563 
   564 (*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
   565   Returns longest lhs first to avoid folding its subexpressions.*)
   566 fun sort_lhs_depths defs =
   567   let val keylist = AList.make (term_depth o lhs_of_thm) defs
   568       val keys = distinct (sort (rev_order o int_ord) (map #2 keylist))
   569   in map (AList.find (op =) keylist) keys end;
   570 
   571 val rev_defs = sort_lhs_depths o map symmetric;
   572 
   573 fun fold_rule defs thm = Library.foldl (fn (th, ds) => rewrite_rule ds th) (thm, rev_defs defs);
   574 fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs));
   575 fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
   576 
   577 
   578 (*** Renaming of parameters in a subgoal
   579      Names may contain letters, digits or primes and must be
   580      separated by blanks ***)
   581 
   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 st Drule.conj_intr_thm, 2) i st)
   640   | _ => no_tac);
   641 
   642 val conjunction_tac = ALLGOALS (REPEAT_ALL_NEW conj_tac);
   643 
   644 fun smart_conjunction_tac 0 = assume_tac 1
   645   | smart_conjunction_tac _ = TRY conjunction_tac;
   646 
   647 end;
   648 
   649 structure BasicTactic: BASIC_TACTIC = Tactic;
   650 open BasicTactic;