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