just one type Bires.netpair, based on Bires.tag with explicit weight;
more general order_list operations;
--- a/src/Provers/blast.ML Sat Jul 05 16:19:23 2025 +0200
+++ b/src/Provers/blast.ML Sun Jul 06 11:33:23 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*)
--- a/src/Provers/classical.ML Sat Jul 05 16:19:23 2025 +0200
+++ b/src/Provers/classical.ML Sun Jul 06 11:33:23 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 Bires.netpair
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 Bires.netpair;
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,11 +263,11 @@
then rules added most recently (preferring the head of the list).*)
fun tag_brls k [] = []
| tag_brls k (brl::brls) =
- (1000000*Bires.subgoals_of brl + k, brl) ::
+ ({weight = 0, index = 1000000*Bires.subgoals_of brl + 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;
+ | tag_brls' w k (brl::brls) = ({weight = w, index = k}, brl) :: tag_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
@@ -736,8 +732,8 @@
(*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 (fn (_, rl) => Bires.subgoals_of rl = 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;
--- a/src/Pure/Isar/context_rules.ML Sat Jul 05 16:19:23 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML Sun Jul 06 11:33:23 2025 +0200
@@ -7,11 +7,9 @@
signature CONTEXT_RULES =
sig
- type netpair = (int * int) Bires.netpair
- 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
@@ -61,13 +59,13 @@
(* context data *)
-type netpair = (int * int) Bires.netpair;
-val empty_netpairs: netpair list = replicate (length rule_indexes) (Net.empty, Net.empty);
+val empty_netpairs: Bires.netpair list =
+ replicate (length rule_indexes) Bires.empty_netpair;
datatype rules = Rules of
{next: int,
rules: (int * ((int * bool) * thm)) list,
- netpairs: netpair list,
+ netpairs: Bires.netpair list,
wrappers:
((Proof.context -> (int -> tactic) -> int -> tactic) * stamp) list *
((Proof.context -> (int -> tactic) -> int -> tactic) * stamp) list};
@@ -75,13 +73,14 @@
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 (i, b) opt_weight th (Rules {next, rules, netpairs, wrappers}) =
let
- val w = opt_w |> \<^if_none>\<open>Bires.subgoals_of (b, th)\<close>;
+ val weight = opt_weight |> \<^if_none>\<open>Bires.subgoals_of (b, th)\<close>;
+ 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 (Bires.insert_tagged_rule ((w, next), (b, th'))) netpairs) wrappers
+ make_rules (next - 1) ((weight, ((i, b), th')) :: rules)
+ (nth_map i (Bires.insert_tagged_rule (tag, (b, th'))) netpairs) wrappers
end;
fun del_rule0 th (rs as Rules {next, rules, netpairs, wrappers}) =
@@ -108,8 +107,8 @@
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 (Bires.insert_tagged_rule ((w, n), (b, th))))
+ val netpairs = fold (fn (index, (weight, ((i, b), th))) =>
+ nth_map i (Bires.insert_tagged_rule ({weight = weight, index = index}, (b, th))))
(next upto ~1 ~~ rules) empty_netpairs;
in make_rules (next - 1) rules netpairs wrappers end;
);
@@ -134,22 +133,13 @@
(* 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));
--- a/src/Pure/bires.ML Sat Jul 05 16:19:23 2025 +0200
+++ b/src/Pure/bires.ML Sun Jul 06 11:33:23 2025 +0200
@@ -8,18 +8,27 @@
signature BIRES =
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
- val delete_tagged_rules: rule list -> 'a netpair -> 'a netpair
- val biresolution_from_nets_tac: Proof.context ->
- ('a list -> rule list) -> bool -> 'a Net.net * 'a Net.net -> int -> tactic
- val biresolve_from_nets_tac: Proof.context -> int netpair -> int -> tactic
- val bimatch_from_nets_tac: Proof.context -> int netpair -> int -> tactic
+
+ 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
@@ -33,9 +42,9 @@
(** Natural Deduction using (bires_flg, rule) pairs **)
-type rule = bool * thm; (*see Thm.biresolution*)
+(* type rule *)
-type 'a netpair = ('a * rule) Net.net * ('a * rule) Net.net;
+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;
@@ -46,15 +55,34 @@
| 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 increasing integers **)
(*insert one tagged brl into the pair of nets*)
-fun insert_tagged_rule (kbrl as (k, (eres, th))) (inet, enet) =
+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, kbrl) enet)
+ 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, kbrl) inet, enet);
+ 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;
@@ -64,7 +92,7 @@
fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
in
-fun delete_tagged_rule (brl as (eres, th)) (inet, enet) =
+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)
@@ -76,21 +104,21 @@
end;
-(*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) =
+(*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 kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps;
- in PRIMSEQ (Thm.biresolution (SOME ctxt) match (order kbrls) i) end);
+ 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 order_list false;
-fun bimatch_from_nets_tac ctxt = biresolution_from_nets_tac ctxt order_list true;
+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;
(*** Simpler version for resolve_tac -- only one net, and no hyps ***)
--- a/src/Pure/library.ML Sat Jul 05 16:19:23 2025 +0200
+++ b/src/Pure/library.ML Sun Jul 06 11:33:23 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;
--- a/src/Tools/intuitionistic.ML Sat Jul 05 16:19:23 2025 +0200
+++ b/src/Tools/intuitionistic.ML Sun Jul 06 11:33:23 2025 +0200
@@ -25,7 +25,7 @@
fun REMDUPS tac ctxt = tac ctxt THEN_ALL_NEW remdups_tac ctxt;
-fun bires_tac ctxt = Bires.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