expt

other

(in-package "ACL2")

local

(local (include-book "../pass1/top"))

local

(local (include-book "expt-helper"))

expt-type-prescription-rationaltheorem

(defthm expt-type-prescription-rational
  (implies (rationalp x) (rationalp (expt x i)))
  :rule-classes (:type-prescription :generalize))

expt-type-prescription-integertheorem

(defthm expt-type-prescription-integer
  (implies (and (<= 0 i) (integerp x)) (integerp (expt x i)))
  :rule-classes (:type-prescription :generalize))

expt-type-prescription-non-zerotheorem

(defthm expt-type-prescription-non-zero
  (implies (and (acl2-numberp x) (not (equal x 0)))
    (not (equal (expt x i) 0)))
  :rule-classes (:type-prescription :generalize))

expt-type-prescription-positivetheorem

(defthm expt-type-prescription-positive
  (implies (and (< 0 r) (real/rationalp r)) (< 0 (expt r i)))
  :rule-classes (:type-prescription :generalize))

expt-type-prescription-nonnegativetheorem

(defthm expt-type-prescription-nonnegative
  (implies (and (<= 0 x) (real/rationalp x))
    (<= 0 (expt x i)))
  :rule-classes (:type-prescription :generalize))

|(equal (expt x i) 0)|theorem

(defthm |(equal (expt x i) 0)|
  (equal (equal (expt x i) 0)
    (and (equal (fix x) 0) (not (equal (ifix i) 0)))))

|(expt x 0)|theorem

(defthm |(expt x 0)| (equal (expt x 0) 1))

|(expt 0 i)|theorem

(defthm |(expt 0 i)|
  (equal (expt 0 i)
    (if (zip i)
      1
      0)))

|(expt x 1)|theorem

(defthm |(expt x 1)| (equal (expt x 1) (fix x)))

|(expt 1 i)|theorem

(defthm |(expt 1 i)| (equal (expt 1 i) 1))

|(expt x -1)|theorem

(defthm |(expt x -1)| (equal (expt x -1) (/ x)))

case-split-on-non-integer-exponentstheorem

(defthm case-split-on-non-integer-exponents
  (implies (case-split (not (integerp n)))
    (equal (expt x n) 1)))

|(expt (+ x y) 2)|theorem

(defthm |(expt (+ x y) 2)|
  (equal (expt (+ x y) 2) (+ (expt x 2) (* 2 x y) (expt y 2)))
  :hints (("Goal" :expand (expt (+ x y) 2))))

|(expt (+ x y) 3)|theorem

(defthm |(expt (+ x y) 3)|
  (equal (expt (+ x y) 3)
    (+ (expt x 3)
      (* 3 (expt x 2) y)
      (* 3 x (expt y 2))
      (expt y 3)))
  :hints (("Goal" :expand ((expt (+ x y) 3) (expt (+ x y) 2)))))

|(/ (expt x i))|theorem

(defthm |(/ (expt x i))|
  (equal (/ (expt x i)) (expt (/ x) i)))

local

(local (in-theory (disable functional-commutativity-of-expt-/-base)))

|(expt x (- i))|theorem

(defthm |(expt x (- i))|
  (equal (expt x (- i)) (expt (/ x) i)))

|(expt (/ x) (* c i))|theorem

(defthm |(expt (/ x) (* c i))|
  (implies (syntaxp (quotep c))
    (equal (expt (/ x) (* c i)) (expt x (* (- c) i)))))

|(expt (* x y) i)|theorem

(defthm |(expt (* x y) i)|
  (equal (expt (* x y) i) (* (expt x i) (expt y i))))

|(expt (expt x i) j)|theorem

(defthm |(expt (expt x i) j)|
  (implies (and (integerp i) (integerp j))
    (equal (expt (expt x i) j) (expt x (* i j)))))

|(expt x (+ i j))|theorem

(defthm |(expt x (+ i j))|
  (implies (and (integerp i) (integerp j))
    (equal (expt x (+ i j))
      (if (equal (+ i j) 0)
        1
        (* (expt x i) (expt x j))))))

|(expt x (+ i j)) with non-negative exponents|theorem

