Finding lexicographic orders for termination proofs in Isabelle/HOL


We present a simple method to formally prove termination of recursive functions by searching for lexicographic combinations of size measures. Despite its simplicity, the method turns out to be powerful enough to solve a large majority of termination problems encountered in daily theorem proving practice.

In K. Schneider and J. Brandt, editors, Theorem Proving in Higher Order Logics (TPHOLs 2007), volume 4732 of Lecture Notes in Computer Science, pages 38–53. Springer Verlag