# HG changeset patch # User wenzelm # Date 1751794403 -7200 # Node ID ea8d633fd4a895f017e903c151674aa439d5f6fa # Parent 14f24aa1adb34d8ea78f9c083c9c7b2fceef09b9 just one type Bires.netpair, based on Bires.tag with explicit weight; more general order_list operations; diff -r 14f24aa1adb3 -r ea8d633fd4a8 src/Provers/blast.ML --- 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*) diff -r 14f24aa1adb3 -r ea8d633fd4a8 src/Provers/classical.ML --- 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; diff -r 14f24aa1adb3 -r ea8d633fd4a8 src/Pure/Isar/context_rules.ML --- 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>\Bires.subgoals_of (b, th)\; + val weight = opt_weight |> \<^if_none>\Bires.subgoals_of (b, 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 (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)); diff -r 14f24aa1adb3 -r ea8d633fd4a8 src/Pure/bires.ML --- 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 ***) diff -r 14f24aa1adb3 -r ea8d633fd4a8 src/Pure/library.ML --- 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; diff -r 14f24aa1adb3 -r ea8d633fd4a8 src/Tools/intuitionistic.ML --- 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