← 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/cat.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/cat.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
;; Necessary defuns
 
4
 
 
5
(defund bvecp (x k)
 
6
  (declare (xargs :guard (integerp k)))
 
7
  (and (integerp x)
 
8
       (<= 0 x)
 
9
       (< x (expt 2 k))))
 
10
 
 
11
(defun natp (x)
 
12
  (declare (xargs :guard t))
 
13
  (and (integerp x)
 
14
       (<= 0 x)))
 
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
(defund all-ones (n)
 
41
  (declare (xargs :guard (and (integerp n) (<= 0 n))))
 
42
  (if (zp n)
 
43
      0 ;degenerate case
 
44
    (1- (expt 2 n))))
 
45
 
 
46
(include-book "cat-def")
 
47
 
 
48
; "Definition" used in the library for the purpose of documentation.
 
49
(defthm cat-def
 
50
  (implies (and (natp m) (natp n))
 
51
           (equal (cat x m y n)
 
52
                  (+ (* (expt 2 n) (bits x (1- m) 0))
 
53
                     (bits y (1- n) 0))))
 
54
  :hints (("Goal" :in-theory (enable cat)))
 
55
  :rule-classes nil)
 
56
 
 
57
(local (include-book "cat-proofs"))
 
58
 
 
59
#|
 
60
Concatenate the M-bit value X onto the N-bit value Y.  X will occupy the high bits of the result.
 
61
 
 
62
(cat x m y n) is well-defined only when the following predicate is true:
 
63
 
 
64
(and (natp m)
 
65
     (bvecp x m)
 
66
     (natp n)
 
67
     (bvecp y n))
 
68
 
 
69
|#
 
70
 
 
71
;; New stuff
 
72
 
 
73
(defthm cat-nonnegative-integer-type
 
74
  (and (integerp (cat x m y n))
 
75
       (<= 0 (cat x m y n)))
 
76
  :rule-classes (:type-prescription)
 
77
  )
 
78
 
 
79
;this rule is no better than cat-nonnegative-integer-type and might be worse:
 
80
(in-theory (disable (:type-prescription binary-cat)))
 
81
 
 
82
;just a rewrite rule
 
83
(defthm cat-natp
 
84
  (natp (cat x m y n)))
 
85
 
 
86
;bozo disable? drop bvecp hyp and wrap bits around conclusion??
 
87
(defthm cat-0
 
88
  (implies (and (case-split (bvecp y n))
 
89
                (case-split (integerp n))
 
90
                (case-split (integerp m))
 
91
                (case-split (<= 0 m))
 
92
                )                 
 
93
           (equal (cat 0 m y n) y)))
 
94
 
 
95
;BOZO just use this one??
 
96
(defthm cat-0-alt
 
97
  (implies (and ;(case-split (bvecp y n))
 
98
                (case-split (integerp n))
 
99
                (case-split (integerp m))
 
100
                (case-split (<= 0 m))
 
101
                )                 
 
102
           (equal (cat 0 m y n) (bits y (1- n) 0))))
 
103
 
 
104
;We can rely on bits-tail to complete the simplification down to x if desired.
 
105
(defthm cat-with-n-0
 
106
  (equal (binary-cat x m y 0)
 
107
         (bits x (1- m) 0)))
 
108
 
 
109
;bozo disable?
 
110
(defthm cat-with-n-0-alt
 
111
  (implies (case-split (bvecp x m))
 
112
           (equal (cat x m y 0)
 
113
                  x)))
 
114
 
 
115
;We can rely on bits-tail to complete the simplification down to y if desired.
 
116
(defthm cat-with-m-0
 
117
  (equal (binary-cat x 0 y n)
 
118
         (bits y (1- n) 0)))
 
119
 
 
120
;bozo disable?
 
121
(defthm cat-with-m-0-alt
 
122
  (implies (case-split (bvecp y n))
 
123
           (equal (cat x 0 y n)
 
124
                  y)))
 
125
 
 
126
;change this behavior?? no, it makes for a nice setbits bvecp lemma
 
127
(defthm cat-with-n-not-a-natural
 
128
  (implies (or (not (integerp n))
 
129
               (< n 0))
 
130
           (equal (cat x m y n)
 
131
                  0)))
 
