在Isabelle中定义参数化缩写：将等价类r `` {p}缩写为[p]的正确方法

要把表达式r `` {p}缩写成更简洁的形式（比如⟦p⟧，我更推荐这个，避免和Isabelle默认的列表语法[p]冲突），用自带的abbreviation命令就能轻松实现，具体分两种场景处理：

场景1：等价关系r是全局固定的 #

如果你的等价关系r是整个理论里固定不变的（比如整数模2的等价关系），直接用abbreviation绑定缩写即可：

-- 先定义一个等价关系示例
definition mod2 :: "int ⇒ int ⇒ bool" where
  "mod2 a b ⟷ a mod 2 = b mod 2"

-- 证明它是等价关系（等价类的前提是等价关系，可选但推荐）
lemma mod2_equiv: "equiv mod2"
  unfolding equiv_def refl_def sym_def trans_def mod2_def
  by auto

-- 定义等价类缩写
abbreviation "⟦p⟧ ≡ mod2 `` {p}"

之后在理论里输入⟦3⟧，Isabelle会自动解析成mod2 `` {3}，也就是所有奇数的集合。

要是你执意要用[p]作为缩写，也可以通过语法规则覆盖（不推荐，容易引发歧义）：

syntax
  "_equiv_class" :: "term ⇒ term"  ("[_]")
translations
  "[p]" ⇌ "CONST image mod2 (CONST Collect (λx. x = p))"

场景2：等价关系r是参数化的（支持多等价关系） #

如果需要同时处理多个等价关系（比如模2、模3），用locale封装是最优解，把r作为参数，不同的locale解释对应不同的等价类缩写：

-- 定义等价关系的locale，限定r为等价关系
locale Equiv =
  fixes r :: "'a ⇒ 'a ⇒ bool"
  assumes equiv_r: "equiv r"
begin
  -- 在locale内部定义参数化的等价类缩写
  abbreviation "⟦p⟧ ≡ r `` {p}"
end

-- 将模2关系解释到locale
interpretation mod2_equiv: Equiv mod2 using mod2_equiv by unfold_locales

-- 再定义模3关系并解释到locale
definition mod3 :: "int ⇒ int ⇒ bool" where
  "mod3 a b ⟷ a mod 3 = b mod 3"

lemma mod3_equiv: "equiv mod3"
  unfolding equiv_def refl_def sym_def trans_def mod3_def
  by auto

interpretation mod3_equiv: Equiv mod3 using mod3_equiv by unfold_locales

这样在mod2_equiv上下文里，⟦3⟧指奇数集合；在mod3_equiv上下文里，⟦3⟧指所有3的倍数集合，完美实现参数化的等价类缩写。

最后提一句：abbreviation只是语法层面的替换，不会引入新常量，完全不影响后续证明，这也是它比definition更适合做这类缩写的原因。

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