为什么Isabelle prover无法识别已定义的类？

Question

class semigroup=
  fixes mult::"'a⇒'a⇒'a" (infixl "⊗" 70)
  assumes assoc: "(x⊗y)⊗z=x⊗(y⊗z)"

theorem main_theorem:
  fixes K::"semigroup"
  shows "∀x,y,z∈K. (x⊗y)⊗z=x⊗(y⊗z)"

代码fixes K::"semigroup"提示“未定义的类型名称: semigroup”错误。

Answer 1

类是排序，即类型的属性，而不是类型。在使用它们时，这有两个主要优点。首先，一个类型可以在多个类中。其次，一个类中可以有两种类型。但是，Isabelle不允许您在同一个类中多次使用一个类型。

这对你意味着什么：

class semigroup=
  fixes mult::"'a⇒'a⇒'a" (infixl "⊗" 70)
  assumes assoc: "(x⊗y)⊗z=x⊗(y⊗z)"

theorem main_theorem:
  fixes x y z ::"'a :: semigroup"
  shows "(x⊗y)⊗z=x⊗(y⊗z)"

下面是一个需要两个类的示例：

  fixes x y z ::"'a :: {semigroup, plus}"
  shows "(x⊗y)⊗z=x⊗(y+z)"

如果您省略了排序加号，您将得到错误消息Variable 'a::semigroup not of sort plus。

在Isabelle中，更常见的情况是不编写∀，而是依赖于由引理自动完成的泛化。纯forall也更易于操作。