isabelle - 在 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/jEditby (rule refl)用粉红色突出显示并说

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

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

标签： isabelleproofjedit

Answer 1