• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
    • Real
    • ACL2-tutorial
    • Debugging
    • Miscellaneous
    • Prover-output
    • Built-in-theorems
      • Built-in-theorems-about-arithmetic
      • Built-in-theorems-about-symbols
      • Built-in-theorems-about-characters
      • Built-in-theorems-about-lists
      • Built-in-theorems-about-arrays
      • Built-in-theorems-about-strings
      • Built-in-theorems-about-alists
      • Built-in-theorems-about-total-order
      • Built-in-theorems-about-system-utilities
      • Built-in-theorems-about-cons-pairs
      • Built-in-theorems-for-tau
      • Built-in-theorems-about-bad-atoms
      • Built-in-theorems-about-logical-connectives
      • Built-in-theorems-about-booleans
      • Built-in-theorems-about-random$
      • Built-in-theorems-about-eqlables
    • Macros
    • Interfacing-tools
    • About-ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Built-in-theorems

Built-in-theorems-about-arithmetic

Built-in theorems about arithmetic.

Definition: closure

(defaxiom closure
          (and (acl2-numberp (+ x y))
               (acl2-numberp (* x y))
               (acl2-numberp (- x))
               (acl2-numberp (/ x)))
          :rule-classes nil)

Definition: associativity-of-+

(defaxiom associativity-of-+
          (equal (+ (+ x y) z) (+ x (+ y z))))

Definition: commutativity-of-+

(defaxiom commutativity-of-+
          (equal (+ x y) (+ y x)))

Definition: unicity-of-0

(defaxiom unicity-of-0 (equal (+ 0 x) (fix x)))

Definition: inverse-of-+

(defaxiom inverse-of-+ (equal (+ x (- x)) 0))

Definition: associativity-of-*

(defaxiom associativity-of-*
          (equal (* (* x y) z) (* x (* y z))))

Definition: commutativity-of-*

(defaxiom commutativity-of-*
          (equal (* x y) (* y x)))

Definition: unicity-of-1

(defaxiom unicity-of-1 (equal (* 1 x) (fix x)))

Definition: inverse-of-*

(defaxiom inverse-of-*
          (implies (and (acl2-numberp x) (not (equal x 0)))
                   (equal (* x (/ x)) 1)))

Definition: distributivity

(defaxiom distributivity
          (equal (* x (+ y z))
                 (+ (* x y) (* x z))))

Definition: <-on-others

(defaxiom <-on-others
          (equal (< x y) (< (+ x (- y)) 0))
          :rule-classes nil)

Definition: zero

(defaxiom zero (not (< 0 0))
          :rule-classes nil)

Definition: trichotomy

