如何解决伊莎贝尔的终止证明
function aux :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list" where
"aux p xs = (if ¬isEmpty xs ∧ p (hd xs) then hd xs#aux p (drop 1 xs) else [])"
by pat_completeness auto
isEmpty 是
fun isEmpty :: "'a list ⇒ bool" where
"isEmpty [] = True"
| "isEmpty (_#_) = False"
我对此完全陌生,所以我不知道终止证明是如何工作的,或者 pat_completeness 是如何工作的。
任何人都可以提供参考以了解更多信息和/或帮助我解决这个特定示例吗?
提前致谢。
解决方法
文档位于 https://isabelle.in.tum.de/dist/Isabelle2021/doc/functions.pdf 的第 4 节。
这个想法是提供一个有充分根据的关系,并且递归调用的参数正在减少。在您的情况下,第二个参数的长度正在减少,因此:
function aux :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list" where
"aux p xs = (if xs≠ [] ∧ p (hd xs) then hd xs#aux p (drop 1 xs) else [])"
by pat_completeness auto
termination
by (relation ‹measure (λ(_,xs). length xs)›)
auto
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。