blob: d3fb779d75e2c3c7183e6e4bae302d11cefa0fff (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
(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)))))
|
