--- 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
--- 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 =
--- 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 ***)
--- 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,
--- 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;
--- 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>\<open>Tactic.subgoals_of_brl (b, th)\<close>;
+ val w = opt_w |> \<^if_none>\<open>Bires.subgoals_of (b, th)\<close>;
val th' = Thm.trim_context th;
in
make_rules (next - 1) ((w, ((i, b), th')) :: rules)
--- 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 **)
--- 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