expt-helper - ACL2 Book

Included Books

basic-arithmetic inequalities prefer-times

other

(in-package "ACL2")

local

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

local

(local (include-book "inequalities"))

local

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

fcmacro

(defmacro fc (x) x)

expt-crocktheorem

(defthm expt-crock
  (equal (expt x 1) (fix x))
  :hints (("Goal" :expand (expt x 1))))

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

(encapsulate nil
  (local (defun math-induction-start-at-k
      (k n)
      (declare (xargs :measure (if (and (integerp k) (integerp n) (< k n))
            (- n k)
            0)))
      (if (and (integerp k) (integerp n) (< k n))
        (math-induction-start-at-k k (+ -1 n))
        t)))
  (local (defthm justify-induction
      (implies (and (integerp i) (< 1 r) (real/rationalp r))
        (< (expt r i) (expt r (+ 1 i))))
      :hints (("Goal" :in-theory (enable prefer-*-to-/)))))
  (defthm expt-is-increasing-for-base>1
    (implies (and (< 1 r)
        (< i j)
        (real/rationalp r)
        (integerp i)
        (integerp j))
      (< (expt r i) (expt r j)))
    :rule-classes (:rewrite :linear)
    :hints (("Goal" :do-not '(generalize)
       :induct (math-induction-start-at-k i j)
       :in-theory (enable prefer-*-to-/)) ("Subgoal *1/1" :use (:instance justify-induction (i (+ -1 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))))
  :hints (("Goal" :expand (expt r (+ i j)))))

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)))))
  :hints (("Goal" :do-not '(generalize))))