plus - ACL2 Book

other

(in-package "ACL2")

integerp-of-+-when-integerp-1theorem

(defthm integerp-of-+-when-integerp-1
  (implies (integerp x)
    (equal (integerp (+ x y)) (integerp (fix y))))
  :hints (("Goal" :cases ((integerp y)))))

integerp-of-+-when-integerp-2theorem

(defthm integerp-of-+-when-integerp-2
  (implies (integerp y)
    (equal (integerp (+ x y)) (integerp (fix x))))
  :hints (("Goal" :use (:instance integerp-of-+-when-integerp-1 (x y) (y x)))))

integerp-of-+theorem

(defthmd integerp-of-+
  (implies (and (integerp x) (integerp y)) (integerp (+ x y))))

integerp-of-+-when-integerp-1-cheaptheorem

(defthm integerp-of-+-when-integerp-1-cheap
  (implies (integerp x)
    (equal (integerp (+ x y)) (integerp (fix y))))
  :rule-classes ((:rewrite :backchain-limit-lst (0))))

+-combine-constantstheorem

(defthm +-combine-constants
  (implies (syntaxp (and (quotep k2) (quotep k1)))
    (equal (+ k1 k2 i) (+ (+ k1 k2) i))))

equal-of-+-cancel-1+theorem

(defthm equal-of-+-cancel-1+
  (equal (equal (+ x y) x)
    (and (equal 0 (fix y)) (acl2-numberp x))))

equal-of-+-cancel-1+-alttheorem

(defthmd equal-of-+-cancel-1+-alt
  (equal (equal x (+ x y))
    (and (equal 0 (fix y)) (acl2-numberp x))))

equal-of-+-cancel-2theorem

(defthm equal-of-+-cancel-2
  (equal (equal (+ y x) x)
    (and (equal 0 (fix y)) (acl2-numberp x))))

equal-of-+-cancel-2-alttheorem

(defthmd equal-of-+-cancel-2-alt
  (equal (equal x (+ y x))
    (and (equal 0 (fix y)) (acl2-numberp x))))

equal-of-+-cancel-2+theorem

(defthm equal-of-+-cancel-2+
  (equal (equal (+ y1 x y2) x)
    (and (equal (+ y1 y2) 0) (acl2-numberp x))))

equal-of-+-cancel-2+-alttheorem

(defthmd equal-of-+-cancel-2+-alt
  (equal (equal x (+ y1 x y2))
    (and (equal (+ y1 y2) 0) (acl2-numberp x))))

equal-of-+-cancel-3theorem

(defthm equal-of-+-cancel-3
  (equal (equal (+ y1 y2 x) x)
    (and (equal (+ y1 y2) 0) (acl2-numberp x))))

equal-of-+-cancel-3-alttheorem

(defthmd equal-of-+-cancel-3-alt
  (equal (equal x (+ y1 y2 x))
    (and (equal (+ y1 y2) 0) (acl2-numberp x))))

equal-of-+-and-+-cancel-1+-1+theorem

(defthm equal-of-+-and-+-cancel-1+-1+
  (equal (equal (+ x y1) (+ x y2)) (equal (fix y1) (fix y2))))

equal-of-+-and-+-cancel-1+-2theorem

(defthm equal-of-+-and-+-cancel-1+-2
  (equal (equal (+ x y1) (+ y2 x)) (equal (fix y1) (fix y2))))

equal-of-+-and-+-cancel-2-1+theorem

(defthmd equal-of-+-and-+-cancel-2-1+
  (equal (equal (+ y1 x) (+ x y2)) (equal (fix y1) (fix y2))))

equal-of-+-and-+-cancel-2-2theorem

(defthm equal-of-+-and-+-cancel-2-2
  (equal (equal (+ y1 x) (+ y2 x)) (equal (fix y1) (fix y2))))

equal-of-+-and-+-cancel-1+-2+theorem

(defthm equal-of-+-and-+-cancel-1+-2+
  (equal (equal (+ x y1) (+ y2 x y3))
    (equal (fix y1) (+ y2 y3))))

equal-of-+-and-+-cancel-2+-2+theorem

(defthm equal-of-+-and-+-cancel-2+-2+
  (equal (equal (+ y1 x y2) (+ y3 x y4))
    (equal (+ y1 y2) (+ y3 y4))))

