Isabelle中定义域的乘法群时typedef报类型统一失败错误如何解决

错误产生原因 #

你写的集合定义{x :: 'a set. x ≠ 0}里给变量x多加了set类型标注：你本意是要取域类型'a的非零元素，但这里的标注把x的类型指定成了'a set（也就是元素为'a类型的集合类型），Isabelle的类型系统找不到集合类型对应的0实例，因此报类型匹配失败的错误。

正确的乘法群定义方式 #

首先修正typedef的语法错误，同时补全非空证明、群操作实例化的部分即可：

theory Scratch
  imports
    "HOL.Fields"
    "HOL.Groups"
begin

typedef (overloaded) 'a mul_group = "{x :: 'a :: field. x ≠ 0}"
  by (auto intro: exI[of _ 1]) (* 证明集合非空：域的乘法单位元1满足1≠0 *)

(* 给mul_group实例化群结构 *)
instantiation mul_group :: (field) group
begin
  definition mul_mul_group_def: "a * b = Abs_mul_group (Rep_mul_group a * Rep_mul_group b)"
  definition one_mul_group_def: "1 = Abs_mul_group 1"
  definition inverse_mul_group_def: "inverse a = Abs_mul_group (inverse (Rep_mul_group a))"
  definition divide_mul_group_def: "a / b = a * inverse b"

  instance
    apply (intro_classes)
    (* 展开定义，利用域的乘法性质证明所有群公理 *)
    unfolding mul_mul_group_def one_mul_group_def inverse_mul_group_def divide_mul_group_def
    apply (simp_all add: Rep_mul_group_inject Abs_mul_group_inverse field_class.field_mult_commute field_class.field_mult_assoc field_class.field_mult_left_inverse)
    done
end

end

相关说明：

• 修正后的typedef直接指定元素为'a :: field类型，去掉了多余的set标注，符合取域非零元素的需求
• 证明步骤by (auto intro: exI[of _ 1])是typedef的必填项：所有域的公理都要求乘法单位元1不等于加法单位元0，可以直接用来证明目标集合非空
• 后续的实例化代码把域的乘法、逆元、单位元都映射到你定义的mul_group类型上，直接复用域已有的乘法性质就能完成群公理的证明，不需要手动写复杂的证明步骤

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