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 following:

Base Case:
(implies (zp n) (p n))
Induction Step:
(implies (and (not (zp n))
              (p (- n 1)))
         (p n))
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 hypothesis.

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 defined:
 (defun fact (k)
  (if (zp k)
      (* k (fact (- k 1))))).
even though the formal parameter of this definition of fact is k, not n.