# HG changeset patch # User wenzelm # Date 1752262582 -7200 # Node ID 0a8977dcb21a5e69177a09bb68523ec52f71083d # Parent d8ecaff223ff9b48ebfd72de2b986918531b1344 more accurate delete operation via authentic index --- minor performance tuning; diff -r d8ecaff223ff -r 0a8977dcb21a src/Provers/classical.ML --- a/src/Provers/classical.ML Fri Jul 11 15:17:42 2025 +0200 +++ b/src/Provers/classical.ML Fri Jul 11 21:36:22 2025 +0200 @@ -266,15 +266,15 @@ insert_brl (2 * k + 1) (Bires.kind_rule kind th) #> (case swapped of NONE => I | SOME th' => insert_brl (2 * k) (true, th')); -fun delete_rl kind ((th, swapped): rl) = - Bires.delete_tagged_rule (Bires.kind_rule kind th) #> - (case swapped of NONE => I | SOME th' => Bires.delete_tagged_rule (true, th')); +fun delete_rl k ((th, swapped): rl) = + Bires.delete_tagged_rule (2 * k + 1, th) #> + (case swapped of NONE => I | SOME th' => Bires.delete_tagged_rule (2 * k, th')); fun insert_plain_rule ({kind, tag, info = {rl = (th, _), ...}}: decl) = Bires.insert_tagged_rule (tag, (Bires.kind_elim kind, th)); -fun delete_plain_rule ({kind, info = {rl = (th, _), ...}, ...}: decl) = - Bires.delete_tagged_rule (Bires.kind_rule kind th); +fun delete_plain_rule ({tag = {index, ...}, info = {rl = (th, _), ...}, ...}: decl) = + Bires.delete_tagged_rule (index, th); fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th); @@ -452,7 +452,7 @@ if null old_decls then (warn_thm ctxt (fn () => "Undeclared classical rule\n") th; cs) else let - fun del which ({kind, info, ...}: decl) = delete_rl kind (which info); + fun del which ({tag = {index, ...}, info, ...}: decl) = delete_rl index (which info); val safe0_netpair' = fold (del #rl) old_decls safe0_netpair; val safep_netpair' = fold (del #rl) old_decls safep_netpair; val unsafe_netpair' = fold (del #rl) old_decls unsafe_netpair; diff -r d8ecaff223ff -r 0a8977dcb21a src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Fri Jul 11 15:17:42 2025 +0200 +++ b/src/Pure/Isar/context_rules.ML Fri Jul 11 21:36:22 2025 +0200 @@ -49,8 +49,8 @@ fun insert_decl ({kind, tag, info = th}: decl) = Bires.insert_tagged_rule (tag, Bires.kind_rule kind th); -fun remove_decl ({info = th, ...}: decl) = - Bires.delete_tagged_rule (false, th) o Bires.delete_tagged_rule (true, th); +fun remove_decl ({tag = {index, ...}, info = th, ...}: decl) = + Bires.delete_tagged_rule (index, th); (* context data *) diff -r d8ecaff223ff -r 0a8977dcb21a src/Pure/bires.ML --- a/src/Pure/bires.ML Fri Jul 11 15:17:42 2025 +0200 +++ b/src/Pure/bires.ML Fri Jul 11 21:36:22 2025 +0200 @@ -54,7 +54,7 @@ type netpair = (tag * rule) Net.net * (tag * rule) Net.net val empty_netpair: netpair val insert_tagged_rule: tag * rule -> netpair -> netpair - val delete_tagged_rule: rule -> netpair -> netpair + val delete_tagged_rule: int * thm -> netpair -> netpair val biresolution_from_nets_tac: Proof.context -> tag ord -> (rule -> bool) option -> bool -> netpair -> int -> tactic @@ -229,19 +229,15 @@ | NONE => error "insert_tagged_rule: elimination rule with no premises") else (Net.insert_term (K false) (Thm.concl_of th, tagged_rule) inet, enet); -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); - -end; +fun delete_tagged_rule (index, th) ((inet, enet): netpair) = + let + fun eq ((), ({index = index', ...}, _)) = index = index'; + val inet' = Net.delete_term_safe eq (Thm.concl_of th, ()) inet; + val enet' = + (case try Thm.major_prem_of th of + SOME prem => Net.delete_term_safe eq (prem, ()) enet + | NONE => enet); + in (inet', enet') end; (*biresolution using a pair of nets rather than rules: