even-odd2-proofs

other

(in-package "ACL2")

local

(local (include-book "integerp"))

local

(local (include-book "arith"))

local

(local (include-book "arith2"))

local

(local (include-book "fp2"))

in-theory

(in-theory (disable evenp))

even-auxfunction

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

even-aux-reduce-1theorem

(defthm even-aux-reduce-1
  (implies (case-split (not (zp x)))
    (equal (even-aux (+ -1 x)) (not (even-aux x))))
  :hints (("goal" :in-theory (enable even-aux))))

even-aux-reduce-2theorem

(defthmd even-aux-reduce-2
  (implies (and (integerp x) (< 1 x))
    (equal (even-aux (+ -2 x)) (even-aux x)))
  :hints (("goal" :in-theory (enable even-aux))))

even-aux-reduce-3theorem

(defthm even-aux-reduce-3
  (implies (case-split (not (zp x)))
    (equal (even-aux (+ 1 x)) (not (even-aux x))))
  :hints (("goal" :expand (even-aux (+ 1 x))
     :in-theory (enable even-aux-reduce-2))))

even-plus-even-pos-auxtheorem

(defthm even-plus-even-pos-aux
  (implies (and (even-aux x)
      (even-aux y)
      (integerp x)
      (<= 0 x)
      (<= 0 y))
    (even-aux (+ x y)))
  :hints (("Goal" :in-theory (enable even-aux zp))))

even-minus-even-pos-auxtheorem

(defthm even-minus-even-pos-aux
  (implies (and (even-aux x)
      (even-aux y)
      (integerp x)
      (integerp y)
      (<= 0 x)
      (<= 0 y))
    (even-aux (- x y)))
  :hints (("Subgoal *1/6" :cases ((equal y x) (equal y (+ -1 x)))
     :in-theory (set-difference-theories (enable even-aux-reduce-2)
       '(even-aux))) ("Goal" :cases (<= y x) :in-theory (enable even-aux))))

evenfunction

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

even-is-evenp-postheorem

(defthmd even-is-evenp-pos
  (implies (and (integerp x) (<= 0 x))
    (equal (even-aux x) (evenp x)))
  :hints (("Goal" :in-theory (enable even-aux evenp))))

even-is-evenptheorem

(defthmd even-is-evenp
  (implies (integerp x) (equal (even x) (evenp x)))
  :hints (("Goal" :in-theory (enable even evenp even-is-evenp-pos))))

even-aux-negativetheorem

(defthm even-aux-negative
  (implies (<= x 0) (even-aux x))
  :hints (("Goal" :in-theory (enable even-aux))))

even-minustheorem

(defthm even-minus
  (implies (case-split (acl2-numberp x))
    (equal (even (* -1 x)) (even x)))
  :hints (("Goal" :in-theory (enable even))))

even-means-integerptheorem

(defthm even-means-integerp
  (implies (even x) (integerp x))
  :hints (("Goal" :in-theory (enable even)))
  :rule-classes (:forward-chaining))

even-plus-eventheorem

(defthm even-plus-even
  (implies (and (even x) (even y)) (even (+ x y)))
  :otf-flg t
  :hints (("Goal" :in-theory (set-difference-theories (enable even)
       '(even-minus-even-pos-aux even-plus-even-pos-aux))
     :use ((:instance even-plus-even-pos-aux (x x) (y y)) (:instance even-plus-even-pos-aux (x (- x)) (y (- y)))
       (:instance even-minus-even-pos-aux (x x) (y (- y)))
       (:instance even-minus-even-pos-aux (x (- x)) (y y))
       (:instance even-minus-even-pos-aux (x (- y)) (y x))
       (:instance even-minus-even-pos-aux (x y) (y (- x)))))))

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))))
  :hints (("Goal" :use (:instance even-plus-even (x (* -1 x)) (y (+ x y))))))

oddfunction

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

odd-means-integerptheorem

(defthm odd-means-integerp
  (implies (odd x) (integerp x))
  :hints (("Goal" :in-theory (enable odd)))
  :rule-classes (:forward-chaining))

odd-plus-eventheorem

(defthm odd-plus-even
  (implies (and (odd x) (even y))
    (and (odd (+ x y)) (odd (+ y x))))
  :hints (("Goal" :in-theory (enable odd))))

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))))
  :hints (("Goal" :in-theory (enable odd))))

even-reducetheorem

(defthm even-reduce
  (implies (case-split (integerp n))
    (equal (even (+ -1 n)) (not (even n))))
  :hints (("Goal" :in-theory (enable even))))

odd-reducetheorem

(defthm odd-reduce
  (implies (case-split (integerp n))
    (equal (odd (+ -1 n)) (not (odd n))))
  :hints (("Goal" :in-theory (enable odd))))

odd-plus-oddtheorem

(defthm odd-plus-odd
  (implies (and (odd x) (odd y)) (even (+ x y)))
  :hints (("Goal" :use ((:instance odd-reduce (n (+ x y 1))) (:instance odd-reduce (n (+ x 1)))
       (:instance even-plus-even (x (+ 1 x y)) (y (- (+ 1 x)))))
     :in-theory (set-difference-theories (enable odd) '(odd-reduce)))))

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))))
  :hints (("Goal" :in-theory (enable odd))))

induct-schemefunction

(defun induct-scheme
  (n)
  (if (zp n)
    t
    (cons 'a (induct-scheme (+ -1 n)))))

even-double-postheorem

(defthm even-double-pos
  (implies (and (integerp x) (<= 0 x)) (even (* 2 x)))
  :hints (("Goal" :induct (induct-scheme x)
     :in-theory (enable even even-aux))))

even-doubletheorem

(defthm even-double
  (implies (integerp x) (even (* 2 x)))
  :hints (("Goal" :use ((:instance even-double-pos) (:instance even-minus (x (* 2 x)))
       (:instance even-double-pos (x (- x))))
     :in-theory (disable even-minus even-double-pos))))

odd-doubletheorem

(defthm odd-double
  (implies (integerp x) (not (odd (* 2 x))))
  :hints (("Goal" :in-theory (enable odd))))

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))))
  :hints (("Goal" :cases ((acl2-numberp y)) :in-theory (enable odd))))

even-means-half-is-integertheorem

(defthm even-means-half-is-integer
  (implies (even x) (integerp (* 1/2 x)))
  :hints (("goal" :use even-is-evenp :in-theory (enable evenp))))

Included Books