在 Isabelle 中证明类型分类定理

Question

我要使用类型类来证明微不足道：

class order =
  fixes lesseq :: " 'a ⇒ 'a ⇒ bool" (infix "≼" 50)
  assumes refl:    "x ≼ x"
      and trans:   "x ≼ y ⟹ y ≼ z ⟹ x ≼ z"
      and antisym: "x ≼ y ⟹ y ≼ x ⟹ x = y"
begin

  theorem "(myle:: ('b::order) ⇒ 'b ⇒ bool) x x"
  proof -
    show ?thesis by (rule refl)
  qed

end

在这里，Isabelle/jEdit 用粉红色突出显示 by (rule refl) 并说

Failed to apply initial proof method⌂:
goal (1 subgoal):
 1. myle x x

这里有什么问题？否则证明似乎通过了。

Answer 1

myle 和 ≼ 不是同一个函数。

类型注释(myle:: ('b::order) ⇒ 'b ⇒ bool) 只是声明myle 是一个函数，它接受两个'b 类型的元素并返回一个布尔值，而'b 是属于order 类型类的类型。

如果您想证明有关 ≼ 的某些信息，只需使用相同的符号或名称 lesseq。