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
|
(in-package "ACL2")
(defund bvecp (x k)
(declare (xargs :guard (integerp k)))
(and (integerp x)
(<= 0 x)
(< x (expt 2 k))))
(include-book "ground-zero")
#|(defun decode (x n)
(if (< x n) (ash 1 x) 0))
(in-theory (disable decode))
|#
(local ; ACL2 primitive
(defun natp (x)
(declare (xargs :guard t))
(and (integerp x)
(<= 0 x))))
(local (include-book "../arithmetic/fl"))
(local (include-book "ash"))
(local (include-book "bvecp"))
(defund decode (x n)
(declare (xargs :guard (rationalp n)))
(if (and (natp x) (< x n))
(ash 1 x)
0))
(defthm decode-nonnegative-integer-type
(and (integerp (decode x n))
(<= 0 (decode x n)))
:rule-classes (:type-prescription)
:hints (("Goal" :in-theory (enable decode))))
;this rule is no better than decode-nonnegative-integer-type and might be worse:
(in-theory (disable (:type-prescription decode)))
(defthm decode-natp
(natp (decode x n)))
(defthm decode-bvecp
(implies (and (<= n k)
(case-split (integerp k))
)
(bvecp (decode x n) k))
:hints (("Goal" :in-theory (enable decode))))
|
