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