Nominal Isabelle多分类原子的α等价证明问题求助

问题背景 #

我正在试验Nominal2对多分类原子的支持，参考了Nominal2包中的多分类原子示例及相关论文内容，旨在定义Church风格带类型λ演算（变量自身携带类型信息，如λxₒ. xₒ）。编写的代码如下：

theory Scratch
  imports "Nominal2.Nominal2" "Nominal2.Atoms"
begin

(* 使用Nominal2.Atoms中的var、ty、Var类型构造器 *)

nominal_datatype exp =
    EVar var
  | EApp exp exp
  | EAbs x::var M::exp binds x in M

(* 尝试证明α等价的抽象项相等，但无法自动完成 *)
lemma "EAbs (Var x (TVar ''o'')) (EVar (Var x (TVar ''o''))) = EAbs (Var y (TVar ''o'')) (EVar (Var y (TVar ''o'')))"
  sorry (* 无法自动证明该等式 *)

end

问题在于：单分类原子场景下，此类α等价的证明可由Nominal2自动完成，但使用多分类原子（var类型包含类型标签）时，无法自动推导两个α等价项的相等性。推测根源是缺少针对at_base类型（多分类原子的基础类型）的类似alpha_lst的simproc，但不确定是否存在其他疏漏。

原因分析 #

Nominal2默认的α-等价化简机制（如alpha_lst simproc）是为单分类原子设计的。对于多分类原子类型（如var，由at_base实例化而来），默认的化简规则不会自动处理带类型标签的变量重命名，因此无法自动识别两个仅变量名不同、类型一致的抽象项是α等价的。

解决方案 #

方法1：手动利用生成的EAbs_eq_iff定理证明 #

Nominal2的nominal_datatype会为每个带绑定的构造器生成对应的等价性判定定理，对于EAbs，对应的定理是EAbs_eq_iff，可以用它来手动完成证明：

lemma "EAbs (Var x (TVar ''o'')) (EVar (Var x (TVar ''o''))) = EAbs (Var y (TVar ''o'')) (EVar (Var y (TVar ''o'')))"
  apply (rule EAbs_eq_iff)
  apply simp  (* 自动验证两个绑定变量的类型一致 *)
  apply (rule allI)
  apply (case_tac z)
  apply (simp split: if_splits)
  done

方法2：添加自定义化简规则到simpset #

为了让simp能够自动处理此类多分类原子的α等价，可以手动添加针对var类型的变量重命名化简规则。首先证明一个通用的α等价引理，然后将其添加到simpset中：

(* 证明通用的带类型抽象项α等价规则 *)
lemma alpha_abs_var:
  assumes "a = Var x τ" and "b = Var y τ"
  shows "EAbs a (EVar a) = EAbs b (EVar b)"
  using assms
  apply (rule EAbs_eq_iff)
  apply simp
  apply (rule allI)
  apply (case_tac z)
  apply (simp split: if_splits)
  done

(* 将规则添加到simpset *)
declare alpha_abs_var[simp]

(* 现在可以自动证明原引理 *)
lemma "EAbs (Var x (TVar ''o'')) (EVar (Var x (TVar ''o''))) = EAbs (Var y (TVar ''o'')) (EVar (Var y (TVar ''o'')))"
  by simp

方法3：注册针对at_base的α化简simproc（进阶） #

如果需要处理更复杂的多分类原子α等价场景，可以参考Nominal2中alpha_lst simproc的实现，为at_base类型注册对应的化简过程。这需要对Nominal2的内部机制有一定了解，具体步骤如下：

• 参考Nominal2源码中alpha_lst的实现逻辑
• 为var类型实现对应的freshness和重命名的化简规则
• 将自定义simproc注册到Isabelle的化简器中

这种方法适合需要大量处理多分类原子α等价的场景，一次性配置后即可自动处理所有类似情况。

内容的提问来源于stack exchange，提问作者Javier Díaz