# HG changeset patch # User wenzelm # Date 1752483466 -7200 # Node ID af6f55b15749f409dbfd5e077de4651dbaeb8a5f # Parent 81400a301993d68015aad8e04469e77077a430b1 tuned; diff -r 81400a301993 -r af6f55b15749 src/Provers/classical.ML --- a/src/Provers/classical.ML Sun Jul 13 17:29:48 2025 +0100 +++ b/src/Provers/classical.ML Mon Jul 14 10:57:46 2025 +0200 @@ -287,6 +287,9 @@ fun err_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th); +fun err_thm_illformed ctxt kind th = + err_thm ctxt ("Ill-formed " ^ Bires.kind_name kind) th; + fun make_elim ctxt th = if Thm.no_prems th then err_thm ctxt "Ill-formed destruction rule" th else Tactic.make_elim th; @@ -405,27 +408,30 @@ (th, make_info1 (maybe_swapped_rl (flat_rule ctxt th)) th) cs; fun addSE w ctxt th cs = - if Thm.no_prems th then err_thm ctxt "Ill-formed elimination rule" th - else - 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; + let + val kind = Bires.elim_bang_kind; + val _ = Thm.no_prems th andalso err_thm_illformed ctxt kind th; + val info = make_info1 (no_swapped_rl (classical_rule ctxt (flat_rule ctxt th))) th; + in extend_rules ctxt kind w (th, info) cs end; fun addSD w ctxt th = addSE w ctxt (make_elim ctxt th); fun addI w ctxt th cs = let + val kind = Bires.intro_kind; val th' = flat_rule ctxt th; - val dup_th' = dup_intr th' handle THM _ => err_thm ctxt "Ill-formed introduction rule" th; + val dup_th' = dup_intr th' handle THM _ => err_thm_illformed ctxt kind 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; + in extend_rules ctxt kind w (th, info) cs end; fun addE w ctxt th cs = let - val _ = Thm.no_prems th andalso err_thm ctxt "Ill-formed elimination rule" th; + val kind = Bires.elim_kind; + val _ = Thm.no_prems th andalso err_thm_illformed ctxt kind th; val th' = classical_rule ctxt (flat_rule ctxt th); - val dup_th' = dup_elim ctxt th' handle THM _ => err_thm ctxt "Ill-formed elimination rule" th; + val dup_th' = dup_elim ctxt th' handle THM _ => err_thm_illformed ctxt kind th 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; + in extend_rules ctxt kind w (th, info) cs end; fun addD w ctxt th = addE w ctxt (make_elim ctxt th); diff -r 81400a301993 -r af6f55b15749 src/Pure/bires.ML --- a/src/Pure/bires.ML Sun Jul 13 17:29:48 2025 +0100 +++ b/src/Pure/bires.ML Mon Jul 14 10:57:46 2025 +0200 @@ -32,6 +32,7 @@ val kind_extra: kind -> bool val kind_index: kind -> int val kind_elim: kind -> bool + val kind_name: kind -> string val kind_domain: kind list val kind_values: 'a -> 'a list val kind_map: kind -> ('a -> 'a) -> 'a list -> 'a list @@ -130,6 +131,9 @@ fun kind_index (Kind (i, _)) = i; fun kind_elim (Kind (_, b)) = b; +fun kind_name kind = + if kind_elim kind then "elimination rule" else "introduction rule"; + val kind_domain = map #1 kind_infos; fun kind_values x =