expt

other

(in-package "ACL2")

local

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

local

(local (include-book "inequalities"))

local

(local (include-book "prefer-times"))

local

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

fcmacro

(defmacro fc (x) x)

expt-type-prescription-rationalptheorem

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

expt-type-prescription-positive-1theorem

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

expt-type-prescription-positive-2theorem

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

expt-type-prescription-nonzerotheorem

(defthm expt-type-prescription-nonzero
  (implies (and (fc (acl2-numberp r)) (not (equal r 0)))
    (not (equal 0 (expt r i))))
  :rule-classes (:type-prescription :generalize))

expt-type-prescription-integerptheorem

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

equal-expt-0theorem

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

expt-0theorem

(defthm expt-0
  (and (equal (expt x 0) 1)
    (equal (expt 0 i)
      (if (zip i)
        1
        0))))

expt-1theorem

(defthm expt-1
  (and (equal (expt x 1) (fix x)) (equal (expt 1 i) 1)))

local

(local (defthm expt-minus (equal (expt r (- i)) (/ (expt r i)))))

local

(local (defthm expt-minus-redux
    (equal (expt r (* -1 i)) (/ (expt r i)))
    :hints (("Goal" :use ((:theorem (equal (* -1 i) (- i))))))))

exponents-add-1theorem

(defthm exponents-add-1
  (implies (and (fc (integerp i)) (fc (integerp j)))
    (equal (expt r (+ i j))
      (if (equal (+ i j) 0)
        1
        (* (expt r i) (expt r j))))))

exponents-add-for-nonpos-exponentstheorem

(defthm exponents-add-for-nonpos-exponents
  (implies (and (<= i 0) (<= j 0) (fc (integerp i)) (fc (integerp j)))
    (equal (expt r (+ i j)) (* (expt r i) (expt r j)))))

exponents-add-for-nonneg-exponentstheorem

(defthm exponents-add-for-nonneg-exponents
  (implies (and (<= 0 i) (<= 0 j) (fc (integerp i)) (fc (integerp j)))
    (equal (expt r (+ i j)) (* (expt r i) (expt r j)))))

exponents-add-2theorem

(defthm exponents-add-2
  (implies (and (not (equal 0 r))
      (fc (acl2-numberp r))
      (fc (integerp i))
      (fc (integerp j)))
    (equal (expt r (+ i j)) (* (expt r i) (expt r j)))))

distributivity-of-expt-over-*theorem

(defthm distributivity-of-expt-over-*
  (equal (expt (* a b) i) (* (expt a i) (expt b i))))

functional-commutativity-of-expt-/-basetheorem

(defthm functional-commutativity-of-expt-/-base
  (equal (expt (/ r) i) (/ (expt r i))))

exponents-multiplytheorem

(defthm exponents-multiply
  (implies (and (fc (integerp i)) (fc (integerp j)))
    (equal (expt (expt r i) j) (expt r (* i j))))
  :hints (("Subgoal *1/4'" :in-theory (enable prefer-*-to-/))))

expt-is-increasing-for-base>1theorem

(defthm expt-is-increasing-for-base>1
  (implies (and (< 1 r)
      (< i j)
      (fc (rationalp r))
      (fc (integerp i))
      (fc (integerp j)))
    (< (expt r i) (expt r j)))
  :rule-classes (:rewrite :linear))

expt-is-decreasing-for-pos-base<1theorem

(defthm expt-is-decreasing-for-pos-base<1
  (implies (and (< 0 r)
      (< r 1)
      (< i j)
      (fc (rationalp r))
      (fc (integerp i))
      (fc (integerp j)))
    (< (expt r j) (expt r i)))
  :rule-classes (:rewrite :linear)
  :hints (("Goal" :use ((:instance expt-is-increasing-for-base>1 (r (/ r))))
     :in-theory (enable prefer-*-to-/))))

expt-is-weakly-increasing-for-base>1theorem

(defthm expt-is-weakly-increasing-for-base>1
  (implies (and (<= 1 r)
      (<= i j)
      (fc (rationalp r))
      (fc (integerp i))
      (fc (integerp j)))
    (<= (expt r i) (expt r j)))
  :rule-classes (:rewrite :linear)
  :hints (("Goal" :use expt-is-increasing-for-base>1
     :in-theory (disable expt-is-increasing-for-base>1))))

expt-is-weakly-decreasing-for-pos-base<1theorem

(defthm expt-is-weakly-decreasing-for-pos-base<1
  (implies (and (< 0 r)
      (<= r 1)
      (<= i j)
      (fc (rationalp r))
      (fc (integerp i))
      (fc (integerp j)))
    (<= (expt r j) (expt r i)))
  :rule-classes (:rewrite :linear)
  :hints (("Goal" :use expt-is-decreasing-for-pos-base<1
     :in-theory (disable expt-is-decreasing-for-pos-base<1))))

local

(local (defthm stupid-hack
    (implies (and (rationalp x) (not (equal x 0)))
      (equal (* x (/ x) (expt a b)) (expt a b)))))

local

(local (in-arithmetic-theory '((:rewrite commutativity-of-*) (:rewrite commutativity-2-of-*)
      (:rewrite stupid-hack)
      (:rewrite expt-1)
      (:rewrite expt-0))))

expt->-1-1theorem

(defthm expt->-1-1
  (implies (and (< 1 r) (< 0 i) (fc (rationalp r)) (fc (integerp i)))
    (< 1 (expt r i)))
  :rule-classes :linear)

expt->-1-2theorem

(defthm expt->-1-2
  (implies (and (< 0 r)
      (< r 1)
      (< i 0)
      (fc (rationalp r))
      (fc (integerp i)))
    (< 1 (expt r i)))
  :rule-classes :linear)

expt-<-1-1theorem

(defthm expt-<-1-1
  (implies (and (< 0 r)
      (< r 1)
      (< 0 i)
      (fc (rationalp r))
      (fc (integerp i)))
    (< (expt r i) 1))
  :rule-classes :linear)

expt-<-1-2theorem

(defthm expt-<-1-2
  (implies (and (< 1 r) (< i 0) (fc (rationalp r)) (fc (integerp i)))
    (< (expt r i) 1))
  :hints (("Goal" :in-theory (enable prefer-*-to-/)))
  :rule-classes :linear)

Included Books