Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER
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)
n
(nat-recursion (- n 1))))
Similarly, the term (fact n) suggests this induction if fact
is defined:
(defun fact (k)
(if (zp k)
1
(* k (fact (- k 1))))).
even though the formal parameter of this definition of fact is k, not n.
