minus - ACL2 Book

other

(in-package "ACL2")

integerp-of--theorem

(defthm integerp-of--
  (equal (integerp (- x)) (integerp (fix x)))
  :hints (("Goal" :cases ((integerp x)))))

integerp-of---when-integerptheorem

(defthmd integerp-of---when-integerp
  (implies (integerp x) (integerp (- x))))

in-theory

(in-theory (disable rationalp-unary--))

rationalp-of--theorem

(defthm rationalp-of--
  (equal (rationalp (- x)) (rationalp (fix x)))
  :hints (("Goal" :cases ((rationalp x)))))

--of--theorem

(defthm --of-- (equal (- (- x)) (fix x)))

equal-of---and-constanttheorem

(defthm equal-of---and-constant
  (implies (syntaxp (quotep k))
    (equal (equal k (- x))
      (and (acl2-numberp k) (equal (fix x) (- k))))))

equal-of---when-variabletheorem

(defthm equal-of---when-variable
  (implies (and (syntaxp (and (symbolp x) (not (symbolp k)))))
    (equal (equal k (- x))
      (and (acl2-numberp k) (equal (fix x) (- k))))))

<-of-minus-and-constanttheorem

(defthm <-of-minus-and-constant
  (implies (syntaxp (quotep k))
    (equal (< (- x) k) (< (- k) x)))
  :hints (("Goal" :cases ((< (- x) k)))))

<-of-constant-and-minustheorem

(defthm <-of-constant-and-minus
  (implies (syntaxp (quotep k))
    (equal (< k (- x)) (< x (- k))))
  :rule-classes ((:rewrite :loop-stopper nil))
  :hints (("Goal" :cases ((< k (- x))))))

equal-of-minus-selftheorem

(defthm equal-of-minus-self
  (equal (equal x (- x)) (equal x 0)))

equal-of---and--theorem

(defthm equal-of---and--
  (equal (equal (- x) (- y)) (equal (fix x) (fix y))))

<-of---and--theorem

(defthm <-of---and--
  (equal (< (- x) (- y)) (< (fix y) (fix x)))
  :hints (("Goal" :cases ((< (- x) (- y))))))

x-less-than-minus-xtheorem

(defthm x-less-than-minus-x
  (equal (< x (- x)) (< x 0))
  :hints (("Goal" :cases ((< x 0)))))

move-minus-to-constanttheorem

(defthm move-minus-to-constant
  (implies (syntaxp (quotep k))
    (equal (equal k (- x))
      (if (acl2-numberp x)
        (and (equal (- k) x) (acl2-numberp k))
        (equal k 0)))))