(defthm |(expt x (+ i j)) with non-negative exponents|
  (implies (and (<= 0 i) (<= 0 j) (integerp i) (integerp j))
    (equal (expt x (+ i j)) (* (expt x i) (expt x j)))))

|(expt x (+ i j)) with non-positive exponents|theorem

(defthm |(expt x (+ i j)) with non-positive exponents|
  (implies (and (<= i 0) (<= j 0) (integerp i) (integerp j))
    (equal (expt x (+ i j)) (* (expt x i) (expt x j)))))

|(expt x (+ i j)) with non-zero base|theorem

(defthm |(expt x (+ i j)) with non-zero base|
  (implies (and (not (equal 0 x))
      (acl2-numberp x)
      (integerp i)
      (integerp j))
    (equal (expt x (+ i j)) (* (expt x i) (expt x j)))))

expt-expt-linear-atheorem

(defthm expt-expt-linear-a
  (implies (and (< 1 x)
      (< i j)
      (real/rationalp x)
      (integerp i)
      (integerp j))
    (< (expt x i) (expt x j)))
  :rule-classes (:rewrite :linear))

expt-expt-linear-btheorem

(defthm expt-expt-linear-b
  (implies (and (< 0 x)
      (< x 1)
      (< i j)
      (real/rationalp x)
      (integerp i)
      (integerp j))
    (< (expt x j) (expt x i)))
  :rule-classes (:rewrite :linear))

expt-expt-linear-ctheorem

(defthm expt-expt-linear-c
  (implies (and (<= 1 x)
      (<= i j)
      (real/rationalp x)
      (integerp i)
      (integerp j))
    (<= (expt x i) (expt x j)))
  :rule-classes (:rewrite :linear))

expt-expt-linear-dtheorem

(defthm expt-expt-linear-d
  (implies (and (< 0 x)
      (<= x 1)
      (<= i j)
      (real/rationalp x)
      (integerp i)
      (integerp j))
    (<= (expt x j) (expt x i)))
  :rule-classes (:rewrite :linear))

expt-x-linear-atheorem

(defthm expt-x-linear-a
  (implies (and (real/rationalp x) (< 1 x) (integerp c) (< 1 c))
    (< x (expt x c)))
  :rule-classes (:rewrite :linear))

expt-x-linear-btheorem

(defthm expt-x-linear-b
  (implies (and (real/rationalp x)
      (< x 1)
      (< 0 x)
      (integerp c)
      (< 1 c))
    (< (expt x c) x))
  :rule-classes (:rewrite :linear))

expt-x-linear-ctheorem

(defthm expt-x-linear-c
  (implies (and (real/rationalp x) (<= 1 x) (integerp c) (<= 1 c))
    (<= x (expt x c)))
  :rule-classes (:rewrite :linear))

expt-x-linear-dtheorem

(defthm expt-x-linear-d
  (implies (and (real/rationalp x)
      (<= x 1)
      (<= 0 x)
      (integerp c)
      (<= 1 c))
    (<= (expt x c) x))
  :rule-classes (:rewrite :linear))

expt-x-linear-etheorem

(defthm expt-x-linear-e
  (implies (and (real/rationalp x) (< 1 x) (integerp c) (<= c 0))
    (< (expt x c) x))
  :rule-classes (:rewrite :linear))

expt-x-linear-ftheorem

(defthm expt-x-linear-f
  (implies (and (real/rationalp x)
      (< x 1)
      (< 0 x)
      (integerp c)
      (<= c 0))
    (< x (expt x c)))
  :rule-classes (:rewrite :linear))

expt-x-linear-gtheorem

(defthm expt-x-linear-g
  (implies (and (real/rationalp x) (<= 1 x) (integerp c) (<= c 0))
    (<= (expt x c) x))
  :rule-classes (:rewrite :linear))

expt-x-linear-htheorem

(defthm expt-x-linear-h
  (implies (and (real/rationalp x)
      (<= x 1)
      (<= 0 x)
      (integerp c)
      (<= c 0))
    (<= x (expt x c)))
  :rule-classes (:rewrite :linear))

expt-1-linear-atheorem

(defthm expt-1-linear-a
  (implies (and (< 1 x) (< 0 i) (real/rationalp x) (integerp i))
    (< 1 (expt x i)))
  :rule-classes :linear)

expt-1-linear-btheorem

