3
(include-book "ground-zero")
4
(include-book "../../arithmetic/negative-syntaxp")
5
(include-book "../../arithmetic/power2p")
7
(local (include-book "../../arithmetic/top"))
8
(local (include-book "bvecp"))
11
(declare (xargs :guard (integerp k)))
17
(defun expo-measure (x)
18
; (declare (xargs :guard (and (real/rationalp x) (not (equal x 0)))))
19
(cond ((not (rationalp x)) 0)
21
((< x 1) (cons 1 (fl (/ x))))
25
(declare (xargs :guard t
26
:measure (expo-measure x)))
27
(cond ((or (not (rationalp x)) (equal x 0)) 0)
28
((< x 0) (expo (- x)))
29
((< x 1) (1- (expo (* 2 x))))
31
(t (1+ (expo (/ x 2))))))
34
(declare (xargs :guard t))
39
;this book is still a mess
42
(declare (xargs :guard (real/rationalp x)))
47
The new version of bits is like Russinoff's "bits" but uses mod instead of rem.
48
The use of "mod" seems to allow nicer results to be proved.
50
For example, bits now *always* returns a non-negative integer. Many hyps of other lemmas require
51
expressions to be non-negative integers, and with the old bits, this requires further checking of the
52
arguments (at worst, checking all the way to the leaves of the expression tree each time).
54
Add case-split to all hyps about i and j (indices to bits must be integers and j must be <= i or else weird
55
stuff may happen (but we can easily handle these cases).
59
;In proofs about RTL terms, i and j should always be natural number constants
62
(declare (xargs :guard (and (natp x)
66
(mbe :logic (if (or (not (integerp i))
69
(fl (/ (mod x (expt 2 (1+ i))) (expt 2 j))))
72
(logand (ash x (- j)) (1- (ash 1 (1+ (- i j))))))))
74
(defthm bits-nonnegative-integerp-type
75
(and (<= 0 (bits x i j))
76
(integerp (bits x i j)))
77
:hints (("Goal" :in-theory (enable bits)))
78
:rule-classes (:type-prescription))
80
;this rule is no better than bits-nonnegative-integer-type and might be worse
81
(in-theory (disable (:type-prescription bits)))
87
:hints (("Goal" :in-theory (enable bits))))
89
(defthm bits-with-i-not-an-integer
90
(implies (not (integerp i))
93
:hints (("Goal" :in-theory (enable bits))))
95
(defthm bits-with-j-not-an-integer
96
(implies (not (integerp j))
99
:hints (("Goal" :in-theory (enable bits))))
101
(defthm bits-with-indices-in-the-wrong-order
105
:hints (("Goal" :in-theory (enable bits))))
107
(defthm bits-upper-bound
108
(< (bits x i j) (expt 2 (+ 1 i (- j))))
109
:rule-classes (:rewrite (:linear :trigger-terms ((bits x i j))))
110
:hints (("Goal" :in-theory (enable bits
114
;has the right pattern to rewrite stuff like this: (<= (EXPT 2 J) (BITS Y (+ -1 J) 0)) to nil
115
(defthm bits-upper-bound-special
116
(< (BITS x (1- i) 0) (EXPT 2 i))
117
:hints (("Goal" :use (:instance bits-upper-bound (i (1- i)) (j 0))))
121
(defthm bits-upper-bound-tighter
122
(implies (case-split (<= j i))
123
(<= (bits x i j) (1- (expt 2 (+ i 1 (- j))))))
124
:rule-classes (:rewrite (:linear :trigger-terms ((bits x i j))))
125
:hints (("Goal" :cases ((rationalp x) (not (acl2-numberp x)))
126
:in-theory (enable bits
131
;like mod-upper-bound-3
132
(defthm bits-upper-bound-2
133
(implies (and (<= (expt 2 (+ 1 i (- j))) z) ;backchain-limit?
134
;(case-split (integerp i))
135
;(case-split (integerp j))
142
;I have many theorems dealing with the simplification of bits of a sum
148
;taking sort of a long time (3-4 secs)
149
(defthm bits-sum-lowbits
150
(implies (and (rationalp x)
154
(equal (bits (+ x y) i j)
155
(bits (+ (lowbits x i) y) i j)))
156
:hints (("Goal" :in-theory (enable ;mod-cancel
159
(in-theory (disable bits-sum-lowbits))
161
;special case of the above -- helps rewrite the constant to a unique (positive) value
162
;make another rule to handle negative constants
163
(defthm bits-sum-reduce-leading-constant
164
(implies (and (syntaxp (and (quotep x) (>= (cadr x) (expt 2 (+ (cadr i) 1)))))
169
(equal (bits (+ x y) i j)
170
(bits (+ (lowbits x i) y) i j)))
171
:hints (("Goal" :use bits-sum-lowbits )))
173
(defun oldbits (x i j)
174
(fl (/ (rem x (expt 2 (1+ i))) (expt 2 j))))
176
(in-theory (disable bits)) ;move up
178
;(in-theory (disable INTEGER-HAS-DENOM-1-OTHER-WAY))
180
(in-theory (disable rem))
187
(implies (and (<= (* a (expt 2 (+ i 1))) x)
188
(< x (* (1+ a) (expt 2 (+ i 1))))
194
(equal (bits x i 0) (- x (* a (expt 2 (+ i 1))))))
196
:hints (("Goal" :in-theory (enable bits)
197
:use (:instance mod-force-eric (y (expt 2 (+ i 1)))))))
199
(defthm bits-force-with-a-chosen-neg
200
(implies (and (< x 0)
201
(<= (* -1 (expt 2 (+ i 1))) x)
206
(equal (bits x i 0) (- x (* -1 (expt 2 (+ i 1))))))
208
:use (:instance bits-force (a -1)))))
211
;(in-theory (disable bits-force))
216
(implies (and ;(rationalp x)
217
(case-split (integerp n))
218
(case-split (integerp i))
219
(case-split (integerp j))
221
(and (equal (bits (* (expt 2 n) x) i j)
222
(bits x (- i n) (- j n)))
223
(equal (bits (* x (expt 2 n)) i j)
224
(bits x (- i n) (- j n)))))
225
:hints (("Goal" :cases ((and (acl2-numberp n) (not (rationalp n)))
226
(and (rationalp n) (not (integerp n)))
228
:in-theory (e/d (expt-minus
234
( ;these are disabled to speed up he proof:
235
INTEGERP-PROD-OF-3-FIRST-AND-LAST
236
INTEGERP-PROD-OF-3-LAST-TWO
240
; Basically a restatement of bits-shift:
241
(defthm bits-shift-up-1
242
(implies (and (integerp k)
245
(equal (bits (* (expt 2 k) x) i j)
246
(bits x (- i k) (- j k))))
247
:hints (("Goal" :use ((:instance bits-shift (n k)))))
252
(implies (and ;(rationalp x)
253
(case-split (integerp n))
254
(case-split (integerp i))
255
(case-split (integerp j))
257
(and (equal (bits (* (expt 2 n) x) i j)
258
(bits x (- i n) (- j n)))
259
(equal (bits (* x (expt 2 n)) i j)
260
(bits x (- i n) (- j n)))))
261
:hints (("Goal" :cases ((and (acl2-numberp n) (not (rationalp n)))
262
(and (rationalp n) (not (integerp n)))
264
:in-theory (enable expt-minus
270
(local (in-theory (enable mod-cancel)))
272
;allows you to split bit vectors into two parts
273
;free var n (where to split)
274
;resembles doc's bits-plus-bits-1 and another rule in merge
275
(defthm bits-plus-bits2
276
(implies (and ;(rationalp x)
284
(+ (* (bits x i n) (expt 2 (- n j)))
287
:hints (("Goal" :in-theory (enable bits mod expt-split expt-minus))))
289
;a hint that worked for this before I made such nice rules is in junk.lisp under bits-plus-bits-hint
291
;(in-theory (disable bits-plus-bits-1)) ;keep disabled
296
;could use even-odd phrasing?
297
(defthm bits-down-to-1-case-split
298
(implies (and (integerp x)
303
(if (equal (bitn x 0) 0)
304
(/ (bits x i 0) 2) ;use the fact that we know bit 0 is 0?
305
(/ (1- (bits x i 0)) 2) ;use the fact that we know bit 0 is 1?
308
:hints (("Goal" :in-theory (enable bits mod bitn))))
311
;this really has two separate cases
312
;generalize with j not 0?
313
(defthm bits-split-around-zero
314
(implies (and (>= x (- (expt 2 (+ i 1))))
315
(< x (expt 2 (+ i 1)))
317
(case-split (integerp i))
318
(case-split (<= 0 i))
323
(+ x (expt 2 (+ i 1))))))
324
:hints (("Goal" :in-theory (enable bits)
325
:use ((:instance bits-force (a 0))
326
(:instance bits-force (a -1))))))
329
;(local (in-theory (disable expt-inverse)))
331
(defthm bits-bvecp-simple
332
(implies (equal k (+ 1 i (* -1 j)))
333
(bvecp (bits x i j) k))
334
:hints (("Goal" :in-theory (enable
340
(implies (and (<= (+ 1 i (- j)) k)
341
(case-split (integerp k))
343
(bvecp (bits x i j) k))
344
:hints (("Goal" :use ((:instance bits-bvecp-simple
345
(k (+ 1 i (* -1 j)))))
346
:in-theory (disable bits-bvecp-simple))))
348
(in-theory (disable bits-bvecp-simple))
350
;do we want this rule enabled?
351
(defthm bits-bvecp-fw
352
(implies (equal n (- (1+ i) j)) ; note equal here to help with the fw chaining
353
(bvecp (bits x i j) n))
355
((:forward-chaining :trigger-terms ((bits x i j)))))
357
;these may be made moot by my method of using lowbits with bits of a sum
360
(defthm bits-sum-simplify-first-term
361
(implies (and (>= (abs x) (expt 2 (+ j 1))) ;prevents loop
367
(equal (bits (+ x y) j 0)
368
(bits (+ (lowbits x j) y) j 0)))
369
:hints (("Goal" :in-theory (enable lowbits
372
(defthm bits-sum-simplify-second-term
373
(implies (and (>= (abs x) (expt 2 (+ j 1))) ;prevents loop
379
(equal (bits (+ y x) j 0)
380
(bits (+ (lowbits x j) y) j 0)))
381
:hints (("Goal" :in-theory (enable lowbits
387
(local (in-theory (disable mod-cancel)))
389
;better names: make the dropped term x, the others a,b,c,...
390
;;; more bits thms like this!
392
(defthm bits-sum-drop-irrelevant-term-2-of-2
393
(implies (integerp (/ y (expt 2 (+ 1 i))))
394
(equal (bits (+ x y) i j)
396
:hints (("Goal" :cases ((rationalp y) (not (acl2-numberp y)))
397
:in-theory (enable bits))))
399
(defthm bits-sum-drop-irrelevant-term-1-of-2
400
(implies (integerp (/ y (expt 2 (+ 1 i))))
401
(equal (bits (+ y x) i j)
403
:hints (("Goal" :cases ((rationalp y) (not (acl2-numberp y)))
404
:in-theory (enable bits))))
406
(defthm bits-sum-drop-irrelevant-term-3-of-3
407
(implies (integerp (/ y (expt 2 (+ 1 i))))
408
(equal (bits (+ w x y) i j)
410
:hints (("Goal" :in-theory (disable bits-sum-drop-irrelevant-term-1-of-2
411
bits-sum-drop-irrelevant-term-2-of-2)
412
:use (:instance bits-sum-drop-irrelevant-term-1-of-2 (x (+ w x))))))
414
(defthm bits-sum-drop-irrelevant-term-2-of-3
415
(implies (integerp (/ y (expt 2 (+ 1 i))))
416
(equal (bits (+ w y x) i j)
418
:hints (("Goal" :in-theory (disable bits-sum-drop-irrelevant-term-3-of-3
419
bits-sum-drop-irrelevant-term-1-of-2
420
bits-sum-drop-irrelevant-term-2-of-2)
421
:use (:instance bits-sum-drop-irrelevant-term-1-of-2 (x (+ w x))))))
423
(defthm bits-sum-drop-irrelevant-term-1-of-3
424
(implies (and (integerp x)
433
(integerp (/ y (expt 2 (+ 1 i))))
435
(equal (bits (+ y w x) i j)
437
:hints (("Goal" :in-theory (disable bits-sum-drop-irrelevant-term-2-of-3
438
bits-sum-drop-irrelevant-term-3-of-3
439
bits-sum-drop-irrelevant-term-1-of-2
440
bits-sum-drop-irrelevant-term-2-of-2)
441
:use (:instance bits-sum-drop-irrelevant-term-1-of-2 (x (+ w x))))))
447
This series of events deals with simplifying expressions like
450
Intuitively, bits 6 down-to 0 appear on both sides of the sum and should be "cancelled".
451
The remaining bits will need to be "shifted" back into place.
453
More rules are probably needed to make the theory complete.
457
(defthm bits-cancel-lowbits-in-comparison
458
(implies (and (> i+ i)
466
(equal (equal (+ k (bits x i j))
468
(equal (* (expt 2 (+ 1 i (- j)))
472
:use (:instance bits-plus-bits-1 (n (+ i 1)) (i i+))
473
:in-theory (enable expt-split)
476
(defthm bits-cancel-lowbits-in-comparison-alt-2
477
(implies (and (> i+ i)
485
(equal (equal (+ (bits x i j) k)
487
(equal (* (expt 2 (+ 1 i (- j)))
491
:use (:instance bits-plus-bits-1 (n (+ i 1)) (i i+))
492
:in-theory (enable expt-split)
497
;todo: rephrase the conclusion of the above by moving the "constant" (* 2 (EXPT 2 I) (/ (EXPT 2 J))) to the other
499
;a good idea since k is usually divisible by that quantity (with the rule above, we often end up with an
500
equality in which each side should have a power of 2 divided out of it
501
; not needed if we have good meta rules for cancelling factors from an inequality
504
(defthm bits-cancel-lowbits-in-comparison-2
505
(implies (and (> i+ i)
514
(equal (equal (+ k (bits x i j))
518
(/ k (expt 2 (+ 1 i (- j)))))))
520
:use (:instance bits-cancel-lowbits-in-comparison)
521
:in-theory (set-difference-theories
523
'(bits-cancel-lowbits-in-comparison))
529
(defthm bits-cancel-lowbits-in-comparison-3
530
(implies (and (> i+ i)
539
(equal (equal (+ (bits x i+ j) k)
541
(equal (* (expt 2 (+ 1 i (- j )))
545
:use (:instance bits-plus-bits-1 (n (+ i 1)) (i i+))
546
:in-theory (set-difference-theories
549
BITS-CANCEL-LOWBITS-IN-COMPARISON-ALT-2))
553
(defthm bits-cancel-lowbits-in-comparison-no-constant
554
(implies (and (> i+ i)
561
(equal (equal (bits x i j)
563
(equal (* 2 (EXPT 2 I)
568
:use (:instance bits-plus-bits-1 (n (+ i 1)) (i i+))
569
:in-theory (set-difference-theories
571
'( BITS-CANCEL-LOWBITS-IN-COMPARISON-ALT-2
575
(defthm bits-cancel-lowbits-in-comparison-no-constant-2
576
(implies (and (> i+ i)
583
(equal (equal (bits x i+ j)
585
(equal (* 2 (EXPT 2 I)
590
:use (:instance bits-plus-bits-1 (n (+ i 1)) (i i+))
591
:in-theory (set-difference-theories
593
'( BITS-CANCEL-LOWBITS-IN-COMPARISON-ALT-2
597
;the theory above (cancelling bits in comparisons) is not complete
598
;it should also deal with bitn
599
;perhaps a bind-free rule would be a good idea here?
606
(implies (and (case-split (rationalp x))
607
(case-split (integerp i))
608
(case-split (<= j i))
609
(case-split (integerp j))
611
(equal (bits (* -1 x) i j)
612
(if (integerp (* 1/2 x (/ (expt 2 i))))
614
(if (integerp (* x (/ (expt 2 j))))
615
(+ (* 2 (expt 2 i) (/ (expt 2 j))) (- (bits x i j)))
616
(+ -1 (* 2 (expt 2 i) (/ (expt 2 j))) (- (bits x i j)))))))
617
:hints (("goal" :in-theory (enable mod-mult-of-n
627
(defthm bits-minus-alt
628
(implies (and (syntaxp (negative-syntaxp x))
629
(case-split (rationalp x))
630
(case-split (integerp i))
631
(case-split (<= j i))
632
(case-split (integerp j))
635
(if (integerp (* 1/2 (- X) (/ (EXPT 2 I))))
637
(if (INTEGERP (* (- X) (/ (EXPT 2 J))))
638
(+ (* 2 (EXPT 2 I) (/ (EXPT 2 J))) (- (bits (- x) i j)))
639
(+ -1 (* 2 (EXPT 2 I) (/ (EXPT 2 J))) (- (bits (- x) i j)))))))
640
:hints (("Goal" :in-theory (disable bits-minus)
641
:use (:instance bits-minus (x (- x)))))
648
(defthm bits-shift-alt
649
(implies (and (syntaxp (should-have-a-2-factor-divided-out x))
650
(> j 0) ;restricts application
657
(bits (/ x 2) (- i 1) (- j 1))))
658
:hints (("Goal" :in-theory (set-difference-theories
661
:use (:instance bits-shift (x (/ x 2)) (n 1)))))
666
;drops hyps like this: (<= (BITS x 30 24) 253)
667
;Recall that <= gets rewritten to < during proofs
668
(defthm bits-drop-silly-upper-bound
669
(implies (and (syntaxp (quotep k))
670
(>= k (1- (expt 2 (+ 1 i (- j)))))
671
(case-split (<= j i))
672
; (case-split (rationalp x))
673
(case-split (integerp i))
674
(case-split (integerp j))
675
; (case-split (rationalp k))
677
(equal (< k (bits x i j))
680
;rewrite things like (<= 4096 (BITS x 23 12)) to false
681
;Recall that <= gets rewritten to < during proofs
682
(defthm bits-drop-silly-lower-bound
683
(implies (and (syntaxp (quotep k))
684
(> k (1- (expt 2 (+ 1 i (- j)))))
685
(case-split (<= j i))
686
; (case-split (rationalp x))
687
(case-split (integerp i))
688
(case-split (integerp j))
689
; (case-split (rationalp k))
691
(equal (< (bits x i j) k)
694
;rewrite (< -64 (BITS <signal> 64 59)) to t
695
(defthm bits-drop-silly-bound-3
696
(implies (and (syntaxp (quotep k))
699
(equal (< k (bits x i j))
702
(defthm bits-drop-silly-bound-4
703
(implies (and (syntaxp (quotep k))
706
(equal (< (bits x i j) k)
710
(equal (< (bits x i j) 1)
711
(equal (bits x i j) 0)))
713
;put bits-cancel- in the name?
714
(defthm bits-at-least-zeros
715
(implies (and (syntaxp (quotep k))
716
(equal k (expt 2 (- j2 j)))
718
(case-split (rationalp x))
719
(case-split (integerp i))
720
(case-split (integerp j))
721
(case-split (integerp j2))
723
(equal (< (BITS x i j)
726
:hints (("Goal" :use (:instance bits-plus-bits2 (n j2)))))
728
(defthm bits-upper-with-subrange
729
(implies (and (syntaxp (quotep k))
731
(equal k (expt 2 (- j2 j)))
732
(case-split (<= j2 i)) ;drop?
733
(case-split (rationalp x))
734
(case-split (integerp i))
735
(case-split (integerp j))
736
(case-split (integerp j2))
739
(BINARY-+ k (BINARY-* k (BITS x i j2)))))
740
:hints (("Goal" :use (:instance bits-plus-bits2 (j j) (n j2)))))
742
(defthm bits-upper-with-subrange-alt
743
(implies (and (syntaxp (quotep k))
745
(equal k (expt 2 (- j2 j)))
746
(case-split (<= j2 i)) ;drop?
747
(case-split (rationalp x))
748
(case-split (integerp i))
749
(case-split (integerp j))
750
(case-split (integerp j2))
752
(equal (< (BINARY-+ k (BINARY-* k (BITS x i j2)))
755
:hints (("Goal" :use (:instance bits-plus-bits2 (j j) (n j2)))))
758
;make another version for k negative?
759
(defthm bits-equal-impossible-constant
760
(implies (and (syntaxp (quotep k))
761
(<= (expt 2 (+ 1 i (- j))) k)
763
(not (equal (bits x i j) k))))
772
(defthm bits-sum-drop-irrelevant-term-1-of-1
773
(implies (and (rationalp x) ;(integerp x)
780
(integerp (/ x (expt 2 (+ 1 i))))
784
:hints (("Goal" :in-theory (enable bits bits)))
785
:rule-classes ((:rewrite :backchain-limit-lst (nil nil nil nil nil 1)))
789
(defthm bits-with-x-not-rational
790
(implies (not (rationalp x))
793
:hints (("Goal" :in-theory (set-difference-theories
795
'( ;REARRANGE-FRACTIONAL-COEFS-<
800
(defthm bits-compare-to-zero
801
(implies (and (case-split (rationalp x))
802
(case-split (integerp i))
803
(case-split (integerp j))
805
(equal (not (< 0 (bits x i j)))
806
(equal 0 (bits x i j)))))
813
(defthmd bits-ignore-negative-bits-of-integer-main-case
814
(implies (and (<= j 0)
816
(case-split (integerp j))
817
(case-split (<= j i))
820
(* (expt 2 (- j)) (bits x i 0))))
821
:hints (("Goal" :cases ((<= j i))
822
:in-theory (enable bits)))
825
(defthm bits-ignore-negative-bits-of-integer
826
(implies (and (and (syntaxp (not (and (quotep j) (equal 0 (cadr j)))))) ;prevents loops
829
(case-split (integerp j))
832
(* (expt 2 (- j)) (bits x i 0))))
833
:hints (("Goal"; :cases ((<= j i))
834
:use bits-ignore-negative-bits-of-integer-main-case
835
:in-theory (enable)))
840
;disable since it can be bad to leave "naked" signals?
841
(defthmd bits-does-nothing-2
842
(implies (and (<= j 0) ;a bit strange (j will usually be zero?)
843
(bvecp x (+ i 1)) ;expand?
844
(case-split (integerp i))
845
(case-split (integerp j))
848
(* (expt 2 (- j)) x)))
849
:hints (("Goal" :cases ((<= j 0))
850
:in-theory (enable bits bvecp))))
858
;(include-book "factor-out")
860
(defthm bits-shift-better
861
(implies (and (bind-free (can-take-out-numeric-power-of-2 x) (c))
863
(case-split (integerp i))
864
(case-split (integerp j))
867
(bits (/ x c) (- i (expo c)) (- j (expo c)))))
868
:hints (("Goal" :in-theory (set-difference-theories
871
:use (:instance bits-shift
881
(defthm bits-does-nothing
882
(implies (and (bvecp x (1+ i))
883
(case-split (integerp i))
884
; (case-split (integerp j))
888
:hints (("Goal" :in-theory (enable bits-does-nothing-2)
892
(in-theory (disable bits-does-nothing))
896
(defthm bits-with-bad-index-2
897
(IMPLIES (NOT (INTEGERP i))
898
(EQUAL (BITS x (1- i) 0)
900
:hints (("Goal" :in-theory (enable bits))))
902
(local (defthm bvecp-bits-0-aux
903
(implies (and (case-split (natp i)) ;(natp i)
904
(case-split (<= j i))
906
(equal (bits x i j) 0))
907
:hints (("Goal" :in-theory (enable bits bvecp)
908
:use (;(:instance mod-equal (m x) (n (expt 2 (1+ i))))
909
(:instance expt-weak-monotone (n j) (m (1+ i))))))))
911
(defthmd bvecp-bits-0
913
(equal (bits x i j) 0))
914
:hints (("Goal" :cases ((< i j))
915
:in-theory (set-difference-theories
919
;add case-split to hyps?
921
(defthm bits-drop-from-minus-original
922
(implies (and (<= y x)
926
(equal (bits (+ x (* -1 y)) (1- n) 0)
929
:hints (("Goal" :cases ((integerp n))
930
:in-theory (enable bvecp)))
933
;add case-split to hyps?
934
(defthm bits-drop-from-minus
935
(implies (and (bvecp x (1+ i))
938
(case-split (acl2-numberp i)))
939
(equal (bits (+ x (* -1 y)) i 0)
941
:hints (("Goal" :use ((:instance bits-drop-from-minus-original
943
:in-theory (disable bits-drop-from-minus-original))))
946
(implies (and (bvecp x (1+ i))
947
(case-split (acl2-numberp i)))
950
:hints (("Goal" :in-theory (enable bvecp bits-does-nothing))))
952
(defthm bits-tail-special
954
(equal (bits x (1- i) 0)
956
:hints (("Goal" :cases ((acl2-numberp i)))))
961
comments from bits.lisp (these may duplicate comments in this book)
964
(defthm bits-shift-out-even
965
(implies (and (integerp x)
971
(bits (/ x 2) (- i 1) (- j 1) )))
972
:hints (("Goal" :in-theory (enable expt-minus
975
expt-split-rewrite)))
981
;could use even-odd phrasing?
982
(defthm bits-down-to-1-case-split
983
(implies (and (integerp x)
988
(if (equal (bitn x 0) 0)
989
(/ (bits x i 0) 2) ;use the fact that we know bit 0 is 0?
990
(/ (1- (bits x i 0)) 2) ;use the fact that we know bit 0 is 1?
997
(IMPLIES (AND (INTEGERP N) (<= 0 N) (rationalP X) (<= 0 x))
998
(EQUAL (FLOOR (* 1/2 x) 1)
999
(FLOOR (* 1/2 (FLOOR x 1))
1002
:hints (("Goal" :in-theory (enable floor))))
1005
:hints (("Goal" :in-theory (set-difference-theories
1012
(IMPLIES (AND (INTEGERP N) (<= 0 N) (INTEGERP X))
1013
(EQUAL (FL (* 1/2 X (/ (EXPT 2 N))))
1014
(FL (* 1/2 (FL (* X (/ (EXPT 2 N))))))))
1016
:hints (("Goal" :in-theory (set-difference-theories
1022
;these may be made moot by my method of using lowbits with bits of a sum
1024
(defthm bits-sum-simplify-first-term
1025
(implies (and (>= (abs x) (expt 2 (+ j 1))) ;prevents loop
1031
(equal (bits (+ x y) j 0)
1032
(bits (+ (lowbits x j) y) j 0))))
1034
(defthm bits-sum-simplify-second-term
1035
(implies (and (>= (abs x) (expt 2 (+ j 1))) ;prevents loop
1041
(equal (bits (+ y x) j 0)
1042
(bits (+ (lowbits x j) y) j 0))))
1047
This series of events deals with simplifying expressions like
1050
Intuitively, bits 6 down-to 0 appear on both sides of the sum and should be "cancelled".
1051
The remaining bits will need to be "shifted" back into place.
1053
More rules are probably needed to make the theory complete.
1056
(defthm bits-cancel-lowbits-in-comparison
1057
(implies (and (> i+ i)
1065
(equal (equal (+ k (bits x i j))
1067
(equal (* (expt 2 (+ 1 i (- j)))
1068
(BITS X I+ (+ 1 I)))
1071
(defthm bits-cancel-lowbits-in-comparison-alt-2
1072
(implies (and (> i+ i)
1080
(equal (equal (+ (bits x i j) k)
1082
(equal (* (expt 2 (+ 1 i (- j)))
1083
(BITS X I+ (+ 1 I)))
1088
;todo: rephrase the conclusion of the above by moving the "constant" (* 2 (EXPT 2 I) (/ (EXPT 2 J))) to the other
1090
;a good idea since k is usually divisible by that quantity (with the rule above, we often end up with an
1091
equality in which each side should have a power of 2 divided out of it
1092
; not needed if we have good meta rules for cancelling factors from an inequality
1095
(defthm bits-cancel-lowbits-in-comparison-2
1096
(implies (and (> i+ i)
1105
(equal (equal (+ k (bits x i j))
1108
(BITS X I+ (+ 1 I)))
1109
(/ k (expt 2 (+ 1 i (- j))))))))
1114
(defthm bits-cancel-lowbits-in-comparison-3
1115
(implies (and (> i+ i)
1124
(equal (equal (+ (bits x i+ j) k)
1126
(equal (* (expt 2 (+ 1 i (- j )))
1127
(BITS X I+ (+ 1 I)))
1131
(defthm bits-cancel-lowbits-in-comparison-no-constant
1132
(implies (and (> i+ i)
1139
(equal (equal (bits x i j)
1141
(equal (* 2 (EXPT 2 I)
1143
(BITS X I+ (+ 1 I)))
1146
(defthm bits-cancel-lowbits-in-comparison-no-constant-2
1147
(implies (and (> i+ i)
1154
(equal (equal (bits x i+ j)
1156
(equal (* 2 (EXPT 2 I)
1158
(BITS X I+ (+ 1 I)))
1160
;the theory above (cancelling bits in comparisons) is not complete
1161
;it should also deal with bitn
1162
;perhaps a meta rule would be a good idea here?
1165
(defthm bits-shift-alt
1166
(implies (and (syntaxp (should-have-a-2-factor-divided-out x))
1167
(> j 0) ;restricts application
1173
(bits (/ x 2) (- i 1) (- j 1)))))
1175
(defthm bits-turn-bound-into-equal
1176
(implies (and (syntaxp (quotep k))
1177
(equal k (+ -2 (expt 2 (+ 1 i (- j)))))
1178
(case-split (<= j i))
1179
(case-split (rationalp x))
1180
(case-split (integerp i))
1181
(case-split (integerp j))
1182
(case-split (rationalp k))
1184
(equal (< k (bits x i j))
1185
(equal (bits x i j) (+ k 1))))
1186
:hints (("Goal" :in-theory (disable bits-upper-bound-tighter
1189
:use bits-upper-bound-tighter))
1198
;(in-theory (disable nbits-shift-out-even))
1207
(defthm bits-sum-drop-irrelevant-term-1-of-1
1208
(implies (and (rationalp x) ;(integerp x)
1215
(integerp (/ x (expt 2 (+ 1 i))))
1219
:hints (("Goal" :in-theory (enable bits bits)))
1220
:rule-classes ((:rewrite :backchain-limit-lst (nil nil nil nil nil 1)))
1224
(defthm bits-shift-better
1225
(implies (and (bind-free (can-take-out-numeric-power-of-2 x) (c))
1227
(case-split (integerp i))
1228
(case-split (integerp j))
1231
(bits (/ x c) (- i (expo c)) (- j (expo c))))))
1233
;high bits don't matter - add syntaxp hyp that one addend is a constant with high bits still present
1240
;It may be easier to reason about bits if we use this rule instead of expanding/enabling bits.
1241
(defthmd bits-alt-def
1243
(if (or (not (integerp i))
1246
(mod (fl (/ x (expt 2 j))) (expt 2 (+ 1 i (- j))))))
1247
:hints (("Goal" :in-theory (enable bits))))
1254
(defthm bits-bvecp-simple-2
1255
(bvecp (bits x (1- i) 0) i)
1256
:hints (("Goal" :cases ((acl2-numberp i)))))
1259
;Follows from BITS-SUM-DROP-IRRELEVANT-TERM-2-OF-2.
1261
(defthmd bits-plus-mult-2
1262
(implies (and (< n k)
1266
(equal (bits (+ x (* y (expt 2 k))) n m)
1268
:hints (("Goal" :cases ((integerp n))))) ;why cases hint needed?
1270
(defthmd bits-plus-mult-2-rewrite
1271
(implies (and (syntaxp (quotep c))
1272
(equal (mod c (expt 2 (1+ n))) 0))
1273
(equal (bits (+ c x) n m)
1275
:hints (("Goal" :use ((:instance bits-plus-mult-2
1277
(y (/ c (expt 2 (1+ n))))
1280
:in-theory (enable mod))))
1282
(defthm bits-plus-bits
1283
(implies (and (integerp m)
1289
(+ (bits x (1- p) m)
1290
(* (expt 2 (- p m)) (bits x n p)))))
1292
:hints (("Goal" :use ((:instance bits-plus-bits2 (i n) (j m) (n p))))))
1294
(defthm bits-less-than-x
1296
(<= (bits x i 0) x))
1297
:rule-classes (:rewrite :linear)
1298
:hints (("goal" :in-theory (enable bits))))
1300
(defthm bits-less-than-x-gen
1301
(implies (and (<= 0 x)
1302
(case-split (<= 0 j))
1303
(case-split (not (complex-rationalp x)))
1305
(<= (bits x i j) x))
1306
:rule-classes (:rewrite :linear)
1307
:hints (("goal" :in-theory (enable bits x-times-something>=1))))
1309
(defthm bits-bvecp-when-x-is
1310
(implies (and (bvecp x k)
1311
(case-split (<= 0 j))
1313
(bvecp (bits x i j) k))
1314
:hints (("Goal" :in-theory (enable bvecp))))
1316
(defthmd bits-bits-1
1317
(implies (and (<= k (- i j))
1318
(case-split (<= 0 l))
1319
(case-split (integerp i))
1320
(case-split (integerp j))
1321
(case-split (integerp k))
1322
(case-split (integerp l))
1324
(equal (bits (bits x i j) k l)
1325
(bits x (+ k j) (+ l j))))
1326
:hints (("Goal" :in-theory (enable bits expt-split))))
1328
(defthmd bits-bits-2
1329
(implies (and (> k (- i j))
1330
(case-split (<= 0 l))
1331
; (case-split (integerp i))
1332
(case-split (integerp j))
1333
(case-split (integerp k))
1334
(case-split (integerp l))
1336
(equal (bits (bits x i j) k l)
1337
(bits x i (+ l j))))
1338
:hints (("Goal" :in-theory (enable bits expt-split))))
1341
(implies (and (case-split (<= 0 l))
1342
(case-split (integerp i))
1343
(case-split (integerp j))
1344
(case-split (integerp k))
1345
(case-split (integerp l))
1347
(equal (bits (bits x i j) k l)
1349
(bits x (+ k j) (+ l j))
1350
(bits x i (+ l j)))))
1351
:hints (("Goal" :in-theory (enable bits-bits-1 bits-bits-2))))
1354
;The following trivial corollary of bits-bits is worth keeping enabled.
1356
(defthm bits-bits-constants
1357
(implies (and (syntaxp (quotep i))
1358
(syntaxp (quotep j))
1359
(syntaxp (quotep k))
1365
(equal (bits (bits x i j) k l)
1367
(bits x (+ k j) (+ l j))
1368
(bits x i (+ l j))))))
1372
(implies (and (< x (expt 2 (+ 1 i)))
1373
(case-split (integerp x))
1374
(case-split (<= 0 x))
1375
(case-split (integerp i))
1377
(equal (bits x i 0) x)))
1380
(equal (bits 0 i j) 0))
1386
;could prove a version where we drop bits from both args?
1387
(defthm bits-sum-drop-bits-around-arg-2
1388
(implies (and (<= i i+)
1390
(case-split (integerp i+))
1392
(equal (bits (+ x (bits y i+ 0)) i j)
1393
(bits (+ x y) i j)))
1394
:hints (("Goal" :in-theory (enable bits))))
1396
;Follows from BITS-SUM-DROP-BITS-AROUND-ARG-2.
1397
(defthm bits-sum-drop-bits-around-arg-1
1398
(implies (and (<= i i+)
1400
(case-split (integerp i+))
1402
(equal (bits (+ (bits x i+ 0) y) i j)
1403
(bits (+ x y) i j))))
1405
(defthm bits-sum-drop-bits-around-arg-2-special-case
1406
(implies (integerp y) ;case-split?
1407
(equal (bits (+ x (bits y i 0)) i j)
1408
(bits (+ x y) i j))))
1410
(defthm bits-sum-drop-bits-around-arg-1-special-case
1411
(implies (integerp x) ;case-split?
1412
(equal (bits (+ (bits x i 0) y) i j)
1413
(bits (+ x y) i j))))
1416
;Follows from BVECP-SUM-OF-BVECPS.
1418
(equal (bits (+ (bits x (1- i) 0)
1420
i ;actually, this could be anything >= i ??
1422
(+ (bits x (1- i) 0)
1424
:hints (("Goal" :in-theory (enable bits-tail))))
1429
(defthmd bits-of-non-integer-special
1430
(implies (case-split (not (integerp i)))
1431
(equal (BITS X (1- i) 0)
1435
(defthmd bits-fl-helper
1436
(implies (and (<= 0 j)
1439
(equal (bits (fl x) i j)
1441
:hints (("Goal" :in-theory (enable bits mod-fl-eric)))))
1445
(equal (bits (fl x) i j)
1447
:hints (("Goal" :use bits-fl-helper)))
1449
(defthmd bits-shift-down-eric
1450
(implies (and (<= 0 j)
1455
(equal (bits (* x (/ (expt 2 k)))
1458
(bits x (+ i k) (+ j k))))
1459
:hints (("Goal" :in-theory (e/d (expt-minus) (bits-shift))
1460
:use (:instance bits-shift (n (- k))))))
1462
(defthmd bits-shift-down-1
1463
(implies (and (<= 0 j)
1468
(equal (bits (fl (/ x (expt 2 k)))
1471
(bits x (+ i k) (+ j k))))
1472
:hints (("Goal" :in-theory (enable bits-fl bits-shift-down-eric))))
1475
(defthm bits-fl-by-2-helper
1476
(implies (and (integerp i)
1479
(equal (fl (* 1/2 (bits x i 0))) ;gen 0 to j?
1482
:hints (("Goal" :in-theory (disable LESS-THAN-MULTIPLY-THROUGH-BY-INVERTED-FACTOR-FROM-LEFT-HAND-SIDE)
1483
:use ((:instance bits-shift-down-1 (k 1) (i (1- i)) (j 0))
1484
(:instance bits-plus-bits (n i) (m 0) (p 1))
1485
(:instance fl-unique (x (/ (bits x i 0) 2)) (n (bits x i 1))))))))
1487
(defthmd bits-fl-by-2
1488
(equal (fl (* 1/2 (bits x i 0)))
1490
:hints (("Goal" :use (:instance bits-fl-by-2-helper))))
1492
(defthm mod-bits-by-2
1493
(implies (and (integerp x)
1497
(equal (mod (bits x i 0) 2)
1499
:hints (("Goal" :in-theory (enable bits))))
1506
(defthm bits-sum-drop-bits-around-arg-2-really-special-case
1507
(implies (rationalp y)
1508
(equal (bits (+ x (bits y i 0)) i 0)
1509
(bits (+ x y) i 0)))
1510
:hints (("Goal" :in-theory (enable bits)))))
1512
(defthm bits-sum-drop-bits-around-arg-1-really-special-case
1513
(implies (integerp x)
1514
(equal (bits (+ (bits x i 0) y) i 0)
1515
(bits (+ x y) i 0))))
1520
(defthm bits-shift-by-constant-power-of-2
1521
(implies (and (syntaxp (quotep k))
1523
(case-split (integerp i))
1524
(case-split (integerp j))
1526
(equal (bits (* k x) i j)
1527
(bits x (- i (expo k)) (- j (expo k)))))
1528
:hints (("Goal" :in-theory (enable power2p-rewrite))))
1531
(defthm bits-shift-second-with-more
1532
(implies (and ;(rationalp x)
1533
(case-split (integerp n))
1534
(case-split (integerp i))
1535
(case-split (integerp j))
1537
(equal (bits (* x (expt 2 n) y) i j)
1538
(bits (* x y) (- i n) (- j n))))
1539
:hints (("Goal" :in-theory (disable bits-shift)
1540
:use (:instance bits-shift (x (* x y))))))
1542
(defthmd bits-times-2
1543
(implies (and (acl2-numberp i)
1546
(equal (bits (* 2 x) i j)
1547
(bits x (1- i) (1- j))))
1548
:hints (("Goal" :use ((:instance bits-shift (n 1))))))
1550
(defthmd bits+2**k-2
1551
(implies (and (< x (expt 2 k))
1553
(rationalp x) ;(integerp x)
1556
(case-split (integerp m))
1557
(case-split (integerp n))
1558
(case-split (integerp k))
1560
(equal (bits (+ x (* y (expt 2 k))) n m)
1561
(bits y (- n k) (- m k))))
1562
:hints (("goal" :in-theory (disable FL-EQUAL-0)
1563
:use ((:instance bits-shift-down-1
1564
(x (+ x (* y (expt 2 k))))
1567
(:instance fl-unique (x (/ (+ x (* y (expt 2 k))) (expt 2 k))) (n y))))))
1569
(defthm bits+2**k-2-alt
1570
(implies (and (< x (expt 2 k))
1572
(rationalp x) ;(integerp x)
1575
(case-split (integerp m))
1576
(case-split (integerp n))
1577
(case-split (integerp k))
1579
(equal (bits (+ x (* (expt 2 k) y)) n m)
1580
(bits y (- n k) (- m k))))
1582
:hints (("Goal" :in-theory (disable bits+2**k-2)
1583
:use (:instance bits+2**k-2))))
1585
;basically the same as bits+2**k-2; drop one?
1587
(defthmd bits-plus-mult-1
1588
(implies (and (bvecp x k) ;actually, x need not be an integer...
1591
(case-split (integerp m))
1592
(case-split (integerp n))
1593
(case-split (integerp k))
1595
(equal (bits (+ x (* y (expt 2 k))) n m)
1596
(bits y (- n k) (- m k))))
1597
:hints (("Goal" :in-theory (enable bvecp)
1598
:use (bits+2**k-2))))
1601
(implies (and (integerp x)
1607
(iff (= (mod x (expt 2 (+ m n 1))) 0)
1608
(and (= (bits x (+ m n) n) 0)
1609
(= (mod x (expt 2 n)) 0))))
1611
:hints (("goal" :in-theory (e/d (bits expt-split) (BITS-FL))
1612
:use ((:instance mod-0-0 (m x) (n (expt 2 n)) (p (expt 2 (1+ m))))
1613
(:instance bits-shift-down-1 (k n) (i m) (j 0))))))
1615
;this is silly? just open up bits!
1616
(defthm mod-bits-equal
1617
(implies (= (mod x (expt 2 (1+ i))) (mod y (expt 2 (1+ i))))
1618
(= (bits x i j) (bits y i j)))
1620
:hints (("Goal" :in-theory (enable bits))))
1622
(defthmd mod-bits-equal-cor
1623
(implies (and (integerp x)
1628
(equal (bits (mod x (expt 2 n)) i j)
1630
:hints (("Goal" :use ((:instance mod-bits-equal
1631
(x (mod x (expt 2 n)))
1634
;not needed? just expand bits?
1636
(implies (and (case-split (integerp x))
1637
(case-split (integerp i)) ;gen?
1638
;(case-split (<= 0 i))
1641
(mod x (expt 2 (1+ i)))))
1643
:cases ((rationalp i) (complex-rationalp i))
1644
:in-theory (e/d (bits) ( EXPT-SPLIT)))))
1646
(defthmd bits-bits-sum
1647
(implies (and (integerp x)
1650
(equal (bits (+ (bits x i 0) y) i 0)
1651
(bits (+ x y) i 0)))
1652
:hints (("Goal" :in-theory (enable bits mod-sum))))
1654
;reorder? make rewrite?
1655
(defthm bits-shift-up-2
1656
(implies (and (integerp x)
1661
(equal (* (expt 2 k) (bits x i 0))
1662
(bits (* (expt 2 k) x) (+ i k) 0)))
1664
;:hints (("Goal" :cases ((equal 0 k))))
1670
(implies (and (case-split (integerp i))
1671
(case-split (integerp j))
1672
(case-split (integerp k))
1674
(equal (bits (expt 2 k) i j)
1681
:hints (("Goal" :use (:instance bits-shift (x 1) (n k))))
1685
(natp (bits x i j)))
1688
(defthmd bits-shift-down-eric
1689
(implies (and (<= 0 j)
1694
(equal (bits (* x (/ (expt 2 k)))
1697
(bits x (+ i k) (+ j k))))
1698
:hints (("Goal" :use (:instance bits-shift-down-1)))
1703
(implies (and (<= 0 i)
1707
(equal (mod (bits x i 0) (expt 2 j))
1708
(bits x (min i (1- j)) 0)))
1709
:hints (("Goal" :in-theory (enable bits)))
1712
(defthm bits-expt-constant
1713
(implies (and (syntaxp (and (quotep k) (power2p (cadr k))))
1715
(case-split (integerp k)) ;gen?
1716
(case-split (integerp i))
1717
(case-split (integerp j))
1724
(expt 2 (- (expo k) j)))))
1725
:hints (("Goal" :in-theory (enable power2p-rewrite))))
1729
(defthm bits-minus-better-helper-1
1730
(implies (and (integerp x)
1732
(equal (equal 0 (bits x i 0))
1733
(integerp (* 1/2 x (/ (expt 2 i))))
1735
:hints (("Goal" :in-theory (enable expt-split mod-equal-0)
1736
:expand (BITS X I 0)))
1739
(defthm bits-minus-better-helper-2
1740
(implies (and (integerp x)
1742
(equal (equal 0 (bits x (1- j) 0))
1743
(integerp (* x (/ (expt 2 j))))
1745
:hints (("Goal" :in-theory (enable expt-split mod-equal-0)
1746
:expand (bits x (1- j) 0)))
1749
;note that although the RHS looks slightly gross,
1750
;gen the (integerp x) hyp!!
1751
(defthm bits-minus-better
1752
(implies (and (case-split (integerp x)) ;gen!
1753
(case-split (integerp i))
1754
(case-split (<= j i)) ;drop?
1755
(case-split (integerp j))
1757
(equal (bits (* -1 x) i j)
1758
(if (equal 0 (bits x i 0))
1760
(if (equal 0 (bits x (1- j) 0))
1761
(+ (* 2 (expt 2 i) (/ (expt 2 j))) (- (bits x i j)))
1762
(+ -1 (* 2 (expt 2 i) (/ (expt 2 j))) (- (bits x i j)))))))
1763
:hints (("Goal" :use bits-minus
1764
:in-theory (enable mod-does-nothing expt-split mod-cancel)))
1770
;Unlike bits-tail, this allows j to be non-zero.
1771
;Note that the conclusion is (bits x ...), not just x.
1772
;i is a free variable
1773
;watch out for loops with this rule
1774
;BOZO export in lib/ or user/!
1775
(defthm bits-tighten
1776
(implies (and (bvecp x i)
1778
(case-split (integerp n))
1782
:rule-classes ((:rewrite :match-free :all))
1783
:hints (("goal" :use (:instance expt-weak-monotone (n i) (m (+ 1 n)))
1784
:in-theory (e/d (bits bvecp) (expt-compare)))))
1787
(implies (and (integerp x)
1791
(equal (bits x (1- i) j)
1792
(- (fl (/ x (expt 2 j)))
1794
(fl (/ x (expt 2 i)))))))
1795
:hints (("Goal" :in-theory (enable bits mod))))
1798
(implies (and (< i 0)
1800
(equal (bits x i j) 0))
1801
:hints (("Goal" :in-theory (enable bits))))
1803
(defthmd bits-shift-down-2
1804
(implies (and (natp x)
1807
(equal (fl (/ (bits x (+ i k) 0) (expt 2 k)))
1808
(bits (fl (/ x (expt 2 k))) i 0)))
1809
:hints (("Goal" :use ((:instance bits-plus-bits (n (+ i k)) (m 0) (p k)))
1810
:in-theory (enable bits-shift-down-1))))
added
removed
books/rtl/rel6/support/support/bits-proofs.lisp
