abs

other

(in-package "ACL2")

include-book

(include-book "top")

abs-*theorem

(defthm abs-*
  (implies (and (real/rationalp x) (real/rationalp y))
    (equal (abs (* x y)) (* (abs x) (abs y)))))

abs-uminustheorem

(defthm abs-uminus (equal (abs (- x)) (abs (fix x))))

realp-abstheorem

(defthm realp-abs
  (implies (real/rationalp x) (real/rationalp (abs x))))

numberp-abstheorem

(defthm numberp-abs
  (implies (acl2-numberp x) (acl2-numberp (abs x))))

abs-x->-0theorem

(defthm abs-x->-0
  (implies (and (real/rationalp x) (<= 0 x))
    (equal (abs x) x)))

abs-x-=-0-iff-x=0theorem

(defthm abs-x-=-0-iff-x=0
  (implies (and (real/rationalp x) (not (= 0 x)))
    (< 0 (abs x))))

not-abs-x-<-0theorem

(defthm not-abs-x-<-0
  (not (< (abs x) 0))
  :rule-classes (:rewrite :type-prescription))

abs-x-generalize-weaktheorem

(defthm abs-x-generalize-weak
  (implies (real/rationalp x)
    (and (<= 0 (abs x)) (real/rationalp (abs x))))
  :rule-classes (:generalize :rewrite))

abs-x-generalize-strongtheorem

(defthm abs-x-generalize-strong
  (implies (and (real/rationalp x) (not (equal x 0)))
    (< 0 (abs x)))
  :rule-classes (:generalize :rewrite))

abs-triangletheorem

(defthm abs-triangle (<= (abs (+ x y)) (+ (abs x) (abs y))))

in-theory

(in-theory (disable abs))

Included Books