← 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/land.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/land.lisp
 
1
; Port land0 theorems to land.  The original definition of land (in rel4) was
 
2
; that of land0 in the current release.  So the port is to keep all the lemmas
 
3
; about land0 and then use equality of land0 with land to port them to land.
 
4
 
 
5
(in-package "ACL2")
 
6
 
 
7
(include-book "land0")
 
8
(local (include-book "top1")) ; for land0-bits-1 and land0-bits-2
 
9
 
 
10
(defun binary-land (x y n)
 
11
  (declare (xargs :guard (and (natp x) 
 
12
                              (natp y)
 
13
                              (integerp n)
 
14
                              (< 0 n))
 
15
                  :measure (nfix n)
 
16
                  :verify-guards nil))
 
17
  (mbe :logic
 
18
       (cond ((zp n)
 
19
              0)
 
20
             ((equal n 1)
 
21
              (if (and (equal (bitn x 0) 1)
 
22
                       (equal (bitn y 0) 1))
 
23
                  1
 
24
                0))
 
25
             (t (+ (* 2 (binary-land (fl (/ x 2)) (fl (/ y 2)) (1- n)))
 
26
                   (binary-land (mod x 2) (mod y 2) 1))))
 
27
       :exec ; (land0 x y n)
 
28
       (logand (bits x (1- n) 0)
 
29
               (bits y (1- n) 0))))
 
30
 
 
31
(defmacro land (&rest x)
 
32
  (declare (xargs :guard (and (consp x)
 
33
                              (consp (cdr x))
 
34
                              (consp (cddr x)))))
 
35
  (cond ((endp (cdddr x)) ;(land x y n) -- the base case
 
36
         `(binary-land ,@x))
 
37
        (t         
 
38
         `(binary-land ,(car x)
 
39
                       (land ,@(cdr x))
 
40
                       ,(car (last x))))))
 
41
 
 
42
; We attempt to derive all land results from corresponding land0 results.
 
43
 
 
44
(encapsulate
 
45
 ()
 
46
 
 
47
 (local
 
48
  (defun p0 (x y n)
 
49
    (equal (land x y n)
 
50
           (land0 x y n))))
 
51
 
 
52
 (local
 
53
  (defthm p0-holds-inductive-step
 
54
    (implies (and (not (zp n))
 
55
                  (not (equal n 1))
 
56
                  (p0 (fl (* x 1/2))
 
57
                      (fl (* y 1/2))
 
58
                      (+ -1 n))
 
59
                  (p0 (mod x 2) (mod y 2) 1))
 
60
             (p0 x y n))
 
61
    :hints (("Goal" :use (land0-def binary-land)))))
 
62
 
 
63
 (local
 
64
  (defthm p0-holds-base-1
 
65
    (p0 x y 1)
 
66
    :hints (("Goal" :in-theory (enable bitn)
 
67
             :expand ((binary-land0 x y 1))))))
 
68
 
 
69
 (local
 
70
  (defthm p0-holds-base-0
 
71
    (implies (zp n)
 
72
             (p0 x y n))
 
73
    :hints (("Goal" :expand ((binary-land0 x y n))))))
 
74
 
 
75
 (local
 
76
  (defthm p0-holds
 
77
    (p0 x y n)
 
78
    :hints (("Goal" :induct (land x y n)
 
79
             :in-theory (disable p0)))
 
80
    :rule-classes nil))
 
81
 
 
82
 (defthmd land-is-land0
 
83
   (equal (land x y n)
 
84
          (land0 x y n))
 
85
   :hints (("Goal" :use p0-holds))))
 
86
 
 
87
(local (in-theory (e/d (land-is-land0) (binary-land))))
 
88
 
 
89
;Allows things like (in-theory (disable land)) to refer to binary-land.
 
90
(add-macro-alias land binary-land)
 
91
 
 
92
(defthm land-nonnegative-integer-type
 
93
  (and (integerp (land x y n))
 
94
       (<= 0 (land x y n)))
 
95
  :rule-classes (:type-prescription))
 
96
 
 
97
;(:type-prescription land) is no better than land-nonnegative-integer-type and might be worse:
 
98
(in-theory (disable (:type-prescription binary-land)))
 
99
 
 
100
;drop this if we plan to keep natp enabled?
 
101
(defthm land-natp
 
102
  (natp (land x y n)))
 
103
 
 
104
;BOZO split into 2 rules?
 
