Included Books
other
(in-package "ACL2")
local
(local (include-book "basic-arithmetic"))
local
(local (include-book "expt"))
arith-associativity-of-*theorem
(defthm arith-associativity-of-* (equal (* (* x y) z) (* x (* y z))))
arith-commutativity-of-*theorem
(defthm arith-commutativity-of-* (equal (* x y) (* y x)))
arith-commutativity-2-of-*theorem
(defthm arith-commutativity-2-of-* (equal (* x y z) (* y x z)))
arith-unicity-of-1theorem
(defthm arith-unicity-of-1 (and (equal (* 1 x) (fix x)) (equal (* x 1) (fix x))))
arith-times-zerotheorem
(defthm arith-times-zero (and (equal (* 0 x) 0) (equal (* x 0) 0)))
arith-inverse-of-*-1theorem
(defthm arith-inverse-of-*-1 (implies (and (rationalp x) (not (equal x 0))) (equal (* x (/ x)) 1)))
arith-inverse-of-*-2theorem
(defthm arith-inverse-of-*-2 (implies (and (rationalp x) (not (equal x 0))) (equal (* x (/ x) y) (fix y))))
arith-inverse-of-*-3theorem
(defthm arith-inverse-of-*-3 (implies (and (rationalp x) (not (equal x 0))) (equal (* x y (/ x)) (fix y))))
arith-functional-self-inversion-of-/theorem
(defthm arith-functional-self-inversion-of-/ (equal (/ (/ x)) (fix x)))
arith-distributivity-of-/-over-*theorem
(defthm arith-distributivity-of-/-over-* (equal (/ (* x y)) (* (/ x) (/ y))))
arith-functional-commutativity-of-minus-*-righttheorem
(defthm arith-functional-commutativity-of-minus-*-right (equal (* x (- y)) (- (* x y))))
arith-functional-commutativity-of-minus-*-lefttheorem
(defthm arith-functional-commutativity-of-minus-*-left (equal (* (- x) y) (- (* x y))))
arith-distributivity-1theorem
(defthm arith-distributivity-1 (equal (* x (+ y z)) (+ (* x y) (* x z))))
arith-distributivity-2theorem
(defthm arith-distributivity-2 (equal (* (+ y z) x) (+ (* x y) (* x z))))
arith-fold-consts-in-*theorem
(defthm arith-fold-consts-in-* (implies (and (syntaxp (quotep c)) (syntaxp (quotep d))) (equal (* c d x) (* (* c d) x))))
arith-expt-0theorem
(defthm arith-expt-0 (and (equal (expt x 0) 1) (equal (expt 0 i) (if (zip i) 1 0))))
arith-expt-1theorem
(defthm arith-expt-1 (and (equal (expt x 1) (fix x)) (equal (expt 1 i) 1)))
arith-expt-minus-1theorem
(defthm arith-expt-minus-1 (equal (expt x -1) (/ x)))
arith-functional-commutativity-of-expt-/theorem
(defthm arith-functional-commutativity-of-expt-/ (equal (/ (expt r i)) (expt (/ r) i)))
local
(local (in-theory (disable functional-commutativity-of-expt-/-base)))
arith-expt-minus-exponenttheorem
(defthm arith-expt-minus-exponent (equal (expt r (- i)) (expt (/ r) i)))
arith-expt-negative-constant-exponenttheorem
(defthm arith-expt-negative-constant-exponent (implies (syntaxp (quotep i)) (equal (expt (/ r) (* i j)) (expt r (* (- i) j)))))
arith-exponents-multiplytheorem
(defthm arith-exponents-multiply (implies (and (integerp i) (integerp j)) (equal (expt (expt r i) j) (expt r (* i j)))))
arith-distributivity-of-expt-over-*theorem
(defthm arith-distributivity-of-expt-over-* (equal (expt (* a b) i) (* (expt a i) (expt b i))))
arith-fix-revealedtheorem
(defthm arith-fix-revealed (implies (acl2-numberp x) (equal (fix x) x)))
arith-rational-implies2theorem
(defthm arith-rational-implies2 (implies (rationalp x) (equal (* (numerator x) (/ (denominator x))) x)))
arith-exponents-add-1theorem
(defthm arith-exponents-add-1 (implies (and (integerp i) (integerp j) (not (equal (+ i j) 0))) (equal (expt r (+ i j)) (* (expt r i) (expt r j)))))
arith-exponents-add-for-nonpos-exponentsatheorem
(defthm arith-exponents-add-for-nonpos-exponentsa (implies (and (<= i 0) (<= j 0) (integerp i) (integerp j)) (equal (expt r (+ i j)) (* (expt r i) (expt r j)))))
arith-exponents-add-for-nonneg-exponentsatheorem
(defthm arith-exponents-add-for-nonneg-exponentsa (implies (and (<= 0 i) (<= 0 j) (integerp i) (integerp j)) (equal (expt r (+ i j)) (* (expt r i) (expt r j)))))
arith-exponents-add-2theorem
(defthm arith-exponents-add-2 (implies (and (not (equal 0 r)) (acl2-numberp r) (integerp i) (integerp j)) (equal (expt r (+ i j)) (* (expt r i) (expt r j)))))
in-theory
(in-theory (disable arith-associativity-of-* arith-commutativity-of-* arith-commutativity-2-of-* arith-unicity-of-1 arith-times-zero arith-inverse-of-*-1 arith-inverse-of-*-2 arith-inverse-of-*-3 arith-functional-self-inversion-of-/ arith-distributivity-of-/-over-* arith-functional-commutativity-of-minus-*-right arith-functional-commutativity-of-minus-*-left arith-reciprocal-minusa arith-distributivity-1 arith-distributivity-2 arith-fold-consts-in-* arith-expt-0 arith-expt-1 arith-expt-minus-1 arith-functional-commutativity-of-expt-/ arith-expt-minus-exponent arith-expt-negative-constant-exponent arith-exponents-multiply arith-distributivity-of-expt-over-* arith-fix-revealed arith-rational-implies2 arith-exponents-add-1 arith-exponents-add-for-nonpos-exponentsa arith-exponents-add-for-nonneg-exponentsa arith-exponents-add-2))
other
(in-arithmetic-theory '((:rewrite arith-associativity-of-*) (:rewrite arith-commutativity-of-*) (:rewrite arith-commutativity-2-of-*) (:rewrite arith-unicity-of-1) (:rewrite arith-times-zero) (:rewrite arith-inverse-of-*-1) (:rewrite arith-inverse-of-*-2) (:rewrite arith-inverse-of-*-3) (:rewrite arith-functional-self-inversion-of-/) (:rewrite arith-distributivity-of-/-over-*) (:rewrite arith-functional-commutativity-of-minus-*-right) (:rewrite arith-functional-commutativity-of-minus-*-left) (:rewrite arith-reciprocal-minusa) (:rewrite arith-distributivity-1) (:rewrite arith-distributivity-2) (:rewrite arith-fold-consts-in-*) (:rewrite arith-expt-0) (:rewrite arith-expt-1) (:rewrite arith-expt-minus-1) (:rewrite arith-functional-commutativity-of-expt-/) (:rewrite arith-expt-minus-exponent) (:rewrite arith-expt-negative-constant-exponent) (:rewrite arith-exponents-multiply) (:rewrite arith-distributivity-of-expt-over-*) (:rewrite arith-fix-revealed) (:rewrite arith-rational-implies2) (:rewrite arith-exponents-add-1) (:rewrite arith-exponents-add-for-nonpos-exponentsa) (:rewrite arith-exponents-add-for-nonneg-exponentsa) (:rewrite arith-exponents-add-2)))