Wellfounded Schematic Definitions

A program scheme looks like a recursive function definition, except that it has free variables `on the right hand side'. As is well-known, equalities between schemes can capture powerful program transformations, e.g., translation to tail-recursive form. In this paper, we present a simple and general way to define program schemes, based on a particular form of the wellfounded recursion theorem. Each program scheme specifies a schematic induction theorem, which is automatically derived by formal proof from the wellfounded induction theorem. We present a few examples of how formal program transformations are expressed and proved in our approach. The mechanization reported here has been incorporated into both the HOL and Isabelle/HOL systems.

paper