← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/coi/super-ihs/super-ihs-definitions.lsp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/coi/super-ihs/super-ihs-definitions.lsp
 
1
; Computational Object Inference
 
2
; Copyright (C) 2005-2014 Kookamara LLC
 
3
;
 
4
; Contact:
 
5
;
 
6
;   Kookamara LLC
 
7
;   11410 Windermere Meadows
 
8
;   Austin, TX 78759, USA
 
9
;   http://www.kookamara.com/
 
10
;
 
11
; License: (An MIT/X11-style license)
 
12
;
 
13
;   Permission is hereby granted, free of charge, to any person obtaining a
 
14
;   copy of this software and associated documentation files (the "Software"),
 
15
;   to deal in the Software without restriction, including without limitation
 
16
;   the rights to use, copy, modify, merge, publish, distribute, sublicense,
 
17
;   and/or sell copies of the Software, and to permit persons to whom the
 
18
;   Software is furnished to do so, subject to the following conditions:
 
19
;
 
20
;   The above copyright notice and this permission notice shall be included in
 
21
;   all copies or substantial portions of the Software.
 
22
;
 
23
;   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 
24
;   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 
25
;   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 
26
;   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 
27
;   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 
28
;   FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
 
29
;   DEALINGS IN THE SOFTWARE.
 
30
 
1
31
; Jared: what's this file for?  It's not certifiable, so I'm
2
32
; renaming it to a .lsp extension for Make compatibility
3
33
 
9
39
;(in-package "SUPER-IHS")
10
40
 
11
41
;;
12
 
;; This file isolates super-ihs definitions and types. The file currently 
 
42
;; This file isolates super-ihs definitions and types. The file currently
13
43
;; contains the following ACL2 constructs as they occur in the super-ihs book:
14
44
;; - defun
15
45
;; - defund
28
58
  :hints (("Goal" :in-theory (enable logext logapp))))
29
59
 
