# HG changeset patch # User wenzelm # Date 1752352667 -7200 # Node ID 1e39653de9742184321004a757cd26e0a0883d61 # Parent 5e9c9f2c2cd847b55daaefa246f078da03365c86# Parent df2d774bcf210ec1853435a217d1dc6f9175ff34 merged diff -r 5e9c9f2c2cd8 -r 1e39653de974 src/FOLP/simp.ML --- a/src/FOLP/simp.ML Fri Jul 11 10:12:01 2025 +0200 +++ b/src/FOLP/simp.ML Sat Jul 12 22:37:47 2025 +0200 @@ -267,10 +267,8 @@ (** Deletion of congruences and rewrites **) -(*delete a thm from a thm net*) fun delete_thm th net = - Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net - handle Net.DELETE => net; + Net.delete_term_safe Thm.eq_thm_prop (Thm.concl_of th, th) net; val delete_thms = fold_rev delete_thm; diff -r 5e9c9f2c2cd8 -r 1e39653de974 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jul 11 10:12:01 2025 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sat Jul 12 22:37:47 2025 +0200 @@ -307,12 +307,14 @@ let fun add stature th = Termtab.update (normalize_vars (Thm.prop_of th), stature) - val {safeIs, (* safeEs, *) unsafeIs, (* unsafeEs, *) ...} = - ctxt |> claset_of |> Classical.rep_cs - val intros = map #1 (Item_Net.content safeIs @ Item_Net.content unsafeIs) + fun claset_rules kind = + map #1 (Classical.dest_decls ctxt (fn (_, {kind = kind', ...}) => kind = kind')); + + val intros = claset_rules Bires.intro_bang_kind @ claset_rules Bires.intro_kind; (* Add once it is used: - val elims = Item_Net.content safeEs @ Item_Net.content unsafeEs - |> map Classical.classical_rule + val elims = + (claset_rules Bires.elim_bang_kind @ claset_rules Bires.elim_kind) + |> map (Classical.classical_rule ctxt); *) val specs = Spec_Rules.get ctxt val (rec_defs, nonrec_defs) = specs diff -r 5e9c9f2c2cd8 -r 1e39653de974 src/Provers/blast.ML --- a/src/Provers/blast.ML Fri Jul 11 10:12:01 2025 +0200 +++ b/src/Provers/blast.ML Sat Jul 12 22:37:47 2025 +0200 @@ -933,10 +933,8 @@ let val State {ctxt, ntrail, nclosed, ntried, ...} = state; val trace = Config.get ctxt trace; val stats = Config.get ctxt stats; - val {safe0_netpair, safep_netpair, unsafe_netpair, ...} = - Classical.rep_cs (Classical.claset_of ctxt); - val safeList = [safe0_netpair, safep_netpair]; - val unsafeList = [unsafe_netpair]; + val safeList = [Classical.safe0_netpair_of ctxt, Classical.safep_netpair_of ctxt]; + val unsafeList = [Classical.unsafe_netpair_of ctxt]; fun prv (tacs, trs, choices, []) = (printStats state (trace orelse stats, start, tacs); cont (tacs, trs, choices)) (*all branches closed!*) diff -r 5e9c9f2c2cd8 -r 1e39653de974 src/Provers/classical.ML --- a/src/Provers/classical.ML Fri Jul 11 10:12:01 2025 +0200 +++ b/src/Provers/classical.ML Sat Jul 12 22:37:47 2025 +0200 @@ -1,5 +1,6 @@ (* Title: Provers/classical.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Makarius Theorem prover for classical reasoning, including predicate calculus, set theory, etc. @@ -10,6 +11,9 @@ For a rule to be safe, its premises and conclusion should be logically equivalent. There should be no variables in the premises that are not in the conclusion. + +Rules are maintained in "canonical reverse order", meaning that later +declarations take precedence. *) (*higher precedence than := facilitates use of references*) @@ -20,20 +24,19 @@ signature CLASSICAL_DATA = sig - val imp_elim: thm (* P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R *) - val not_elim: thm (* ~P ==> P ==> R *) - val swap: thm (* ~ P ==> (~ R ==> P) ==> R *) - val classical: thm (* (~ P ==> P) ==> P *) - val sizef: thm -> int (* size function for BEST_FIRST, typically size_of_thm *) - val hyp_subst_tacs: (Proof.context -> int -> tactic) list (* optional tactics for - substitution in the hypotheses; assumed to be safe! *) + val imp_elim: thm (* P \ Q \ (\ R \ P) \ (Q \ R) \ R *) + val not_elim: thm (* \ P \ P \ R *) + val swap: thm (* \ P \ (\ R \ P) \ R *) + val classical: thm (* (\ P \ P) \ P *) + val sizef: thm -> int (*size function for BEST_FIRST, typically size_of_thm*) + val hyp_subst_tacs: (Proof.context -> int -> tactic) list + (*optional tactics for substitution in the hypotheses; assumed to be safe!*) end; signature BASIC_CLASSICAL = sig type wrapper = (int -> tactic) -> int -> tactic type claset - val print_claset: Proof.context -> unit val addDs: Proof.context * thm list -> Proof.context val addEs: Proof.context * thm list -> Proof.context val addIs: Proof.context * thm list -> Proof.context @@ -85,30 +88,28 @@ val clarify_step_tac: Proof.context -> int -> tactic val step_tac: Proof.context -> int -> tactic val slow_step_tac: Proof.context -> int -> tactic - val swapify: thm list -> thm list val swap_res_tac: Proof.context -> thm list -> int -> tactic val inst_step_tac: Proof.context -> int -> tactic val inst0_step_tac: Proof.context -> int -> tactic val instp_step_tac: Proof.context -> int -> tactic + + val print_claset: Proof.context -> unit end; signature CLASSICAL = sig include BASIC_CLASSICAL val classical_rule: Proof.context -> thm -> thm - type rule = thm * (thm * thm list) * (thm * thm list) - val rep_cs: claset -> - {safeIs: rule Item_Net.T, - safeEs: rule Item_Net.T, - unsafeIs: rule Item_Net.T, - unsafeEs: rule Item_Net.T, - swrappers: (string * (Proof.context -> wrapper)) list, - uwrappers: (string * (Proof.context -> wrapper)) list, - safe0_netpair: Bires.netpair, - safep_netpair: Bires.netpair, - unsafe_netpair: Bires.netpair, - dup_netpair: Bires.netpair, - extra_netpair: Bires.netpair} + type rl = thm * thm option + type info = {rl: rl, dup_rl: rl, plain: thm} + type decl = info Bires.decl + type decls = info Bires.decls + val safe0_netpair_of: Proof.context -> Bires.netpair + val safep_netpair_of: Proof.context -> Bires.netpair + val unsafe_netpair_of: Proof.context -> Bires.netpair + val dup_netpair_of: Proof.context -> Bires.netpair + val extra_netpair_of: Proof.context -> Bires.netpair + val dest_decls: Proof.context -> ((thm * decl) -> bool) -> (thm * decl) list val get_cs: Context.generic -> claset val map_cs: (claset -> claset) -> Context.generic -> Context.generic val safe_dest: int option -> attribute @@ -131,18 +132,19 @@ functor Classical(Data: CLASSICAL_DATA): CLASSICAL = struct -(** classical elimination rules **) +(** Support for classical reasoning **) -(* -Classical reasoning requires stronger elimination rules. For -instance, make_elim of Pure transforms the HOL rule injD into +(* classical elimination rules *) + +(*Classical reasoning requires stronger elimination rules. For + instance, make_elim of Pure transforms the HOL rule injD into - [| inj f; f x = f y; x = y ==> PROP W |] ==> PROP W + \inj f; f x = f y; x = y \ PROP W\ \ PROP W -Such rules can cause fast_tac to fail and blast_tac to report "PROOF -FAILED"; classical_rule will strengthen this to + Such rules can cause fast_tac to fail and blast_tac to report "PROOF + FAILED"; classical_rule will strengthen this to - [| inj f; ~ W ==> f x = f y; x = y ==> W |] ==> W + \inj f; \ W \ f x = f y; x = y \ W\ \ W *) fun classical_rule ctxt rule = @@ -166,41 +168,48 @@ in if Thm.equiv_thm thy (rule, rule'') then rule else rule'' end else rule; -(*flatten nested meta connectives in prems*) + +(* flatten nested meta connectives in prems *) + fun flat_rule ctxt = Conv.fconv_rule (Conv.prems_conv ~1 (Object_Logic.atomize_prems ctxt)); -(*** Useful tactics for classical reasoning ***) +(* Useful tactics for classical reasoning *) -(*Prove goal that assumes both P and ~P. +(*Prove goal that assumes both P and \ P. No backtracking if it finds an equal assumption. Perhaps should call ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*) fun contr_tac ctxt = eresolve_tac ctxt [Data.not_elim] THEN' (eq_assume_tac ORELSE' assume_tac ctxt); -(*Finds P-->Q and P in the assumptions, replaces implication by Q. - Could do the same thing for P<->Q and P... *) +(*Finds P \ Q and P in the assumptions, replaces implication by Q. + Could do the same thing for P \ Q and P.*) fun mp_tac ctxt i = eresolve_tac ctxt [Data.not_elim, Data.imp_elim] i THEN assume_tac ctxt i; (*Like mp_tac but instantiates no variables*) fun eq_mp_tac ctxt i = ematch_tac ctxt [Data.not_elim, Data.imp_elim] i THEN eq_assume_tac i; -(*Creates rules to eliminate ~A, from rules to introduce A*) -fun swapify intrs = intrs RLN (2, [Data.swap]); -val swapped = Thm.rule_attribute [] (fn _ => fn th => th RSN (2, Data.swap)); +(*Creates rules to eliminate \ A, from rules to introduce A*) +fun maybe_swap_rule th = + (case [th] RLN (2, [Data.swap]) of + [] => NONE + | [res] => SOME res + | _ => raise THM ("RSN: multiple unifiers", 2, [th, Data.swap])); + +fun swap_rule intr = intr RSN (2, Data.swap); +val swapped = Thm.rule_attribute [] (K swap_rule); (*Uses introduction rules in the normal way, or on negated assumptions, trying rules in order. *) fun swap_res_tac ctxt rls = let - val transfer = Thm.transfer' ctxt; - fun addrl rl brls = (false, transfer rl) :: (true, transfer rl RSN (2, Data.swap)) :: brls; + fun addrl rl brls = (false, rl) :: (true, swap_rule rl) :: brls; in assume_tac ctxt ORELSE' contr_tac ctxt ORELSE' - biresolve_tac ctxt (fold_rev addrl rls []) + biresolve_tac ctxt (fold_rev (addrl o Thm.transfer' ctxt) rls []) end; (*Duplication of unsafe rules, for complete provers*) @@ -211,19 +220,27 @@ in rule_by_tactic ctxt (TRYALL (eresolve_tac ctxt [revcut_rl])) rl end; -(**** Classical rule sets ****) + +(** Classical rule sets **) + +type rl = thm * thm option; (*internal form, with possibly swapped version*) +type info = {rl: rl, dup_rl: rl, plain: thm}; +type rule = thm * info; (*external form, internal forms*) -type rule = thm * (thm * thm list) * (thm * thm list); - (*external form, internal form (possibly swapped), dup form (possibly swapped)*) +type decl = info Bires.decl; +type decls = info Bires.decls; + +fun maybe_swapped_rl th : rl = (th, maybe_swap_rule th); +fun no_swapped_rl th : rl = (th, NONE); + +fun make_info rl dup_rl plain : info = {rl = rl, dup_rl = dup_rl, plain = plain}; +fun make_info1 rl plain : info = make_info rl rl plain; type wrapper = (int -> tactic) -> int -> tactic; datatype claset = CS of - {safeIs: rule Item_Net.T, (*safe introduction rules*) - safeEs: rule Item_Net.T, (*safe elimination rules*) - unsafeIs: rule Item_Net.T, (*unsafe introduction rules*) - unsafeEs: rule Item_Net.T, (*unsafe elimination rules*) + {decls: decls, (*rule declarations in canonical order*) swrappers: (string * (Proof.context -> wrapper)) list, (*for transforming safe_step_tac*) uwrappers: (string * (Proof.context -> wrapper)) list, (*for transforming step_tac*) safe0_netpair: Bires.netpair, (*nets for trivial cases*) @@ -232,15 +249,9 @@ 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_cs = CS - {safeIs = empty_rules, - safeEs = empty_rules, - unsafeIs = empty_rules, - unsafeEs = empty_rules, + {decls = Bires.empty_decls, swrappers = [], uwrappers = [], safe0_netpair = Bires.empty_netpair, @@ -252,358 +263,208 @@ fun rep_cs (CS args) = args; -(*** Adding (un)safe introduction or elimination rules. - - In case of overlap, new rules are tried BEFORE old ones!! -***) +(* netpair primitives to insert / delete rules *) -fun joinrules (intrs, elims) = map (pair true) elims @ map (pair false) intrs; +fun insert_brl i brl = + Bires.insert_tagged_rule ({weight = Bires.subgoals_of brl, index = i}, brl); -(*Priority: prefer rules with fewest subgoals, - then rules added most recently (preferring the head of the list).*) -fun tag_brls k [] = [] - | tag_brls k (brl::brls) = - ({weight = Bires.subgoals_of brl, index = k}, brl) :: tag_brls (k + 1) brls; +fun insert_rl kind k ((th, swapped): rl) = + insert_brl (2 * k + 1) (Bires.kind_rule kind th) #> + (case swapped of NONE => I | SOME th' => insert_brl (2 * k) (true, th')); -fun tag_weight_brls _ _ [] = [] - | tag_weight_brls w k (brl::brls) = - ({weight = w, index = k}, brl) :: tag_weight_brls w (k + 1) brls; +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 = {plain = th, ...}}: decl) = + Bires.insert_tagged_rule (tag, (Bires.kind_rule kind th)); -(*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 - new insertions the lowest priority.*) -fun insert (nI, nE) = Bires.insert_tagged_rules o (tag_brls (~(2*nI+nE))) o joinrules; +fun delete_plain_rule ({tag = {index, ...}, info = {plain = th, ...}, ...}: decl) = + Bires.delete_tagged_rule (index, th); + -fun insert_default_weight w0 w (nI, nE) = - Bires.insert_tagged_rules o tag_weight_brls (the_default w0 w) (~(nI + nE)) o single; +(* erros and warnings *) -fun delete x = Bires.delete_tagged_rules (joinrules x); - -fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th); +fun err_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th); fun make_elim ctxt th = - if Thm.no_prems th then bad_thm ctxt "Ill-formed destruction rule" th + if Thm.no_prems th then err_thm ctxt "Ill-formed destruction rule" th else Tactic.make_elim th; +fun init_decl kind opt_weight info : decl = + let val weight = the_default (Bires.kind_index kind) opt_weight + in {kind = kind, tag = Bires.weight_tag weight, info = info} end; + +fun is_declared decls th kind = + exists (fn {kind = kind', ...} => kind = kind') (Bires.get_decls decls th); + fun warn_thm ctxt msg th = if Context_Position.is_really_visible ctxt - then warning (msg ^ Thm.string_of_thm ctxt th) else (); + then warning (msg () ^ Thm.string_of_thm ctxt th) else (); -fun warn_rules ctxt msg rules (r: rule) = - Item_Net.member rules r andalso (warn_thm ctxt msg (#1 r); true); +fun warn_kind ctxt decls prefix th kind = + is_declared decls th kind andalso + (warn_thm ctxt (fn () => prefix ^ Bires.kind_description kind ^ "\n") th; true); -fun warn_claset ctxt r (CS {safeIs, safeEs, unsafeIs, unsafeEs, ...}) = - warn_rules ctxt "Rule already declared as safe introduction (intro!)\n" safeIs r orelse - warn_rules ctxt "Rule already declared as safe elimination (elim!)\n" safeEs r orelse - warn_rules ctxt "Rule already declared as introduction (intro)\n" unsafeIs r orelse - warn_rules ctxt "Rule already declared as elimination (elim)\n" unsafeEs r; +fun warn_other_kinds ctxt decls th = + let val warn = warn_kind ctxt decls "Rule already declared as " th in + warn Bires.intro_bang_kind orelse + warn Bires.elim_bang_kind orelse + warn Bires.intro_kind orelse + warn Bires.elim_kind + end; -(*** add rules ***) +(* extend and merge rules *) + +local + +type netpairs = (Bires.netpair * Bires.netpair) * (Bires.netpair * Bires.netpair); + +fun add_safe_rule (decl: decl) (netpairs: netpairs) = + let + val {kind, tag = {index, ...}, info = {rl, ...}} = decl; + val no_subgoals = Bires.no_subgoals (Bires.kind_rule kind (#1 rl)); + in (apfst o (if no_subgoals then apfst else apsnd)) (insert_rl kind index rl) netpairs end; + +fun add_unsafe_rule (decl: decl) ((safe_netpairs, (unsafe_netpair, dup_netpair)): netpairs) = + let + val {kind, tag = {index, ...}, info = {rl, dup_rl, ...}} = decl; + val unsafe_netpair' = insert_rl kind index rl unsafe_netpair; + val dup_netpair' = insert_rl kind index dup_rl dup_netpair; + in (safe_netpairs, (unsafe_netpair', dup_netpair')) end; + +fun add_rule (decl as {kind, ...}: decl) = + if Bires.kind_safe kind then add_safe_rule decl + else if Bires.kind_unsafe kind then add_unsafe_rule decl + else I; + + +fun trim_context_rl (th1, opt_th2) = + (Thm.trim_context th1, Option.map Thm.trim_context opt_th2); + +fun trim_context_info {rl, dup_rl, plain} : info = + {rl = trim_context_rl rl, dup_rl = trim_context_rl dup_rl, plain = Thm.trim_context plain}; -fun add_safe_intro w r - (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = - if Item_Net.member safeIs r then cs +fun extend_rules ctxt kind opt_weight (th, info) cs = + let + val th' = Thm.trim_context th; + val decl' = init_decl kind opt_weight (trim_context_info info); + val CS {decls, swrappers, uwrappers, safe0_netpair, safep_netpair, + unsafe_netpair, dup_netpair, extra_netpair} = cs; + in + (case Bires.extend_decls (th', decl') decls of + (NONE, _) => (warn_kind ctxt decls "Ignoring duplicate " th kind; cs) + | (SOME new_decl, decls') => + let + val _ = warn_other_kinds ctxt decls th; + val ((safe0_netpair', safep_netpair'), (unsafe_netpair', dup_netpair')) = + add_rule new_decl ((safe0_netpair, safep_netpair), (unsafe_netpair, dup_netpair)); + val extra_netpair' = insert_plain_rule new_decl extra_netpair; + in + CS { + decls = decls', + swrappers = swrappers, + uwrappers = uwrappers, + safe0_netpair = safe0_netpair', + safep_netpair = safep_netpair', + unsafe_netpair = unsafe_netpair', + dup_netpair = dup_netpair', + extra_netpair = extra_netpair'} + end) + end; + +in + +fun merge_cs (cs, cs2) = + if pointer_eq (cs, cs2) then cs else let - val (th, rl, _) = r; - val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) - List.partition (Thm.no_prems o fst) [rl]; - val nI = Item_Net.length safeIs + 1; - val nE = Item_Net.length safeEs; - in - CS - {safeIs = Item_Net.update r safeIs, - safe0_netpair = insert (nI, nE) (map fst safe0_rls, maps snd safe0_rls) safe0_netpair, - safep_netpair = insert (nI, nE) (map fst safep_rls, maps snd safep_rls) safep_netpair, - safeEs = safeEs, - unsafeIs = unsafeIs, - unsafeEs = unsafeEs, - swrappers = swrappers, - uwrappers = uwrappers, - unsafe_netpair = unsafe_netpair, - dup_netpair = dup_netpair, - extra_netpair = insert_default_weight 0 w (nI, nE) (false, th) extra_netpair} - end; + val CS {decls, swrappers, uwrappers, safe0_netpair, safep_netpair, + unsafe_netpair, dup_netpair, extra_netpair} = cs; + val CS {decls = decls2, swrappers = swrappers2, uwrappers = uwrappers2, ...} = cs2; -fun add_safe_elim w r - (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = - if Item_Net.member safeEs r then cs - else - let - val (th, rl, _) = r; - val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) - List.partition (Thm.one_prem o #1) [rl]; - val nI = Item_Net.length safeIs; - val nE = Item_Net.length safeEs + 1; + val (new_decls, decls') = Bires.merge_decls (decls, decls2); + val ((safe0_netpair', safep_netpair'), (unsafe_netpair', dup_netpair')) = + fold add_rule new_decls ((safe0_netpair, safep_netpair), (unsafe_netpair, dup_netpair)); + val extra_netpair' = fold insert_plain_rule new_decls extra_netpair; in - CS - {safeEs = Item_Net.update r safeEs, - safe0_netpair = insert (nI, nE) ([], map fst safe0_rls) safe0_netpair, - safep_netpair = insert (nI, nE) ([], map fst safep_rls) safep_netpair, - safeIs = safeIs, - unsafeIs = unsafeIs, - unsafeEs = unsafeEs, - swrappers = swrappers, - uwrappers = uwrappers, - unsafe_netpair = unsafe_netpair, - dup_netpair = dup_netpair, - extra_netpair = insert_default_weight 0 w (nI, nE) (true, th) extra_netpair} + CS { + decls = decls', + swrappers = AList.merge (op =) (K true) (swrappers, swrappers2), + uwrappers = AList.merge (op =) (K true) (uwrappers, uwrappers2), + safe0_netpair = safe0_netpair', + safep_netpair = safep_netpair', + unsafe_netpair = unsafe_netpair', + dup_netpair = dup_netpair', + extra_netpair = extra_netpair'} end; -fun add_unsafe_intro w r - (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = - if Item_Net.member unsafeIs r then cs - else - let - val (th, rl, dup_rl) = r; - val nI = Item_Net.length unsafeIs + 1; - val nE = Item_Net.length unsafeEs; - in - CS - {unsafeIs = Item_Net.update r unsafeIs, - unsafe_netpair = insert (nI, nE) ([fst rl], snd rl) unsafe_netpair, - dup_netpair = insert (nI, nE) ([fst dup_rl], snd dup_rl) dup_netpair, - safeIs = safeIs, - safeEs = safeEs, - unsafeEs = unsafeEs, - swrappers = swrappers, - uwrappers = uwrappers, - safe0_netpair = safe0_netpair, - safep_netpair = safep_netpair, - extra_netpair = insert_default_weight 1 w (nI, nE) (false, th) extra_netpair} - end; +fun addSI w ctxt th cs = + extend_rules ctxt Bires.intro_bang_kind w + (th, make_info1 (maybe_swapped_rl (flat_rule ctxt th)) th) cs; -fun add_unsafe_elim w r - (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = - if Item_Net.member unsafeEs r then cs +fun addSE w ctxt th cs = + if Thm.no_prems th then err_thm ctxt "Ill-formed elimination rule" th else - let - val (th, rl, dup_rl) = r; - val nI = Item_Net.length unsafeIs; - val nE = Item_Net.length unsafeEs + 1; - in - CS - {unsafeEs = Item_Net.update r unsafeEs, - unsafe_netpair = insert (nI, nE) ([], [fst rl]) unsafe_netpair, - dup_netpair = insert (nI, nE) ([], [fst dup_rl]) dup_netpair, - safeIs = safeIs, - safeEs = safeEs, - unsafeIs = unsafeIs, - swrappers = swrappers, - uwrappers = uwrappers, - safe0_netpair = safe0_netpair, - safep_netpair = safep_netpair, - extra_netpair = insert_default_weight 1 w (nI, nE) (true, th) extra_netpair} - end; - -fun trim_context (th, (th1, ths1), (th2, ths2)) = - (Thm.trim_context th, - (Thm.trim_context th1, map Thm.trim_context ths1), - (Thm.trim_context th2, map Thm.trim_context ths2)); - -fun addSI w ctxt th (cs as CS {safeIs, ...}) = - let - val th' = flat_rule ctxt th; - val rl = (th', swapify [th']); - val r = trim_context (th, rl, rl); - val _ = - warn_rules ctxt "Ignoring duplicate safe introduction (intro!)\n" safeIs r orelse - warn_claset ctxt r cs; - in add_safe_intro w r cs end; - -fun addSE w ctxt th (cs as CS {safeEs, ...}) = - let - val _ = Thm.no_prems th andalso bad_thm ctxt "Ill-formed elimination rule" th; - val th' = classical_rule ctxt (flat_rule ctxt th); - val rl = (th', []); - val r = trim_context (th, rl, rl); - val _ = - warn_rules ctxt "Ignoring duplicate safe elimination (elim!)\n" safeEs r orelse - warn_claset ctxt r cs; - in add_safe_elim w r cs end; + let val info = make_info1 (no_swapped_rl (classical_rule ctxt (flat_rule ctxt th))) th + in extend_rules ctxt Bires.elim_bang_kind w (th, info) cs end; fun addSD w ctxt th = addSE w ctxt (make_elim ctxt th); -fun addI w ctxt th (cs as CS {unsafeIs, ...}) = +fun addI w ctxt th cs = let val th' = flat_rule ctxt th; - val dup_th' = dup_intr th' handle THM _ => bad_thm ctxt "Ill-formed introduction rule" th; - val r = trim_context (th, (th', swapify [th']), (dup_th', swapify [dup_th'])); - val _ = - warn_rules ctxt "Ignoring duplicate introduction (intro)\n" unsafeIs r orelse - warn_claset ctxt r cs; - in add_unsafe_intro w r cs end; + val dup_th' = dup_intr th' handle THM _ => err_thm ctxt "Ill-formed introduction rule" th; + val info = make_info (maybe_swapped_rl th') (maybe_swapped_rl dup_th') th; + in extend_rules ctxt Bires.intro_kind w (th, info) cs end; -fun addE w ctxt th (cs as CS {unsafeEs, ...}) = +fun addE w ctxt th cs = let - val _ = Thm.no_prems th andalso bad_thm ctxt "Ill-formed elimination rule" th; + val _ = Thm.no_prems th andalso err_thm ctxt "Ill-formed elimination rule" th; val th' = classical_rule ctxt (flat_rule ctxt th); - val dup_th' = dup_elim ctxt th' handle THM _ => bad_thm ctxt "Ill-formed elimination rule" th; - val r = trim_context (th, (th', []), (dup_th', [])); - val _ = - warn_rules ctxt "Ignoring duplicate elimination (elim)\n" unsafeEs r orelse - warn_claset ctxt r cs; - in add_unsafe_elim w r cs end; + val dup_th' = dup_elim ctxt th' handle THM _ => err_thm ctxt "Ill-formed elimination rule" th; + val info = make_info (no_swapped_rl th') (no_swapped_rl dup_th') th; + in extend_rules ctxt Bires.elim_kind w (th, info) cs end; fun addD w ctxt th = addE w ctxt (make_elim ctxt th); - -(*** delete rules ***) - -local - -fun del_safe_intro (r: rule) - (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = - let - val (th, rl, _) = r; - val (safe0_rls, safep_rls) = List.partition (Thm.no_prems o fst) [rl]; - in - CS - {safe0_netpair = delete (map fst safe0_rls, maps snd safe0_rls) safe0_netpair, - safep_netpair = delete (map fst safep_rls, maps snd safep_rls) safep_netpair, - safeIs = Item_Net.remove r safeIs, - safeEs = safeEs, - unsafeIs = unsafeIs, - unsafeEs = unsafeEs, - swrappers = swrappers, - uwrappers = uwrappers, - unsafe_netpair = unsafe_netpair, - dup_netpair = dup_netpair, - extra_netpair = delete ([th], []) extra_netpair} - end; - -fun del_safe_elim (r: rule) - (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = - let - val (th, rl, _) = r; - val (safe0_rls, safep_rls) = List.partition (Thm.one_prem o #1) [rl]; - in - CS - {safe0_netpair = delete ([], map fst safe0_rls) safe0_netpair, - safep_netpair = delete ([], map fst safep_rls) safep_netpair, - safeIs = safeIs, - safeEs = Item_Net.remove r safeEs, - unsafeIs = unsafeIs, - unsafeEs = unsafeEs, - swrappers = swrappers, - uwrappers = uwrappers, - unsafe_netpair = unsafe_netpair, - dup_netpair = dup_netpair, - extra_netpair = delete ([], [th]) extra_netpair} - end; - -fun del_unsafe_intro (r as (th, (th', swapped_th'), (dup_th', swapped_dup_th'))) - (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = - CS - {unsafe_netpair = delete ([th'], swapped_th') unsafe_netpair, - dup_netpair = delete ([dup_th'], swapped_dup_th') dup_netpair, - safeIs = safeIs, - safeEs = safeEs, - unsafeIs = Item_Net.remove r unsafeIs, - unsafeEs = unsafeEs, - swrappers = swrappers, - uwrappers = uwrappers, - safe0_netpair = safe0_netpair, - safep_netpair = safep_netpair, - extra_netpair = delete ([th], []) extra_netpair}; - -fun del_unsafe_elim (r as (th, (th', _), (dup_th', _))) - (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = - CS - {unsafe_netpair = delete ([], [th']) unsafe_netpair, - dup_netpair = delete ([], [dup_th']) dup_netpair, - safeIs = safeIs, - safeEs = safeEs, - unsafeIs = unsafeIs, - unsafeEs = Item_Net.remove r unsafeEs, - swrappers = swrappers, - uwrappers = uwrappers, - safe0_netpair = safe0_netpair, - safep_netpair = safep_netpair, - extra_netpair = delete ([], [th]) extra_netpair}; - -fun del f rules th cs = - fold f (Item_Net.lookup rules (th, (th, []), (th, []))) cs; - -in - -fun delrule ctxt th (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, ...}) = - let - val th' = Tactic.make_elim th; - val r = (th, (th, []), (th, [])); - val r' = (th', (th', []), (th', [])); - in - if Item_Net.member safeIs r orelse Item_Net.member safeEs r orelse - Item_Net.member unsafeIs r orelse Item_Net.member unsafeEs r orelse - Item_Net.member safeEs r' orelse Item_Net.member unsafeEs r' - then - cs - |> del del_safe_intro safeIs th - |> del del_safe_elim safeEs th - |> del del_safe_elim safeEs th' - |> del del_unsafe_intro unsafeIs th - |> del del_unsafe_elim unsafeEs th - |> del del_unsafe_elim unsafeEs th' - else (warn_thm ctxt "Undeclared classical rule\n" th; cs) - end; - end; - -(** claset data **) - -(* wrappers *) +(* delete rules *) -fun map_swrappers f - (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = - CS {safeIs = safeIs, safeEs = safeEs, unsafeIs = unsafeIs, unsafeEs = unsafeEs, - swrappers = f swrappers, uwrappers = uwrappers, - safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, extra_netpair = extra_netpair}; - -fun map_uwrappers f - (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = - CS {safeIs = safeIs, safeEs = safeEs, unsafeIs = unsafeIs, unsafeEs = unsafeEs, - swrappers = swrappers, uwrappers = f uwrappers, - safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, extra_netpair = extra_netpair}; +fun delrule ctxt th cs = + let + val ths = th :: the_list (try Tactic.make_elim th); + val CS {decls, swrappers, uwrappers, + safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair} = cs; + val (old_decls, decls') = fold_map Bires.remove_decls ths decls |>> flat; + in + if null old_decls then (warn_thm ctxt (fn () => "Undeclared classical rule\n") th; cs) + else + let + 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; + val dup_netpair' = fold (del #dup_rl) old_decls dup_netpair; + val extra_netpair' = fold delete_plain_rule old_decls extra_netpair; + in + CS { + decls = decls', + swrappers = swrappers, + uwrappers = uwrappers, + safe0_netpair = safe0_netpair', + safep_netpair = safep_netpair', + unsafe_netpair = unsafe_netpair', + dup_netpair = dup_netpair', + extra_netpair = extra_netpair'} + end + end; -(* merge_cs *) - -(*Merge works by adding all new rules of the 2nd claset into the 1st claset, - in order to preserve priorities reliably.*) - -fun merge_thms add thms1 thms2 = - fold_rev (fn thm => if Item_Net.member thms1 thm then I else add thm) (Item_Net.content thms2); - -fun merge_cs (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, ...}, - cs' as CS {safeIs = safeIs2, safeEs = safeEs2, unsafeIs = unsafeIs2, unsafeEs = unsafeEs2, - swrappers, uwrappers, ...}) = - if pointer_eq (cs, cs') then cs - else - cs - |> merge_thms (add_safe_intro NONE) safeIs safeIs2 - |> merge_thms (add_safe_elim NONE) safeEs safeEs2 - |> merge_thms (add_unsafe_intro NONE) unsafeIs unsafeIs2 - |> merge_thms (add_unsafe_elim NONE) unsafeEs unsafeEs2 - |> map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers)) - |> map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers)); - - -(* data *) +(* Claset context data *) structure Claset = Generic_Data ( @@ -615,6 +476,14 @@ val claset_of = Claset.get o Context.Proof; val rep_claset_of = rep_cs o claset_of; +val dest_decls = Bires.dest_decls o #decls o rep_claset_of; + +val safe0_netpair_of = #safe0_netpair o rep_claset_of; +val safep_netpair_of = #safep_netpair o rep_claset_of; +val unsafe_netpair_of = #unsafe_netpair o rep_claset_of; +val dup_netpair_of = #dup_netpair o rep_claset_of; +val extra_netpair_of = #extra_netpair o rep_claset_of; + val get_cs = Claset.get; val map_cs = Claset.map; @@ -627,20 +496,6 @@ fun map_claset f = Context.proof_map (map_cs f); fun put_claset cs = map_claset (K cs); -fun print_claset ctxt = - let - val {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, ...} = rep_claset_of ctxt; - val pretty_thms = map (Thm.pretty_thm_item ctxt o #1) o Item_Net.content; - in - [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs), - Pretty.big_list "introduction rules (intro):" (pretty_thms unsafeIs), - Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs), - Pretty.big_list "elimination rules (elim):" (pretty_thms unsafeEs), - Pretty.strs ("safe wrappers:" :: map #1 swrappers), - Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)] - |> Pretty.chunks |> Pretty.writeln - end; - (* old-style declarations *) @@ -656,7 +511,21 @@ -(*** Modifying the wrapper tacticals ***) +(** Modifying the wrapper tacticals **) + +fun map_swrappers f + (CS {decls, swrappers, uwrappers, + safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = + CS {decls = decls, swrappers = f swrappers, uwrappers = uwrappers, + safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, + unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, extra_netpair = extra_netpair}; + +fun map_uwrappers f + (CS {decls, swrappers, uwrappers, + safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = + CS {decls = decls, swrappers = swrappers, uwrappers = f uwrappers, + safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, + unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, extra_netpair = extra_netpair}; fun appSWrappers ctxt = fold (fn (_, w) => w ctxt) (#swrappers (rep_claset_of ctxt)); fun appWrappers ctxt = fold (fn (_, w) => w ctxt) (#uwrappers (rep_claset_of ctxt)); @@ -684,13 +553,13 @@ fun ctxt delWrapper name = ctxt |> map_claset (map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name)); -(* compose a safe tactic alternatively before/after safe_step_tac *) +(*compose a safe tactic alternatively before/after safe_step_tac*) fun ctxt addSbefore (name, tac1) = ctxt addSWrapper (name, fn ctxt => fn tac2 => tac1 ctxt ORELSE' tac2); fun ctxt addSafter (name, tac2) = ctxt addSWrapper (name, fn ctxt => fn tac1 => tac1 ORELSE' tac2 ctxt); -(*compose a tactic alternatively before/after the step tactic *) +(*compose a tactic alternatively before/after the step tactic*) fun ctxt addbefore (name, tac1) = ctxt addWrapper (name, fn ctxt => fn tac2 => tac1 ctxt APPEND' tac2); fun ctxt addafter (name, tac2) = @@ -707,19 +576,17 @@ -(**** Simple tactics for theorem proving ****) +(** Simple tactics for theorem proving **) (*Attack subgoals using safe inferences -- matching, not resolution*) fun safe_step_tac ctxt = - let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in - appSWrappers ctxt - (FIRST' - [eq_assume_tac, - eq_mp_tac ctxt, - Bires.bimatch_from_nets_tac ctxt safe0_netpair, - FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs), - Bires.bimatch_from_nets_tac ctxt safep_netpair]) - end; + appSWrappers ctxt + (FIRST' + [eq_assume_tac, + eq_mp_tac ctxt, + Bires.bimatch_from_nets_tac ctxt (safe0_netpair_of ctxt), + FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs), + Bires.bimatch_from_nets_tac ctxt (safep_netpair_of ctxt)]); (*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*) fun safe_steps_tac ctxt = @@ -729,7 +596,8 @@ fun safe_tac ctxt = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac ctxt)); -(*** Clarify_tac: do safe steps without causing branching ***) + +(** Clarify_tac: do safe steps without causing branching **) (*version of Bires.bimatch_from_nets_tac that only applies rules that create precisely n subgoals.*) @@ -747,37 +615,36 @@ (*Attack subgoals using safe inferences -- matching, not resolution*) fun clarify_step_tac ctxt = - let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in - appSWrappers ctxt - (FIRST' - [eq_assume_contr_tac ctxt, - Bires.bimatch_from_nets_tac ctxt safe0_netpair, - FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs), - n_bimatch_from_nets_tac ctxt 1 safep_netpair, - bimatch2_tac ctxt safep_netpair]) - end; + appSWrappers ctxt + (FIRST' + [eq_assume_contr_tac ctxt, + Bires.bimatch_from_nets_tac ctxt (safe0_netpair_of ctxt), + FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs), + n_bimatch_from_nets_tac ctxt 1 (safep_netpair_of ctxt), + bimatch2_tac ctxt (safep_netpair_of ctxt)]); fun clarify_tac ctxt = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac ctxt 1)); -(*** Unsafe steps instantiate variables or lose information ***) + +(** Unsafe steps instantiate variables or lose information **) (*Backtracking is allowed among the various these unsafe ways of proving a subgoal. *) fun inst0_step_tac ctxt = assume_tac ctxt APPEND' contr_tac ctxt APPEND' - Bires.biresolve_from_nets_tac ctxt (#safe0_netpair (rep_claset_of ctxt)); + Bires.biresolve_from_nets_tac ctxt (safe0_netpair_of ctxt); (*These unsafe steps could generate more subgoals.*) fun instp_step_tac ctxt = - Bires.biresolve_from_nets_tac ctxt (#safep_netpair (rep_claset_of ctxt)); + Bires.biresolve_from_nets_tac ctxt (safep_netpair_of ctxt); (*These steps could instantiate variables and are therefore unsafe.*) fun inst_step_tac ctxt = inst0_step_tac ctxt APPEND' instp_step_tac ctxt; fun unsafe_step_tac ctxt = - Bires.biresolve_from_nets_tac ctxt (#unsafe_netpair (rep_claset_of ctxt)); + Bires.biresolve_from_nets_tac ctxt (unsafe_netpair_of ctxt); (*Single step for the prover. FAILS unless it makes progress. *) fun step_tac ctxt i = @@ -789,7 +656,7 @@ safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt APPEND' unsafe_step_tac ctxt) i; -(**** The following tactics all fail unless they solve one goal ****) +(** The following tactics all fail unless they solve one goal **) (*Dumb but fast*) fun fast_tac ctxt = @@ -814,7 +681,7 @@ SELECT_GOAL (BEST_FIRST (Thm.no_prems, Data.sizef) (slow_step_tac ctxt 1)); -(***ASTAR with weight weight_ASTAR, by Norbert Voelker*) +(** ASTAR with weight weight_ASTAR, by Norbert Voelker **) val weight_ASTAR = 5; @@ -831,16 +698,16 @@ (slow_step_tac ctxt 1)); -(**** Complete tactic, loosely based upon LeanTaP. This tactic is the outcome +(** Complete tactic, loosely based upon LeanTaP. This tactic is the outcome of much experimentation! Changing APPEND to ORELSE below would prove easy theorems faster, but loses completeness -- and many of the harder - theorems such as 43. ****) + theorems such as 43. **) (*Non-deterministic! Could always expand the first unsafe connective. That's hard to implement and did not perform better in experiments, due to greater search depth required.*) fun dup_step_tac ctxt = - Bires.biresolve_from_nets_tac ctxt (#dup_netpair (rep_claset_of ctxt)); + Bires.biresolve_from_nets_tac ctxt (dup_netpair_of ctxt); (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*) local @@ -866,7 +733,10 @@ fun deepen_tac ctxt = DEEPEN (2, 10) (safe_depth_tac ctxt); -(* attributes *) + +(** attributes **) + +(* declarations *) fun attrib f = Thm.declaration_attribute (fn th => fn context => @@ -886,8 +756,7 @@ |> Thm.attribute_declaration Context_Rules.rule_del th); - -(** concrete syntax of attributes **) +(* concrete syntax *) val introN = "intro"; val elimN = "elim"; @@ -915,8 +784,7 @@ fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) => let val [rules1, rules2, rules4] = Context_Rules.find_rules ctxt false facts goal; - val {extra_netpair, ...} = rep_claset_of ctxt; - val rules3 = Context_Rules.find_rules_netpair ctxt true facts goal extra_netpair; + val rules3 = Context_Rules.find_rules_netpair ctxt true facts goal (extra_netpair_of ctxt); val rules = rules1 @ rules2 @ rules3 @ rules4; val ruleq = Drule.multi_resolves (SOME ctxt) facts rules; val _ = Method.trace ctxt rules; @@ -952,8 +820,7 @@ fun cla_method' tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD' o tac); - -(** method setup **) +(* method setup *) val _ = Theory.setup @@ -988,7 +855,19 @@ "single classical step (safe rules, without splitting)"); -(** outer syntax **) + +(** outer syntax commands **) + +fun print_claset ctxt = + let + val {decls, swrappers, uwrappers, ...} = rep_claset_of ctxt; + val prt_rules = + Bires.pretty_decls ctxt + [Bires.intro_bang_kind, Bires.intro_kind, Bires.elim_bang_kind, Bires.elim_kind] decls; + val prt_wrappers = + [Pretty.strs ("safe wrappers:" :: map #1 swrappers), + Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)]; + in Pretty.writeln (Pretty.chunks (prt_rules @ prt_wrappers)) end; val _ = Outer_Syntax.command \<^command_keyword>\print_claset\ "print context of Classical Reasoner" diff -r 5e9c9f2c2cd8 -r 1e39653de974 src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Fri Jul 11 10:12:01 2025 +0200 +++ b/src/Pure/Isar/context_rules.ML Sat Jul 12 22:37:47 2025 +0200 @@ -37,72 +37,83 @@ (** rule declaration contexts **) +(* rule declarations *) + +type decl = thm Bires.decl; +type decls = thm Bires.decls; + +fun init_decl kind opt_weight th : decl = + let val weight = opt_weight |> \<^if_none>\Bires.subgoals_of (Bires.kind_rule kind th)\; + in {kind = kind, tag = Bires.weight_tag weight, info = th} end; + +fun insert_decl ({kind, tag, info = th}: decl) = + Bires.insert_tagged_rule (tag, Bires.kind_rule kind th); + +fun remove_decl ({tag = {index, ...}, info = th, ...}: decl) = + Bires.delete_tagged_rule (index, th); + + (* context data *) datatype rules = Rules of - {next: int, - rules: (int * (Bires.kind * thm)) list, + {decls: decls, netpairs: Bires.netpair list, wrappers: ((Proof.context -> (int -> tactic) -> int -> tactic) * stamp) list * ((Proof.context -> (int -> tactic) -> int -> tactic) * stamp) list}; -fun make_rules next rules netpairs wrappers = - Rules {next = next, rules = rules, netpairs = netpairs, wrappers = wrappers}; +fun make_rules decls netpairs wrappers = + Rules {decls = decls, netpairs = netpairs, wrappers = wrappers}; -fun add_rule kind opt_weight th (Rules {next, rules, netpairs, wrappers}) = +fun add_rule kind opt_weight th (rules as Rules {decls, netpairs, wrappers}) = let - val weight = opt_weight |> \<^if_none>\Bires.subgoals_of (Bires.kind_rule kind th)\; - val tag = {weight = weight, index = next}; val th' = Thm.trim_context th; - val rules' = (weight, (kind, th')) :: rules; - val netpairs' = netpairs - |> Bires.kind_map kind (Bires.insert_tagged_rule (tag, Bires.kind_rule kind th')); - in make_rules (next - 1) rules' netpairs' wrappers end; - -fun del_rule0 th (rs as Rules {next, rules, netpairs, wrappers}) = - let - fun eq_th (_, (_, th')) = Thm.eq_thm_prop (th, th'); - fun del b netpair = Bires.delete_tagged_rule (b, th) netpair handle Net.DELETE => netpair; - val rules' = filter_out eq_th rules; - val netpairs' = map (del false o del true) netpairs; + val decl' = init_decl kind opt_weight th'; in - if not (exists eq_th rules) then rs - else make_rules next rules' netpairs' wrappers + (case Bires.extend_decls (th', decl') decls of + (NONE, _) => rules + | (SOME new_decl, decls') => + let val netpairs' = Bires.kind_map kind (insert_decl new_decl) netpairs + in make_rules decls' netpairs' wrappers end) end; -fun del_rule th = del_rule0 th o del_rule0 (Tactic.make_elim th); +fun del_rule0 th (rules as Rules {decls, netpairs, wrappers}) = + (case Bires.remove_decls th decls of + ([], _) => rules + | (old_decls, decls') => + let + val netpairs' = + fold (fn decl as {kind, ...} => Bires.kind_map kind (remove_decl decl)) + old_decls netpairs; + in make_rules decls' netpairs' wrappers end); + +fun del_rule th = + fold del_rule0 (th :: the_list (try Tactic.make_elim th)); structure Data = Generic_Data ( type T = rules; - val empty = make_rules ~1 [] Bires.kind_netpairs ([], []); - fun merge - (Rules {rules = rules1, wrappers = (ws1, ws1'), ...}, - Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) = + val empty = make_rules Bires.empty_decls (Bires.kind_values Bires.empty_netpair) ([], []); + fun merge (rules1, rules2) = + if pointer_eq (rules1, rules2) then rules1 + else let + val Rules {decls = decls1, netpairs = netpairs1, wrappers = (ws1, ws1')} = rules1; + val Rules {decls = decls2, netpairs = _, wrappers = (ws2, ws2')} = rules2; + val (new_rules, decls) = Bires.merge_decls (decls1, decls2); + val netpairs = + netpairs1 |> map_index (uncurry (fn i => + new_rules |> fold (fn decl => + if Bires.kind_index (#kind decl) = i then insert_decl decl else I))) val wrappers = - (Library.merge (eq_snd (op =)) (ws1, ws2), Library.merge (eq_snd (op =)) (ws1', ws2')); - 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 (index, (weight, (kind, th))) => - Bires.kind_map kind - (Bires.insert_tagged_rule ({weight = weight, index = index}, (Bires.kind_elim kind, th)))) - (next upto ~1 ~~ rules) Bires.kind_netpairs; - in make_rules (next - 1) rules netpairs wrappers end; + (Library.merge (eq_snd (op =)) (ws1, ws2), + Library.merge (eq_snd (op =)) (ws1', ws2')); + in make_rules decls netpairs wrappers end; ); fun print_rules ctxt = - let - val Rules {rules, ...} = Data.get (Context.Proof ctxt); - fun prt_kind kind = - Pretty.big_list (Bires.kind_title kind ^ ":") - (map_filter (fn (_, (kind', th)) => - if kind = kind' then SOME (Thm.pretty_thm_item ctxt th) else NONE) - (sort (int_ord o apply2 fst) rules)); - in Pretty.writeln (Pretty.chunks (map prt_kind Bires.kind_domain)) end; + let val Rules {decls, ...} = Data.get (Context.Proof ctxt) + in Pretty.writeln (Pretty.chunks (Bires.pretty_decls ctxt Bires.kind_domain decls)) end; (* access data *) @@ -142,8 +153,8 @@ (* wrappers *) fun gen_add_wrapper upd w = - Context.theory_map (Data.map (fn Rules {next, rules, netpairs, wrappers} => - make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers))); + Context.theory_map (Data.map (fn Rules {decls, netpairs, wrappers} => + make_rules decls netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers))); val addSWrapper = gen_add_wrapper Library.apfst; val addWrapper = gen_add_wrapper Library.apsnd; diff -r 5e9c9f2c2cd8 -r 1e39653de974 src/Pure/bires.ML --- a/src/Pure/bires.ML Fri Jul 11 10:12:01 2025 +0200 +++ b/src/Pure/bires.ML Sat Jul 12 22:37:47 2025 +0200 @@ -13,18 +13,50 @@ val no_subgoals: rule -> bool type tag = {weight: int, index: int} - val tag0_ord: tag ord + val tag_weight_ord: tag ord + val tag_index_ord: tag ord val tag_ord: tag ord val weighted_tag_ord: bool -> tag ord val tag_order: (tag * 'a) list -> 'a list + val weight_tag: int -> tag + + eqtype kind + val intro_bang_kind: kind + val elim_bang_kind: kind + val intro_kind: kind + val elim_kind: kind + val intro_query_kind: kind + val elim_query_kind: kind + val kind_safe: kind -> bool + val kind_unsafe: kind -> bool + val kind_extra: kind -> bool + val kind_index: kind -> int + val kind_elim: kind -> bool + val kind_domain: kind list + val kind_values: 'a -> 'a list + val kind_map: kind -> ('a -> 'a) -> 'a list -> 'a list + val kind_rule: kind -> thm -> rule + val kind_description: kind -> string + val kind_title: kind -> string + + type 'a decl = {kind: kind, tag: tag, info: 'a} + val decl_ord: 'a decl ord + val decl_eq_kind: 'a decl * 'a decl -> bool + type 'a decls + val has_decls: 'a decls -> thm -> bool + val get_decls: 'a decls -> thm -> 'a decl list + val dest_decls: 'a decls -> (thm * 'a decl -> bool) -> (thm * 'a decl) list + val pretty_decls: Proof.context -> kind list -> 'a decls -> Pretty.T list + val merge_decls: 'a decls * 'a decls -> 'a decl list * 'a decls + val extend_decls: thm * 'a decl -> 'a decls -> 'a decl option * 'a decls + val remove_decls: thm -> 'a decls -> 'a decl list * 'a decls + val empty_decls: 'a decls 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: int * thm -> 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 @@ -35,27 +67,12 @@ val filt_resolve_from_net_tac: Proof.context -> int -> net -> int -> tactic val resolve_from_net_tac: Proof.context -> net -> int -> tactic val match_from_net_tac: Proof.context -> net -> int -> tactic - - eqtype kind - val intro_bang_kind: kind - val elim_bang_kind: kind - val intro_kind: kind - val elim_kind: kind - val intro_query_kind: kind - val elim_query_kind: kind - val kind_index: kind -> int - val kind_elim: kind -> bool - val kind_domain: kind list - val kind_netpairs: netpair list - val kind_map: kind -> ('a -> 'a) -> 'a list -> 'a list - val kind_rule: kind -> thm -> rule - val kind_title: kind -> string end structure Bires: BIRES = struct -(** Natural Deduction using (bires_flg, rule) pairs **) +(** Rule kinds and declarations **) (* type rule *) @@ -74,69 +91,21 @@ 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; +val tag_weight_ord: tag ord = int_ord o apply2 #weight; +val tag_index_ord: tag ord = int_ord o apply2 #index; -fun weighted_tag_ord weighted = if weighted then tag_ord else tag0_ord; +val tag_ord: tag ord = tag_weight_ord ||| tag_index_ord; + +fun weighted_tag_ord weighted = if weighted then tag_ord else tag_index_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 decreasing integers **) +fun weight_tag weight : tag = {weight = weight, index = 0}; -(*insert one tagged brl into the pair of nets*) -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, tagged_rule) enet) - | NONE => error "insert_tagged_rule: elimination rule with no premises") - 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; +fun next_tag next ({weight, ...}: tag) = {weight = weight, index = next}; -(*delete one kbrl from the pair of nets*) -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); - -fun delete_tagged_rules rls = fold_rev delete_tagged_rule rls; - -end; - -(*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 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 tag_ord NONE false; -fun bimatch_from_nets_tac ctxt = biresolution_from_nets_tac ctxt tag_ord NONE true; - - -(** Rule kinds and declarations **) +(* kind: intro! / elim! / intro / elim / intro? / elim? *) datatype kind = Kind of int * bool; @@ -155,23 +124,138 @@ (intro_query_kind, ("extra introduction", "(intro?)")), (elim_query_kind, ("extra elimination", "(elim?)"))]; +fun kind_safe (Kind (i, _)) = i = 0; +fun kind_unsafe (Kind (i, _)) = i = 1; +fun kind_extra (Kind (i, _)) = i = 2; fun kind_index (Kind (i, _)) = i; fun kind_elim (Kind (_, b)) = b; val kind_domain = map #1 kind_infos; -val kind_netpairs = - replicate (length (distinct (op =) (map kind_index kind_domain))) empty_netpair; + +fun kind_values x = + replicate (length (distinct (op =) (map kind_index kind_domain))) x; fun kind_map kind f = nth_map (kind_index kind) f; fun kind_rule kind thm : rule = (kind_elim kind, thm); val the_kind_info = the o AList.lookup (op =) kind_infos; +fun kind_description kind = + let val (a, b) = the_kind_info kind + in a ^ " " ^ b end; + fun kind_title kind = let val (a, b) = the_kind_info kind in a ^ " rules " ^ b end; +(* rule declarations in canonical order *) + +type 'a decl = {kind: kind, tag: tag, info: 'a}; + +fun decl_ord (args: 'a decl * 'a decl) = tag_index_ord (apply2 #tag args); + +fun decl_eq_kind ({kind, ...}: 'a decl, {kind = kind', ...}: 'a decl) = kind = kind'; + +fun next_decl next ({kind, tag, info}: 'a decl) : 'a decl = + {kind = kind, tag = next_tag next tag, info = info}; + + +abstype 'a decls = Decls of {next: int, rules: 'a decl list Proptab.table} +with + +local + +fun dup_decls (Decls {rules, ...}) (thm, decl) = + member decl_eq_kind (Proptab.lookup_list rules thm) decl; + +fun add_decls (thm, decl) (Decls {next, rules}) = + let + val decl' = next_decl next decl; + val decls' = Decls {next = next - 1, rules = Proptab.cons_list (thm, decl') rules}; + in (decl', decls') end; + +in + +fun has_decls (Decls {rules, ...}) = Proptab.defined rules; + +fun get_decls (Decls {rules, ...}) = Proptab.lookup_list rules; + +fun dest_decls (Decls {rules, ...}) pred = + build (rules |> Proptab.fold (fn (th, ds) => ds |> fold (fn d => pred (th, d) ? cons (th, d)))) + |> sort (decl_ord o apply2 #2); + +fun pretty_decls ctxt kinds decls = + kinds |> map (fn kind => + Pretty.big_list (kind_title kind ^ ":") + (dest_decls decls (fn (_, {kind = kind', ...}) => kind = kind') + |> map (fn (th, _) => Thm.pretty_thm_item ctxt th))); + +fun merge_decls (decls1, decls2) = + decls1 |> fold_map add_decls (rev (dest_decls decls2 (not o dup_decls decls1))); + +fun extend_decls (thm, decl) decls = + if dup_decls decls (thm, decl) then (NONE, decls) + else add_decls (thm, decl) decls |>> SOME; + +fun remove_decls thm (decls as Decls {next, rules}) = + (case get_decls decls thm of + [] => ([], decls) + | old_decls => (old_decls, Decls {next = next, rules = Proptab.delete thm rules})); + +val empty_decls = Decls {next = ~1, rules = Proptab.empty}; + +end; + +end; + + +(* discrimination nets for intr/elim rules *) + +type netpair = (tag * rule) Net.net * (tag * rule) Net.net; + +val empty_netpair: netpair = (Net.empty, Net.empty); + + +(** Natural Deduction using (bires_flg, rule) pairs **) + +(** To preserve the order of the rules, tag them with decreasing integers **) + +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, tagged_rule) enet) + | NONE => error "insert_tagged_rule: elimination rule with no premises") + else (Net.insert_term (K false) (Thm.concl_of th, tagged_rule) inet, enet); + +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: + 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 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 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 **) type net = (int * thm) Net.net; diff -r 5e9c9f2c2cd8 -r 1e39653de974 src/Pure/cterm_items.ML --- a/src/Pure/cterm_items.ML Fri Jul 11 10:12:01 2025 +0200 +++ b/src/Pure/cterm_items.ML Sat Jul 12 22:37:47 2025 +0200 @@ -43,6 +43,12 @@ end; +structure Proptab = Table +( + type key = thm + val ord = pointer_eq_ord (Term_Ord.fast_term_ord o apply2 Thm.full_prop_of) +); + structure Thmtab: sig include TABLE diff -r 5e9c9f2c2cd8 -r 1e39653de974 src/ZF/IntDiv.thy --- a/src/ZF/IntDiv.thy Fri Jul 11 10:12:01 2025 +0200 +++ b/src/ZF/IntDiv.thy Sat Jul 12 22:37:47 2025 +0200 @@ -304,8 +304,7 @@ apply (auto simp add: not_zless_iff_zle not_zle_iff_zless [THEN iff_sym, of "m$*k"] not_zle_iff_zless [THEN iff_sym, of m]) -apply (auto elim: notE - simp add: zless_imp_zle zmult_zle_mono1 zmult_zle_mono1_neg) +apply (auto simp add: zless_imp_zle zmult_zle_mono1 zmult_zle_mono1_neg) done lemma zmult_zless_cancel2: