Termination proof in Isabelle

Question

I'm trying to provide an automatic termination proof for this function:

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 

with isEmpty being

fun isEmpty :: "'a list ⇒ bool" where
  "isEmpty [] = True"
| "isEmpty (_#_) = False"

I'm totally new at this, so I don't know how termination proofs work, or how pat_completeness works, for that matter.

Could anyone provide a reference to learn more about this and/or help me with this particular example?

Thanks in advance.

Answer 1

The documentation is available at https://isabelle.in.tum.de/dist/Isabelle2022/doc/functions.pdf, Section 4. (original link modified from 2021 version).

The idea is to provide a relation that is well-founded and such that the arguments of the recursive calls are decreasing. In your case, the length of the second argument is decreasing, so:

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