(* Title: Pure/tactic.ML
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Fundamental tactics.
*)
signature BASIC_TACTIC =
sig
val trace_goalno_tac: (int -> tactic) -> int -> tactic
val rule_by_tactic: tactic -> thm -> thm
val assume_tac: int -> tactic
val eq_assume_tac: int -> tactic
val compose_tac: (bool * thm * int) -> int -> tactic
val make_elim: thm -> thm
val biresolve_tac: (bool * thm) list -> int -> tactic
val resolve_tac: thm list -> int -> tactic
val eresolve_tac: thm list -> int -> tactic
val forward_tac: thm list -> int -> tactic
val dresolve_tac: thm list -> int -> tactic
val atac: int -> tactic
val rtac: thm -> int -> tactic
val dtac: thm -> int ->tactic
val etac: thm -> int ->tactic
val ftac: thm -> int ->tactic
val datac: thm -> int -> int -> tactic
val eatac: thm -> int -> int -> tactic
val fatac: thm -> int -> int -> tactic
val ares_tac: thm list -> int -> tactic
val solve_tac: thm list -> int -> tactic
val bimatch_tac: (bool * thm) list -> int -> tactic
val match_tac: thm list -> int -> tactic
val ematch_tac: thm list -> int -> tactic
val dmatch_tac: thm list -> int -> tactic
val flexflex_tac: tactic
val distinct_subgoal_tac: int -> tactic
val distinct_subgoals_tac: tactic
val metacut_tac: thm -> int -> tactic
val cut_rules_tac: thm list -> int -> tactic
val cut_facts_tac: thm list -> int -> tactic
val filter_thms: (term * term -> bool) -> int * term * thm list -> thm list
val biresolution_from_nets_tac: ('a list -> (bool * thm) list) ->
bool -> 'a Net.net * 'a Net.net -> int -> tactic
val biresolve_from_nets_tac: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net ->
int -> tactic
val bimatch_from_nets_tac: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net ->
int -> tactic
val net_biresolve_tac: (bool * thm) list -> int -> tactic
val net_bimatch_tac: (bool * thm) list -> int -> tactic
val build_net: thm list -> (int * thm) Net.net
val filt_resolve_tac: thm list -> int -> int -> tactic
val resolve_from_net_tac: (int * thm) Net.net -> int -> tactic
val match_from_net_tac: (int * thm) Net.net -> int -> tactic
val net_resolve_tac: thm list -> int -> tactic
val net_match_tac: thm list -> int -> tactic
val subgoals_of_brl: bool * thm -> int
val lessb: (bool * thm) * (bool * thm) -> bool
val rename_tac: string list -> int -> tactic
val rotate_tac: int -> int -> tactic
val defer_tac: int -> tactic
val filter_prems_tac: (term -> bool) -> int -> tactic
end;
signature TACTIC =
sig
include BASIC_TACTIC
val innermost_params: int -> thm -> (string * typ) list
val term_lift_inst_rule:
thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm -> thm
val untaglist: (int * 'a) list -> 'a list
val orderlist: (int * 'a) list -> 'a list
val insert_tagged_brl: 'a * (bool * thm) ->
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
val build_netpair: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net ->
(bool * thm) list -> (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net
val delete_tagged_brl: bool * thm ->
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
val eq_kbrl: ('a * (bool * thm)) * ('a * (bool * thm)) -> bool
end;
structure Tactic: TACTIC =
struct
(*Discover which goal is chosen: SOMEGOAL(trace_goalno_tac tac) *)
fun trace_goalno_tac tac i st =
case Seq.pull(tac i st) of
NONE => Seq.empty
| seqcell => (tracing ("Subgoal " ^ string_of_int i ^ " selected");
Seq.make(fn()=> seqcell));
(*Makes a rule by applying a tactic to an existing rule*)
fun rule_by_tactic tac rl =
let
val ctxt = Variable.thm_context rl;
val ((_, [st]), ctxt') = Variable.import_thms true [rl] ctxt;
in
(case Seq.pull (tac st) of
NONE => raise THM ("rule_by_tactic", 0, [rl])
| SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt' ctxt) st'))
end;
(*** Basic tactics ***)
(*** The following fail if the goal number is out of range:
thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
(*Solve subgoal i by assumption*)
fun assume_tac i = PRIMSEQ (assumption i);
(*Solve subgoal i by assumption, using no unification*)
fun eq_assume_tac i = PRIMITIVE (eq_assumption i);
(** Resolution/matching tactics **)
(*The composition rule/state: no lifting or var renaming.
The arg = (bires_flg, orule, m) ; see bicompose for explanation.*)
fun compose_tac arg i = PRIMSEQ (bicompose false arg i);
(*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
like [| P&Q; P==>R |] ==> R *)
fun make_elim rl = zero_var_indexes (rl RS revcut_rl);
(*Attack subgoal i by resolution, using flags to indicate elimination rules*)
fun biresolve_tac brules i = PRIMSEQ (biresolution false brules i);
(*Resolution: the simple case, works for introduction rules*)
fun resolve_tac rules = biresolve_tac (map (pair false) rules);
(*Resolution with elimination rules only*)
fun eresolve_tac rules = biresolve_tac (map (pair true) rules);
(*Forward reasoning using destruction rules.*)
fun forward_tac rls = resolve_tac (map make_elim rls) THEN' assume_tac;
(*Like forward_tac, but deletes the assumption after use.*)
fun dresolve_tac rls = eresolve_tac (map make_elim rls);
(*Shorthand versions: for resolution with a single theorem*)
val atac = assume_tac;
fun rtac rl = resolve_tac [rl];
fun dtac rl = dresolve_tac [rl];
fun etac rl = eresolve_tac [rl];
fun ftac rl = forward_tac [rl];
fun datac thm j = EVERY' (dtac thm::replicate j atac);
fun eatac thm j = EVERY' (etac thm::replicate j atac);
fun fatac thm j = EVERY' (ftac thm::replicate j atac);
(*Use an assumption or some rules ... A popular combination!*)
fun ares_tac rules = assume_tac ORELSE' resolve_tac rules;
fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac;
(*Matching tactics -- as above, but forbid updating of state*)
fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i);
fun match_tac rules = bimatch_tac (map (pair false) rules);
fun ematch_tac rules = bimatch_tac (map (pair true) rules);
fun dmatch_tac rls = ematch_tac (map make_elim rls);
(*Smash all flex-flex disagreement pairs in the proof state.*)
val flexflex_tac = PRIMSEQ flexflex_rule;
(*Remove duplicate subgoals.*)
val perm_tac = PRIMITIVE oo Thm.permute_prems;
fun distinct_tac (i, k) =
perm_tac 0 (i - 1) THEN
perm_tac 1 (k - 1) THEN
DETERM (PRIMSEQ (fn st =>
Thm.compose_no_flatten false (st, 0) 1
(Drule.incr_indexes st Drule.distinct_prems_rl))) THEN
perm_tac 1 (1 - k) THEN
perm_tac 0 (1 - i);
fun distinct_subgoal_tac i st =
(case Library.drop (i - 1, Thm.prems_of st) of
[] => no_tac st
| A :: Bs =>
st |> EVERY (fold (fn (B, k) =>
if A aconv B then cons (distinct_tac (i, k)) else I) (Bs ~~ (1 upto length Bs)) []));
fun distinct_subgoals_tac state =
let
val goals = Thm.prems_of state;
val dups = distinct (eq_fst (op aconv)) (goals ~~ (1 upto length goals));
in EVERY (rev (map (distinct_subgoal_tac o snd) dups)) state end;
(*Determine print names of goal parameters (reversed)*)
fun innermost_params i st =
let val (_, _, Bi, _) = dest_state (st, i)
in Term.rename_wrt_term Bi (Logic.strip_params Bi) end;
(*params of subgoal i as they are printed*)
fun params_of_state i st = rev (innermost_params i st);
(*
Like lift_inst_rule but takes terms, not strings, where the terms may contain
Bounds referring to parameters of the subgoal.
insts: [...,(vj,tj),...]
The tj may contain references to parameters of subgoal i of the state st
in the form of Bound k, i.e. the tj may be subterms of the subgoal.
To saturate the lose bound vars, the tj are enclosed in abstractions
corresponding to the parameters of subgoal i, thus turning them into
functions. At the same time, the types of the vj are lifted.
NB: the types in insts must be correctly instantiated already,
i.e. Tinsts is not applied to insts.
*)
fun term_lift_inst_rule (st, i, Tinsts, insts, rule) =
let
val thy = Thm.theory_of_thm st
val cert = Thm.cterm_of thy
val certT = Thm.ctyp_of thy
val maxidx = Thm.maxidx_of st
val paramTs = map #2 (params_of_state i st)
val inc = maxidx+1
fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
(*lift only Var, not term, which must be lifted already*)
fun liftpair (v,t) = (cert (liftvar v), cert t)
fun liftTpair (((a, i), S), T) =
(certT (TVar ((a, i + inc), S)),
certT (Logic.incr_tvar inc T))
in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
(Thm.lift_rule (Thm.cprem_of st i) rule)
end;
(*** Applications of cut_rl ***)
(*The conclusion of the rule gets assumed in subgoal i,
while subgoal i+1,... are the premises of the rule.*)
fun metacut_tac rule i = resolve_tac [cut_rl] i THEN biresolve_tac [(false, rule)] (i+1);
(*"Cut" a list of rules into the goal. Their premises will become new
subgoals.*)
fun cut_rules_tac ths i = EVERY (map (fn th => metacut_tac th i) ths);
(*As above, but inserts only facts (unconditional theorems);
generates no additional subgoals. *)
fun cut_facts_tac ths = cut_rules_tac (filter Thm.no_prems ths);
(**** Indexing and filtering of theorems ****)
(*Returns the list of potentially resolvable theorems for the goal "prem",
using the predicate could(subgoal,concl).
Resulting list is no longer than "limit"*)
fun filter_thms could (limit, prem, ths) =
let val pb = Logic.strip_assums_concl prem; (*delete assumptions*)
fun filtr (limit, []) = []
| filtr (limit, th::ths) =
if limit=0 then []
else if could(pb, concl_of th) then th :: filtr(limit-1, ths)
else filtr(limit,ths)
in filtr(limit,ths) end;
(*** biresolution and resolution using nets ***)
(** To preserve the order of the rules, tag them with increasing integers **)
(*insert tags*)
fun taglist k [] = []
| taglist k (x::xs) = (k,x) :: taglist (k+1) xs;
(*remove tags and suppress duplicates -- list is assumed sorted!*)
fun untaglist [] = []
| untaglist [(k:int,x)] = [x]
| untaglist ((k,x) :: (rest as (k',x')::_)) =
if k=k' then untaglist rest
else x :: untaglist rest;
(*return list elements in original order*)
fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls);
(*insert one tagged brl into the pair of nets*)
fun insert_tagged_brl (kbrl as (k, (eres, th))) (inet, enet) =
if eres then
(case try Thm.major_prem_of th of
SOME prem => (inet, Net.insert_term (K false) (prem, kbrl) enet)
| NONE => error "insert_tagged_brl: elimination rule with no premises")
else (Net.insert_term (K false) (concl_of th, kbrl) inet, enet);
(*build a pair of nets for biresolution*)
fun build_netpair netpair brls =
fold_rev insert_tagged_brl (taglist 1 brls) netpair;
(*delete one kbrl from the pair of nets*)
fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
fun delete_tagged_brl (brl as (eres, th)) (inet, enet) =
(if eres then
(case try Thm.major_prem_of th of
SOME prem => (inet, Net.delete_term eq_kbrl (prem, ((), brl)) enet)
| NONE => (inet, enet)) (*no major premise: ignore*)
else (Net.delete_term eq_kbrl (Thm.concl_of th, ((), brl)) inet, enet))
handle Net.DELETE => (inet,enet);
(*biresolution using a pair of nets rather than rules.
function "order" must sort and possibly filter the list of brls.
boolean "match" indicates matching or unification.*)
fun biresolution_from_nets_tac order match (inet,enet) =
SUBGOAL
(fn (prem,i) =>
let val hyps = Logic.strip_assums_hyp prem
and concl = Logic.strip_assums_concl prem
val kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps
in PRIMSEQ (biresolution match (order kbrls) i) end);
(*versions taking pre-built nets. No filtering of brls*)
val biresolve_from_nets_tac = biresolution_from_nets_tac orderlist false;
val bimatch_from_nets_tac = biresolution_from_nets_tac orderlist true;
(*fast versions using nets internally*)
val net_biresolve_tac =
biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty);
val net_bimatch_tac =
bimatch_from_nets_tac o build_netpair(Net.empty,Net.empty);
(*** Simpler version for resolve_tac -- only one net, and no hyps ***)
(*insert one tagged rl into the net*)
fun insert_krl (krl as (k,th)) =
Net.insert_term (K false) (concl_of th, krl);
(*build a net of rules for resolution*)
fun build_net rls =
fold_rev insert_krl (taglist 1 rls) Net.empty;
(*resolution using a net rather than rules; pred supports filt_resolve_tac*)
fun filt_resolution_from_net_tac match pred net =
SUBGOAL
(fn (prem,i) =>
let val krls = Net.unify_term net (Logic.strip_assums_concl prem)
in
if pred krls
then PRIMSEQ
(biresolution match (map (pair false) (orderlist krls)) i)
else no_tac
end);
(*Resolve the subgoal using the rules (making a net) unless too flexible,
which means more than maxr rules are unifiable. *)
fun filt_resolve_tac rules maxr =
let fun pred krls = length krls <= maxr
in filt_resolution_from_net_tac false pred (build_net rules) end;
(*versions taking pre-built nets*)
val resolve_from_net_tac = filt_resolution_from_net_tac false (K true);
val match_from_net_tac = filt_resolution_from_net_tac true (K true);
(*fast versions using nets internally*)
val net_resolve_tac = resolve_from_net_tac o build_net;
val net_match_tac = match_from_net_tac o build_net;
(*** For Natural Deduction using (bires_flg, rule) pairs ***)
(*The number of new subgoals produced by the brule*)
fun subgoals_of_brl (true,rule) = nprems_of rule - 1
| subgoals_of_brl (false,rule) = nprems_of rule;
(*Less-than test: for sorting to minimize number of new subgoals*)
fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2;
(*Renaming of parameters in a subgoal*)
fun rename_tac xs i =
case Library.find_first (not o Syntax.is_identifier) xs of
SOME x => error ("Not an identifier: " ^ x)
| NONE => PRIMITIVE (rename_params_rule (xs, i));
(*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
right to left if n is positive, and from left to right if n is negative.*)
fun rotate_tac 0 i = all_tac
| rotate_tac k i = PRIMITIVE (rotate_rule k i);
(*Rotates the given subgoal to be the last.*)
fun defer_tac i = PRIMITIVE (permute_prems (i-1) 1);
(* remove premises that do not satisfy p; fails if all prems satisfy p *)
fun filter_prems_tac p =
let fun Then NONE tac = SOME tac
| Then (SOME tac) tac' = SOME(tac THEN' tac');
fun thins H (tac,n) =
if p H then (tac,n+1)
else (Then tac (rotate_tac n THEN' etac thin_rl),0);
in SUBGOAL(fn (subg,n) =>
let val Hs = Logic.strip_assums_hyp subg
in case fst(fold thins Hs (NONE,0)) of
NONE => no_tac | SOME tac => tac n
end)
end;
end;
structure BasicTactic: BASIC_TACTIC = Tactic;
open BasicTactic;