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