30
60
(defthm logext-when-i-is-zero
31
 
  (equal (logext size 0) 
 
61
  (equal (logext size 0)
32
62
         0)
33
 
  :hints (("goal" :in-theory (e/d (logext 
34
 
                                   logapp 
35
 
                                   ) 
 
63
  :hints (("goal" :in-theory (e/d (logext
 
64
                                   logapp
 
65
                                   )
36
66
                                  (LOGAPP-0)))))
37
67
 
38
68
(defthm logext-when-size-is-not-an-integerp
46
76
 
47
77
;rhs?
48
78
(defthm logext-when-size-is-0
49
 
  (equal (logext 0 i) 
 
79
  (equal (logext 0 i)
50
80
         (if (equal (logcar i) 0)
51
81
             0
52
82
           -1))
81
111
                (<= 0 n))
82
112
           (equal (evenp (logext n x))
83
113
                  (evenp (ifix x))))
84
 
  :hints (("Goal" :in-theory (e/d (logext) 
 
114
  :hints (("Goal" :in-theory (e/d (logext)
85
115
                                  (evenp loghead)))))
86
116
 
87
117
(defthm equal-logext-0
122
152
 
123
153
(defthm equal-logcons-0
124
154
  (equal (equal (logcons x y) 0)
125
 
         (and (equal (bfix x) 0) 
 
155
         (and (equal (bfix x) 0)
126
156
              (equal (ifix y) 0)))
127
 
  :hints (("goal" :in-theory (enable logcons 
128
 
                                     even-odd-different-2 
 
157
  :hints (("goal" :in-theory (enable logcons
 
158
                                     even-odd-different-2
129
159
                                     ))))
130
160
 
131
161
(defthm evenp-of-logcons
156
186
  :hints (("Goal" :in-theory (enable logcdr))))
157
187
 
158
188
(defthmd logcdr-of-zero
159
 
  (equal (logcdr 0) 
 
189
  (equal (logcdr 0)
160
190
         0)
161
191
  :hints (("goal" :in-theory (enable logcdr ifix))))
162
192
 
163
193
(defthm logcdr-when-i-is-not-an-integerp
164
194
  (implies (not (integerp i))
165
 
           (equal (logcdr i) 
 
195
           (equal (logcdr i)
166
196
                  0))
167
197
  :hints (("goal" :in-theory (enable logcdr ifix))))
168
198
 
169
199
;more like this?
170
200
(defthm logcdr-greater-than-0-rewrite
171
 
  (equal (< 0 (logcdr x))        
 
201
  (equal (< 0 (logcdr x))
172
202
         (and (integerp x)
173
203
              (<= 2 x))))
174
204
 
190
220
              (if (integerp x)
191
221
                  (unsigned-byte-p (1+ n) x)
192
222
                t)))
193
 
  :hints (("goal" 
 
223
  :hints (("goal"
194
224
           :in-theory (e/d (logcdr unsigned-byte-p ; expt
195
225
                                   EXPONENTS-ADD-UNRESTRICTED
196
226
                                   )
250
280
           (equal (logcdr (expt 2 n))
251
281
                  (expt 2 (1- n))))
252
282
  :hints (("goal" :in-theory (enable logcdr))))
253
 
           
 
283
 
254
284
(defthm logcdr---expt
255
285
  (implies (and (integerp n)
256
286
                (<= 0 n))
257
287
           (equal (logcdr (- (expt 2 n)))
258
 
                  (if (equal n 0) 
259
 
                      -1 
 
288
                  (if (equal n 0)
 
289
                      -1
260
290
                    (- (expt 2 (1- n))))))
261
291
  :hints (("goal" :in-theory (enable logcdr))))
262
292
 
263
293
(defthm logcdr-+2
264
294
  (implies (integerp x)
265
 
           (equal (logcdr (+ 2 x)) 
 
295
           (equal (logcdr (+ 2 x))
266
296
                  (1+ (logcdr x))))
267
297
  :hints (("goal" :in-theory (enable logcdr))))
268
298
 
287
317
(defthmd logcdr-*-1/2-expt
288
318
  (implies (and (syntaxp (quotep n))
289
319
                (integerp (* n m)))
290
 
           (equal (logcdr (* n m)) 
 
320
           (equal (logcdr (* n m))
291
321
                  (floor (* n m) 2)))
292
322
  :hints (("goal" :in-theory (enable logcdr))))
293
323
 
301
331
 
302
332
(defthm logcar-when-i-is-not-an-integerp
303
333
  (implies (not (integerp i))
304
 
           (equal (logcar i) 
 
334
           (equal (logcar i)
305
335
                  0))
306
336
  :hints (("goal" :in-theory (enable logcar ifix))))
307
337
 
352
382
                    (if (acl2-numberp i)
353
383
                        0
354
384
                      (logcar j)))))
355
 
  :hints (("Goal" :use (:instance logcar-+ (i j) (j i)) 
 
385
  :hints (("Goal" :use (:instance logcar-+ (i j) (j i))
356
386
           :in-theory (disable logcar-+))))
357
387
 
358
388
(defthm logcar-evenp
375
405
                (integerp k))
376
406
           (equal (logcar (+ i j (* 2 k)))
377
407
                  (logcar (+ i j))))
378
 
  :hints (("Goal" 
 
408
  :hints (("Goal"
379
409
           :use ((:instance logcar-i+2*j (i (+ i j)) (j k))))))
380
410
 
381
411
(defthm logcar-range
448
478
  :hints (("goal" :in-theory (enable logbitp ifix))))
449
479
 
450
480
(defthm logbitp-when-i-is-zero
451
 
  (equal (logbitp 0 j) 
 
481
  (equal (logbitp 0 j)
452
482
         (equal (logcar j) 1))
453
483
  :hints (("goal" :in-theory (enable logbit logbitp))))
454
484
 
497
527
 
498
528
(defthm logbit-when-i-is-not-an-integerp
499
529
  (implies (not (integerp i))
500
 
           (equal (logbit pos i) 
 
530
           (equal (logbit pos i)
501
531
                  0))
502
532
  :hints
503
533
  (("Goal" :in-theory (enable logbit))))
534
564
  :hints (("Goal" :in-theory (enable logbit))))
535
565
 
536
566
(defthm logbit-of-one
537
 
  (equal (logbit pos 1) 
 
567
  (equal (logbit pos 1)
538
568
         (if (zp pos)
539
569
             1
540
570
           0))
569
599
 
570
600
(defthm logapp-when-size-is-not-an-integerp
571
601
  (implies (not (integerp size))
572
 
           (equal (logapp size i j) 
 
602
           (equal (logapp size i j)
573
603
                  (ifix j)))
574
604
  :hints (("Goal" :in-theory (enable logext
575
605
                                     LOGAPP))))
576
606
 
577
607
(defthm logapp-when-size-is-negative
578
608
  (implies (< size 0)
579
 
           (equal (logapp size i j) 
 
609
           (equal (logapp size i j)
580
610
                  (ifix j)))
581
611
  :hints (("Goal" :in-theory (enable logext
582
612
                                     LOGAPP))))
674
704
in Acl2.  In particular, we prove the following theorem:
675
705
 
676
706
 (defthm convergence-of-iter-sqrt
677
 
   (implies (and (rationalp x)        
 
707
   (implies (and (rationalp x)
678
708
                 (rationalp epsilon)
679
709
                 (< 0 epsilon)
680
710
                 (<= 0 x))
722
752
;drop
723
753
(local (in-theory (enable (force)))) ;unfortunate that i had to do this
724
754
 
725
 
(local (in-theory (disable distributivity-alt))) 
 
755
(local (in-theory (disable distributivity-alt)))
726
756
 
727
757
;(include-book (:relative :back "arithmetic" "top")
728
758
;              :load-compiled-file nil)
742
772
    (let ((mid (/ (+ low high) 2)))
743
773
      (if (<= (* mid mid) x)
744
774
          (iterate-sqrt-range mid high x (1- num-iters))
745
 
        (iterate-sqrt-range low mid x 
 
775
        (iterate-sqrt-range low mid x
746
776
                            (1- num-iters))))))
747
777
 
748
778
;;
763
793
  (implies (and (rationalp low)
764
794
                (rationalp high)
765
795
                (< low high))
766
 
           (< (car (iterate-sqrt-range low high x 
 
796
           (< (car (iterate-sqrt-range low high x
767
797
                                       num-iters))
768
798
              (cdr (iterate-sqrt-range low high x
769
799
                                       num-iters))))
885
915
                      low high x
886
916
                      (guess-num-iters (- high low)
887
917
                                       (/ epsilon
888
 
                                          (+ high 
 
918
                                          (+ high
889
919
                                             high))))))
890
920
          (car range)))
891
921
    nil))
953
983
                               ceiling-greater-than-quotient
954
984
                               guess-num-iters-aux-is-a-good-guess))))
955
985
 
956
 
(in-theory (disable 
 
986
(in-theory (disable
957
987
            LOGNOT
958
988
            LOGCOUNT
959
989
            LOGBITP
972
1002
            BINARY-LOGXOR
973
1003
            LOGNOR
974
1004
            BITP
975
 
            logcar 
 
1005
            logcar
976
1006
            LOGCDR
977
1007
            LOGCONS
978
1008
            LOGBIT
1106
1136
(defun sub1-logcdr-logcdr-carry-induction (m x y c)
1107
1137
  (if (zp m)
1108
1138
      (or x y c)
1109
 
    (sub1-logcdr-logcdr-carry-induction 
1110
 
     (1- m) 
 
1139
    (sub1-logcdr-logcdr-carry-induction
 
1140
     (1- m)
1111
1141
     (logcdr x)
1112
1142
     (logcdr y)
1113
1143
     (b-ior (b-and (logcar x) (logcar y))
1117
1147
(defun sub1-logcdr-logcdr-logcdr-carry-induction (m x y z c)
1118
1148
  (if (zp m)
1119
1149
      (or x y c z)
1120
 
    (sub1-logcdr-logcdr-logcdr-carry-induction 
1121
 
     (1- m) 
 
1150
    (sub1-logcdr-logcdr-logcdr-carry-induction
 
1151
     (1- m)
1122
1152
     (logcdr x)
1123
1153
     (logcdr y)
1124
1154
     (logcdr z)
1129
1159
(defun sub1-sub1-logcdr-logcdr-carry-induction (m n x y c)
1130
1160
  (if (or (zp m) (zp n))
1131
1161
      (or x y c)
1132
 
    (sub1-sub1-logcdr-logcdr-carry-induction 
1133
 
     (1- m) 
 
1162
    (sub1-sub1-logcdr-logcdr-carry-induction
 
1163
     (1- m)
1134
1164
     (1- n)
1135
1165
     (logcdr x)
1136
1166
     (logcdr y)
1188
1218
    (+-r (logcdr a)
1189
1219
         (logcdr b)
1190
1220
         (b-maj (logcar a) (logcar b) c))))
1191
 
  
 
1221
 
1192
1222
(defthm +-induction t
1193
1223
  :rule-classes ((:induction :pattern (+ a b c)
1194
1224
                             :condition (unsigned-byte-p 1 c)
1209
1239
  (or (logendp x)
1210
1240
      (logendp y)
1211
1241
      (logbinr (logcdr x) (logcdr y))))
1212
 
  
 
1242
 
1213
1243
(defthm logand-induction t
1214
1244
  :rule-classes ((:induction :pattern (logand x y)
1215
1245
                             :condition t
1226
1256
                             :scheme (logbinr x y))))
1227
1257
 
1228
1258
(defun loglistr (n x)
1229
 
  (if (zp n) 
 
1259
  (if (zp n)
1230
1260
      (ifix x)
1231
1261
    (logcons 0 (loglistr (1- n) (logcdr x)))))
1232
1262
 
1284
1314
  (cond ((or (zip m) (zp n)) x)
1285
1315
        ((< m 0) (loglist-ashr (1+ m) n (logcdr x)))
1286
1316
        (t (loglist-ashr (1- m) (1- n) x))))
1287
 
        
 
1317
 
1288
1318
(defthm loglist-ash-induction t
1289
1319
  :rule-classes ((:induction :pattern (loglistr n (ash x m))
1290
1320
                             :condition t
1331
1361
(defthm loglist-+-induction t
1332
1362
   :rule-classes ((:induction :pattern (loglistr n (+ x y c))
1333
1363
                              :condition t
1334
 
                              :scheme (sub1-logcdr-logcdr-carry-induction n 
1335
 
                                                                          x 
1336
 
                                                                          y 
 
1364
                              :scheme (sub1-logcdr-logcdr-carry-induction n
 
1365
                                                                          x
 
1366
                                                                          y
1337
1367
                                                                          c))))
1338
1368
 
1339
1369
;same for lognot:
1401
1431
;;                 (< 0 n)
1402
1432
;;                 (unsigned-byte-p n y))
1403
1433
;;            (equal (if (equal 0 (logand (expt 2 (1- n)) y))
1404
 
;;                       y 
 
1434
;;                       y
1405
1435
;;                     (logior (- (expt 2 n)) y))
1406
1436
;;                   (logext n y)))
1407
1437
;;   :rule-classes nil
1419
1449
;;                 (< 0 n)
1420
1450
;;                 (unsigned-byte-p 1 (nth a x)))
1421
1451
;;            (not (logbitp n (nth a x))))
1422
 
;;   :hints (("goal" 
 
1452
;;   :hints (("goal"
1423
1453
;;            :in-theory (enable unsigned-byte-p logbitp*)
1424
1454
;;            :cases ((equal (nth a x) 0)))))
1425
1455
 
1437
1467
                )
1438
1468
           (unsigned-byte-p n (+ p (* 4 x))))
1439
1469
  :hints (("Goal" :in-theory (e/d (logapp) ( UNSIGNED-BYTE-P-LOGAPP))
1440
 
           :use (:instance UNSIGNED-BYTE-P-LOGAPP (size n) (size1 2) (i p) (j x))))) 
 
1470
           :use (:instance UNSIGNED-BYTE-P-LOGAPP (size n) (size1 2) (i p) (j x)))))
1441
1471
 
1442
1472
;; ;drop??? see next lemma
1443
1473
;; (defthmd logcdr-all-ones-lemma
1446
1476
;;                 (integerp n)
1447
1477
;;                 (< 0 n)
1448
1478
;;                 )
1449
 
;;            (equal (logcdr x) 
 
1479
;;            (equal (logcdr x)
1450
1480
;;                   (loghead (1- n) -1)))
1451
1481
;;   :rule-classes nil
1452
 
;;   :hints (("goal" 
 
1482
;;   :hints (("goal"
1453
1483
;;            :induct (unsigned-byte-p n x)
1454
1484
;;            :in-theory (enable LRDT))))
1455
1485
 
1461
1491
           (equal (unsigned-byte-p n (+ 1 x))
1462
1492
                  (and (integerp n)
1463
1493
                       (<= 0 n)
1464
 
                       (not (equal x 
 
1494
                       (not (equal x
1465
1495
                                   (loghead n -1) ;all ones!
1466
1496
                                   )))))
1467
 
  :hints (("goal" 
 
1497
  :hints (("goal"
1468
1498
           :induct (unsigned-byte-p n x)
1469
1499
           :in-theory (e/d (LRDT) (unsigned-byte-p* ;for acl2 3.0
1470
1500
                                   )))))
1489
1519
                  (< x (expt 2 (+ -1 n)))))
1490
1520
  :hints (("Goal" :in-theory (disable LOGBITP-TO-BOUND-WHEN-USB)
1491
1521
           :use (:instance logbitp-to-bound-when-usb))))
1492
 
                 
 
1522
 
1493
1523
(defthm logand-non-negative
1494
1524
  (implies (or (<= 0 x) (<= 0 y))
1495
1525
           (<= 0 (logand x y)))
1668
1698
  (equal (loghead-30-exec i)
1669
1699
         (loghead 30 i))
1670
1700
  :hints (("Goal" :in-theory (enable loghead-30-exec))))
1671
 
           
 
1701
 
1672
1702
(defund logbitp-30-exec (j)
1673
1703
  (declare (type (unsigned-byte 31) j))
1674
1704
  (not (equal 0 (logand 1073741824 j))))
1759
1789
 
1760
1790
;;
1761
1791
;; ODDP
1762
 
;; 
 
1792
;;
1763
1793
 
1764
1794
(in-theory (disable oddp))
1765
1795
 
1794
1824
  (equal (oddp (expt 2 j))
1795
1825
         (or (not (integerp j))
1796
1826
             (<= j 0)))
1797
 
  :hints (("Goal" :in-theory (enable oddp 
 
1827
  :hints (("Goal" :in-theory (enable oddp
1798
1828
                                     expt ;improve evenp rule and drop
1799
1829
                                     EXPONENTS-ADD-UNRESTRICTED))))
1800
1830
 
1801
1831
;consider adding (disabled!) versions of these without the backchain-limits?
1802
 
(defthmd even-odd-different-1 
 
1832
(defthmd even-odd-different-1
1803
1833
  (implies (and (evenp a)
1804
1834
                (not (evenp b)))
1805
1835
           (not (equal a b)))
1807
1837
 
1808
1838
;bzo do we need both of these rules?
1809
1839
;consider adding (disabled!) versions of these without the backchain-limits?
1810
 
(defthmd even-odd-different-2 
 
1840
(defthmd even-odd-different-2
1811
1841
  (implies (and (not (evenp a))
1812
1842
                (evenp b))
1813
1843
           (not (equal a b)))
1827
1857
  :hints (("Goal" :in-theory (enable oddp))))
1828
1858
 
1829
1859
(defthm oddp-of-*
1830
 
  (implies (and (integerp a) 
 
1860
  (implies (and (integerp a)
1831
1861
                (integerp b)
1832
1862
                )
1833
1863
           (equal (oddp (* a b))
1852
1882
   (equal (equal (expt 2 a) (1+ (* 2 b)))
1853
1883
          (and (zp a) (zip b))))
1854
1884
  :hints (("goal" :in-theory (enable expt))))
1855
 
 
 
1885
 
1856
1886
(defthm *ark*-equal-1+-+-*2-*2
1857
1887
  (implies (and (integerp a) (integerp b) (integerp c)
1858
1888
                (<= 0 a))
1889
1919
 
1890
1920
 
1891
1921
(defthm equal-i+-*2
1892
 
  (implies (and (integerp a) 
1893
 
                (integerp b) 
 
1922
  (implies (and (integerp a)
 
1923
                (integerp b)
1894
1924
                (integerp i)
1895
1925
                (<= 0 a)
1896
1926
                (not (evenp i)))
1897
1927
           (equal (equal (expt 2 a) (+ i (* 2 b)))
1898
1928
                  (and (zp a) (equal b (- (* 1/2 (+ -1 i)))))))
1899
1929
  :hints (("Goal" :in-theory (enable even-odd-different-2 even-odd-different-1))))
1900
 
  
 
1930
 
1901
1931
(defthm equal-i+-+-*2-*2
1902
 
  (implies (and (integerp a) 
1903
 
                (integerp b) 
 
1932
  (implies (and (integerp a)
 
1933
                (integerp b)
1904
1934
                (integerp c)
1905
1935
                (integerp i)
1906
1936
                (<= 0 a)
1911
1941
 
1912
1942
 
1913
1943
;; (defthm +i-*2-is-different-from-*2
1914
 
;;   (implies (and (integerp a) 
1915
 
;;                 (integerp b) 
1916
 
;;                 (integerp i) 
 
1944
;;   (implies (and (integerp a)
 
1945
;;                 (integerp b)
 
1946
;;                 (integerp i)
1917
1947
;;                 (not (evenp i)))
1918
1948
;;            (not (equal (+ i (* 2 a)) (* 2 b)))))
1919
1949
;;   :hints (("goal"
2080
2110
                (<= 0 I)
2081
2111
                (rationalp y)
2082
2112
                )
2083
 
           (EQUAL (FLOOR I Y)        
 
2113
           (EQUAL (FLOOR I Y)
2084
2114
                  1)))
2085
2115
 
2086
2116
 
2167
2197
  (declare (type (signed-byte 32) a)
2168
2198
           (type (signed-byte 32) b)
2169
2199
           (type (signed-byte 32) c))
2170
 
  (if (= a 0) 
2171
 
      c 
 
2200
  (if (= a 0)
 
2201
      c
2172
2202
    b))
2173
2203
 
2174
2204
;; We want to open c_conditional when the test value is a constant, since in
2239
2269
;; ADD32
2240
2270
;;
2241
2271
 
2242
 
(defund add32 (a b) 
 
2272
(defund add32 (a b)
2243
2273
  (declare
2244
2274
    (xargs :guard
2245
2275
         (and (signed-byte-p 32 a)
2256
2286
 
2257
2287
;is this ever used?
2258
2288
;I'm somewhat surprised that this doesn't chop its result down to 32 bits or something. -ews
2259
 
(defun addu32 (a b) 
 
2289
(defun addu32 (a b)
2260
2290
  (declare (xargs :guard (and (unsigned-byte-p 32 a)
2261
2291
                              (unsigned-byte-p 32 b))))
2262
2292
  (+ a b))
2266
2296
;;
2267
2297
 
2268
2298
;I'm somewhat surprised that this doesn't chop its result down to 16 bits or something. -ews
2269
 
(defun addu16 (a b) 
 
2299
(defun addu16 (a b)
2270
2300
  (declare (xargs :guard (and (unsigned-byte-p 16 a)
2271
2301
                              (unsigned-byte-p 16 b))))
2272
2302
  (+ a b))
2283
2313
;; ;; optimized for integers.  Thus we define xor32 and do compiler
2284
2314
;; ;; replacments on it.
2285
2315
;; ;does this ever get used?
2286
 
;; (defun xor32 (a b) 
 
2316
;; (defun xor32 (a b)
2287
2317
;;   (declare
2288
2318
;;     (xargs :guard
2289
2319
;;          (and (signed-byte-p 32 a)
2328
2358
 
2329
2359
(local (in-theory (enable FALSIFY-UNSIGNED-BYTE-P)))
2330
2360
 
2331
 
;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;           
 
2361
;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;
2332
2362
;; signed-byte-p, unsigned-byte-p
2333
2363
;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;
2334
2364
 
2383
2413
                )
2384
2414
           (equal (signed-byte-p n x)
2385
2415
                  (integerp n)))
2386
 
  :hints (("goal" 
 
2416
  :hints (("goal"
2387
2417
           :in-theory (enable signed-byte-p unsigned-byte-p)
2388
2418
           :use ((:instance EXPT-IS-INCREASING-FOR-BASE>1
2389
2419
                            (r 2)
2390
2420
                            (i free)
2391
2421
                            (j (1- n)))))))
2392
 
           
 
2422
 
2393
2423
(defthm unsigned-byte-p-subtype
2394
2424
  (implies (and (unsigned-byte-p free x) ;free is a free variable
2395
2425
                (<= free n)
2396
2426
                )
2397
2427
           (equal (unsigned-byte-p n x)
2398
 
                  (integerp n)  
 
2428
                  (integerp n)
2399
2429
                  ))
2400
 
  :hints (("goal" 
 
2430
  :hints (("goal"
2401
2431
           :in-theory (enable signed-byte-p unsigned-byte-p)
2402
2432
           :use ((:instance EXPT-IS-INCREASING-FOR-BASE>1
2403
2433
                            (r 2)
2419
2449
           (and (<= (- m) x)
2420
2450
                (<= x (+ -1 m))))
2421
2451
  :hints (("goal" :in-theory (enable signed-byte-p))))
2422
 
 
 
2452
 
2423
2453
(defthm unsigned-byte-p-logcdr-bridge5
2424
2454
  (implies (and (unsigned-byte-p (1+ n) (1+ x))
2425
2455
                (equal (logcar x) 1)
2470
2500
                (integerp x))
2471
2501
           (equal (unsigned-byte-p n (ash x m))
2472
2502
                  (unsigned-byte-p (max 0 (- n m)) x)))
2473
 
  :hints (("goal" 
2474
 
           :in-theory (e/d (LRDT 
2475
 
                            unsigned-byte-p*) 
 
2503
  :hints (("goal"
 
2504
           :in-theory (e/d (LRDT
 
2505
                            unsigned-byte-p*)
2476
2506
                           (ash* ;fixes a loop that manifested itself in the move to 3.0
2477
2507
                            open-logcons)))))
2478
2508
 
2502
2532
                  (if (equal 0 x)
2503
2533
                      t
2504
2534
                    (SIGNED-BYTE-P (- N m) X))))
2505
 
 
 
2535
 
2506
2536
  :otf-flg t
2507
2537
  :hints (("Goal" ; :induct (logcdr-induction x)
2508
2538
;:nonlinearp t
2509
2539
           :cases ((< x 0))
2510
 
           :in-theory (enable ;lrdt 
 
2540
           :in-theory (enable ;lrdt
2511
2541
                       SIGNED-BYTE-P
2512
2542
                       EXPONENTS-ADD-UNRESTRICTED
2513
2543
                       ))))
2528
2558
;;   :hints (("Goal" :in-theory (disable signed-byte-p-of-shift)
2529
2559
;;            :use ((:instance signed-byte-p-of-shift)
2530
2560
;;                  (:instance signed-byte-p-of-shift (x (- x)))))))
2531
 
           
 
2561
 
2532
2562
 
2533
2563
;;   :otf-flg t
2534
2564
;;   :hints (("Goal" ; :induct (logcdr-induction x)
2535
2565
;; ;:nonlinearp t
2536
2566
;;            :cases ((< x 0))
2537
 
;;            :in-theory (enable ;lrdt 
 
2567
;;            :in-theory (enable ;lrdt
2538
2568
;;                        SIGNED-BYTE-P
2539
2569
;;                        EXPONENTS-ADD-UNRESTRICTED
2540
2570
;;                        ))))
2541
 
        
 
2571
 
2542
2572
 
2543
2573
 
2544
2574
(defthm unsigned-byte-p-1+
2560
2590
                (unsigned-byte-p 1 c))
2561
2591
           (unsigned-byte-p n (+ c x y)))
2562
2592
  :rule-classes nil
2563
 
  :hints (("goal" :in-theory (e/d (unsigned-byte-p EXPONENTS-ADD-UNRESTRICTED) 
 
2593
  :hints (("goal" :in-theory (e/d (unsigned-byte-p EXPONENTS-ADD-UNRESTRICTED)
2564
2594
                                  (unsigned-byte-p-+)))))
2565
2595
 
2566
2596
(defthm unsigned-byte-p-+-bridge
2628
2658
(defthm ash-logior
2629
2659
  (equal (ash (logior x y) n)
2630
2660
         (logior (ash x n) (ash y n)))
2631
 
  :hints (("goal" 
 
2661
  :hints (("goal"
2632
2662
           :in-theory (e/d (LRDT zip) (ash*))
2633
2663
           :cases ((<= 0 n)))))
2634
2664
 
2644
2674
                )
2645
2675
           (equal (ash (ash x m) n)
2646
2676
                  (ash x (+ m n))))
2647
 
  :hints (("goal" 
2648
 
           :in-theory (e/d (LRDT expt2* ;ash 
 
2677
  :hints (("goal"
 
2678
           :in-theory (e/d (LRDT expt2* ;ash
2649
2679
                                 ;logtail*-better
2650
 
                                 ash-as-logtail 
 
2680
                                 ash-as-logtail
2651
2681
                                 ash-as-logapp
2652
2682
                                 open-logcons
2653
 
                                 zip) 
 
2683
                                 zip)
2654
2684
                           (logapp-0-part-2-better
2655
2685
                            EXPT-2-CRUNCHER)))))
2656
2686
 
2688
2718
;;                 (<= 0 n))
2689
2719
;;            (equal (ASH (ASH x m) n)
2690
2720
;;                   (ash x (+ m n)))))
2691
 
;;   :hints (("goal" 
 
2721
;;   :hints (("goal"
2692
2722
;;            :in-theory (enable LRDT ash-as-logtail ash-as-logapp))))
2693
2723
 
2694
2724
;; ;seems useless, and is proven instantly without hints.
2697
2727
;;                 (< n 0)
2698
2728
;;                 (unsigned-byte-p (- n) (nth n1 (nth n2 x))))
2699
2729
;;            (equal (ash (nth n1 (nth n2 x)) n) 0)))
2700
 
;;   :hints (("goal" :use (:instance ASH-GOES-TO-0 
2701
 
;;                                   (count (- n)) 
2702
 
;;                                   (size (- n)) 
 
2730
;;   :hints (("goal" :use (:instance ASH-GOES-TO-0
 
2731
;;                                   (count (- n))
 
2732
;;                                   (size (- n))
2703
2733
;;                                   (i x)))))
2704
2734
 
2705
2735
(defthm ash--1
2706
 
  (equal (ash x -1) 
 
2736
  (equal (ash x -1)
2707
2737
         (logcdr x))
2708
2738
  :hints (("goal" :in-theory (enable ash
2709
2739
                                     logcons ;bzo?
2723
2753
                  (if (< i n)
2724
2754
                      (logbitp i x)
2725
2755
                    (logbitp (1- n) x))))
2726
 
  :hints (("goal" 
 
2756
  :hints (("goal"
2727
2757
           :in-theory (enable LRDT)
2728
2758
           :induct (sub1-sub1-logcdr-induction i n x))))
2729
2759
 
2824
2854
                (unsigned-byte-p n y))
2825
2855
           (logbitp n (+ x y c)))
2826
2856
  :rule-classes nil
2827
 
  :hints (("goal" :in-theory (enable LRDT open-logcons)))) 
 
2857
  :hints (("goal" :in-theory (enable LRDT open-logcons))))
2828
2858
 
2829
2859
(defthm logbitp-+-usb-v2
2830
2860
  (implies (and (integerp n)
2872
2902
 
2873
2903
(defthm logbitp-+-usb-v4
2874
2904
  (implies (and (integerp n)
2875
 
                (< 0 n)    
 
2905
                (< 0 n)
2876
2906
                (not (logbitp (1- n) x))
2877
2907
                (unsigned-byte-p n x)
2878
2908
                (unsigned-byte-p n y)
2881
2911
                (not (logbitp n (+ y x)))))
2882
2912
  :hints (("goal" :use (:instance logbitp-+-usb-v4-helper (c 0)))))
2883
2913
 
2884
 
;; (deftheory overflow-bits 
2885
 
;;   '(logbitp-+-usb-v4 
2886
 
;;    logbitp-+-usb-v3 
2887
 
;;    logbitp-+-usb-v2 
2888
 
;;    logbitp-+-usb-v1 
2889
 
;;    logbitp-+-simple2 
 
2914
;; (deftheory overflow-bits
 
2915
;;   '(logbitp-+-usb-v4
 
2916
;;    logbitp-+-usb-v3
 
2917
;;    logbitp-+-usb-v2
 
2918
;;    logbitp-+-usb-v1
 
2919
;;    logbitp-+-simple2
2890
2920
;;    logbitp-+-simple
2891
2921
;;    unsigned-byte-p-+))
2892
2922
 
2893
2923
(in-theory (disable ;overflow-bits
2894
 
            logbitp-+-usb-v4 
2895
 
            logbitp-+-usb-v3 
2896
 
            logbitp-+-usb-v2 
2897
 
            logbitp-+-usb-v1 
2898
 
            logbitp-+-simple2 
 
2924
            logbitp-+-usb-v4
 
2925
            logbitp-+-usb-v3
 
2926
            logbitp-+-usb-v2
 
2927
            logbitp-+-usb-v1
 
2928
            logbitp-+-simple2
2899
2929
            logbitp-+-simple
2900
2930
            unsigned-byte-p-+))
2901
2931
 
2985
3015
           (equal (logbitp n1 (+ x (loghead n2 y) c))
2986
3016
                  (logbitp n1 (+ x y c))))
2987
3017
  :rule-classes nil
2988
 
  :hints (("goal" 
 
3018
  :hints (("goal"
2989
3019
           :in-theory (enable LRDT open-logcons)
2990
3020
           :induct (sub1-sub1-logcdr-logcdr-carry-induction n1 n2 x y c))))
2991
3021
 
3005
3035
                                     (logbitp n1 (+ x z y)))
3006
3036
                              (equal (logbitp n1 (+ x (loghead n2 y) z))
3007
3037
                                     (logbitp n1 (+ x y z)))))))
3008
 
  :hints (("goal" :use 
 
3038
  :hints (("goal" :use
3009
3039
           ((:instance logbitp-+-loghead-helper (c 0))
3010
3040
            (:instance logbitp-+-loghead-helper (c 0) (x (+ x z)))))))
3011
3041
 
3012
3042
(defthm logbitp-+-logext-bridge
3013
3043
  (implies (and (integerp n1)
3014
 
                (integerp n2)    
 
3044
                (integerp n2)
3015
3045
                (integerp x)
3016
3046
                (integerp y)
3017
3047
                (<= 0 n1)
3023
3053
                                     (logbitp n1 (+ x z y)))
3024
3054
                              (equal (logbitp n1 (+ x (logext n2 y) z))
3025
3055
                                     (logbitp n1 (+ x y z)))))))
3026
 
  :hints (("goal" :use 
 
3056
  :hints (("goal" :use
3027
3057
           ((:instance logbitp-+-logext (i n1) (x (+ x z)) (n n2))))))
3028
3058
 
3029
3059
(defthm logbitp-+-logext-bridge
3040
3070
                                     (logbitp n1 (+ x z y)))
3041
3071
                              (equal (logbitp n1 (+ x (logext n2 y) z))
3042
3072
                                     (logbitp n1 (+ x y z)))))))
3043
 
  :hints (("goal" :use 
 
3073
  :hints (("goal" :use
3044
3074
           ((:instance logbitp-+-logext (i n1) (x (+ x z)) (n n2))))))
3045
3075
 
3046
3076
(defthm logbitp---*2
3061
3091
 
3062
3092
(defthmd negate-as-bits
3063
3093
  (implies (integerp x)
3064
 
           (equal (- x) 
 
3094
           (equal (- x)
3065
3095
                  (1+ (lognot x))))
3066
3096
  :hints (("goal" :in-theory (enable LRDT logendp open-logcons))))
3067
3097
 
3074
3104
                (integerp x))
3075
3105
           (equal (logbitp n (- x))
3076
3106
                  (not (logbitp n (1- x)))))
3077
 
  :hints (("goal" 
 
3107
  :hints (("goal"
3078
3108
           :induct (logbitp n x) ;not necessary, but speeds things up
3079
3109
           :in-theory (enable LRDT negate-as-bits))))
3080
3110
 
3124
3154
 
3125
3155
(defthm negate-as-bits-reverse
3126
3156
  (implies (integerp x)
3127
 
           (equal (1+ (lognot x)) 
 
3157
           (equal (1+ (lognot x))
3128
3158
                  (- x)))
3129
3159
  :hints (("goal" :in-theory (enable LRDT logendp))))
3130
3160
 
3131
3161
(defthm negate-as-bits-reverse-bridge
3132
3162
  (implies (and (integerp x)
3133
3163
                (integerp y))
3134
 
           (equal (+ 1 x (lognot y)) 
 
3164
           (equal (+ 1 x (lognot y))
3135
3165
                  (+ x (- y))))
3136
 
  :hints (("goal" 
 
3166
  :hints (("goal"
3137
3167
           :use (:instance negate-as-bits-reverse (x y))
3138
3168
           :in-theory (disable negate-as-bits-reverse))))
3139
3169
 
3158
3188
 
3159
3189
(defthm logbitp-+-expt-n
3160
3190
  (implies (and (integerp x) ;drop?
3161
 
                (integerp n) 
 
3191
                (integerp n)
3162
3192
                (<= 0 n))
3163
3193
           (equal (logbitp n (+ (expt 2 n) x))
3164
3194
                  (not (logbitp n x))))
3191
3221
                (<= 0 n)
3192
3222
                (equal (loghead (1+ n) x) 0))
3193
3223
           (equal (logbitp n (+ x y)) (logbitp n y)))
3194
 
  :hints (("goal" 
 
3224
  :hints (("goal"
3195
3225
           :in-theory (enable LRDT)
3196
3226
           :induct (sub1-logcdr-logcdr-induction n x y))))
3197
3227
 
3346
3376
                (<= (1- m) n))
3347
3377
           (and (<= (- (expt 2 n)) (logext m x))
3348
3378
                (<= (logext m x) (1- (expt 2 n)))))
3349
 
  :hints (("goal" 
 
3379
  :hints (("goal"
3350
3380
           :in-theory (e/d (signed-byte-p) (signed-byte-p-logext))
3351
3381
           :use ((:instance signed-byte-p-logext (i x) (size1 (1+ n)) (size m))))))
3352
3382
 
3364
3394
                  (if (<= n m)
3365
3395
                      (logext n x)
3366
3396
                    (loghead m x))))
3367
 
  :hints (("goal" 
 
3397
  :hints (("goal"
3368
3398
           :in-theory (e/d (LRDT) (logext* LOGHEAD*))
3369
3399
           :induct (sub1-sub1-logcdr-induction n m x))))
3370
3400
 
3372
3402
  (implies (and (< m n)
3373
3403
                (<= 0 m)
3374
3404
                (integerp m)
3375
 
                (integerp n)     
 
3405
                (integerp n)
3376
3406
                )
3377
3407
           (equal (logext n (ash x m))
3378
3408
                  (ash (logext (- n m) x) m)))
3379
3409
  :hints (("goal"; :induct t
3380
 
           :in-theory (e/d (LRDT) (ASH-RECOLLAPSE 
 
3410
           :in-theory (e/d (LRDT) (ASH-RECOLLAPSE
3381
3411
                                   )))))
3382
3412
 
3383
3413
(defthm logext-logior
3390
3420
         (logext n (logior x y))))
3391
3421
 
3392
3422
(theory-invariant (incompatible (:rewrite logext-logior) (:rewrite logior-of-logext-and-logext)))
3393
 
  
 
3423
 
3394
3424
;; This should be in the loghead section, but it uses so many logext
3395
3425
;; rules we place it here.
3396
3426
 
3461
3491
;; (defthm logtail-logext-hack
3462
3492
;;   (equal (logtail 16 (logext 32 x))
3463
3493
;;          (logext 16 (logtail 16 x)))
3464
 
;;   :hints (("Goal" :in-theory (enable ;logtail 
 
3494
;;   :hints (("Goal" :in-theory (enable ;logtail
3465
3495
;;                                      logext ifix))))
3466
3496
 
3467
3497
;We make this a separate rule so it will be enabled even when logext-logapp is disabled.
3506
3536
                (unsigned-byte-p n y))
3507
3537
           (equal (ash (+ x y) (- n))
3508
3538
                  (if (unsigned-byte-p n (+ x y))
3509
 
                      0 
 
3539
                      0
3510
3540
                    1)))
3511
 
  :hints (("goal" 
 
3541
  :hints (("goal"
3512
3542
           :use (:instance ash-downto-1-or-0-helper (x (+ x y)))
3513
3543
           :in-theory (disable unsigned-byte-p-+))))
3514
3544
 
3549
3579
                (equal n (1+ m)))
3550
3580
           (equal (ash (logext n x) (- m))
3551
3581
                  (if (logbitp m x) -1 0)))
3552
 
  :hints (("goal" :use (:instance ash-sbp-downto-1-or-0-helper 
3553
 
                                  (n m) 
 
3582
  :hints (("goal" :use (:instance ash-sbp-downto-1-or-0-helper
 
3583
                                  (n m)
3554
3584
                                  (x (logext n x))))))
3555
3585
 
3556
3586
(defthm ash-sbp-downto-1-or-0-bridge
3560
3590
                (unsigned-byte-p n y))
3561
3591
           (equal (ash (+ x (- y)) (- n))
3562
3592
                  (if (logbitp n (+ x (- y))) -1 0)))
3563
 
  :hints (("goal" :use (:instance ash-sbp-downto-1-or-0-helper 
 
3593
  :hints (("goal" :use (:instance ash-sbp-downto-1-or-0-helper
3564
3594
                                  (x (+ x (- y))))
3565
3595
           :in-theory (enable unsigned-byte-p signed-byte-p))))
3566
3596
 
3568
3598
 
3569
3599
;; Needed just for the FCP models?
3570
3600
(defthm equal-ash-expt-0-fact
3571
 
  (implies (and (integerp n)                
 
3601
  (implies (and (integerp n)
3572
3602
                (integerp x)
3573
3603
                (<= 0 n))
3574
3604
           (equal (equal (ash (+ x (expt 2 n)) (- n)) 0)
3606
3636
                (unsigned-byte-p n y))
3607
3637
           (equal (ash (+ k x (- y)) (- n))
3608
3638
                  (if (logbitp n (+ x (- y))) 0 1)))
3609
 
  :hints (("goal" :use (:instance ash-sbp-expt-downto-1-or-0-helper 
 
3639
  :hints (("goal" :use (:instance ash-sbp-expt-downto-1-or-0-helper
3610
3640
                                  (x (+ x (- y)))))))
3611
3641
 
3612
3642
(defthm equal-ash-+---expt--1
3613
3643
  (implies (and (integerp n)
3614
 
                (<= 0 n) 
 
3644
                (<= 0 n)
3615
3645
                (signed-byte-p (1+ n) x))
3616
3646
           (equal (equal (ash (+ x (- (expt 2 n))) (- n)) -1)
3617
3647
                  (not (logbitp n x))))
3618
3648
  :hints (("goal" :in-theory (enable LRDT expt))))
3619
3649
 
3620
3650
(defthm equal-ash-+---expt--1-rewrite
3621
 
  (implies (and (syntaxp (quotep k)) (integerp k) 
 
3651
  (implies (and (syntaxp (quotep k)) (integerp k)
3622
3652
                (equal (- (expt 2 (1- (integer-length (- k))))) k)
3623
3653
                (equal n (1- (integer-length (- k))))
3624
3654
                (signed-byte-p (1+ n) x))
3625
3655
           (equal (equal (ash (+ k x) (- n)) -1)
3626
3656
                  (not (logbitp n x))))
3627
 
  :hints (("goal" :use (:instance equal-ash-+---expt--1 
 
3657
  :hints (("goal" :use (:instance equal-ash-+---expt--1
3628
3658
                                  (n (1- (integer-length (- k))))))))
3629
3659
 
3630
3660
(defthm ash-logext-neg
3675
3705
                (integerp n)
3676
3706
                (<= 0 n)
3677
3707
                )
3678
 
           (equal (ash x (- n)) 
 
3708
           (equal (ash x (- n))
3679
3709
                  (logbit n x)))
3680
3710
;  :rule-classes nil
3681
 
  :hints (("goal" 
 
3711
  :hints (("goal"
3682
3712
           :induct (logbitp n x)
3683
3713
           :in-theory (enable LRDT logbit))))
3684
3714
           ;; :induct (sub1-logcdr-induction n x)
3685
3715
;;            :in-theory (enable LOGOPS-RECURSIVE-DEFINITIONS-THEORY logbit))))
3686
 
  
 
3716
 
3687
3717
;; (defthm ash--15-special
3688
3718
;;   (implies
3689
3719
;;    (unsigned-byte-p 16 x)
3695
3725
;;   (implies (and (integerp n1)
3696
3726
;;                 (integerp n2)
3697
3727
;;                 (integerp x)
3698
 
;;                 (<= 0 n1) 
 
3728
;;                 (<= 0 n1)
3699
3729
;;                 (< n2 0))
3700
3730
;;            (equal (ash (loghead n1 x) n2)
3701
3731
;;                   (if (<= n1 (- n2))
3723
3753
                (< 0 n))
3724
3754
           (equal (< (+ (logext n x) (logext n y)) 0)
3725
3755
                  (logbitp n (+ (logext n x) (logext n y)))))
3726
 
  :hints (("goal" :use (:instance sign-as-logbitp 
 
3756
  :hints (("goal" :use (:instance sign-as-logbitp
3727
3757
                                  (x (+ (logext n x) (logext n y)))))))
3728
3758
 
3729
3759
(defthm sign-logext-as-logbitp
3733
3763
                  (logbitp (1- n) x)))
3734
3764
  :hints (("goal" :use (:instance sign-as-logbitp (x (logext n x)) (n (1- n))))))
3735
3765
 
3736
 
(in-theory (disable 
 
3766
(in-theory (disable
3737
3767
            B-NOT
3738
3768
            B-AND
3739
3769
            B-IOR
3756
3786
         (b-ior a (b-ior b c)))
3757
3787
  :hints (("Goal" :in-theory (enable b-ior))))
3758
3788
 
3759
 
(local (in-theory (enable b-xor b-eqv b-nand b-nor 
 
3789
(local (in-theory (enable b-xor b-eqv b-nand b-nor
3760
3790
                          b-andc1 b-andc2 b-orc1 b-orc2 b-not)))
3761
3791
 
3762
3792
 
3782
3812
 
3783
3813
(defthm b-xor-constant
3784
3814
  (implies (and (equal y 0)
3785
 
                (syntaxp (quotep y))    
 
3815
                (syntaxp (quotep y))
3786
3816
                (not (equal x y))
3787
3817
                (unsigned-byte-p 1 x)
3788
3818
                (unsigned-byte-p 1 z))
3951
3981
(in-theory (enable natp))
3952
3982
 
3953
3983
;since UNSIGNED-BYTE-P-FORWARD-TO-NONNEGATIVE-INTEGERP is built into acl2 and we have acl2::unsigned-byte-p-forward-to-expt-bound:
3954
 
(in-theory (disable ACL2::UNSIGNED-BYTE-P-FORWARD)) 
3955
 
 
3956
 
(local (in-theory (enable FALSIFY-UNSIGNED-BYTE-P))) 
3957
 
 
3958
 
(in-theory (disable 
 
3984
(in-theory (disable ACL2::UNSIGNED-BYTE-P-FORWARD))
 
3985
 
 
3986
(local (in-theory (enable FALSIFY-UNSIGNED-BYTE-P)))
 
3987
 
 
3988
(in-theory (disable
3959
3989
;            (:REWRITE ZP-OPEN)
3960
3990
 ;           (:REWRITE ZIP-OPEN)
3961
3991
 
4006
4036
;            (:REWRITE <-0-+-NEGATIVE-2)
4007
4037
;            (:REWRITE <-+-NEGATIVE-0-1)
4008
4038
;           (:REWRITE <-+-NEGATIVE-0-2)
4009
 
;dsh  Removed for ACL2 2.9.2, where NATP-CR and POSP-CR no longer exist.  
 
4039
;dsh  Removed for ACL2 2.9.2, where NATP-CR and POSP-CR no longer exist.
4010
4040
;     This change doesn't appear to affect proofs under ACL2 2.9.
4011
4041
;            (:COMPOUND-RECOGNIZER NATP-CR)
4012
4042
;            (:COMPOUND-RECOGNIZER POSP-CR)
4186
4216
  :hints (("Goal" :in-theory (enable ash))))
4187
4217
 
4188
4218
;bzo think more about the type of ash
4189
 
                 
 
4219
 
4190
4220
(defthm equal-ash-pos-0
4191
4221
  (implies (<= 0 c)
4192
4222
           (equal (equal (ash i c) 0)
4241
4271
                (integerp x)
4242
4272
                )
4243
4273
           (< b (ash x s)))
4244
 
  :hints (("goal" :in-theory (e/d (ash expt) 
 
4274
  :hints (("goal" :in-theory (e/d (ash expt)
4245
4275
                                  (FLOOR-OF-SHIFT-RIGHT-2)))))
4246
4276
 
4247
4277
(defthm ash-bound3
4298
4328
                )
4299
4329
           (equal (ASH (ASH x m) n)
4300
4330
                  (ash x (+ m n))))
4301
 
  :hints (("goal" :in-theory (enable ash ; LOGOPS-RECURSIVE-DEFINITIONS-THEORY 
 
4331
  :hints (("goal" :in-theory (enable ash ; LOGOPS-RECURSIVE-DEFINITIONS-THEORY
4302
4332
                                     expt
4303
4333
                                     ))))
4304
4334
 
4316
4346
  (implies (and (<= n 0)
4317
4347
                (integerp n)
4318
4348
                )
4319
 
           (equal (ash -1 n) 
 
4349
           (equal (ash -1 n)
4320
4350
                  -1))
4321
4351
  :hints (("goal" :in-theory (enable ash ;LRDT
4322
4352
                                     ))))
4323
4353
 
4324
 
(defthm ash-non-decreasing 
 
4354
(defthm ash-non-decreasing
4325
4355
  (implies (and (integerp k)
4326
4356
                (<= 0 k)
4327
4357
                (integerp n)
4377
4407
;;                 )
4378
4408
;;            (equal (ash (ash x m) n)
4379
4409
;;                   (ash x (+ m n))))
4380
 
;;   :hints (("goal" 
 
4410
;;   :hints (("goal"
4381
4411
;;            :in-theory (e/d (;LRDT expt2* ;ash-as-logtail ash-as-logapp open-logcons
4382
4412
;;                             expt
4383
4413
;;                             ash
4515
4545
;this was causing lots of generalization to occur, introducing mod into goals which had nothing to do with mod.
4516
4546
(in-theory (disable (:generalize MOD-X-Y-=-X+Y)))
4517
4547
 
4518
 
(in-theory (disable 
 
4548
(in-theory (disable
4519
4549
            (:DEFINITION NONNEGATIVE-INTEGER-QUOTIENT)
4520
4550
            (:DEFINITION FLOOR)
4521
4551
            (:DEFINITION CEILING)
4569
4599
(defthm integerp-/
4570
4600
  (implies (and (integerp n)
4571
4601
                (not (equal n 0)))
4572
 
           (equal (integerp (/ n)) 
 
4602
           (equal (integerp (/ n))
4573
4603
                  (or (equal n 1) (equal n -1))))
4574
4604
  :hints (("goal" :use ((:instance integerp-0-1 (x (/ n)))
4575
4605
                        (:instance integerp-0-1 (x (/ n)))))))
4798
4828
                     y)))
4799
4829
  :otf-flg t
4800
4830
  :hints (("Goal" :in-theory (e/d (evenp mod
4801
 
                                         FLOOR-NORMALIZES-TO-HAVE-J-BE-1) 
4802
 
                                  (;acl2::evenp-collapse 
 
4831
                                         FLOOR-NORMALIZES-TO-HAVE-J-BE-1)
 
4832
                                  (;acl2::evenp-collapse
4803
4833
                                   mod-cancel)))))
4804
4834
 
4805
4835
(DEFTHM INTEGERP-+-MINUS-*-1
4816
4846
(DEFTHM INTEGERP-+-MINUS-*-4
4817
4847
  (IMPLIES (AND (INTEGERP I) (INTEGERP J))
4818
4848
           (INTEGERP (* I J))))
4819
 
 
 
4849
 
4820
4850
(in-theory (disable INTEGERP-+-MINUS-*)) ;bzo
4821
4851
 
4822
4852
 
4867
4897
  (implies (syntaxp (not (quotep x))) ;without the not-quotep test, the rule matches things like: (< -1 x)
4868
4898
           (equal (< (- x) y)
4869
4899
                  (< 0 (+ x y)))))
4870
 
  
 
4900
 
4871
4901
(defthm move-negated-term-to-other-side-of-<-term-1-on-rhs
4872
4902
  (implies (syntaxp (not (quotep y))) ;without the not-quotep test, the rule matches things like: (< x -1) ?
4873
4903
           (equal (< x (- y))
5052
5082
           :in-theory (disable acl2::integerp-expt))))
5053
5083
 
5054
5084
(defthm integerp-prod-of-3-first-two
5055
 
  (implies (and (integerp (* a b)) 
 
5085
  (implies (and (integerp (* a b))
5056
5086
                (integerp c))
5057
5087
           (integerp (* a b c)))
5058
5088
  :hints (("Goal" :in-theory (disable acl2::integerp-+-minus-*-4)
5149
5179
  :hints (("Goal" :in-theory (enable loghead))))
5150
5180
 
5151
5181
(defthm loghead-when-i-is-0
5152
 
  (equal (loghead size 0) 
5153
 
         0) 
 
5182
  (equal (loghead size 0)
 
5183
         0)
5154
5184
  :hints (("Goal" :in-theory (enable loghead))))
5155
5185
 
5156
5186
(in-theory (disable loghead-size-0)) ;loghead-when-i-is-0 is better
5192
5222
         (if (< (nfix size1) (nfix size))
5193
5223
             (loghead (nfix size1) i)
5194
5224
           (loghead (nfix size) i)))
5195
 
  :hints (("Goal" :in-theory (e/d () 
 
5225
  :hints (("Goal" :in-theory (e/d ()
5196
5226
                                  (loghead-loghead
5197
5227
                                   loghead-leq))
5198
5228
           :use loghead-loghead)))
5199
5229
 
5200
 
(in-theory (disable loghead-loghead)) 
 
5230
(in-theory (disable loghead-loghead))
5201
5231
 
5202
5232
(defthm loghead-does-nothing-rewrite
5203
5233
  (equal (equal (loghead n x) x)
5228
5258
  (equal (logcar (loghead size i))
5229
5259
         (if (or (not (integerp size))
5230
5260
                 (<= size 0))
5231
 
             0 
 
5261
             0
5232
5262
           (logcar i)))
5233
5263
  :hints
5234
5264
  (("Goal" :use logcar-loghead
5235
5265
    :in-theory (e/d (
5236
 
                     ) 
 
5266
                     )
5237
5267
                    (logcar-loghead)))))
5238
5268
 
5239
 
(in-theory (disable logcar-loghead)) 
 
5269
(in-theory (disable logcar-loghead))
5240
5270
 
5241
5271
 
5242
5272
 
5270
5300
  :hints (("Goal" :use (:instance loghead-+-cancel)
5271
5301
           :in-theory (disable loghead-+-cancel))))
5272
5302
 
5273
 
(in-theory (disable loghead-+-cancel)) 
 
5303
(in-theory (disable loghead-+-cancel))
5274
5304
 
5275
5305
;make more versions of this
5276
5306
;bzo normalize the leading constant of things like (LOGHEAD 16 (+ 65535 x)).
5311
5341
             (loghead size (+ i1 i2 j))
5312
5342
           (loghead size (+ i1 i2))))
5313
5343
  :hints (("Goal" :use (:instance loghead-+-loghead-better (i (+ i1 i2)) (j j)))))
5314
 
  
 
5344
 
5315
5345
; improve loghead-cancel-better-alt, etc.
5316
5346
(defthm loghead-sum-subst-helper
5317
5347
  (implies (and (equal (loghead n x) y)
5367
5397
(defthm loghead-of-minus
5368
5398
  (equal (loghead n (- x))
5369
5399
         (if (integerp x)
5370
 
             (if (equal 0 (loghead n x)) 
 
5400
             (if (equal 0 (loghead n x))
5371
5401
                 0
5372
5402
               (- (expt 2 n) (loghead n x)) ;the usual case
5373
5403
               )
5385
5415
                  (EQUAL (LOGHEAD size (+ j A)) (LOGHEAD size K))))
5386
5416
  :hints (("Goal" :use (:instance LOGHEAD-+-CANCEL-BETTER (size size) (i j) (j a) (k (- k j)))))
5387
5417
  )
5388
 
        
 
5418
 
5389
5419
(defthm loghead-plus-constant-equal-constant
5390
5420
  (implies (and (syntaxp (and (quotep j)
5391
5421
                              (quotep k)))
5409
5439
                      (+ -1 (expt 2 n))
5410
5440
                    (+ -1 (loghead n x)))))
5411
5441
  :hints (("Goal" :in-theory (e/d (loghead
5412
 
                                     UNSIGNED-BYTE-P 
 
5442
                                     UNSIGNED-BYTE-P
5413
5443
                                     INTEGER-RANGE-P ;prove a rule for integer-range-p of (+ 1 x)
5414
5444
                                     imod
5415
 
                                     ) 
 
5445
                                     )
5416
5446
                                  (mod-cancel
5417
5447
                                   MOD-STRETCH-BASE ;looped!
5418
5448
                                   MOD-STRETCH-BASE-2 ;looped!
5515
5545
  :hints (("Goal" ;:in-theory (e/d (unary-/-of-expt loghead expt-gather) (expt-minus EXPONENTS-ADD))
5516
5546
           :use (:instance INTEGERP-EXPT (n (- n m)))
5517
5547
           :in-theory (e/d (loghead ifix
5518
 
                                    mod-cancel) 
 
5548
                                    mod-cancel)
5519
5549
                           (INTEGERP-OF-INVERSE-OF-EXPT
5520
5550
                                          MOD-X-I*J ;yucky force!
5521
5551
                                           ))
5572
5602
(defthm loghead-hack
5573
5603
  (equal (loghead 16 (+ -65535 off))
5574
5604
         (loghead 16 (+ 1 off)))
5575
 
  :hints (("Goal" :in-theory (enable loghead 
 
5605
  :hints (("Goal" :in-theory (enable loghead
5576
5606
                                     imod ifix))))
5577
5607
 
5578
5608
(defthm loghead-induction t
5599
5629
                            loghead*-better
5600
5630
                            unsigned-byte-p*
5601
5631
                            logcdr--
5602
 
                          
 
5632
 
5603
5633
                            ) ( ;evenp-of-logcons
5604
5634
                            UNSIGNED-BYTE-P-FORWARD
5605
 
                            ARITH-MOVE-NEGATED-TERM 
 
5635
                            ARITH-MOVE-NEGATED-TERM
5606
5636
                            expt-2-cruncher)))))
5607
5637
 
5608
5638
;See also the rule loghead-almost.
5634
5664
                      (+ (loghead n i) (loghead n j))
5635
5665
                    (+ (loghead n i) (loghead n j) (- (expt 2 n))))))
5636
5666
  :hints (("Goal" :in-theory (disable loghead-split-into-2-cases)
5637
 
           :use (:instance loghead-split-into-2-cases 
 
5667
           :use (:instance loghead-split-into-2-cases
5638
5668
                           (n n)
5639
5669
                           (x (+ (loghead n i) (loghead n j)))
5640
5670
                           ))))
5695
5725
;;             :do-not-induct t
5696
5726
;;             :in-theory (e/d (loghead-sum-split-into-2-cases
5697
5727
;;      ;UNSIGNED-BYTE-P-FORWARD-TO-NONNEGATIVE-INTEGERP
5698
 
;;                              ) 
 
5728
;;                              )
5699
5729
;;                             (LOGHEAD-TYPE ;bzo these disables are gross!
5700
5730
;;                              loghead-identity
5701
5731
;;                              LOGHEAD-DOES-NOTHING-REWRITE
5702
5732
;;                              UNSIGNED-BYTE-P-LOGHEAD-FORWARD-CHAINING)))))
5703
 
       
 
5733
 
5704
5734
(defthm loghead-cancel-lemma
5705
5735
  (implies (and (integerp a)
5706
5736
                (integerp size)
5766
5796
 
5767
5797
(defthmd loghead-hack2
5768
5798
  (implies (and (equal (expt 2 n) (+ (loghead n a) (loghead n b)))
5769
 
                (integerp a) 
 
5799
                (integerp a)
5770
5800
                (integerp b)
5771
5801
                )
5772
5802
           (equal (loghead n (+ a b))
5773
5803
                  0))
5774
5804
  :hints (("Goal" :in-theory (enable loghead-sum-split-into-2-cases))))
5775
 
        
 
5805
 
5776
5806
;; Allows ACL2 to quicly see that facts like this contradict:
5777
5807
;; (EQUAL x (LOGHEAD 16 (+ 4 y)))
5778
5808
;; (EQUAL (LOGHEAD 16 (+ 3 x)) y))
5792
5822
  (equal (evenp (loghead size i))
5793
5823
         (or (zp size)
5794
5824
             (evenp (ifix i))))
5795
 
  :hints (("Goal" :in-theory (e/d (loghead imod) 
 
5825
  :hints (("Goal" :in-theory (e/d (loghead imod)
5796
5826
                                  (mod-cancel)))))
5797
5827
 
5798
5828
;; ;bzo zz will going against acl2's order be bad?
5855
5885
  :hints (("Goal" :use (:instance acl2::loghead-+-cancel-0 (acl2::i i) (acl2::j j) (acl2::size size))
5856
5886
           :in-theory (disable acl2::loghead-+-cancel-0))))
5857
5887
 
5858
 
(in-theory (disable acl2::loghead-+-cancel-0)) 
 
5888
(in-theory (disable acl2::loghead-+-cancel-0))
5859
5889
 
5860
5890
(defthm loghead-+-cancel-0-alt
5861
5891
  (implies (and (integerp m)
5895
5925
           (equal (equal x (loghead n (+ b y)))
5896
5926
                  nil))
5897
5927
  :hints (("Goal" :use (:instance acl2::loghead-cancel-lemma-3 (acl2::n n) (acl2::b b) (acl2::x x) (acl2::a a))
5898
 
           :in-theory (disable acl2::loghead-cancel-lemma-3))))                 
 
5928
           :in-theory (disable acl2::loghead-cancel-lemma-3))))
5899
5929
 
5900
5930
 
5901
5931
 
6002
6032
  (implies (and (integerp j)
6003
6033
                (<= 0 size)
6004
6034
                (integerp size)
6005
 
                (integerp x) 
 
6035
                (integerp x)
6006
6036
                )
6007
6037
           (equal (loghead size (+ x (* j (expt 2 size))))
6008
6038
                  (loghead size x))))
6010
6040
(defthm loghead-of-sum-with-multiple-of-expt-2-size-alt
6011
6041
  (implies (and (integerp j)
6012
6042
                (<= 0 size)
6013
 
                (integerp size) 
6014
 
                (integerp x) 
 
6043
                (integerp size)
 
6044
                (integerp x)
6015
6045
                )
6016
6046
           (equal (loghead size (+ (* j (expt 2 size)) x))
6017
6047
                  (loghead size x))))
6059
6089
  :rule-classes ((:rewrite)
6060
6090
                 (:forward-chaining :trigger-terms ((lognot i)))))
6061
6091
 
6062
 
(defthm lognot-neg 
 
6092
(defthm lognot-neg
6063
6093
  (implies (integerp a)
6064
6094
           (equal (< (lognot a) 0)
6065
6095
                  (<= 0 a)))
6118
6148
  :hints (("Goal" :use (:instance logand-with-mask (size  (INTEGER-LENGTH MASK)))
6119
6149
           :in-theory (e/d () (logand-with-mask)))))
6120
6150
 
6121
 
(in-theory (disable logand-with-mask)) 
 
6151
(in-theory (disable logand-with-mask))
6122
6152
 
6123
6153
 
6124
6154
 
6136
6166
  :hints
6137
6167
  (("Goal" :in-theory (e/d (
6138
6168
;                            LOGHEAD-WITH-SIZE-NON-POSITIVE
6139
 
                            ) 
 
6169
                            )
6140
6170
                           (logextu-as-loghead))
6141
6171
    :use  logextu-as-loghead)))
6142
6172
 
6143
6173
(defthm logand-bit-0
6144
6174
  (implies (unsigned-byte-p 1 x)
6145
 
           (equal (logand x y) 
 
6175
           (equal (logand x y)
6146
6176
                  (b-and x (logcar y))))
6147
6177
  :hints (("goal" :in-theory (e/d (LRDT logand-zip) (LOGHEAD* logand*))))
6148
6178
  :rule-classes ((:rewrite :backchain-limit-lst 1)))
6150
6180
;prove from the other
6151
6181
(defthm logand-bit-1
6152
6182
  (implies (unsigned-byte-p 1 x)
6153
 
           (equal (logand y x) 
 
6183
           (equal (logand y x)
6154
6184
                  (b-and x (logcar y))))
6155
6185
  :hints (("goal" :in-theory (e/d (LRDT logand-zip) (LOGHEAD* logand*))))
6156
6186
  :rule-classes ((:rewrite :backchain-limit-lst 1)))
6170
6200
                 (equal (logand a c) 0)
6171
6201
                 (integerp a)
6172
6202
                 (integerp c))
6173
 
            (equal (logand a b c) 
 
6203
            (equal (logand a b c)
6174
6204
                   0))
6175
6205
   :hints (("goal" :in-theory (enable LRDT
6176
6206
                                      logendp
6177
 
                                      even-odd-different-1 
 
6207
                                      even-odd-different-1
6178
6208
                                      even-odd-different-2
6179
6209
                                      ))))
6180
6210
 
6201
6231
  :hints (("Goal" :in-theory (enable integer-length))))
6202
6232
 
6203
6233
(defthm logand-expt-constant-version
6204
 
  (implies (and (syntaxp (quotep n)) 
 
6234
  (implies (and (syntaxp (quotep n))
6205
6235
                (equal (expt 2 (1- (integer-length n))) n)
6206
6236
                (integerp n))
6207
6237
           (equal (logand n x)
6220
6250
 
6221
6251
;just use logand-expt-constant-version?
6222
6252
(defthm equal-logand-expt-rewrite
6223
 
  (implies (and (syntaxp (quotep n)) 
 
6253
  (implies (and (syntaxp (quotep n))
6224
6254
                (equal (expt 2 (1- (integer-length n))) n)
6225
6255
                (integerp n)
6226
6256
                )
6227
6257
           (equal (equal (logand n x) k)
6228
 
                  (if (logbitp (1- (integer-length n)) x) 
6229
 
                      (equal k n) 
 
6258
                  (if (logbitp (1- (integer-length n)) x)
 
6259
                      (equal k n)
6230
6260
                    (equal k 0))))
6231
 
  :hints (("goal" 
 
6261
  :hints (("goal"
6232
6262
           :in-theory (e/d (LRDT) (logand*))
6233
 
           :use (:instance equal-logand-expt 
 
6263
           :use (:instance equal-logand-expt
6234
6264
                           (n (1- (integer-length n)))))))
6235
6265
 
6236
6266
(defthm logand---expt
6239
6269
                (signed-byte-p (1+ n) x))
6240
6270
           (equal (logand (- (expt 2 n)) x)
6241
6271
                  (if (logbitp n x) (- (expt 2 n)) 0)))
6242
 
  :hints (("goal" 
 
6272
  :hints (("goal"
6243
6273
           :in-theory (enable LRDT expt2* ash open-logcons))))
6244
6274
 
6245
6275
(defthm logand---expt-rewrite
6246
 
  (implies (and (syntaxp (quotep k)) 
6247
 
                (integerp k) 
 
6276
  (implies (and (syntaxp (quotep k))
 
6277
                (integerp k)
6248
6278
                (equal (- (expt 2 (1- (integer-length (- k))))) k)
6249
6279
                (signed-byte-p (integer-length (- k)) x))
6250
6280
           (equal (logand k x)
6290
6320
  :hints (("goal" :in-theory (enable LRDT))))
6291
6321
 
6292
6322
(defthm logand-bfix
6293
 
  (and (equal (logand (bfix x) y) 
 
6323
  (and (equal (logand (bfix x) y)
6294
6324
              (b-and (bfix x) (logcar y)))
6295
 
       (equal (logand y (bfix x)) 
 
6325
       (equal (logand y (bfix x))
6296
6326
              (b-and (bfix x) (logcar y)))))
6297
6327
 
6298
6328
(defthm *ash*-equal-logand-ash-pos-0
6312
6342
           (equal (equal (- (expt 2 n)) (logand (- (expt 2 n)) x))
6313
6343
                  (equal (ash x (- n)) -1)))
6314
6344
  :rule-classes nil
6315
 
  :hints (("goal" 
 
6345
  :hints (("goal"
6316
6346
           :in-theory (e/d (LRDT expt2*
6317
 
                                 ) 
6318
 
                           (LOGCONS-OF-0 
 
6347
                                 )
 
6348
                           (LOGCONS-OF-0
6319
6349
                            )))))
6320
6350
 
6321
6351
(defthm equal-logand---expt---expt
6325
6355
                (equal (- (expt 2 (1- (integer-length (- k))))) k))
6326
6356
           (equal (equal k (logand k x))
6327
6357
                  (equal (ash x (- (1- (integer-length (- k))))) -1)))
6328
 
  :hints (("goal" 
6329
 
           :use (:instance *ash*-equal-logand---expt---expt-helper 
 
6358
  :hints (("goal"
 
6359
           :use (:instance *ash*-equal-logand---expt---expt-helper
6330
6360
                           (n (1- (integer-length (- k))))))))
6331
6361
 
6332
6362
(defthm logand---expt-v2
6338
6368
  :hints (("goal" :in-theory (enable LRDT expt2*))))
6339
6369
 
6340
6370
(defthm logand---expt-rewrite-v2
6341
 
  (implies (and (syntaxp (quotep k)) 
6342
 
                (integerp k) 
 
6371
  (implies (and (syntaxp (quotep k))
 
6372
                (integerp k)
6343
6373
                (equal (- (expt 2 (1- (integer-length (- k))))) k)
6344
6374
                (unsigned-byte-p (integer-length (- k)) x))
6345
6375
           (equal (logand k x)
6346
 
                  (if (logbitp (1- (integer-length (- k))) x) 
6347
 
                      (expt 2 (1- (integer-length (- k)))) 
 
6376
                  (if (logbitp (1- (integer-length (- k))) x)
 
6377
                      (expt 2 (1- (integer-length (- k))))
6348
6378
                    0)))
6349
 
  :hints (("goal" :use (:instance logand---expt-v2 
 
6379
  :hints (("goal" :use (:instance logand---expt-v2
6350
6380
                                  (n (1- (integer-length (- k))))))))
6351
6381
 
6352
6382
(defthm equal-logand---expt-0
6357
6387
                  (unsigned-byte-p n x)))
6358
6388
  :hints (("goal"
6359
6389
           :in-theory (e/d (LRDT)
6360
 
                           (logand---expt-v2 
6361
 
                            logand---expt-rewrite-v2 
 
6390
                           (logand---expt-v2
 
6391
                            logand---expt-rewrite-v2
6362
6392
                            logand---expt)))))
6363
6393
 
6364
6394
(defthm equal-logand---expt-0-rewrite
6365
6395
  (implies (and (integerp x)
6366
 
                (syntaxp (quotep k)) (integerp k) 
 
6396
                (syntaxp (quotep k)) (integerp k)
6367
6397
                (equal (- (expt 2 (1- (integer-length (- k))))) k))
6368
6398
           (equal (equal (logand k x) 0)
6369
6399
                  (unsigned-byte-p (1- (integer-length (- k))) x)))
6370
 
  :hints (("goal" :use (:instance equal-logand---expt-0 
 
6400
  :hints (("goal" :use (:instance equal-logand---expt-0
6371
6401
                                  (n (1- (integer-length (- k))))))))
6372
6402
 
6373
6403
;see from-rtl.lisp for more stuff about logand (and perhaps other functions...)
6383
6413
  (equal (logand x x y)
6384
6414
         (logand x y))
6385
6415
  :hints (("Goal" :in-theory (e/d (LOGAND-ZIP)
6386
 
                                  (logand 
 
6416
                                  (logand
6387
6417
                                   COMMUTATIVITY-OF-LOGAND
6388
6418
                                   logand-associative))
6389
6419
           :use (:instance logand-associative
6432
6462
           (equal (logbitp n (logcdr y))
6433
6463
                  (logbitp (+ 1 n) y)))
6434
6464
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
6435
 
           :in-theory (e/d (logbitp 
 
6465
           :in-theory (e/d (logbitp
6436
6466
                            logcdr
6437
 
                            exponents-add-unrestricted) 
 
6467
                            exponents-add-unrestricted)
6438
6468
                           (FLOOR-OF-SHIFT-RIGHT-2)))))
6439
6469
 
6440
6470
;similarly for logtail?
6470
6500
           (equal (equal (logior y z) x)
6471
6501
                  (and (logbitp (1- (integer-length x)) (logior y z))
6472
6502
                       (equal 0 (logand (lognot x) (logior y z))))))
6473
 
  :hints (("goal" 
6474
 
           :do-not '(;generalize eliminate-destructors 
 
6503
  :hints (("goal"
 
6504
           :do-not '(;generalize eliminate-destructors
6475
6505
                      ;          fertilize ;bzo. why didn't it fertilize completely?
6476
6506
                                )
6477
 
           :in-theory (e/d (LRDT 
6478
 
                              even-odd-different-2 
 
6507
           :in-theory (e/d (LRDT
 
6508
                              even-odd-different-2
6479
6509
                              even-odd-different-1
6480
6510
                              expt2*
6481
6511
                              EQUAL-B-NOT-LOGCAR
6482
6512
                              ;ash
6483
 
                              ) 
 
6513
                              )
6484
6514
                           (integer-length*
6485
6515
                            LOGCONS-OF-0
6486
6516
                            ))
6533
6563
                      (ash (loghead (1+ m) (1+ x)) (1- n))
6534
6564
                    (ash (loghead (1+ m) x) (1- n)))))
6535
6565
  :rule-classes nil
6536
 
  :hints (("goal" 
 
6566
  :hints (("goal"
6537
6567
           :in-theory (e/d (LRDT loghead* equal-logior-*2) (LOGHEAD-SUM-SPLIT-INTO-2-WHEN-I-IS-A-CONSTANT
6538
6568
                                                            LOGCONS-OF-0))
6539
6569
           :induct (sub1-induction n))))
6550
6580
                  (if (equal (logcar x) 0)
6551
6581
                      (ash (loghead (1+ m) (1+ x)) (1- n))
6552
6582
                    (ash (loghead (1+ m) x) (1- n)))))
6553
 
  :hints (("goal" :use (:instance logior-expt-ash-loghead-bridge-helper 
 
6583
  :hints (("goal" :use (:instance logior-expt-ash-loghead-bridge-helper
6554
6584
                                  (n (integer-length v))))))
6555
6585
 
6556
6586
(defthm logior-expt-ash-loghead-bridge-bridge
6604
6634
                (unsigned-byte-p n v)
6605
6635
                (not (unsigned-byte-p n (+ v a))))
6606
6636
           (equal (+ v (logior a (ash x n)))
6607
 
                  (logior (loghead n (+ v a)) 
 
6637
                  (logior (loghead n (+ v a))
6608
6638
                          (ash (1+ x) n))))
6609
6639
  :hints (("goal" :in-theory (e/d (logior-as-+
6610
6640
;                                   ash-+-pos
6612
6642
                                   )
6613
6643
                                  ( UNSIGNED-BYTE-P-+-EASY
6614
6644
                                   UNSIGNED-BYTE-P-+)))
6615
 
          ("goal''" :in-theory (e/d (ash-+-pos 
 
6645
          ("goal''" :in-theory (e/d (ash-+-pos
6616
6646
                                     LOGHEAD-ALMOST
6617
6647
                                     )
6618
6648
                                    ( UNSIGNED-BYTE-P-+)))))
6623
6653
(defthm logior-lognot
6624
6654
  (equal (logior x (lognot x))
6625
6655
         -1)
6626
 
  :hints (("goal" 
6627
 
           :in-theory (enable LRDT logendp)))) 
 
6656
  :hints (("goal"
 
6657
           :in-theory (enable LRDT logendp))))
6628
6658
 
6629
6659
(defthm logor-lognot-1
6630
6660
  (implies (and (integerp x)
6636
6666
                                   (k y))))))
6637
6667
 
6638
6668
(defthm logior-duplicate
6639
 
  (equal (logior x x) 
 
6669
  (equal (logior x x)
6640
6670
         (ifix x))
6641
 
  :hints (("goal" 
 
6671
  :hints (("goal"
6642
6672
           :induct (logcdr-induction x)
6643
 
           :in-theory (enable LRDT zip 
 
6673
           :in-theory (enable LRDT zip
6644
6674
                              ))))
6645
6675
 
6646
6676
;add to rtl library?
6647
6677
(defthm logior-duplicate-1
6648
 
  (equal (logior x x y) 
 
6678
  (equal (logior x x y)
6649
6679
         (logior x y))
6650
 
  :hints (("goal" 
 
6680
  :hints (("goal"
6651
6681
           :in-theory (e/d () ( logior-associative))
6652
6682
           :use ((:instance logior-associative
6653
6683
                            (i x)
6669
6699
 
6670
6700
;; ;; moved to logcar
6671
6701
;; ;; (defthm logcar-logxor
6672
 
;; ;;   (implies (and (integerp a) 
 
6702
;; ;;   (implies (and (integerp a)
6673
6703
;; ;;                 (integerp b))
6674
 
;; ;;            (equal (logcar (logxor a b)) 
 
6704
;; ;;            (equal (logcar (logxor a b))
6675
6705
;; ;;                   (b-xor (logcar a) (logcar b))))
6676
6706
;; ;;   :hints (("goal" :in-theory (enable
6677
6707
;; ;;                               LOGOPS-RECURSIVE-DEFINITIONS-THEORY
6678
6708
;; ;;                               simplify-bit-functions))))
6679
6709
 
6680
6710
;; (defthm logxor-lognot
6681
 
;;   (implies (and (integerp a) 
 
6711
;;   (implies (and (integerp a)
6682
6712
;;                 (integerp b))
6683
6713
;;            (and (equal (logxor (lognot a) b) (lognot (logxor a b)))
6684
6714
;;                 (equal (logxor a (lognot b)) (lognot (logxor a b)))))
6685
 
;;   :hints (("goal" 
 
6715
;;   :hints (("goal"
6686
6716
;;            :in-theory (enable LRDT simplify-bit-functions))))
6687
6717
 
6688
6718
 
6689
6719
 
6690
6720
;; (defthm logxor-cancel2
6691
 
;;   (implies (and (integerp a) 
 
6721
;;   (implies (and (integerp a)
6692
6722
;;                 (integerp b))
6693
6723
;;            (equal (logxor b (logxor b a)) a))
6694
6724
;;   :hints (("goal" :use (:instance commutativity-of-logxor
6720
6750
;;                 (integerp y))
6721
6751
;;            (and
6722
6752
;;             (equal (logior z (logxor x y))
6723
 
;;                    (logior z 
 
6753
;;                    (logior z
6724
6754
;;                            (logior (logand x (lognot y))
6725
6755
;;                                    (logand (lognot x) y))))
6726
6756
;;             (equal (logior (logxor x y) z)
6754
6784
 :hints (("goal" :in-theory (enable LRDT logendp))))
6755
6785
          ;; :induct (logcdr-logcdr-induction x y)
6756
6786
;;            :in-theory (enable LOGOPS-RECURSIVE-DEFINITIONS-THEORY))))
6757
 
 
 
6787
 
6758
6788
(defthm lognand-rewrite
6759
6789
 (implies (and (integerp x)
6760
6790
               (integerp y))
6804
6834
            (implies (and (>= i 0))
6805
6835
                     (<= (logand j i) i)))))
6806
6836
 
6807
 
(in-theory (disable logand-upper-bound)) 
 
6837
(in-theory (disable logand-upper-bound))
6808
6838
 
6809
6839
(defthm equal-logapp-x-y-z-constants
6810
6840
  (implies (and (syntaxp (quotep z))
6828
6858
                (<= 0 n))
6829
6859
           (equal (logapp n (logior w y) (logior x z))
6830
6860
                  (logior (logapp n w x) (logapp n y z))))
6831
 
  :hints (("goal" :in-theory (enable LRDT)))) 
 
6861
  :hints (("goal" :in-theory (enable LRDT))))
6832
6862
 
6833
6863
(defthm logapp-logand
6834
6864
  (implies (and (integerp w)
6869
6899
 
6870
6900
(defthm loghead-logior
6871
6901
  (implies (and (integerp n)
6872
 
                (integerp x) 
 
6902
                (integerp x)
6873
6903
                (integerp y)
6874
6904
                (<= 0 n))
6875
6905
           (equal (loghead n (logior x y))
6895
6925
                    (ash (loghead (- n1 n2) x) n2))))
6896
6926
  :hints (("goal" :in-theory (e/d (loghead*-better ash* LRDT
6897
6927
                                                   zp
6898
 
                                                   ) 
 
6928
                                                   )
6899
6929
                                  ( ;LOGHEAD-OF-*-EXPT-ALT
6900
6930
                                   )))))
6901
6931
 
6983
7013
                  (or (equal x (expt 2 n))
6984
7014
                      (equal x 0))))
6985
7015
  :rule-classes nil
6986
 
  :hints (("goal" 
 
7016
  :hints (("goal"
6987
7017
           :induct (loghead n x)
6988
7018
           :expand (logcdr x)
6989
7019
           :in-theory (e/d (lrdt expt ;logcdr
7006
7036
(local (in-theory (disable UNSIGNED-BYTE-P-OF-LOGCDR))) ;this doesn't play well with LRDT
7007
7037
 
7008
7038
(defthm equal-loghead-lognot-all-ones
7009
 
  (implies (and (integerp n)    
 
7039
  (implies (and (integerp n)
7010
7040
                (integerp x)
7011
7041
                (<= 0 n))
7012
7042
           (equal (equal (loghead n (lognot x)) (1- (expt 2 n)))
7049
7079
  (implies (and (integerp n)
7050
7080
                (<= 0 n)
7051
7081
                (unsigned-byte-p n x))
7052
 
           (equal (loghead n (- (logext n x))) 
 
7082
           (equal (loghead n (- (logext n x)))
7053
7083
                  (loghead n (- x))))
7054
7084
  :hints (("goal" :in-theory (e/d (LRDT open-logcons) (LOGEXTU-AS-LOGHEAD ;forcing
7055
7085
                                                       LOGHEAD-OF-MINUS
7062
7092
                (<= 0 n))
7063
7093
           (equal (loghead n (logxor x y))
7064
7094
                  (logxor (loghead n x) (loghead n y))))
7065
 
  :hints (("goal" :in-theory (enable LRDT)))) 
 
7095
  :hints (("goal" :in-theory (enable LRDT))))
7066
7096
 
7067
7097
(defthm loghead-lognot-loghead
7068
7098
  (implies (and (integerp n1)
7072
7102
                (<= 0 n1))
7073
7103
           (equal (loghead n1 (lognot (loghead n2 x)))
7074
7104
                  (loghead n1 (lognot x))))
7075
 
  :hints (("goal" 
7076
 
           :in-theory (e/d (LRDT logendp) (LOGHEAD-OF-MINUS 
 
7105
  :hints (("goal"
 
7106
           :in-theory (e/d (LRDT logendp) (LOGHEAD-OF-MINUS
7077
7107
                                           )))))
7078
7108
           ;:induct (sub1-sub1-logcdr-induction n2 n1 x))))
7079
7109
 
7125
7155
  :hints (("Goal" :use (:instance loghead-logapp (size (ifix size)))
7126
7156
           :in-theory (disable loghead-logapp))))
7127
7157
 
7128
 
(in-theory (disable loghead-logapp)) 
 
7158
(in-theory (disable loghead-logapp))
7129
7159
 
7130
7160
(defthmd logtail-loghead-better
7131
7161
  (equal (logtail size1 (loghead size i))
7134
7164
  :hints (("Goal" :use (:instance logtail-loghead)
7135
7165
           :in-theory (disable logtail-loghead))))
7136
7166
 
7137
 
(in-theory (disable logtail-loghead)) 
 
7167
(in-theory (disable logtail-loghead))
7138
7168
 
7139
7169
(defthm loghead-logtail
7140
7170
  (equal (loghead i (logtail j x))
7160
7190
  :hints (("Goal" :use (:instance logtail-logapp)
7161
7191
           :in-theory (disable logtail-logapp))))
7162
7192
 
7163
 
(in-theory (disable logtail-logapp)) 
 
7193
(in-theory (disable logtail-logapp))
7164
7194
 
7165
7195
;move to logapp.lisp?
7166
7196
(defthm associativity-of-logapp-better
7174
7204
  :hints (("Goal" :use (:instance associativity-of-logapp)
7175
7205
           :in-theory (disable associativity-of-logapp))))
7176
7206
 
7177
 
(in-theory (disable associativity-of-logapp)) 
7178
 
  
 
7207
(in-theory (disable associativity-of-logapp))
 
7208
 
7179
7209
;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;
7180
7210
;; logtail
7181
7211
;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;
7187
7217
                (<= 0 n))
7188
7218
           (equal (logtail n (logior x y))
7189
7219
                  (logior (logtail n x) (logtail n y))))
7190
 
  :hints (("goal" 
 
7220
  :hints (("goal"
7191
7221
           :in-theory (disable logapp-logior)
7192
7222
           :use ((:instance logapp-logior
7193
7223
                            (w (loghead n x))
7202
7232
                (<= 0 n))
7203
7233
           (equal (logtail n (logand x y))
7204
7234
                  (logand (logtail n x) (logtail n y))))
7205
 
  :hints (("goal" 
 
7235
  :hints (("goal"
7206
7236
           :in-theory (disable logapp-logand)
7207
7237
           :use ((:instance logapp-logand
7208
7238
                            (w (loghead n x))
7216
7246
                (<= 0 n))
7217
7247
           (equal (logtail n (lognot x))
7218
7248
                  (lognot (logtail n x))))
7219
 
  :hints (("goal" 
 
7249
  :hints (("goal"
7220
7250
           :in-theory (disable logapp-lognot)
7221
7251
           :use ((:instance logapp-lognot
7222
7252
                            (x (loghead n x))
7223
7253
                            (y (logtail n x)))))))
7224
7254
 
7225
7255
(defthm logcar-lognot
7226
 
  (equal (logcar (lognot a)) 
 
7256
  (equal (logcar (lognot a))
7227
7257
         (b-not (logcar a)))
7228
7258
  :hints (("Goal" :in-theory (enable  logops-recursive-definitions-theory))))
7229
7259
 
7236
7266
(defthm logcar-logior
7237
7267
  (equal (logcar (logior a b))
7238
7268
         (b-ior (logcar a) (logcar b)))
7239
 
  :hints (("goal" 
 
7269
  :hints (("goal"
7240
7270
           :in-theory (enable logior logops-recursive-definitions-theory))))
7241
7271
 
7242
7272
;move 3rd hyp to conclusion?
7244
7274
  (implies (and (integerp n)
7245
7275
                (integerp x)
7246
7276
                (< 0 n))
7247
 
           (equal (logcar (logext n x)) 
 
7277
           (equal (logcar (logext n x))
7248
7278
                  (logcar x)))
7249
7279
  :hints (("goal" :in-theory (enable logext logbitp oddp; evenp
7250
7280
                                     ))))
7255
7285
                (integerp n)
7256
7286
        ;        (integerp x)
7257
7287
                )
7258
 
           (equal (logcar (ash x n)) 
 
7288
           (equal (logcar (ash x n))
7259
7289
                  (logbit (- n) x)))
7260
7290
  :hints (("goal" :in-theory (e/d (LRDT logbit) (logtail* ;was forcing
7261
7291
                                                 )))))
7262
7292
 
7263
7293
(defthm logcar-ash-both
7264
7294
  (implies (integerp n)
7265
 
           (equal (logcar (ash x n)) 
 
7295
           (equal (logcar (ash x n))
7266
7296
                  (if (< 0 n)
7267
7297
                      0
7268
7298
                    (logbit (- n) x))))
7311
7341
                t)))
7312
7342
  :hints (("goal"
7313
7343
           :cases ((evenp x))
7314
 
           :in-theory (e/d (logcdr 
7315
 
                            signed-byte-p 
 
7344
           :in-theory (e/d (logcdr
 
7345
                            signed-byte-p
7316
7346
                            expt
7317
 
                            ) 
 
7347
                            )
7318
7348
                           (expt-2-cruncher
7319
7349
                            FLOOR-OF-SHIFT-RIGHT-2
7320
7350
                            )))))
7332
7362
  (implies (integerp x)
7333
7363
           (equal (logcdr (* 4 x))
7334
7364
                  (* 2 x)))
7335
 
  :hints (("goal" :in-theory (enable logcdr))))  
 
7365
  :hints (("goal" :in-theory (enable logcdr))))
7336
7366
 
7337
7367
 
7338
7368
(defthm logcdr-logcar
7348
7378
(defthm logcdr-+1
7349
7379
  (implies (integerp x)
7350
7380
           (and (implies (equal (logcar x) 0)
7351
 
                         (equal (logcdr (+ 1 x)) 
 
7381
                         (equal (logcdr (+ 1 x))
7352
7382
                                (logcdr x)))
7353
7383
                (implies (equal (logcar x) 1)
7354
 
                         (equal (logcdr (+ 1 x)) 
 
7384
                         (equal (logcdr (+ 1 x))
7355
7385
                                (+ 1 (logcdr x))))
7356
7386
                (implies (and (integerp y)
7357
7387
                              (equal (logcar x) 1))
7358
 
                         (equal (logcdr (+ 1 x y)) 
 
7388
                         (equal (logcdr (+ 1 x y))
7359
7389
                                (+ 1 (logcdr x) (logcdr y))))
7360
7390
                (implies (and (integerp y)
7361
7391
                              (equal (logcar x) 1))
7362
 
                         (equal (logcdr (+ 1 y x)) 
 
7392
                         (equal (logcdr (+ 1 y x))
7363
7393
                                (+ 1 (logcdr x) (logcdr y))))))
7364
7394
  :hints (("Goal" :in-theory (enable logcons))))
7365
7395
 
7366
7396
(defthm logcdr-+3
7367
7397
  (and (implies (and (integerp x)
7368
7398
                     (equal (logcar x) 0))
7369
 
                (equal (logcdr (+ 3 x)) 
 
7399
                (equal (logcdr (+ 3 x))
7370
7400
                       (+ 1 (logcdr x))))
7371
7401
       (implies (and (integerp x)
7372
7402
                     (equal (logcar x) 1))
7373
 
                (equal (logcdr (+ 3 x)) 
 
7403
                (equal (logcdr (+ 3 x))
7374
7404
                       (+ 2 (logcdr x)))))
7375
7405
  :hints (("goal" :in-theory (enable logcar logcdr))))
7376
7406
 
7384
7414
  (implies (and (integerp n)
7385
7415
                ;(integerp x)
7386
7416
                (< 1 n))
7387
 
           (equal (logcdr (logext n x)) 
 
7417
           (equal (logcdr (logext n x))
7388
7418
                  (logext (1- n) (logcdr x))))
7389
7419
  :hints (("goal" :in-theory (enable LRDT))))
7390
 
           
 
7420
 
7391
7421
(defthm logcdr-bitop
7392
7422
  (and (equal (logcdr (b-and x y)) 0)
7393
7423
       (equal (logcdr (b-ior x y)) 0)
7414
7444
;;                   (+ (logcdr a)
7415
7445
;;                      (logcdr b)
7416
7446
;;                      (b-maj (logcar a) (logcar b) 0)))))
7417
 
  
 
7447
 
7418
7448
;; (defthm logcdr-+-carry-bit
7419
7449
;;   (implies (and (integerp a)
7420
7450
;;                 (integerp b)
7427
7457
(in-theory (disable logtail))
7428
7458
 
7429
7459
(defthm logtail-when-i-is-zero
7430
 
  (equal (logtail pos 0) 
7431
 
         0) 
 
7460
  (equal (logtail pos 0)
 
7461
         0)
7432
7462
  :hints (("Goal" :in-theory (enable logtail))))
7433
7463
 
7434
 
(in-theory (disable logtail-size-0)) 
 
7464
(in-theory (disable logtail-size-0))
7435
7465
 
7436
7466
(defthm logtail-when-i-is-not-an-integerp
7437
7467
  (implies (not (integerp i))
7438
 
           (equal (logtail pos i) 
 
7468
           (equal (logtail pos i)
7439
7469
                  0))
7440
7470
  :hints
7441
7471
  (("Goal" :in-theory (enable logtail))))
7442
7472
 
7443
7473
(defthm logtail-when-pos-is-not-positive
7444
7474
  (implies (<= pos 0)
7445
 
           (equal (logtail pos i) 
 
7475
           (equal (logtail pos i)
7446
7476
                  (ifix i)
7447
7477
                  ))
7448
7478
  :hints (("Goal" :in-theory (enable logtail))))
7456
7486
 
7457
7487
(defthm logtail-when-pos-is-not-an-integerp
7458
7488
  (implies (not (integerp pos))
7459
 
           (equal (logtail pos i) 
 
7489
           (equal (logtail pos i)
7460
7490
                  (ifix i)
7461
7491
                  ))
7462
7492
  :hints (("Goal" :in-theory (enable logtail))))
7506
7536
 
7507
7537
;the ifix was causing case splits
7508
7538
(defthm logtail-0-i-better
7509
 
  (equal (logtail 0 i) 
 
7539
  (equal (logtail 0 i)
7510
7540
         (ifix i)))
7511
7541
 
7512
7542
(defthmd logtail-0-i-better-no-split
7513
7543
  (implies (integerp i)
7514
 
           (equal (logtail 0 i) 
 
7544
           (equal (logtail 0 i)
7515
7545
                  i)))
7516
7546
 
7517
7547
(in-theory (disable logtail-0-i))
7567
7597
                (integerp n)
7568
7598
                (<= 0 n))
7569
7599
           (<= (lshu n x s) bound))
7570
 
  :hints (("goal" :use (:instance unsigned-byte-p-lshu 
 
7600
  :hints (("goal" :use (:instance unsigned-byte-p-lshu
7571
7601
                                  (size n) (size1 n)
7572
7602
                                  (i x) (cnt s))
7573
7603
           :in-theory (disable unsigned-byte-p-lshu)))
7587
7617
           (< (* x d) c))
7588
7618
  :hints (("goal" :cases ((<= (* x d) (* a x)))
7589
7619
           :in-theory (enable *-PRESERVES->=-FOR-NONNEGATIVES))))
7590
 
          
 
7620
 
7591
7621
(defthmd <-expt-bridge
7592
7622
  (implies (and (< (* V (EXPT 2 S)) (EXPT 2 N1))
7593
7623
                (<= 0 v)
7613
7643
  :hints (("Goal" :do-not-induct t
7614
7644
           :in-theory (e/d (lshu
7615
7645
                            <-expt-bridge
7616
 
                            UNSIGNED-BYTE-P 
 
7646
                            UNSIGNED-BYTE-P
7617
7647
                            ASH-BOUND4
7618
7648
                            ASH-BOUND3a)
7619
7649
                           ()))))
7624
7654
                (integerp n2)
7625
7655
                (<= 0 n2)
7626
7656
                (integerp s)
7627
 
                (<= 0 n1)    
 
7657
                (<= 0 n1)
7628
7658
                (< s n1)
7629
7659
                (integerp v)
7630
7660
                (<= 0 v)
7631
7661
                )
7632
7662
           (<= (lshu n2 v s) (1- (expt 2 n1))))
7633
7663
  :rule-classes nil
7634
 
  :hints (("goal" :use (lshu-bound-2) 
 
7664
  :hints (("goal" :use (lshu-bound-2)
7635
7665
           :in-theory (e/d (UNSIGNED-BYTE-P)
7636
7666
                           (  lshu-bound-2 EXPT-MINUS)))))
7637
7667
 
7681
7711
;Returns a term representing the conjunctionof TERM1 and TERM2.
7682
7712
(defund make-conjunction (term1 term2)
7683
7713
  (declare (type t term1 term2))
7684
 
  (if (equal term1 ''t)  
 
7714
  (if (equal term1 ''t)
7685
7715
      term2 ;conjoining something with "true" has no effect
7686
7716
    (if (equal term2 ''t)
7687
7717
        term1 ;conjoining something with "true" has no effect
7751
7781
  (if (not (consp term))
7752
7782
      `(integerp ,term)
7753
7783
    (case (car term)
7754
 
          (binary-+ (make-conjunction 
 
7784
          (binary-+ (make-conjunction
7755
7785
                     (hyp-for-addends n (cadr term))
7756
7786
                     (hyp-for-addends n (caddr term))))
7757
7787
          (unary-- (hyp-for-addend n (cadr term)))
7799
7829
                           (loghead-sum-eval (strip-logheads-from-sum n term) alist))))
7800
7830
  :hints (("Goal" :in-theory (e/d (make-conjunction
7801
7831
                                     strip-loghead-from-term
7802
 
                                     CALL-TO-LOGHEAD-WITH-N-OR-GREATER-SIZE) 
 
7832
                                     CALL-TO-LOGHEAD-WITH-N-OR-GREATER-SIZE)
7803
7833
                                  (UNSIGNED-BYTE-P-LOGHEAD-FORWARD-CHAINING ;i think this prevents specious simplification
7804
7834
                                   ))
7805
7835
           :do-not '(generalize eliminate-destructors))))
7836
7866
; rules that simplify max and min expressions, in case we later disable min and max.
7837
7867
 
7838
7868
(defthm equal-max-x-x
7839
 
  (equal (max x x) 
 
7869
  (equal (max x x)
7840
7870
         x))
7841
7871
 
7842
7872
(defthm max-linear
7857
7887
   (equal
7858
7888
    (equal (max a b) b)
7859
7889
    (<= a b)))))
7860
 
   
 
7890
 
7861
7891
(defthm max-constants
7862
7892
  (implies
7863
7893
   (and
7864
7894
    (syntaxp (quotep x))
7865
7895
    (syntaxp (quotep y)))
7866
 
   (equal 
 
7896
   (equal
7867
7897
    (max x (max y z))
7868
7898
    (max (max x y) z))))
7869
7899
 
7950
7980
 
7951
7981
(defthm equal-a-min-a
7952
7982
  (implies
7953
 
   (and 
 
7983
   (and
7954
7984
    (rationalp a)
7955
7985
    (rationalp b))
7956
7986
   (and
8022
8052
   (and
8023
8053
    (syntaxp (quotep x))
8024
8054
    (syntaxp (quotep y)))
8025
 
   (equal 
 
8055
   (equal
8026
8056
    (min x (min y z))
8027
8057
    (min (min x y) z))))
8028
8058
 
8049
8079
                              simplify-bit-functions))))
8050
8080
 
8051
8081
(defthm logxor-lognot-one
8052
 
  (implies (and (integerp a) 
 
8082
  (implies (and (integerp a)
8053
8083
                (integerp b))
8054
8084
           (equal (logxor (lognot a) b)
8055
8085
                  (lognot (logxor a b)))))
8073
8103
                                     LOGAND-NEG
8074
8104
                                     ))))
8075
8105
 
8076
 
(defthm integerp-logand 
 
8106
(defthm integerp-logand
8077
8107
  (integerp (logand x y)))
8078
8108
 
8079
 
(defthm integerp-logxor 
 
8109
(defthm integerp-logxor
8080
8110
  (integerp (logxor x y)))
8081
8111
 
8082
8112
(defthm integerp-logior
8085
8115
(defthm integerp-logext
8086
8116
  (integerp (logext x y)))
8087
8117
 
8088
 
(defthm rationalp-logand 
 
8118
(defthm rationalp-logand
8089
8119
  (rationalp (logand x y)))
8090
8120
 
8091
 
(defthm rationalp-logxor 
 
8121
(defthm rationalp-logxor
8092
8122
  (rationalp (logxor x y)))
8093
8123
 
8094
8124
(defthm rationalp-logior
8104
8134
;;     (< 0 n) ;; extraneous
8105
8135
;;     (integerp n) ;; extraneous
8106
8136
;;     (integerp x)  ;; extraneous
8107
 
;;     (integerp m) 
 
8137
;;     (integerp m)
8108
8138
;;     (<= n m))
8109
8139
;;    (not (logbitp m x)))
8110
8140
;;   :hints (("Goal"
8118
8148
           (not (logbitp m x)))
8119
8149
  :otf-flg t
8120
8150
  :hints (("Goal" :in-theory (e/d (ifix ;LOGBITP-WITH-NON-INTEGER ;UNSIGNED-BYTE-p
8121
 
                                        ) 
 
8151
                                        )
8122
8152
                                  (LOGBITP-N-UNSIGNED-BYTE-P-N
8123
8153
                                   OPEN-LOGCONS))
8124
8154
           :use (:instance LOGBITP-N-UNSIGNED-BYTE-P-N (n m)))))
8203
8233
;;            :do-not '(generalize eliminate-destructors)
8204
8234
;;            )))
8205
8235
 
8206
 
 
 
8236
 
8207
8237
 
8208
8238
 
8209
8239
 
8215
8245
           (equal (logext n (+ x (expt 2 n)))
8216
8246
                  (logext n x)))
8217
8247
  :hints (("goal" :in-theory (e/d (LRDT
8218
 
                                     open-logcons) 
8219
 
                                  (LOGCONS-OF-0 
 
8248
                                     open-logcons)
 
8249
                                  (LOGCONS-OF-0
8220
8250
                                   )))))
8221
8251
 
8222
 
(local (in-theory (enable open-logcons))) 
 
8252
(local (in-theory (enable open-logcons)))
8223
8253
 
8224
8254
(local (in-theory (disable logcons-of-0)))
8225
8255
 
8278
8308
                            UNSIGNED-BYTE-P
8279
8309
                            INTEGER-RANGE-P
8280
8310
                            ;logext
8281
 
                            ) 
 
8311
                            )
8282
8312
                           (
8283
8313
;                            expt2*
8284
8314
                            SIGN-LOGEXT-AS-LOGBITP)))))
8298
8328
                            UNSIGNED-BYTE-P
8299
8329
                            INTEGER-RANGE-P
8300
8330
                            ;logext
8301
 
                            ) 
 
8331
                            )
8302
8332
                           (SIGN-LOGEXT-AS-LOGBITP)))))
8303
 
 
 
8333
 
8304
8334
 
8305
8335
;improve
8306
8336
;go the other way too?
8423
8453
                (<= 0 SIZE1)
8424
8454
                )
8425
8455
           (equal (unsigned-byte-p size (logapp size1 i j))
8426
 
                  (and (integerp size) 
 
8456
                  (and (integerp size)
8427
8457
                       (<= 0 size)
8428
8458
                       (if (integerp j)
8429
8459
                           (unsigned-byte-p (- size size1) j)
8434
8464
           :in-theory (e/d (FALSIFY-UNSIGNED-BYTE-P)
8435
8465
                           ( unsigned-byte-p-logapp)))))
8436
8466
 
8437
 
(in-theory (disable unsigned-byte-p-logapp)) 
 
8467
(in-theory (disable unsigned-byte-p-logapp))
8438
8468
 
8439
8469
(defthm ash-<=-to-sbp
8440
8470
  (implies (and (signed-byte-p (- 32 N) V)
8445
8475
                (<= -2147483648 (ASH V N))))
8446
8476
  :hints (("goal"
8447
8477
 
8448
 
           :in-theory (disable ASH-AS-LOGTAIL 
 
8478
           :in-theory (disable ASH-AS-LOGTAIL
8449
8479
                               signed-byte-p-ash
8450
8480
                               )
8451
8481
           :use ((:instance signed-byte-p-ash (x v) (n 32) (m n))))))
8663
8693
;think more about how we want to handle claims about bit vectors of length 1.  do we prefer to normalize all the claims to claims about 0, or do we
8664
8694
;want to leave  (equal (logcar x) 1) to get ACL2 to substitute 1 for (logcar x)? -ews
8665
8695
;eric saw something similar to this at AMD.
8666
 
(defthm equal-logcar-1 
8667
 
  (equal (equal (logcar x) 1) 
8668
 
         (not (equal (logcar x) 0))) 
 
8696
(defthm equal-logcar-1
 
8697
  (equal (equal (logcar x) 1)
 
8698
         (not (equal (logcar x) 0)))
8669
8699
  :hints (("goal" :in-theory (enable))))
8670
8700
 
8671
8701
 
8706
8736
                (< 0 n))
8707
8737
           (<= (logext n x) x))
8708
8738
  :rule-classes :linear
8709
 
  :hints (("goal" :in-theory (e/d (SIGNED-BYTE-P) (logext-identity 
 
8739
  :hints (("goal" :in-theory (e/d (SIGNED-BYTE-P) (logext-identity
8710
8740
                                                   logext-does-nothing-rewrite
8711
8741
                                                   signed-byte-p-logext
8712
8742
                                                   SIGNED-BYTE-P-OF-LOGEXT
8758
8788
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
8759
8789
           :in-theory (enable logapp))))
8760
8790
 
8761
 
(in-theory (disable logcar-logapp)) 
 
8791
(in-theory (disable logcar-logapp))
8762
8792
 
8763
8793
(defthm logbitp-logapp-better
8764
8794
  (equal (logbitp pos (logapp size i j))
8773
8803
(defthm logext-of-logext-same
8774
8804
  (equal (logext size (logext size i))
8775
8805
         (logext size i))
8776
 
  :hints (("Goal" :in-theory (e/d (logext) 
 
8806
  :hints (("Goal" :in-theory (e/d (logext)
8777
8807
                                  (EQUAL-LOGAPP-X-Y-Z
8778
 
                                   EQUAL-LOGAPP-X-Y-Z-CONSTANTS                                   
 
8808
                                   EQUAL-LOGAPP-X-Y-Z-CONSTANTS
8779
8809
                                   ;;LOGHEAD-LOGAPP
8780
8810
                                   )))))
8781
8811
 
8782
8812
(defthm logext-+-logext-better-alt
8783
8813
  (equal (logext size (+ (logext size j) i))
8784
8814
         (logext size (+ (ifix j) i)))
8785
 
  :hints (("Goal" :use (:instance  logext-+-logext-better) 
 
8815
  :hints (("Goal" :use (:instance  logext-+-logext-better)
8786
8816
           :in-theory (disable  logext-+-logext-better))))
8787
8817
 
8788
8818
(defthm logbitp-of-product-with-2
8803
8833
                  )))
8804
8834
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
8805
8835
           :in-theory (e/d (FLOOR-NORMALIZES-TO-HAVE-J-BE-1 EXPONENTS-ADD-UNRESTRICTED logbitp) ()))))
8806
 
        
 
8836
 
8807
8837
(defthm logbitp-of-*-expt-2-special
8808
8838
  (implies (and (integerp x)
8809
8839
                (<= 0 n)
8844
8874
;have no affect on subsequent proofs.
8845
8875
 
8846
8876
;stuff enabled or added by the @logops book:
8847
 
(in-theory (enable 
 
8877
(in-theory (enable
8848
8878
;            (:EXECUTABLE-COUNTERPART IMMEDIATE-FORCE-MODEP) ;trying without this...
8849
8879
;            (:INDUCTION EXPT) ;trying without this
8850
8880
            ))
8852
8882
 
8853
8883
;stuff disabled by the @logops book:
8854
8884
;bzo remove stuff from this!
8855
 
(in-theory (disable 
 
8885
(in-theory (disable
8856
8886
            (:FORWARD-CHAINING INTEGERP-*-MEANS)
8857
8887
            (:DEFINITION LOGENDP)
8858
8888
            (:DEFINITION B-MAJ)
8922
8952
            (:REWRITE UNSIGNED-BYTE-P-+-EASY)
8923
8953
            (:FORWARD-CHAINING UNSIGNED-BYTE-P-+-EASY-FC)
8924
8954
            (:REWRITE UNSIGNED-BYTE-P-+-BRIDGE2)
8925
 
 ;           (:REWRITE SIGNED-BYTE-P-+)                          
 
8955
 ;           (:REWRITE SIGNED-BYTE-P-+)
8926
8956
;            (:REWRITE SIGNED-BYTE-P-UNSIGNED-BYTE-P)
8927
8957
;            (:REWRITE UNSIGNED-BYTE-P-SUBTYPE)
8928
8958
;            (:REWRITE SIGNED-BYTE-P-SUBTYPE)
9095
9125
 
9096
9126
 
9097
9127
 
9098
 
;;; The true-listp guard to nth and update-nth is used elswhere, 
9099
 
;;; There are two versions, which are identical except that our 
 
9128
;;; The true-listp guard to nth and update-nth is used elswhere,
 
9129
;;; There are two versions, which are identical except that our
9100
9130
;;; guard is that the index is in the list, not that the list is true.
9101
9131
 
9102
9132
 
9163
9193
   (and
9164
9194
    (signed-byte-p 32 x)
9165
9195
    (signed-byte-p 32 y))
9166
 
   (and 
 
9196
   (and
9167
9197
    (<= (- (expt 2 31)) (LOGIOR x y))
9168
9198
    (<= (logior x y) (1- (expt 2 31)))))
9169
9199
  :hints (("goal" :in-theory (disable  signed-byte-p-logops)
9175
9205
   (and
9176
9206
    (signed-byte-p 32 x)
9177
9207
    (signed-byte-p 32 y))
9178
 
   (and 
 
9208
   (and
9179
9209
    (<= (- (expt 2 31)) (LOGXOR x y))
9180
9210
    (<= (logxor x y) (1- (expt 2 31)))))
9181
9211
  :hints (("goal" :in-theory (disable  signed-byte-p-logops)
9186
9216
(defthm logxor-bit-bound
9187
9217
  (implies
9188
9218
    (and (unsigned-byte-p 1 x) (unsigned-byte-p 1 y))
9189
 
  (and 
 
9219
  (and
9190
9220
   (<= 0 (logxor x y))
9191
9221
   (<= (logxor x y) 1)))
9192
9222
  :hints (("goal" :in-theory (disable UNSIGNED-BYTE-P-LOGXOR)
9215
9245
           (<= (LOGAND X Y) 2147483647)))
9216
9246
 
9217
9247
 
9218
 
;The out rules in the next series may not handle all these cases, 
 
9248
;The out rules in the next series may not handle all these cases,
9219
9249
;so it has been left it in this file, but commented out
9220
9250
 
9221
9251
 
9293
9323
 
9294
9324
;; BY: This book is rather fragile.  For example, it seems previously to have
9295
9325
;;     been certified with EXPT enabled, but it is currently disabled, so I
9296
 
;;     had to deal with that throughout. 
 
9326
;;     had to deal with that throughout.
9297
9327
 
9298
9328
 
9299
9329
;drop?
9327
9357
           ;:do-not '(generalize eliminate-destructors)
9328
9358
           :in-theory (enable LOGOPS-RECURSIVE-DEFINITIONS-THEORY b-and b-xor open-logcons))))
9329
9359
 
9330
 
;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;           
 
9360
;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;
9331
9361
;; signed-byte-p, unsigned-byte-p
9332
9362
;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;
9333
9363
 
9384
9414
;trying without this...
9385
9415
;; (defthm loghead-24-16-bridge
9386
9416
;;   (implies (unsigned-byte-p 16 x)
9387
 
;;            (equal (loghead 24 x) 
 
9417
;;            (equal (loghead 24 x)
9388
9418
;;                   x)))
9389
9419
 
9390
9420
;Prove a bound on (loghead n x) perhaps?
9473
9503
  (implies (and (integerp x)
9474
9504
                (integerp y))
9475
9505
           (and (equal (logior z (logxor x y))
9476
 
                       (logior z 
 
9506
                       (logior z
9477
9507
                               (logior (logand x (lognot y))
9478
9508
                                       (logand (lognot x) y))
9479
9509
                               ))
9510
9540
 
9511
9541
(in-theory (enable ash-as-logtail))  ;do we want this enabled or not?
9512
9542
 
9513
 
;; added this one. 
 
9543
;; added this one.
9514
9544
;drop?
9515
9545
(defthmd *ark*-fold-in-two-crock
9516
9546
  (implies (and (acl2-numberp x)
9628
9658
  (implies (and (integerp n1)
9629
9659
                (integerp n2)
9630
9660
                (integerp x)
9631
 
                (<= 0 n1) 
 
9661
                (<= 0 n1)
9632
9662
                (< n2 0))
9633
9663
           (equal (ash (loghead n1 x) n2)
9634
9664
                  (if (<= n1 (- n2))
9640
9670
;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;
9641
9671
;; floor
9642
9672
;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;-;
9643
 
    
 
9673
 
9644
9674
(in-theory (enable floor-*-1/2-expt-2))
9645
9675
 
9646
9676
(in-theory (enable sign-+-logext-logext-as-logbitp))
9701
9731
                    )))
9702
9732
  :hints (("Goal" :use (:instance logextu-as-loghead))))
9703
9733
 
9704
 
;bzo move, 
 
9734
;bzo move,
9705
9735
;generalize: rewrite a claim about signed-byte-p of a constant to a claim about the index.
9706
9736
(defthm signed-byte-p-of-1
9707
9737
  (equal (signed-byte-p n 1)
9709
9739
              (< 1 n)))
9710
9740
  :hints (("Goal" :in-theory (enable signed-byte-p))))
9711
9741
 
9712
 
;bzo we could need a rule like this for subtracting 2, subtracting 3, etc. 
 
9742
;bzo we could need a rule like this for subtracting 2, subtracting 3, etc.
9713
9743
;(and the rules for those cases would get grosser) I bet that subtracting 1
9714
 
;covers most of the cases we'll see in practice.this rule gives us a little 
9715
 
;flexibility around the ends of the unsigned-byte-p range without just 
 
9744
;covers most of the cases we'll see in practice.this rule gives us a little
 
9745
;flexibility around the ends of the unsigned-byte-p range without just
9716
9746
;opening up to arithmetic
9717
9747
(defthm unsigned-byte-p-of-one-less-than-x
9718
9748
  (implies (syntaxp (not (quotep x))) ;prevents loops (i think because acl2 unifies say, the constant 42 with the pattern (+ -1 x)
9757
9787
;; (defthm plus-of-logapp-suck-in
9758
9788
;;   (implies (unsigned-byte-p 16 (+ x y))
9759
9789
;;            (equal (+ x (logapp 16 y j))
9760
 
;;                   (if (unsigned-byte-p 16 y) 
 
9790
;;                   (if (unsigned-byte-p 16 y)
9761
9791
;;                       (logapp 16 (+ x y) j)
9762
9792
;;                     (+ (loghead 16 y) (- y) (logapp 16 (+ x y) j)) ;this seems strange
9763
9793
;;                     )))
9769
9799
(defthm plus-of-logapp-suck-in
9770
9800
  (implies (unsigned-byte-p n (+ x y))
9771
9801
           (equal (+ x (logapp n y j))
9772
 
                  (if (unsigned-byte-p n y) 
 
9802
                  (if (unsigned-byte-p n y)
9773
9803
                      (logapp n (+ x y) j)
9774
9804
                    (+ (loghead n y) (- y) (logapp n (+ x y) j)) ;this seems strange
9775
9805
                    )))
9778
9808
(defthm plus-of-logapp-suck-in-alt
9779
9809
  (implies (unsigned-byte-p n (+ x z y))
9780
9810
           (equal (+ x z (logapp n y j))
9781
 
                  (if (unsigned-byte-p n y) 
 
9811
                  (if (unsigned-byte-p n y)
9782
9812
                      (logapp n (+ x z y) j)
9783
9813
                    (+ (loghead n y) (- y) (logapp n (+ x z y) j)) ;this seems strange
9784
9814
                    )))
9792
9822
           (equal (+ (- (* 1/2 x))
9793
9823
                     (- (* 1/2 x))
9794
9824
                     y)
9795
 
                  (+ (- x) 
 
9825
                  (+ (- x)
9796
9826
                     y))))
9797
9827
 
9798
9828
(defthm logtail-of-loghead-becomes-logbit
9802
9832
                )
9803
9833
           (equal (logtail m (loghead n x))
9804
9834
                  (logbit m x)))
9805
 
  :hints (("Goal" :in-theory (e/d (logtail-loghead-better) 
 
9835
  :hints (("Goal" :in-theory (e/d (logtail-loghead-better)
9806
9836
                                  (loghead-logtail)))))
9807
9837
 
9808
9838
(defthm loghead-split
9825
9855
                           (equal (loghead size i)
9826
9856
                                  (loghead size i2))))))
9827
9857
  :hints (("Goal" :in-theory (enable logapp-equal-logapp-rewrite))))
9828
 
                    
 
9858
 
9829
9859
 
9830
9860
(defthmd loghead-split-special
9831
9861
  (implies (and (syntaxp (equal x 'x))
9835
9865
           (equal (loghead n x)
9836
9866
                  (logapp (+ -1 n) (loghead (+ -1 n) x) (logbit (+ -1 n) x))))
9837
9867
 :hints (("Goal" :use (:instance  loghead-split))))
9838
 
        
 
9868
 
9839
9869
;kill the 16 version
9840
9870
;keep this disabled.
9841
9871
(defthmd equal-of-logheads-split
9897
9927
                (equal (ash z n) z) ; bzo ;figure out what this should simplify to and prove a rule, then rephrase this rule
9898
9928
                )))
9899
9929
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
9900
 
           :in-theory (e/d (floor-normalizes-to-have-j-be-1 
9901
 
                            logtail 
9902
 
                            loghead 
9903
 
                            ash) 
 
9930
           :in-theory (e/d (floor-normalizes-to-have-j-be-1
 
9931
                            logtail
 
9932
                            loghead
 
9933
                            ash)
9904
9934
                           ( ;(:type-prescription floor)
9905
9935
                            (:type-prescription floor)
9906
9936
                            )))))
9957
9987
;;                             oddp
9958
9988
;;                             evenp
9959
9989
;;                             ifix
9960
 
;;                             ) 
 
9990
;;                             )
9961
9991
;;                            (loghead-of-prod-lemma
9962
9992
;;                             mod-cancel
9963
9993
;;                             evenp-collapse
9970
10000
;;                   (loghead n (* i (ifix j)))))
9971
10001
;;   :hints (("Goal" ; :use (:instance  loghead-of-prod-lemma (x (logapp 31 a -1)) (y k))
9972
10002
;;            :in-theory (e/d (logext
9973
 
;;                             loghead logapp 
 
10003
;;                             loghead logapp
9974
10004
;;                             imod
9975
10005
;;                             logbitp
9976
10006
;;                             oddp
9979
10009
;;                             mod-stretch-base
9980
10010
;;                             mod-stretch-base-2
9981
10011
;;                             EXPONENTS-ADD-UNRESTRICTED
9982
 
;;                             ) 
 
10012
;;                             )
9983
10013
;;                            (loghead-of-prod-lemma
9984
10014
;;                             mod-cancel
9985
10015
;;                             evenp-collapse
10005
10035
                (integerp x)
10006
10036
                (integerp m)
10007
10037
                (< 0 n)
10008
 
                
 
10038
 
10009
10039
                (< 0 (+ n m)))
10010
10040
           (equal (ash (logext n x) m)
10011
10041
                  (logext (+ n m)
10019
10049
                (integerp b))
10020
10050
           (equal (+ a (ASH b k))
10021
10051
                  (logapp k a b)))
10022
 
  :hints (("Goal" :in-theory (e/d (ASH-AS-LOGAPP) 
 
10052
  :hints (("Goal" :in-theory (e/d (ASH-AS-LOGAPP)
10023
10053
                                  (LOGAPP-0-PART-2-BETTER)))))
10024
10054
 
10025
10055
 
10053
10083
                      (and (equal b (logtail size x))
10054
10084
                           (< (loghead size a) (loghead size x))))))
10055
10085
  :hints (("Goal" ; :do-not '(generalize eliminate-destructors)
10056
 
           :in-theory (e/d (LOGAPP 
 
10086
           :in-theory (e/d (LOGAPP
10057
10087
                              imod ifloor
10058
 
                              LOGTAIL 
 
10088
                              LOGTAIL
10059
10089
                              mod-cancel
10060
 
                              loghead) 
 
10090
                              loghead)
10061
10091
                           ()))))
10062
10092
 
10063
10093
;bzo clean up rhs?
10102
10132
                    (+ -1 x))))
10103
10133
  :hints (("Goal" :in-theory (enable ash logcdr ifloor))))
10104
10134
 
10105
 
(in-theory (disable ash-logcdr-1)) 
 
10135
(in-theory (disable ash-logcdr-1))
10106
10136
 
10107
10137
(defthm logcdr-logapp
10108
10138
  (equal (logcdr (logapp size i j))
10159
10189
                                   INTEGER-RANGE-P
10160
10190
                                   logbitp
10161
10191
                                   EXPONENTS-ADD-UNRESTRICTED ;shouldn't be needed?
10162
 
                                   ) 
 
10192
                                   )
10163
10193
                                  (FLOOR-BY-TWICE-HACK)))))
10164
10194
 
10165
10195
;; (defthm usb-tighten
10169
10199
;;   :rule-classes ((:rewrite :backchain-limit-lst (0)))
10170
10200
;;   :hints (("Goal" :in-theory (e/d (unsigned-byte-p
10171
10201
;;                                      INTEGER-RANGE-P
10172
 
;;                                      logbitp) 
 
10202
;;                                      logbitp)
10173
10203
;;                                   (FLOOR-BY-TWICE-HACK)))))
10174
10204
 
10175
10205
;think more about this
10176
 
;looped! 
 
10206
;looped!
10177
10207
(defthmd loghead-when-know-top-bit
10178
10208
  (implies (and (equal (logbit m x) b) ;using m so that this will be sure to match
10179
10209
                (equal m (+ -1 n))
10262
10292
                  ))
10263
10293
  :hints (("Goal" :cases ((integerp y))
10264
10294
           :in-theory (e/d (mod)))))
10265
 
 
 
10295
 
10266
10296
;generalize to handle addends other than 1 with corresponding predicates (like "multiple of 4" than even)?
10267
10297
;prove without using elimination?
10268
10298
;bzo gen
10306
10336
           (equal (+ a (* j b))
10307
10337
                  (logapp (expo j) a b)))
10308
10338
  :hints (("Goal" :in-theory (e/d (ash ;POWER2P
10309
 
                                       ) 
 
10339
                                       )
10310
10340
                                  (FLOOR-BY-TWICE-HACK sum-with-shift-becomes-logapp
10311
10341
                                                       EXPO-COMPARISON-REWRITE-TO-BOUND
10312
10342
                                                       EXPO-COMPARISON-REWRITE-TO-BOUND-2))
10338
10368
                       (or (equal x (expt 2 (+ -1 n)))
10339
10369
                           (and (signed-byte-p n x)
10340
10370
                           (not (equal x (- (expt 2 (+ -1 n))))))))))
10341
 
  :hints (("Goal" :in-theory (enable signed-byte-p 
 
10371
  :hints (("Goal" :in-theory (enable signed-byte-p
10342
10372
                                     integer-range-p ;prove a rule for integer-range-p of (+ 1 x)
10343
10373
                                     ))))
10344
10374
 
10350
10380
           (equal (logbitp n (+ -1 x))
10351
10381
                  (not (logbitp n x))))
10352
10382
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
10353
 
           :in-theory (e/d (logbitp loghead ;floor 
 
10383
           :in-theory (e/d (logbitp loghead ;floor
10354
10384
                                    imod
10355
10385
    ;oddp evenp expt
10356
10386
                                    )
10375
10405
           (equal (logbitp n (+ -1 x))
10376
10406
                  (logbitp n x)))
10377
10407
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
10378
 
           :in-theory (e/d (logbitp loghead ;floor 
 
10408
           :in-theory (e/d (logbitp loghead ;floor
10379
10409
                                    imod
10380
10410
    ;oddp evenp expt
10381
10411
                                    )
10389
10419
                      (not (LOGBITP n X))
10390
10420
                    (LOGBITP n X))))
10391
10421
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
10392
 
           :in-theory (e/d (LOGBITP LOGHEAD ;floor 
 
10422
           :in-theory (e/d (LOGBITP LOGHEAD ;floor
10393
10423
                                    imod
10394
10424
;oddp EVENP expt
10395
10425
                                    )
10409
10439
                    (logtail n x))))
10410
10440
  :hints (("Goal" :in-theory (enable logtail
10411
10441
                                     loghead
10412
 
                                     UNSIGNED-BYTE-P 
 
10442
                                     UNSIGNED-BYTE-P
10413
10443
                                     INTEGER-RANGE-P ;prove a rule for integer-range-p of (+ 1 x)
10414
10444
                                     ))))
10415
10445
 
10427
10457
                    (+ -1 (logext 32 x)))))
10428
10458
  :otf-flg t
10429
10459
  :hints (("Goal" :in-theory (enable logext
10430
 
                                     UNSIGNED-BYTE-P 
 
10460
                                     UNSIGNED-BYTE-P
10431
10461
                                     INTEGER-RANGE-P ;prove a rule for integer-range-p of (+ 1 x)
10432
10462
                                     ))))
10433
10463
 
10489
10519
                (integerp c))
10490
10520
           (equal (LOGHEAD n (+ a (- (LOGEXT n b)) c))
10491
10521
                  (LOGHEAD n (+ a (- (ifix b)) c)))))
10492
 
           
 
10522
 
10493
10523
(defthm removeme7
10494
10524
  (implies (and (integerp k)
10495
10525
                (integerp a))
10497
10527
                  (loghead n (+ a (- (* k (ifix b))))))))
10498
10528
 
10499
10529
;;Note the overflow case:
10500
 
;;(truncate (- (expt 2 31)) -1) is equal to (expt2 31), which is not a signed-byte-p 32.                                  
 
10530
;;(truncate (- (expt 2 31)) -1) is equal to (expt2 31), which is not a signed-byte-p 32.
10501
10531
;bzo gen
10502
10532
(defthm signed-byte-p-of-truncate
10503
10533
  (implies (and (signed-byte-p 32 i)
10554
10584
 
10555
10585
(defthmd hackz
10556
10586
  (implies (natp i)
10557
 
           (equal (+ (/ a) 
 
10587
           (equal (+ (/ a)
10558
10588
                     (* I (/ a)))
10559
10589
                  (/ (+ 1 i) a))))
10560
10590
 
10561
10591
(defthm hackzz
10562
10592
  (implies (natp i)
10563
 
           (equal (+ (/ (+ 1 I)) 
 
10593
           (equal (+ (/ (+ 1 I))
10564
10594
                     (* I (/ (+ 1 I))))
10565
10595
                  1))
10566
10596
  :hints (("Goal" :in-theory (disable DISTRIBUTIVITY-ALT)
10645
10675
                    (logbitp n x))))
10646
10676
  :otf-flg t
10647
10677
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
10648
 
           :in-theory (e/d (LOGBITP LOGHEAD ;floor 
 
10678
           :in-theory (e/d (LOGBITP LOGHEAD ;floor
10649
10679
                                    mod-helper-2
10650
10680
                     ;oddp EVENP expt
10651
10681
                                    imod
10715
10745
(defthmd one-way
10716
10746
  (IMPLIES (AND (INTEGERP (* 1/2 (FLOOR X 16384)))
10717
10747
                (INTEGERP X))
10718
 
           (EQUAL (MOD X 16384) 
 
10748
           (EQUAL (MOD X 16384)
10719
10749
                  (MOD X 32768)))
10720
10750
  :hints (("Goal" :in-theory (disable evenp-collapse))))
10721
10751
 
10722
10752
 
10723
10753
;keep this disabled most of the time
10724
10754
(defthmd loghead-split-x-rewrite
10725
 
  (implies (and (syntaxp (equal x 'x)) 
 
10755
  (implies (and (syntaxp (equal x 'x))
10726
10756
                (integerp n)
10727
10757
                (< 0 n))
10728
10758
           (equal (loghead n x)
10732
10762
  :hints (("Goal" :by loghead-split)))
10733
10763
 
10734
10764
(defthmd loghead-split-y-rewrite
10735
 
  (implies (and (syntaxp (equal x 'y)) 
 
10765
  (implies (and (syntaxp (equal x 'y))
10736
10766
                (integerp n)
10737
10767
                (< 0 n))
10738
10768
           (equal (loghead n x)
10808
10838
                  (logtail (- n m) x)))
10809
10839
  :hints (("Goal" :use (:instance INTEGERP-EXPT (n (- n m)))
10810
10840
           :in-theory (e/d (logtail ifloor ifix FLOOR-NORMALIZES-TO-HAVE-J-BE-1
10811
 
                              EXPONENTS-ADD-UNRESTRICTED) 
 
10841
                              EXPONENTS-ADD-UNRESTRICTED)
10812
10842
                           (INTEGERP-EXPT)))))
10813
10843
 
10814
10844
(defthm logtail-shift-constant-version
10949
10979
 
10950
10980
 
10951
10981
(defthm loghead-of-difference-equal-0-rewrite-alt
10952
 
  (implies (and (integerp x) 
 
10982
  (implies (and (integerp x)
10953
10983
                (integerp y)
10954
10984
                (<= 0 n)
10955
10985
                (integerp n)
10957
10987
           (equal (equal 0 (loghead n (+ y (- x))))
10958
10988
                  (equal (loghead n x) (loghead n y))))
10959
10989
  :hints
10960
 
  (("Goal" :in-theory (e/d (;loghead 
 
10990
  (("Goal" :in-theory (e/d (;loghead
10961
10991
                            LOGHEAD-SUM-SPLIT-INTO-2-CASES
10962
10992
                            imod ifix) (mod-=-0)))))
10963
10993
 
10964
10994
 
10965
10995
(defthm loghead-of-difference-equal-0-rewrite
10966
 
  (implies (and (integerp x) 
 
10996
  (implies (and (integerp x)
10967
10997
                (integerp y)
10968
10998
                (<= 0 n)
10969
10999
                (integerp n)
10971
11001
           (equal (equal 0 (loghead n (+ (- x) y)))
10972
11002
                  (equal (loghead n x) (loghead n y))))
10973
11003
  :hints
10974
 
  (("Goal" :in-theory (e/d (;loghead 
 
11004
  (("Goal" :in-theory (e/d (;loghead
10975
11005
                            LOGHEAD-SUM-SPLIT-INTO-2-CASES
10976
 
                            imod ifix) (mod-=-0))))) 
 
11006
                            imod ifix) (mod-=-0)))))
10977
11007
 
10978
11008
;bzo harvest the stuff below
10979
11009
 
10996
11026
  (implies (and (unsigned-byte-p 16 x)
10997
11027
                (integerp n)
10998
11028
                (< 0 n))
10999
 
           (equal (ash x n) 
 
11029
           (equal (ash x n)
11000
11030
                  (ash (ash x (1- n)) 1)))
11001
11031
  :hints (("Goal" :in-theory (e/d (ash expt)(unsigned-byte-p)))))
11002
11032
 
11019
11049
;move?
11020
11050
;rephrase conclusion?
11021
11051
 
11022
 
(defthm shift-bounds 
 
11052
(defthm shift-bounds
11023
11053
  (implies (unsigned-byte-p 16 x)
11024
11054
           (<= (lshu 32 x 16) (- (expt 2 32) (expt 2 16))))
11025
11055
  :hints (("Goal" :in-theory (e/d (lshu loghead ash) nil))))
11029
11059
;; (defthm sbp-of-logapp-hack
11030
11060
;;   (implies (signed-byte-p 16 b)
11031
11061
;;            (signed-byte-p 32 (logapp 16 a b)))
11032
 
;;   :hints (("Goal" :in-theory (enable logapp 
 
11062
;;   :hints (("Goal" :in-theory (enable logapp
11033
11063
;;                                      signed-byte-p
11034
11064
;;                                      integer-range-p))))
11035
11065
 
11051
11081
;We want to extend an inequality like (< x 65535) to (< x 65536) when we also know (not (equal x 65535)) and (integerp x).
11052
11082
;Writing the rule with the free variable means we really must find the disquality right there in the context.
11053
11083
;Perhaps this should pay attention to whether we're trying to satisfy or falsity the <.
11054
 
;seemed to loop. 
 
11084
;seemed to loop.
11055
11085
(defthmd extend-<
11056
11086
  (implies (and (not (equal x free))
11057
11087
                (equal free k)
11079
11109
  :hints (("Goal" :in-theory (enable logbitp signed-byte-p))))
11080
11110
(in-theory (disable LOGBITP-TEST-OF-TOP-BIT))
11081
11111
 
11082
 
;; 
 
11112
;;
11083
11113
;; (defthm loghead-subst-32
11084
11114
;;   (implies (and (equal (loghead 32 x) k)
11085
11115
;;                 (syntaxp (quotep k))
11086
11116
;;                 )
11087
 
;;            (equal (loghead 31 x) 
 
11117
;;            (equal (loghead 31 x)
11088
11118
;;                   (loghead 31 k))))
11089
11119
 
11090
 
 
 
11120
 
11091
11121
;bzo gen
11092
11122
(defthm loghead-subst-2
11093
11123
  (implies (and (equal (loghead 31 x) k)
11094
11124
                (syntaxp (quotep k))
11095
11125
                )
11096
 
           (equal (loghead 32 x) 
 
11126
           (equal (loghead 32 x)
11097
11127
                  (logapp 31 k (logbit 31 x))
11098
11128
                  )))
11099
11129
 
11117
11147
(defthm logeqv-commutative
11118
11148
  (equal (logeqv x y)
11119
11149
         (logeqv y x))
11120
 
  :hints (("Goal" :in-theory (e/d (logeqv lognot) 
 
11150
  :hints (("Goal" :in-theory (e/d (logeqv lognot)
11121
11151
                                  (LOGAND-LOGIOR ;bzo forcing
11122
11152
                                   )))))
11123
11153
 
11154
11184
                  (equal -1 x)))
11155
11185
  :hints (("Goal" :use (:instance divide-both-sides-hack (x (- y)) (y (* x y)) (z y))))
11156
11186
  )
11157
 
                 
 
11187
 
11158
11188
;gen?
11159
11189
(defthm ash-equal-minus-expt2n
11160
11190
  (implies (and (< 0 n)
11181
11211
                           (<= 0 y))
11182
11212
                      (and (< x 0)
11183
11213
                           (< y 0)))))
11184
 
  :hints (("Goal" :in-theory (enable logeqv 
11185
 
                                     logorc1 
 
11214
  :hints (("Goal" :in-theory (enable logeqv
 
11215
                                     logorc1
11186
11216
                                     ))))
11187
11217
 
11188
11218
;; (defthm logeqv-pos
11223
11253
  (equal (logbit n (logcar x))
11224
11254
         (if (and (< 0 n)
11225
11255
                  (integerp n))
11226
 
             0 
 
11256
             0
11227
11257
           (logcar x))))
11228
11258
 
11229
11259
;changed the RHS to do a case-split because 0 is so much simpler than (ash (logbit (+ -1 n) x) (+ -1 n))
11295
11325
 
11296
11326
;gen the 1
11297
11327
(defthm loghead-equal-logapp-same-rewrite
11298
 
  (implies (and (integerp n) 
 
11328
  (implies (and (integerp n)
11299
11329
                (< 0 n))
11300
11330
           (equal (equal (loghead n x) (logapp (+ -1 n) x 1))
11301
11331
                  (equal 1 (logbit (+ -1 n) x)))))
11302
 
        
 
11332
 
11303
11333
(defthm loghead-equal-loghead-one-shorter-rewrite
11304
11334
  (implies (and (integerp x)
11305
11335
                (integerp n)
11355
11385
           (equal (logbit pos i)
11356
11386
                  (logbit pos j))))
11357
11387
 
11358
 
 
11359
 
;; 
 
11388
 
 
11389
;;
11360
11390
;; (defthm logbitp-subst-32
11361
11391
;;   (implies (and (equal (loghead 32 x) k)
11362
11392
;;                 (syntaxp (quotep k))
11363
11393
;;                 )
11364
 
;;            (equal (logbitp 31 x) 
 
11394
;;            (equal (logbitp 31 x)
11365
11395
;;                   (logbitp 31 k))))
11366
11396
 
11367
11397
;can this loop?
11428
11458
                       (equal (loghead (+ -1 n) x) 0))))
11429
11459
  :otf-flg t
11430
11460
  :hints (("Goal" :in-theory (e/d (ash
11431
 
                                   LOGHEAD-SPLIT-X-REWRITE) 
11432
 
                                  (loghead-when-mostly-0 
 
11461
                                   LOGHEAD-SPLIT-X-REWRITE)
 
11462
                                  (loghead-when-mostly-0
11433
11463
                                   LOGTAIL-LEAVES-SINGLE-BIT
11434
11464
                                   LOGHEAD-EQUAL-LOGAPP-SAME-REWRITE
11435
11465
                                   LOGAPP-0-PART-1-BETTER
11452
11482
  :hints (("Goal" :in-theory (enable logext ash))))
11453
11483
 
11454
11484
(defthm logext-equal-min-value-hack-gen-constant-version
11455
 
  (implies (and (syntaxp (and (quotep k) 
 
11485
  (implies (and (syntaxp (and (quotep k)
11456
11486
                              (quotep n)
11457
11487
                              ))
11458
11488
                (equal k (- (expt 2 (+ -1 n))))
11501
11531
 
11502
11532
;Can cause a case split.
11503
11533
(defthmd loghead-suck-in-one-plus
11504
 
  (implies (and (syntaxp (and (consp x) 
11505
 
                              (equal (car x) 'binary-+) 
 
11534
  (implies (and (syntaxp (and (consp x)
 
11535
                              (equal (car x) 'binary-+)
11506
11536
                              (quotep (cadr x))))
11507
11537
                (integerp x)
11508
11538
                (<= 0 n)
11596
11626
                (<= 0 n))
11597
11627
           (equal (logapp n (loghead n x) y)
11598
11628
                  (logapp n x y))))
11599
 
        
 
11629
 
11600
11630
 
11601
11631
;; ;kind of weird
11602
11632
;; ;bzo gross hints
11649
11679
                (<= (expt 2 n) y))
11650
11680
           (equal (equal x y)
11651
11681
                  nil)))
11652
 
        
 
11682
 
11653
11683
(defthm loghead-cancel-constants-hack
11654
11684
  (implies (and (syntaxp (and (quotep k1)   ;i think i want these syntaxp hyps, right?
11655
11685
                              (quotep k2)))
11690
11720
 
11691
11721
 
11692
11722
(defthm loghead-of-logext-hack-1
11693
 
  (implies (and (integerp x) 
 
11723
  (implies (and (integerp x)
11694
11724
                (integerp y))
11695
11725
           (equal (loghead size (+ (- (logext size x)) y))
11696
11726
                  (loghead size (+ (- x) y))))
11703
11733
                               LOGHEAD-+-CANCEL-BETTER))))
11704
11734
 
11705
11735
(defthm loghead-of-logext-hack-1-alt
11706
 
  (implies (and (integerp x) 
 
11736
  (implies (and (integerp x)
11707
11737
                (integerp y))
11708
11738
           (equal (loghead size (+ y (- (logext size x))))
11709
11739
                  (loghead size (+ y (- x)))))
11716
11746
                               LOGHEAD-+-CANCEL-BETTER))))
11717
11747
 
11718
11748
(defthm loghead-of-logext-hack-2
11719
 
  (implies (and (integerp x) 
 
11749
  (implies (and (integerp x)
11720
11750
                (integerp y)
11721
11751
                (integerp i)
11722
11752
                )
11726
11756
  )
11727
11757
 
11728
11758
(defthm loghead-of-logext-hack-3
11729
 
  (implies (and (integerp x) 
 
11759
  (implies (and (integerp x)
11730
11760
                (integerp y)
11731
11761
                (integerp i)
11732
11762
                )
11748
11778
                         (loghead size zblah2)))))
11749
11779
 
11750
11780
(defthm loghead-of-logext-hack-4
11751
 
  (implies (and (integerp x) 
 
11781
  (implies (and (integerp x)
11752
11782
                (integerp y)
11753
11783
                (integerp i)
11754
11784
                (integerp z)
11761
11791
           :use ((:instance loghead-of-sum-of-prod-of-loghead-lemma (n size) (y -1) (a (+ z y w)) (x x))))))
11762
11792
 
11763
11793
(defthm loghead-of-logext-hack-5
11764
 
  (implies (and (integerp x) 
 
11794
  (implies (and (integerp x)
11765
11795
                (integerp y)
11766
11796
                (integerp i)
11767
11797
                (integerp w)
11780
11810
                (integerp b))
11781
11811
           (equal (< (+ 1/2 b) a)
11782
11812
                  (<= (+ 1 b) a))))
11783
 
                 
 
11813
 
11784
11814
(defthm divides-hack-more
11785
11815
  (equal (integerp (+ 1/65536 (* 1/65536 x)))
11786
11816
         (divides 65536 (+ 1 x)))
11825
11855
                  (loghead (+ 1 n) a)))
11826
11856
  :hints (("Goal" :in-theory (e/d (equal-logapp-x-y-z
11827
11857
                                     logtail-loghead-better
11828
 
                                     ) 
 
11858
                                     )
11829
11859
                                  (loghead-logtail)))))
11830
11860
 
11831
11861
 
11924
11954
                )
11925
11955
           (equal (LOGEXT size (+ a b d (* k (LOGEXT size c))))
11926
11956
                  (LOGEXT size (+ a b (* k c) d)))))
11927
 
  
 
11957
 
11928
11958
(defthm logapp-recombine-logext-case
11929
11959
  (implies (and (<= n size) ;other case?
11930
11960
                (integerp size))
11941
11971
 
11942
11972
;bzo - gen?
11943
11973
(defthm loghead-sum-weird
11944
 
  (implies (and (integerp y) 
 
11974
  (implies (and (integerp y)
11945
11975
                (integerp x)
11946
11976
                (integerp z)
11947
11977
                (<= n size)
11960
11990
(defthm logapp-chop-hack-1
11961
11991
  (implies (and (<= n size)
11962
11992
                (integerp size)
11963
 
                (integerp y) 
 
11993
                (integerp y)
11964
11994
                (integerp x)
11965
11995
                (integerp n)
11966
11996
                (<= 0 n)
12014
12044
                )
12015
12045
           (equal (LOGAPP m (+ w v x y (* N (LOGEXT size z))) xx)
12016
12046
                  (LOGAPP m (+ w v x y (* N z)) xx))))
12017
 
 
 
12047
 
12018
12048
(defthm loghead-hack-blah
12019
 
  (implies (and (integerp y) 
 
12049
  (implies (and (integerp y)
12020
12050
                (integerp z)
12021
12051
                (<= 0 size)
12022
12052
                (integerp size))
12077
12107
;; ;                                   loghead-split-special
12078
12108
;; ;                                  logbit ;bzo
12079
12109
;; ;                                 equal-of-logheads-split
12080
 
;;                                    ) 
 
12110
;;                                    )
12081
12111
;;                                   ()))))
12082
12112
 
12083
12113
;trying...
12138
12168
;;   (equal (logapp 16 val (loghead 16 (logtail 16 val)))
12139
12169
;;          (loghead 32 val))
12140
12170
;;   :hints (("Goal" :in-theory (e/d (logtail-loghead-better
12141
 
;;                                      equal-logapp-x-y-z) 
 
12171
;;                                      equal-logapp-x-y-z)
12142
12172
;;                                   (loghead-logtail)))))
12143
12173
 
12144
12174
(defthm logapp-recollapse
12149
12179
           (equal (logapp n val (loghead m (logtail n val)))
12150
12180
                  (loghead (+ n m) val)))
12151
12181
  :hints (("Goal" :in-theory (e/d (logtail-loghead-better
12152
 
                                   equal-logapp-x-y-z) 
 
12182
                                   equal-logapp-x-y-z)
12153
12183
                                  (loghead-logtail)))))
12154
12184
 
12155
12185
 
12202
12232
                (< off 1))
12203
12233
           (equal (< (+ off x) y)
12204
12234
                  (< x y))))
12205
 
                 
 
12235
 
12206
12236
 
12207
12237
(defthmd non-multiple-addend-doesnt-matter-when-comparing-multiples
12208
12238
  (implies (and (integerp z)
12220
12250
                                  (x (/ x y))
12221
12251
                                  (y (/ z y)))))
12222
12252
  )
12223
 
                 
 
12253
 
12224
12254
 
12225
12255
(defthmd compare-of-add-to-shifted
12226
12256
  (implies (and (unsigned-byte-p m off)
12260
12290
                                       (z (- (EXPT 2 N)))
12261
12291
                                       )
12262
12292
           )
12263
 
          ("Goal" 
 
12293
          ("Goal"
12264
12294
           :cases ((< x 0))
12265
12295
           :in-theory (enable UNSIGNED-BYTE-P))))
12266
12296
 
12350
12380
  (implies (and (integerp size) (< 0 size))
12351
12381
           (equal (logext size (expt 2 (+ -1 size)))
12352
12382
                  (-  (expt 2 (+ -1 size)))))
12353
 
  :hints (("Goal" :in-theory (e/d (logext EQUAL-LOGAPP-X-Y-Z) 
 
12383
  :hints (("Goal" :in-theory (e/d (logext EQUAL-LOGAPP-X-Y-Z)
12354
12384
                                  (logapp-subst-in-first-arg ;LOGAPP-HACK2 ;bzo
12355
12385
                                   )))))
12356
 
 
 
12386
 
12357
12387
;bzo gen
12358
12388
(defthmd minus-of-logext
12359
12389
  (implies (and (integerp size)
12364
12394
                      (expt 2 (+ -1 size))
12365
12395
                    (logext size (- i)))))
12366
12396
  :hints (("Goal" :use ((:instance LOGEXT-LOGHEAD (n size) (m size) (x i)))
12367
 
           :in-theory (e/d (ASH-1-EXPT-REWRITE) 
 
12397
           :in-theory (e/d (ASH-1-EXPT-REWRITE)
12368
12398
                           (LOGEXT-LOGHEAD
12369
12399
                            DUMB ;why?!
12370
12400
                            )))))
12401
12431
                (< 0 size1))
12402
12432
           (equal (logext size1 (logext size2 x))
12403
12433
                  (logext size1 x))))
12404
 
        
 
12434
 
12405
12435
(defthmd loghead-split-when-usb-one-longer
12406
12436
  (implies (and (unsigned-byte-p (+ 1 n) x)
12407
12437
                (integerp n)
12452
12482
 
12453
12483
 
12454
12484
(defthmd loghead-0-hack
12455
 
 (implies (and (equal (loghead 16 offset1) 
 
12485
 (implies (and (equal (loghead 16 offset1)
12456
12486
                      (loghead 16 offset2))
12457
12487
               (integerp offset1)
12458
12488
               (integerp offset2))
12477
12507
                                   (n size2)
12478
12508
                                   (y (logtail size2 (loghead size1 x)))
12479
12509
                                   (z  (loghead size1 x))))
12480
 
          
12481
 
           :in-theory (e/d (loghead-equal-rewrite) 
 
12510
 
 
12511
           :in-theory (e/d (loghead-equal-rewrite)
12482
12512
                           (equal-logapp-x-y-z
12483
12513
                            equal-logapp-x-y-z-constants
12484
12514
                            LOGAPP-RECOMBINE-LOGHEAD-CASE
12504
12534
                  (equal (logtail size2 (loghead size1 x)) 0)))
12505
12535
  :hints (("Goal" :in-theory (e/d (LOGTAIL-LOGHEAD-BETTEr
12506
12536
                                   LOGEXT-SUBST-WITH-LOGHEAD
12507
 
                                   LOGTAIL-LOGEXT) 
 
12537
                                   LOGTAIL-LOGEXT)
12508
12538
                                  (LOGTAIL-EQUAL-0
12509
12539
                                   LOGEXT-LOGTAIL
12510
12540
                                   LOGHEAD-LOGTAIL)))))
12526
12556
                                   (n size2)
12527
12557
                                   (y (logtail size2 (logext size1 x)))
12528
12558
                                   (z  (logext size1 x))))
12529
 
          
12530
 
           :in-theory (e/d (loghead-equal-rewrite) 
 
12559
 
 
12560
           :in-theory (e/d (loghead-equal-rewrite)
12531
12561
                           (LOGAPP-RECOMBINE-LOGEXT-CASE
12532
12562
                            equal-logapp-x-y-z
12533
12563
                            equal-logapp-x-y-z-constants
12598
12628
                       (unsigned-byte-p size (loghead size1 x)))))
12599
12629
  :hints (("Goal" :use (:instance expt-weakly-monotonic-linear)
12600
12630
           :in-theory (e/d (logapp UNSIGNED-BYTE-P
12601
 
                                   ) 
 
12631
                                   )
12602
12632
                           (EXPT-IS-WEAKLY-INCREASING-FOR-BASE>1
12603
12633
                            EXPT-COMPARE)))))
12604
12634
 
12612
12642
                  (ifix x)))
12613
12643
  :hints (("Goal" :cases ((and (integerp n)
12614
12644
                               (<= 0 n)))
12615
 
           :in-theory (e/d (ash-as-logapp) 
 
12645
           :in-theory (e/d (ash-as-logapp)
12616
12646
                           (logapp-0-part-2-better)))))
12617
12647
 
12618
12648
(defthm logtail-of-sum-of-ash-alt
12659
12689
  (implies (and (unsigned-byte-p 16 x)
12660
12690
                (<= 0 k)
12661
12691
                (integerp k))
12662
 
           (equal (unsigned-byte-p 16 (+ (- k) x))         
 
12692
           (equal (unsigned-byte-p 16 (+ (- k) x))
12663
12693
                  (<= k x))))
12664
12694
 
12665
12695
(defthm unsigned-byte-p-becomes-inequality-alt
12666
12696
  (implies (and (unsigned-byte-p 16 x)
12667
12697
                (<= 0 k)
12668
12698
                (integerp k))
12669
 
           (equal (unsigned-byte-p 16 (+ x (- k)))         
 
12699
           (equal (unsigned-byte-p 16 (+ x (- k)))
12670
12700
                  (<= k x))))
12671
12701
 
12672
12702
(defthmd usb-of-sum-with-two-other-addends-hack
12717
12747
;why did this suddenly become necessary?
12718
12748
(defthm logbit-too-big-no-free-vars
12719
12749
  (implies (unsigned-byte-p n x)
12720
 
           (equal (logbit n x) 
 
12750
           (equal (logbit n x)
12721
12751
                  0))
12722
12752
  :hints (("Goal" :in-theory (enable logbit logbitp))))
12723
12753
 
12796
12826
                (unsigned-byte-p 16 i)
12797
12827
                (<= (- 65536 bigconst) i) ;most likely to fail?
12798
12828
                (<= 0 bigconst)
12799
 
                (integerp bigconst) 
 
12829
                (integerp bigconst)
12800
12830
                )
12801
12831
           (equal (loghead 16 (+ bigconst i))
12802
12832
                  (+ (- bigconst 65536) i)))
12829
12859
 
12830
12860
 
12831
12861
(defthm loghead-equality-impossible
12832
 
  (implies (and (syntaxp (and (quotep k1) 
 
12862
  (implies (and (syntaxp (and (quotep k1)
12833
12863
                              (quotep k2)))
12834
12864
                (not (equal 0 (loghead 16 (+ k1 k2))))
12835
12865
                (unsigned-byte-p 16 x) ;not needed?
12839
12869
           (equal (equal x (+ k1 (loghead 16 (+ k2 x)))) ;note that x appears twice in LHS
12840
12870
                  nil))
12841
12871
  :hints (("Goal" :in-theory (e/d (loghead-sum-split-into-2-cases
12842
 
                                   loghead-of-minus) 
 
12872
                                   loghead-of-minus)
12843
12873
                                  (unsigned-byte-p-loghead-forward-chaining
12844
 
;loghead-type 
 
12874
;loghead-type
12845
12875
;(:type-prescription loghead)
12846
12876
                                   )))))
12847
12877
 
12858
12888
           (not (UNSIGNED-BYTE-P n (LOGAPP m i j)))))
12859
12889
 
12860
12890
(defthm loghead-lower-bound-when-top-bit-one
12861
 
  (implies (and (logbitp (+ -1 n) x) 
 
12891
  (implies (and (logbitp (+ -1 n) x)
12862
12892
                (integerp n)
12863
12893
                (< 0 n)
12864
12894
                (integerp x))
12894
12924
                  (ifix x)
12895
12925
                  ))
12896
12926
  :hints (("Goal" :use (:instance logapp-reassemble (i x))
12897
 
           :in-theory (e/d (LOGAPP) 
 
12927
           :in-theory (e/d (LOGAPP)
12898
12928
                           (logapp-reassemble
12899
12929
                            EQUAL-LOGAPP-X-Y-Z-CONSTANTS
12900
12930
                            LOGAPP-DOES-NOTHING-REWRITE))))
12932
12962
                (INTEGERP N)
12933
12963
                (< 0 N))
12934
12964
           (SIGNED-BYTE-P N (+ X (- (EXPT 2 (+ -1 N))))))
12935
 
  :hints (("Goal" :in-theory (enable SIGNED-BYTE-P 
 
12965
  :hints (("Goal" :in-theory (enable SIGNED-BYTE-P
12936
12966
                                     unSIGNED-BYTE-P
12937
12967
                                     EXPONENTS-ADD-UNRESTRICTED))))
12938
12968
 
12953
12983
           (equal (logext n (+ k x))
12954
12984
                  (+ (- (expt 2 (+ -1 n))) x)))
12955
12985
  :hints (("Goal" :in-theory (enable logext logbitp-+-expt-n-rewrite))))
12956
 
        
 
12986
 
12957
12987
;gen!?
12958
12988
(defthm half-cancel
12959
12989
  (equal (+ x (- (* 1/2 x)) y)
12965
12995
                (< 0 n))
12966
12996
           (equal (EQUAL x (+ (expt 2 n) (LOGEXT n x)))
12967
12997
                  (<= (expt 2 (+ -1 n)) x)))
12968
 
  :hints (("Goal" :in-theory (enable logext 
 
12998
  :hints (("Goal" :in-theory (enable logext
12969
12999
                                     logapp
12970
13000
                                     EXPONENTS-ADD-UNRESTRICTED))))
12971
13001
 
13008
13038
 
13009
13039
;generalize: if the logior of y and the lognot of z is not -1, then (equal (logior z x) y) = nil.
13010
13040
 
13011
 
(defthm logior-hack 
 
13041
(defthm logior-hack
13012
13042
  (implies (and (not (logbitp 8 y))
13013
13043
                (integerp x) ;drop
13014
13044
                )
13044
13074
                  (and (integerp x)
13045
13075
                       (equal 0 (loghead n x))
13046
13076
                       (equal (ifix y) (logtail n x))))))
13047
 
        
 
13077
 
13048
13078
;trying a switch of the direction to associate logapp!  doing it this way
13049
13079
;means the sizes in the logapp nest are the sizes of their corresponding
13050
13080
;values, rather than sums of the sizes of several values
13061
13091
;This one's :executable-counterpart stays enabled.
13062
13092
(defund expt-execute (r i) (expt r i))
13063
13093
 
13064
 
;Allows expt calls with small exponents to be computed  
 
13094
;Allows expt calls with small exponents to be computed
13065
13095
;You can change 1000 to your own desired bound.
13066
13096
(defthmd expt-execute-rewrite
13067
13097
  (implies (and (syntaxp (and (quotep r) (quotep i) (< (abs (cadr i)) 1000))))
13202
13232
                  (loghead m (+ z x)))))
13203
13233
 
13204
13234
 
13205
 
        
 
13235
 
13206
13236
;bzo gen the 0?
13207
13237
;; (defthm loghead-plus-constant-compare-to-zero
13208
13238
;;   (implies (and (syntaxp (quotep j))
13220
13250
                (integerp c))
13221
13251
           (equal (logapp size (ash x c) y)
13222
13252
                  (logapp size 0 y))))
13223
 
        
 
13253
 
13224
13254
(defthm equal-logapp-with-logtail-of-self-rewrite
13225
13255
  (equal (equal y (acl2::logapp 16 x (acl2::logtail 16 y)))
13226
13256
         (and (integerp y)
13407
13437
  :hints (("Goal" :in-theory (enable unsigned-byte-p signed-byte-p))))
13408
13438
 
13409
13439
;this might be expensive?
13410
 
(defthm equal-bit-1 
13411
 
  (implies (unsigned-byte-p 1 x) 
13412
 
           (equal (equal x 1) 
 
13440
(defthm equal-bit-1
 
13441
  (implies (unsigned-byte-p 1 x)
 
13442
           (equal (equal x 1)
13413
13443
                  (not (equal x 0)))))
13414
13444
 
13415
13445
(defthm unsigned-byte-p-+-easy