Filtering...

integerp-helper

books/arithmetic-5/lib/basic-ops/integerp-helper

Included Books

top building-blocks default-hint
other
(in-package "ACL2")
local
(local (include-book "../../support/top"))
include-book
(include-book "building-blocks")
include-book
(include-book "default-hint")
other
(set-default-hints '((nonlinearp-default-hint stable-under-simplificationp
     hist
     pspv)))
other
(table acl2-defaults-table :state-ok t)
even-and-odd-alternateencapsulate
(encapsulate nil
  (local (defun induct-nat
      (x)
      (if (and (integerp x) (> x 0))
        (induct-nat (1- x))
        nil)))
  (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)) ("Subgoal *1/1''" :use (:instance (:theorem (implies (integerp a) (integerp (+ 1 a))))
            (a (+ -1/2 (* 1/2 x))))))))
  (local (defthm x-or-x/2-5
      (implies (integerp x) (integerp (- x)))
      :rule-classes nil))
  (local (defthm foo
      (implies (and (integerp x) (integerp y)) (integerp (+ x y)))
      :rule-classes nil))
  (local (defthm bar (equal (+ x (- (* 1/2 x))) (* 1/2 x))))
  (local (defthm x-or-x/2-11
      (implies (and (integerp x) (<= x 0))
        (or (integerp (/ x 2)) (integerp (/ (1+ x) 2))))
      :rule-classes nil
      :hints (("Goal" :in-theory (disable functional-self-inversion-of-minus)
         :use ((:instance x-or-x/2-4 (x (- x))) (:instance foo (x (+ 1/2 (- (* 1/2 x)))) (y x)))))))
  (local (defthm x-or-x/2
      (implies (integerp x)
        (or (integerp (/ x 2)) (integerp (/ (1+ x) 2))))
      :rule-classes nil
      :hints (("Goal" :in-theory (disable functional-self-inversion-of-minus)
         :use ((:instance x-or-x/2-4) (:instance x-or-x/2-11))))))
  (defthm even-and-odd-alternate
    (implies (acl2-numberp x)
      (equal (integerp (+ 1/2 x))
        (and (integerp (* 2 x)) (not (integerp x)))))
    :hints (("Subgoal 3'" :use ((:instance (:theorem (implies (and (integerp x) (integerp y)) (integerp (* x y))))
          (x (+ 1/2 x))
          (y 2)))) ("Subgoal 2'" :use ((:instance x-or-x/2 (x (* 2 x)))))))
  (local (defun ind
      (x)
      (cond ((not (integerp x)) t)
        ((< x -1) (ind (+ 2 x)))
        ((< 1 x) (ind (+ -2 x)))
        ((equal x -1) t)
        ((equal x 0) t)
        ((equal x 1) t)
        (t t))))
  (local (defthm reduce-integerp
      (implies (and (integerp x) (acl2-numberp y))
        (iff (integerp (+ x y)) (integerp y)))))
  (defthm sum-is-even-helper
    (implies (and (integerp x) (integerp y))
      (equal (integerp (+ (* 1/2 x) (* 1/2 y)))
        (if (integerp (* 1/2 x))
          (integerp (* 1/2 y))
          (not (integerp (* 1/2 y))))))
    :hints (("Goal" :induct (ind x)) ("Subgoal *1/3.1" :use (:instance x-or-x/2 (x y))
        :in-theory (disable even-and-odd-alternate)))))