isabelle - 伊莎贝尔引理可以用来陈述关于定义的事实吗？

Question

我有伊莎贝尔的定义：

definition two_integer_max_case_def :: "nat ⇒ nat ⇒ nat" where
"two_integer_max_case_def a b = (case a > b of True ⇒ a | False ⇒ b)"

带输出

consts
  two_integer_max_case_def :: "nat ⇒ nat ⇒ nat

我可以从这个定义中获得价值：

value "two_integer_max_case_def 3 4"

输出：

"4"
  :: "nat"

因此，这是可识别且正确的表达/术语。但是我尝试使用这个定义来声明引理：

lemma spec_1:
  assumes "a: nat" "b: nat" "a > b"
  shows "two_integer_max_case_def a b = a"

不幸的是，这个引理不被接受（没有生成目标/子目标），而是给出了错误消息：

Type unification failed: Clash of types "_ ⇒ _" and "_ set"

Type error in application: incompatible operand type

Operator:  (∈) a :: ??'a set ⇒ bool
Operand:   nat :: int ⇒ nat

我的引理有什么问题？我只是使用了不正确的相等操作（也许有一些微妙之处 - nat 实例与 nat 集的混淆）还是更普遍的问题？也许我不允许为（可能是终止）定义陈述定理/引理，并且我只能为已经完成终止证明的函数陈述引理（在函数声明时）？

是否可以更正（如果可以为定义说明引理）我的引理，使其被接受并生成证明目标？

Answer 1