105
(defthm land-with-n-not-a-natp
 
106
  (implies (not (natp n))
 
107
           (equal (land x y n)
 
108
                  0)))
 
109
 
 
110
(defthmd land-bvecp-simple
 
111
  (bvecp (land x y n) n)
 
112
  :hints (("Goal" :use land0-bvecp-simple)))
 
113
 
 
114
(defthm land-bvecp
 
115
  (implies (and (<= n k)
 
116
                (case-split (integerp k)))
 
117
           (bvecp (land x y n) k)))
 
118
 
 
119
 
 
120
;;
 
121
;; Rules to normalize land terms (recall that LAND is a macro for BINARY-LAND):
 
122
;;
 
123
 
 
124
;This guarantees that the n parameters to nested LAND calls match.
 
125
;Note the MIN in the conclusion.
 
126
;BOZO do we expect MIN to be enabled?  Maybe we should use IF instead for this and other rules?
 
127
(defthm land-nest-tighten
 
128
  (implies (and (syntaxp (not (equal m n)))
 
129
                (case-split (integerp m))
 
130
                (case-split (integerp n))
 
131
                )
 
132
           (equal (land x (land y z m) n)
 
133
                  (land x (land y z (min m n)) (min m n)))))
 
134
 
 
135
; allow the n's to differ on this?
 
136
(defthm land-associative
 
137
  (equal (land (land x y n) z n)
 
138
         (land x (land y z n) n)))
 
139
 
 
140
(defthm land-commutative
 
141
  (equal (land y x n)
 
142
         (land x y n)))
 
143
 
 
144
; allow the n's to differ on this?
 
145
(defthm land-commutative-2
 
146
  (equal (land y (land x z n) n)
 
147
         (land x (land y z n) n)))
 
148
 
 
149
; allow the n's to differ on this?
 
150
(defthm land-combine-constants
 
151
  (implies (syntaxp (and (quotep x)
 
152
                         (quotep y)
 
153
                         (quotep n)))
 
154
           (equal (land x (land y z n) n)
 
155
                  (land (land x y n) z n))))
 
156
 
 
157
(defthm land-0
 
158
  (equal (land 0 y n)
 
159
         0))
 
160
 
 
161
;nicer than the analogous rule for logand? is it really?
 
162
;BOZO gen the second 1 in the lhs?
 
163
(defthm land-1
 
164
  (equal (land 1 y 1)
 
165
         (bitn y 0)))
 
166
 
 
167
(defthm land-self
 
168
  (equal (land x x n)
 
169
         (bits x (1- n) 0)))
 
170
 
 
171
;perhaps use only the main rule, bits-land?
 
172
(defthmd bits-land-1
 
173
  (implies (and (< i n)
 
174
                (case-split (<= 0 j))
 
175
                (case-split (integerp n))
 
176
                )
 
177
           (equal (bits (land x y n) i j)
 
178
                  (land (bits x i j) 
 
179
                        (bits y i j) 
 
180
                        (+ 1 i (- j)))))
 
181
  :hints (("Goal" :use bits-land0-1)))
 
182
 
 
183
;perhaps use only the main rule, bits-land?
 
184
(defthmd bits-land-2
 
185
  (implies (and (<= n i)
 
186
                (case-split (<= 0 j))
 
187
                (case-split (integerp n))
 
188
                )
 
189
           (equal (bits (land x y n) i j)
 
190
                  (land (bits x i j) 
 
191
                        (bits y i j) 
 
192
                        (+ n (- j)))))
 
193
  :hints (("Goal" :use bits-land0-2)))
 
194
 
 
195
;Notice the call to MIN in the conclusion.
 
196
(defthm bits-land
 
197
  (implies (and (case-split (<= 0 j))
 
198
                (case-split (integerp n))
 
199
                (case-split (integerp i))
 
200
                )
 
201
           (equal (bits (land x y n) i j)
 
202
                  (land (bits x i j) 
 
203
                        (bits y i j) 
 
204
                        (+ (min n (+ 1 i)) (- j))))))
 
205
 
 
206
(defthmd bitn-land-1
 
207
  (implies (and (< m n)
 
208
                (case-split (<= 0 m))
 
209
                (case-split (integerp n))
 
210
                )
 
211
           (equal (bitn (land x y n) m)
 
212
                  (land (bitn x m) 
 
213
                        (bitn y m) 
 
214
                        1))))
 
