我正在尝试为此功能提供自动终止证明:
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 是如何工作的。
任何人都可以提供参考以了解更多信息和/或帮助我解决这个特定的例子吗?
提前致谢。