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
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
|
(in-package "ACL2")
(local (include-book "arithmetic/idiv" :dir :system))
(local (include-book "arithmetic/realp" :dir :system))
(include-book "ln")
; Added by Matt K. for v2-7.
(add-match-free-override :once t)
(set-match-free-default :once)
(defun raise (a x)
(if (= x 0)
1
(if (equal (fix a) 0)
0
(acl2-exp (* x (acl2-ln a))))))
(encapsulate
()
(local
(defthm raise-expt-for-non-negative-exponents
(implies (and (integerp i)
(<= 0 i))
(equal (raise a i)
(expt a i)))))
(local
(defthm raise-expt-for-negative-exponents
(implies (and (integerp i)
(< i 0))
(equal (raise a i)
(expt a i)))
:hints (("Goal"
:use ((:instance raise-expt-for-non-negative-exponents
(i (- i))))
:in-theory (disable raise-expt-for-non-negative-exponents)))))
(defthm raise-expt
(implies (integerp i)
(equal (raise a i)
(expt a i)))
:hints (("Goal"
:cases ((<= 0 i)))))
)
(defthm raise-acl2-exp
(implies (acl2-numberp x)
(equal (raise (acl2-exp 1) x)
(acl2-exp x))))
(defthm power-of-sums
(implies (and (acl2-numberp x)
(acl2-numberp y))
(equal (raise a (+ x y))
(if (equal (+ x y) 0)
1
(* (raise a x) (raise a y))))))
(defthm raise-a---x
(implies (acl2-numberp x)
(equal (raise a (- x))
(/ (raise a x)))))
(defthm raise-sqrt
(implies (and (realp x)
(<= 0 x))
(equal (raise x 1/2) (acl2-sqrt x)))
:hints (("Goal"
:use ((:instance y*y=x->y=sqrt-x
(x x)
(y (raise x 1/2))))
:in-theory (disable y*y=x->y=sqrt-x))
("Subgoal 3"
:use ((:instance acl2-exp->-0-for-reals
(x (* 1/2 (acl2-ln x)))))
:in-theory (disable acl2-exp->-0-for-reals))
("Subgoal 2"
:use ((:instance exp-sum
(x (* 1/2 (acl2-ln x)))
(y (* 1/2 (acl2-ln x)))))
:in-theory (disable exp-sum))))
|
