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