Derivation and Use of Induction Schemes in Higher-Order Logic

We discuss how to formally derive induction schemes for recursively defined functions in higher order logic. The functions are able to be defined using ML-style pattern-matching, and the induction schemes are also phrased in terms of these patterns. As part of the TFL system, this facility is portable: it has been incorporated into both the HOL and Isabelle systems.

paper