src/Pure/tactic.ML
author wenzelm
Sat Nov 19 14:21:06 2005 +0100 (2005-11-19)
changeset 18209 6bcd9b2ca49b
parent 18145 6757627acf59
child 18471 ca9a864018d6
permissions -rw-r--r--
added CONJUNCTS: treat conjunction as separate sub-goals;
     1 (*  Title:      Pure/tactic.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 
     6 Tactics.
     7 *)
     8 
     9 signature BASIC_TACTIC =
    10 sig
    11   val ares_tac          : thm list -> int -> tactic
    12   val assume_tac        : int -> tactic
    13   val atac      : int ->tactic
    14   val bimatch_from_nets_tac:
    15       (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
    16   val bimatch_tac       : (bool*thm)list -> int -> tactic
    17   val biresolution_from_nets_tac:
    18         ('a list -> (bool * thm) list) ->
    19         bool -> 'a Net.net * 'a Net.net -> int -> tactic
    20   val biresolve_from_nets_tac:
    21       (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
    22   val biresolve_tac     : (bool*thm)list -> int -> tactic
    23   val build_net : thm list -> (int*thm) Net.net
    24   val build_netpair:    (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net ->
    25       (bool*thm)list -> (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net
    26   val compose_inst_tac  : (string*string)list -> (bool*thm*int) ->
    27                           int -> tactic
    28   val compose_tac       : (bool * thm * int) -> int -> tactic
    29   val cut_facts_tac     : thm list -> int -> tactic
    30   val cut_rules_tac     : thm list -> int -> tactic
    31   val cut_inst_tac      : (string*string)list -> thm -> int -> tactic
    32   val datac             : thm -> int -> int -> tactic
    33   val defer_tac         : int -> tactic
    34   val distinct_subgoals_tac     : tactic
    35   val dmatch_tac        : thm list -> int -> tactic
    36   val dresolve_tac      : thm list -> int -> tactic
    37   val dres_inst_tac     : (string*string)list -> thm -> int -> tactic
    38   val dtac              : thm -> int ->tactic
    39   val eatac             : thm -> int -> int -> tactic
    40   val etac              : thm -> int ->tactic
    41   val eq_assume_tac     : int -> tactic
    42   val ematch_tac        : thm list -> int -> tactic
    43   val eresolve_tac      : thm list -> int -> tactic
    44   val eres_inst_tac     : (string*string)list -> thm -> int -> tactic
    45   val fatac             : thm -> int -> int -> tactic
    46   val filter_prems_tac  : (term -> bool) -> int -> tactic
    47   val filter_thms       : (term*term->bool) -> int*term*thm list -> thm list
    48   val filt_resolve_tac  : thm list -> int -> int -> tactic
    49   val flexflex_tac      : tactic
    50   val fold_goals_tac    : thm list -> tactic
    51   val fold_rule         : thm list -> thm -> thm
    52   val fold_tac          : thm list -> tactic
    53   val forward_tac       : thm list -> int -> tactic
    54   val forw_inst_tac     : (string*string)list -> thm -> int -> tactic
    55   val ftac              : thm -> int ->tactic
    56   val insert_tagged_brl : ('a * (bool * thm)) *
    57     (('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net) ->
    58       ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
    59   val delete_tagged_brl : (bool * thm) *
    60     (('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net) ->
    61       ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
    62   val is_fact           : thm -> bool
    63   val lessb             : (bool * thm) * (bool * thm) -> bool
    64   val lift_inst_rule    : thm * int * (string*string)list * thm -> thm
    65   val make_elim         : thm -> thm
    66   val match_from_net_tac        : (int*thm) Net.net -> int -> tactic
    67   val match_tac : thm list -> int -> tactic
    68   val metacut_tac       : thm -> int -> tactic
    69   val net_bimatch_tac   : (bool*thm) list -> int -> tactic
    70   val net_biresolve_tac : (bool*thm) list -> int -> tactic
    71   val net_match_tac     : thm list -> int -> tactic
    72   val net_resolve_tac   : thm list -> int -> tactic
    73   val norm_hhf_tac      : int -> tactic
    74   val prune_params_tac  : tactic
    75   val rename_params_tac : string list -> int -> tactic
    76   val rename_tac        : string -> int -> tactic
    77   val rename_last_tac   : string -> string list -> int -> tactic
    78   val resolve_from_net_tac      : (int*thm) Net.net -> int -> tactic
    79   val resolve_tac       : thm list -> int -> tactic
    80   val res_inst_tac      : (string*string)list -> thm -> int -> tactic
    81   val rewrite_goal_tac  : thm list -> int -> tactic
    82   val rewrite_goals_rule: thm list -> thm -> thm
    83   val rewrite_rule      : thm list -> thm -> thm
    84   val rewrite_goals_tac : thm list -> tactic
    85   val rewrite_tac       : thm list -> tactic
    86   val asm_rewrite_goal_tac: bool * bool * bool -> (simpset -> tactic) -> simpset -> int -> tactic
    87   val rewtac            : thm -> tactic
    88   val rotate_tac        : int -> int -> tactic
    89   val rtac              : thm -> int -> tactic
    90   val rule_by_tactic    : tactic -> thm -> thm
    91   val solve_tac         : thm list -> int -> tactic
    92   val subgoal_tac       : string -> int -> tactic
    93   val subgoals_tac      : string list -> int -> tactic
    94   val subgoals_of_brl   : bool * thm -> int
    95   val term_lift_inst_rule       :
    96       thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm
    97       -> thm
    98   val instantiate_tac   : (string * string) list -> tactic
    99   val thin_tac          : string -> int -> tactic
   100   val trace_goalno_tac  : (int -> tactic) -> int -> tactic
   101   val CONJUNCTS: tactic -> int -> tactic
   102 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 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) = term_of a aconv term_of 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  (*Applying Thm.varifyT to the result of thawfn would (re-)generalize
   213           all type variables that appear in the subgoals. Unfortunately, it
   214           would also break the function AxClass.intro_classes_tac, even in the
   215           trivial case where the type class has no axioms.*)
   216         Seq.single (thawfn implied)
   217     end
   218 end;
   219 
   220 
   221 (*Determine print names of goal parameters (reversed)*)
   222 fun innermost_params i st =
   223   let val (_, _, Bi, _) = dest_state (st, i)
   224   in rename_wrt_term Bi (Logic.strip_params Bi) end;
   225 
   226 (*params of subgoal i as they are printed*)
   227 fun params_of_state st i =
   228   let val (_, _, Bi, _) = dest_state(st,i)
   229       val params = Logic.strip_params Bi
   230   in rev(rename_wrt_term Bi params) end;
   231 
   232 (*read instantiations with respect to subgoal i of proof state st*)
   233 fun read_insts_in_state (st, i, sinsts, rule) =
   234   let val thy = Thm.theory_of_thm st
   235       and params = params_of_state st i
   236       and rts = types_sorts rule and (types,sorts) = types_sorts st
   237       fun types'(a, ~1) = (case AList.lookup (op =) params a of NONE => types (a, ~1) | sm => sm)
   238         | types' ixn = types ixn;
   239       val used = Drule.add_used rule (Drule.add_used st []);
   240   in read_insts thy rts (types',sorts) used sinsts end;
   241 
   242 (*Lift and instantiate a rule wrt the given state and subgoal number *)
   243 fun lift_inst_rule' (st, i, sinsts, rule) =
   244 let val (Tinsts,insts) = read_insts_in_state (st, i, sinsts, rule)
   245     and {maxidx,...} = rep_thm st
   246     and params = params_of_state st i
   247     val paramTs = map #2 params
   248     and inc = maxidx+1
   249     fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
   250       | liftvar t = raise TERM("Variable expected", [t]);
   251     fun liftterm t = list_abs_free (params,
   252                                     Logic.incr_indexes(paramTs,inc) t)
   253     (*Lifts instantiation pair over params*)
   254     fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
   255     val lifttvar = pairself (ctyp_fun (Logic.incr_tvar inc))
   256 in Drule.instantiate (map lifttvar Tinsts, map liftpair insts)
   257                      (Thm.lift_rule (Thm.cprem_of st i) rule)
   258 end;
   259 
   260 fun lift_inst_rule (st, i, sinsts, rule) = lift_inst_rule'
   261   (st, i, map (apfst Syntax.indexname) sinsts, rule);
   262 
   263 (*
   264 Like lift_inst_rule but takes terms, not strings, where the terms may contain
   265 Bounds referring to parameters of the subgoal.
   266 
   267 insts: [...,(vj,tj),...]
   268 
   269 The tj may contain references to parameters of subgoal i of the state st
   270 in the form of Bound k, i.e. the tj may be subterms of the subgoal.
   271 To saturate the lose bound vars, the tj are enclosed in abstractions
   272 corresponding to the parameters of subgoal i, thus turning them into
   273 functions. At the same time, the types of the vj are lifted.
   274 
   275 NB: the types in insts must be correctly instantiated already,
   276     i.e. Tinsts is not applied to insts.
   277 *)
   278 fun term_lift_inst_rule (st, i, Tinsts, insts, rule) =
   279 let val {maxidx,thy,...} = rep_thm st
   280     val paramTs = map #2 (params_of_state st i)
   281     and inc = maxidx+1
   282     fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
   283     (*lift only Var, not term, which must be lifted already*)
   284     fun liftpair (v,t) = (cterm_of thy (liftvar v), cterm_of thy t)
   285     fun liftTpair (((a, i), S), T) =
   286       (ctyp_of thy (TVar ((a, i + inc), S)),
   287        ctyp_of thy (Logic.incr_tvar inc T))
   288 in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
   289                      (Thm.lift_rule (Thm.cprem_of st i) rule)
   290 end;
   291 
   292 (*** Resolve after lifting and instantation; may refer to parameters of the
   293      subgoal.  Fails if "i" is out of range.  ***)
   294 
   295 (*compose version: arguments are as for bicompose.*)
   296 fun gen_compose_inst_tac instf sinsts (bires_flg, rule, nsubgoal) i st =
   297   if i > nprems_of st then no_tac st
   298   else st |>
   299     (compose_tac (bires_flg, instf (st, i, sinsts, rule), nsubgoal) i
   300      handle TERM (msg,_)   => (warning msg;  no_tac)
   301           | THM  (msg,_,_) => (warning msg;  no_tac));
   302 
   303 val compose_inst_tac = gen_compose_inst_tac lift_inst_rule;
   304 val compose_inst_tac' = gen_compose_inst_tac lift_inst_rule';
   305 
   306 (*"Resolve" version.  Note: res_inst_tac cannot behave sensibly if the
   307   terms that are substituted contain (term or type) unknowns from the
   308   goal, because it is unable to instantiate goal unknowns at the same time.
   309 
   310   The type checker is instructed not to freeze flexible type vars that
   311   were introduced during type inference and still remain in the term at the
   312   end.  This increases flexibility but can introduce schematic type vars in
   313   goals.
   314 *)
   315 fun res_inst_tac sinsts rule i =
   316     compose_inst_tac sinsts (false, rule, nprems_of rule) i;
   317 
   318 fun res_inst_tac' sinsts rule i =
   319     compose_inst_tac' sinsts (false, rule, nprems_of rule) i;
   320 
   321 (*eresolve elimination version*)
   322 fun eres_inst_tac sinsts rule i =
   323     compose_inst_tac sinsts (true, rule, nprems_of rule) i;
   324 
   325 fun eres_inst_tac' sinsts rule i =
   326     compose_inst_tac' sinsts (true, rule, nprems_of rule) i;
   327 
   328 (*For forw_inst_tac and dres_inst_tac.  Preserve Var indexes of rl;
   329   increment revcut_rl instead.*)
   330 fun make_elim_preserve rl =
   331   let val {maxidx,...} = rep_thm rl
   332       fun cvar ixn = cterm_of ProtoPure.thy (Var(ixn,propT));
   333       val revcut_rl' =
   334           instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
   335                              (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
   336       val arg = (false, rl, nprems_of rl)
   337       val [th] = Seq.list_of (bicompose false arg 1 revcut_rl')
   338   in  th  end
   339   handle Bind => raise THM("make_elim_preserve", 1, [rl]);
   340 
   341 (*instantiate and cut -- for a FACT, anyway...*)
   342 fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule);
   343 
   344 (*forward tactic applies a RULE to an assumption without deleting it*)
   345 fun forw_inst_tac sinsts rule = cut_inst_tac sinsts rule THEN' assume_tac;
   346 
   347 (*dresolve tactic applies a RULE to replace an assumption*)
   348 fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule);
   349 
   350 (*instantiate variables in the whole state*)
   351 val instantiate_tac = PRIMITIVE o read_instantiate;
   352 
   353 val instantiate_tac' = PRIMITIVE o Drule.read_instantiate';
   354 
   355 (*Deletion of an assumption*)
   356 fun thin_tac s = eres_inst_tac [("V",s)] thin_rl;
   357 
   358 (*** Applications of cut_rl ***)
   359 
   360 (*Used by metacut_tac*)
   361 fun bires_cut_tac arg i =
   362     resolve_tac [cut_rl] i  THEN  biresolve_tac arg (i+1) ;
   363 
   364 (*The conclusion of the rule gets assumed in subgoal i,
   365   while subgoal i+1,... are the premises of the rule.*)
   366 fun metacut_tac rule = bires_cut_tac [(false,rule)];
   367 
   368 (*Recognizes theorems that are not rules, but simple propositions*)
   369 fun is_fact rl =
   370     case prems_of rl of
   371         [] => true  |  _::_ => false;
   372 
   373 (*"Cut" a list of rules into the goal.  Their premises will become new
   374   subgoals.*)
   375 fun cut_rules_tac ths i = EVERY (map (fn th => metacut_tac th i) ths);
   376 
   377 (*As above, but inserts only facts (unconditional theorems);
   378   generates no additional subgoals. *)
   379 fun cut_facts_tac ths = cut_rules_tac  (List.filter is_fact ths);
   380 
   381 (*Introduce the given proposition as a lemma and subgoal*)
   382 fun subgoal_tac sprop =
   383   DETERM o res_inst_tac [("psi", sprop)] cut_rl THEN' SUBGOAL (fn (prop, _) =>
   384     let val concl' = Logic.strip_assums_concl prop in
   385       if null (term_tvars concl') then ()
   386       else warning"Type variables in new subgoal: add a type constraint?";
   387       all_tac
   388   end);
   389 
   390 (*Introduce a list of lemmas and subgoals*)
   391 fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops);
   392 
   393 
   394 (**** Indexing and filtering of theorems ****)
   395 
   396 (*Returns the list of potentially resolvable theorems for the goal "prem",
   397         using the predicate  could(subgoal,concl).
   398   Resulting list is no longer than "limit"*)
   399 fun filter_thms could (limit, prem, ths) =
   400   let val pb = Logic.strip_assums_concl prem;   (*delete assumptions*)
   401       fun filtr (limit, []) = []
   402         | filtr (limit, th::ths) =
   403             if limit=0 then  []
   404             else if could(pb, concl_of th)  then th :: filtr(limit-1, ths)
   405             else filtr(limit,ths)
   406   in  filtr(limit,ths)  end;
   407 
   408 
   409 (*** biresolution and resolution using nets ***)
   410 
   411 (** To preserve the order of the rules, tag them with increasing integers **)
   412 
   413 (*insert tags*)
   414 fun taglist k [] = []
   415   | taglist k (x::xs) = (k,x) :: taglist (k+1) xs;
   416 
   417 (*remove tags and suppress duplicates -- list is assumed sorted!*)
   418 fun untaglist [] = []
   419   | untaglist [(k:int,x)] = [x]
   420   | untaglist ((k,x) :: (rest as (k',x')::_)) =
   421       if k=k' then untaglist rest
   422       else    x :: untaglist rest;
   423 
   424 (*return list elements in original order*)
   425 fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls);
   426 
   427 (*insert one tagged brl into the pair of nets*)
   428 fun insert_tagged_brl (kbrl as (k, (eres, th)), (inet, enet)) =
   429   if eres then
   430     (case try Thm.major_prem_of th of
   431       SOME prem => (inet, Net.insert_term (K false) (prem, kbrl) enet)
   432     | NONE => error "insert_tagged_brl: elimination rule with no premises")
   433   else (Net.insert_term (K false) (concl_of th, kbrl) inet, enet);
   434 
   435 (*build a pair of nets for biresolution*)
   436 fun build_netpair netpair brls =
   437     foldr insert_tagged_brl netpair (taglist 1 brls);
   438 
   439 (*delete one kbrl from the pair of nets*)
   440 fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Drule.eq_thm_prop (th, th')
   441 
   442 fun delete_tagged_brl (brl as (eres, th), (inet, enet)) =
   443   (if eres then
   444     (case try Thm.major_prem_of th of
   445       SOME prem => (inet, Net.delete_term eq_kbrl (prem, ((), brl)) enet)
   446     | NONE => (inet, enet))  (*no major premise: ignore*)
   447   else (Net.delete_term eq_kbrl (Thm.concl_of th, ((), brl)) inet, enet))
   448   handle Net.DELETE => (inet,enet);
   449 
   450 
   451 (*biresolution using a pair of nets rather than rules.
   452     function "order" must sort and possibly filter the list of brls.
   453     boolean "match" indicates matching or unification.*)
   454 fun biresolution_from_nets_tac order match (inet,enet) =
   455   SUBGOAL
   456     (fn (prem,i) =>
   457       let val hyps = Logic.strip_assums_hyp prem
   458           and concl = Logic.strip_assums_concl prem
   459           val kbrls = Net.unify_term inet concl @
   460                       List.concat (map (Net.unify_term enet) hyps)
   461       in PRIMSEQ (biresolution match (order kbrls) i) end);
   462 
   463 (*versions taking pre-built nets.  No filtering of brls*)
   464 val biresolve_from_nets_tac = biresolution_from_nets_tac orderlist false;
   465 val bimatch_from_nets_tac   = biresolution_from_nets_tac orderlist true;
   466 
   467 (*fast versions using nets internally*)
   468 val net_biresolve_tac =
   469     biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty);
   470 
   471 val net_bimatch_tac =
   472     bimatch_from_nets_tac o build_netpair(Net.empty,Net.empty);
   473 
   474 (*** Simpler version for resolve_tac -- only one net, and no hyps ***)
   475 
   476 (*insert one tagged rl into the net*)
   477 fun insert_krl (krl as (k,th), net) =
   478     Net.insert_term (K false) (concl_of th, krl) net;
   479 
   480 (*build a net of rules for resolution*)
   481 fun build_net rls =
   482     foldr insert_krl Net.empty (taglist 1 rls);
   483 
   484 (*resolution using a net rather than rules; pred supports filt_resolve_tac*)
   485 fun filt_resolution_from_net_tac match pred net =
   486   SUBGOAL
   487     (fn (prem,i) =>
   488       let val krls = Net.unify_term net (Logic.strip_assums_concl prem)
   489       in
   490          if pred krls
   491          then PRIMSEQ
   492                 (biresolution match (map (pair false) (orderlist krls)) i)
   493          else no_tac
   494       end);
   495 
   496 (*Resolve the subgoal using the rules (making a net) unless too flexible,
   497    which means more than maxr rules are unifiable.      *)
   498 fun filt_resolve_tac rules maxr =
   499     let fun pred krls = length krls <= maxr
   500     in  filt_resolution_from_net_tac false pred (build_net rules)  end;
   501 
   502 (*versions taking pre-built nets*)
   503 val resolve_from_net_tac = filt_resolution_from_net_tac false (K true);
   504 val match_from_net_tac = filt_resolution_from_net_tac true (K true);
   505 
   506 (*fast versions using nets internally*)
   507 val net_resolve_tac = resolve_from_net_tac o build_net;
   508 val net_match_tac = match_from_net_tac o build_net;
   509 
   510 
   511 (*** For Natural Deduction using (bires_flg, rule) pairs ***)
   512 
   513 (*The number of new subgoals produced by the brule*)
   514 fun subgoals_of_brl (true,rule)  = nprems_of rule - 1
   515   | subgoals_of_brl (false,rule) = nprems_of rule;
   516 
   517 (*Less-than test: for sorting to minimize number of new subgoals*)
   518 fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2;
   519 
   520 
   521 (*** Meta-Rewriting Tactics ***)
   522 
   523 val simple_prover =
   524   SINGLE o (fn ss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_ss ss)));
   525 
   526 val rewrite = MetaSimplifier.rewrite_aux simple_prover;
   527 val simplify = MetaSimplifier.simplify_aux simple_prover;
   528 val rewrite_rule = simplify true;
   529 val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
   530 
   531 (*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
   532 fun asm_rewrite_goal_tac mode prover_tac ss =
   533   SELECT_GOAL
   534     (PRIMITIVE (MetaSimplifier.rewrite_goal_rule mode (SINGLE o prover_tac) ss 1));
   535 
   536 fun rewrite_goal_tac rews =
   537   let val ss = MetaSimplifier.empty_ss addsimps rews in
   538     fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
   539       (MetaSimplifier.theory_context (Thm.theory_of_thm st) ss) i st
   540   end;
   541 
   542 (*Rewrite throughout proof state. *)
   543 fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
   544 
   545 (*Rewrite subgoals only, not main goal. *)
   546 fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
   547 fun rewtac def = rewrite_goals_tac [def];
   548 
   549 val norm_hhf_tac =
   550   rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
   551   THEN' SUBGOAL (fn (t, i) =>
   552     if Drule.is_norm_hhf t then all_tac
   553     else rewrite_goal_tac [Drule.norm_hhf_eq] i);
   554 
   555 
   556 (*** for folding definitions, handling critical pairs ***)
   557 
   558 (*The depth of nesting in a term*)
   559 fun term_depth (Abs(a,T,t)) = 1 + term_depth t
   560   | term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t)
   561   | term_depth _ = 0;
   562 
   563 val lhs_of_thm = #1 o Logic.dest_equals o prop_of;
   564 
   565 (*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
   566   Returns longest lhs first to avoid folding its subexpressions.*)
   567 fun sort_lhs_depths defs =
   568   let val keylist = AList.make (term_depth o lhs_of_thm) defs
   569       val keys = distinct (sort (rev_order o int_ord) (map #2 keylist))
   570   in map (AList.find (op =) keylist) keys end;
   571 
   572 val rev_defs = sort_lhs_depths o map symmetric;
   573 
   574 fun fold_rule defs thm = Library.foldl (fn (th, ds) => rewrite_rule ds th) (thm, rev_defs defs);
   575 fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs));
   576 fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
   577 
   578 
   579 (*** Renaming of parameters in a subgoal
   580      Names may contain letters, digits or primes and must be
   581      separated by blanks ***)
   582 
   583 fun rename_params_tac xs i =
   584   case Library.find_first (not o Syntax.is_identifier) xs of
   585       SOME x => error ("Not an identifier: " ^ x)
   586     | NONE =>
   587        (if !Logic.auto_rename
   588          then (warning "Resetting Logic.auto_rename";
   589              Logic.auto_rename := false)
   590         else (); PRIMITIVE (rename_params_rule (xs, i)));
   591 
   592 fun rename_tac str i =
   593   let val cs = Symbol.explode str in
   594   case #2 (take_prefix (Symbol.is_letdig orf Symbol.is_blank) cs) of
   595       [] => rename_params_tac (scanwords Symbol.is_letdig cs) i
   596     | c::_ => error ("Illegal character: " ^ c)
   597   end;
   598 
   599 (*Rename recent parameters using names generated from a and the suffixes,
   600   provided the string a, which represents a term, is an identifier. *)
   601 fun rename_last_tac a sufs i =
   602   let val names = map (curry op^ a) sufs
   603   in  if Syntax.is_identifier a
   604       then PRIMITIVE (rename_params_rule (names,i))
   605       else all_tac
   606   end;
   607 
   608 (*Prunes all redundant parameters from the proof state by rewriting.
   609   DOES NOT rewrite main goal, where quantification over an unused bound
   610     variable is sometimes done to avoid the need for cut_facts_tac.*)
   611 val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
   612 
   613 (*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
   614   right to left if n is positive, and from left to right if n is negative.*)
   615 fun rotate_tac 0 i = all_tac
   616   | rotate_tac k i = PRIMITIVE (rotate_rule k i);
   617 
   618 (*Rotates the given subgoal to be the last.*)
   619 fun defer_tac i = PRIMITIVE (permute_prems (i-1) 1);
   620 
   621 (* remove premises that do not satisfy p; fails if all prems satisfy p *)
   622 fun filter_prems_tac p =
   623   let fun Then NONE tac = SOME tac
   624         | Then (SOME tac) tac' = SOME(tac THEN' tac');
   625       fun thins ((tac,n),H) =
   626         if p H then (tac,n+1)
   627         else (Then tac (rotate_tac n THEN' etac thin_rl),0);
   628   in SUBGOAL(fn (subg,n) =>
   629        let val Hs = Logic.strip_assums_hyp subg
   630        in case fst(Library.foldl thins ((NONE,0),Hs)) of
   631             NONE => no_tac | SOME tac => tac n
   632        end)
   633   end;
   634 
   635 
   636 (*meta-level conjunction*)
   637 val conj_tac = SUBGOAL (fn (Const ("all", _) $ Abs (_, _, Const ("==>", _) $
   638       (Const ("==>", _) $ _ $ (Const ("==>", _) $ _ $ Bound 0)) $ Bound 0), i) =>
   639     (fn st =>
   640       compose_tac (false, Drule.incr_indexes st Drule.conj_intr_thm, 2) i st)
   641   | _ => no_tac);
   642 
   643 val conjunction_tac = ALLGOALS (REPEAT_ALL_NEW conj_tac);
   644 
   645 fun smart_conjunction_tac 0 = assume_tac 1
   646   | smart_conjunction_tac _ = TRY conjunction_tac;
   647 
   648 (*treat conjunction as separate sub-goals*)
   649 fun CONJUNCTS tac =
   650   SELECT_GOAL (TRY conjunction_tac
   651     THEN tac
   652     THEN PRIMITIVE Drule.conj_curry);
   653 
   654 end;
   655 
   656 structure BasicTactic: BASIC_TACTIC = Tactic;
   657 open BasicTactic;