Automatic Derivation and Application of Induction Schemes for Mutually
Recursive Functions
This paper advocates and explores the use of multi-predicate
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. Multi-predicate 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.
paper