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.