132
 
 
133
(defthm cat-with-m-not-a-natural
 
134
  (implies (or (not (integerp m))
 
135
               (< m 0))
 
136
           (equal (cat x m y n)
 
137
                  0)))
 
138
 
 
139
(defthm cat-bvecp-simple
 
140
  (bvecp (cat x m y n) (+ m n)))
 
141
 
 
142
(defthm cat-bvecp
 
143
  (implies (and (<= (+ m n) k)
 
144
                (case-split (integerp k)))
 
145
           (bvecp (cat x m y n) k)))
 
146
 
 
147
(defthm cat-associative
 
148
  (implies (and (case-split (<= (+ m n) p)) ;gen?
 
149
                (case-split (<= 0 m))
 
150
                (case-split (<= 0 n))
 
151
                (case-split (<= 0 q))
 
152
                (case-split (integerp m))
 
153
                (case-split (integerp n))
 
154
                (case-split (integerp p))
 
155
                (case-split (integerp q))
 
156
                )
 
157
           (equal (cat (cat x m y n) p z q)
 
158
                  (cat x m (cat y n z q) (+ n q)))))
 
159
 
 
160
;prove from something more general (cat-equal-split??)
 
161
;BOZO move hyps to conclusion?
 
162
(defthm cat-equal-0
 
163
  (implies (and (case-split (bvecp x m))
 
164
                (case-split (bvecp y n))
 
165
                (case-split (natp n))
 
166
                (case-split (natp m))
 
167
                )
 
168
           (equal (equal (cat x m y n) 0)
 
169
                  (and (equal x 0)
 
170
                       (equal y 0)))))
 
171
 
 
172
(defthm cat-combine-constants
 
173
  (implies (and (syntaxp (and (quotep x)
 
174
                              (quotep m)
 
175
                              (quotep y)
 
176
                              (quotep n)))
 
177
                (equal (+ n p) r)
 
178
                (case-split (<= 0 m))
 
179
                (case-split (<= 0 n))
 
180
                (case-split (<= 0 p))
 
181
                (case-split (integerp m))
 
182
                (case-split (integerp n))
 
183
                (case-split (integerp p))
 
184
                )
 
185
           (equal (cat x m (cat y n z p) r)
 
186
                  (cat (cat x m y n) (+ m n) z p))))
 
187
 
 
188
;allows r to be > n+p
 
189
;perhaps we only want this one, not cat-combine-constants ??
 
190
(defthm cat-combine-constants-gen
 
191
  (implies (and (syntaxp (and (quotep x)
 
192
                              (quotep m)
 
193
                              (quotep y)
 
194
                              (quotep r)
 
195
                              (quotep p)))
 
196
                (case-split (<= (+ n p) r)) ;other case?
 
197
                (case-split (bvecp y n)) ;BOZO instead put bits in the conclusion?
 
198
                (case-split (<= 0 m))
 
199
                (case-split (<= 0 n))
 
200
                (case-split (<= 0 p))
 
201
                (case-split (integerp m))
 
202
                (case-split (integerp n))
 
203
                (case-split (integerp p))
 
204
                (case-split (integerp r))
 
205
                )
 
206
           (equal (cat x m (cat y n z p) r)
 
207
                  (cat (cat x m y (+ r (- p))) (+ m r (- p)) z p))))
 
208
 
 
209
(defthm cat-constant-equal-constant-hack
 
210
  (implies (and (syntaxp (and (quotep k1) (quotep k2)))
 
211
                (case-split (bvecp x n))
 
212
                (case-split (bvecp k1 m))
 
213
                (case-split (rationalp k2))
 
214
                (case-split (natp n))
 
215
                (case-split (natp m))
 
216
                )
 
217
           (equal (equal (cat k1 m x n) k2)
 
218
                  (equal x (- k2 (* (expt 2 n) k1))))))
 
219
 
 
220
(defthm cat-upper-bound
 
221
  (< (cat x m y n)
 
222
     (expt 2 (+ m n)))
 
223
  :rule-classes (:rewrite :linear))
 
