# HG changeset patch # User wenzelm # Date 1751808419 -7200 # Node ID ae85cd17ffbe77f6e3a039ac341a669df32b4229 # Parent 982e7128ce0f5d3f9117b8a4e15a42147119b1c3# Parent f7a6b012600e5b092d739143b56e7f80b60ad8da merged diff -r 982e7128ce0f -r ae85cd17ffbe src/CTT/CTT.thy --- a/src/CTT/CTT.thy Fri Jul 04 15:08:09 2025 +0100 +++ b/src/CTT/CTT.thy Sun Jul 06 15:26:59 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! @@ -421,7 +421,7 @@ fun mp_tac ctxt i = eresolve_tac ctxt @{thms subst_prodE} i THEN assume_tac ctxt i (*"safe" when regarded as predicate calculus rules*) -val safe_brls = sort (make_ord lessb) +val safe_brls = sort Bires.subgoals_ord [ (true, @{thm FE}), (true,asm_rl), (false, @{thm ProdI}), (true, @{thm SumE}), (true, @{thm PlusE}) ] @@ -431,7 +431,7 @@ (*0 subgoals vs 1 or more*) val (safe0_brls, safep_brls) = - List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls + List.partition Bires.no_subgoals safe_brls fun safestep_tac ctxt thms i = form_tac ctxt ORELSE diff -r 982e7128ce0f -r ae85cd17ffbe src/FOL/ex/Prolog.thy --- a/src/FOL/ex/Prolog.thy Fri Jul 04 15:08:09 2025 +0100 +++ b/src/FOL/ex/Prolog.thy Sun Jul 06 15:26:59 2025 +0200 @@ -64,7 +64,7 @@ (*backtracking version*) ML \ fun prolog_tac ctxt = - DEPTH_FIRST (has_fewer_prems 1) (resolve_tac ctxt @{thms rules} 1) + DEPTH_FIRST Thm.no_prems (resolve_tac ctxt @{thms rules} 1) \ schematic_goal \rev(?x, a:b:c:Nil)\ diff -r 982e7128ce0f -r ae85cd17ffbe src/FOL/intprover.ML --- a/src/FOL/intprover.ML Fri Jul 04 15:08:09 2025 +0100 +++ b/src/FOL/intprover.ML Sun Jul 06 15:26:59 2025 +0200 @@ -39,7 +39,7 @@ (handles double negations). Could instead rewrite by not_def as the first step of an intuitionistic proof. *) -val safe_brls = sort (make_ord lessb) +val safe_brls = sort Bires.subgoals_ord [ (true, @{thm FalseE}), (false, @{thm TrueI}), (false, @{thm refl}), (false, @{thm impI}), (false, @{thm notI}), (false, @{thm allI}), (true, @{thm conjE}), (true, @{thm exE}), @@ -59,7 +59,7 @@ (*0 subgoals vs 1 or more: the p in safep is for positive*) val (safe0_brls, safep_brls) = - List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls; + List.partition Bires.no_subgoals safe_brls; (*Attack subgoals using safe inferences -- matching, not resolution*) fun safe_step_tac ctxt = @@ -90,11 +90,11 @@ (*Slower but smarter than fast_tac*) fun best_tac ctxt = - SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1)); + SELECT_GOAL (BEST_FIRST (Thm.no_prems, size_of_thm) (step_tac ctxt 1)); (*Uses all_dupE: allows multiple use of universal assumptions. VERY slow.*) fun best_dup_tac ctxt = - SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_dup_tac ctxt 1)); + SELECT_GOAL (BEST_FIRST (Thm.no_prems, size_of_thm) (step_dup_tac ctxt 1)); end; diff -r 982e7128ce0f -r ae85cd17ffbe src/FOLP/classical.ML --- a/src/FOLP/classical.ML Fri Jul 04 15:08:09 2025 +0100 +++ b/src/FOLP/classical.ML Sun Jul 06 15:26:59 2025 +0200 @@ -111,11 +111,11 @@ (*Note that allE precedes exI in haz_brls*) fun make_cs {safeIs,safeEs,hazIs,hazEs} = let val (safe0_brls, safep_brls) = (*0 subgoals vs 1 or more*) - List.partition (curry (op =) 0 o subgoals_of_brl) - (sort (make_ord lessb) (joinrules(safeIs, safeEs))) + List.partition Bires.no_subgoals + (sort Bires.subgoals_ord (joinrules(safeIs, safeEs))) in CS{safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs, safe0_brls=safe0_brls, safep_brls=safep_brls, - haz_brls = sort (make_ord lessb) (joinrules(hazIs, hazEs))} + haz_brls = sort Bires.subgoals_ord (joinrules(hazIs, hazEs))} end; (*** Manipulation of clasets ***) @@ -174,7 +174,7 @@ (*Slower but smarter than fast_tac*) fun best_tac ctxt cs = - SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac ctxt cs 1)); + SELECT_GOAL (BEST_FIRST (Thm.no_prems, sizef) (step_tac ctxt cs 1)); (*Using a "safe" rule to instantiate variables is unsafe. This tactic allows backtracking from "safe" rules to "unsafe" rules here.*) diff -r 982e7128ce0f -r ae85cd17ffbe src/FOLP/intprover.ML --- a/src/FOLP/intprover.ML Fri Jul 04 15:08:09 2025 +0100 +++ b/src/FOLP/intprover.ML Sun Jul 06 15:26:59 2025 +0200 @@ -34,7 +34,7 @@ (handles double negations). Could instead rewrite by not_def as the first step of an intuitionistic proof. *) -val safe_brls = sort (make_ord lessb) +val safe_brls = sort Bires.subgoals_ord [ (true, @{thm FalseE}), (false, @{thm TrueI}), (false, @{thm refl}), (false, @{thm impI}), (false, @{thm notI}), (false, @{thm allI}), (true, @{thm conjE}), (true, @{thm exE}), @@ -49,7 +49,7 @@ (*0 subgoals vs 1 or more: the p in safep is for positive*) val (safe0_brls, safep_brls) = - List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls; + List.partition Bires.no_subgoals safe_brls; (*Attack subgoals using safe inferences*) fun safe_step_tac ctxt = FIRST' [uniq_assume_tac ctxt, @@ -72,6 +72,6 @@ (*Slower but smarter than fast_tac*) fun best_tac ctxt = - SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1)); + SELECT_GOAL (BEST_FIRST (Thm.no_prems, size_of_thm) (step_tac ctxt 1)); end; diff -r 982e7128ce0f -r ae85cd17ffbe src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Fri Jul 04 15:08:09 2025 +0100 +++ b/src/HOL/Nominal/nominal_datatype.ML Sun Jul 06 15:26:59 2025 +0200 @@ -588,7 +588,7 @@ (fn ctxt => resolve_tac ctxt [exI] 1 THEN resolve_tac ctxt @{thms CollectI} 1 THEN - QUIET_BREADTH_FIRST (has_fewer_prems 1) + QUIET_BREADTH_FIRST Thm.no_prems (resolve_tac ctxt rep_intrs 1))) thy |> (fn ((_, r), thy) => let val permT = mk_permT diff -r 982e7128ce0f -r ae85cd17ffbe src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Fri Jul 04 15:08:09 2025 +0100 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Sun Jul 06 15:26:59 2025 +0200 @@ -603,7 +603,7 @@ val pulled_tac_result = Seq.pull tac_result val tac_failed = is_none pulled_tac_result orelse - not (has_fewer_prems 1 (fst (the pulled_tac_result))) + not (Thm.no_prems (fst (the pulled_tac_result))) in if tac_failed then (wittler THEN' ASAP wittler tac) i st else tac_result diff -r 982e7128ce0f -r ae85cd17ffbe src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Fri Jul 04 15:08:09 2025 +0100 +++ b/src/HOL/Tools/Meson/meson.ML Sun Jul 06 15:26:59 2025 +0200 @@ -685,10 +685,10 @@ discrimination as to their size! With BEST_FIRST, fails for problem 41.*) fun best_prolog_tac ctxt sizef horns = - BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac ctxt horns 1); + BEST_FIRST (Thm.no_prems, sizef) (prolog_step_tac ctxt horns 1); fun depth_prolog_tac ctxt horns = - DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac ctxt horns 1); + DEPTH_FIRST Thm.no_prems (prolog_step_tac ctxt horns 1); (*Return all negative clauses, as possible goal clauses*) fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls)); @@ -717,7 +717,7 @@ MESON all_tac (make_clauses ctxt) (fn cls => THEN_BEST_FIRST (resolve_tac ctxt (gocls cls) 1) - (has_fewer_prems 1, sizef) + (Thm.no_prems, sizef) (prolog_step_tac ctxt (make_horns cls) 1)) ctxt @@ -739,14 +739,14 @@ 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) end; fun iter_deepen_prolog_tac ctxt horns = - ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' ctxt horns); + ITER_DEEPEN iter_deepen_limit Thm.no_prems (prolog_step_tac' ctxt horns); fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON all_tac (make_clauses ctxt) (fn cls => @@ -761,7 +761,7 @@ ["clauses:"] @ map (Thm.string_of_thm ctxt) horns)) in THEN_ITER_DEEPEN iter_deepen_limit - (resolve_tac ctxt goes 1) (has_fewer_prems 1) (prolog_step_tac' ctxt horns) + (resolve_tac ctxt goes 1) Thm.no_prems (prolog_step_tac' ctxt horns) end)); fun meson_tac ctxt ths = diff -r 982e7128ce0f -r ae85cd17ffbe src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Fri Jul 04 15:08:09 2025 +0100 +++ b/src/HOL/Tools/record.ML Sun Jul 06 15:26:59 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 982e7128ce0f -r ae85cd17ffbe src/Provers/blast.ML --- a/src/Provers/blast.ML Fri Jul 04 15:08:09 2025 +0100 +++ b/src/Provers/blast.ML Sun Jul 06 15:26:59 2025 +0200 @@ -566,18 +566,18 @@ | isVarForm (Const (c, _) $ Var _) = (c = Data.not_name) | isVarForm _ = false; -fun netMkRules state P vars (nps: Classical.netpair list) = +fun netMkRules state P vars (nps: Bires.netpair list) = case P of (Const ("*Goal*", _) $ G) => let val pG = mk_Trueprop (toTerm 2 G) val intrs = maps (fn (inet,_) => Net.unify_term inet pG) nps - in map (fromIntrRule state vars o #2) (order_list intrs) end + in map (fromIntrRule state vars o #2) (Bires.tag_order intrs) end | _ => if isVarForm P then [] (*The formula is too flexible, reject*) else let val pP = mk_Trueprop (toTerm 3 P) val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps - in map_filter (fromRule state vars o #2) (order_list elims) end; + in map_filter (fromRule state vars o #2) (Bires.tag_order elims) end; (*Normalize a branch--for tracing*) diff -r 982e7128ce0f -r ae85cd17ffbe src/Provers/classical.ML --- a/src/Provers/classical.ML Fri Jul 04 15:08:09 2025 +0100 +++ b/src/Provers/classical.ML Sun Jul 06 15:26:59 2025 +0200 @@ -97,7 +97,6 @@ include BASIC_CLASSICAL val classical_rule: Proof.context -> thm -> thm type rule = thm * (thm * thm list) * (thm * thm list) - type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net val rep_cs: claset -> {safeIs: rule Item_Net.T, safeEs: rule Item_Net.T, @@ -105,11 +104,11 @@ unsafeEs: rule Item_Net.T, swrappers: (string * (Proof.context -> wrapper)) list, uwrappers: (string * (Proof.context -> wrapper)) list, - safe0_netpair: netpair, - safep_netpair: netpair, - unsafe_netpair: netpair, - dup_netpair: netpair, - extra_netpair: Context_Rules.netpair} + safe0_netpair: Bires.netpair, + safep_netpair: Bires.netpair, + unsafe_netpair: Bires.netpair, + dup_netpair: Bires.netpair, + extra_netpair: Bires.netpair} val get_cs: Context.generic -> claset val map_cs: (claset -> claset) -> Context.generic -> Context.generic val safe_dest: int option -> attribute @@ -217,7 +216,6 @@ type rule = thm * (thm * thm list) * (thm * thm list); (*external form, internal form (possibly swapped), dup form (possibly swapped)*) -type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net; type wrapper = (int -> tactic) -> int -> tactic; datatype claset = @@ -228,17 +226,15 @@ unsafeEs: rule Item_Net.T, (*unsafe elimination rules*) swrappers: (string * (Proof.context -> wrapper)) list, (*for transforming safe_step_tac*) uwrappers: (string * (Proof.context -> wrapper)) list, (*for transforming step_tac*) - safe0_netpair: netpair, (*nets for trivial cases*) - safep_netpair: netpair, (*nets for >0 subgoals*) - unsafe_netpair: netpair, (*nets for unsafe rules*) - dup_netpair: netpair, (*nets for duplication*) - extra_netpair: Context_Rules.netpair}; (*nets for extra rules*) + safe0_netpair: Bires.netpair, (*nets for trivial cases*) + safep_netpair: Bires.netpair, (*nets for >0 subgoals*) + unsafe_netpair: Bires.netpair, (*nets for unsafe rules*) + dup_netpair: Bires.netpair, (*nets for duplication*) + extra_netpair: Bires.netpair}; (*nets for extra rules*) val empty_rules: rule Item_Net.T = Item_Net.init (Thm.eq_thm_prop o apply2 #1) (single o Thm.full_prop_of o #1); -val empty_netpair = (Net.empty, Net.empty); - val empty_cs = CS {safeIs = empty_rules, @@ -247,11 +243,11 @@ unsafeEs = empty_rules, swrappers = [], uwrappers = [], - safe0_netpair = empty_netpair, - safep_netpair = empty_netpair, - unsafe_netpair = empty_netpair, - dup_netpair = empty_netpair, - extra_netpair = empty_netpair}; + safe0_netpair = Bires.empty_netpair, + safep_netpair = Bires.empty_netpair, + unsafe_netpair = Bires.empty_netpair, + dup_netpair = Bires.empty_netpair, + extra_netpair = Bires.empty_netpair}; fun rep_cs (CS args) = args; @@ -267,27 +263,26 @@ then rules added most recently (preferring the head of the list).*) fun tag_brls k [] = [] | tag_brls k (brl::brls) = - (1000000*subgoals_of_brl brl + k, brl) :: - tag_brls (k+1) brls; + ({weight = Bires.subgoals_of brl, index = k}, brl) :: tag_brls (k + 1) brls; -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 tag_weight_brls _ _ [] = [] + | tag_weight_brls w k (brl::brls) = + ({weight = w, index = k}, brl) :: tag_weight_brls w (k + 1) brls; (*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 new insertions the lowest priority.*) -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 insert (nI, nE) = Bires.insert_tagged_rules o (tag_brls (~(2*nI+nE))) o joinrules; -fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls; -fun delete x = delete_tagged_list (joinrules x); +fun insert_default_weight w0 w (nI, nE) = + Bires.insert_tagged_rules o tag_weight_brls (the_default w0 w) (~(nI + nE)) o single; + +fun delete x = Bires.delete_tagged_rules (joinrules x); fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th); fun make_elim ctxt th = - if has_fewer_prems 1 th then bad_thm ctxt "Ill-formed destruction rule" th + if Thm.no_prems th then bad_thm ctxt "Ill-formed destruction rule" th else Tactic.make_elim th; fun warn_thm ctxt msg th = @@ -329,7 +324,7 @@ uwrappers = uwrappers, unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, - extra_netpair = insert' (the_default 0 w) (nI, nE) ([th], []) extra_netpair} + extra_netpair = insert_default_weight 0 w (nI, nE) (false, th) extra_netpair} end; fun add_safe_elim w r @@ -340,7 +335,7 @@ let val (th, rl, _) = r; val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) - List.partition (fn (rl, _) => Thm.nprems_of rl = 1) [rl]; + List.partition (Thm.one_prem o #1) [rl]; val nI = Item_Net.length safeIs; val nE = Item_Net.length safeEs + 1; in @@ -355,7 +350,7 @@ uwrappers = uwrappers, unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, - extra_netpair = insert' (the_default 0 w) (nI, nE) ([], [th]) extra_netpair} + extra_netpair = insert_default_weight 0 w (nI, nE) (true, th) extra_netpair} end; fun add_unsafe_intro w r @@ -379,7 +374,7 @@ uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - extra_netpair = insert' (the_default 1 w) (nI, nE) ([th], []) extra_netpair} + extra_netpair = insert_default_weight 1 w (nI, nE) (false, th) extra_netpair} end; fun add_unsafe_elim w r @@ -403,7 +398,7 @@ uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - extra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) extra_netpair} + extra_netpair = insert_default_weight 1 w (nI, nE) (true, th) extra_netpair} end; fun trim_context (th, (th1, ths1), (th2, ths2)) = @@ -423,7 +418,7 @@ fun addSE w ctxt th (cs as CS {safeEs, ...}) = let - val _ = has_fewer_prems 1 th andalso bad_thm ctxt "Ill-formed elimination rule" th; + val _ = Thm.no_prems th andalso bad_thm ctxt "Ill-formed elimination rule" th; val th' = classical_rule ctxt (flat_rule ctxt th); val rl = (th', []); val r = trim_context (th, rl, rl); @@ -446,7 +441,7 @@ fun addE w ctxt th (cs as CS {unsafeEs, ...}) = let - val _ = has_fewer_prems 1 th andalso bad_thm ctxt "Ill-formed elimination rule" th; + val _ = Thm.no_prems th andalso bad_thm ctxt "Ill-formed elimination rule" th; val th' = classical_rule ctxt (flat_rule ctxt th); val dup_th' = dup_elim ctxt th' handle THM _ => bad_thm ctxt "Ill-formed elimination rule" th; val r = trim_context (th, (th', []), (dup_th', [])); @@ -488,7 +483,7 @@ safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = let val (th, rl, _) = r; - val (safe0_rls, safep_rls) = List.partition (fn (rl, _) => Thm.nprems_of rl = 1) [rl]; + val (safe0_rls, safep_rls) = List.partition (Thm.one_prem o #1) [rl]; in CS {safe0_netpair = delete ([], map fst safe0_rls) safe0_netpair, @@ -721,9 +716,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!*) @@ -736,12 +731,11 @@ (*** Clarify_tac: do safe steps without causing branching ***) -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 Bires.tag_ord + (SOME (fn rl => Bires.subgoals_of rl = 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 +751,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 +767,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 = @@ -804,12 +798,12 @@ (*Slower but smarter than fast_tac*) fun best_tac ctxt = Object_Logic.atomize_prems_tac ctxt THEN' - SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac ctxt 1)); + SELECT_GOAL (BEST_FIRST (Thm.no_prems, Data.sizef) (step_tac ctxt 1)); (*even a bit smarter than best_tac*) fun first_best_tac ctxt = Object_Logic.atomize_prems_tac ctxt THEN' - SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac ctxt))); + SELECT_GOAL (BEST_FIRST (Thm.no_prems, Data.sizef) (FIRSTGOAL (step_tac ctxt))); fun slow_tac ctxt = Object_Logic.atomize_prems_tac ctxt THEN' @@ -817,7 +811,7 @@ fun slow_best_tac ctxt = Object_Logic.atomize_prems_tac ctxt THEN' - SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac ctxt 1)); + SELECT_GOAL (BEST_FIRST (Thm.no_prems, Data.sizef) (slow_step_tac ctxt 1)); (***ASTAR with weight weight_ASTAR, by Norbert Voelker*) @@ -827,13 +821,13 @@ fun astar_tac ctxt = Object_Logic.atomize_prems_tac ctxt THEN' SELECT_GOAL - (ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev) + (ASTAR (Thm.no_prems, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev) (step_tac ctxt 1)); fun slow_astar_tac ctxt = Object_Logic.atomize_prems_tac ctxt THEN' SELECT_GOAL - (ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev) + (ASTAR (Thm.no_prems, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev) (slow_step_tac ctxt 1)); @@ -846,7 +840,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 @@ -910,7 +904,7 @@ Attrib.setup \<^binding>\intro\ (Context_Rules.add safe_intro unsafe_intro Context_Rules.intro_query) "declaration of Classical introduction rule" #> Attrib.setup \<^binding>\rule\ (Scan.lift Args.del >> K rule_del) - "remove declaration of intro/elim/dest rule"); + "remove declaration of Classical intro/elim/dest rule"); diff -r 982e7128ce0f -r ae85cd17ffbe src/Provers/typedsimp.ML --- a/src/Provers/typedsimp.ML Fri Jul 04 15:08:09 2025 +0100 +++ b/src/Provers/typedsimp.ML Sun Jul 06 15:26:59 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 982e7128ce0f -r ae85cd17ffbe src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Fri Jul 04 15:08:09 2025 +0100 +++ b/src/Pure/Isar/context_rules.ML Sun Jul 06 15:26:59 2025 +0200 @@ -1,5 +1,6 @@ (* Title: Pure/Isar/context_rules.ML - Author: Stefan Berghofer and Markus Wenzel, TU Muenchen + Author: Stefan Berghofer, TU Muenchen + Author: Makarius Declarations of intro/elim/dest rules in Pure (see also Provers/classical.ML for a more specialized version of the same idea). @@ -7,11 +8,9 @@ signature CONTEXT_RULES = sig - type netpair = ((int * int) * (bool * thm)) Net.net * ((int * int) * (bool * thm)) Net.net - val netpair_bang: Proof.context -> netpair - val netpair: Proof.context -> netpair - val orderlist: ((int * int) * 'a) list -> 'a list - val find_rules_netpair: Proof.context -> bool -> thm list -> term -> netpair -> thm list + val netpair_bang: Proof.context -> Bires.netpair + val netpair: Proof.context -> Bires.netpair + val find_rules_netpair: Proof.context -> bool -> thm list -> term -> Bires.netpair -> thm list val find_rules: Proof.context -> bool -> thm list -> term -> thm list list val print_rules: Proof.context -> unit val addSWrapper: (Proof.context -> (int -> tactic) -> int -> tactic) -> theory -> theory @@ -38,36 +37,12 @@ (** rule declaration contexts **) -(* rule kinds *) - -val intro_bangK = (0, false); -val elim_bangK = (0, true); -val introK = (1, false); -val elimK = (1, true); -val intro_queryK = (2, false); -val elim_queryK = (2, true); - -val kind_names = - [(intro_bangK, "safe introduction rules (intro!)"), - (elim_bangK, "safe elimination rules (elim!)"), - (introK, "introduction rules (intro)"), - (elimK, "elimination rules (elim)"), - (intro_queryK, "extra introduction rules (intro?)"), - (elim_queryK, "extra elimination rules (elim?)")]; - -val rule_kinds = map #1 kind_names; -val rule_indexes = distinct (op =) (map #1 rule_kinds); - - (* context data *) -type netpair = ((int * int) * (bool * thm)) Net.net * ((int * int) * (bool * thm)) Net.net; -val empty_netpairs: netpair list = replicate (length rule_indexes) (Net.empty, Net.empty); - datatype rules = Rules of {next: int, - rules: (int * ((int * bool) * thm)) list, - netpairs: netpair list, + rules: (int * (Bires.kind * thm)) list, + netpairs: Bires.netpair list, wrappers: ((Proof.context -> (int -> tactic) -> int -> tactic) * stamp) list * ((Proof.context -> (int -> tactic) -> int -> tactic) * stamp) list}; @@ -75,30 +50,33 @@ fun make_rules next rules netpairs wrappers = Rules {next = next, rules = rules, netpairs = netpairs, wrappers = wrappers}; -fun add_rule (i, b) opt_w th (Rules {next, rules, netpairs, wrappers}) = +fun add_rule kind opt_weight th (Rules {next, rules, netpairs, wrappers}) = let - val w = opt_w |> \<^if_none>\Tactic.subgoals_of_brl (b, th)\; + val weight = opt_weight |> \<^if_none>\Bires.subgoals_of (Bires.kind_rule kind th)\; + val tag = {weight = weight, index = next}; 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 - end; + val rules' = (weight, (kind, th')) :: rules; + val netpairs' = netpairs + |> Bires.kind_map kind (Bires.insert_tagged_rule (tag, Bires.kind_rule kind th')); + in make_rules (next - 1) rules' 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_rule (b, th) netpair handle Net.DELETE => netpair; + val rules' = filter_out eq_th rules; + val netpairs' = map (del false o del true) netpairs; 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 + else make_rules next rules' netpairs' wrappers end; fun del_rule th = del_rule0 th o del_rule0 (Tactic.make_elim th); -structure Rules = Generic_Data +structure Data = Generic_Data ( type T = rules; - val empty = make_rules ~1 [] empty_netpairs ([], []); + val empty = make_rules ~1 [] Bires.kind_netpairs ([], []); fun merge (Rules {rules = rules1, wrappers = (ws1, ws1'), ...}, Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) = @@ -108,48 +86,41 @@ val rules = Library.merge (fn ((_, (k1, th1)), (_, (k2, th2))) => 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)))) - (next upto ~1 ~~ rules) empty_netpairs; + val netpairs = + fold (fn (index, (weight, (kind, th))) => + Bires.kind_map kind + (Bires.insert_tagged_rule ({weight = weight, index = index}, (Bires.kind_elim kind, th)))) + (next upto ~1 ~~ rules) Bires.kind_netpairs; in make_rules (next - 1) rules netpairs wrappers end; ); fun print_rules ctxt = let - val Rules {rules, ...} = Rules.get (Context.Proof ctxt); - fun prt_kind (i, b) = - Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":") - (map_filter (fn (_, (k, th)) => - if k = (i, b) then SOME (Thm.pretty_thm_item ctxt th) else NONE) + val Rules {rules, ...} = Data.get (Context.Proof ctxt); + fun prt_kind kind = + Pretty.big_list (Bires.kind_title kind ^ ":") + (map_filter (fn (_, (kind', th)) => + if kind = kind' then SOME (Thm.pretty_thm_item ctxt th) else NONE) (sort (int_ord o apply2 fst) rules)); - in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end; + in Pretty.writeln (Pretty.chunks (map prt_kind Bires.kind_domain)) end; (* access data *) -fun netpairs ctxt = let val Rules {netpairs, ...} = Rules.get (Context.Proof ctxt) in netpairs end; +fun netpairs ctxt = let val Rules {netpairs, ...} = Data.get (Context.Proof ctxt) in netpairs end; val netpair_bang = hd o netpairs; val netpair = hd o tl o netpairs; (* retrieving rules *) -fun untaglist [] = [] - | untaglist [(_ : int * int, x)] = [x] - | untaglist ((k, x) :: (rest as (k', _) :: _)) = - if k = k' then untaglist rest - else x :: untaglist rest; - -fun orderlist brls = - untaglist (sort (prod_ord int_ord int_ord o apply2 fst) brls); - -fun orderlist_no_weight brls = - untaglist (sort (int_ord o apply2 (snd o fst)) brls); - local +fun order weighted = + make_order_list (Bires.weighted_tag_ord weighted) NONE; + fun may_unify weighted t net = - map snd ((if weighted then orderlist else orderlist_no_weight) (Net.unify_term net t)); + map snd (order weighted (Net.unify_term net t)); fun find_erules _ [] = K [] | find_erules w (fact :: _) = may_unify w (Logic.strip_assums_concl (Thm.prop_of fact)); @@ -171,7 +142,7 @@ (* wrappers *) fun gen_add_wrapper upd w = - Context.theory_map (Rules.map (fn Rules {next, rules, netpairs, wrappers} => + Context.theory_map (Data.map (fn Rules {next, rules, netpairs, wrappers} => make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers))); val addSWrapper = gen_add_wrapper Library.apfst; @@ -179,7 +150,7 @@ fun gen_wrap which ctxt = - let val Rules {wrappers, ...} = Rules.get (Context.Proof ctxt) + let val Rules {wrappers, ...} = Data.get (Context.Proof ctxt) in fold_rev (fn (w, _) => w ctxt) (which wrappers) end; val Swrap = gen_wrap #1; @@ -192,20 +163,20 @@ (* add and del rules *) -val rule_del = Thm.declaration_attribute (Rules.map o del_rule); +val rule_del = Thm.declaration_attribute (Data.map o del_rule); fun rule_add k view opt_w = - Thm.declaration_attribute (fn th => Rules.map (add_rule k opt_w (view th) o del_rule th)); + Thm.declaration_attribute (fn th => Data.map (add_rule k opt_w (view th) o del_rule th)); -val intro_bang = rule_add intro_bangK I; -val elim_bang = rule_add elim_bangK I; -val dest_bang = rule_add elim_bangK Tactic.make_elim; -val intro = rule_add introK I; -val elim = rule_add elimK I; -val dest = rule_add elimK Tactic.make_elim; -val intro_query = rule_add intro_queryK I; -val elim_query = rule_add elim_queryK I; -val dest_query = rule_add elim_queryK Tactic.make_elim; +val intro_bang = rule_add Bires.intro_bang_kind I; +val elim_bang = rule_add Bires.elim_bang_kind I; +val dest_bang = rule_add Bires.elim_bang_kind Tactic.make_elim; +val intro = rule_add Bires.intro_kind I; +val elim = rule_add Bires.elim_kind I; +val dest = rule_add Bires.elim_kind Tactic.make_elim; +val intro_query = rule_add Bires.intro_query_kind I; +val elim_query = rule_add Bires.elim_query_kind I; +val dest_query = rule_add Bires.elim_query_kind Tactic.make_elim; val _ = Theory.setup (snd o Global_Theory.add_thms [((Binding.empty, Drule.equal_intr_rule), [intro_query NONE])]); @@ -219,12 +190,12 @@ val _ = Theory.setup (Attrib.setup \<^binding>\intro\ (add intro_bang intro intro_query) - "declaration of introduction rule" #> + "declaration of Pure introduction rule" #> Attrib.setup \<^binding>\elim\ (add elim_bang elim elim_query) - "declaration of elimination rule" #> + "declaration of Pure elimination rule" #> Attrib.setup \<^binding>\dest\ (add dest_bang dest dest_query) - "declaration of destruction rule" #> + "declaration of Pure destruction rule" #> Attrib.setup \<^binding>\rule\ (Scan.lift Args.del >> K rule_del) - "remove declaration of intro/elim/dest rule"); + "remove declaration of Pure intro/elim/dest rule"); end; diff -r 982e7128ce0f -r ae85cd17ffbe src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Jul 04 15:08:09 2025 +0100 +++ b/src/Pure/ROOT.ML Sun Jul 06 15:26:59 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 982e7128ce0f -r ae85cd17ffbe src/Pure/bires.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/bires.ML Sun Jul 06 15:26:59 2025 +0200 @@ -0,0 +1,203 @@ +(* Title: Pure/bires.ML + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Makarius + +Biresolution and resolution using nets. +*) + +signature BIRES = +sig + type rule = bool * thm + val subgoals_of: rule -> int + val subgoals_ord: rule ord + val no_subgoals: rule -> bool + + type tag = {weight: int, index: int} + val tag0_ord: tag ord + val tag_ord: tag ord + val weighted_tag_ord: bool -> tag ord + val tag_order: (tag * 'a) list -> 'a list + + type netpair = (tag * rule) Net.net * (tag * rule) Net.net + val empty_netpair: netpair + + val insert_tagged_rule: tag * rule -> netpair -> netpair + val insert_tagged_rules: (tag * rule) list -> netpair -> netpair + val delete_tagged_rule: rule -> netpair -> netpair + val delete_tagged_rules: rule list -> netpair -> netpair + val biresolution_from_nets_tac: Proof.context -> tag ord -> (rule -> bool) option -> + bool -> netpair -> int -> tactic + val biresolve_from_nets_tac: Proof.context -> netpair -> int -> tactic + val bimatch_from_nets_tac: Proof.context -> netpair -> int -> tactic + + type net = (int * thm) Net.net + val build_net: thm list -> net + val filt_resolve_from_net_tac: Proof.context -> int -> net -> int -> tactic + val resolve_from_net_tac: Proof.context -> net -> int -> tactic + val match_from_net_tac: Proof.context -> net -> int -> tactic + + eqtype kind + val intro_bang_kind: kind + val elim_bang_kind: kind + val intro_kind: kind + val elim_kind: kind + val intro_query_kind: kind + val elim_query_kind: kind + val kind_index: kind -> int + val kind_elim: kind -> bool + val kind_domain: kind list + val kind_netpairs: netpair list + val kind_map: kind -> ('a -> 'a) -> 'a list -> 'a list + val kind_rule: kind -> thm -> rule + val kind_title: kind -> string +end + +structure Bires: BIRES = +struct + +(** Natural Deduction using (bires_flg, rule) pairs **) + +(* type rule *) + +type rule = bool * thm; (*see Thm.biresolution*) + +fun subgoals_of (true, thm) = Thm.nprems_of thm - 1 + | subgoals_of (false, thm) = Thm.nprems_of thm; + +val subgoals_ord = int_ord o apply2 subgoals_of; + +fun no_subgoals (true, thm) = Thm.one_prem thm + | no_subgoals (false, thm) = Thm.no_prems thm; + + +(* tagged rules *) + +type tag = {weight: int, index: int}; + +val tag0_ord: tag ord = int_ord o apply2 #index; +val tag_ord: tag ord = int_ord o apply2 #weight ||| tag0_ord; + +fun weighted_tag_ord weighted = if weighted then tag_ord else tag0_ord; + +fun tag_order list = make_order_list tag_ord NONE list; + + +(* discrimination nets for intr/elim rules *) + +type netpair = (tag * rule) Net.net * (tag * rule) Net.net; + +val empty_netpair: netpair = (Net.empty, Net.empty); + + +(** To preserve the order of the rules, tag them with decreasing integers **) + +(*insert one tagged brl into the pair of nets*) +fun insert_tagged_rule (tagged_rule as (_, (eres, th))) ((inet, enet): netpair) = + if eres then + (case try Thm.major_prem_of th of + SOME prem => (inet, Net.insert_term (K false) (prem, tagged_rule) enet) + | NONE => error "insert_tagged_rule: elimination rule with no premises") + else (Net.insert_term (K false) (Thm.concl_of th, tagged_rule) inet, enet); + +fun insert_tagged_rules rls = fold_rev insert_tagged_rule rls; + + +(*delete one kbrl from the pair of nets*) +local + fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th') +in + +fun delete_tagged_rule (brl as (eres, th)) ((inet, enet): netpair) = + (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); + +fun delete_tagged_rules rls = fold_rev delete_tagged_rule rls; + +end; + +(*biresolution using a pair of nets rather than rules: + boolean "match" indicates matching or unification.*) +fun biresolution_from_nets_tac ctxt ord pred match ((inet, enet): netpair) = + SUBGOAL + (fn (prem, i) => + let + val hyps = Logic.strip_assums_hyp prem; + val concl = Logic.strip_assums_concl prem; + val tagged_rules = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps; + val order = make_order_list ord pred; + in PRIMSEQ (Thm.biresolution (SOME ctxt) match (order tagged_rules) i) end); + +(*versions taking pre-built nets. No filtering of brls*) +fun biresolve_from_nets_tac ctxt = biresolution_from_nets_tac ctxt tag_ord NONE false; +fun bimatch_from_nets_tac ctxt = biresolution_from_nets_tac ctxt tag_ord NONE true; + + +(** Rule kinds and declarations **) + +datatype kind = Kind of int * bool; + +val intro_bang_kind = Kind (0, false); +val elim_bang_kind = Kind (0, true); +val intro_kind = Kind (1, false); +val elim_kind = Kind (1, true); +val intro_query_kind = Kind (2, false); +val elim_query_kind = Kind (2, true); + +val kind_infos = + [(intro_bang_kind, ("safe introduction", "(intro!)")), + (elim_bang_kind, ("safe elimination", "(elim!)")), + (intro_kind, ("introduction", "(intro)")), + (elim_kind, ("elimination", "(elim)")), + (intro_query_kind, ("extra introduction", "(intro?)")), + (elim_query_kind, ("extra elimination", "(elim?)"))]; + +fun kind_index (Kind (i, _)) = i; +fun kind_elim (Kind (_, b)) = b; + +val kind_domain = map #1 kind_infos; +val kind_netpairs = + replicate (length (distinct (op =) (map kind_index kind_domain))) empty_netpair; + +fun kind_map kind f = nth_map (kind_index kind) f; +fun kind_rule kind thm : rule = (kind_elim kind, thm); + +val the_kind_info = the o AList.lookup (op =) kind_infos; + +fun kind_title kind = + let val (a, b) = the_kind_info kind + in a ^ " rules " ^ b end; + + +(** Simpler version for resolve_tac -- only one net, and no hyps **) + +type net = (int * thm) Net.net; + +(*build a net of rules for resolution*) +fun build_net rls : net = + fold_rev (fn (k, th) => Net.insert_term (K false) (Thm.concl_of th, (k, th))) + (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 982e7128ce0f -r ae85cd17ffbe src/Pure/goal.ML --- a/src/Pure/goal.ML Fri Jul 04 15:08:09 2025 +0100 +++ b/src/Pure/goal.ML Sun Jul 06 15:26:59 2025 +0200 @@ -268,7 +268,7 @@ (*with structural marker*) fun SELECT_GOAL tac i st = - if Thm.nprems_of st = 1 andalso i = 1 then tac st + if Thm.one_prem st andalso i = 1 then tac st else (PRIMITIVE (restrict i 1) THEN tac THEN PRIMITIVE (unrestrict i)) st; (*without structural marker*) diff -r 982e7128ce0f -r ae85cd17ffbe src/Pure/library.ML --- a/src/Pure/library.ML Fri Jul 04 15:08:09 2025 +0100 +++ b/src/Pure/library.ML Sun Jul 06 15:26:59 2025 +0200 @@ -219,7 +219,8 @@ val sort_strings: string list -> string list val sort_by: ('a -> string) -> 'a list -> 'a list val tag_list: int -> 'a list -> (int * 'a) list - val untag_list: (int * 'a) list -> 'a list + val untag_list: (''tag * 'a) list -> 'a list + val make_order_list: ''tag ord -> ('a -> bool) option -> (''tag * 'a) list -> 'a list val order_list: (int * 'a) list -> 'a list (*misc*) @@ -1047,13 +1048,18 @@ (*remove tags and suppress duplicates -- list is assumed sorted!*) fun untag_list [] = [] - | untag_list [(k: int, x)] = [x] - | untag_list ((k, x) :: (rest as (k', x') :: _)) = - if k = k' then untag_list rest + | untag_list [(_, x)] = [x] + | untag_list ((tag, x) :: (rest as (tag', _) :: _)) = + if tag = tag' then untag_list rest else x :: untag_list rest; -(*return list elements in original order*) -fun order_list list = untag_list (sort (int_ord o apply2 fst) list); +fun make_order_list ord pred list = + list + |> (case pred of NONE => I | SOME p => filter (p o snd)) + |> sort (ord o apply2 fst) + |> untag_list; + +fun order_list list = make_order_list int_ord NONE list; diff -r 982e7128ce0f -r ae85cd17ffbe src/Pure/logic.ML --- a/src/Pure/logic.ML Fri Jul 04 15:08:09 2025 +0100 +++ b/src/Pure/logic.ML Sun Jul 06 15:26:59 2025 +0200 @@ -27,6 +27,7 @@ val strip_prems: int * term list * term -> term list * term val count_prems: term -> int val no_prems: term -> bool + val one_prem: term -> bool val nth_prem: int * term -> term val close_term: (string * term) list -> term -> term val close_prop: (string * term) list -> term list -> term -> term @@ -221,6 +222,9 @@ fun no_prems (Const ("Pure.imp", _) $ _ $ _) = false | no_prems _ = true; +fun one_prem (Const ("Pure.imp", _) $ _ $ B) = no_prems B + | one_prem _ = false; + (*Select Ai from A1\...Ai\B*) fun nth_prem (1, Const ("Pure.imp", _) $ A $ _) = A | nth_prem (i, Const ("Pure.imp", _) $ _ $ B) = nth_prem (i - 1, B) diff -r 982e7128ce0f -r ae85cd17ffbe src/Pure/search.ML --- a/src/Pure/search.ML Fri Jul 04 15:08:09 2025 +0100 +++ b/src/Pure/search.ML Sun Jul 06 15:26:59 2025 +0200 @@ -52,10 +52,10 @@ fun has_fewer_prems n rule = Thm.nprems_of rule < n; (*Apply a tactic if subgoals remain, else do nothing.*) -val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac; +val IF_UNSOLVED = COND Thm.no_prems all_tac; (*Force a tactic to solve its goal completely, otherwise fail *) -fun SOLVE tac = tac THEN COND (has_fewer_prems 1) all_tac no_tac; +fun SOLVE tac = tac THEN COND Thm.no_prems all_tac no_tac; (*Execute tac1, but only execute tac2 if there are at least as many subgoals as before. This ensures that tac2 is only applied to an outcome of tac1.*) @@ -72,7 +72,7 @@ | n => DEPTH_FIRST (has_fewer_prems n) tac); (*Uses depth-first search to solve ALL subgoals*) -val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1); +val DEPTH_SOLVE = DEPTH_FIRST Thm.no_prems; diff -r 982e7128ce0f -r ae85cd17ffbe src/Pure/tactic.ML --- a/src/Pure/tactic.ML Fri Jul 04 15:08:09 2025 +0100 +++ b/src/Pure/tactic.ML Sun Jul 06 15:26:59 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,17 +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 val rotate_tac: int -> int -> tactic val defer_tac: int -> tactic @@ -51,19 +40,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,87 +184,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*) -fun subgoals_of_brl (true, rule) = Thm.nprems_of rule - 1 - | subgoals_of_brl (false, rule) = Thm.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 find_first (not o Symbol_Pos.is_identifier) xs of @@ -325,5 +220,4 @@ end; -structure Basic_Tactic: BASIC_TACTIC = Tactic; -open Basic_Tactic; +open Tactic; diff -r 982e7128ce0f -r ae85cd17ffbe src/Pure/thm.ML --- a/src/Pure/thm.ML Fri Jul 04 15:08:09 2025 +0100 +++ b/src/Pure/thm.ML Sun Jul 06 15:26:59 2025 +0200 @@ -82,6 +82,7 @@ val take_prems_of: int -> thm -> term list val nprems_of: thm -> int val no_prems: thm -> bool + val one_prem: thm -> bool val prem_of: thm -> int -> term val major_prem_of: thm -> term val cprop_of: thm -> cterm @@ -532,6 +533,7 @@ fun take_prems_of n = Logic.take_imp_prems n o prop_of; val nprems_of = Logic.count_prems o prop_of; val no_prems = Logic.no_prems o prop_of; +val one_prem = Logic.one_prem o prop_of; fun prem_of th i = Logic.nth_prem (i, prop_of th) handle TERM _ => raise THM ("prem_of", i, [th]); diff -r 982e7128ce0f -r ae85cd17ffbe src/Sequents/modal.ML --- a/src/Sequents/modal.ML Fri Jul 04 15:08:09 2025 +0100 +++ b/src/Sequents/modal.ML Sun Jul 06 15:26:59 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; @@ -83,7 +83,7 @@ rewrite_goals_tac ctxt Modal_Rule.rewrite_rls THEN solven_tac ctxt d 1; fun step_tac ctxt n = - COND (has_fewer_prems 1) all_tac + COND Thm.no_prems all_tac (DETERM(fres_safe_tac ctxt n) ORELSE (fres_unsafe_tac ctxt n APPEND fres_bound_tac ctxt n)); diff -r 982e7128ce0f -r ae85cd17ffbe src/Sequents/prover.ML --- a/src/Sequents/prover.ML Fri Jul 04 15:08:09 2025 +0100 +++ b/src/Sequents/prover.ML Sun Jul 06 15:26:59 2025 +0200 @@ -223,7 +223,7 @@ SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1)); fun best_tac ctxt = - SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1)); + SELECT_GOAL (BEST_FIRST (Thm.no_prems, size_of_thm) (step_tac ctxt 1)); val _ = Theory.setup (Method.setup \<^binding>\safe\ (method safe_tac) "" #> diff -r 982e7128ce0f -r ae85cd17ffbe src/Tools/intuitionistic.ML --- a/src/Tools/intuitionistic.ML Fri Jul 04 15:08:09 2025 +0100 +++ b/src/Tools/intuitionistic.ML Sun Jul 06 15:26:59 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 Bires.tag_ord NONE; fun safe_step_tac ctxt = Context_Rules.Swrap ctxt diff -r 982e7128ce0f -r ae85cd17ffbe src/ZF/Tools/typechk.ML --- a/src/ZF/Tools/typechk.ML Fri Jul 04 15:08:09 2025 +0100 +++ b/src/ZF/Tools/typechk.ML Sun Jul 06 15:26:59 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)));