(defthm expt-1-linear-b
  (implies (and (<= 0 x)
      (< x 1)
      (< 0 i)
      (real/rationalp x)
      (integerp i))
    (< (expt x i) 1))
  :rule-classes :linear)

expt-1-linear-ctheorem

(defthm expt-1-linear-c
  (implies (and (<= 1 x) (<= 0 i) (real/rationalp x) (integerp i))
    (<= 1 (expt x i)))
  :rule-classes :linear)

expt-1-linear-dtheorem

(defthm expt-1-linear-d
  (implies (and (<= 0 x)
      (<= x 1)
      (<= 0 i)
      (real/rationalp x)
      (integerp i))
    (<= (expt x i) 1))
  :rule-classes :linear)

expt-1-linear-etheorem

(defthm expt-1-linear-e
  (implies (and (< 1 x) (< i 0) (real/rationalp x) (integerp i))
    (< (expt x i) 1))
  :rule-classes :linear)

expt-1-linear-ftheorem

(defthm expt-1-linear-f
  (implies (and (< 0 x)
      (< x 1)
      (< i 0)
      (real/rationalp x)
      (integerp i))
    (< 1 (expt x i)))
  :rule-classes :linear)

expt-1-linear-gtheorem

(defthm expt-1-linear-g
  (implies (and (<= 1 x) (<= i 0) (real/rationalp x) (integerp i))
    (<= (expt x i) 1))
  :rule-classes :linear)

expt-1-linear-htheorem

(defthm expt-1-linear-h
  (implies (and (< 0 x)
      (<= x 1)
      (< i 0)
      (real/rationalp x)
      (integerp i))
    (<= 1 (expt x i)))
  :rule-classes :linear)

expt-type-negative-base-even-exponenttheorem

(defthm expt-type-negative-base-even-exponent
  (implies (and (< x 0)
      (real/rationalp x)
      (integerp i)
      (integerp (* 1/2 i)))
    (< 0 (expt x i)))
  :rule-classes (:type-prescription :generalize))

expt-type-negative-base-odd-exponenttheorem

(defthm expt-type-negative-base-odd-exponent
  (implies (and (< x 0)
      (real/rationalp x)
      (integerp i)
      (not (integerp (* 1/2 i))))
    (< (expt x i) 0))
  :rule-classes (:type-prescription :generalize))

expt-type-nonpositive-base-even-exponenttheorem

(defthm expt-type-nonpositive-base-even-exponent
  (implies (and (<= x 0)
      (real/rationalp x)
      (integerp i)
      (integerp (* 1/2 i)))
    (<= 0 (expt x i)))
  :rule-classes (:type-prescription :generalize)
  :hints (("Goal" :use ((:instance expt-type-negative-base-even-exponent)))))

expt-type-nonpositive-base-odd-exponenttheorem

(defthm expt-type-nonpositive-base-odd-exponent
  (implies (and (<= x 0)
      (real/rationalp x)
      (integerp i)
      (not (integerp (* 1/2 i))))
    (<= (expt x i) 0))
  :rule-classes (:type-prescription :generalize)
  :hints (("Goal" :use ((:instance expt-type-negative-base-odd-exponent)))))

expt-negative-base-even-exponentstheorem

(defthm expt-negative-base-even-exponents
  (implies (and (real/rationalp x) (integerp i) (integerp (* 1/2 i)))
    (equal (expt (- x) i) (expt x i)))
  :hints (("Goal" :use ((:instance expt-negative-base-even-exponent (r x))))))

expt-negative-base-odd-exponentstheorem

(defthm expt-negative-base-odd-exponents
  (implies (and (real/rationalp x)
      (integerp i)
      (not (integerp (* 1/2 i))))
    (equal (expt (- x) i) (- (expt x i))))
  :hints (("Goal" :use ((:instance expt-negative-base-odd-exponent (r x))))))

other

(deftheory strong-expt-rules
  `(expt-type-negative-base-even-exponent expt-type-negative-base-odd-exponent
    expt-type-nonpositive-base-even-exponent
    expt-type-nonpositive-base-odd-exponent
    expt-negative-base-even-exponents
    expt-negative-base-odd-exponents))

in-theory

(in-theory (disable strong-expt-rules))

Included Books