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