src/Pure/tactic.ML
author wenzelm
Sat Dec 13 15:00:39 2008 +0100 (2008-12-13)
changeset 29091 b81fe045e799
parent 27243 d549b5b0f344
child 29276 94b1ffec9201
permissions -rw-r--r--
Context.display_names;
     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 Basic tactics.
     7 *)
     8 
     9 signature BASIC_TACTIC =
    10 sig
    11   val trace_goalno_tac: (int -> tactic) -> int -> tactic
    12   val rule_by_tactic: tactic -> thm -> thm
    13   val assume_tac: int -> tactic
    14   val eq_assume_tac: int -> tactic
    15   val compose_tac: (bool * thm * int) -> int -> tactic
    16   val make_elim: thm -> thm
    17   val biresolve_tac: (bool * thm) list -> int -> tactic
    18   val resolve_tac: thm list -> int -> tactic
    19   val eresolve_tac: thm list -> int -> tactic
    20   val forward_tac: thm list -> int -> tactic
    21   val dresolve_tac: thm list -> int -> tactic
    22   val atac: int -> tactic
    23   val rtac: thm -> int -> tactic
    24   val dtac: thm -> int ->tactic
    25   val etac: thm -> int ->tactic
    26   val ftac: thm -> int ->tactic
    27   val datac: thm -> int -> int -> tactic
    28   val eatac: thm -> int -> int -> tactic
    29   val fatac: thm -> int -> int -> tactic
    30   val ares_tac: thm list -> int -> tactic
    31   val solve_tac: thm list -> int -> tactic
    32   val bimatch_tac: (bool * thm) list -> int -> tactic
    33   val match_tac: thm list -> int -> tactic
    34   val ematch_tac: thm list -> int -> tactic
    35   val dmatch_tac: thm list -> int -> tactic
    36   val flexflex_tac: tactic
    37   val distinct_subgoal_tac: int -> tactic
    38   val distinct_subgoals_tac: tactic
    39   val metacut_tac: thm -> int -> tactic
    40   val cut_rules_tac: thm list -> int -> tactic
    41   val cut_facts_tac: thm list -> int -> tactic
    42   val filter_thms: (term * term -> bool) -> int * term * thm list -> thm list
    43   val biresolution_from_nets_tac: ('a list -> (bool * thm) list) ->
    44     bool -> 'a Net.net * 'a Net.net -> int -> tactic
    45   val biresolve_from_nets_tac: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net ->
    46     int -> tactic
    47   val bimatch_from_nets_tac: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net ->
    48     int -> tactic
    49   val net_biresolve_tac: (bool * thm) list -> int -> tactic
    50   val net_bimatch_tac: (bool * thm) list -> int -> tactic
    51   val build_net: thm list -> (int * thm) Net.net
    52   val filt_resolve_tac: thm list -> int -> int -> tactic
    53   val resolve_from_net_tac: (int * thm) Net.net -> int -> tactic
    54   val match_from_net_tac: (int * thm) Net.net -> int -> tactic
    55   val net_resolve_tac: thm list -> int -> tactic
    56   val net_match_tac: thm list -> int -> tactic
    57   val subgoals_of_brl: bool * thm -> int
    58   val lessb: (bool * thm) * (bool * thm) -> bool
    59   val rename_tac: string list -> int -> tactic
    60   val rotate_tac: int -> int -> tactic
    61   val defer_tac: int -> tactic
    62   val filter_prems_tac: (term -> bool) -> int -> tactic
    63 end;
    64 
    65 signature TACTIC =
    66 sig
    67   include BASIC_TACTIC
    68   val innermost_params: int -> thm -> (string * typ) list
    69   val term_lift_inst_rule:
    70     thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm -> thm
    71   val untaglist: (int * 'a) list -> 'a list
    72   val orderlist: (int * 'a) list -> 'a list
    73   val insert_tagged_brl: 'a * (bool * thm) ->
    74     ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
    75       ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
    76   val build_netpair: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net ->
    77     (bool * thm) list -> (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net
    78   val delete_tagged_brl: bool * thm ->
    79     ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
    80       ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
    81   val eq_kbrl: ('a * (bool * thm)) * ('a * (bool * thm)) -> bool
    82 end;
    83 
    84 structure Tactic: TACTIC =
    85 struct
    86 
    87 (*Discover which goal is chosen:  SOMEGOAL(trace_goalno_tac tac) *)
    88 fun trace_goalno_tac tac i st =
    89     case Seq.pull(tac i st) of
    90         NONE    => Seq.empty
    91       | seqcell => (tracing ("Subgoal " ^ string_of_int i ^ " selected");
    92                          Seq.make(fn()=> seqcell));
    93 
    94 (*Makes a rule by applying a tactic to an existing rule*)
    95 fun rule_by_tactic tac rl =
    96   let
    97     val ctxt = Variable.thm_context rl;
    98     val ((_, [st]), ctxt') = Variable.import_thms true [rl] ctxt;
    99   in
   100     (case Seq.pull (tac st) of
   101       NONE => raise THM ("rule_by_tactic", 0, [rl])
   102     | SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt' ctxt) st'))
   103   end;
   104 
   105 
   106 (*** Basic tactics ***)
   107 
   108 (*** The following fail if the goal number is out of range:
   109      thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
   110 
   111 (*Solve subgoal i by assumption*)
   112 fun assume_tac i = PRIMSEQ (assumption i);
   113 
   114 (*Solve subgoal i by assumption, using no unification*)
   115 fun eq_assume_tac i = PRIMITIVE (eq_assumption i);
   116 
   117 
   118 (** Resolution/matching tactics **)
   119 
   120 (*The composition rule/state: no lifting or var renaming.
   121   The arg = (bires_flg, orule, m) ;  see bicompose for explanation.*)
   122 fun compose_tac arg i = PRIMSEQ (bicompose false arg i);
   123 
   124 (*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
   125   like [| P&Q; P==>R |] ==> R *)
   126 fun make_elim rl = zero_var_indexes (rl RS revcut_rl);
   127 
   128 (*Attack subgoal i by resolution, using flags to indicate elimination rules*)
   129 fun biresolve_tac brules i = PRIMSEQ (biresolution false brules i);
   130 
   131 (*Resolution: the simple case, works for introduction rules*)
   132 fun resolve_tac rules = biresolve_tac (map (pair false) rules);
   133 
   134 (*Resolution with elimination rules only*)
   135 fun eresolve_tac rules = biresolve_tac (map (pair true) rules);
   136 
   137 (*Forward reasoning using destruction rules.*)
   138 fun forward_tac rls = resolve_tac (map make_elim rls) THEN' assume_tac;
   139 
   140 (*Like forward_tac, but deletes the assumption after use.*)
   141 fun dresolve_tac rls = eresolve_tac (map make_elim rls);
   142 
   143 (*Shorthand versions: for resolution with a single theorem*)
   144 val atac    =   assume_tac;
   145 fun rtac rl =  resolve_tac [rl];
   146 fun dtac rl = dresolve_tac [rl];
   147 fun etac rl = eresolve_tac [rl];
   148 fun ftac rl =  forward_tac [rl];
   149 fun datac thm j = EVERY' (dtac thm::replicate j atac);
   150 fun eatac thm j = EVERY' (etac thm::replicate j atac);
   151 fun fatac thm j = EVERY' (ftac thm::replicate j atac);
   152 
   153 (*Use an assumption or some rules ... A popular combination!*)
   154 fun ares_tac rules = assume_tac  ORELSE'  resolve_tac rules;
   155 
   156 fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac;
   157 
   158 (*Matching tactics -- as above, but forbid updating of state*)
   159 fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i);
   160 fun match_tac rules  = bimatch_tac (map (pair false) rules);
   161 fun ematch_tac rules = bimatch_tac (map (pair true) rules);
   162 fun dmatch_tac rls   = ematch_tac (map make_elim rls);
   163 
   164 (*Smash all flex-flex disagreement pairs in the proof state.*)
   165 val flexflex_tac = PRIMSEQ flexflex_rule;
   166 
   167 (*Remove duplicate subgoals.*)
   168 val perm_tac = PRIMITIVE oo Thm.permute_prems;
   169 
   170 fun distinct_tac (i, k) =
   171   perm_tac 0 (i - 1) THEN
   172   perm_tac 1 (k - 1) THEN
   173   DETERM (PRIMSEQ (fn st =>
   174     Thm.compose_no_flatten false (st, 0) 1
   175       (Drule.incr_indexes st Drule.distinct_prems_rl))) THEN
   176   perm_tac 1 (1 - k) THEN
   177   perm_tac 0 (1 - i);
   178 
   179 fun distinct_subgoal_tac i st =
   180   (case Library.drop (i - 1, Thm.prems_of st) of
   181     [] => no_tac st
   182   | A :: Bs =>
   183       st |> EVERY (fold (fn (B, k) =>
   184         if A aconv B then cons (distinct_tac (i, k)) else I) (Bs ~~ (1 upto length Bs)) []));
   185 
   186 fun distinct_subgoals_tac state =
   187   let
   188     val goals = Thm.prems_of state;
   189     val dups = distinct (eq_fst (op aconv)) (goals ~~ (1 upto length goals));
   190   in EVERY (rev (map (distinct_subgoal_tac o snd) dups)) state end;
   191 
   192 (*Determine print names of goal parameters (reversed)*)
   193 fun innermost_params i st =
   194   let val (_, _, Bi, _) = dest_state (st, i)
   195   in rename_wrt_term Bi (Logic.strip_params Bi) end;
   196 
   197 (*params of subgoal i as they are printed*)
   198 fun params_of_state i st = rev (innermost_params i st);
   199 
   200 (*
   201 Like lift_inst_rule but takes terms, not strings, where the terms may contain
   202 Bounds referring to parameters of the subgoal.
   203 
   204 insts: [...,(vj,tj),...]
   205 
   206 The tj may contain references to parameters of subgoal i of the state st
   207 in the form of Bound k, i.e. the tj may be subterms of the subgoal.
   208 To saturate the lose bound vars, the tj are enclosed in abstractions
   209 corresponding to the parameters of subgoal i, thus turning them into
   210 functions. At the same time, the types of the vj are lifted.
   211 
   212 NB: the types in insts must be correctly instantiated already,
   213     i.e. Tinsts is not applied to insts.
   214 *)
   215 fun term_lift_inst_rule (st, i, Tinsts, insts, rule) =
   216 let
   217     val thy = Thm.theory_of_thm st
   218     val cert = Thm.cterm_of thy
   219     val certT = Thm.ctyp_of thy
   220     val maxidx = Thm.maxidx_of st
   221     val paramTs = map #2 (params_of_state i st)
   222     val inc = maxidx+1
   223     fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
   224     (*lift only Var, not term, which must be lifted already*)
   225     fun liftpair (v,t) = (cert (liftvar v), cert t)
   226     fun liftTpair (((a, i), S), T) =
   227       (certT (TVar ((a, i + inc), S)),
   228        certT (Logic.incr_tvar inc T))
   229 in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
   230                      (Thm.lift_rule (Thm.cprem_of st i) rule)
   231 end;
   232 
   233 
   234 
   235 (*** Applications of cut_rl ***)
   236 
   237 (*The conclusion of the rule gets assumed in subgoal i,
   238   while subgoal i+1,... are the premises of the rule.*)
   239 fun metacut_tac rule i = resolve_tac [cut_rl] i  THEN  biresolve_tac [(false, rule)] (i+1);
   240 
   241 (*"Cut" a list of rules into the goal.  Their premises will become new
   242   subgoals.*)
   243 fun cut_rules_tac ths i = EVERY (map (fn th => metacut_tac th i) ths);
   244 
   245 (*As above, but inserts only facts (unconditional theorems);
   246   generates no additional subgoals. *)
   247 fun cut_facts_tac ths = cut_rules_tac (filter Thm.no_prems ths);
   248 
   249 
   250 (**** Indexing and filtering of theorems ****)
   251 
   252 (*Returns the list of potentially resolvable theorems for the goal "prem",
   253         using the predicate  could(subgoal,concl).
   254   Resulting list is no longer than "limit"*)
   255 fun filter_thms could (limit, prem, ths) =
   256   let val pb = Logic.strip_assums_concl prem;   (*delete assumptions*)
   257       fun filtr (limit, []) = []
   258         | filtr (limit, th::ths) =
   259             if limit=0 then  []
   260             else if could(pb, concl_of th)  then th :: filtr(limit-1, ths)
   261             else filtr(limit,ths)
   262   in  filtr(limit,ths)  end;
   263 
   264 
   265 (*** biresolution and resolution using nets ***)
   266 
   267 (** To preserve the order of the rules, tag them with increasing integers **)
   268 
   269 (*insert tags*)
   270 fun taglist k [] = []
   271   | taglist k (x::xs) = (k,x) :: taglist (k+1) xs;
   272 
   273 (*remove tags and suppress duplicates -- list is assumed sorted!*)
   274 fun untaglist [] = []
   275   | untaglist [(k:int,x)] = [x]
   276   | untaglist ((k,x) :: (rest as (k',x')::_)) =
   277       if k=k' then untaglist rest
   278       else    x :: untaglist rest;
   279 
   280 (*return list elements in original order*)
   281 fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls);
   282 
   283 (*insert one tagged brl into the pair of nets*)
   284 fun insert_tagged_brl (kbrl as (k, (eres, th))) (inet, enet) =
   285   if eres then
   286     (case try Thm.major_prem_of th of
   287       SOME prem => (inet, Net.insert_term (K false) (prem, kbrl) enet)
   288     | NONE => error "insert_tagged_brl: elimination rule with no premises")
   289   else (Net.insert_term (K false) (concl_of th, kbrl) inet, enet);
   290 
   291 (*build a pair of nets for biresolution*)
   292 fun build_netpair netpair brls =
   293     fold_rev insert_tagged_brl (taglist 1 brls) netpair;
   294 
   295 (*delete one kbrl from the pair of nets*)
   296 fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
   297 
   298 fun delete_tagged_brl (brl as (eres, th)) (inet, enet) =
   299   (if eres then
   300     (case try Thm.major_prem_of th of
   301       SOME prem => (inet, Net.delete_term eq_kbrl (prem, ((), brl)) enet)
   302     | NONE => (inet, enet))  (*no major premise: ignore*)
   303   else (Net.delete_term eq_kbrl (Thm.concl_of th, ((), brl)) inet, enet))
   304   handle Net.DELETE => (inet,enet);
   305 
   306 
   307 (*biresolution using a pair of nets rather than rules.
   308     function "order" must sort and possibly filter the list of brls.
   309     boolean "match" indicates matching or unification.*)
   310 fun biresolution_from_nets_tac order match (inet,enet) =
   311   SUBGOAL
   312     (fn (prem,i) =>
   313       let val hyps = Logic.strip_assums_hyp prem
   314           and concl = Logic.strip_assums_concl prem
   315           val kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps
   316       in PRIMSEQ (biresolution match (order kbrls) i) end);
   317 
   318 (*versions taking pre-built nets.  No filtering of brls*)
   319 val biresolve_from_nets_tac = biresolution_from_nets_tac orderlist false;
   320 val bimatch_from_nets_tac   = biresolution_from_nets_tac orderlist true;
   321 
   322 (*fast versions using nets internally*)
   323 val net_biresolve_tac =
   324     biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty);
   325 
   326 val net_bimatch_tac =
   327     bimatch_from_nets_tac o build_netpair(Net.empty,Net.empty);
   328 
   329 (*** Simpler version for resolve_tac -- only one net, and no hyps ***)
   330 
   331 (*insert one tagged rl into the net*)
   332 fun insert_krl (krl as (k,th)) =
   333   Net.insert_term (K false) (concl_of th, krl);
   334 
   335 (*build a net of rules for resolution*)
   336 fun build_net rls =
   337   fold_rev insert_krl (taglist 1 rls) Net.empty;
   338 
   339 (*resolution using a net rather than rules; pred supports filt_resolve_tac*)
   340 fun filt_resolution_from_net_tac match pred net =
   341   SUBGOAL
   342     (fn (prem,i) =>
   343       let val krls = Net.unify_term net (Logic.strip_assums_concl prem)
   344       in
   345          if pred krls
   346          then PRIMSEQ
   347                 (biresolution match (map (pair false) (orderlist krls)) i)
   348          else no_tac
   349       end);
   350 
   351 (*Resolve the subgoal using the rules (making a net) unless too flexible,
   352    which means more than maxr rules are unifiable.      *)
   353 fun filt_resolve_tac rules maxr =
   354     let fun pred krls = length krls <= maxr
   355     in  filt_resolution_from_net_tac false pred (build_net rules)  end;
   356 
   357 (*versions taking pre-built nets*)
   358 val resolve_from_net_tac = filt_resolution_from_net_tac false (K true);
   359 val match_from_net_tac = filt_resolution_from_net_tac true (K true);
   360 
   361 (*fast versions using nets internally*)
   362 val net_resolve_tac = resolve_from_net_tac o build_net;
   363 val net_match_tac = match_from_net_tac o build_net;
   364 
   365 
   366 (*** For Natural Deduction using (bires_flg, rule) pairs ***)
   367 
   368 (*The number of new subgoals produced by the brule*)
   369 fun subgoals_of_brl (true,rule)  = nprems_of rule - 1
   370   | subgoals_of_brl (false,rule) = nprems_of rule;
   371 
   372 (*Less-than test: for sorting to minimize number of new subgoals*)
   373 fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2;
   374 
   375 
   376 (*Renaming of parameters in a subgoal*)
   377 fun rename_tac xs i =
   378   case Library.find_first (not o Syntax.is_identifier) xs of
   379       SOME x => error ("Not an identifier: " ^ x)
   380     | NONE => PRIMITIVE (rename_params_rule (xs, i));
   381 
   382 (*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
   383   right to left if n is positive, and from left to right if n is negative.*)
   384 fun rotate_tac 0 i = all_tac
   385   | rotate_tac k i = PRIMITIVE (rotate_rule k i);
   386 
   387 (*Rotates the given subgoal to be the last.*)
   388 fun defer_tac i = PRIMITIVE (permute_prems (i-1) 1);
   389 
   390 (* remove premises that do not satisfy p; fails if all prems satisfy p *)
   391 fun filter_prems_tac p =
   392   let fun Then NONE tac = SOME tac
   393         | Then (SOME tac) tac' = SOME(tac THEN' tac');
   394       fun thins H (tac,n) =
   395         if p H then (tac,n+1)
   396         else (Then tac (rotate_tac n THEN' etac thin_rl),0);
   397   in SUBGOAL(fn (subg,n) =>
   398        let val Hs = Logic.strip_assums_hyp subg
   399        in case fst(fold thins Hs (NONE,0)) of
   400             NONE => no_tac | SOME tac => tac n
   401        end)
   402   end;
   403 
   404 end;
   405 
   406 structure BasicTactic: BASIC_TACTIC = Tactic;
   407 open BasicTactic;