Filtering...

even-odd

books/rtl/rel9/arithmetic/even-odd

Included Books

integerp predicate fp2
other
(in-package "ACL2")
local
(local (include-book "integerp"))
local
(local (include-book "predicate"))
local
(local (include-book "fp2"))
even-int-implies-inttheorem
(defthmd even-int-implies-int
  (implies (and (integerp (* 1/2 x)) (rationalp x))
    (integerp x))
  :rule-classes ((:rewrite :backchain-limit-lst (1 nil)))
  :hints (("Goal" :in-theory (disable integerp-prod)
     :use (:instance integerp-prod (x (* 1/2 x)) (y 2)))))
induct-natfunction
(defun induct-nat
  (x)
  (if (and (integerp x) (> x 0))
    (induct-nat (1- x))
    nil))
local
(local (defthm x-or-x/2-4
    (implies (and (integerp x) (>= x 0))
      (or (integerp (/ x 2)) (integerp (/ (1+ x) 2))))
    :rule-classes nil
    :hints (("Goal" :induct (induct-nat x)))))
integerp-+theorem
(defthm integerp-+
  (implies (and (integerp x) (integerp y)) (integerp (+ x y))))
x-or-x/2theorem
(defthm x-or-x/2
  (implies (integerp x)
    (or (integerp (/ x 2)) (integerp (/ (1+ x) 2))))
  :rule-classes nil
  :hints (("Goal" :in-theory (disable integerp-+)
     :use ((:instance integerp-+ (x (+ 1/2 (* -1/2 x))) (y x)) (:instance x-or-x/2-4)
       (:instance x-or-x/2-4 (x (- x)))))))
integerp-sum-of-odds-over-2encapsulate
(encapsulate nil
  (local (defthm hack-int
      (implies (and (integerp x) (integerp y)) (integerp (+ x y)))))
  (defthm integerp-sum-of-odds-over-2
    (implies (and (rationalp x)
        (rationalp y)
        (integerp (* 2 x))
        (not (integerp x)))
      (equal (integerp (+ x y))
        (and (integerp (* 2 y)) (not (integerp y)))))
    :hints (("Goal" :in-theory (disable even-int-implies-int)
       :use ((:instance even-int-implies-int (x (+ (* 2 x) (* 2 y)))) (:instance hack-int (x (+ 1/2 x)) (y (+ 1/2 y)))
         (:instance x-or-x/2 (x (* 2 x)))
         (:instance x-or-x/2 (x (* 2 y))))))))
in-theory
(in-theory (disable integerp-sum-of-odds-over-2))
integerp-sum-of-odds-over-2-leading-constanttheorem
(defthm integerp-sum-of-odds-over-2-leading-constant
  (implies (and (syntaxp (and (quotep x) (integerp (* 2 x)) (not (integerp x))))
      (rationalp x)
      (rationalp y)
      (integerp (* 2 x))
      (not (integerp x))
      (integerp (* 2 y))
      (not (integerp y)))
    (integerp (+ x y)))
  :hints (("Goal" :use integerp-sum-of-odds-over-2)))
even-and-odd-alternate-erictheorem
(defthm even-and-odd-alternate-eric
  (implies (and (rationalp x) (integerp (* 2 x)))
    (equal (integerp (+ 1/2 x)) (not (integerp x)))))
even-and-odd-alternate-3theorem
(defthm even-and-odd-alternate-3
  (implies (and (integerp x))
    (equal (integerp (+ -1/2 (* -1/2 x)))
      (not (integerp (* 1/2 x)))))
  :hints (("Goal" :in-theory (disable integerp-minus)
     :use (:instance integerp-minus (x (+ -1/2 (* -1/2 x)))))))
even-and-odd-alternate-eric-2-bktheorem
(defthm even-and-odd-alternate-eric-2-bk
  (implies (rationalp x)
    (implies (and (integerp (* 2 x)) (not (integerp x)))
      (integerp (+ 1/2 x)))))
even-odd-5theorem
(defthm even-odd-5
  (implies (and (rationalp x) (integerp (* 1/2 x)))
    (and (integerp (- x 1)) (not (integerp (* 1/2 (- x 1))))))
  :hints (("Goal" :in-theory (enable even-int-implies-int))))
even-and-odd-alternate-eric-2-fwtheorem
(defthm even-and-odd-alternate-eric-2-fw
  (implies (rationalp x)
    (implies (integerp (+ 1/2 x))
      (and (integerp (* 2 x)) (not (integerp x)))))
  :hints (("Goal" :in-theory (disable even-odd-5)
     :use (:instance even-odd-5 (x (+ 1 (* 2 x)))))))
even-and-odd-alternate-eric-2theorem
(defthm even-and-odd-alternate-eric-2
  (implies (rationalp x)
    (equal (integerp (+ 1/2 x))
      (and (integerp (* 2 x)) (not (integerp x))))))
in-theory
(in-theory (disable even-and-odd-alternate-eric-2-fw
    even-and-odd-alternate-eric-2-bk))