Filtering...

integerp

books/rtl/rel9/arithmetic/integerp

Included Books

negative-syntaxp predicate fp2
other
(in-package "ACL2")
include-book
(include-book "negative-syntaxp")
local
(local (include-book "predicate"))
local
(local (include-book "fp2"))
local
(local (in-theory (disable a2)))
quotient-not-integerpencapsulate
(encapsulate nil
  (local (defthm no-room-for-an-integerp-between-0-and-1
      (implies (and (< x 1) (< 0 x)) (not (integerp x)))))
  (defthm quotient-not-integerp
    (implies (and (< i j)
        (<= 0 i)
        (<= 0 j)
        (case-split (< 0 i))
        (case-split (< 0 j))
        (case-split (rationalp j)))
      (not (integerp (/ i j))))))
integerp-minus-auxencapsulate
(encapsulate nil
  (local (defthm minus-1-rewrite (equal (* -1 x) (- x))))
  (defthm integerp-minus-aux
    (implies (acl2-numberp x)
      (equal (integerp (* -1 x)) (integerp x)))))
integerp-minustheorem
(defthm integerp-minus
  (implies (and (syntaxp (negative-syntaxp x))
      (case-split (acl2-numberp x)))
    (equal (integerp x) (integerp (* -1 x)))))
in-theory
(in-theory (disable integerp-minus-aux))
integerp-sum-take-out-known-integertheorem
(defthm integerp-sum-take-out-known-integer
  (implies (integerp n)
    (and (equal (integerp (+ n x)) (integerp (fix x)))
      (equal (integerp (+ x n)) (integerp (fix x))))))
integerp-sum-take-out-known-integer-3theorem
(defthm integerp-sum-take-out-known-integer-3
  (implies (integerp n)
    (and (equal (integerp (+ x n y)) (integerp (fix (+ x y))))
      (equal (integerp (+ x y n)) (integerp (fix (+ x y))))))
  :hints (("Goal" :in-theory (disable integerp-sum-take-out-known-integer)
     :use (:instance integerp-sum-take-out-known-integer (x (+ x y))))))
integerp-prodtheorem
(defthm integerp-prod
  (implies (and (integerp x) (integerp y)) (integerp (* x y)))
  :rule-classes (:rewrite :type-prescription))
integerp-prod-of-3-last-twotheorem
(defthm integerp-prod-of-3-last-two
  (implies (and (integerp (* b c)) (integerp a))
    (integerp (* a b c))))
integerp-prod-of-3-first-and-lasttheorem
(defthm integerp-prod-of-3-first-and-last
  (implies (and (integerp (* a c)) (integerp b))
    (integerp (* a b c)))
  :hints (("Goal" :in-theory (disable integerp-prod-of-3-last-two)
     :use (:instance integerp-prod-of-3-last-two (a b) (b a)))))
integerp-prod-of-3-first-twotheorem
(defthm integerp-prod-of-3-first-two
  (implies (and (integerp (* a b)) (integerp c))
    (integerp (* a b c)))
  :hints (("Goal" :in-theory (disable integerp-prod-of-3-last-two
       integerp-prod-of-3-first-and-last)
     :use (:instance integerp-prod-of-3-last-two (a c) (c a)))))
integerp-+-reduce-leading-constanttheorem
(defthm integerp-+-reduce-leading-constant
  (implies (syntaxp (and (quotep k) (or (>= (cadr k) 1) (< (cadr k) 0))))
    (equal (integerp (+ k x))
      (integerp (+ (+ k (- (floor k 1))) x)))))