		Search-engine friendly clone of the ACL2 documentation.

Introduction-to-the-theorem-prover

Special-cases-for-rewrite-rules

Convenient short forms for rewrite rule formulas

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.