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