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
IFFand the result of expanding any abbreviations in lhs is the application of some function symbol other than
* In the special case where there is only one hyp term, i.e., k=1,
) can be written hyp1.
* In the special case where there are no hyp terms, k=0, the
term is logically just
T and the whole
IMPLIES can be dropped; such
a formula may be written as an unconditional
* If you build a rewrite rule from a formula that concludes with
it is treated as though it were
is logically equivalent to what you typed.
* If you build a rewrite rule from a formula that concludes with an
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
NOT, or an
AND, but with some other
term, say, lhs, then ACL2 acts like you typed
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.