Convenient short forms for rewrite rule formulas
In principle, every rewrite rule is made from a formula of this
(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
* 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.