From f292ea0c9594e4c2bd3581cef8b7989a8391d9b3 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Sat, 4 Sep 2021 01:16:29 +0900 Subject: fast-expt: Add fast-expt.lisp file. --- fast-expt.lisp | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 fast-expt.lisp (limited to 'fast-expt.lisp') 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))))) -- cgit v1.2.3