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