224
 
 
225
;perhaps the :linear rule cat-upper-bound is enough, but this may help stupid hyps be rewritten away
 
226
(defthm cat-compare-to-constant-1
 
227
  (implies (and (syntaxp (quotep k))
 
228
                (<= (expt 2 (+ m n)) k))
 
229
           (< (cat x m y n) k)))
 
230
 
 
231
;provides a tighter bound
 
232
(defthm cat-upper-bound-tight
 
233
  (implies (and (case-split (<= 0 m))
 
234
                (case-split (<= 0 n))
 
235
                (case-split (integerp m))
 
236
                (case-split (integerp n))
 
237
                )
 
238
           (<= (cat x m y n)
 
239
               (1- (expt 2 (+ n m))))))
 
240
 
 
241
 
 
242
(defthm cat-compare-to-constant-2
 
243
  (implies (and (syntaxp (quotep k))
 
244
                (<= (1- (expt 2 (+ m n))) k)
 
245
                (case-split (<= 0 m))
 
246
                (case-split (<= 0 n))
 
247
                (case-split (integerp m))
 
248
                (case-split (integerp n))
 
249
                )
 
250
           (not (< k (cat x m y n)))))
 
251
 
 
252
;BOZO consider adding?
 
253
;problem if we case-split something that turns out to be false?
 
254
(defthm bits-with-i-not-an-integer-2
 
255
  (implies (case-split (not (integerp i)))
 
256
           (equal (bits x i j)
 
257
                  0)))
 
258
 
 
259
(defthm bits-with-j-not-an-integer-2
 
260
  (implies (case-split (not (integerp j)))
 
261
           (equal (bits x i j)
 
262
                  0)))
 
263
 
 
264
;also case-split that i>=j in any call to bits?
 
265
 
 
266
 
 
267
;loops with bits-<-1
 
268
;BOZO add theory invariant!
 
269
;BOZO ask matt about parity..
 
270
(defthmd bits-equal-0-to-bound
 
271
  (equal (equal 0 (bits x i j))
 
272
         (< (bits x i j) 1)))
 