215
(defthmd bitn-land-2
 
216
  (implies (and (<= n m)
 
217
                (case-split (<= 0 m))
 
218
                (case-split (integerp n))
 
219
                )
 
220
           (equal (bitn (land x y n) m)
 
221
                  0)))
 
222
 
 
223
;notice the IF in the conclusion
 
224
;we expect this to cause case splits only rarely, since m and n will usually be constants
 
225
(defthm bitn-land
 
226
  (implies (and (case-split (<= 0 k))
 
227
                (case-split (integerp n))
 
228
                )
 
229
           (equal (bitn (land x y n) k)
 
230
                  (if (< k n)
 
231
                      (land (bitn x k)
 
232
                            (bitn y k) 
 
233
                            1)
 
234
                    0))))
 
235
 
 
236
;BOZO see land-equal-0
 
237
;drop bvecp hyps and put bitn in conclusion?
 
238
(defthm land-of-single-bits-equal-0
 
239
  (implies (and (case-split (bvecp x 1))
 
240
                (case-split (bvecp y 1))
 
241
                )
 
242
           (equal (equal 0 (land x y 1))
 
243
                  (or (equal x 0)
 
244
                      (equal y 0)))))
 
245
 
 
246
(defthm land-of-single-bits-equal-1
 
247
  (implies (and (case-split (bvecp x 1))
 
248
                (case-split (bvecp y 1))
 
249
                )
 
250
           (equal (equal 1 (land x y 1))
 
251
                  (and (equal x 1)
 
252
                       (equal y 1)))))
 
253
 
 
254
(defthm land-ones
 
255
  (equal (land (1- (expt 2 n)) x n)
 
256
         (bits x (1- n) 0))
 
257
  :hints (("Goal" :use land0-ones))
 
258
  :rule-classes ())
 
