• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math
    • Arithmetic
      • Lispfloat
      • Arithmetic-1
        • Inequalities-of-products
        • Basic-product-normalization
        • Inequalities-of-reciprocals
        • Arithmetic/natp-posp
        • Basic-expt-normalization
        • More-rational-identities
        • Inequalities-of-exponents
        • Basic-sum-normalization
        • Basic-rational-identities
        • Basic-expt-type-rules
        • Inequalities-of-sums
        • Basic-products-with-negations
        • Fc
      • Number-theory
      • Proof-by-arith
      • Arith-equivs
      • Number-theory
      • Arithmetic-3
      • Arithmetic-2
      • Arithmetic-light
      • Arithmetic-5
    • Bit-vectors
    • Algebra

• Arithmetic-1

Basic-product-normalization

Trivial normalization and cancellation rules for products.

Definitions and Theorems

Theorem: commutativity-2-of-*

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

Theorem: functional-self-inversion-of-/

(defthm functional-self-inversion-of-/
        (equal (/ (/ x)) (fix x)))

Theorem: distributivity-of-/-over-*

(defthm distributivity-of-/-over-*
        (equal (/ (* x y)) (* (/ x) (/ y))))

Theorem: /-cancellation-on-right

(defthm /-cancellation-on-right
        (implies (and (fc (acl2-numberp x))
                      (fc (not (equal x 0))))
                 (equal (* x y (/ x)) (fix y))))

Theorem: /-cancellation-on-left

(defthm /-cancellation-on-left
        (implies (and (fc (acl2-numberp x))
                      (fc (not (equal 0 x))))
                 (equal (* x (/ x) y) (fix y))))

Theorem: right-cancellation-for-*

(defthm right-cancellation-for-*
        (equal (equal (* x z) (* y z))
               (or (equal 0 (fix z))
                   (equal (fix x) (fix y)))))

Theorem: left-cancellation-for-*

(defthm left-cancellation-for-*
        (equal (equal (* z x) (* z y))
               (or (equal 0 (fix z))
                   (equal (fix x) (fix y)))))

Theorem: zero-is-only-zero-divisor

(defthm zero-is-only-zero-divisor
        (equal (equal (* x y) 0)
               (or (equal (fix x) 0)
                   (equal (fix y) 0))))

Theorem: equal-*-x-y-x

(defthm equal-*-x-y-x
        (equal (equal (* x y) x)
               (or (equal x 0)
                   (and (equal y 1) (acl2-numberp x)))))

Theorem: equal-*-x-y-y

(defthm equal-*-x-y-y
        (equal (equal (* x y) y)
               (or (equal y 0)
                   (and (equal x 1) (acl2-numberp y)))))

Theorem: equal-/

(defthm equal-/
        (implies (and (fc (acl2-numberp x))
                      (fc (not (equal 0 x))))
                 (equal (equal (/ x) y)
                        (equal 1 (* x y)))))

Theorem: numerator-nonzero-forward

(defthm
 numerator-nonzero-forward
 (implies (not (equal (numerator r) 0))
          (and (not (equal r 0))
               (acl2-numberp r)))
 :rule-classes ((:forward-chaining :trigger-terms ((numerator r)))))

Theorem: uniqueness-of-*-inverses

(defthm uniqueness-of-*-inverses
        (equal (equal (* x y) 1)
               (and (not (equal (fix x) 0))
                    (equal y (/ x)))))

Theorem: equal-/-/

(defthm equal-/-/
        (equal (equal (/ a) (/ b))
               (equal (fix a) (fix b))))

Theorem: equal-*-/-1

(defthm equal-*-/-1
        (implies (and (acl2-numberp x) (not (equal x 0)))
                 (equal (equal (* (/ x) y) z)
                        (and (acl2-numberp z)
                             (equal (fix y) (* x z))))))

Theorem: equal-*-/-2

(defthm equal-*-/-2
        (implies (and (acl2-numberp x) (not (equal x 0)))
                 (equal (equal (* y (/ x)) z)
                        (and (acl2-numberp z)
                             (equal (fix y) (* z x))))))

Theorem: fold-consts-in-*

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

Theorem: times-zero

(defthm times-zero (equal (* 0 x) 0))