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