Isabelle/HOL中是否支持动态获取变量名称？

这种直接在HOL逻辑层面实现你想要的expand函数的方式不可行，核心原因如下：

• Isabelle/HOL是形式化逻辑系统，其中的常量（比如sa、sb）本质是纯粹的数学对象，它们的名称只是语法层面的标识——逻辑语义中并不携带名称信息。编译或处理后，逻辑对象本身和它的语法名称没有绑定关系，因此无法在HOL定义里通过逻辑值动态反推出它的原始名称字符串。
• 你设想的nameof函数在HOL中没有合法语义，因为HOL的函数只能基于逻辑对象的数学属性操作，无法访问语法层面的名称元数据。

如果需要实现类似功能，可参考以下两种思路：

1. 手动维护名称映射 #

在HOL中显式定义一个从nat set到string的映射函数，手动关联常量与名称：

consts sa :: "nat set"
       sb :: "nat set"

axiomatization where
  sa_fin: "finite sa"
  and sb_fin: "finite sb"

definition name_of :: "nat set ⇒ string" where
  "name_of s = (if s = sa then ''sa'' else if s = sb then ''sb'' else '''')"

definition expand :: "nat set set ⇒ string set" where
  "expand S = {name_of s | s. s ∈ S}"

definition U :: "nat set set" where "U = {sa, sb}"

这种方式的缺点是需要手动维护映射关系，新增常量时必须同步更新name_of函数，无法自动动态获取名称。

2. 借助Isabelle的ML元语言实现 #

Isabelle的底层是ML语言，可以访问语法树和元数据，因此可通过编写ML代码动态收集常量的名称。示例如下：

(* 示例ML代码，用于获取指定常量的名称字符串 *)
fun get_const_name c =
  let val ctxt = Proof_Context.theory_of @{context}
  in Syntax.string_of_term ctxt (Const (c, @{typ "nat set"})) end

(* 获取sa和sb的名称 *)
val sa_name = get_const_name @{const_name sa}
val sb_name = get_const_name @{const_name sb}

这种方式可以动态获取语法层面的名称，但ML代码属于元语言层面，无法直接嵌入到HOL的定义中，仅适用于工具脚本、证明自动化或生成辅助定义。

内容的提问来源于stack exchange，提问作者Alicia M.