Isabelle 上的函数终止/完整性

问题描述

我有一个语言环境 field 和函数 pow_F 定义如下

function (in field)
  pow_F :: "'a ⇒ nat ⇒ 'a" where
  "pow_F x 0 = ONE_F" |
  "pow_F x (Suc n) = x ⋆ (pow_F x n)"

其中 ONE_F 和 ⋆ 是在字段语言环境中定义的中性元素和乘法函数。

这个函数的行为很奇怪，因为我什至无法证明以下内容

lemma (in field) "pow_F x 0 = ONE_F"

尽管它直接来自 pow_F 的定义。当我运行大锤时，证明者要么放弃，要么计时器用完。

这是怎么回事？

解决方法

当您使用 function 时，您必须先证明终止，然后才能使用 pow_F.simps 规则。您可能想改用 fun（它会自动证明终止）。