equal-of-+-and-+-cancel-3-3theorem

(defthm equal-of-+-and-+-cancel-3-3
  (equal (equal (+ y1 y2 x) (+ y3 y4 x))
    (equal (+ y1 y2) (+ y3 y4))))

equal-of-+-and-+-cancel-3-1+theorem

(defthm equal-of-+-and-+-cancel-3-1+
  (equal (equal (+ y1 y2 x) (+ x y3))
    (equal (+ y1 y2) (fix y3))))

equal-of-+-and-+-cancel-2-3theorem

(defthm equal-of-+-and-+-cancel-2-3
  (equal (equal (+ y1 x) (+ y2 y3 x))
    (equal (fix y1) (+ y2 y3))))

equal-of-+-and-+-cancel-2-4theorem

(defthm equal-of-+-and-+-cancel-2-4
  (equal (equal (+ y1 x) (+ y2 y3 y4 x))
    (equal (fix y1) (+ y2 y3 y4))))

<-of-+-cancel-1+-1theorem

(defthm <-of-+-cancel-1+-1
  (equal (< (+ x y) x) (< y 0))
  :hints (("Goal" :cases ((< y 0)))))

<-of-+-cancel-1-1+theorem

(defthm <-of-+-cancel-1-1+
  (equal (< x (+ x y)) (< 0 y))
  :hints (("Goal" :cases ((< 0 y)))))

<-of-+-cancel-1+-1+theorem

(defthm <-of-+-cancel-1+-1+
  (equal (< (+ x y) (+ x z)) (< y z))
  :hints (("Goal" :cases ((< y z)))))

<-of-+-cancel-1-2theorem

(defthm <-of-+-cancel-1-2 (equal (< x (+ y x)) (< 0 y)))

<-of-+-cancel-1-2+theorem

(defthm <-of-+-cancel-1-2+
  (equal (< x (+ y x z)) (< 0 (+ y z))))

<-of-+-cancel-1+-2+theorem

(defthm <-of-+-cancel-1+-2+
  (equal (< (+ x w) (+ y x z)) (< w (+ y z)))
  :hints (("Goal" :cases ((< w (+ y z))))))

<-of-+-cancel-1+-2theorem

(defthm <-of-+-cancel-1+-2
  (equal (< (+ x y) (+ z x)) (< y z)))

<-of-+-cancel-2-2theorem

(defthm <-of-+-cancel-2-2
  (equal (< (+ y x) (+ z x)) (< y z)))

<-of-+-cancel-2-1+theorem

(defthm <-of-+-cancel-2-1+
  (equal (< (+ y x) (+ x z)) (< y z)))

<-of-+-cancel-1-3theorem

(defthm <-of-+-cancel-1-3
  (equal (< x (+ y (+ z x))) (< 0 (+ y z))))

<-of-+-cancel-3-1theorem

(defthm <-of-+-cancel-3-1
  (equal (< (+ y (+ z x)) x) (< (+ y z) 0)))

<-of-+-cancel-3-1+theorem

(defthm <-of-+-cancel-3-1+
  (equal (< (+ y y2 x) (+ x z)) (< (+ y y2) z)))

<-of-+-cancel-2-1theorem

(defthm <-of-+-cancel-2-1 (equal (< (+ y x) x) (< y 0)))

<-of-+-cancel-2+-1theorem

(defthm <-of-+-cancel-2+-1
  (equal (< (+ y x z) x) (< (+ y z) 0)))

<-of-+-cancel-1-3+theorem

(defthm <-of-+-cancel-1-3+
  (equal (< x (+ y1 y2 x y3)) (< 0 (+ y1 y2 y3))))

<-of-+-combine-constants-1theorem

(defthm <-of-+-combine-constants-1
  (implies (syntaxp (and (quotep k2) (quotep k1)))
    (equal (< k1 (+ k2 x)) (< (- k1 k2) x)))
  :hints (("Goal" :cases ((< k1 (+ k2 x))))))

<-of-+-combine-constants-2theorem

(defthm <-of-+-combine-constants-2
  (implies (syntaxp (and (quotep k2) (quotep k1)))
    (equal (< (+ k1 x) k2) (< x (- k2 k1))))
  :hints (("Goal" :cases ((< (+ k1 x) k2)))))

