src/Pure/tactic.ML
author wenzelm
Thu Dec 07 00:42:04 2006 +0100 (2006-12-07)
changeset 21687 f689f729afab
parent 20302 265b2342cf21
child 21708 45e7491bea47
permissions -rw-r--r--
reorganized structure Goal vs. Tactic;
     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 lessb             : (bool * thm) * (bool * thm) -> bool
    63   val lift_inst_rule    : thm * int * (string*string)list * thm -> thm
    64   val make_elim         : thm -> thm
    65   val match_from_net_tac        : (int*thm) Net.net -> int -> tactic
    66   val match_tac : thm list -> int -> tactic
    67   val metacut_tac       : thm -> int -> tactic
    68   val net_bimatch_tac   : (bool*thm) list -> int -> tactic
    69   val net_biresolve_tac : (bool*thm) list -> int -> tactic
    70   val net_match_tac     : thm list -> int -> tactic
    71   val net_resolve_tac   : thm list -> int -> tactic
    72   val prune_params_tac  : tactic
    73   val rename_params_tac : string list -> int -> tactic
    74   val rename_tac        : string -> int -> tactic
    75   val rename_last_tac   : string -> string list -> int -> tactic
    76   val resolve_from_net_tac      : (int*thm) Net.net -> int -> tactic
    77   val resolve_tac       : thm list -> int -> tactic
    78   val res_inst_tac      : (string*string)list -> thm -> int -> tactic
    79   val rewrite_goals_rule: thm list -> thm -> thm
    80   val rewrite_rule      : thm list -> thm -> thm
    81   val rewrite_goals_tac : thm list -> tactic
    82   val rewrite_tac       : thm list -> tactic
    83   val rewtac            : thm -> tactic
    84   val rotate_tac        : int -> int -> tactic
    85   val rtac              : thm -> int -> tactic
    86   val rule_by_tactic    : tactic -> thm -> thm
    87   val solve_tac         : thm list -> int -> tactic
    88   val subgoal_tac       : string -> int -> tactic
    89   val subgoals_tac      : string list -> int -> tactic
    90   val subgoals_of_brl   : bool * thm -> int
    91   val term_lift_inst_rule       :
    92       thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm
    93       -> thm
    94   val instantiate_tac   : (string * string) list -> tactic
    95   val thin_tac          : string -> int -> tactic
    96   val trace_goalno_tac  : (int -> tactic) -> int -> tactic
    97 end;
    98 
    99 signature TACTIC =
   100 sig
   101   include BASIC_TACTIC
   102   val innermost_params: int -> thm -> (string * typ) list
   103   val untaglist: (int * 'a) list -> 'a list
   104   val eq_kbrl: ('a * (bool * thm)) * ('a * (bool * thm)) -> bool
   105   val orderlist: (int * 'a) list -> 'a list
   106   val rewrite: bool -> thm list -> cterm -> thm
   107   val simplify: bool -> thm list -> thm -> thm
   108   val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) ->
   109                           int -> tactic
   110   val lift_inst_rule'   : thm * int * (indexname * string) list * thm -> thm
   111   val eres_inst_tac'    : (indexname * string) list -> thm -> int -> tactic
   112   val res_inst_tac'     : (indexname * string) list -> thm -> int -> tactic
   113   val instantiate_tac'  : (indexname * string) list -> tactic
   114   val make_elim_preserve: thm -> thm
   115 end;
   116 
   117 structure Tactic: TACTIC =
   118 struct
   119 
   120 (*Discover which goal is chosen:  SOMEGOAL(trace_goalno_tac tac) *)
   121 fun trace_goalno_tac tac i st =
   122     case Seq.pull(tac i st) of
   123         NONE    => Seq.empty
   124       | seqcell => (tracing ("Subgoal " ^ string_of_int i ^ " selected");
   125                          Seq.make(fn()=> seqcell));
   126 
   127 (*Makes a rule by applying a tactic to an existing rule*)
   128 fun rule_by_tactic tac rl =
   129   let
   130     val ctxt = Variable.thm_context rl;
   131     val ((_, [st]), ctxt') = Variable.import true [rl] ctxt;
   132   in
   133     (case Seq.pull (tac st) of
   134       NONE => raise THM ("rule_by_tactic", 0, [rl])
   135     | SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt' ctxt) st'))
   136   end;
   137 
   138 
   139 (*** Basic tactics ***)
   140 
   141 (*** The following fail if the goal number is out of range:
   142      thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
   143 
   144 (*Solve subgoal i by assumption*)
   145 fun assume_tac i = PRIMSEQ (assumption i);
   146 
   147 (*Solve subgoal i by assumption, using no unification*)
   148 fun eq_assume_tac i = PRIMITIVE (eq_assumption i);
   149 
   150 (** Resolution/matching tactics **)
   151 
   152 (*The composition rule/state: no lifting or var renaming.
   153   The arg = (bires_flg, orule, m) ;  see bicompose for explanation.*)
   154 fun compose_tac arg i = PRIMSEQ (bicompose false arg i);
   155 
   156 (*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
   157   like [| P&Q; P==>R |] ==> R *)
   158 fun make_elim rl = zero_var_indexes (rl RS revcut_rl);
   159 
   160 (*Attack subgoal i by resolution, using flags to indicate elimination rules*)
   161 fun biresolve_tac brules i = PRIMSEQ (biresolution false brules i);
   162 
   163 (*Resolution: the simple case, works for introduction rules*)
   164 fun resolve_tac rules = biresolve_tac (map (pair false) rules);
   165 
   166 (*Resolution with elimination rules only*)
   167 fun eresolve_tac rules = biresolve_tac (map (pair true) rules);
   168 
   169 (*Forward reasoning using destruction rules.*)
   170 fun forward_tac rls = resolve_tac (map make_elim rls) THEN' assume_tac;
   171 
   172 (*Like forward_tac, but deletes the assumption after use.*)
   173 fun dresolve_tac rls = eresolve_tac (map make_elim rls);
   174 
   175 (*Shorthand versions: for resolution with a single theorem*)
   176 val atac    =   assume_tac;
   177 fun rtac rl =  resolve_tac [rl];
   178 fun dtac rl = dresolve_tac [rl];
   179 fun etac rl = eresolve_tac [rl];
   180 fun ftac rl =  forward_tac [rl];
   181 fun datac thm j = EVERY' (dtac thm::replicate j atac);
   182 fun eatac thm j = EVERY' (etac thm::replicate j atac);
   183 fun fatac thm j = EVERY' (ftac thm::replicate j atac);
   184 
   185 (*Use an assumption or some rules ... A popular combination!*)
   186 fun ares_tac rules = assume_tac  ORELSE'  resolve_tac rules;
   187 
   188 fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac;
   189 
   190 (*Matching tactics -- as above, but forbid updating of state*)
   191 fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i);
   192 fun match_tac rules  = bimatch_tac (map (pair false) rules);
   193 fun ematch_tac rules = bimatch_tac (map (pair true) rules);
   194 fun dmatch_tac rls   = ematch_tac (map make_elim rls);
   195 
   196 (*Smash all flex-flex disagreement pairs in the proof state.*)
   197 val flexflex_tac = PRIMSEQ flexflex_rule;
   198 
   199 (*Remove duplicate subgoals.*)
   200 fun distinct_subgoals_tac state =
   201   let
   202     val perm_tac = PRIMITIVE oo Thm.permute_prems;
   203 
   204     fun distinct_tac (i, k) =
   205       perm_tac 0 (i - 1) THEN
   206       perm_tac 1 (k - 1) THEN
   207       DETERM (PRIMSEQ (fn st =>
   208         Thm.compose_no_flatten false (st, 0) 1
   209           (Drule.incr_indexes st Drule.distinct_prems_rl))) THEN
   210       perm_tac 1 (1 - k) THEN
   211       perm_tac 0 (1 - i);
   212 
   213     fun distinct_subgoal_tac i st =
   214       (case Library.drop (i - 1, Thm.prems_of st) of
   215         [] => no_tac st
   216       | A :: Bs =>
   217           st |> EVERY (fold (fn (B, k) =>
   218             if A aconv B then cons (distinct_tac (i, k)) else I) (Bs ~~ (1 upto length Bs)) []));
   219 
   220     val goals = Thm.prems_of state;
   221     val dups = distinct (eq_fst (op aconv)) (goals ~~ (1 upto length goals));
   222   in EVERY (rev (map (distinct_subgoal_tac o snd) dups)) state end;
   223 
   224 (*Determine print names of goal parameters (reversed)*)
   225 fun innermost_params i st =
   226   let val (_, _, Bi, _) = dest_state (st, i)
   227   in rename_wrt_term Bi (Logic.strip_params Bi) end;
   228 
   229 (*params of subgoal i as they are printed*)
   230 fun params_of_state i st = rev (innermost_params i st);
   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 i st
   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 i st
   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.read_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 i st)
   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 (*"Cut" a list of rules into the goal.  Their premises will become new
   369   subgoals.*)
   370 fun cut_rules_tac ths i = EVERY (map (fn th => metacut_tac th i) ths);
   371 
   372 (*As above, but inserts only facts (unconditional theorems);
   373   generates no additional subgoals. *)
   374 fun cut_facts_tac ths = cut_rules_tac (filter Thm.no_prems ths);
   375 
   376 (*Introduce the given proposition as a lemma and subgoal*)
   377 fun subgoal_tac sprop =
   378   DETERM o res_inst_tac [("psi", sprop)] cut_rl THEN' SUBGOAL (fn (prop, _) =>
   379     let val concl' = Logic.strip_assums_concl prop in
   380       if null (term_tvars concl') then ()
   381       else warning"Type variables in new subgoal: add a type constraint?";
   382       all_tac
   383   end);
   384 
   385 (*Introduce a list of lemmas and subgoals*)
   386 fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops);
   387 
   388 
   389 (**** Indexing and filtering of theorems ****)
   390 
   391 (*Returns the list of potentially resolvable theorems for the goal "prem",
   392         using the predicate  could(subgoal,concl).
   393   Resulting list is no longer than "limit"*)
   394 fun filter_thms could (limit, prem, ths) =
   395   let val pb = Logic.strip_assums_concl prem;   (*delete assumptions*)
   396       fun filtr (limit, []) = []
   397         | filtr (limit, th::ths) =
   398             if limit=0 then  []
   399             else if could(pb, concl_of th)  then th :: filtr(limit-1, ths)
   400             else filtr(limit,ths)
   401   in  filtr(limit,ths)  end;
   402 
   403 
   404 (*** biresolution and resolution using nets ***)
   405 
   406 (** To preserve the order of the rules, tag them with increasing integers **)
   407 
   408 (*insert tags*)
   409 fun taglist k [] = []
   410   | taglist k (x::xs) = (k,x) :: taglist (k+1) xs;
   411 
   412 (*remove tags and suppress duplicates -- list is assumed sorted!*)
   413 fun untaglist [] = []
   414   | untaglist [(k:int,x)] = [x]
   415   | untaglist ((k,x) :: (rest as (k',x')::_)) =
   416       if k=k' then untaglist rest
   417       else    x :: untaglist rest;
   418 
   419 (*return list elements in original order*)
   420 fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls);
   421 
   422 (*insert one tagged brl into the pair of nets*)
   423 fun insert_tagged_brl (kbrl as (k, (eres, th)), (inet, enet)) =
   424   if eres then
   425     (case try Thm.major_prem_of th of
   426       SOME prem => (inet, Net.insert_term (K false) (prem, kbrl) enet)
   427     | NONE => error "insert_tagged_brl: elimination rule with no premises")
   428   else (Net.insert_term (K false) (concl_of th, kbrl) inet, enet);
   429 
   430 (*build a pair of nets for biresolution*)
   431 fun build_netpair netpair brls =
   432     foldr insert_tagged_brl netpair (taglist 1 brls);
   433 
   434 (*delete one kbrl from the pair of nets*)
   435 fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Drule.eq_thm_prop (th, th')
   436 
   437 fun delete_tagged_brl (brl as (eres, th), (inet, enet)) =
   438   (if eres then
   439     (case try Thm.major_prem_of th of
   440       SOME prem => (inet, Net.delete_term eq_kbrl (prem, ((), brl)) enet)
   441     | NONE => (inet, enet))  (*no major premise: ignore*)
   442   else (Net.delete_term eq_kbrl (Thm.concl_of th, ((), brl)) inet, enet))
   443   handle Net.DELETE => (inet,enet);
   444 
   445 
   446 (*biresolution using a pair of nets rather than rules.
   447     function "order" must sort and possibly filter the list of brls.
   448     boolean "match" indicates matching or unification.*)
   449 fun biresolution_from_nets_tac order match (inet,enet) =
   450   SUBGOAL
   451     (fn (prem,i) =>
   452       let val hyps = Logic.strip_assums_hyp prem
   453           and concl = Logic.strip_assums_concl prem
   454           val kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps
   455       in PRIMSEQ (biresolution match (order kbrls) i) end);
   456 
   457 (*versions taking pre-built nets.  No filtering of brls*)
   458 val biresolve_from_nets_tac = biresolution_from_nets_tac orderlist false;
   459 val bimatch_from_nets_tac   = biresolution_from_nets_tac orderlist true;
   460 
   461 (*fast versions using nets internally*)
   462 val net_biresolve_tac =
   463     biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty);
   464 
   465 val net_bimatch_tac =
   466     bimatch_from_nets_tac o build_netpair(Net.empty,Net.empty);
   467 
   468 (*** Simpler version for resolve_tac -- only one net, and no hyps ***)
   469 
   470 (*insert one tagged rl into the net*)
   471 fun insert_krl (krl as (k,th), net) =
   472     Net.insert_term (K false) (concl_of th, krl) net;
   473 
   474 (*build a net of rules for resolution*)
   475 fun build_net rls =
   476     foldr insert_krl Net.empty (taglist 1 rls);
   477 
   478 (*resolution using a net rather than rules; pred supports filt_resolve_tac*)
   479 fun filt_resolution_from_net_tac match pred net =
   480   SUBGOAL
   481     (fn (prem,i) =>
   482       let val krls = Net.unify_term net (Logic.strip_assums_concl prem)
   483       in
   484          if pred krls
   485          then PRIMSEQ
   486                 (biresolution match (map (pair false) (orderlist krls)) i)
   487          else no_tac
   488       end);
   489 
   490 (*Resolve the subgoal using the rules (making a net) unless too flexible,
   491    which means more than maxr rules are unifiable.      *)
   492 fun filt_resolve_tac rules maxr =
   493     let fun pred krls = length krls <= maxr
   494     in  filt_resolution_from_net_tac false pred (build_net rules)  end;
   495 
   496 (*versions taking pre-built nets*)
   497 val resolve_from_net_tac = filt_resolution_from_net_tac false (K true);
   498 val match_from_net_tac = filt_resolution_from_net_tac true (K true);
   499 
   500 (*fast versions using nets internally*)
   501 val net_resolve_tac = resolve_from_net_tac o build_net;
   502 val net_match_tac = match_from_net_tac o build_net;
   503 
   504 
   505 (*** For Natural Deduction using (bires_flg, rule) pairs ***)
   506 
   507 (*The number of new subgoals produced by the brule*)
   508 fun subgoals_of_brl (true,rule)  = nprems_of rule - 1
   509   | subgoals_of_brl (false,rule) = nprems_of rule;
   510 
   511 (*Less-than test: for sorting to minimize number of new subgoals*)
   512 fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2;
   513 
   514 
   515 (*** Meta-Rewriting Tactics ***)
   516 
   517 val simple_prover =
   518   SINGLE o (fn ss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_ss ss)));
   519 
   520 val rewrite = MetaSimplifier.rewrite_aux simple_prover;
   521 val simplify = MetaSimplifier.simplify_aux simple_prover;
   522 val rewrite_rule = simplify true;
   523 val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
   524 
   525 (*Rewrite throughout proof state. *)
   526 fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
   527 
   528 (*Rewrite subgoals only, not main goal. *)
   529 fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
   530 fun rewtac def = rewrite_goals_tac [def];
   531 
   532 
   533 (*** for folding definitions, handling critical pairs ***)
   534 
   535 (*The depth of nesting in a term*)
   536 fun term_depth (Abs(a,T,t)) = 1 + term_depth t
   537   | term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t)
   538   | term_depth _ = 0;
   539 
   540 val lhs_of_thm = #1 o Logic.dest_equals o prop_of;
   541 
   542 (*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
   543   Returns longest lhs first to avoid folding its subexpressions.*)
   544 fun sort_lhs_depths defs =
   545   let val keylist = AList.make (term_depth o lhs_of_thm) defs
   546       val keys = sort_distinct (rev_order o int_ord) (map #2 keylist)
   547   in map (AList.find (op =) keylist) keys end;
   548 
   549 val rev_defs = sort_lhs_depths o map symmetric;
   550 
   551 fun fold_rule defs = fold rewrite_rule (rev_defs defs);
   552 fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs));
   553 fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
   554 
   555 
   556 (*** Renaming of parameters in a subgoal
   557      Names may contain letters, digits or primes and must be
   558      separated by blanks ***)
   559 
   560 fun rename_params_tac xs i =
   561   case Library.find_first (not o Syntax.is_identifier) xs of
   562       SOME x => error ("Not an identifier: " ^ x)
   563     | NONE =>
   564        (if !Logic.auto_rename
   565          then (warning "Resetting Logic.auto_rename";
   566              Logic.auto_rename := false)
   567         else (); PRIMITIVE (rename_params_rule (xs, i)));
   568 
   569 fun rename_tac str i =
   570   let val cs = Symbol.explode str in
   571   case #2 (take_prefix (Symbol.is_letdig orf Symbol.is_blank) cs) of
   572       [] => rename_params_tac (scanwords Symbol.is_letdig cs) i
   573     | c::_ => error ("Illegal character: " ^ c)
   574   end;
   575 
   576 (*Rename recent parameters using names generated from a and the suffixes,
   577   provided the string a, which represents a term, is an identifier. *)
   578 fun rename_last_tac a sufs i =
   579   let val names = map (curry op^ a) sufs
   580   in  if Syntax.is_identifier a
   581       then PRIMITIVE (rename_params_rule (names,i))
   582       else all_tac
   583   end;
   584 
   585 (*Prunes all redundant parameters from the proof state by rewriting.
   586   DOES NOT rewrite main goal, where quantification over an unused bound
   587     variable is sometimes done to avoid the need for cut_facts_tac.*)
   588 val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
   589 
   590 (*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
   591   right to left if n is positive, and from left to right if n is negative.*)
   592 fun rotate_tac 0 i = all_tac
   593   | rotate_tac k i = PRIMITIVE (rotate_rule k i);
   594 
   595 (*Rotates the given subgoal to be the last.*)
   596 fun defer_tac i = PRIMITIVE (permute_prems (i-1) 1);
   597 
   598 (* remove premises that do not satisfy p; fails if all prems satisfy p *)
   599 fun filter_prems_tac p =
   600   let fun Then NONE tac = SOME tac
   601         | Then (SOME tac) tac' = SOME(tac THEN' tac');
   602       fun thins H (tac,n) =
   603         if p H then (tac,n+1)
   604         else (Then tac (rotate_tac n THEN' etac thin_rl),0);
   605   in SUBGOAL(fn (subg,n) =>
   606        let val Hs = Logic.strip_assums_hyp subg
   607        in case fst(fold thins Hs (NONE,0)) of
   608             NONE => no_tac | SOME tac => tac n
   609        end)
   610   end;
   611 
   612 end;
   613 
   614 structure BasicTactic: BASIC_TACTIC = Tactic;
   615 open BasicTactic;