Function Definition in Higher-Order Logic

Abstract

We use a formally proven wellfounded recursion theorem as the basis upon which to build a function definition facility for Higher Order Logic. This approach offers flexibility in the choice of wellfounded relations used, the deferral of termination arguments, and automatic isolation of termination conditions. Building on this platform, we provide the ability to define recursive functions via pattern matching. The system is parameterized and has been instantiated to quite different theorem provers (HOL and Isabelle).

paper