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