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