<-of-+-and-+-combine-constantstheorem

(defthm <-of-+-and-+-combine-constants
  (implies (syntaxp (and (quotep k2) (quotep k1)))
    (equal (< (+ k1 x) (+ k2 y))
      (if (< k1 k2)
        (< x (+ (- k2 k1) y))
        (< (+ (- k1 k2) x) y))))
  :hints (("Goal" :cases ((< (+ k1 x) (+ k2 y))))))

equal-of-+-combine-constantstheorem

(defthm equal-of-+-combine-constants
  (implies (syntaxp (and (quotep k1) (quotep k2)))
    (equal (equal k1 (+ k2 x))
      (and (acl2-numberp k1) (equal (- k1 k2) (fix x))))))

rationalp-of-+-when-rationalp-arg1theorem

(defthm rationalp-of-+-when-rationalp-arg1
  (implies (rationalp x)
    (equal (rationalp (+ x y)) (rationalp (fix y))))
  :hints (("Goal" :cases ((rationalp (fix y))))))

rationalp-of-+-when-rationalp-arg2theorem

(defthm rationalp-of-+-when-rationalp-arg2
  (implies (rationalp y)
    (equal (rationalp (+ x y)) (rationalp (fix x))))
  :hints (("Goal" :cases ((rationalp (fix x))))))

in-theory

(in-theory (disable rationalp-+))

<-of-+-arg1-when-negative-constanttheorem

(defthm <-of-+-arg1-when-negative-constant
  (implies (and (syntaxp (quotep k)) (< k 0))
    (equal (< (+ k x) y) (< x (+ (- k) y))))
  :hints (("Goal" :cases ((< (+ k x) y)))))

<-of-+-arg2-when-negative-constanttheorem

(defthm <-of-+-arg2-when-negative-constant
  (implies (and (syntaxp (quotep k)) (< k 0))
    (equal (< y (+ k x)) (< (+ (- k) y) x)))
  :hints (("Goal" :cases ((< y (+ k x))))))

equal-of-+-when-negative-constanttheorem

(defthm equal-of-+-when-negative-constant
  (implies (syntaxp (and (quotep k)
        (< (unquote k) 0)
        (if (symbolp x)
          (symbolp y)
          t)))
    (equal (equal x (+ k y))
      (and (equal (+ (- k) x) (fix y)) (acl2-numberp x)))))

<-of-+-of-1-when-integerstheorem

(defthmd <-of-+-of-1-when-integers
  (implies (and (syntaxp (not (quotep y))) (integerp x) (integerp y))
    (equal (< x (+ 1 y)) (<= x y))))

binary-+-bring-constant-forwardtheorem

(defthmd binary-+-bring-constant-forward
  (implies (syntaxp (quotep x)) (equal (+ y x) (+ x y))))

natp-of-+-when-integerp-and-integerptheorem

(defthmd natp-of-+-when-integerp-and-integerp
  (implies (and (integerp x) (integerp y))
    (equal (natp (+ x y)) (<= 0 (+ x y)))))

natp-of-+-when-natp-and-natptheorem

(defthm natp-of-+-when-natp-and-natp
  (implies (and (natp x) (natp y)) (natp (+ x y))))

equal-of-+-and-+-cancel-constantstheorem

(defthm equal-of-+-and-+-cancel-constants
  (implies (syntaxp (and (quotep k1) (quotep k2)))
    (equal (equal (+ k1 x) (+ k2 y))
      (if (< k1 k2)
        (equal (fix x) (+ (- k2 k1) y))
        (equal (+ (- k1 k2) x) (fix y))))))

natp-of-+-of-constanttheorem

(defthmd natp-of-+-of-constant
  (implies (and (syntaxp (quotep x))
      (natp x)
      (<= (- x) y)
      (integerp y))
    (natp (+ x y)))
  :hints (("Goal" :in-theory (enable natp))))

natp-of-+-of-constant-strongtheorem

(defthmd natp-of-+-of-constant-strong
  (implies (and (syntaxp (quotep x)) (natp x) (integerp y))
    (equal (natp (+ x y)) (<= (- x) y)))
  :hints (("Goal" :in-theory (enable natp))))