Further information on expanding definitions via rewriting

We assume you've read about ``*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 ``*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?

formula1: (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))

Evidently we replaced

The definition of

(defun true-listp (x) (if (consp x) (true-listp (cdr x)) (equal x nil))).

By rewriting once with the definition of *formula1* to:

formula1': (implies (and (not (consp z)) (if (consp z) (true-listp (cdr z)) (equal z nil))) (equal (rev (rev z)) z)).

Note how the call of

Next, note that the first hypothesis above is that *formula1'*
to

formula1'': (implies (and (not (consp z)) (if nil (true-listp (cdr z)) (equal z nil))) (equal (rev (rev z)) z)).

(We will explore replacement of equals by equals later.)

Furthermore, we know the basic axiom about

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

Rewriting with this particular axiom, using *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

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