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