(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: positive

(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: rational-implies1

(defaxiom rational-implies1
          (implies (rationalp x)
                   (and (integerp (denominator x))
                        (integerp (numerator x))
                        (< 0 (denominator x))))
          :rule-classes nil)

Definition: rational-implies2

(defaxiom rational-implies2
          (implies (rationalp x)
                   (equal (* (/ (denominator x)) (numerator x))
                          x)))

Definition: integer-implies-rational

(defaxiom integer-implies-rational
          (implies (integerp x) (rationalp x))
          :rule-classes nil)

Definition: complex-implies1

(defaxiom complex-implies1
          (and (real/rationalp (realpart x))
               (real/rationalp (imagpart x)))
          :rule-classes nil)

Definition: complex-definition

(defaxiom complex-definition
          (implies (and (real/rationalp x)
                        (real/rationalp y))
                   (equal (complex x y) (+ x (* #C(0 1) y)))))

Definition: nonzero-imagpart

(defaxiom nonzero-imagpart
          (implies (complex/complex-rationalp x)
                   (not (equal 0 (imagpart x))))
          :rule-classes nil)

Definition: realpart-imagpart-elim

(defaxiom realpart-imagpart-elim
          (implies (acl2-numberp x)
                   (equal (complex (realpart x) (imagpart x))
                          x))
          :rule-classes (:rewrite :elim))

Definition: realpart-complex

(defaxiom realpart-complex
          (implies (and (real/rationalp x)
                        (real/rationalp y))
                   (equal (realpart (complex x y)) x)))

Definition: imagpart-complex

(defaxiom imagpart-complex
          (implies (and (real/rationalp x)
                        (real/rationalp y))
                   (equal (imagpart (complex x y)) y)))

Definition: nonnegative-product

(defaxiom nonnegative-product
          (implies (real/rationalp x)
                   (and (real/rationalp (* x x))
                        (<= 0 (* x x))))
          :rule-classes ((:type-prescription :typed-term (* x x))))

Definition: integer-0

(defaxiom integer-0 (integerp 0)
          :rule-classes nil)

Definition: integer-1

(defaxiom integer-1 (integerp 1)
          :rule-classes nil)

Definition: integer-step

(defaxiom integer-step
          (implies (integerp x)
                   (and (integerp (+ x 1))
                        (integerp (+ x -1))))
          :rule-classes nil)

Definition: lowest-terms

(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: completion-of-+

(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: completion-of-*

(defaxiom completion-of-*
          (equal (* x y)
                 (if (acl2-numberp x)
                     (if (acl2-numberp y) (* x y) 0)
                     0))
          :rule-classes nil)

Definition: completion-of-unary-minus

(defaxiom completion-of-unary-minus
          (equal (- x)
                 (if (acl2-numberp x) (- x) 0))
          :rule-classes nil)

Definition: completion-of-unary-/

(defaxiom completion-of-unary-/
          (equal (/ x)
                 (if (and (acl2-numberp x) (not (equal x 0)))
                     (/ x)
                     0))
          :rule-classes nil)

Definition: completion-of-<

(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: completion-of-complex

(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: completion-of-numerator

(defaxiom completion-of-numerator
          (equal (numerator x)
                 (if (rationalp x) (numerator x) 0))
          :rule-classes nil)

Definition: completion-of-denominator

(defaxiom completion-of-denominator
          (equal (denominator x)
                 (if (rationalp x) (denominator x) 1))
          :rule-classes nil)

Definition: completion-of-realpart

(defaxiom completion-of-realpart
          (equal (realpart x)
                 (if (acl2-numberp x) (realpart x) 0))
          :rule-classes nil)

Definition: completion-of-imagpart

(defaxiom completion-of-imagpart
          (equal (imagpart x)
                 (if (acl2-numberp x) (imagpart x) 0))
          :rule-classes nil)

Theorem: zp-compound-recognizer

(defthm zp-compound-recognizer
        (equal (zp x)
               (or (not (integerp x)) (<= x 0)))
        :rule-classes :compound-recognizer)

Theorem: zp-open

(defthm zp-open
        (implies (syntaxp (not (variablep x)))
                 (equal (zp x)
                        (if (integerp x) (<= x 0) t))))

Theorem: zip-compound-recognizer

(defthm zip-compound-recognizer
        (equal (zip x)
               (or (not (integerp x)) (equal x 0)))
        :rule-classes :compound-recognizer)

Theorem: zip-open

(defthm zip-open
        (implies (syntaxp (not (variablep x)))
                 (equal (zip x)
                        (or (not (integerp x)) (equal x 0)))))

Theorem: complex-equal

(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: natp-compound-recognizer

(defthm natp-compound-recognizer
        (equal (natp x)
               (and (integerp x) (<= 0 x)))
        :rule-classes :compound-recognizer)

Theorem: bitp-compound-recognizer

(defthm bitp-compound-recognizer
        (equal (bitp x)
               (or (equal x 0) (equal x 1)))
        :rule-classes :compound-recognizer)

Theorem: posp-compound-recognizer

(defthm posp-compound-recognizer
        (equal (posp x)
               (and (integerp x) (< 0 x)))
        :rule-classes :compound-recognizer)

Theorem: expt-type-prescription-non-zero-base

(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: rationalp-expt-type-prescription

(defthm rationalp-expt-type-prescription
        (implies (rationalp r)
                 (rationalp (expt r i)))
        :rule-classes :type-prescription)

Theorem: integer-range-p-forward

(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: signed-byte-p-forward-to-integerp

(defthm signed-byte-p-forward-to-integerp
        (implies (signed-byte-p n x)
                 (integerp x))
        :rule-classes :forward-chaining)

Theorem: unsigned-byte-p-forward-to-nonnegative-integerp

(defthm unsigned-byte-p-forward-to-nonnegative-integerp
        (implies (unsigned-byte-p n x)
                 (and (integerp x) (<= 0 x)))
        :rule-classes :forward-chaining)

Theorem: rationalp-+

(defthm rationalp-+
        (implies (and (rationalp x) (rationalp y))
                 (rationalp (+ x y))))

Theorem: rationalp-*

(defthm rationalp-*
        (implies (and (rationalp x) (rationalp y))
                 (rationalp (* x y))))

Theorem: rationalp-unary--

(defthm rationalp-unary--
        (implies (rationalp x)
                 (rationalp (- x))))

Theorem: rationalp-unary-/

(defthm rationalp-unary-/
        (implies (rationalp x)
                 (rationalp (/ x))))

Theorem: rationalp-implies-acl2-numberp

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

Theorem: default-+-1

(defthm default-+-1
        (implies (not (acl2-numberp x))
                 (equal (+ x y) (fix y))))

Theorem: default-+-2

(defthm default-+-2
        (implies (not (acl2-numberp y))
                 (equal (+ x y) (fix x))))

Theorem: default-*-1

(defthm default-*-1
        (implies (not (acl2-numberp x))
                 (equal (* x y) 0)))

Theorem: default-*-2

(defthm default-*-2
        (implies (not (acl2-numberp y))
                 (equal (* x y) 0)))

Theorem: default-unary-minus

(defthm default-unary-minus
        (implies (not (acl2-numberp x))
                 (equal (- x) 0)))

Theorem: default-unary-/

(defthm default-unary-/
        (implies (or (not (acl2-numberp x)) (equal x 0))
                 (equal (/ x) 0)))

Theorem: default-<-1

(defthm default-<-1
        (implies (not (acl2-numberp x))
                 (equal (< x y) (< 0 y))))

Theorem: default-<-2

(defthm default-<-2
        (implies (not (acl2-numberp y))
                 (equal (< x y) (< x 0))))

Theorem: default-complex-1

(defthm default-complex-1
        (implies (not (real/rationalp x))
                 (equal (complex x y) (complex 0 y))))

Theorem: default-complex-2

(defthm default-complex-2
        (implies (not (real/rationalp y))
                 (equal (complex x y)
                        (if (real/rationalp x) x 0))))

Theorem: complex-0

(defthm complex-0
        (equal (complex x 0) (realfix x)))

Theorem: add-def-complex

(defthm add-def-complex
        (equal (+ x y)
               (complex (+ (realpart x) (realpart y))
                        (+ (imagpart x) (imagpart y))))
        :rule-classes nil)

Theorem: realpart-+

(defthm realpart-+
        (equal (realpart (+ x y))
               (+ (realpart x) (realpart y))))

Theorem: imagpart-+

(defthm imagpart-+
        (equal (imagpart (+ x y))
               (+ (imagpart x) (imagpart y))))

Theorem: default-numerator

(defthm default-numerator
        (implies (not (rationalp x))
                 (equal (numerator x) 0)))

Theorem: default-denominator

(defthm default-denominator
        (implies (not (rationalp x))
                 (equal (denominator x) 1)))

Theorem: default-realpart

(defthm default-realpart
        (implies (not (acl2-numberp x))
                 (equal (realpart x) 0)))

Theorem: default-imagpart

(defthm default-imagpart
        (implies (not (acl2-numberp x))
                 (equal (imagpart x) 0)))

Theorem: commutativity-2-of-+

(defthm commutativity-2-of-+
        (equal (+ x (+ y z)) (+ y (+ x z))))

Theorem: fold-consts-in-+

(defthm fold-consts-in-+
        (implies (and (syntaxp (quotep x))
                      (syntaxp (quotep y)))
                 (equal (+ x (+ y z)) (+ (+ x y) z))))

Theorem: distributivity-of-minus-over-+

(defthm distributivity-of-minus-over-+
        (equal (- (+ x y)) (+ (- x) (- y))))

Theorem: pos-listp-forward-to-integer-listp

(defthm pos-listp-forward-to-integer-listp
        (implies (pos-listp x)
                 (integer-listp x))
        :rule-classes :forward-chaining)