### SPECIAL-CASES-FOR-REWRITE-RULES

convenient short forms for rewrite rule formulas
Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

In principle, every rewrite rule is made from a formula of this shape:

(IMPLIES (AND *hyp1* ... *hypk*)
(*eqv* *lhs* *rhs*))

where *eqv* is either `EQUAL`

or `IFF`

and the result of expanding any
abbreviations in *lhs* is the application of some function symbol other
than `IF`

.* In the special case where there is only one *hyp* term, i.e., *k*=1,
the `(AND `

*hyp1*`)`

can be written *hyp1*.

* In the special case where there are no *hyp* terms, *k*=0, the `(AND)`

term is logically just `T`

and the whole `IMPLIES`

can be dropped; such
a formula may be written as an unconditional `EQUAL`

or `IFF`

term.

* If you build a rewrite rule from a formula that concludes with `(NOT `

*x*`)`

,
it is treated as though it were `(EQUAL `

*x*` NIL)`

, which
is logically equivalent to what you typed.

* If you build a rewrite rule from a formula that concludes with an `AND`

, ACL2
will build a rewrite rule for each conjunct of the `AND`

. This is because

(IMPLIES hyp (AND concl1 concl2))

is propositionally equivalent to
(AND (IMPLIES hyp concl1)
(IMPLIES hyp concl2)).

However, if you use an `OR`

-expression as a hypothesis, ACL2 does *not* do the
dual transformation. Thus, `(IMPLIES (OR hyp1 hyp2) concl)`

generates one rewrite
rule.* Finally, if you build a rewrite rule from a formula that does not conclude
with an `EQUAL`

, an `IFF`

, a `NOT`

, or an `AND,`

but with some other
term, say, *lhs*, then ACL2 acts like you typed `(IFF `

*lhs*` T)`

,
which is logically equivalent to what you typed.

Thus, regardless of what you type, every rule has *k* hypotheses. For
unconditional rules, *k* is 0 and the hypotheses are vacuously true.
Whether or not you write an `EQUAL`

or an `IFF`

in the conclusion, every
rule is either an equality or a propositional equivalence, every rule has a
left-hand side, and every rule has a right-hand side.

Use your browser's **Back Button** now to return to
introduction-to-rewrite-rules-part-1.