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