# HG changeset patch # User wenzelm # Date 1751723632 -7200 # Node ID cb93bd70c5614859e3f10fd52be5b57401bc4692 # Parent be34513a58a10e5860ec5fe038372a64dba4d115 clarified modules; more direct operations for sort/filter; diff -r be34513a58a1 -r cb93bd70c561 src/CTT/CTT.thy --- a/src/CTT/CTT.thy Sat Jul 05 15:03:26 2025 +0200 +++ b/src/CTT/CTT.thy Sat Jul 05 15:53:52 2025 +0200 @@ -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 be34513a58a1 -r cb93bd70c561 src/FOL/intprover.ML --- a/src/FOL/intprover.ML Sat Jul 05 15:03:26 2025 +0200 +++ b/src/FOL/intprover.ML Sat Jul 05 15:53:52 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 = diff -r be34513a58a1 -r cb93bd70c561 src/FOLP/classical.ML --- a/src/FOLP/classical.ML Sat Jul 05 15:03:26 2025 +0200 +++ b/src/FOLP/classical.ML Sat Jul 05 15:53:52 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 ***) diff -r be34513a58a1 -r cb93bd70c561 src/FOLP/intprover.ML --- a/src/FOLP/intprover.ML Sat Jul 05 15:03:26 2025 +0200 +++ b/src/FOLP/intprover.ML Sat Jul 05 15:53:52 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, diff -r be34513a58a1 -r cb93bd70c561 src/Provers/classical.ML --- a/src/Provers/classical.ML Sat Jul 05 15:03:26 2025 +0200 +++ b/src/Provers/classical.ML Sat Jul 05 15:53:52 2025 +0200 @@ -267,7 +267,7 @@ 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) :: + (1000000*Bires.subgoals_of brl + k, brl) :: tag_brls (k+1) brls; fun tag_brls' _ _ [] = [] @@ -733,12 +733,11 @@ (*** Clarify_tac: do safe steps without causing branching ***) -fun nsubgoalsP n (k, brl) = (subgoals_of_brl brl = n); - (*version of Bires.bimatch_from_nets_tac that only applies rules that create precisely n subgoals.*) fun n_bimatch_from_nets_tac ctxt n = - Bires.biresolution_from_nets_tac ctxt (order_list o filter (nsubgoalsP n)) true; + Bires.biresolution_from_nets_tac ctxt + (order_list o filter (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; diff -r be34513a58a1 -r cb93bd70c561 src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Sat Jul 05 15:03:26 2025 +0200 +++ b/src/Pure/Isar/context_rules.ML Sat Jul 05 15:53:52 2025 +0200 @@ -77,7 +77,7 @@ fun add_rule (i, b) opt_w th (Rules {next, rules, netpairs, wrappers}) = let - val w = opt_w |> \<^if_none>\Tactic.subgoals_of_brl (b, th)\; + val w = opt_w |> \<^if_none>\Bires.subgoals_of (b, th)\; val th' = Thm.trim_context th; in make_rules (next - 1) ((w, ((i, b), th')) :: rules) diff -r be34513a58a1 -r cb93bd70c561 src/Pure/bires.ML --- a/src/Pure/bires.ML Sat Jul 05 15:03:26 2025 +0200 +++ b/src/Pure/bires.ML Sat Jul 05 15:53:52 2025 +0200 @@ -9,6 +9,9 @@ sig type rule = bool * thm type 'a netpair = ('a * rule) Net.net * ('a * rule) Net.net; + val subgoals_of: rule -> int + val subgoals_ord: rule ord + val no_subgoals: rule -> bool val insert_tagged_rule: 'a * rule -> 'a netpair -> 'a netpair val insert_tagged_rules: ('a * rule) list -> 'a netpair -> 'a netpair val delete_tagged_rule: rule -> 'a netpair -> 'a netpair @@ -27,10 +30,19 @@ structure Bires: BIRES = struct -type rule = bool * thm; (*eres flag, see Thm.biresolution*) +(** Natural Deduction using (bires_flg, rule) pairs **) + +type rule = bool * thm; (*see Thm.biresolution*) type 'a netpair = ('a * rule) Net.net * ('a * rule) Net.net; +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 rl = subgoals_of rl = 0; + (** To preserve the order of the rules, tag them with increasing integers **) diff -r be34513a58a1 -r cb93bd70c561 src/Pure/tactic.ML --- a/src/Pure/tactic.ML Sat Jul 05 15:03:26 2025 +0200 +++ b/src/Pure/tactic.ML Sat Jul 05 15:53:52 2025 +0200 @@ -33,8 +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 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 @@ -186,16 +184,6 @@ in filtr(limit,ths) end; -(*** 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