# HG changeset patch # User wenzelm # Date 1751717985 -7200 # Node ID 61aae966dd957684c9b4d4a842b99010f32e638f # Parent 070585eb5d5441fc4c641eb8b58c85cf2956359e clarified modules: explicit structure Bires; diff -r 070585eb5d54 -r 61aae966dd95 src/CTT/CTT.thy --- 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 \ 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})))) \ method_setup form = \Scan.succeed (fn ctxt => SIMPLE_METHOD (form_tac ctxt))\ @@ -391,9 +391,9 @@ ML \ (*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! diff -r 070585eb5d54 -r 61aae966dd95 src/HOL/Tools/Meson/meson.ML --- 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) diff -r 070585eb5d54 -r 61aae966dd95 src/HOL/Tools/record.ML --- 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>\Record.tuple_iso_tuple\, @{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; diff -r 070585eb5d54 -r 61aae966dd95 src/Provers/classical.ML --- 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 diff -r 070585eb5d54 -r 61aae966dd95 src/Provers/typedsimp.ML --- 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*) diff -r 070585eb5d54 -r 61aae966dd95 src/Pure/Isar/context_rules.ML --- 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; ); diff -r 070585eb5d54 -r 61aae966dd95 src/Pure/ROOT.ML --- 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"; diff -r 070585eb5d54 -r 61aae966dd95 src/Pure/bires.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; + diff -r 070585eb5d54 -r 61aae966dd95 src/Pure/tactic.ML --- 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; diff -r 070585eb5d54 -r 61aae966dd95 src/Sequents/modal.ML --- 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; diff -r 070585eb5d54 -r 61aae966dd95 src/Tools/intuitionistic.ML --- 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 diff -r 070585eb5d54 -r 61aae966dd95 src/ZF/Tools/typechk.ML --- 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)));