259
 
 
260
;land-with-all-ones will rewrite (land x n) [note there's only one value being ANDed], because (land x n)
 
261
;expands to (BINARY-LAND X (ALL-ONES N) N) - now moot???
 
262
;BOZO drop bvecp hyp and move to conclusion?
 
263
(defthm land-with-all-ones
 
264
  (implies (case-split (bvecp x n))
 
265
           (equal (land (all-ones n) x n)
 
266
                  x)))
 
267
 
 
268
(defthmd land-ones-rewrite
 
269
  (implies (and (syntaxp (and (quotep k) (quotep n)))
 
270
                (equal k (1- (expt 2 n))) ;this computes on constants...
 
271
                )
 
272
           (equal (land k x n)
 
273
                  (bits x (1- n) 0)))
 
274
  :hints (("Goal" :use land0-ones-rewrite)))
 
275
 
 
276
(defthm land-def-original
 
277
  (implies (and (integerp x)
 
278
                (integerp y)
 
279
                (> n 0)
 
280
                (integerp n)
 
281
                )
 
282
           (equal (land x y n)
 
283
                  (+ (* 2 (land (fl (/ x 2)) (fl (/ y 2)) (1- n)))
 
284
                     (land (mod x 2) (mod y 2) 1))))
 
285
  :hints (("Goal" :use land0-def))
 
286
  :rule-classes ())
 
287
 
 
288
(defthmd land-mod-2
 
289
  (implies (and (natp x)
 
290
                (natp y)
 
291
                (natp n)
 
292
                (> n 0))
 
293
           (equal (mod (land x y n) 2)
 
294
                  (land (mod x 2) (mod y 2) 1)))
 
295
  :hints (("Goal" :use land0-mod-2)))
 
296
 
 
297
;BOZO RHS isn't simplified...
 
298
(defthmd land-fl-2
 
299
  (implies (and (natp x)
 
300
                (natp y)
 
301
                (natp n)
 
302
                (> n 0))
 
303
           (equal (fl (/ (land x y n) 2))
 
304
                  (land (fl (/ x 2)) (fl (/ y 2)) (1- n))))
 
305
  :hints (("Goal" :use land0-fl-2)))
 
306
 
 
307
;BOZO rename to land-with-n-0
 
308
;what if n is negative? or not an integer?
 
309
(defthm land-x-y-0
 
310
  (equal (land x y 0) 0))
 
311
 
 
312
;actually, maybe only either x or y must be a bvecp of length n
 
313
;n is a free var
 
314
(defthm land-reduce
 
315
    (implies (and (bvecp x n)
 
316
                  (bvecp y n)
 
317
                  (natp n)
 
318
                  (natp m)
 
319
                  (< n m))
 
320
             (equal (land x y m)
 
321
                    (land x y n))))
 
322
 
 
323
;deceptive name; this only works for single bits!
 
324
(defthm land-equal-0
 
325
  (implies (and (bvecp i 1)
 
326
                (bvecp j 1))
 
327
           (equal (equal 0 (land i j 1))
 
328
                  (or (equal i 0)
 
329
                      (equal j 0)))))
 
330
 
 
331
;make alt version?
 
332
(defthm land-bnd
 
333
  (implies (case-split (<= 0 x))
 
334
           (<= (land x y n) x))
 
335
  :rule-classes (:rewrite :linear))
 
336
 
 
337
;enable? make an alt version??
 
338
(defthmd land-ignores-bits
 
339
  (equal (land (bits x (1- n) 0) y n)
 
340
         (land x y n))
 
341
  :hints (("Goal" :use land0-ignores-bits)))
 
342
 
 
343
(defthmd land-with-shifted-arg
 
344
  (implies (and (integerp x) ;gen?
 
345
                (rationalp y)
 
346
                (integerp m)
 
347
                (integerp n)
 
348
                (<= 0 m)
 
349
                )
 
350
           (equal (land (* (expt 2 m) x) y n)
 
351
                  (* (expt 2 m) (land x (bits y (1- n) m) (+ n (- m))))))
 
352
  :hints (("Goal" :use land0-with-shifted-arg)))
 
353
 
 
354
(defthm land-shift
 
355
  (implies (and (integerp x)
 
356
                (integerp y)
 
357
                (natp k))
 
358
           (= (land (* (expt 2 k) x)
 
359
                    (* (expt 2 k) y)
 
360
                    n)
 
361
              (* (expt 2 k) (land x y (- n k)))))
 
362
  :hints (("Goal" :use land0-shift))
 
363
  :rule-classes nil)
 
364
 
 
365
(defthmd land-expt
 
366
  (implies (and (natp n)
 
367
                (natp k)
 
368
                (< k n))
 
369
           (equal (land x (expt 2 k) n)
 
370
                  (* (expt 2 k) (bitn x k))))
 
371
  :hints (("Goal" :use land0-expt)))
 
372
 
 
373
(defthm land-slice
 
374
  (implies (and (<= j i) ;drop? or not?
 
375
                (<= i n)
 
376
                (integerp n)
 
377
                (integerp i)
 
378
                (integerp j)
 
379
                (<= 0 j)
 
380
                )
 
381
           (equal (land x (- (expt 2 i) (expt 2 j)) n)
 
382
                  (* (expt 2 j) (bits x (1- i) j))))
 
383
  :hints (("Goal" :use land0-slice))
 
384
  :rule-classes ())
 
385
 
 
386
(defthmd land-slices
 
387
  (implies (and (natp n)
 
388
                (natp l)
 
389
                (natp k)
 
390
                (<= l k)
 
391
                (< k n))
 
392
           (equal (land (- (expt 2 n) (1+ (expt 2 l)))
 
393
                        (- (expt 2 n) (expt 2 k))
 
394
                        n)
 
395
                  (if (= l k)
 
396
                      (- (expt 2 n) (expt 2 (1+ k)))
 
397
                    (- (expt 2 n) (expt 2 k)))))
 
398
  :hints (("Goal" :use land0-slices)))
 
399
 
 
400
(defthm land-upper-bound
 
401
  (implies (and (integerp n)
 
402
                (<= 0 n))
 
403
           (< (land x y n) (expt 2 n)))
 
404
  :rule-classes (:rewrite :linear))
 
405
 
 
406
(defthm land-upper-bound-tight
 
407
  (implies (and (integerp n)
 
408
                (<= 0 n))
 
409
           (<= (land x y n) (1- (expt 2 n)))))
 
410
 
 
411
(defthm land-fl-1
 
412
  (equal (land (fl x) y n)
 
413
         (land x y n)))
 
414
 
 
415
(defthm land-fl-2-eric ;BOZO name conflicted...
 
416
  (equal (land x (fl y) n)
 
417
         (land x y n)))
 
418
 
 
419
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
420
; Added in move to rel5 (should perhaps be in a -proofs file):
 
421
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
422
 
 
423
(defthm land-bvecp-2
 
424
  (implies (and (bvecp x m)
 
425
                (bvecp y m))
 
426
           (bvecp (land x y n) m))
 
427
  :hints (("Goal" :in-theory (enable bvecp))))
 
428
 
 
429
; Start proof of fl-land.
 
430
 
 
431
(local
 
432
 (defun fl-land-induction (k n)
 
433
   (if (zp k)
 
434
       n
 
435
     (fl-land-induction (1- k) (1+ n)))))
 
436
 
 
437
 
 
438
(local
 
439
 (defthmd fl-land-induction-step-1
 
440
   (implies (not (zp k))
 
441
            (equal (land (fl (* x (/ (expt 2 k))))
 
442
                         (fl (* y (/ (expt 2 k))))
 
443
                         n)
 
444
                   (land (fl (/ (fl (* x (/ (expt 2 (1- k))))) 2))
 
445
                         (fl (/ (fl (* y (/ (expt 2 (1- k))))) 2))
 
446
                         n)))
 
447
   :hints (("Goal" :in-theory (disable land-fl-1
 
448
                                       land-fl-2-eric
 
449
                                       land-is-land0
 
450
                                       fl/int-rewrite)
 
451
            :expand ((expt 2 k))
 
452
            :use ((:instance fl/int-rewrite
 
453
                             (x (* x (/ (expt 2 (1- k)))))
 
454
                             (n 2))
 
455
                  (:instance fl/int-rewrite
 
456
                             (x (* y (/ (expt 2 (1- k)))))
 
457
                             (n 2)))))))
 
458
 
 
459
(local
 
460
 (defthmd fl-land-induction-step-2
 
461
   (equal (land (fl (/ (fl (* x (/ (expt 2 (1- k))))) 2))
 
462
                (fl (/ (fl (* y (/ (expt 2 (1- k))))) 2))
 
463
                n)
 
464
          (fl (/ (land (fl (* x (/ (expt 2 (1- k)))))
 
465
                       (fl (* y (/ (expt 2 (1- k)))))
 
466
                       (1+ n))
 
467
                 2)))
 
468
   :hints (("Goal" :in-theory (disable land-fl-1
 
469
                                       land-fl-2-eric
 
470
                                       land-is-land0
 
471
                                       fl/int-rewrite)
 
472
            :expand ((land (fl (* x (/ (expt 2 (1- k)))))
 
473
                           (fl (* y (/ (expt 2 (1- k)))))
 
474
                           (1+ n)))))))
 
475
 
 
476
(local
 
477
 (defthmd fl-land-induction-step-3
 
478
   (implies (and (not (zp k))
 
479
                 (equal (fl (* (/ (expt 2 (+ -1 k)))
 
480
                               (land x y (+ k n))))
 
481
                        (land (fl (* x (/ (expt 2 (+ -1 k)))))
 
482
                              (fl (* y (/ (expt 2 (+ -1 k)))))
 
483
                              (+ 1 n)))
 
484
                 (natp x)
 
485
                 (natp y)
 
486
                 (natp n))
 
487
            (equal (fl (/ (land (fl (* x (/ (expt 2 (1- k)))))
 
488
                                (fl (* y (/ (expt 2 (1- k)))))
 
489
                                (1+ n))
 
490
                          2))
 
491
                   (fl (/ (fl (* (/ (expt 2 (+ -1 k)))
 
492
                                 (land x y (+ k n))))
 
493
                          2))))))
 
494
 
 
495
(local
 
496
 (defthmd fl-land-induction-step-4
 
497
   (implies (and (not (zp k))
 
498
                 (equal (fl (* (/ (expt 2 (+ -1 k)))
 
499
                               (land x y (+ k n))))
 
500
                        (land (fl (* x (/ (expt 2 (+ -1 k)))))
 
501
                              (fl (* y (/ (expt 2 (+ -1 k)))))
 
502
                              (+ 1 n)))
 
503
                 (natp x)
 
504
                 (natp y)
 
505
                 (natp n))
 
506
            (equal (fl (/ (fl (* (/ (expt 2 (+ -1 k)))
 
507
                                 (land x y (+ k n))))
 
508
                          2))
 
509
                   (fl (* (/ (expt 2 k))
 
510
                          (land x y (+ k n))))))
 
511
   :hints (("Goal" :expand ((expt 2 k))))))
 
512
 
 
513
(local
 
514
 (defthm fl-land-induction-step
 
515
   (implies (and (not (zp k))
 
516
                 (equal (fl (* (/ (expt 2 (+ -1 k)))
 
517
                               (land x y (+ k n))))
 
518
                        (land (fl (* x (/ (expt 2 (+ -1 k)))))
 
519
                              (fl (* y (/ (expt 2 (+ -1 k)))))
 
520
                              (+ 1 n)))
 
521
                 (natp x)
 
522
                 (natp y)
 
523
                 (natp n))
 
524
            (equal (fl (* (/ (expt 2 k))
 
525
                          (land x y (+ k n))))
 
526
                   (land (fl (* x (/ (expt 2 k))))
 
527
                         (fl (* y (/ (expt 2 k))))
 
528
                         n)))
 
529
   :hints (("Goal" :use (fl-land-induction-step-1
 
530
                         fl-land-induction-step-2
 
531
                         fl-land-induction-step-3
 
532
                         fl-land-induction-step-4)))))
 
533
 
 
534
(defthmd fl-land
 
535
  (implies (and (natp x)
 
536
                (natp y)
 
537
                (natp n)
 
538
                (natp k))
 
539
           (equal (fl (/ (land x y (+ n k)) (expt 2 k)))
 
540
                  (land (fl (/ x (expt 2 k))) (fl (/ y (expt 2 k))) n)))
 
541
  :hints (("Goal" :induct (fl-land-induction k n)
 
542
           :in-theory (disable land-is-land0 land-fl-1 land-fl-2-eric))))
 
543
 
 
544
 
 
545
(defthmd land-def
 
546
  (implies (and (integerp x)
 
547
                (integerp y)
 
548
                (integerp n)
 
549
                (> n 0))
 
550
           (equal (land x y n)
 
551
                  (+ (* 2 (land (fl (/ x 2)) (fl (/ y 2)) (1- n)))
 
552
                     (land (bitn x 0) (bitn y 0) 1))))
 
553
  :hints (("Goal" :in-theory (enable bitn-rec-0)
 
554
           :use land-def-original)))
 
555
 
 
556
; Proof of mod-land as derived from bits-land:
 
557
 
 
558
; (land x y k)))
 
