← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/rtl/rel6/support/support/log.lisp

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/rtl/rel6/support/support/log.lisp
 
1
;;;**************************************************************
 
2
;;;An ACL2 Library of Floating Point Arithmetic
 
3
 
 
4
;;;David M. Russinoff
 
5
;;;Advanced Micro Devices, Inc.
 
6
;;;February, 1998
 
7
;;;***************************************************************
 
8
(in-package "ACL2")
 
9
 
 
10
;This book includes theorems mixing the logical operators (logand, etc.) with bits and bitn.
 
11
 
 
12
(include-book "ground-zero")
 
13
 
 
14
(local (include-book "log-proofs"))
 
15
 
 
16
(defund fl (x)
 
17
  (declare (xargs :guard (real/rationalp x)))
 
18
  (floor x 1))
 
19
 
 
20
(defund bits (x i j)
 
21
  (declare (xargs :guard (and (natp x)
 
22
                              (natp i)
 
23
                              (natp j))
 
24
                  :verify-guards nil))
 
25
  (mbe :logic (if (or (not (integerp i))
 
26
                      (not (integerp j)))
 
27
                  0
 
28
                (fl (/ (mod x (expt 2 (1+ i))) (expt 2 j))))
 
29
       :exec  (if (< i j)
 
30
                  0
 
31
                (logand (ash x (- j)) (1- (ash 1 (1+ (- i j))))))))
 
32
 
 
33
(defund bitn (x n)
 
34
  (declare (xargs :guard (and (natp x)
 
35
                              (natp n))
 
36
                  :verify-guards nil))
 
37
  (mbe :logic (bits x n n)
 
38
       :exec  (if (evenp (ash x (- n))) 0 1)))
 
39
 
 
40
(defun natp (x)
 
41
  (declare (xargs :guard t))
 
42
  (and (integerp x)
 
43
       (<= 0 x)))
 
44
 
 
45
(defund bvecp (x k)
 
46
  (declare (xargs :guard (integerp k)))
 
47
  (and (integerp x)
 
48
       (<= 0 x)
 
49
       (< x (expt 2 k))))
 
50
 
 
51
(include-book "lnot")
 
52
(include-book "logand")
 
53
(include-book "logior")
 
54
(include-book "logxor")
 
55
 
 
56
;move!
 
57
;rename! mod-lognot-by-2
 
58
(defthm mod-logior-9
 
59
  (implies (integerp i)
 
60
           (iff (= (mod (lognot i) 2) 0)
 
61
                (not (= (mod i 2) 0)))))
 
62
 
 
63
;move!
 
