--- 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 =>
--- 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 =>
--- 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])]);
--- 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;