559
; = {by land-bvecp and bits-tail}
 
560
; (bits (land x y k) (1- k) 0)
 
561
; = {by (:instance bits-land (x x) (y y) (n k) (i (1- k)) (j 0))}
 
562
; (land (bits x (1- k) 0) (bits y (1- k) 0) k)
 
563
; = {by (:instance bits-land (x x) (y y) (n n) (i (1- k)) (j 0))}
 
564
; (bits (land x y n) (1- k) 0)
 
565
; = {by hypothesis}
 
566
; (bits (land x y n) (min (1- n) (1- k)) 0)
 
567
; = {by (:instance mod-bits (x (land x y n)) (i (1- n)) (j k))}
 
568
; (mod (bits (land x y n) (1- n) 0) (expt 2 k))
 
569
; = {by land-bvecp}
 
570
; (mod (land x y n) (expt 2 k))
 
571
 
 
572
(defthmd mod-land
 
573
  (implies (and (integerp n)
 
574
                (integerp k)
 
575
                (<= k n))
 
576
           (equal (mod (land x y n) (expt 2 k))
 
577
                  (land x y k)))
 
578
  :hints (("Goal"
 
579
           :use
 
580
           ((:instance bits-land (x x) (y y) (n k) (i (1- k)) (j 0))
 
581
            (:instance mod-bits (x (land x y n)) (i (1- n)) (j k))))))
 
582
 
 
583
(defthmd land-bits-1
 
584
  (equal (land (bits x (1- n) 0)
 
585
               y
 
586
               n)
 
587
         (land x y n))
 
588
  :hints (("Goal" :use land0-bits-1)))
 
589
 
 
590
(defthmd land-bits-2
 
591
  (equal (land x
 
592
               (bits y (1- n) 0)
 
593
               n)
 
594
         (land x y n))
 
595
  :hints (("Goal" :use land0-bits-2)))
 
596
 
 
597
(defthm land-base
 
598
  (equal (land x y 1)
 
599
         (if (and (equal (bitn x 0) 1)
 
600
                  (equal (bitn y 0) 1))
 
601
             1
 
602
           0))
 
603
  :hints (("Goal" :use land0-base))
 
604
  :rule-classes nil)