# HG changeset patch # User wenzelm # Date 1751719164 -7200 # Node ID 7189368734cdbb8f09bf87a4ebe73d8fb63ffa0f # Parent 61aae966dd957684c9b4d4a842b99010f32e638f tuned signature: more explicit types; diff -r 61aae966dd95 -r 7189368734cd src/Provers/classical.ML --- a/src/Provers/classical.ML Sat Jul 05 14:19:45 2025 +0200 +++ b/src/Provers/classical.ML Sat Jul 05 14:39:24 2025 +0200 @@ -97,7 +97,7 @@ include BASIC_CLASSICAL val classical_rule: Proof.context -> thm -> thm type rule = thm * (thm * thm list) * (thm * thm list) - type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net + type netpair = int Bires.netpair val rep_cs: claset -> {safeIs: rule Item_Net.T, safeEs: rule Item_Net.T, @@ -217,7 +217,7 @@ type rule = thm * (thm * thm list) * (thm * thm list); (*external form, internal form (possibly swapped), dup form (possibly swapped)*) -type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net; +type netpair = int Bires.netpair; type wrapper = (int -> tactic) -> int -> tactic; datatype claset = diff -r 61aae966dd95 -r 7189368734cd src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Sat Jul 05 14:19:45 2025 +0200 +++ b/src/Pure/Isar/context_rules.ML Sat Jul 05 14:39:24 2025 +0200 @@ -7,7 +7,7 @@ signature CONTEXT_RULES = sig - type netpair = ((int * int) * (bool * thm)) Net.net * ((int * int) * (bool * thm)) Net.net + 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 @@ -61,7 +61,7 @@ (* context data *) -type netpair = ((int * int) * (bool * thm)) Net.net * ((int * int) * (bool * thm)) Net.net; +type netpair = (int * int) Bires.netpair; val empty_netpairs: netpair list = replicate (length rule_indexes) (Net.empty, Net.empty); datatype rules = Rules of diff -r 61aae966dd95 -r 7189368734cd src/Pure/bires.ML --- a/src/Pure/bires.ML Sat Jul 05 14:19:45 2025 +0200 +++ b/src/Pure/bires.ML Sat Jul 05 14:39:24 2025 +0200 @@ -1,25 +1,22 @@ (* Title: Pure/bires.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Makarius Biresolution and resolution using nets. *) signature BIRES = sig - val insert_tagged_brl: 'a * (bool * thm) -> - ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net -> - ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net - val delete_tagged_brl: bool * thm -> - ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net -> - ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net - val eq_kbrl: ('a * (bool * thm)) * ('a * (bool * thm)) -> bool + type rule = bool * thm + type 'a netpair = ('a * rule) Net.net * ('a * rule) Net.net; + val insert_tagged_brl: 'a * rule -> 'a netpair -> 'a netpair + val delete_tagged_brl: rule -> 'a netpair -> 'a netpair + val eq_kbrl: ('a * rule) * ('a * rule) -> bool val build_net: thm list -> (int * thm) Net.net val biresolution_from_nets_tac: Proof.context -> - ('a list -> (bool * thm) list) -> bool -> 'a Net.net * 'a Net.net -> int -> tactic - val biresolve_from_nets_tac: Proof.context -> - (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net -> int -> tactic - val bimatch_from_nets_tac: Proof.context -> - (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net -> int -> tactic + ('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 val filt_resolve_from_net_tac: Proof.context -> int -> (int * thm) Net.net -> int -> tactic val resolve_from_net_tac: Proof.context -> (int * thm) Net.net -> int -> tactic val match_from_net_tac: Proof.context -> (int * thm) Net.net -> int -> tactic @@ -28,6 +25,11 @@ structure Bires: BIRES = struct +type rule = bool * thm; (*eres flag, see Thm.biresolution*) + +type 'a netpair = ('a * rule) Net.net * ('a * rule) Net.net; + + (** To preserve the order of the rules, tag them with increasing integers **) (*insert one tagged brl into the pair of nets*)