# HG changeset patch
# User wenzelm
# Date 1752267829 -7200
# Node ID 7f9c4466c6a550f6c6f1d77215b7cea8753b6c08
# Parent  3020b1660bec2b8f09254419a018b99748489b65
proper "plain" rule for extra_netpair (amending 8aa1c98b948b): need to avoid flat_rule / Object_Logic.atomize_prems for the sake of "standard" Isar proof, e.g. (line 34 of "$AFP/AWN/Qmsg_Lifting.thy);

diff -r 3020b1660bec -r 7f9c4466c6a5 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Jul 11 21:39:03 2025 +0200
+++ b/src/Provers/classical.ML	Fri Jul 11 23:03:49 2025 +0200
@@ -96,7 +96,7 @@
   include BASIC_CLASSICAL
   val classical_rule: Proof.context -> thm -> thm
   type rl = thm * thm option
-  type info = {rl: rl, dup_rl: rl}
+  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
@@ -215,7 +215,7 @@
 (**** Classical rule sets ****)
 
 type rl = thm * thm option;  (*internal form, with possibly swapped version*)
-type info = {rl: rl, dup_rl: rl};
+type info = {rl: rl, dup_rl: rl, plain: thm};
 type rule = thm * info;  (*external form, internal forms*)
 
 type decl = info Bires.decl;
@@ -224,8 +224,8 @@
 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 : info = {rl = rl, dup_rl = dup_rl};
-fun make_info1 rl : info = make_info rl rl;
+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;
 
@@ -270,10 +270,10 @@
   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 insert_plain_rule ({kind, tag, info = {plain = th, ...}}: decl) =
+  Bires.insert_tagged_rule (tag, (Bires.kind_rule kind th));
 
-fun delete_plain_rule ({tag = {index, ...}, info = {rl = (th, _), ...}, ...}: decl) =
+fun delete_plain_rule ({tag = {index, ...}, info = {plain = th, ...}, ...}: decl) =
   Bires.delete_tagged_rule (index, th);
 
 fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th);
@@ -337,7 +337,7 @@
 
 fun add_unsafe_rule (decl: decl) ((safe_netpairs, (unsafe_netpair, dup_netpair)): netpairs) =
   let
-    val {kind, tag = {index, ...}, info = {rl, dup_rl}} = decl;
+    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;
@@ -351,8 +351,8 @@
 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} : info =
-  {rl = trim_context_rl rl, dup_rl = trim_context_rl dup_rl};
+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 extend_rules ctxt kind opt_weight (th, info) cs =
   let
@@ -410,12 +410,12 @@
 
 fun addSI w ctxt th cs =
   extend_rules ctxt Bires.intro_bang_kind w
-    (th, make_info1 (maybe_swapped_rl (flat_rule ctxt th))) cs;
+    (th, make_info1 (maybe_swapped_rl (flat_rule ctxt th)) th) cs;
 
 fun addSE w ctxt th cs =
   if Thm.no_prems th then bad_thm ctxt "Ill-formed elimination rule" th
   else
-    let val info = make_info1 (no_swapped_rl (classical_rule ctxt (flat_rule ctxt th)))
+    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);
@@ -424,7 +424,7 @@
   let
     val th' = flat_rule ctxt th;
     val dup_th' = dup_intr th' handle THM _ => bad_thm ctxt "Ill-formed introduction rule" th;
-    val info = make_info (maybe_swapped_rl th') (maybe_swapped_rl dup_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 =
@@ -432,7 +432,7 @@
     val _ = Thm.no_prems th andalso bad_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 info = make_info (no_swapped_rl th') (no_swapped_rl dup_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);