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