Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER
Any time you are proving a formula and see a subterm in the formula that contains no variables, you can just evaluate the subterm.
This is familiar from algebra: It is not uncommon to rearrange a polynominal to collect all the constants and then add them up:
(3x + 2 + 7y + 2) = (3x + 7y + (2 + 2)) = (3x + 7y + 4).That last step is just evaluation.
It happens often in ACL2 proofs because theorems involve constants and defined functions and when those constants ``drift into the maw'' of a function, the function call can be eliminated and replaced by a new constant. ACL2 does this automatically; you don't have to tell it. In fact, there are a few occasions where you might prefer it not evaluate and those are the ones you have to look out for! They'll be obvious when they happen because you'll see a mysterious constant crop up in the proof.
Evaluation is legal because it is just the repeated use of unconditional rewriting to replace definitions by their instantiated bodies until no function calls remain.
Now use your browser's Back Button to return to the example proof in logic-knowledge-taken-for-granted.
