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