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