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