# HG changeset patch
# User wenzelm
# Date 1752569325 -7200
# Node ID c2a88a1cd07d122776ca9bb2ed717f536a923733
# Parent  75064081894e61b8dbba3fdd4916424e7b10be50
explicit "dest" rules: no longer declare [elim_format, elim];

diff -r 75064081894e -r c2a88a1cd07d src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Mon Jul 14 22:58:27 2025 +0200
+++ b/src/Provers/clasimp.ML	Tue Jul 15 10:48:45 2025 +0200
@@ -56,6 +56,21 @@
 
 local
 
+val safe_atts =
+ {intro = Classical.safe_intro NONE,
+  elim = Classical.safe_elim NONE,
+  dest = Classical.safe_dest NONE};
+
+val unsafe_atts =
+ {intro = Classical.unsafe_intro NONE,
+  elim = Classical.unsafe_elim NONE,
+  dest = Classical.unsafe_dest NONE};
+
+val pure_atts =
+ {intro = Context_Rules.intro_query NONE,
+  elim = Context_Rules.elim_query NONE,
+  dest = Context_Rules.dest_query NONE};
+
 (*Takes (possibly conditional) theorems of the form A<->B to
         the Safe Intr     rule B==>A and
         the Safe Destruct rule A==>B.
@@ -66,11 +81,11 @@
   Thm.declaration_attribute (fn th => fn context =>
     let
       val n = Thm.nprems_of th;
-      val (elim, intro) = if n = 0 then safe else unsafe;
+      val {intro, elim, dest} = if n = 0 then safe else unsafe;
       val zero_rotate = zero_var_indexes o rotate_prems n;
       val decls =
         [(intro, zero_rotate (th RS Data.iffD2)),
-         (elim, Tactic.make_elim (zero_rotate (th RS Data.iffD1)))]
+         (dest, zero_rotate (th RS Data.iffD1))]
         handle THM _ => [(elim, zero_rotate (th RS Data.notE))]
         handle THM _ => [(intro, th)];
     in fold (uncurry Thm.attribute_declaration) decls context end);
@@ -79,7 +94,7 @@
   let
     val zero_rotate = zero_var_indexes o rotate_prems (Thm.nprems_of th);
     val rls =
-      [zero_rotate (th RS Data.iffD2), Tactic.make_elim (zero_rotate (th RS Data.iffD1))]
+      [zero_rotate (th RS Data.iffD2), zero_rotate (th RS Data.iffD1)]
         handle THM _ => [zero_rotate (th RS Data.notE)]
         handle THM _ => [th];
   in fold (Thm.attribute_declaration del) rls context end);
