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