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
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
|
(in-package "ACL2")
(local ; ACL2 primitive
(defun natp (x)
(declare (xargs :guard t))
(and (integerp x)
(<= 0 x))))
(defund bvecp (x k)
(declare (xargs :guard (integerp k)))
(and (integerp x)
(<= 0 x)
(< x (expt 2 k))))
(defund fl (x)
(declare (xargs :guard (real/rationalp x)))
(floor x 1))
(local (include-book "../arithmetic/top"))
(defun expo-measure (x)
; (declare (xargs :guard (and (real/rationalp x) (not (equal x 0)))))
(cond ((not (rationalp x)) 0)
((< x 0) '(2 . 0))
((< x 1) (cons 1 (fl (/ x))))
(t (fl x))))
(defund expo (x)
(declare (xargs :guard t
:measure (expo-measure x)))
(cond ((or (not (rationalp x)) (equal x 0)) 0)
((< x 0) (expo (- x)))
((< x 1) (1- (expo (* 2 x))))
((< x 2) 0)
(t (1+ (expo (/ x 2))))))
(local (include-book "ground-zero"))
(local (include-book "bvecp"))
(local (include-book "ash"))
(local (include-book "float"))
(defund encode (x n)
(declare (xargs :guard (and (acl2-numberp x)
(integerp n)
(<= 0 n))))
(if (zp n)
0
(if (= x (ash 1 n))
n
(encode x (1- n)))))
(defthm encode-nonnegative-integer-type
(and (integerp (encode x n))
(<= 0 (encode x n)))
:rule-classes (:type-prescription)
:hints (("Goal" :in-theory (enable encode))))
;this rule is no better than encode-nonnegative-integer-type and might be worse:
(in-theory (disable (:type-prescription encode)))
(defthm encode-natp
(natp (encode x n)))
(defthm encode-bvecp-helper
(implies (and (case-split (integerp n))
(case-split (<= 0 n))
)
(bvecp (encode x n) (+ 1 (expo n)))) ;The +1 is necessary
:hints (("Subgoal *1/5" :use (:instance EXPT-WEAK-MONOTONE
(n (+ 1 (EXPO (1- N))))
(m (+ 1 (EXPO N))))
:in-theory (set-difference-theories
(enable encode bvecp power2p ash-rewrite)
'(
expt-compare
)))
("Goal"
:in-theory (set-difference-theories
(enable encode bvecp power2p ash-rewrite)
'(
expt-compare
)))
))
(defthm encode-bvecp-old
(implies (and (<= (+ 1 (expo n)) k)
(case-split (integerp k))
)
(BVECP (ENCODE x n) k))
:hints (("Goal" :in-theory (disable encode-bvecp-helper)
:expand (ENCODE X N)
:use (encode-bvecp-helper))))
(defthmd expo-expt-reduction
(implies (and (integerp k)
(rationalp n)
(< 0 n)
(< n (expt 2 k)))
(<= (+ 1 (expo n)) k))
:hints (("Goal" :use ((:instance expo-comparison-rewrite-to-bound-2
(k (1- k))
(x n)))
:in-theory (disable expo-comparison-rewrite-to-bound-2))))
(local
(defthmd encode-non-positive-integer
(implies (not (and (integerp n)
(< 0 n)))
(equal (encode x n) 0))
:hints (("Goal" :expand ((encode x n))))))
(defthm encode-bvecp
(implies (and (< n (expt 2 k))
(case-split (integerp k)))
(bvecp (encode x n) k))
:hints (("Goal" :in-theory (enable expo-expt-reduction encode-non-positive-integer)
:cases ((and (integerp n) (< 0 n))))))
; may not need this now
(defthm encode-reduce-n
(implies (and (integerp n)
(<= 0 n)
(bvecp x n))
(equal (encode x n)
(encode x (1- n))))
:hints (("Goal" :in-theory (set-difference-theories
(enable encode bvecp power2p ash-rewrite )
'(
expt-compare
)))))
|
