Isabelle的终止证明

Question

我试图为这个函数提供一个自动终止证明：

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_complete是如何工作。

有人能提供一个参考来了解更多关于这方面的信息和/或帮助我举这个特定的例子吗？

提前谢谢。

Answer 1

文档可在https://isabelle.in.tum.de/dist/Isabelle2022/doc/functions.pdf，第4节。(原链接修改自2021年版本(。

这个想法是提供一个有充分根据的关系，这样递归调用的参数就会减少。在您的情况下，第二个参数的长度正在减少，因此：

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