Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

We assume you've read about
``instances'' and picked up
our basic terminology including the ideas of *matching* a *pattern* term to a
*target* term, obtaining a *substitution* and how to *instantiate* a term
with a substitution. We use these notions below without further citation.

In addition, we assume you've read about
``rewriting'' where we
introduced the idea of treating a theorem (axiom, definition, or lemma)
as a *conditional rewrite* rule and replaced one term by an equivalent one
provided we can *relieve the hypotheses*.

Suppose you're trying to prove *formula1* and you transform it
to *formula2* by rewriting.
What happened?

Evidently we replacedformula1: (implies (and (not (consp z)) (true-listp z)) (equal (rev (rev z)) z))

formula2: (implies (and (not (consp z)) (equal z nil)) (equal (rev (rev z)) z))

`(true-listp z)`

by `(equal z nil)`

.
But how did that happen? What really happened was the sequential
application of several unconditional rewrites and the use of replacement of
equals by equals.
The definition of `true-listp`

is:

(defun true-listp (x) (if (consp x) (true-listp (cdr x)) (equal x nil))).By rewriting once with the definition of

`true-listp`

,
we transform Note how the call offormula1': (implies (and (not (consp z)) (if (consp z) (true-listp (cdr z)) (equal z nil))) (equal (rev (rev z)) z)).

`true-listp`

has been replaced by the entire body
of `true-listp`

.
Next, note that the first hypothesis above is that `(consp z)`

is false.
That is, `(not (consp z))`

is the same as `(equal (consp z) nil)`

.
Thus, replacement of equals by equals means we can transform *formula1'* to

(We will explore replacement of equals by equals later.)formula1'': (implies (and (not (consp z)) (if nil (true-listp (cdr z)) (equal z nil))) (equal (rev (rev z)) z)).

Furthermore, we know the basic axiom about `if`

:

Axiomif-nil: (if nil x y) = y.

Rewriting with this particular axiom, using `(if nil x y)`

as the pattern
and `y`

as the replacement, will transform *formula1''* to

formula2: (implies (and (not (consp z)) (equal z nil)) (equal (rev (rev z)) z)).

Often when we say we derived one formula from another by ``expansion'' and or
by ``rewriting'' we take many rewrite steps, as here. We typically use hypotheses of the
formula without noting ``replacement of equals by equals'' as when we replaced
`(consp z)`

by `nil`

, and we typically omit to mention the use of basic
axioms like `if-nil`

above.

Now use your browser's **Back Button** to return to the example proof in
logic-knowledge-taken-for-granted.