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