Automatic Derivation and Application of Induction Schemes for Mutually Recursive Functions

This paper advocates and explores the use of multipredicate induction schemes for proofs about mutually recursive functions. The interactive application of multi-predicate schemes stemming from datatype definitions is already well-established practice; this paper describes an automated proof procedure based on multi-predicate schemes. Multipredicate schemes may be formally derived from (mutually recursive) function definitions; such schemes are often helpful in proving properties of mutually recursive functions where the recursion pattern does not follow that of the underlying datatypes. These ideas have been implemented using the HOL theorem prover and the Clam proof planner.