Built-in axioms and theorems about numbers.
Definition:
(defaxiom closure (and (acl2-numberp (+ x y)) (acl2-numberp (* x y)) (acl2-numberp (- x)) (acl2-numberp (/ x))) :rule-classes nil)
Definition:
(defaxiom associativity-of-+ (equal (+ (+ x y) z) (+ x (+ y z))))
Definition:
(defaxiom commutativity-of-+ (equal (+ x y) (+ y x)))
Definition:
(defaxiom unicity-of-0 (equal (+ 0 x) (fix x)))
Definition:
(defaxiom inverse-of-+ (equal (+ x (- x)) 0))
Definition:
(defaxiom associativity-of-* (equal (* (* x y) z) (* x (* y z))))
Definition:
(defaxiom commutativity-of-* (equal (* x y) (* y x)))
Definition:
(defaxiom unicity-of-1 (equal (* 1 x) (fix x)))
Definition:
(defaxiom inverse-of-* (implies (and (acl2-numberp x) (not (equal x 0))) (equal (* x (/ x)) 1)))
Definition:
(defaxiom distributivity (equal (* x (+ y z)) (+ (* x y) (* x z))))
Definition:
(defaxiom <-on-others (equal (< x y) (< (+ x (- y)) 0)) :rule-classes nil)
Definition:
(defaxiom zero (not (< 0 0)) :rule-classes nil)
Definition:
(defaxiom trichotomy (and (implies (acl2-numberp x) (or (< 0 x) (equal x 0) (< 0 (- x)))) (or (not (< 0 x)) (not (< 0 (- x))))) :rule-classes nil)
Definition:
(defaxiom positive (and (implies (and (< 0 x) (< 0 y)) (< 0 (+ x y))) (implies (and (real/rationalp x) (real/rationalp y) (< 0 x) (< 0 y)) (< 0 (* x y)))) :rule-classes nil)
Definition:
(defaxiom rational-implies1 (implies (rationalp x) (and (integerp (denominator x)) (integerp (numerator x)) (< 0 (denominator x)))) :rule-classes nil)
Definition:
(defaxiom rational-implies2 (implies (rationalp x) (equal (* (/ (denominator x)) (numerator x)) x)))
Definition:
(defaxiom integer-implies-rational (implies (integerp x) (rationalp x)) :rule-classes nil)
Definition:
(defaxiom complex-implies1 (and (real/rationalp (realpart x)) (real/rationalp (imagpart x))) :rule-classes nil)
Definition:
(defaxiom complex-definition (implies (and (real/rationalp x) (real/rationalp y)) (equal (complex x y) (+ x (* #C(0 1) y)))))
Definition:
(defaxiom nonzero-imagpart (implies (complex/complex-rationalp x) (not (equal 0 (imagpart x)))) :rule-classes nil)
Definition:
(defaxiom realpart-imagpart-elim (implies (acl2-numberp x) (equal (complex (realpart x) (imagpart x)) x)) :rule-classes (:rewrite :elim))
Definition:
(defaxiom realpart-complex (implies (and (real/rationalp x) (real/rationalp y)) (equal (realpart (complex x y)) x)))
Definition:
(defaxiom imagpart-complex (implies (and (real/rationalp x) (real/rationalp y)) (equal (imagpart (complex x y)) y)))
Definition:
(defaxiom nonnegative-product (implies (real/rationalp x) (and (real/rationalp (* x x)) (<= 0 (* x x)))) :rule-classes ((:type-prescription :typed-term (* x x))))
Definition:
(defaxiom integer-0 (integerp 0) :rule-classes nil)
Definition:
(defaxiom integer-1 (integerp 1) :rule-classes nil)
Definition:
(defaxiom integer-step (implies (integerp x) (and (integerp (+ x 1)) (integerp (+ x -1)))) :rule-classes nil)
Definition:
(defaxiom lowest-terms (implies (and (integerp n) (rationalp x) (integerp r) (integerp q) (< 0 n) (equal (numerator x) (* n r)) (equal (denominator x) (* n q))) (equal n 1)) :rule-classes nil)
Definition:
(defaxiom completion-of-+ (equal (+ x y) (if (acl2-numberp x) (if (acl2-numberp y) (+ x y) x) (if (acl2-numberp y) y 0))) :rule-classes nil)
Definition:
(defaxiom completion-of-* (equal (* x y) (if (acl2-numberp x) (if (acl2-numberp y) (* x y) 0) 0)) :rule-classes nil)
Definition:
(defaxiom completion-of-unary-minus (equal (- x) (if (acl2-numberp x) (- x) 0)) :rule-classes nil)
Definition:
(defaxiom completion-of-unary-/ (equal (/ x) (if (and (acl2-numberp x) (not (equal x 0))) (/ x) 0)) :rule-classes nil)
Definition:
(defaxiom completion-of-< (equal (< x y) (if (and (real/rationalp x) (real/rationalp y)) (< x y) (let ((x1 (if (acl2-numberp x) x 0)) (y1 (if (acl2-numberp y) y 0))) (or (< (realpart x1) (realpart y1)) (and (equal (realpart x1) (realpart y1)) (< (imagpart x1) (imagpart y1))))))) :rule-classes nil)
Definition:
(defaxiom completion-of-complex (equal (complex x y) (complex (if (real/rationalp x) x 0) (if (real/rationalp y) y 0))) :rule-classes nil)
Definition:
(defaxiom completion-of-numerator (equal (numerator x) (if (rationalp x) (numerator x) 0)) :rule-classes nil)
Definition:
(defaxiom completion-of-denominator (equal (denominator x) (if (rationalp x) (denominator x) 1)) :rule-classes nil)
Definition:
(defaxiom completion-of-realpart (equal (realpart x) (if (acl2-numberp x) (realpart x) 0)) :rule-classes nil)
Definition:
(defaxiom completion-of-imagpart (equal (imagpart x) (if (acl2-numberp x) (imagpart x) 0)) :rule-classes nil)
Theorem:
(defthm zp-compound-recognizer (equal (zp x) (or (not (integerp x)) (<= x 0))) :rule-classes :compound-recognizer)
Theorem:
(defthm zp-open (implies (syntaxp (not (variablep x))) (equal (zp x) (if (integerp x) (<= x 0) t))))
Theorem:
(defthm zip-compound-recognizer (equal (zip x) (or (not (integerp x)) (equal x 0))) :rule-classes :compound-recognizer)
Theorem:
(defthm zip-open (implies (syntaxp (not (variablep x))) (equal (zip x) (or (not (integerp x)) (equal x 0)))))
Theorem:
(defthm complex-equal (implies (and (real/rationalp x1) (real/rationalp y1) (real/rationalp x2) (real/rationalp y2)) (equal (equal (complex x1 y1) (complex x2 y2)) (and (equal x1 x2) (equal y1 y2)))))
Theorem:
(defthm natp-compound-recognizer (equal (natp x) (and (integerp x) (<= 0 x))) :rule-classes :compound-recognizer)
Theorem:
(defthm bitp-compound-recognizer (equal (bitp x) (or (equal x 0) (equal x 1))) :rule-classes :compound-recognizer)
Theorem:
(defthm posp-compound-recognizer (equal (posp x) (and (integerp x) (< 0 x))) :rule-classes :compound-recognizer)
Theorem:
(defthm expt-type-prescription-non-zero-base (implies (and (acl2-numberp r) (not (equal r 0))) (not (equal (expt r i) 0))) :rule-classes :type-prescription)
Theorem:
(defthm rationalp-expt-type-prescription (implies (rationalp r) (rationalp (expt r i))) :rule-classes :type-prescription)
Theorem:
(defthm integer-range-p-forward (implies (and (integer-range-p lower (1+ upper-1) x) (integerp upper-1)) (and (integerp x) (<= lower x) (<= x upper-1))) :rule-classes :forward-chaining)
Theorem:
(defthm signed-byte-p-forward-to-integerp (implies (signed-byte-p n x) (integerp x)) :rule-classes :forward-chaining)
Theorem:
(defthm unsigned-byte-p-forward-to-nonnegative-integerp (implies (unsigned-byte-p n x) (and (integerp x) (<= 0 x))) :rule-classes :forward-chaining)
Theorem:
(defthm rationalp-+ (implies (and (rationalp x) (rationalp y)) (rationalp (+ x y))))
Theorem:
(defthm rationalp-* (implies (and (rationalp x) (rationalp y)) (rationalp (* x y))))
Theorem:
(defthm rationalp-unary-- (implies (rationalp x) (rationalp (- x))))
Theorem:
(defthm rationalp-unary-/ (implies (rationalp x) (rationalp (/ x))))
Theorem:
(defthm rationalp-implies-acl2-numberp (implies (rationalp x) (acl2-numberp x)))
Theorem:
(defthm default-+-1 (implies (not (acl2-numberp x)) (equal (+ x y) (fix y))))
Theorem:
(defthm default-+-2 (implies (not (acl2-numberp y)) (equal (+ x y) (fix x))))
Theorem:
(defthm default-*-1 (implies (not (acl2-numberp x)) (equal (* x y) 0)))
Theorem:
(defthm default-*-2 (implies (not (acl2-numberp y)) (equal (* x y) 0)))
Theorem:
(defthm default-unary-minus (implies (not (acl2-numberp x)) (equal (- x) 0)))
Theorem:
(defthm default-unary-/ (implies (or (not (acl2-numberp x)) (equal x 0)) (equal (/ x) 0)))
Theorem:
(defthm default-<-1 (implies (not (acl2-numberp x)) (equal (< x y) (< 0 y))))
Theorem:
(defthm default-<-2 (implies (not (acl2-numberp y)) (equal (< x y) (< x 0))))
Theorem:
(defthm default-complex-1 (implies (not (real/rationalp x)) (equal (complex x y) (complex 0 y))))
Theorem:
(defthm default-complex-2 (implies (not (real/rationalp y)) (equal (complex x y) (if (real/rationalp x) x 0))))
Theorem:
(defthm complex-0 (equal (complex x 0) (realfix x)))
Theorem:
(defthm add-def-complex (equal (+ x y) (complex (+ (realpart x) (realpart y)) (+ (imagpart x) (imagpart y)))) :rule-classes nil)
Theorem:
(defthm realpart-+ (equal (realpart (+ x y)) (+ (realpart x) (realpart y))))
Theorem:
(defthm imagpart-+ (equal (imagpart (+ x y)) (+ (imagpart x) (imagpart y))))
Theorem:
(defthm default-numerator (implies (not (rationalp x)) (equal (numerator x) 0)))
Theorem:
(defthm default-denominator (implies (not (rationalp x)) (equal (denominator x) 1)))
Theorem:
(defthm default-realpart (implies (not (acl2-numberp x)) (equal (realpart x) 0)))
Theorem:
(defthm default-imagpart (implies (not (acl2-numberp x)) (equal (imagpart x) 0)))
Theorem:
(defthm commutativity-2-of-+ (equal (+ x (+ y z)) (+ y (+ x z))))
Theorem:
(defthm fold-consts-in-+ (implies (and (syntaxp (quotep x)) (syntaxp (quotep y))) (equal (+ x (+ y z)) (+ (+ x y) z))))
Theorem:
(defthm distributivity-of-minus-over-+ (equal (- (+ x y)) (+ (- x) (- y))))
Theorem:
(defthm pos-listp-forward-to-integer-listp (implies (pos-listp x) (integer-listp x)) :rule-classes :forward-chaining)