273
 
 
274
;we had a special case where j was 0, but I think this is better (it's certainly more general):
 
275
;better name?
 
276
;think about whether this can be proved without opening bits (including bits-plus-bits??)
 
277
;prove bvecp-bits from this??
 
278
;the regular bits-bvecp should fire first...
 
279
(defthm bits-slice-zero-gen
 
280
  (implies (and (case-split (<= 0 k))
 
281
                (case-split (integerp k))
 
282
                (case-split (integerp j))
 
283
                )
 
284
           (equal (bvecp (bits x i j) k)
 
285
                  (equal 0 (bits x i (+ k j))))))
 
286
 
 
287
;move!
 
288
;this can help, especially when we aren't multiplying through by inverted factors
 
289
(defthm bits-upper-bound-new
 
290
  (< (* (/ (expt 2 i)) (bits x (1- i) 0)) 1)
 
291
  :rule-classes (:rewrite :linear)
 
292
   )
 
293
 
 
294
 (defthmd cat-bvecp-rewrite
 
295
   (implies (and (case-split (<= 0 k))
 
296
                 (case-split (<= 0 n))
 
297
                 (case-split (<= 0 m))
 
298
                 (case-split (integerp n)) 
 
299
                 (case-split (integerp m)) 
 
300
                 (case-split (integerp k)) 
 
301
                 )
 
302
            (equal (bvecp (cat x m y n) k)
 
303
                   (if (<= (+ m n) k)
 
304
                       t
 
305
                     (if (<= n k)
 
306
                         (equal 0 (bits x (1- m) (+ k (* -1 n))))                      
 
307
                       (and (equal 0 (bits x (1- m) 0))
 
308
                            (equal 0 (bits y (1- n) k))))))))
 
309
 
 
310
(defthm cat-bvecp-rewrite-constants
 
311
  (implies (and (syntaxp (and (quotep k) (quotep m) (quotep n)))
 
312
                (case-split (<= 0 k))
 
313
                (case-split (<= 0 n))
 
314
                (case-split (<= 0 m))
 
315
                (case-split (integerp n)) 
 
316
                (case-split (integerp m)) 
 
317
                (case-split (integerp k)) 
 
318
                )
 
319
           (equal (bvecp (cat x m y n) k)
 
320
                  (if (<= (+ m n) k)
 
321
                      t
 
322
                    (if (<= n k)
 
323
                        (equal 0 (bits x (1- m) (+ k (* -1 n))))                      
 
324
                      (and (equal 0 (bits x (1- m) 0))
 
325
                           (equal 0 (bits y (1- n) k))))))))
 
326
 
 
327
;k is a free variable.
 
328
;There is no real analogue of this for y (that is, we can't change n to something smaller).
 
329
(defthm cat-tighten-x
 
330
  (implies (and (bvecp x k) ;k becomes bound here
 
331
                (< k m) ;if k=m, this rule can loop
 
332
                (case-split (<= 0 k))
 
333
                (case-split (integerp k))
 
334
                (case-split (integerp m))
 
335
                )
 
336
           (equal (cat x m y n)
 
337
                  (cat x k y n))))
 
338
 
 
339
(defthm cat-equal-y
 
340
  (implies (and (bvecp y (+ m n))
 
341
                (case-split (integerp m))
 
342
                (case-split (<= 0 m))
 
343
                (case-split (integerp n))
 
344
                (case-split (<= 0 n)))
 
345
           (equal (equal y (binary-cat x m y n))
 
346
                  (equal (bits y (+ -1 m n) n)
 
347
                         (bits x (1- m) 0)))))
 
348
 
 
349
(defthm cat-equal-y-alt
 
350
  (implies (and (case-split (integerp m))
 
351
                (case-split (<= 0 m))
 
352
                (case-split (integerp n))
 
353
                (case-split (<= 0 n)))
 
354
           (equal (equal y (binary-cat x m y n))
 
355
                  (if (bvecp y (+ m n))
 
356
                      (equal (bits y (+ -1 m n) n)
 
357
                             (bits x (1- m) 0))
 
358
                    nil))))
 
359
 
 
360
(defthm cat-equal-bits-of-y
 
361
  (implies (and; (case-split (bvecp y n))
 
362
;                (case-split (bvecp x m))
 
363
                (case-split (integerp m))
 
364
                (case-split (<= 0 m))
 
365
                (case-split (integerp n))
 
366
                (case-split (<= 0 n)))
 
367
           (equal (equal (bits y (1- n) 0) (binary-cat x m y n))
 
368
                  (equal (bits x (1- m) 0) 0))))
 
369
 
 
370
;requires y to be a bvecp of length n
 
371
;drop this one?
 
372
(defthm cat-equal-y-special
 
373
  (implies (and (case-split (bvecp y n))
 
374
                (case-split (integerp m))
 
375
                (case-split (<= 0 m)) ;gen!
 
376
                (case-split (integerp n))
 
377
                (case-split (<= 0 n)))
 
378
           (equal (equal y (binary-cat x m y n))
 
379
                  (equal 0 (bits x (1- m) 0)))))
 
380
 
 
381
;enable?
 
382
;make into 2 separate lemmas (can drop the bits from x or from y)
 
383
(defthmd cat-ignores-bits
 
384
  (equal (cat (bits x (1- m) 0)
 
385
              m (bits y (1- n) 0)
 
386
              n)
 
387
         (cat x m y n)))
 
388
 
 
389
(defthmd bits-cat-1
 
390
  (implies (and (< i n)
 
391
                (case-split (<= 0 j))
 
392
                (case-split (integerp n))
 
393
                (case-split (integerp m))
 
394
                (case-split (<= 0 m))
 
395
                )
 
396
           (equal (bits (cat x m y n) i j)
 
397
                  (bits y i j))))
 
398
 
 
399
(defthmd bits-cat-2-1
 
400
  (implies (and (<= n j) ;case 2
 
401
                (< i (+ m n))  ;case 2-1
 
402
                (case-split (natp n))
 
403
                (case-split (integerp i))
 
404
                (case-split (integerp j))
 
405
                (case-split (natp m))
 
406
                )
 
407
           (equal (bits (cat x m y n) i j)
 
408
                  (bits x (- i n) (- j n)))))
 
409
 
 
410
(defthmd bits-cat-2-2
 
411
  (implies (and (<= n j)  ;case 2
 
412
                (<= (+ m n) i)  ;case 2-1
 
413
                (case-split (natp n))
 
414
                (case-split (integerp i))
 
415
                (case-split (integerp j))
 
416
                (case-split (natp m))
 
417
                )
 
418
           (equal (bits (cat x m y n) i j)
 
419
                  (bits x (+ m -1) (- j n)))))
 
420
 
 
421
;note the IF in the conclusion
 
422
(defthmd bits-cat-2
 
423
  (implies (and (<= n j)  ;case 2
 
424
                (case-split (natp n))
 
425
                (case-split (integerp i))
 
426
                (case-split (integerp j))
 
427
                (case-split (natp m))
 
428
                )
 
429
           (equal (bits (cat x m y n) i j)
 
430
                  (bits x (if (< i (+ m n))
 
431
                              (- i n)
 
432
                            (1- m))
 
433
                        (- j n)))))
 
434
 
 
435
 
 
436
;Note the IF in the conclusion
 
437
(defthmd bits-cat-3
 
438
  (implies (and (>= i n)
 
439
                (< j n)
 
440
                (case-split (natp n))
 
441
                (case-split (natp m))
 
442
                (case-split (natp i))
 
443
                (case-split (natp j))
 
444
                )
 
445
           (equal (bits (cat x m y n) i j)
 
446
                  (cat (bits x (if (< i (+ m n))
 
447
                                    (- i n)
 
448
                                  (1- m))
 
449
                              0)
 
450
                        (+ 1 (- i n))
 
451
                        (bits y (1- n) j)
 
452
                        (- n j)))))
 
453
 
 
454
;includes both bits-cat-1, bits-cat-2, and bits-cat-3
 
455
;we expect the indices to be constants, so this won't cause case-splits
 
456
;gen
 
457
(defthm bits-cat
 
458
  (implies (and (case-split (natp n))
 
459
                (case-split (natp m))
 
460
                (case-split (natp i))
 
461
                (case-split (natp j)))
 
462
           (equal (bits (cat x m y n) i j)
 
463
                  (if (< i n)
 
464
                      (bits y i j)
 
465
                    (if (>= j n)
 
466
                        (bits x (if (< i (+ m n))
 
467
                                    (- i n)
 
468
                                  (1- m)) 
 
469
                              (- j n))
 
470
                      (cat (bits x (if (< i (+ m n))
 
471
                                        (- i n)
 
472
                                      (1- m)) 0)
 
473
                            (+ 1 (- i n))
 
474
                            (bits y (1- n) j)
 
475
                            (- n j)))))))
 
476
 
 
477
;The following trivial corollary of bits-cat is worth keeping enabled.
 
478
 
 
479
(defthm bits-cat-constants
 
480
  (implies (and (syntaxp (quotep n))
 
481
                (syntaxp (quotep m))
 
482
                (syntaxp (quotep i))
 
483
                (syntaxp (quotep j))
 
484
                (natp n)
 
485
                (natp m)
 
486
                (natp i)
 
487
                (natp j))
 
488
           (equal (bits (cat x m y n) i j)
 
489
                  (if (< i n)
 
490
                      (bits y i j)
 
491
                    (if (>= j n)
 
492
                        (bits x (if (< i (+ m n))
 
493
                                    (- i n)
 
494
                                  (1- m)) 
 
495
                              (- j n))
 
496
                      (cat (bits x (if (< i (+ m n))
 
497
                                       (- i n)
 
498
                                     (1- m)) 0)
 
499
                           (+ 1 (- i n))
 
500
                           (bits y (1- n) j)
 
501
                           (- n j)))))))
 
502
 
 
503
;bitn-cat should be all we need for simplifying (bitn (cat...))
 
504
(defthmd bitn-cat-1
 
505
  (implies (and (< i n)
 
506
                (case-split (natp n))
 
507
                (case-split (natp m))
 
508
                (case-split (natp i))
 
509
                )
 
510
           (equal (bitn (cat x m y n) i)
 
511
                  (bitn y i))))
 
512
 
 
513
;bitn-cat should be all we need for simplifying (bitn (cat...))
 
514
(defthmd bitn-cat-2
 
515
  (implies (and (>= i n)
 
516
                (case-split (natp n))
 
517
                (case-split (natp m))
 
518
                (case-split (integerp i))
 
519
                )
 
520
           (equal (bitn (cat x m y n) i)
 
521
                  (if (< i (+ m n))
 
522
                      (bitn x (- i n))
 
523
                    0))))
 
524
 
 
525
;includes both bitn-cat-1 and bitn-cat-2
 
526
(defthm bitn-cat
 
527
  (implies (and (case-split (natp n))
 
528
                (case-split (natp m))
 
529
                (case-split (natp i)))
 
530
           (equal (bitn (cat x m y n) i)
 
531
                  (if (< i n)
 
532
                      (bitn y i)
 
533
                    (if (< i (+ m n))
 
534
                      (bitn x (- i n))
 
535
                    0)))))
 
536
 
 
537
;The following trivial corollary of bitn-cat is worth keeping enabled.
 
538
 
 
539
(defthm bitn-cat-constants
 
540
  (implies (and (syntaxp (quotep n))
 
541
                (syntaxp (quotep m))
 
542
                (syntaxp (quotep i))
 
543
                (natp n)
 
544
                (natp m)
 
545
                (natp i))
 
546
           (equal (bitn (cat x m y n) i)
 
547
                  (if (< i n)
 
548
                      (bitn y i)
 
549
                    (if (< i (+ m n))
 
550
                      (bitn x (- i n))
 
551
                    0)))))
 
552
 
 
553
(defthm cat-bits-bits
 
554
  (implies (and (equal j (1+ k))
 
555
                (equal n (+ 1 (- l) k))
 
556
                (case-split (<= (+ 1 (- j) i) m))
 
557
                (case-split (<= j i))
 
558
                (case-split (<= l k))
 
559
                (case-split (integerp i))
 
560
                (case-split (integerp k))
 
561
                (case-split (integerp l))
 
562
                (case-split (integerp m))
 
563
                )
 
564
           (equal (cat (bits x i j) m (bits x k l) n)
 
565
                  (bits x i l))))
 
566
 
 
567
(defthm cat-bitn-bits
 
568
    (implies (and (equal j (+ 1 k))
 
569
                  (equal n (+ 1 (- l) k))
 
570
                  (case-split (<= 1 m))
 
571
                  (case-split (<= l k))
 
572
                  (case-split (integerp j))
 
573
                  (case-split (integerp k))
 
574
                  (case-split (integerp l))
 
575
                  (case-split (integerp m))
 
576
                  )
 
577
             (equal (cat (bitn x j) m (bits x k l) n)
 
578
                    (bits x j l))))
 
579
 
 
580
(defthm cat-bits-bitn
 
581
  (implies (and (equal j (+ 1 k))
 
582
                (case-split (<= (+ 1 (- j) i) m))
 
583
                (case-split (<= j i))
 
584
                (case-split (integerp i))
 
585
                (case-split (integerp j))
 
586
                (case-split (integerp k))
 
587
                (case-split (integerp m))
 
588
                )
 
589
           (equal (cat (bits x i j) m (bitn x k) 1)
 
590
                  (bits x i k))))
 
591
 
 
592
(defthm cat-bitn-bitn
 
593
  (implies (and (equal i (+ 1 j))
 
594
                (case-split (integerp i))
 
595
                (case-split (integerp j)))
 
596
           (equal (cat (bitn x i) 1 (bitn x j) 1)
 
597
                  (bits x i j))))
 
598
 
 
599
 
 
600
;may not want this enabled (but probably do want CAT-EQUAL-CONSTANT enabled)
 
601
;the BITS calls around X and Y in the conclusion allow us to drop the hyps that X and Y are bvecps.
 
602
(defthmd cat-split-equality
 
603
  (implies (and (case-split (bvecp k (+ m n))) ;if not, K can't be equal to the CAT expression
 
604
                (case-split (integerp m))
 
605
                (case-split (<= 0 m))
 
606
                (case-split (integerp n))
 
607
                (case-split (<= 0 n))
 
608
                )
 
609
           (equal (equal k (cat x m y n))
 
610
                  (and (equal (bits y (1- n) 0) (bits k (1- n) 0))
 
611
                       (equal (bits x (1- m) 0) (bits k (+ -1 m n) n))))))
 
612
 
 
613
 
 
614
 
 
615
;generalize this by dropping the bvecp-hyps and wrapping bits around x and y in the conclusion?
 
616
;follows trivially from   cat-split-equality
 
617
;prove a version of this without the bvecp hyps?
 
618
(defthm cat-equal-constant
 
619
  (implies (and (syntaxp (and (quotep k)
 
620
                              (quotep m)
 
621
                              (quotep n)))
 
622
                (case-split (bvecp y n))
 
623
                (case-split (bvecp x m))
 
624
                (case-split (< k (expt 2 (+ m n)))) ;drop!
 
625
                (case-split (integerp k))
 
626
                (case-split (<= 0 k))
 
627
                (case-split (integerp m))
 
628
                (case-split (<= 0 m))
 
629
                (case-split (integerp n))
 
630
                (case-split (<= 0 n))
 
631
                )
 
632
           (equal (equal k (cat x m y n))
 
633
                  (and (equal y (bits k (1- n) 0))
 
634
                       (equal x (bits k (+ -1 m n) n))))))
 
635
 
 
636
;lacks the bvecp hyps.  do we want this or cat-equal-rewrite?
 
637
(defthm cat-equal-rewrite-alt
 
638
  (implies (and (case-split (natp n))
 
639
                (case-split (natp m))
 
640
                )
 
641
           (equal (equal (cat x1 m y1 n)
 
642
                         (cat x2 m y2 n))
 
643
                  (and (equal (bits x1 (1- m) 0) (bits x2 (1- m) 0))
 
644
                       (equal (bits y1 (1- n) 0) (bits y2 (1- n) 0))))))
 
645
 
 
646
;move hyps to conclusion?
 
647
(defthm cat-equal-rewrite
 
648
  (implies (and (case-split (bvecp x1 m))
 
649
                (case-split (bvecp y1 n))
 
650
                (case-split (bvecp x2 m))
 
651
                (case-split (bvecp y2 n))
 
652
                (case-split (integerp n))
 
653
                (case-split (<= 0 n))
 
654
                (case-split (integerp m))
 
655
                (case-split (<= 0 m))
 
656
                )
 
657
           (equal (equal (cat x1 m y1 n)
 
658
                         (cat x2 m y2 n))
 
659
                  (and (equal x1 x2)
 
660
                       (equal y1 y2)))))
 
661
 
 
662
(defthm cat-bits-bits-bits
 
663
  (implies (and (<= k i)
 
664
                (<= l k)
 
665
                (<= j l)
 
666
                (integerp i)
 
667
                (integerp j)
 
668
                (integerp k)
 
669
                (integerp l)
 
670
                )
 
671
           (equal (cat (bits x i (+ 1 k))
 
672
                       (+ 2 i (- k))
 
673
                       (cat (bits x k l)
 
674
                            (+ 1 k (- l))
 
675
                            (bits x (1- l) j)
 
676
                            (+ l (- j)))
 
677
                       (+ 1 (- j) k))
 
678
                  (bits x i j)))
 
679
  :rule-classes nil)
 
680
 
 
681
#|
 
682
bits-dont-match can prove things like this:
 
683
(thm (IMPLIES (EQUAL 7 (BITS x 8 6))
 
684
              (NOT (EQUAL 3 (BITS x 15 6)))))
 
685
|#
 
686
 
 
687
(defthm bits-dont-match 
 
688
  (implies (and (syntaxp (and (quotep i)
 
689
                              (quotep j)
 
690
                              (quotep k)))
 
691
                (equal (bits x i2 j2) k2) ;i2, j2, and k2 are free vars
 
692
                (syntaxp (and (quotep i2)
 
693
                              (quotep j2)
 
694
                              (quotep k2)))
 
695
                (<= j2 j) (<= j i) (<= i i2)
 
696
                (not (equal k (bits k2 (+ i (- j2)) (+ (- j2) j))))
 
697
                (<= 0 i) (<= 0 j) (<= 0 k) (<= 0 i2) (<= 0 j2) (<= 0 k2)
 
698
                (integerp i) (integerp j)  (integerp k) (integerp i2) (integerp j2) (integerp k2)
 
699
                )
 
700
           (equal (equal k (bits x i j))
 
701
                  nil)))
 
702
 
 
703
; improve somehow?
 
704
(defthm bits-match
 
705
  (implies (and (syntaxp (and (quotep i)
 
706
                              (quotep j)
 
707
                              (quotep k)))
 
708
                (equal (bits x i2 j2) k2) ;i2, j2, and k2 are free vars
 
709
                (syntaxp (and (quotep i2)
 
710
                              (quotep j2)
 
711
                              (quotep k2)))
 
712
                (<= j2 j) (<= j i) (<= i i2)
 
713
                (equal k (bits k2 (+ i (- j2)) (+ (- j2) j)))
 
714
                (<= 0 i) (<= 0 j) (<= 0 k) (<= 0 i2) (<= 0 j2) (<= 0 k2)
 
715
                (integerp i) (integerp j)  (integerp k) (integerp i2) (integerp j2) (integerp k2)
 
716
                )
 
717
           (equal (equal k (bits x i j))
 
718
                  t)))
 
719
 
 
720
 
 
721
;make into a rewrite rule
 
722
(defthm cat-with-slice-of-x-equal-x
 
723
  (implies (and (bvecp x (+ m n))
 
724
                (case-split (bvecp y n))
 
725
                (case-split (<= 0 m))
 
726
                (case-split (<= 0 n))
 
727
                (case-split (integerp m))
 
728
                (case-split (integerp n))
 
729
                )
 
730
           (equal (equal x (cat (bits x (+ -1 m n) n) m y n))
 
731
                  (equal (bits x (1- n) 0) y))
 
732
           ))
 
733
 
 
734
;cat-with-slice-of-x-equal-x won't match, so we use kk here
 
735
;add a syntaxp hyp?
 
736
(defthm cat-with-slice-of-x-equal-x-rewrite
 
737
  (implies (and (equal kk (+ -1 m n))
 
738
                (bvecp x (+ m n))
 
739
                (case-split (bvecp y n))
 
740
                (case-split (<= 0 m))
 
741
                (case-split (<= 0 n))
 
742
                (case-split (integerp m))
 
743
                (case-split (integerp n))
 
744
                )
 
745
           (equal (equal x (cat (bits x kk n) m y n))
 
746
                  (equal (bits x (1- n) 0) y))
 
747
           ))
 
748
 
 
749
;If X and Y have identical bits in the range [i..j], then they also match on any subrange [k..l] of [i..j]
 
750
(defthmd bits-equal-implies-subranges-equal-helper
 
751
  (implies (and (equal (bits x i j) (bits y i j))
 
752
                (<= j l)
 
753
                (<= k i)
 
754
                (case-split (integerp i))
 
755
                (case-split (integerp j))
 
756
                (case-split (integerp k))
 
757
                (case-split (integerp l))
 
758
                )
 
759
           (equal (equal (bits x k l) (bits y k l))
 
760
                  t))
 
761
  :rule-classes ((:rewrite :match-free :all)))
 
762
 
 
763
(defthm bits-equal-implies-subranges-equal
 
764
  (implies (and (equal (bits x i j) (bits y i j))
 
765
                (<= j l)
 
766
                (<= k i)
 
767
                (case-split (integerp i))
 
768
                (case-split (integerp j))
 
769
                )
 
770
           (equal (equal (bits x k l) (bits y k l))
 
771
                  t))
 
772
  :rule-classes ((:rewrite :match-free :all)))
 
773
 
 
774
(defthmd cat-bits-1
 
775
    (equal (cat (bits x (1- m) 0) m y n)
 
776
           (cat x m y n)))
 
777
 
 
778
(defthmd cat-bits-2
 
779
    (equal (cat x m (bits y (1- n) 0) n)
 
780
           (cat x m y n)))