|
|
|---|
|
|
|
|---|
Rewrite: -i, i + j, i - j, and i * j are integers, when i and j are integers.
The system has powerful enough type reasoning to `get' these facts automatically most of the time. There are cases, however, where we need to bring the full power of the rewriter to bear on the problem. In general one would like to keep lemmas like this to a minimum so as to avoid swamping the rewriter.
Theorem:
(defthm integerp-+-minus-* (and (implies (integerp i) (integerp (- i))) (implies (and (integerp i) (integerp j)) (and (integerp (+ i j)) (integerp (- i j)) (integerp (* i j))))))