@@ -88,15 +103,10 @@
 
 val iff_add =
   Thm.declaration_attribute (fn th =>
-    Thm.attribute_declaration (add_iff
-      (Classical.safe_elim NONE, Classical.safe_intro NONE)
-      (Classical.unsafe_elim NONE, Classical.unsafe_intro NONE)) th
+    Thm.attribute_declaration (add_iff safe_atts unsafe_atts) th
     #> Thm.attribute_declaration Simplifier.simp_add th);
 
-val iff_add' =
-  add_iff
-    (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE)
-    (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE);
+val iff_add' = add_iff pure_atts pure_atts;
 
 val iff_del =
   Thm.declaration_attribute (fn th =>
diff -r 75064081894e -r c2a88a1cd07d src/Provers/classical.ML
--- a/src/Provers/classical.ML	Mon Jul 14 22:58:27 2025 +0200
+++ b/src/Provers/classical.ML	Tue Jul 15 10:48:45 2025 +0200
@@ -290,10 +290,6 @@
 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;
-
 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;
@@ -313,8 +309,10 @@
   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.dest_bang_kind orelse
     warn Bires.intro_kind orelse
-    warn Bires.elim_kind
+    warn Bires.elim_kind orelse
+    warn Bires.dest_kind
   end;
 
 
@@ -352,20 +350,23 @@
 fun ext_info ctxt kind th =
   if kind = Bires.intro_bang_kind then
     make_info1 (maybe_swapped_rl (flat_rule ctxt th)) th
-  else if kind = Bires.elim_bang_kind then
-    let val _ = Thm.no_prems th andalso err_thm_illformed ctxt kind th
-    in make_info1 (no_swapped_rl (classical_rule ctxt (flat_rule ctxt th))) th end
+  else if kind = Bires.elim_bang_kind orelse kind = Bires.dest_bang_kind then
+    let
+      val _ = Thm.no_prems th andalso err_thm_illformed ctxt kind th;
+      val elim = if Bires.kind_make_elim kind then Tactic.make_elim th else th;
+    in make_info1 (no_swapped_rl (classical_rule ctxt (flat_rule ctxt elim))) elim end
   else if kind = Bires.intro_kind then
     let
       val th' = flat_rule ctxt th;
       val dup_th' = dup_intr th' handle THM _ => err_thm_illformed ctxt kind th;
     in make_info (maybe_swapped_rl th') (maybe_swapped_rl dup_th') th end
-  else if kind = Bires.elim_kind then
+  else if kind = Bires.elim_kind orelse kind = Bires.dest_kind then
     let
       val _ = Thm.no_prems th andalso err_thm_illformed ctxt kind th;
-      val th' = classical_rule ctxt (flat_rule ctxt th);
+      val elim = if Bires.kind_make_elim kind then Tactic.make_elim th else th;
+      val th' = classical_rule ctxt (flat_rule ctxt elim);
       val dup_th' = dup_elim ctxt th' handle THM _ => err_thm_illformed ctxt kind th;
-    in make_info (no_swapped_rl th') (no_swapped_rl dup_th') th end
+    in make_info (no_swapped_rl th') (no_swapped_rl dup_th') elim end
   else raise Fail "Bad rule kind";
 
 in
@@ -429,10 +430,9 @@
 
 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;
+    val (old_decls, decls') = Bires.remove_decls th decls;
   in
     if null old_decls then (warn_thm ctxt (fn () => "Undeclared classical rule\n") th; cs)
     else
@@ -492,15 +492,15 @@
 
 (* old-style ML declarations *)
 
-fun ml_decl kind view (ctxt, ths) =
-  map_claset (fold_rev (extend_rules ctxt kind NONE o view ctxt) ths) ctxt;
+fun ml_decl kind (ctxt, ths) =
+  map_claset (fold_rev (extend_rules ctxt kind NONE) ths) ctxt;
 
-val op addSIs = ml_decl Bires.intro_bang_kind (K I);
-val op addSEs = ml_decl Bires.elim_bang_kind (K I);
-val op addSDs = ml_decl Bires.elim_bang_kind make_elim;
-val op addIs = ml_decl Bires.intro_kind (K I);
-val op addEs = ml_decl Bires.elim_kind (K I);
-val op addDs = ml_decl Bires.elim_kind make_elim;
+val op addSIs = ml_decl Bires.intro_bang_kind;
+val op addSEs = ml_decl Bires.elim_bang_kind;
+val op addSDs = ml_decl Bires.dest_bang_kind;
+val op addIs = ml_decl Bires.intro_kind;
+val op addEs = ml_decl Bires.elim_kind;
+val op addDs = ml_decl Bires.dest_kind;
 
 fun ctxt delrules ths = map_claset (fold_rev (delrule ctxt) ths) ctxt;
 
@@ -733,17 +733,16 @@
 
 (* declarations *)
 
-fun attrib kind view w =
+fun attrib kind w =
   Thm.declaration_attribute (fn th => fn context =>
-    let val ctxt = Context.proof_of context
-    in map_cs (extend_rules ctxt kind w (view ctxt th)) context end);
+    map_cs (extend_rules (Context.proof_of context) kind w th) context);
 
-val safe_intro = attrib Bires.intro_bang_kind (K I);
-val safe_elim = attrib Bires.elim_bang_kind (K I);
-val safe_dest = attrib Bires.elim_bang_kind make_elim;
-val unsafe_intro = attrib Bires.intro_kind (K I);
-val unsafe_elim = attrib Bires.elim_kind (K I);
-val unsafe_dest = attrib Bires.elim_kind make_elim;
+val safe_intro = attrib Bires.intro_bang_kind;
+val safe_elim = attrib Bires.elim_bang_kind;
+val safe_dest = attrib Bires.dest_bang_kind;
+val unsafe_intro = attrib Bires.intro_kind;
+val unsafe_elim = attrib Bires.elim_kind;
+val unsafe_dest = attrib Bires.dest_kind;
 
 val rule_del =
   Thm.declaration_attribute (fn th => fn context =>
diff -r 75064081894e -r c2a88a1cd07d src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Mon Jul 14 22:58:27 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML	Tue Jul 15 10:48:45 2025 +0200
@@ -68,7 +68,8 @@
 fun add_rule kind opt_weight th (rules as Rules {decls, netpairs, wrappers}) =
   let
     val th' = Thm.trim_context th;
-    val decl' = init_decl kind opt_weight th';
+    val th'' = if Bires.kind_make_elim kind then Thm.trim_context (Tactic.make_elim th) else th';
+    val decl' = init_decl kind opt_weight th'';
   in
     (case Bires.extend_decls (th', decl') decls of
       (NONE, _) => rules
@@ -77,7 +78,7 @@
         in make_rules decls' netpairs' wrappers end)
   end;
 
-fun del_rule0 th (rules as Rules {decls, netpairs, wrappers}) =
+fun del_rule th (rules as Rules {decls, netpairs, wrappers}) =
   (case Bires.remove_decls th decls of
     ([], _) => rules
   | (old_decls, decls') =>
@@ -87,9 +88,6 @@
             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;
@@ -173,21 +171,20 @@
 
 (* add and del rules *)
 
-
 val rule_del = Thm.declaration_attribute (Data.map o del_rule);
 
-fun rule_add k view opt_w =
-  Thm.declaration_attribute (fn th => Data.map (add_rule k opt_w (view th) o del_rule th));
+fun rule_add k opt_w =
+  Thm.declaration_attribute (fn th => Data.map (add_rule k opt_w th o del_rule th));
 
-val intro_bang  = rule_add Bires.intro_bang_kind I;
-val elim_bang   = rule_add Bires.elim_bang_kind I;
-val dest_bang   = rule_add Bires.elim_bang_kind Tactic.make_elim;
-val intro       = rule_add Bires.intro_kind I;
-val elim        = rule_add Bires.elim_kind I;
-val dest        = rule_add Bires.elim_kind Tactic.make_elim;
-val intro_query = rule_add Bires.intro_query_kind I;
-val elim_query  = rule_add Bires.elim_query_kind I;
-val dest_query  = rule_add Bires.elim_query_kind Tactic.make_elim;
+val intro_bang  = rule_add Bires.intro_bang_kind;
+val elim_bang   = rule_add Bires.elim_bang_kind;
+val dest_bang   = rule_add Bires.dest_bang_kind;
+val intro       = rule_add Bires.intro_kind;
+val elim        = rule_add Bires.elim_kind;
+val dest        = rule_add Bires.dest_kind;
+val intro_query = rule_add Bires.intro_query_kind;
+val elim_query  = rule_add Bires.elim_query_kind;
+val dest_query  = rule_add Bires.dest_query_kind;
 
 val _ = Theory.setup
   (snd o Global_Theory.add_thms [((Binding.empty, Drule.equal_intr_rule), [intro_query NONE])]);
diff -r 75064081894e -r c2a88a1cd07d src/Pure/bires.ML
--- a/src/Pure/bires.ML	Mon Jul 14 22:58:27 2025 +0200
+++ b/src/Pure/bires.ML	Tue Jul 15 10:48:45 2025 +0200
@@ -23,15 +23,19 @@
   eqtype kind
   val intro_bang_kind: kind
   val elim_bang_kind: kind
+  val dest_bang_kind: kind
   val intro_kind: kind
   val elim_kind: kind
+  val dest_kind: kind
   val intro_query_kind: kind
   val elim_query_kind: kind
+  val dest_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_is_elim: kind -> bool
+  val kind_make_elim: kind -> bool
   val kind_name: kind -> string
   val kind_domain: kind list
   val kind_values: 'a -> 'a list
@@ -106,33 +110,48 @@
 fun next_tag next ({weight, ...}: tag) = {weight = weight, index = next};
 
 
-(* kind: intro! / elim! / intro / elim / intro? / elim? *)
+(* kind: intro/elim/dest *)
+
+datatype kind = Kind of {index: int, is_elim: bool, make_elim: bool};
 
-datatype kind = Kind of int * bool;
+fun make_intro_kind i = Kind {index = i, is_elim = false, make_elim = false};
+fun make_elim_kind i = Kind {index = i, is_elim = true, make_elim = false};
+fun make_dest_kind i = Kind {index = i, is_elim = true, make_elim = true};
 
-val intro_bang_kind = Kind (0, false);
-val elim_bang_kind = Kind (0, true);
-val intro_kind = Kind (1, false);
-val elim_kind = Kind (1, true);
-val intro_query_kind = Kind (2, false);
-val elim_query_kind = Kind (2, true);
+val intro_bang_kind = make_intro_kind 0;
+val elim_bang_kind = make_elim_kind 0;
+val dest_bang_kind = make_dest_kind 0;
+
+val intro_kind = make_intro_kind 1;
+val elim_kind = make_elim_kind 1;
+val dest_kind = make_dest_kind 1;
+
+val intro_query_kind = make_intro_kind 2;
+val elim_query_kind = make_elim_kind 2;
+val dest_query_kind = make_dest_kind 2;
 
 val kind_infos =
  [(intro_bang_kind, ("safe introduction", "(intro!)")),
   (elim_bang_kind, ("safe elimination", "(elim!)")),
+  (dest_bang_kind, ("safe destruction", "(dest!)")),
   (intro_kind, ("unsafe introduction", "(intro)")),
   (elim_kind, ("unsafe elimination", "(elim)")),
+  (dest_kind, ("unsafe destruction", "(dest)")),
   (intro_query_kind, ("extra introduction", "(intro?)")),
-  (elim_query_kind, ("extra elimination", "(elim?)"))];
+  (elim_query_kind, ("extra elimination", "(elim?)")),
+  (dest_query_kind, ("extra destruction", "(dest?)"))];
 
-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;
+fun kind_safe (Kind {index, ...}) = index = 0;
+fun kind_unsafe (Kind {index, ...}) = index = 1;
+fun kind_extra (Kind {index, ...}) = index = 2;
+fun kind_index (Kind {index, ...}) = index;
+fun kind_is_elim (Kind {is_elim, ...}) = is_elim;
+fun kind_make_elim (Kind {make_elim, ...}) = make_elim;
 
-fun kind_name kind =
-  if kind_elim kind then "elimination rule" else "introduction rule";
+fun kind_name (Kind {is_elim, make_elim, ...}) =
+  if is_elim andalso make_elim then "destruction rule"
+  else if is_elim then "elimination rule"
+  else "introduction rule";
 
 val kind_domain = map #1 kind_infos;
 
@@ -140,7 +159,7 @@
   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);
+fun kind_rule kind thm : rule = (kind_is_elim kind, thm);
 
 val the_kind_info = the o AList.lookup (op =) kind_infos;