We develop a formalization of the Size-Change Principle in Isabelle/HOL and use it to construct formally certified termination proofs for recursive functions automatically.
The formal Isabelle theories described in this paper are now part of the
Isabelle/HOL Library. They can be found in the directory HOL/SizeChange of the
Isabelle Distribution.