Induction on natural numbers
See logic-knowledge-taken-for-granted-inductive-proof for an
explanation of what we mean by the induction suggested by a recursive
function or a term.
Classical Induction on Natural Numbers: Induction is familiar in the
arithmetic setting. To prove (p n), for all n, by classical
induction on the construction of the natural numbers, prove each of the
(implies (zp n) (p n))
(implies (and (not (zp n))
(p (- n 1)))
The Base Case establishes that p holds for 0. In fact, because
of the definition of zp , it
establishes that (p n) holds when n is 0 and it holds when
n is not a natural number.
The Induction Step establishes that if n is a natural number other
than 0, and if p holds for n-1, then p holds for n.
The hypothesis (p (- n 1)) above is called the induction
A function that suggests this induction is
(defun nat-recursion (n)
(if (zp n)
(nat-recursion (- n 1))))
Similarly, the term (fact n) suggests this induction if fact is
(defun fact (k)
(if (zp k)
(* k (fact (- k 1))))).
even though the formal parameter of this definition of fact is k,