如何解决为什么 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 也更易于操作。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。