64
(defthm mod-logior-10
 
65
  (implies (and (integerp i)
 
66
                (integerp j))
 
67
           (iff (and (= (mod i 2) 0) (= (mod j 2) 0))
 
68
                (= (mod (logior i j) 2) 0)))
 
69
  :rule-classes ()
 
70
  :hints (("Goal" :use mod-logior-by-2
 
71
           :in-theory (set-difference-theories
 
72
                       (enable mod-by-2)
 
73
                       '(logior)))))
 
74
 
 
75
;BOZO export!
 
76
;gen?
 
77
(defthm logior-logand
 
78
  (implies (and (integerp x)
 
79
                (<= 0 x)
 
80
                (integerp y)
 
81
                (<= 0 y)
 
82
                (integerp z)
 
83
                (<= 0 z))
 
84
           (equal (logior x (logand y z))
 
85
                  (logand (logior x y) (logior x z))))
 
86
  :rule-classes ())
 
87
 
 
88
;BOZO export!
 
89
(defthm logior-logand-alt
 
90
  (implies (and (integerp x)
 
91
                (<= 0 x)
 
92
                (integerp y)
 
93
                (<= 0 y)
 
94
                (integerp z)
 
95
                (<= 0 z))
 
96
           (equal (logior (logand y z) x)
 
97
                  (logand (logior x y) (logior x z))))
 
98
  :rule-classes ())
 
99
 
 
100
(defthm logand-logior
 
101
  (implies (and (integerp x) (<= 0 x)
 
102
                (integerp y) (<= 0 y)
 
103
                (integerp z) (<= 0 z))
 
104
           (equal (logand x (logior y z))
 
105
                  (logior (logand x y) (logand x z))))
 
106
  :rule-classes ())
 
107
 
 
108
(defthm logand-logior-alt
 
109
  (implies (and (integerp x) (>= x 0)
 
110
                (integerp y) (>= y 0)
 
111
                (integerp z) (>= z 0))
 
112
           (equal (logand (logior y z) x)
 
113
                  (logior (logand y x) (logand z x))))
 
114
  :rule-classes ())
 
115
 
 
116
(defthm mod-logand-aux
 
117
  (implies (and (integerp x) (>= x 0)
 
118
                (integerp y) (>= y 0)
 
119
                (integerp n) (>= n 0))
 
120
           (= (mod (logand x y) (expt 2 n))
 
121
              (logand (mod x (expt 2 n)) y)))
 
122
  :rule-classes ())
 
123
 
 
124
;generalize (mod y (expt 2 n)) to anything < 2^n?
 
125
(defthm and-dist-d
 
126
    (implies (and (integerp x) (>= x 0)
 
127
                  (integerp y) (>= y 0)
 
128
                  (integerp n) (>= n 0)
 
129
                  (< x (expt 2 n)))
 
130
             (= (logand x y)
 
131
                (logand x (mod y (expt 2 n)))))
 
132
  :rule-classes ())
 
133
 
 
134
;compare to mod-logand-aux
 
135
;we can wrap the mod around x or y or both (same for bits of logand?)
 
136
(defthm mod-logand
 
137
  (implies (and (integerp x) (>= x 0)
 
138
                (integerp y) (>= y 0)
 
139
                (integerp n) (>= n 0))
 
140
           (equal (mod (logand x y) (expt 2 n))
 
141
                  (logand (mod x (expt 2 n)) (mod y (expt 2 n))))))
 
142
 
 
143
;prove that we can wrap the bits around either arg in the conclusion or both...
 
144
;will have to shift if we don't wrap bits??
 
145
(defthm bits-logand
 
146
   (implies (and     ;(<= i j)
 
147
             (case-split (natp x)) ;drop?
 
148
             (case-split (natp y)) ;drop?
 
149
             (case-split (natp i))
 
150
             (case-split (natp j))
 
151
             )
 
152
            (equal (bits (logand x y) i j)
 
153
                   (logand (bits x i j) (bits y i j)))))
 
154
 
 
155
(defthm bitn-logand
 
156
  (implies (and (integerp x) ; (>= x 0)
 
157
                (integerp y) ; (>= y 0)
 
158
                (integerp n) (>= n 0)
 
159
                )
 
160
           (equal (bitn (logand x y) n)
 
161
                  (logand (bitn x n) (bitn y n)))))
 
162
 
 
163
(defthm bits-logior
 
164
    (implies (and ;(>= i j)
 
165
                  (case-split (natp x))
 
166
                  (case-split (natp y))
 
167
                  (case-split (natp i))
 
168
                  (case-split (natp j))
 
169
                  )
 
170
             (equal (bits (logior x y) i j)
 
171
                    (logior (bits x i j) (bits y i j)))))
 
172
 
 
173
;someday prove from bits-logior (will have to generalize bits-logior?)?
 
174
(defthm bitn-logior
 
175
    (implies (and (integerp x)
 
176
                  (integerp y)
 
177
                  (integerp n)
 
178
                  (>= n 0))
 
179
             (equal (bitn (logior x y) n)
 
180
                    (logior (bitn x n) (bitn y n)))))
 
181
 
 
182
;give better name, perhaps "logand-with-power2" ?
 
183
(defthm and-bits-a
 
184
    (implies (and (integerp x) (>= x 0)
 
185
                  (integerp k) (>= k 0))
 
186
             (= (logand x (expt 2 k))
 
187
                (* (expt 2 k) (bitn x k))))
 
188
  :rule-classes ())
 
189
 
 
190
(defthm and-bits-b
 
191
  (implies (and (integerp x) (>= x 0)
 
192
                (integerp k) (>= k 0))
 
193
           (= (logior x (expt 2 k))
 
194
              (+ x
 
195
                 (* (expt 2 k) 
 
196
                    (- 1 (bitn x k))))))
 
197
  :rule-classes ())
 
198
 
 
199
(defthm logand-slice
 
200
  (implies (and (integerp x) (>= x 0)
 
201
                (integerp n) (>= n 0)
 
202
                (integerp k) (>= k 0)
 
203
                (< k n))
 
204
           (= (logand x (- (expt 2 n) (expt 2 k)))
 
205
              (* (expt 2 k) (bits x (1- n) k))))
 
206
  :rule-classes ())
 
207
 
 
208
;move to logxor.lisp?
 
209
(defthmd logxor-rewrite
 
210
   (implies (and (< x (expt 2 n))
 
211
                 (< y (expt 2 n))
 
212
                 (integerp n) (>= n 1) ;gen?
 
213
                 (integerp x) (>= x 0)
 
214
                 (integerp y) (>= y 0))
 
215
            (= (logxor x y)
 
216
               (logior (logand x (lnot y n))
 
217
                       (logand y (lnot x n))))))
 
218
 
 
219
;n is a free var
 
220
(defthmd logxor-rewrite-2
 
221
    ;; ! Do we really want to get rid of logxor?
 
222
    (implies (and (bvecp x n)
 
223
                  (bvecp y n)
 
224
                  (natp n)
 
225
                  (not (= n 0)))
 
226
             (equal (logxor x y)
 
227
                    (logior (logand x (lnot y n))
 
228
                            (logand y (lnot x n)))))
 
229
    :rule-classes ((:rewrite :match-free :all)))
 
230
 
 
231
(defthm bitn-logxor
 
232
  (implies (and (case-split (integerp x))
 
233
                (case-split (integerp y))
 
234
                (case-split (integerp n))
 
235
                (case-split (>= n 0))
 
236
                )
 
237
           (equal (bitn (logxor x y) n)
 
238
                  (logxor (bitn x n) (bitn y n)))))
 
239
 
 
240
 
 
241
 
 
242
(defthm bits-logxor
 
243
  (implies (and (case-split (natp x))
 
244
                (case-split (natp y))
 
245
                (case-split (natp i))
 
246
                (case-split (natp j))
 
247
;(>= i j)
 
248
                )
 
249
           (equal (bits (logxor x y) i j)
 
250
                  (logxor (bits x i j) (bits y i j))))
 
251
  :hints (("Goal" :in-theory (set-difference-theories
 
252
                              (enable bvecp natp expt-split)
 
253
                              '())
 
254
           :use ((:instance hack1 (x (+ i x y)))
 
255
                 (:instance bits-logxor-aux (n (+ i x y)))))))
 
256