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