为什么 Isabelle 证明者无法识别定义的类？

问题描述

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" 提示“未定义类型名称：半群”错误。

解决方法

类是排序，即类型的属性，而不是类型。这在使用它们时有两个主要优点。首先一个类型可以在多个类中。其次，两个类型可以在一个类中。但是，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 也更易于操作。