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