basic-arithmetic

other

(in-package "ACL2")

local

(local (include-book "basic-arithmetic-helper"))

nonlinearp-default-hint-pass1function

(defun nonlinearp-default-hint-pass1
  (stable-under-simplificationp hist pspv)
  (cond (stable-under-simplificationp (if (access rewrite-constant
          (access prove-spec-var pspv :rewrite-constant)
          :nonlinearp)
        nil
        '(:computed-hint-replacement t :nonlinearp t)))
    ((access rewrite-constant
       (access prove-spec-var pspv :rewrite-constant)
       :nonlinearp) (if (equal (caar hist) 'settled-down-clause)
        nil
        '(:computed-hint-replacement t :nonlinearp nil)))
    (t nil)))

commutativity-2-of-+theorem

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

functional-self-inversion-of-minustheorem

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

distributivity-of-minus-over-+theorem

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

minus-cancellation-on-righttheorem

(defthm minus-cancellation-on-right
  (equal (+ x y (- x)) (fix y)))

minus-cancellation-on-lefttheorem

(defthm minus-cancellation-on-left
  (equal (+ x (- x) y) (fix y)))

right-cancellation-for-+theorem

(defthm right-cancellation-for-+
  (equal (equal (+ x z) (+ y z)) (equal (fix x) (fix y))))

left-cancellation-for-+theorem

(defthm left-cancellation-for-+
  (equal (equal (+ x y) (+ x z)) (equal (fix y) (fix z))))

equal-minus-0theorem

(defthm equal-minus-0
  (equal (equal (- x) 0) (equal (fix x) 0)))

equal-+-x-y-0theorem

(defthm equal-+-x-y-0
  (implies (syntaxp (not (and (consp y) (equal (car y) 'binary-+))))
    (equal (equal (+ x y) 0)
      (and (equal (fix x) (- y)) (equal (- x) (fix y))))))

equal-+-x-y-xtheorem

(defthm equal-+-x-y-x
  (equal (equal (+ x y) x)
    (and (acl2-numberp x) (equal (fix y) 0))))

equal-+-x-y-ytheorem

(defthm equal-+-x-y-y
  (equal (equal (+ x y) y)
    (and (acl2-numberp y) (equal (fix x) 0))))

equal-minus-minustheorem

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

fold-consts-in-+theorem

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

commutativity-2-of-*theorem

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

functional-self-inversion-of-/theorem

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

distributivity-of-/-over-*theorem

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

/-cancellation-on-righttheorem

(defthm /-cancellation-on-right
  (equal (* y x (/ y))
    (if (not (equal (fix y) 0))
      (fix x)
      0)))

/-cancellation-on-lefttheorem

(defthm /-cancellation-on-left
  (equal (* y (/ y) x)
    (if (not (equal (fix y) 0))
      (fix x)
      0)))

right-cancellation-for-*theorem

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

left-cancellation-for-*theorem

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

equal-/-0theorem

(defthm equal-/-0 (equal (equal (/ x) 0) (equal (fix x) 0)))

equal-*-x-y-0theorem

(defthm equal-*-x-y-0
  (equal (equal (* x y) 0)
    (or (equal (fix x) 0) (equal (fix y) 0))))

equal-*-x-y-xtheorem

(defthm equal-*-x-y-x
  (equal (equal (* x y) x)
    (and (acl2-numberp x) (or (equal x 0) (equal y 1))))
  :hints (("Goal" :use ((:instance right-cancellation-for-* (z x) (x y) (y 1))))))

equal-*-y-x-xtheorem

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

equal-/-/theorem

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

fold-consts-in-*theorem

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

equal-/theorem

(defthm equal-/
  (equal (equal (/ x) y)
    (if (not (equal (fix x) 0))
      (equal 1 (* x y))
      (equal y 0))))

numerator-nonzero-forwardtheorem

(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)))))

times-zerotheorem

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

functional-commutativity-of-minus-*-righttheorem

(defthm functional-commutativity-of-minus-*-right
  (implies (syntaxp (not (quotep y)))
    (equal (* x (- y)) (- (* x y)))))

functional-commutativity-of-minus-*-lefttheorem

(defthm functional-commutativity-of-minus-*-left
  (implies (syntaxp (not (quotep x)))
    (equal (* (- x) y) (- (* x y)))))

reciprocal-minus-atheorem

(defthm reciprocal-minus-a (equal (/ (- x)) (- (/ x))))

Included Books