Isabelle中是否存在可获取datatype条目名称的内置函数？

你预期的直接返回A/B/C构造器本身的函数在Isabelle类型系统中无法实现：三个构造器的类型各不相同（A为int ⇒ Test、B为string ⇒ Test、C为nat ⇒ Test），无法作为同一个函数的合法返回值。你可以通过以下两种方案实现等效需求：

方案1：手动定义映射函数（推荐日常使用） #

为你的自定义datatype配套定义构造器枚举类型和映射函数，适配性最高、验证成本最低：

(* 首先定义Test类型对应的构造器枚举 *)
datatype Test_Ctor = A_ctor | B_ctor | C_ctor

(* 实现你需要的映射函数f *)
fun f :: "Test ⇒ Test_Ctor" where
  "f (A _) = A_ctor"
| "f (B _) = B_ctor"
| "f (C _) = C_ctor"

执行效果完全匹配你的需求：

• f (A 5) = A_ctor
• f (B ''hi'') = B_ctor
• f (C 234789623) = C_ctor

方案2：ML层反射接口（适合通用工具开发） #

如果你需要针对任意datatype做通用的构造器识别，可以调用Isabelle Datatype包提供的ML层接口，直接获取构造器的字符串名称：

(* 示例：获取Test类型值的构造器名称 *)
val sample_term = @{term "A 5"};
val ctor_name = Datatype.ctor_name_of (Thm.term_of sample_term);
(* 输出结果为字符串 "A" *)

该方案仅可在ML环境中使用，不适合普通Isabelle证明/定义场景。

内容的提问来源于stack exchange，提问作者Kookie