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
|
;;;***************************************************************
;;;An ACL2 Library of Floating Point Arithmetic
;;;David M. Russinoff
;;;Advanced Micro Devices, Inc.
;;;February, 1998
;;;***************************************************************
(in-package "ACL2")
(local (include-book "trunc"))
(include-book "log")
(include-book "float")
(include-book "trunc")
(local (include-book "bits"))
(local (include-book "../arithmetic/top"))
(local (in-theory (enable expt-minus)))
(defthm bits-trunc-2
(implies (and (= n (1+ (expo x)))
;(rationalp x) ;(integerp x)
(>= x 0)
;(integerp n)
; (>= n k)
(integerp k)
(> k 0)
)
(= (trunc x k)
(* (expt 2 (- n k))
(bits x (1- n) (- n k)))))
:rule-classes ()
:hints (("goal" :in-theory (enable bits trunc-rewrite expt-split))))
(local
(defthm bits-trunc-3
(implies (and (integerp x)
(> x 0)
(integerp n) (> n k)
(integerp k) (> k 0)
(= (expo x) (1- n)))
(= (trunc x k)
(logand x (- (expt 2 n) (expt 2 (- n k))))))
:rule-classes ()
:hints (("goal" :use ((:instance bits-trunc-2)
(:instance logand-slice (k (- n k)))))
)))
(local
(defthm bits-trunc-4
(implies (and (integerp x) (> x 0)
(integerp n) (> n k)
(integerp k) (> k 0)
(>= x (expt 2 (1- n)))
(< x (expt 2 n)))
(= (trunc x k)
(logand x (- (expt 2 n) (expt 2 (- n k))))))
:rule-classes ()
:hints (("goal" :use ((:instance bits-trunc-3)
(:instance expo-unique (n (1- n))))))))
(local
(defthm bits-trunc-5
(implies (and (integerp x) (> x 0)
(integerp m) (>= m n)
(integerp n) (> n k)
(integerp k) (> k 0)
(>= x (expt 2 (1- n)))
(< x (expt 2 n)))
(= (trunc x k)
(logand x (mod (- (expt 2 m) (expt 2 (- n k))) (expt 2 n)))))
:rule-classes ()
:hints (("goal" :use ((:instance bits-trunc-4)
;(:instance mod-2m-2n-k)
)))))
(include-book "land")
(include-book "merge")
(defthm bits-trunc
(implies (and (>= x (expt 2 (1- n)))
(< x (expt 2 n))
(integerp x) (> x 0)
(integerp m) (>= m n)
(integerp n) (> n k)
(integerp k) (> k 0)
)
(= (trunc x k)
(land x (- (expt 2 m) (expt 2 (- n k))) n)))
:rule-classes ()
:hints (("goal" :in-theory (e/d (bits-tail land expt-split) (expt-minus))
:use ((:instance bits-trunc-5)))))
#|
(defthm bits-trunc-6
(implies (and (integerp x) (> x 0)
(integerp m) (>= m n)
(integerp n) (> n k)
(integerp k) (> k 0)
(>= x (expt 2 (1- n)))
(< x (expt 2 n)))
(= (trunc x k)
(logand x (- (expt 2 m) (expt 2 (- n k))))))
:rule-classes ()
:hints (("goal" :use (;(:instance hack-82)
(:instance bits-trunc-5)
(:instance expt-weak-monotone (n (- n k)))
(:instance and-dist-d (y (- (expt 2 m) (expt 2 (- n k)))))))))
|#
|
