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