--- a/src/CTT/CTT.thy Thu Jul 03 15:28:31 2025 +0200
+++ b/src/CTT/CTT.thy Sat Jul 05 14:19:45 2025 +0200
@@ -328,18 +328,18 @@
ML \<open>
fun routine_tac rls ctxt prems =
- ASSUME ctxt (filt_resolve_from_net_tac ctxt 4 (Tactic.build_net (prems @ rls)));
+ ASSUME ctxt (Bires.filt_resolve_from_net_tac ctxt 4 (Bires.build_net (prems @ rls)));
(*Solve all subgoals "A type" using formation rules. *)
-val form_net = Tactic.build_net @{thms form_rls};
+val form_net = Bires.build_net @{thms form_rls};
fun form_tac ctxt =
- REPEAT_FIRST (ASSUME ctxt (filt_resolve_from_net_tac ctxt 1 form_net));
+ REPEAT_FIRST (ASSUME ctxt (Bires.filt_resolve_from_net_tac ctxt 1 form_net));
(*Type checking: solve a:A (a rigid, A flexible) by intro and elim rules. *)
fun typechk_tac ctxt thms =
let val tac =
- filt_resolve_from_net_tac ctxt 3
- (Tactic.build_net (thms @ @{thms form_rls} @ @{thms element_rls}))
+ Bires.filt_resolve_from_net_tac ctxt 3
+ (Bires.build_net (thms @ @{thms form_rls} @ @{thms element_rls}))
in REPEAT_FIRST (ASSUME ctxt tac) end
(*Solve a:A (a flexible, A rigid) by introduction rules.
@@ -347,16 +347,16 @@
goals like ?a:SUM(A,B) have a trivial head-string *)
fun intr_tac ctxt thms =
let val tac =
- filt_resolve_from_net_tac ctxt 1
- (Tactic.build_net (thms @ @{thms form_rls} @ @{thms intr_rls}))
+ Bires.filt_resolve_from_net_tac ctxt 1
+ (Bires.build_net (thms @ @{thms form_rls} @ @{thms intr_rls}))
in REPEAT_FIRST (ASSUME ctxt tac) end
(*Equality proving: solve a=b:A (where a is rigid) by long rules. *)
fun equal_tac ctxt thms =
REPEAT_FIRST
(ASSUME ctxt
- (filt_resolve_from_net_tac ctxt 3
- (Tactic.build_net (thms @ @{thms form_rls element_rls intrL_rls elimL_rls refl_elem}))))
+ (Bires.filt_resolve_from_net_tac ctxt 3
+ (Bires.build_net (thms @ @{thms form_rls element_rls intrL_rls elimL_rls refl_elem}))))
\<close>
method_setup form = \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (form_tac ctxt))\<close>
@@ -391,9 +391,9 @@
ML \<open>
(*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification.
Uses other intro rules to avoid changing flexible goals.*)
-val eqintr_net = Tactic.build_net @{thms EqI intr_rls}
+val eqintr_net = Bires.build_net @{thms EqI intr_rls}
fun eqintr_tac ctxt =
- REPEAT_FIRST (ASSUME ctxt (filt_resolve_from_net_tac ctxt 1 eqintr_net))
+ REPEAT_FIRST (ASSUME ctxt (Bires.filt_resolve_from_net_tac ctxt 1 eqintr_net))
(** Tactics that instantiate CTT-rules.
Vars in the given terms will be incremented!
--- a/src/HOL/Tools/Meson/meson.ML Thu Jul 03 15:28:31 2025 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Sat Jul 05 14:19:45 2025 +0200
@@ -739,7 +739,7 @@
fun prolog_step_tac' ctxt horns =
let val horn0s = (*0 subgoals vs 1 or more*)
take_prefix Thm.no_prems horns
- val nrtac = resolve_from_net_tac ctxt (Tactic.build_net horns)
+ val nrtac = Bires.resolve_from_net_tac ctxt (Bires.build_net horns)
in fn i => eq_assume_tac i ORELSE
match_tac ctxt horn0s i ORELSE (*no backtracking if unit MATCHES*)
((assume_tac ctxt i APPEND nrtac i) THEN check_tac)
--- a/src/HOL/Tools/record.ML Thu Jul 03 15:28:31 2025 +0200
+++ b/src/HOL/Tools/record.ML Sat Jul 05 14:19:45 2025 +0200
@@ -71,7 +71,7 @@
val isoN = "_Tuple_Iso";
val iso_tuple_intro = @{thm isomorphic_tuple_intro};
-val iso_tuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros};
+val iso_tuple_intros = Bires.build_net @{thms isomorphic_tuple.intros};
val tuple_iso_tuple = (\<^const_name>\<open>Record.tuple_iso_tuple\<close>, @{thm tuple_iso_tuple});
@@ -154,7 +154,7 @@
end;
fun iso_tuple_intros_tac ctxt =
- resolve_from_net_tac ctxt iso_tuple_intros THEN'
+ Bires.resolve_from_net_tac ctxt iso_tuple_intros THEN'
CSUBGOAL (fn (cgoal, i) =>
let
val goal = Thm.term_of cgoal;
--- a/src/Provers/classical.ML Thu Jul 03 15:28:31 2025 +0200
+++ b/src/Provers/classical.ML Sat Jul 05 14:19:45 2025 +0200
@@ -273,7 +273,7 @@
fun tag_brls' _ _ [] = []
| tag_brls' w k (brl::brls) = ((w, k), brl) :: tag_brls' w (k + 1) brls;
-fun insert_tagged_list rls = fold_rev Tactic.insert_tagged_brl rls;
+fun insert_tagged_list rls = fold_rev Bires.insert_tagged_brl rls;
(*Insert into netpair that already has nI intr rules and nE elim rules.
Count the intr rules double (to account for swapify). Negate to give the
@@ -281,7 +281,7 @@
fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules;
fun insert' w (nI, nE) = insert_tagged_list o tag_brls' w (~(nI + nE)) o joinrules;
-fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls;
+fun delete_tagged_list rls = fold_rev Bires.delete_tagged_brl rls;
fun delete x = delete_tagged_list (joinrules x);
fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th);
@@ -721,9 +721,9 @@
(FIRST'
[eq_assume_tac,
eq_mp_tac ctxt,
- bimatch_from_nets_tac ctxt safe0_netpair,
+ Bires.bimatch_from_nets_tac ctxt safe0_netpair,
FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs),
- bimatch_from_nets_tac ctxt safep_netpair])
+ Bires.bimatch_from_nets_tac ctxt safep_netpair])
end;
(*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*)
@@ -738,10 +738,10 @@
fun nsubgoalsP n (k, brl) = (subgoals_of_brl brl = n);
-(*version of bimatch_from_nets_tac that only applies rules that
+(*version of Bires.bimatch_from_nets_tac that only applies rules that
create precisely n subgoals.*)
fun n_bimatch_from_nets_tac ctxt n =
- biresolution_from_nets_tac ctxt (order_list o filter (nsubgoalsP n)) true;
+ Bires.biresolution_from_nets_tac ctxt (order_list o filter (nsubgoalsP n)) true;
fun eq_contr_tac ctxt i = ematch_tac ctxt [Data.not_elim] i THEN eq_assume_tac i;
fun eq_assume_contr_tac ctxt = eq_assume_tac ORELSE' eq_contr_tac ctxt;
@@ -757,7 +757,7 @@
appSWrappers ctxt
(FIRST'
[eq_assume_contr_tac ctxt,
- bimatch_from_nets_tac ctxt safe0_netpair,
+ Bires.bimatch_from_nets_tac ctxt safe0_netpair,
FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs),
n_bimatch_from_nets_tac ctxt 1 safep_netpair,
bimatch2_tac ctxt safep_netpair])
@@ -773,17 +773,17 @@
fun inst0_step_tac ctxt =
assume_tac ctxt APPEND'
contr_tac ctxt APPEND'
- biresolve_from_nets_tac ctxt (#safe0_netpair (rep_claset_of ctxt));
+ Bires.biresolve_from_nets_tac ctxt (#safe0_netpair (rep_claset_of ctxt));
(*These unsafe steps could generate more subgoals.*)
fun instp_step_tac ctxt =
- biresolve_from_nets_tac ctxt (#safep_netpair (rep_claset_of ctxt));
+ Bires.biresolve_from_nets_tac ctxt (#safep_netpair (rep_claset_of ctxt));
(*These steps could instantiate variables and are therefore unsafe.*)
fun inst_step_tac ctxt = inst0_step_tac ctxt APPEND' instp_step_tac ctxt;
fun unsafe_step_tac ctxt =
- biresolve_from_nets_tac ctxt (#unsafe_netpair (rep_claset_of ctxt));
+ Bires.biresolve_from_nets_tac ctxt (#unsafe_netpair (rep_claset_of ctxt));
(*Single step for the prover. FAILS unless it makes progress. *)
fun step_tac ctxt i =
@@ -846,7 +846,7 @@
That's hard to implement and did not perform better in experiments, due to
greater search depth required.*)
fun dup_step_tac ctxt =
- biresolve_from_nets_tac ctxt (#dup_netpair (rep_claset_of ctxt));
+ Bires.biresolve_from_nets_tac ctxt (#dup_netpair (rep_claset_of ctxt));
(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)
local
--- a/src/Provers/typedsimp.ML Thu Jul 03 15:28:31 2025 +0200
+++ b/src/Provers/typedsimp.ML Sat Jul 05 14:19:45 2025 +0200
@@ -79,26 +79,26 @@
(*Process the default rewrite rules*)
val simp_rls = process_rewrites default_rls;
-val simp_net = Tactic.build_net simp_rls;
+val simp_net = Bires.build_net simp_rls;
(*If subgoal is too flexible (e.g. ?a=?b or just ?P) then filt_resolve_tac
will fail! The filter will pass all the rules, and the bound permits
no ambiguity.*)
(*Resolution with rewrite/sub rules. Builds the tree for filt_resolve_tac.*)
-fun rewrite_res_tac ctxt = filt_resolve_from_net_tac ctxt 2 simp_net;
+fun rewrite_res_tac ctxt = Bires.filt_resolve_from_net_tac ctxt 2 simp_net;
(*The congruence rules for simplifying subterms. If subgoal is too flexible
then only refl,refl_red will be used (if even them!). *)
fun subconv_res_tac ctxt congr_rls =
- filt_resolve_from_net_tac ctxt 2 (Tactic.build_net (map subconv_rule congr_rls))
- ORELSE' filt_resolve_from_net_tac ctxt 1 (Tactic.build_net [refl, refl_red]);
+ Bires.filt_resolve_from_net_tac ctxt 2 (Bires.build_net (map subconv_rule congr_rls))
+ ORELSE' Bires.filt_resolve_from_net_tac ctxt 1 (Bires.build_net [refl, refl_red]);
(*Resolve with asms, whether rewrites or not*)
fun asm_res_tac ctxt asms =
let val (xsimp_rls, xother_rls) = process_rules asms
in routine_tac ctxt xother_rls ORELSE'
- filt_resolve_from_net_tac ctxt 2 (Tactic.build_net xsimp_rls)
+ Bires.filt_resolve_from_net_tac ctxt 2 (Bires.build_net xsimp_rls)
end;
(*Single step for simple rewriting*)
--- a/src/Pure/Isar/context_rules.ML Thu Jul 03 15:28:31 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML Sat Jul 05 14:19:45 2025 +0200
@@ -81,13 +81,13 @@
val th' = Thm.trim_context th;
in
make_rules (next - 1) ((w, ((i, b), th')) :: rules)
- (nth_map i (Tactic.insert_tagged_brl ((w, next), (b, th'))) netpairs) wrappers
+ (nth_map i (Bires.insert_tagged_brl ((w, next), (b, th'))) netpairs) wrappers
end;
fun del_rule0 th (rs as Rules {next, rules, netpairs, wrappers}) =
let
fun eq_th (_, (_, th')) = Thm.eq_thm_prop (th, th');
- fun del b netpair = Tactic.delete_tagged_brl (b, th) netpair handle Net.DELETE => netpair;
+ fun del b netpair = Bires.delete_tagged_brl (b, th) netpair handle Net.DELETE => netpair;
in
if not (exists eq_th rules) then rs
else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers
@@ -109,7 +109,7 @@
k1 = k2 andalso Thm.eq_thm_prop (th1, th2)) (rules1, rules2);
val next = ~ (length rules);
val netpairs = fold (fn (n, (w, ((i, b), th))) =>
- nth_map i (Tactic.insert_tagged_brl ((w, n), (b, th))))
+ nth_map i (Bires.insert_tagged_brl ((w, n), (b, th))))
(next upto ~1 ~~ rules) empty_netpairs;
in make_rules (next - 1) rules netpairs wrappers end;
);
--- a/src/Pure/ROOT.ML Thu Jul 03 15:28:31 2025 +0200
+++ b/src/Pure/ROOT.ML Sat Jul 05 14:19:45 2025 +0200
@@ -198,6 +198,7 @@
ML_file "tactical.ML";
ML_file "search.ML";
ML_file "tactic.ML";
+ML_file "bires.ML";
ML_file "raw_simplifier.ML";
ML_file "conjunction.ML";
ML_file "assumption.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/bires.ML Sat Jul 05 14:19:45 2025 +0200
@@ -0,0 +1,100 @@
+(* Title: Pure/bires.ML
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+
+Biresolution and resolution using nets.
+*)
+
+signature BIRES =
+sig
+ 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 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
+ val build_net: thm list -> (int * thm) Net.net
+ 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
+end
+
+structure Bires: BIRES =
+struct
+
+(** To preserve the order of the rules, tag them with increasing integers **)
+
+(*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) (Thm.concl_of th, kbrl) inet, enet);
+
+(*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 ctxt order match (inet, enet) =
+ SUBGOAL
+ (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*)
+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;
+
+
+(*** 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) (Thm.concl_of th, krl);
+
+(*build a net of rules for resolution*)
+fun build_net rls =
+ 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 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 (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_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*)
+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);
+
+end;
+
--- a/src/Pure/tactic.ML Thu Jul 03 15:28:31 2025 +0200
+++ b/src/Pure/tactic.ML Sat Jul 05 14:19:45 2025 +0200
@@ -4,7 +4,7 @@
Fundamental tactics.
*)
-signature BASIC_TACTIC =
+signature TACTIC =
sig
val trace_goalno_tac: (int -> tactic) -> int -> tactic
val rule_by_tactic: Proof.context -> tactic -> thm -> thm
@@ -33,15 +33,6 @@
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: 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
@@ -51,19 +42,6 @@
val filter_prems_tac: Proof.context -> (term -> bool) -> int -> tactic
end;
-signature TACTIC =
-sig
- include BASIC_TACTIC
- 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 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
- val build_net: thm list -> (int * thm) Net.net
-end;
-
structure Tactic: TACTIC =
struct
@@ -208,77 +186,6 @@
in filtr(limit,ths) end;
-(*** biresolution and resolution using nets ***)
-
-(** To preserve the order of the rules, tag them with increasing integers **)
-
-(*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) (Thm.concl_of th, kbrl) inet, enet);
-
-(*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 ctxt order match (inet, enet) =
- SUBGOAL
- (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*)
-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;
-
-
-(*** 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) (Thm.concl_of th, krl);
-
-(*build a net of rules for resolution*)
-fun build_net rls =
- 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 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 (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_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*)
-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 ***)
(*The number of new subgoals produced by the brule*)
@@ -325,5 +232,4 @@
end;
-structure Basic_Tactic: BASIC_TACTIC = Tactic;
-open Basic_Tactic;
+open Tactic;
--- a/src/Sequents/modal.ML Thu Jul 03 15:28:31 2025 +0200
+++ b/src/Sequents/modal.ML Sat Jul 05 14:19:45 2025 +0200
@@ -59,8 +59,8 @@
(* NB No back tracking possible with aside rules *)
-val aside_net = Tactic.build_net Modal_Rule.aside_rls;
-fun aside_tac ctxt n = DETERM (REPEAT (filt_resolve_from_net_tac ctxt 999 aside_net n));
+val aside_net = Bires.build_net Modal_Rule.aside_rls;
+fun aside_tac ctxt n = DETERM (REPEAT (Bires.filt_resolve_from_net_tac ctxt 999 aside_net n));
fun rule_tac ctxt rls n = fresolve_tac ctxt rls n THEN aside_tac ctxt n;
fun fres_safe_tac ctxt = fresolve_tac ctxt Modal_Rule.safe_rls;
--- a/src/Tools/intuitionistic.ML Thu Jul 03 15:28:31 2025 +0200
+++ b/src/Tools/intuitionistic.ML Sat Jul 05 14:19:45 2025 +0200
@@ -25,7 +25,7 @@
fun REMDUPS tac ctxt = tac ctxt THEN_ALL_NEW remdups_tac ctxt;
-fun bires_tac ctxt = Tactic.biresolution_from_nets_tac ctxt Context_Rules.orderlist;
+fun bires_tac ctxt = Bires.biresolution_from_nets_tac ctxt Context_Rules.orderlist;
fun safe_step_tac ctxt =
Context_Rules.Swrap ctxt
--- a/src/ZF/Tools/typechk.ML Thu Jul 03 15:28:31 2025 +0200
+++ b/src/ZF/Tools/typechk.ML Sat Jul 05 14:19:45 2025 +0200
@@ -93,13 +93,13 @@
(*Compile a term-net for speed*)
val basic_net =
- Tactic.build_net @{thms TrueI refl reflexive iff_refl ballI allI conjI impI};
+ Bires.build_net @{thms TrueI refl reflexive iff_refl ballI allI conjI impI};
(*Instantiates variables in typing conditions.
drawback: does not simplify conjunctions*)
fun type_solver_tac ctxt hyps = SELECT_GOAL
(DEPTH_SOLVE (eresolve_tac ctxt @{thms FalseE} 1
- ORELSE resolve_from_net_tac ctxt basic_net 1
+ ORELSE Bires.resolve_from_net_tac ctxt basic_net 1
ORELSE (ares_tac ctxt hyps 1
APPEND typecheck_step_tac ctxt)));