(in-package "ACL2")

(defmacro square (x)
  `(* ,x ,x))

(defun fast-expt (b n)
  (cond
    ((zp n) 1)
    ((evenp n) (square (fast-expt b (/ n 2))))
    (t (* b (fast-expt b (- n 1))))))

(defthm add-halves
  (implies (and (acl2-numberp n)
                (evenp n))
           (equal n (+ (* 1/2 n) (* 1/2 n))))
  :rule-classes nil)

(defthm expt-add-halves
  (implies (and (acl2-numberp n)
                (acl2-numberp b)
                (evenp n))
           (equal (expt b n) (expt b (+ (* 1/2 n) (* 1/2 n)))))
  :hints (("Goal" :do-not-induct t
                  :use (:instance add-halves (n n))))
  :rule-classes nil)

(defthm add-expts
  (implies (and (natp b)
                (natp n)
                (natp m))
           (equal (expt b (+ n m))
                  (* (expt b n)
                     (expt b m)))))

(defthm expt-fast-expt
  (implies (and (natp n)
                (natp b))
           (equal (fast-expt b n)
                  (expt b n)))
   :hints (("Subgoal *1/4'''" :use (:instance expt-add-halves (n n)))))