Isabelle中用类型类实现列表自由幺半群遇报错，求解决方案

核心错误原因 #

你遇到的Undefined type name报错，是因为**instantiation命令需要针对类型构造器（如list）而非具体类型（如'a list）**。Isabelle的实例化语法要求明确标注类型构造器的参数约束，而非直接写带参数的具体类型。

正确实现步骤 #

要表达列表在拼接操作下的自由幺半群，需定义包含结合律、单位元的幺半群类型类，再将列表类型实例化到该类中。以下是可直接运行的代码：

(* 先取消默认符号绑定，避免冲突 *)
no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65) and plus (infixl "+" 65)

(* 定义半群类：仅要求结合律 *)
class semigroup =
  fixes plus :: "'a ⇒ 'a ⇒ 'a" (infixl "+" 65)
  assumes assoc: "(x + y) + z = x + (y + z)"

(* 定义幺半群类：继承半群，增加单位元 *)
class monoid = semigroup +
  fixes zero :: "'a" ("0")
  assumes left_zero: "0 + x = x"
  assumes right_zero: "x + 0 = x"

(* 重新定义列表类型（也可直接用系统自带list，此处为符号统一重定义） *)
datatype 'a list =
    Nil  ("[]")
    | Cons 'a "'a list"  (infixr "#" 65)

(* 实例化列表到monoid类：list是类型构造器，参数约束为type（任意类型） *)
instantiation list :: (type) monoid
begin

(* 定义拼接操作作为plus *)
primrec plus_list :: "'a list ⇒ 'a list ⇒ 'a list" where
  "plus_list [] ys = ys" |
  "plus_list (x # xs) ys = x # (plus_list xs ys)"

(* 定义空列表作为单位元zero *)
definition zero_list :: "'a list" where
  "zero_list = []"

(* 证明幺半群的公理 *)
lemma plus_assoc: "(xs + ys) + zs = xs + (ys + zs)"
  by (induct xs) auto

lemma left_zero: "0 + xs = xs"
  unfolding zero_list_def plus_list.simps by simp

lemma right_zero: "xs + 0 = xs"
  unfolding zero_list_def by (induct xs) auto

(* 注册实例，关联定义与公理 *)
instance
  apply (intro_classes)
  apply (rule plus_assoc)
  apply (rule left_zero)
  apply (rule right_zero)
  done

end

(* 测试示例 *)
value "[1,2] + [3,4]"  (* 输出: [1,2,3,4] *)
value "0 :: nat list"   (* 输出: [] *)

语法细节说明 #

1. 类型类定义：
   现代Isabelle使用class 类名 = 父类 + ...的格式，而非旧文档中的class 类名 where ...。fixes用于声明类的操作，assumes用于声明公理。

2. 多态类型实例化：
   正确语法为instantiation 类型构造器 :: (参数约束) 目标类，比如list :: (type) monoid表示：将接受任意type类参数的list构造器，实例化为monoid类的成员。

3. 公理证明：
   幺半群必须满足结合律、左单位元、右单位元三条公理，实例化时需逐一证明这些性质，通过intro_classes启动类实例化的证明流程。

关于文档语法差异 #

你看到的旧文档（如classes.pdf早期版本）使用的是Isabelle旧版语法，现代Isabelle（2020+）已统一为class C = ...的定义方式，实例化多态类型的语法也更严谨，必须明确区分类型构造器和具体类型。

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