--- a/src/Pure/tactic.ML Sat Dec 20 19:12:41 2014 +0100
+++ b/src/Pure/tactic.ML Sat Dec 20 22:23:37 2014 +0100
@@ -35,19 +35,15 @@
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 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 biresolution_from_nets_tac: Proof.context ->
+ ('a list -> (bool * thm) list) -> bool -> 'a Net.net * 'a Net.net -> int -> tactic
+ val biresolve_from_nets_tac: Proof.context ->
+ (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net -> int -> tactic
+ val bimatch_from_nets_tac: Proof.context ->
+ (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net -> int -> tactic
+ val filt_resolve_from_net_tac: Proof.context -> int -> (int * thm) Net.net -> int -> tactic
+ val resolve_from_net_tac: Proof.context -> (int * thm) Net.net -> int -> tactic
+ val match_from_net_tac: Proof.context -> (int * thm) Net.net -> int -> tactic
val subgoals_of_brl: bool * thm -> int
val lessb: (bool * thm) * (bool * thm) -> bool
val rename_tac: string list -> int -> tactic
@@ -63,8 +59,6 @@
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
@@ -219,10 +213,6 @@
| 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 (tag_list 1 brls) netpair;
-
(*delete one kbrl from the pair of nets*)
fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
@@ -238,24 +228,19 @@
(*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) =
+fun biresolution_from_nets_tac ctxt 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 (Thm.biresolution NONE match (order kbrls) i) end);
+ (fn (prem, i) =>
+ let
+ val hyps = Logic.strip_assums_hyp prem;
+ val concl = Logic.strip_assums_concl prem;
+ val kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps;
+ in PRIMSEQ (Thm.biresolution (SOME ctxt) match (order kbrls) i) end);
(*versions taking pre-built nets. No filtering of brls*)
-val biresolve_from_nets_tac = biresolution_from_nets_tac order_list false;
-val bimatch_from_nets_tac = biresolution_from_nets_tac order_list true;
+fun biresolve_from_nets_tac ctxt = biresolution_from_nets_tac ctxt order_list false;
+fun bimatch_from_nets_tac ctxt = biresolution_from_nets_tac ctxt order_list 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 ***)
@@ -268,27 +253,23 @@
fold_rev insert_krl (tag_list 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) =>
+fun filt_resolution_from_net_tac ctxt 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 (Thm.biresolution NONE match (map (pair false) (order_list krls)) i)
+ PRIMSEQ (Thm.biresolution (SOME ctxt) match (map (pair false) (order_list 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;
+fun filt_resolve_from_net_tac ctxt maxr net =
+ let fun pred krls = length krls <= maxr
+ in filt_resolution_from_net_tac ctxt false pred net 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;
+fun resolve_from_net_tac ctxt = filt_resolution_from_net_tac ctxt false (K true);
+fun match_from_net_tac ctxt = filt_resolution_from_net_tac ctxt true (K true);
(*** For Natural Deduction using (bires_flg, rule) pairs ***)