diff options
| -rw-r--r-- | fast-expt.lisp | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/fast-expt.lisp b/fast-expt.lisp new file mode 100644 index 0000000..3318946 --- /dev/null +++ b/fast-expt.lisp @@ -0,0 +1,38 @@ +(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))))) |