Filtering...

types-helper

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

Included Books

top
other
(in-package "ACL2")
local
(local (include-book "../../support/top"))
local
(local (defthm one-a
    (implies (and (< 0 x) (< x 1)) (not (integerp x)))))
local
(local (defthm one-b
    (implies (and (< x 0) (< -1 x)) (not (integerp x)))))
local
(local (defthm two-a
    (implies (and (real/rationalp x) (< 1 x))
      (and (< 0 (/ x)) (< (/ x) 1)))
    :hints (("Goal" :in-theory (enable normalize-<-/-to-*-2)))))
local
(local (defthm two-b
    (implies (and (real/rationalp x) (< x -1))
      (and (< (/ x) 0) (< -1 (/ x))))
    :hints (("Goal" :in-theory (enable normalize-<-/-to-*-1)))))
local
(local (defthm three
    (implies (complex/complex-rationalp x)
      (not (integerp (/ x))))))
not-integerp-/-1theorem
(defthm not-integerp-/-1
  (implies (< 1 x) (not (integerp (/ x))))
  :hints (("Goal" :cases ((real/rationalp x) (complex/complex-rationalp x)))))
not-integerp-/-2theorem
(defthm not-integerp-/-2
  (implies (< x -1) (not (integerp (/ x))))
  :hints (("Goal" :cases ((real/rationalp x) (complex/complex-rationalp x)))))
integerp-/-helpertheorem
(defthm integerp-/-helper
  (implies (integerp x)
    (equal (integerp (/ x))
      (or (equal x -1) (equal x 0) (equal x 1))))
  :hints (("Goal" :use ((:instance not-integerp-/-1) (:instance not-integerp-/-2))
     :in-theory (disable not-integerp-/-1 not-integerp-/-2))))