--- a/NEWS Tue Jul 15 21:18:04 2025 +0100
+++ b/NEWS Tue Jul 15 23:13:12 2025 +0200
@@ -16,6 +16,16 @@
state output (if enabled). This affects Isabelle/jEdit panels for Output
vs. State in particular.
+* Declarations of intro/elim/dest rules for Pure and the Classical
+Reasoner (e.g. HOL) are handled more uniformly and efficiently: the
+order of rule declarations is maintained accurately, regardless of
+intermediate [rule del] declarations. Furthermore, [dest] is now a
+proper declaration on its own account, instead of the former expansion
+[elim_format, elim]. Consequently, [rule del] no longer deletes the
+[elim_format] of the given rule, only the original rule. Rare
+INCOMPATIBILITY: tools like "blast" and "auto" may fail in unusual
+situations.
+
* A Prover IDE session, e.g. in Isabelle/jEdit or Isabelle/VSCode, is
now able to load markup and messages from the underlying session
database. Example: "isabelle jedit -l HOL src/HOL/Nat.thy" for theory
--- a/src/HOL/Hahn_Banach/Function_Norm.thy Tue Jul 15 21:18:04 2025 +0100
+++ b/src/HOL/Hahn_Banach/Function_Norm.thy Tue Jul 15 23:13:12 2025 +0200
@@ -151,7 +151,7 @@
then show ?thesis unfolding fn_norm_def by (rule the_lubI_ex)
qed
-lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]:
+lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [intro?]:
assumes "continuous V f norm"
assumes b: "b \<in> B V f"
shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
--- a/src/HOL/Hahn_Banach/Normed_Space.thy Tue Jul 15 21:18:04 2025 +0100
+++ b/src/HOL/Hahn_Banach/Normed_Space.thy Tue Jul 15 23:13:12 2025 +0200
@@ -19,9 +19,9 @@
locale seminorm =
fixes V :: "'a::{minus, plus, zero, uminus} set"
fixes norm :: "'a \<Rightarrow> real" (\<open>\<parallel>_\<parallel>\<close>)
- assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>"
- and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
- and subadditive [iff?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
+ assumes ge_zero [intro?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>"
+ and abs_homogenous [intro?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
+ and subadditive [intro?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
declare seminorm.intro [intro?]
--- a/src/Provers/clasimp.ML Tue Jul 15 21:18:04 2025 +0100
+++ b/src/Provers/clasimp.ML Tue Jul 15 23:13:12 2025 +0200
@@ -27,7 +27,7 @@
val slow_simp_tac: Proof.context -> int -> tactic
val best_simp_tac: Proof.context -> int -> tactic
val iff_add: attribute
- val iff_add': attribute
+ val iff_add_pure: attribute
val iff_del: attribute
val iff_modifiers: Method.modifier parser list
val clasimp_modifiers: Method.modifier parser list
@@ -43,65 +43,72 @@
(* simp as classical wrapper *)
-(* FIXME !? *)
-fun clasimp f name tac ctxt = f (ctxt, (name, fn _ => CHANGED o tac ctxt));
-
-(*Add a simpset to the claset!*)
(*Caution: only one simpset added can be added by each of addSss and addss*)
-val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" Simplifier.safe_asm_full_simp_tac;
-val addss = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac;
+local
+ fun add_wrapper f name tac ctxt = f (ctxt, (name, fn _ => CHANGED o tac ctxt));
+in
+ val addSss =
+ add_wrapper Classical.addSafter "safe_asm_full_simp_tac" Simplifier.safe_asm_full_simp_tac;
+ val addss =
+ add_wrapper Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac;
+end;
(* iffs: addition of rules to simpsets and clasets simultaneously *)
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};
+
+val del_atts =
+ {intro = Classical.rule_del,
+ elim = Classical.rule_del,
+ dest = Classical.rule_del};
+
(*Takes (possibly conditional) theorems of the form A<->B to
the Safe Intr rule B==>A and
the Safe Destruct rule A==>B.
Also ~A goes to the Safe Elim rule A ==> ?R
Failing other cases, A is added as a Safe Intr rule*)
-fun add_iff safe unsafe =
+fun iff_decl safe unsafe =
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);
-fun del_iff del = Thm.declaration_attribute (fn th => fn context =>
- 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))]
- handle THM _ => [zero_rotate (th RS Data.notE)]
- handle THM _ => [th];
- in fold (Thm.attribute_declaration del) rls context end);
-
in
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 Simplifier.simp_add th);
+ Thm.attribute_declaration (iff_decl 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_pure = iff_decl pure_atts pure_atts;
val iff_del =
Thm.declaration_attribute (fn th =>
- Thm.attribute_declaration (del_iff Classical.rule_del) th #>
- Thm.attribute_declaration (del_iff Context_Rules.rule_del) th #>
+ Thm.attribute_declaration (iff_decl del_atts del_atts) th #>
Thm.attribute_declaration Simplifier.simp_del th);
end;
@@ -183,19 +190,19 @@
(Attrib.setup \<^binding>\<open>iff\<close>
(Scan.lift
(Args.del >> K iff_del ||
- Scan.option Args.add -- Args.query >> K iff_add' ||
+ Scan.option Args.add -- Args.query >> K iff_add_pure ||
Scan.option Args.add >> K iff_add))
"declaration of Simplifier / Classical rules");
(* method modifiers *)
-val iffN = "iff";
+val iff_token = Args.$$$ "iff";
val iff_modifiers =
- [Args.$$$ iffN -- Scan.option Args.add -- Args.colon >> K (Method.modifier iff_add \<^here>),
- Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (Method.modifier iff_add' \<^here>),
- Args.$$$ iffN -- Args.del -- Args.colon >> K (Method.modifier iff_del \<^here>)];
+ [iff_token -- Scan.option Args.add -- Args.colon >> K (Method.modifier iff_add \<^here>),
+ iff_token -- Scan.option Args.add -- Args.query_colon >> K (Method.modifier iff_add_pure \<^here>),
+ iff_token -- Args.del -- Args.colon >> K (Method.modifier iff_del \<^here>)];
val clasimp_modifiers =
Simplifier.simp_modifiers @ Splitter.split_modifiers @
--- a/src/Provers/classical.ML Tue Jul 15 21:18:04 2025 +0100
+++ b/src/Provers/classical.ML Tue Jul 15 23:13:12 2025 +0200
@@ -285,34 +285,33 @@
(* erros and warnings *)
-fun err_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 err_thm ctxt "Ill-formed destruction rule" th
- else Tactic.make_elim th;
+fun err_thm_illformed ctxt kind th =
+ err_thm ctxt (fn () => "Ill-formed " ^ Bires.kind_name kind) 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 () ^ "\n" ^ Thm.string_of_thm ctxt th) else ();
-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_kind ctxt prefix th kind =
+ if Context_Position.is_really_visible ctxt then
+ warn_thm ctxt (fn () => prefix ^ " " ^ Bires.kind_description kind) th
+ else ();
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;
+ if Context_Position.is_really_visible ctxt then
+ (case Bires.get_decls decls th of
+ [] => ()
+ | ds =>
+ Bires.kind_domain
+ |> filter (member (op =) (map #kind ds))
+ |> List.app (warn_kind ctxt "Rule already declared as" th))
+ else ();
(* extend and merge rules *)
@@ -346,15 +345,39 @@
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 =
+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 orelse kind = Bires.dest_bang_kind then
+ let
+ val _ = Thm.no_prems th andalso err_thm_illformed ctxt kind th;
+ val elim = Bires.kind_make_elim kind 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 orelse kind = Bires.dest_kind then
+ let
+ val _ = Thm.no_prems th andalso err_thm_illformed ctxt kind th;
+ val elim = Bires.kind_make_elim kind 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') elim end
+ else raise Fail "Bad rule kind";
+
+in
+
+fun extend_rules ctxt kind opt_weight th cs =
let
val th' = Thm.trim_context th;
- val decl' = init_decl kind opt_weight (trim_context_info info);
+ val decl' = init_decl kind opt_weight (trim_context_info (ext_info ctxt kind th));
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)
+ (NONE, _) => (warn_kind ctxt "Ignoring duplicate" th kind; cs)
| (SOME new_decl, decls') =>
let
val _ = warn_other_kinds ctxt decls th;
@@ -374,8 +397,6 @@
end)
end;
-in
-
fun merge_cs (cs, cs2) =
if pointer_eq (cs, cs2) then cs
else
@@ -400,48 +421,24 @@
extra_netpair = 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 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;
-
-fun addSD w ctxt th = addSE w ctxt (make_elim ctxt th);
-
-fun addI w ctxt th cs =
- let
- val th' = flat_rule ctxt th;
- 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 =
- let
- 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 _ => 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);
-
end;
(* delete rules *)
-fun delrule ctxt th cs =
+fun delrule ctxt warn 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;
+ val _ =
+ if Bires.has_decls decls (Tactic.make_elim th) then
+ warn_thm ctxt
+ (fn () => "Not deleting elim format --- need to to declare proper dest rule") th
+ else ();
in
- if null old_decls then (warn_thm ctxt (fn () => "Undeclared classical rule\n") th; cs)
+ if null old_decls then
+ (if warn then warn_thm ctxt (fn () => "Undeclared classical rule") th else (); cs)
else
let
fun del which ({tag = {index, ...}, info, ...}: decl) = delete_rl index (which info);
@@ -497,17 +494,19 @@
fun put_claset cs = map_claset (K cs);
-(* old-style declarations *)
+(* old-style ML declarations *)
-fun decl f (ctxt, ths) = map_claset (fold_rev (f ctxt) ths) ctxt;
+fun ml_decl kind (ctxt, ths) =
+ map_claset (fold_rev (extend_rules ctxt kind NONE) ths) ctxt;
-val op addSIs = decl (addSI NONE);
-val op addSEs = decl (addSE NONE);
-val op addSDs = decl (addSD NONE);
-val op addIs = decl (addI NONE);
-val op addEs = decl (addE NONE);
-val op addDs = decl (addD NONE);
-val op delrules = decl delrule;
+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 true) ths) ctxt;
@@ -738,21 +737,21 @@
(* declarations *)
-fun attrib f =
+fun attrib kind w =
Thm.declaration_attribute (fn th => fn context =>
- map_cs (f (Context.proof_of context) th) context);
+ map_cs (extend_rules (Context.proof_of context) kind w th) context);
-val safe_elim = attrib o addSE;
-val safe_intro = attrib o addSI;
-val safe_dest = attrib o addSD;
-val unsafe_elim = attrib o addE;
-val unsafe_intro = attrib o addI;
-val unsafe_dest = attrib o addD;
+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 =>
context
- |> map_cs (delrule (Context.proof_of context) th)
+ |> map_cs (delrule (Context.proof_of context) (not (Context_Rules.declared_rule context th)) th)
|> Thm.attribute_declaration Context_Rules.rule_del th);
@@ -861,13 +860,10 @@
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;
+ in Pretty.writeln (Pretty.chunks (Bires.pretty_decls ctxt decls @ prt_wrappers)) end;
val _ =
Outer_Syntax.command \<^command_keyword>\<open>print_claset\<close> "print context of Classical Reasoner"
--- a/src/Pure/General/pretty.ML Tue Jul 15 21:18:04 2025 +0100
+++ b/src/Pure/General/pretty.ML Tue Jul 15 23:13:12 2025 +0200
@@ -243,7 +243,7 @@
let
val bs = out prt;
val bs' =
- if Bytes.size bs <= String.maxSize then bs
+ if Bytes.size bs + 8000 <= String.maxSize then bs
else out (from_ML (ML_Pretty.no_markup (to_ML prt)));
in Bytes.content bs' end;
--- a/src/Pure/Isar/context_rules.ML Tue Jul 15 21:18:04 2025 +0100
+++ b/src/Pure/Isar/context_rules.ML Tue Jul 15 23:13:12 2025 +0200
@@ -12,6 +12,7 @@
val netpair: Proof.context -> Bires.netpair
val find_rules_netpair: Proof.context -> bool -> thm list -> term -> Bires.netpair -> thm list
val find_rules: Proof.context -> bool -> thm list -> term -> thm list list
+ val declared_rule: Context.generic -> thm -> bool
val print_rules: Proof.context -> unit
val addSWrapper: (Proof.context -> (int -> tactic) -> int -> tactic) -> theory -> theory
val addWrapper: (Proof.context -> (int -> tactic) -> int -> tactic) -> theory -> theory
@@ -68,7 +69,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'' = Thm.trim_context (Bires.kind_make_elim kind th);
+ val decl' = init_decl kind opt_weight th'';
in
(case Bires.extend_decls (th', decl') decls of
(NONE, _) => rules
@@ -77,7 +79,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,8 +89,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
(
@@ -111,9 +111,13 @@
in make_rules decls netpairs wrappers end;
);
+fun declared_rule context =
+ let val Rules {decls, ...} = Data.get context
+ in Bires.has_decls decls end;
+
fun print_rules ctxt =
let val Rules {decls, ...} = Data.get (Context.Proof ctxt)
- in Pretty.writeln (Pretty.chunks (Bires.pretty_decls ctxt Bires.kind_domain decls)) end;
+ in Pretty.writeln (Pretty.chunks (Bires.pretty_decls ctxt decls)) end;
(* access data *)
@@ -173,21 +177,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 Tue Jul 15 21:18:04 2025 +0100
+++ b/src/Pure/bires.ML Tue Jul 15 23:13:12 2025 +0200
@@ -23,15 +23,20 @@
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 -> thm -> thm
+ 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
@@ -46,7 +51,7 @@
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 pretty_decls: Proof.context -> '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
@@ -105,30 +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!)")),
- (intro_kind, ("introduction", "(intro)")),
- (elim_kind, ("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 ? Tactic.make_elim;
+
+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;
@@ -136,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;
@@ -185,11 +208,13 @@
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 pretty_decls ctxt decls =
+ kind_domain |> map_filter (fn kind =>
+ (case dest_decls decls (fn (_, {kind = kind', ...}) => kind = kind') of
+ [] => NONE
+ | ds =>
+ SOME (Pretty.big_list (kind_title kind ^ ":")
+ (map (Thm.pretty_thm_item ctxt o #1) ds))));
fun merge_decls (decls1, decls2) =
decls1 |> fold_map add_decls (rev (dest_decls decls2 (not o dup_decls decls1)));