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 Preserving Parity: Here is
another way to decompose natural numbers. To prove (p n), for all
n, prove each of the following:
Base Case 1: (implies (zp n) (p n))
Base Case 2: (implies (equal n 1) (p n))
Induction Step:
(implies (and (not (zp n))
(not (equal n 1))
(p (- n 2)))
(p n))
Base Case 1 establishes that p holds for 0 (and all objects other
than positive naturals).Base Case 2 establishes that p holds for 1.
The Induction Step establishes that if n is a natural number greater than 1,
and if p holds for n-2, then p holds for n.
Note that we have thus proved that (p n) holds, for all n. For example,
(p -7), (p 'abc), and (p 0) are all established by Base Case 1.
(p 1) is established by Base Case 2. (p 2) is established from (p 0)
and the Induction Step. Think about it! (p 3) is established form (p 1)
and the Induction Step, etc.
A function that suggests this induction is:
(defun parity (n)
(if (zp n)
'even
(if (equal n 1)
'odd
(parity (- n 2))))).
