我在 isabelle 中遇到一个错误，我在 isabelle 中尝试在global_interpretation后构建类层次结构时不理解。
这里有一个玩具非工作的例子来说明。
theory mnwe
imports Main
begin
class natop =
fixes natop :: "nat <Rightarrow> 'a <Rightarrow> 'a"
definition (in natop) list_double :: "'a list <Rightarrow> 'a list"
where "list_double xs = map (natop 2) xs"
global_interpretation semiring_1_natop: natop "<lambda>n x. of_nat n * x"
defines list_double = semiring_1_natop.list_double
.
class special_list =
fixes speclist :: "'a list"
class double_special_list = semiring_1 + special_list +
assumes "list_double speclist = speclist"
end
最后一个类double_special_list引发以下错误：
Type inference imposes additional sort constraint semiring_1 of type parameter 'a of sort type
哼？类double_special_list显式继承自类semiring_1...
有人可以启发我我做错了什么吗？
更新：
如果我放弃class special_list而是这样做
class double_special_list = semiring_1 +
fixes speclist :: "'a list"
assumes "list_double speclist = speclist"
我收到错误
Type unification failed: Variable 'a::type not of sort semiring_1
这又是一个"嗯？"给定semiring_1超类规范。
好的，以下工作(至少不会引发任何错误(，但对我来说，在类double_special_listfixes中隐藏semiring_1超类声明似乎很奇怪。老实说，我不太确定我问题中的代码和这个答案中的代码有什么区别，以及为什么前者是一个错误，但你去吧。
theory answer
imports Main
begin
class natop =
fixes natop :: "nat <Rightarrow> 'a <Rightarrow> 'a"
definition (in natop) list_double :: "'a list <Rightarrow> 'a list"
where "list_double xs = map (natop 2) xs"
global_interpretation semiring_1_natop: natop "<lambda>n x. of_nat n * x"
defines list_double = semiring_1_natop.list_double
.
class double_special_list =
fixes speclist :: "'a::semiring_1 list"
assumes "list_double speclist = speclist"
lemma test:
fixes a b c :: "'a::double_special_list"
shows "a * (b + c) = a * b + a * c"
by (simp add: algebra_simps)
end