even-odd2

other

(in-package "ACL2")

include-book

(include-book "ground-zero")

local

(local (include-book "even-odd2-proofs"))

even-auxfunction

(defund even-aux
  (x)
  (if (zp x)
    t
    (if (eql 1 x)
      nil
      (even-aux (+ -2 x)))))

evenfunction

(defund even
  (x)
  (if (not (integerp x))
    nil
    (if (< x 0)
      (even-aux (- x))
      (even-aux x))))

oddfunction

(defund odd (x) (and (integerp x) (not (even x))))

even-is-evenptheorem

(defthmd even-is-evenp
  (implies (integerp x) (equal (even x) (evenp x))))

even-minustheorem

(defthm even-minus
  (implies (case-split (acl2-numberp x))
    (equal (even (* -1 x)) (even x))))

even-means-integerptheorem

(defthm even-means-integerp
  (implies (even x) (integerp x))
  :rule-classes (:forward-chaining))

odd-means-integerptheorem

(defthm odd-means-integerp
  (implies (odd x) (integerp x))
  :rule-classes (:forward-chaining))

even-sum-rewrite-1theorem

(defthm even-sum-rewrite-1
  (implies (and (even x) (case-split (acl2-numberp y)))
    (and (equal (even (+ x y)) (even y))
      (equal (even (+ y x)) (even y)))))

even-sum-rewrite-2theorem

(defthm even-sum-rewrite-2
  (implies (odd x)
    (and (equal (even (+ x y)) (odd y))
      (equal (even (+ y x)) (odd y)))))

odd-sum-rewrite-1theorem

(defthm odd-sum-rewrite-1
  (implies (even x)
    (and (equal (odd (+ x y)) (odd y))
      (equal (odd (+ y x)) (odd y)))))

odd-sum-rewrite-2theorem

(defthm odd-sum-rewrite-2
  (implies (and (odd x) (case-split (acl2-numberp y)))
    (and (equal (odd (+ x y)) (even y))
      (equal (odd (+ y x)) (even y)))))

other

(theory-invariant (incompatible (:rewrite even-reduce) (:definition even-aux)))

even-reducetheorem

(defthm even-reduce
  (implies (case-split (integerp n))
    (equal (even (+ -1 n)) (not (even n)))))

odd-reducetheorem

(defthm odd-reduce
  (implies (case-split (integerp n))
    (equal (odd (+ -1 n)) (not (odd n)))))

even-doubletheorem

(defthm even-double (implies (integerp x) (even (* 2 x))))

odd-doubletheorem

(defthm odd-double
  (implies (integerp x) (not (odd (* 2 x)))))

even-means-half-is-integertheorem

(defthm even-means-half-is-integer
  (implies (even x) (integerp (* 1/2 x))))

Included Books