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.