5
(include-book "../lib1/top")
7
(set-inhibit-warnings "theory")
9
;;;**********************************************************************
11
;;;**********************************************************************
13
;; (defund trunc (x n)
14
;; (declare (xargs :guard (integerp n)))
16
;; (fl (* (expt 2 (1- n)) (sig x)))
17
;; (expt 2 (- (1+ (expo x)) n))))
19
;; (defthmd trunc-integer-type-prescription
20
;; (implies (and (>= (expo x) n)
21
;; (case-split (integerp n))
23
;; (integerp (trunc x n)))
24
;; :rule-classes :type-prescription)
26
;; (defthmd trunc-rewrite
27
;; (implies (and (rationalp x)
32
;; (fl (* (expt 2 (- (1- n) (expo x))) (abs x)))
33
;; (expt 2 (- (1+ (expo x)) n))))))
36
;; (equal (abs (trunc x n))
37
;; (* (fl (* (expt 2 (1- n)) (sig x))) (expt 2 (- (1+ (expo x)) n)))))
43
;; (defthm fl-sig-expt-2-lemma-1
44
;; (implies (and (<= n 0)
46
;; (< (* (SIG X) (EXPT 2 (+ -1 N))) 1))
47
;; :hints (("Goal" :in-theory (enable expt-weak-monotone-linear)
48
;; :cases ((not (<= (expt 2 (+ -1 n)) (/ 2)))))
50
;; :use ((:instance sig-upper-bound)))
52
;; :use ((:instance expt-weak-monotone-linear
59
;; (implies (and (rationalp x)
63
;; :rule-classes nil))
68
;; (defthm fl-sig-expt-2
69
;; (implies (and (<= n 0)
72
;; (equal (fl (* (SIG X) (EXPT 2 (+ -1 N)))) 0))
73
;; :hints (("Goal" :use ((:instance fl-is-0
75
;; (expt 2 (+ -1 n)))))
76
;; (:instance sig-lower-bound))))))
80
;; (implies (and (rationalp x)
83
;; (equal (trunc x n) 0))
84
;; :hints (("Goal" :in-theory (enable trunc)))))
86
;; ;; moved to trunc.lisp
88
;; (implies (and (rationalp x)
91
;; (equal (trunc x n) 0))
92
;; :hints (("Goal" :in-theory (enable trunc))))
96
;; (implies (and (< 0 n)
99
;; (equal (sgn (trunc x n))
104
(local (include-book "../support/trunc"))
105
(set-enforce-redundancy nil)
107
(implies (and (integerp n)
109
(equal (trunc x n) 0))))
111
; (set-enforce-redundancy t)
113
;; (defthm trunc-positive
114
;; (implies (and (< 0 x)
115
;; (case-split (rationalp x))
116
;; (case-split (integerp n))
117
;; (case-split (< 0 n))
119
;; (< 0 (trunc x n)))
120
;; :rule-classes (:rewrite :linear))
123
;; (defthm trunc-negative
124
;; (implies (and (< x 0)
125
;; (case-split (rationalp x))
126
;; (case-split (integerp n))
127
;; (case-split (< 0 n)))
128
;; (< (trunc x n) 0))
129
;; :rule-classes (:rewrite :linear))
133
;; (equal (trunc 0 n) 0))
136
;; (defthmd trunc-minus
137
;; (equal (trunc (* -1 x) n)
138
;; (* -1 (trunc x n))))
141
;; (defthmd trunc-shift
142
;; (implies (integerp n)
143
;; (equal (trunc (* x (expt 2 k)) n)
144
;; (* (trunc x n) (expt 2 k)))))
147
;; (defthmd trunc-upper-bound
148
;; (implies (and (rationalp x)
150
;; (<= (abs (trunc x n)) (abs x)))
151
;; :rule-classes :linear)
153
;; (defthmd trunc-upper-pos
154
;; (implies (and (<= 0 x)
157
;; (<= (trunc x n) x))
158
;; :rule-classes :linear)
161
;; (defthm expo-trunc
162
;; (implies (and (< 0 n)
165
;; (equal (expo (trunc x n))
169
;; (defthm expo-trunc-strong
170
;; (implies (and (nat n)
173
;; (equal (expo (trunc x n))
177
(set-enforce-redundancy nil)
180
(local (include-book "../support/trunc"))
181
(defthmd trunc-lower-bound
182
(implies (and (rationalp x)
184
(> (abs (trunc x n)) (- (abs x) (expt 2 (- (1+ (expo x)) n)))))
185
:hints (("Goal" :by trunc-lower-1))
186
:rule-classes (:linear))
188
(defthmd trunc-lower-2
189
(implies (and (rationalp x)
193
(> (abs (trunc x n)) (* (abs x) (- 1 (expt 2 (- 1 n))))))
194
:rule-classes :linear)
196
(defthmd trunc-lower-2-pos
197
(implies (and (rationalp x)
201
(> (trunc x n) (* x (- 1 (expt 2 (- 1 n))))))
202
:rule-classes :linear
203
:hints (("Goal" :by trunc-lower-pos))))
205
;; moved into trunc.lisp ??
208
;----------------------------------------------------------------------
210
;; (defthm trunc-diff
211
;; (implies (and (rationalp x)
214
;; (< (abs (- x (trunc x n))) (expt 2 (- (1+ (expo x)) n))))
217
;; (defthm trunc-diff-pos
218
;; (implies (and (rationalp x)
222
;; (< (- x (trunc x n)) (expt 2 (- (1+ (expo x)) n))))
226
;; (defthm trunc-exactp-a
227
;; (exactp (trunc x n) n)
228
;; :hints (("Goal" :use ((:instance trunc-exactp-b---rtl-rel5-support)))))
231
;; (defthm trunc-diff-expo
232
;; (implies (and (rationalp x)
233
;; (not (exactp x n))
236
;; (<= (expo (- x (trunc x n))) (- (expo x) n)))
240
;; (defthm trunc-exactp-b
241
;; (implies (and (rationalp x)
244
;; (iff (= x (trunc x n))
246
;; :hints (("Goal" :use ((:instance trunc-exactp-a---rtl-rel5-support))))
250
;; (defthmd trunc-exactp-c
251
;; (implies (and (exactp a n)
256
;; (<= a (trunc x n))))
259
;; (defthmd trunc-monotone
260
;; (implies (and (<= x y)
264
;; (<= (trunc x n) (trunc y n)))
265
;; :rule-classes :linear)
267
;----------------------------------------------------------------------
270
;; (defthm trunc-diff
271
;; (implies (and (rationalp x)
274
;; (< (abs (- x (trunc x n))) (expt 2 (- (1+ (expo x)) n))))
277
;; (defthm exactp-diff-cor
278
;; (implies (and (rationalp x)
284
;; (<= (abs (- x y)) (abs x))
285
;; (<= (abs (- x y)) (abs y)))
286
;; (exactp (- x y) n))
291
(local (include-book "../../arithmetic/basic"))
293
(defthm not-exact-strictly-greater-than
294
(implies (and (rationalp x)
299
(> x (expt 2 (expo x))))
300
:hints (("Goal" :in-theory (enable exactp-2**n)
301
:cases ((= x (expt 2 (expo x)))))
302
("Subgoal 2" :use ((:instance expo-lower-bound))))))
305
;; (implies (and (rationalp x)
318
(defthm strictly-greater-than-implies-no-less-than-fp+
319
(implies (and (rationalp x)
321
(> x (expt 2 (expo x)))
324
(>= x (+ (expt 2 (expo x))
325
(expt 2 (- (EXPO X) N)))))
326
:hints (("Goal" :in-theory (enable exactp-2**n)
327
:use ((:instance fp+2
328
(x (expt 2 (expo x)))
332
;; (defthmd expo-monotone
333
;; (implies (and (<= (abs x) (abs y))
334
;; (case-split (rationalp x))
335
;; (case-split (not (equal x 0)))
336
;; (case-split (rationalp y)))
337
;; (<= (expo x) (expo y)))
338
;; :rule-classes :linear)
341
(defthm expo-of-x-minus-extra-bit-is-expo-x
342
(implies (and (exactp x (1+ n))
348
(equal (expo (+ x (* -1 (expt 2 (+ (expo x) (* -1 n))))))
350
:hints (("Goal" :in-theory (enable exactp-2**n)
351
:use ((:instance expo-monotone
352
(x (- x (expt 2 (- (expo x) n))))
354
(:instance expo-monotone
355
(x (expt 2 (expo x)))
356
(y (- x (expt 2 (- (expo x) n)))))
357
(:instance strictly-greater-than-implies-no-less-than-fp+))))))
359
;; next we want to prove (- x (expt 2 (- (exp x) n))) is exactp n
363
(local (include-book "../../arithmetic/even-odd"))
364
(defthm integerp-x-not-1/2x-lemma
365
(implies (and (integerp x)
366
(not (integerp (* x (/ 2)))))
367
(integerp (+ (* x (/ 2)) (* -1 (/ 2))))))))
369
;; may need some rule to merge 1/2 into expt 2
371
(defthm merged-1/2-into-expt2
372
(implies (and (integerp n)
374
(equal (* 1/2 x (expt 2 n))
375
(* x (expt 2 (+ -1 n)))))
385
(implies (and (not (exactp x n))
391
(exactp (+ x (* -1 (expt 2 (+ (expo x) (* -1 n)))))
393
:hints (("Goal" :in-theory (enable exactp2 a15)
394
:use ((:instance integerp-x-not-1/2x-lemma
395
(x (* X (EXPT 2 (+ N (* -1 (EXPO X))))))))))))
398
;; (implies (and (rationalp x)
403
;; (exactp (fp+ x n) n))
408
;; (defthm not-exact-strictly-greater-than
409
;; (implies (and (rationalp x)
410
;; (not (exactp x n))
414
;; (> x (expt 2 (expo x))))
415
;; :hints (("Goal" :in-theory (enable exactp-2**n)
416
;; :cases ((= x (expt 2 (expo x)))))
417
;; ("Subgoal 2" :use ((:instance expo-lower-bound))))))
421
(defthm expt-2-minus-half
422
(implies (integerp n)
423
(equal (+ (EXPT 2 (+ 1 n))
432
;;; lots of stupid lemmas!!
436
(implies (and (not (exactp x n))
442
(exactp (+ x (expt 2 (+ (expo x) (* -1 n)))) n))
444
:use ((:instance a-is-n-exact)
445
(:instance expo-lower-bound)
446
(:instance expt-strong-monotone-linear
448
(n (+ (expo x) (* -1 n))))
450
(x (- x (expt 2 (+ (expo x) (* -1 n)))))))))))
452
;; (defthmd trunc-exactp-c
453
;; (implies (and (exactp a n)
458
;; (<= a (trunc x n))))
461
(defthm trunc-midpoint-lemma
462
(implies (and (> n 0)
464
(rationalp x) (> x 0)
467
(= (- x (expt 2 (- (expo x) n)))
469
:hints (("Goal" :in-theory (enable trunc-upper-pos)
470
:cases ((< (- x (expt 2 (- (expo x) n))) (trunc x n))))
471
("Subgoal 2" :use ((:instance trunc-exactp-c
472
(a (- x (expt 2 (- (expo x) n)))))))
473
("Subgoal 1" :use ((:instance fp+2
475
(x (- x (expt 2 (- (expo x) n)))))
476
(:instance expo-lower-bound)
477
(:instance expt-strong-monotone-linear
479
(n (+ (expo x) (* -1 n)))))))
482
;; (defthmd sig-lower-bound
483
;; (implies (and (rationalp x)
484
;; (not (equal x 0)))
486
;; :rule-classes (:rewrite :linear))
489
;; (defthmd sig-upper-bound
491
;; :rule-classes (:rewrite :linear))
496
(defthm sig-x-integerp
497
(implies (and (integerp (sig x))
501
:hints (("Goal" :in-theory (enable sig-lower-bound
506
;;; The following are exported!!!
507
;;; Thu Oct 12 13:57:55 2006
509
(defthm trunc-midpoint
510
(implies (and (natp n)
511
(rationalp x) (> x 0)
514
(= (- x (expt 2 (- (expo x) n)))
516
:hints (("Goal" :cases ((equal n 0)))
517
("Subgoal 2" :use ((:instance trunc-midpoint-lemma)))
518
("Subgoal 1" :in-theory (enable exactp sgn trunc)
519
:use ((:instance fp-rep (x x)))))
523
(defthm expo-of-x-minus-extra-bit-is-expo-x
524
(implies (and (exactp x (1+ n))
530
(equal (expo (+ x (* -1 (expt 2 (+ (expo x) (* -1 n))))))
536
(implies (and (not (exactp x n))
542
(exactp (+ x (* -1 (expt 2 (+ (expo x) (* -1 n)))))
548
(implies (and (not (exactp x n))
554
(exactp (+ x (expt 2 (+ (expo x) (* -1 n))))
560
;; TODO: consider move this to trunc.lisp and trunc-proofs.lisp
561
;; Thu Oct 12 09:28:40 2006
564
;----------------------------------------------------------------------
566
;; (defthmd trunc-trunc
567
;; (implies (and (>= n m)
570
;; (equal (trunc (trunc x n) m)
574
;; (defthm plus-trunc
575
;; (implies (and (rationalp x)
580
;; (exactp x (+ k (- (expo x) (expo y)))))
581
;; (= (+ x (trunc y k))
582
;; (trunc (+ x y) (+ k (- (expo (+ x y)) (expo y))))))
585
;----------------------------------------------------------------------
590
(defthm minus-trunc-1-lemma
591
(implies (and (rationalp x)
598
(> (+ k (- (expo (- x y)) (expo y))) 0)
599
(= n (+ k (- (expo x) (expo y)))) ;; why we need "n"??
600
(exactp x (+ k (- (expo x) (expo y)))))
601
(equal (- x (trunc y k))
602
(trunc (- x y) (+ k (- (expo (- x y)) (expo y))))))
603
:hints (("Goal" :in-theory (enable trunc-rewrite exactp2 sgn a15)
604
:use ((:instance fl+int-rewrite
605
(x (* Y (EXPT 2 (+ -1 K (* -1 (EXPO Y))))))
606
(n (* -1 X (EXPT 2 (+ -1 K (* -1 (EXPO Y))))))))))))
609
(defthm minus-trunc-1
610
(implies (and (rationalp x)
617
(> (+ k (- (expo (- x y)) (expo y))) 0)
618
(= n (+ k (- (expo x) (expo y)))) ;; why we need "n"??
619
(exactp x (+ k (- (expo x) (expo y)))))
620
(equal (- x (trunc y k))
621
(- (trunc (- y x) (+ k (- (expo (- x y)) (expo y)))))))
622
:hints (("Goal" :use ((:instance trunc-minus
624
(n (+ k (- (expo (- x y)) (expo y)))))
625
(:instance minus-trunc-1-lemma))))
631
;----------------------------------------------------------------------
633
;; (defthm bits-trunc
634
;; (implies (and (= n (1+ (expo x)))
639
;; (* (expt 2 (- n k))
640
;; (bits x (1- n) (- n k)))))
641
;; :hints (("Goal" :use ((:instance bits-trunc-2---rtl-rel5-support))))
645
;; (defthm trunc-land
646
;; (implies (and (>= x (expt 2 (1- n)))
648
;; (integerp x) (> x 0)
649
;; (integerp m) (>= m n)
650
;; (integerp n) (> n k)
651
;; (integerp k) (> k 0))
653
;; (land x (- (expt 2 m) (expt 2 (- n k))) n)))
654
;; :hints (("Goal" :use ((:instance bits-trunc-
658
;; make change directly into rel5/lib/round.lisp, rel5/support/lextra.lisp
661
;; (defthmd trunc-split
662
;; (implies (and (= n (1+ (expo x)))
668
;; (equal (trunc x m)
670
;; (* (expt 2 (- n m))
671
;; (bits x (1- (- n k)) (- n m)))))))
674
;;;**********************************************************************
675
;;; Rounding Away from Zero
676
;;;**********************************************************************
679
;; (defund away (x n)
681
;; (cg (* (expt 2 (1- n)) (sig x)))
682
;; (expt 2 (- (1+ (expo x)) n))))
685
(defthmd away-integer-type-prescription
686
(implies (and (>= (expo x) n)
687
(case-split (integerp n))
689
(integerp (away x n)))
690
:hints (("Goal" :in-theory (enable away)))
691
:rule-classes :type-prescription)
693
;; (defthmd away-rewrite
694
;; (implies (and (rationalp x)
699
;; (cg (* (expt 2 (- (1- n) (expo x))) (abs x)))
700
;; (expt 2 (- (1+ (expo x)) n))))))
704
;; (implies (and (rationalp x)
706
;; (equal (abs (away x n))
707
;; (* (cg (* (expt 2 (1- n)) (sig x))) (expt 2 (- (1+ (expo x)) n))))))
713
;; ;; (defthm fl-sig-is-minus-1
714
;; ;; (implies (and (rationalp x)
715
;; ;; (not (equal x 0)))
716
;; ;; (equal (FL (* -1/2 (SIG X)))
718
;; ;; :hints (("Goal"
719
;; ;; :in-theory (enable fl-minus)
720
;; ;; :use ((:instance sig-upper-bound)
721
;; ;; (:instance sig-lower-bound))))))
726
(local (include-book "../support/away"))
728
(implies (and (<= n 0)
733
(* (sgn x) (expt 2 (+ 1 (expo x) (- n))))))
734
:hints (("Goal" :by away-to-0-or-fewer-bits))))
740
;; (implies (and (rationalp x) (not (= x 0)))
742
;; (* (sgn x) (expt 2 (1+ (expo x))))))
744
;; druss this is what you wrote in the lemma
749
;; (equal (sgn (away x n))
752
;; (defthm away-positive
753
;; (implies (and (< 0 x)
754
;; (case-split (rationalp x))
757
;; :rule-classes (:rewrite :linear))
759
;; (defthm away-negative
760
;; (implies (and (< x 0)
761
;; (case-split (rationalp x))
764
;; :rule-classes (:rewrite :linear))
767
;; (equal (away 0 n) 0))
770
;; (defthmd away-minus
771
;; (= (away (* -1 x) n) (* -1 (away x n))))
774
;; (defthmd away-shift
775
;; (implies (integerp n)
776
;; (= (away (* x (expt 2 k)) n)
777
;; (* (away x n) (expt 2 k)))))
780
;; (defthmd away-lower-bound
781
;; (implies (and (case-split (rationalp x))
782
;; (case-split (integerp n)))
783
;; (>= (abs (away x n)) (abs x)))
784
;; :rule-classes :linear)
786
;; (defthmd away-lower-pos
787
;; (implies (and (>= x 0)
788
;; (case-split (rationalp x))
789
;; (case-split (integerp n)))
790
;; (>= (away x n) x))
791
;; :rule-classes :linear)
794
;; ;----------------------------------------------------------------------
796
(defthmd away-upper-bound
797
(implies (and (rationalp x)
800
(< (abs (away x n)) (+ (abs x) (expt 2 (- (1+ (expo x)) n)))))
801
:hints (("Goal" :use away-upper-1))
802
:rule-classes :linear)
804
;; ;----------------------------------------------------------------------
806
;; (defthmd away-upper-2
807
;; (implies (and (rationalp x)
811
;; (< (abs (away x n)) (* (abs x) (+ 1 (expt 2 (- 1 n))))))
812
;; :rule-classes :linear)
815
;; (defthmd away-diff
816
;; (implies (and (rationalp x)
819
;; (< (abs (- (away x n) x)) (expt 2 (- (1+ (expo x)) n))))
820
;; :rule-classes :linear)
822
;; (defthmd away-diff-pos
823
;; (implies (and (rationalp x)
827
;; (< (- (away x n) x) (expt 2 (- (1+ (expo x)) n))))
828
;; :rule-classes :linear)
830
;; ;; (defthm away-exactp-d
831
;; ;; (implies (and (rationalp x)
835
;; ;; (<= (abs (away x n)) (expt 2 (1+ (expo x)))))
836
;; ;; :rule-classes ())
838
(defthm away-expo-upper
839
(implies (and (rationalp x)
842
(<= (abs (away x n)) (expt 2 (1+ (expo x)))))
844
:cases ((equal n 0)))
845
("Subgoal 2" :use ((:instance away-exactp-d)))
846
("Subgoal 1" :in-theory (enable abs away sgn natp)))
850
;; (defthmd expo-away-lower-bound
851
;; (implies (and (rationalp x)
853
;; (>= (expo (away x n)) (expo x)))
854
;; :hints (("Goal" :cases ((equal n 0)))
855
;; ("Subgoal 2" :use ((:instance
856
;; expo-away-lower-bound---rtl-rel5-support)))
857
;; ("Subgoal 1" :cases ((equal x 0))
858
;; :in-theory (enable sgn))
859
;; ("Subgoal 1.2" :use ((:instance expo-prod-lower
861
;; (y (expt 2 (+ 1 (expo x))))))))
862
;; :rule-classes (:linear))
864
;; included in round.lisp already.
865
;; Thu Oct 12 10:15:13 2006. Fixed (and (integerp n) (> n 0)) into (natp n)
870
(defthm away-x-zero-implies-zero
871
(implies (rationalp x)
872
(equal (equal (away x n) 0)
874
:hints (("Goal" :cases ((< 0 x)
878
(defthmd expo-away-upper-bound
879
(implies (and (rationalp x)
881
(<= (expo (away x n)) (1+ (expo x))))
882
:hints (("Goal" :in-theory (enable expo-monotone)
883
:cases ((equal x 0)))
885
:use ((:instance away-expo-upper)
886
(:instance expo-monotone
888
(y (expt 2 (+ 1 (expo x)))))
889
(:instance expo-monotone
890
(x (* -1 (away x n)))
891
(y (expt 2 (+ 1 (expo x))))))))
892
:rule-classes :linear))
895
;; TODO: refactor into away.lisp!!!
896
;; Thu Oct 12 10:17:09 2006
900
;; (implies (and (rationalp x)
902
;; (not (= (abs (away x n)) (expt 2 (1+ (expo x))))))
903
;; (equal (expo (away x n))
905
;; :hints (("Goal" :cases ((equal x 0) (< x 0) (> x 0)))
906
;; ("Subgoal 2" :in-theory (enable sgn)
907
;; :use ((:instance expo-away---rtl-rel5-support)))
908
;; ("Subgoal 1" :in-theory (enable sgn)
909
;; :use ((:instance expo-away---rtl-rel5-support)))))
912
;; (defthm away-exactp-a
913
;; (implies (case-split (< 0 n))
914
;; (exactp (away x n) n))
915
;; :hints (("Goal" :use ((:instance away-exactp-b---rtl-rel5-support)))))
918
;; (defthmd away-diff-expo
919
;; (implies (and (rationalp x)
920
;; (not (exactp x n))
923
;; (<= (expo (- (away x n) x)) (- (expo x) n)))
924
;; :rule-classes :linear)
927
;; (defthm away-exactp-b
928
;; (implies (and (rationalp x)
931
;; (iff (= x (away x n))
933
;; :hints (("Goal" :use ((:instance away-exactp-a---rtl-rel5-support))))
936
;; (defthmd away-exactp-c
937
;; (implies (and (exactp a n)
945
;; (>= a (away x n))))
947
;; (defthmd away-exactp-c
948
;; (implies (and (exactp a n)
954
;; (>= a (away x n))))
957
;; (defthmd away-monotone
958
;; (implies (and (rationalp x)
962
;; (<= (away x n) (away y n)))
963
;; :rule-classes :linear)
966
;; (defthm trunc-away
967
;; (implies (and (rationalp x) (> x 0)
968
;; (integerp n) (> n 0)
969
;; (not (exactp x n)))
972
;; (expt 2 (+ (expo x) 1 (- n))))))
975
;----------------------------------------------------------------------
980
(defthm local-expt-expand
981
(implies (integerp n)
982
(equal (EXPT 2 (+ 1 n))
984
:hints (("Goal" :use ((:instance a15
990
(defthm away-midpoint-lemma
991
(implies (and (> n 0)
993
(rationalp x) (> x 0)
996
(= (+ x (expt 2 (- (expo x) n)))
998
:hints (("Goal" :in-theory (enable a15)
999
:use ((:instance trunc-away)
1000
(:instance trunc-midpoint)
1001
(:instance local-expt-expand
1002
(n (expt 2 (+ (expo x) (* -1 n))))))))
1007
(defthm sig-x-integerp
1008
(implies (and (integerp (sig x))
1012
:hints (("Goal" :in-theory (enable sig-lower-bound
1013
sig-upper-bound)))))
1015
(defthm away-midpoint
1016
(implies (and (natp n)
1017
(rationalp x) (> x 0)
1021
(+ x (expt 2 (- (expo x) n)))))
1022
:hints (("Goal" :cases ((equal n 0)))
1023
("Subgoal 2" :use away-midpoint-lemma)
1024
("Subgoal 1" :in-theory (enable exactp sgn)
1025
:use ((:instance fp-rep (x x)))))
1029
;----------------------------------------------------------------------
1031
;; (defthmd away-away
1032
;; (implies (and (rationalp x)
1038
;; (equal (away (away x n) m)
1042
;; (defthm plus-away
1043
;; (implies (and (exactp x (+ k (- (expo x) (expo y))))
1049
;; (= (+ x (away y k))
1051
;; (+ k (- (expo (+ x y)) (expo y))))))
1052
;; :rule-classes ())
1054
;----------------------------------------------------------------------
1058
;; (defthm minus-trunc-1
1059
;; (implies (and (rationalp x)
1066
;; (> (+ k (- (expo (- x y)) (expo y))) 0)
1067
;; (= n (+ k (- (expo x) (expo y)))) ;; why we need "n"??
1068
;; (exactp x (+ k (- (expo x) (expo y)))))
1069
;; (equal (- x (trunc y k))
1070
;; (- (trunc (- y x) (+ k (- (expo (- x y)) (expo y)))))))
1071
;; :hints (("Goal" :use ((:instance trunc-minus
1073
;; (n (+ k (- (expo (- x y)) (expo y)))))
1074
;; (:instance minus-trunc-1-lemma)))))
1077
(defthm minus-trunc-2
1078
(implies (and (rationalp x)
1085
(> (+ k (- (expo (- x y)) (expo y))) 0)
1086
(= n (+ k (- (expo x) (expo y)))) ;; why we need "n"??
1087
(exactp x (+ k (- (expo x) (expo y)))))
1088
(equal (- x (trunc y k))
1089
(away (- x y) (+ k (- (expo (- x y)) (expo y))))))
1090
:hints (("Goal" :in-theory (enable away-rewrite trunc-rewrite cg exactp2 sgn
1094
;----------------------------------------------------------------------
1099
(defthm trunc-minus-specific
1100
(equal (TRUNC (+ (* -1 X) (* -1 Y)) n)
1101
(* -1 (trunc (+ x y) n)))
1102
:hints (("Goal" :use ((:instance trunc-minus
1107
(defthm expo-minus-specific
1108
(equal (EXPO (+ (* -1 X) (* -1 Y)))
1110
:hints (("Goal" :use ((:instance expo-minus
1115
(defthm away-minus-specific
1116
(equal (away (+ (* -1 X) (* -1 Y)) n)
1117
(* -1 (away (+ x y) n)))
1118
:hints (("Goal" :use ((:instance away-minus
1124
(defthm trunc-plus-minus-lemmma
1125
(implies (and (rationalp x)
1132
(= k1 (+ k (- (expo x) (expo y))))
1133
(= k2 (+ k (expo (+ x y)) (* -1 (expo y))))
1136
(equal (+ x (trunc y k))
1137
(if (= (sgn (+ x y)) (sgn y))
1139
(away (+ x y) k2))))
1140
:hints (("Goal" :cases ((< y 0))
1141
:in-theory (enable sgn trunc-minus away-minus expo-minus))
1142
("Subgoal 2" :use ((:instance plus-trunc)))
1143
("Subgoal 1" :cases ((< (* -1 y) x)))
1144
("Subgoal 1.2" :use ((:instance minus-trunc-1
1147
("Subgoal 1.1" :use ((:instance minus-trunc-2
1151
(defthm trunc-plus-minus
1152
(implies (and (rationalp x)
1159
(= k1 (+ k (- (expo x) (expo y))))
1160
(= k2 (+ k (expo (+ x y)) (* -1 (expo y))))
1163
(equal (+ x (trunc y k))
1164
(if (= (sgn (+ x y)) (sgn y))
1166
(away (+ x y) k2))))
1168
:hints (("Goal" :cases ((not (< 0 x)))
1169
:in-theory (enable sgn trunc-minus away-minus expo-minus))
1170
("Subgoal 2" :use ((:instance trunc-plus-minus-lemmma)))
1171
("Subgoal 1" :use ((:instance trunc-plus-minus-lemmma
1178
;; (implies (and (rationalp x)
1187
;; (expt 2 (- (1+ (expo x)) n))
1188
;; (- (expt 2 (- (1+ (expo x)) m))))
1190
;; :rule-classes ())
1192
;;;**********************************************************************
1193
;;; Unbiased Rounding
1194
;;;**********************************************************************
1200
;; (defund near (x n)
1201
;; (let ((z (fl (* (expt 2 (1- n)) (sig x))))
1202
;; (f (re (* (expt 2 (1- n)) (sig x)))))
1212
;; (defthm near-choice
1213
;; (or (= (near x n) (trunc x n))
1214
;; (= (near x n) (away x n)))
1215
;; :rule-classes ())
1219
(implies (and (rationalp x)
1222
(equal (sgn (near x n))
1224
:hints (("Goal" :in-theory (enable sgn-near-2))))
1226
;; probably want to disable sgn-near in support/near.lisp
1227
;; this is what originall is sgn-near-2 in the rel5
1229
;; ;; (defthm near-pos
1230
;; ;; (implies (and (< 0 x)
1234
;; ;; (< 0 (near x n)))
1235
;; ;; :rule-classes (:TYPE-PRESCRIPTION :LINEAR))
1237
;; ;; (defthmd near-neg
1238
;; ;; (implies (and (< x 0)
1243
;; ;; (< (near x n) 0))
1244
;; ;; :rule-classes (:TYPE-PRESCRIPTION :LINEAR))
1246
;; ;; (defthm near-0
1247
;; ;; (equal (near 0 n)
1251
(defthm near-positive
1252
(implies (and (< 0 x)
1257
:hints (("Goal" :by near-pos))
1258
:rule-classes (:type-prescription :linear))
1260
(defthmd near-negative
1261
(implies (and (< x 0)
1267
:hints (("Goal" :in-theory (enable near-neg)))
1268
:rule-classes (:type-prescription :linear))
1275
;; (defthm near-exactp-a
1277
;; (exactp (near x n) n))
1278
;; :hints (("Goal" :use ((:instance near-exactp-b---rtl-rel5-support)))))
1281
;; (defthm near-exactp-b
1282
;; (implies (and (rationalp x)
1285
;; (iff (= x (near x n))
1287
;; :hints (("Goal" :use ((:instance near-exactp-a---rtl-rel5-support))))
1288
;; :rule-classes ())
1294
;; (defthmd near-minus
1295
;; (equal (near (* -1 x) n)
1296
;; (* -1 (near x n)))))
1299
;; (defthmd near-exactp-c-lemma
1300
;; (implies (and (exactp a n)
1308
;; (>= a (near x n)))
1310
;; :use ((:instance near-exactp-c---rtl-rel5-support))))))
1313
;; (defthmd near-exactp-d-lemma
1314
;; (implies (and (rationalp x)
1321
;; (<= a (near x n)))
1323
;; :use ((:instance near-exactp-d---rtl-rel5-support))))))
1326
;; (defthmd near-exactp-c
1327
;; (implies (and (exactp a n)
1334
;; (>= a (near x n)))
1335
;; :hints (("Goal" :cases ((< x 0))
1336
;; :in-theory (enable near-minus))
1337
;; ("Subgoal 2" :use ((:instance near-exactp-c-lemma)))
1338
;; ("Subgoal 1" :use ((:instance near-exactp-d-lemma
1340
;; (a (* -1 a)))))))
1345
;; (defthmd near-exactp-d
1346
;; (implies (and (rationalp x)
1352
;; (<= a (near x n)))
1353
;; :hints (("Goal" :cases ((< x 0))
1354
;; :in-theory (enable near-minus))
1355
;; ("Subgoal 2" :use ((:instance near-exactp-d-lemma)))
1356
;; ("Subgoal 1" :use ((:instance near-exactp-c-lemma
1358
;; (a (* -1 a)))))))
1364
;; (defthm expo-trunc-strong
1365
;; (implies (and (natp n)
1367
;; (not (= (abs (trunc x n)) (expt 2 (1+ (expo x))))))
1368
;; (equal (expo (trunc x n))
1370
;; :hints (("Goal" :cases ((equal n 0)))))
1371
;; ("Subgoal 1" :in-theory (enable trunc-rewrite))))
1375
(implies (and (rationalp x)
1378
(not (= (abs (near x n)) (expt 2 (1+ (expo x))))))
1379
(equal (expo (near x n))
1381
:hints (("Goal" :cases ((equal (near x n) (trunc x n))))
1382
("Subgoal 2" :use ((:instance near-choice)
1383
(:instance expo-away))))
1387
;; (defthm near<=away
1388
;; (implies (and (rationalp x)
1392
;; (<= (near x n) (away x n)))
1393
;; :rule-classes ())
1396
;; (defthm near>=trunc
1397
;; (implies (and (rationalp x)
1401
;; (>= (near x n) (trunc x n)))
1402
;; :rule-classes ())
1405
;; (defthmd near-shift
1406
;; (implies (and (rationalp x)
1409
;; (= (near (* x (expt 2 k)) n)
1410
;; (* (near x n) (expt 2 k)))))
1413
;; (defthmd near-minus
1414
;; (equal (near (* -1 x) n)
1415
;; (* -1 (near x n))))
1419
;----------------------------------------------------------------------
1424
;; (defthm equal-diff-trunc-away-1
1425
;; (implies (and (exactp y n)
1428
;; (case-split (<= x y))
1430
;; (equal (abs (- x (trunc x n))) (abs (- (away x n)
1434
;; (>= (abs (- x y)) (abs (- x (near x n)))))
1435
;; :hints (("Goal" :use ((:instance trunc-upper-pos)
1436
;; (:instance near-choice)
1437
;; (:instance away-lower-pos)
1438
;; (:instance away-exactp-c
1443
;; (defthm equal-diff-trunc-away-2
1444
;; (implies (and (exactp y n)
1447
;; (case-split (<= y x))
1449
;; (equal (abs (- x (trunc x n))) (abs (- (away x n)
1453
;; (>= (abs (- x y)) (abs (- x (near x n)))))
1454
;; :hints (("Goal" :use ((:instance near-choice)
1455
;; (:instance trunc-upper-pos)
1456
;; (:instance away-lower-pos)
1457
;; (:instance trunc-exactp-c
1463
;; (defthm near2-lemma
1464
;; (implies (and (exactp y n)
1468
;; (case-split (not (equal (abs (- x (trunc x n))) (abs (- (away x n)
1472
;; (>= (abs (- x y)) (abs (- x (near x n)))))
1473
;; :hints (("Goal" :cases ((not (> (abs (- x (trunc x n))) (abs (- (away x n)
1475
;; ("Subgoal 2" :cases ((not (< x y))))
1476
;; ("Subgoal 2.2" :use ((:instance near1-b)
1477
;; (:instance trunc-upper-pos)
1478
;; (:instance away-lower-pos)
1479
;; (:instance away-exactp-c
1481
;; ("Subgoal 2.1" :use ((:instance near1-b)
1482
;; (:instance trunc-upper-pos)
1483
;; (:instance away-lower-pos)
1484
;; (:instance trunc-exactp-c
1486
;; ("Subgoal 1" :cases ((not (< x y))))
1487
;; ("Subgoal 1.2" :use ((:instance near1-a)
1488
;; (:instance trunc-upper-pos)
1489
;; (:instance away-lower-pos)
1490
;; (:instance away-exactp-c
1492
;; ("Subgoal 1.1" :use ((:instance near1-a)
1493
;; (:instance trunc-upper-pos)
1494
;; (:instance away-lower-pos)
1495
;; (:instance trunc-exactp-c
1500
;; ;; (defthm exactp-equal-trunc-equal
1501
;; ;; (implies (and (exactp x n)
1503
;; ;; (rationalp x))
1504
;; ;; (equal (trunc x n) x))
1505
;; ;; :hints (("Goal" :in-theory (enable exactp trunc)
1506
;; ;; :use ((:instance fp-rep)
1507
;; ;; (:instance a15
1510
;; ;; (j2 (+ 1 (EXPO X) (* -1 N))))))))
1515
;; ;; (defthm exactp-equal-away-equal
1516
;; ;; (implies (and (exactp x n)
1518
;; ;; (rationalp x))
1519
;; ;; (equal (away x n) x))
1520
;; ;; :hints (("Goal" :in-theory (enable cg exactp away)
1521
;; ;; :use ((:instance fp-rep)
1522
;; ;; (:instance a15
1525
;; ;; (j2 (+ 1 (EXPO X) (* -1 N))))))))
1529
;; (defthm near2-lemma-futher
1530
;; (implies (and (exactp y n)
1536
;; (>= (abs (- x y)) (abs (- x (near x n)))))
1537
;; :hints (("Goal" :cases ((equal (abs (- x (trunc x n))) (abs (- (away x n)
1539
;; ("Subgoal 2" :use ((:instance near2-lemma)))
1540
;; ("Subgoal 1" :cases ((not (< x y))))
1541
;; ("Subgoal 1.2" :use ((:instance equal-diff-trunc-away-1)))
1542
;; ("Subgoal 1.1" :use ((:instance equal-diff-trunc-away-2))))))
1547
;; (implies (and (exactp y n)
1552
;; (>= (abs (- x y)) (abs (- x (near x n)))))
1553
;; :hints (("Goal" :cases ((not (> x 0)))
1554
;; :in-theory (enable near-minus trunc-minus away-minus
1556
;; ("Subgoal 2" :use ((:instance near2-lemma-futher)))
1557
;; ("Subgoal 1" :use ((:instance near2-lemma-futher
1559
;; (y (* -1 y)))))))
1563
;; (implies (and (integerp n)
1566
;; (<= (abs (- x (near x n)))
1567
;; (expt 2 (- (expo x) n))))
1568
;; :hints (("Goal" :cases ((not (> x 0)))
1569
;; :in-theory (enable near-minus expo-minus))
1570
;; ("Subgoal 2" :use ((:instance near-est---rtl-rel5-support)))
1571
;; ("Subgoal 1" :use ((:instance near-est---rtl-rel5-support
1573
;; :rule-classes ())
1580
;; (defthm fl-1/2-sig-x-is-zero-specific
1581
;; (implies (rationalp x)
1582
;; (equal (fl (* 1/2 (sig x)))
1584
;; :hints (("Goal" :use ((:instance sig-upper-bound)
1585
;; (:instance sig-lower-bound))))))
1588
;; (defthm near-monotone
1589
;; (implies (and (<= x y)
1595
;; (<= (near x n) (near y n)))
1596
;; :hints (("Goal" :in-theory (enable near-minus)
1597
;; :cases ((not (equal x 0))))
1598
;; ("Subgoal 2" :use ((:instance near-negative
1600
;; ("Subgoal 1" :cases ((not (> x 0))))
1601
;; ("Subgoal 1.2" :use ((:instance
1602
;; near-monotone---rtl-rel5-support)))
1603
;; ("Subgoal 1.1" :cases ((not (> y 0))))
1604
;; ("Subgoal 1.1.2" :use ((:instance near-positive (x y))
1605
;; (:instance near-positive (x (* -1 x)))))
1606
;; ("Subgoal 1.1.1" :use ((:instance near-monotone---rtl-rel5-support
1609
;; (:instance near-positive (x (* -1 x)))))))
1616
;; (defund near-witness (x y n)
1617
;; (if (= (expo x) (expo y))
1618
;; (/ (+ (near x n) (near y n)) 2)
1619
;; (expt 2 (expo y))))
1623
;; (defthm near-near-lemma
1624
;; (implies (and (rationalp x)
1630
;; (not (= (near x n) (near y n))))
1631
;; (and (<= x (near-witness x y n))
1632
;; (<= (near-witness x y n) y)
1633
;; (exactp (near-witness x y n) (1+ n))))
1634
;; :rule-classes ())
1636
;; (defthm near-near
1637
;; (implies (and (rationalp x)
1647
;; (< y (fp+ a (1+ n)))
1648
;; (exactp a (1+ n)))
1649
;; (<= (near y k) (near x k)))
1650
;; :rule-classes ())
1653
;----------------------------------------------------------------------
1656
;;; either (near x n) < (near a n)
1657
;;; or (near a n) < (near y n)
1661
;----------------------------------------------------------------------
1665
;; (defthm a-is-n-exact
1666
;; (implies (and (not (exactp x n))
1667
;; (exactp x (1+ n))
1672
;; (exactp (+ x (* -1 (expt 2 (+ (expo x) (* -1 n)))))
1674
;; :hints (("Goal" :in-theory (enable exactp2 a15)
1675
;; :use ((:instance integerp-x-not-1/2x-lemma
1676
;; (x (* X (EXPT 2 (+ N (* -1 (EXPO X)))))))))))
1679
;; (IMPLIES (AND (RATIONALP X)
1687
;; (>= Y (FP+ X N)))
1688
;; :RULE-CLASSES NIL)
1693
(local (include-book "../../arithmetic/basic"))
1695
(defthm hack-artithm-1
1696
(implies (and (< 0 x)
1706
(defthm expo-a-less-than-specific
1707
(implies (and (integerp n)
1711
(< (EXPT 2 (+ (EXPO A) (* -1 N))) a))
1712
:hints (("Goal" :in-theory (enable sgn)
1713
:use ((:instance expt-strong-monotone-linear
1714
(n (+ (expo a) (* -1 n)))
1716
(:instance fp-rep (x a))
1717
(:instance sig-lower-bound (x a))
1718
(:instance hack-artithm-1
1719
(x (expt 2 (+ (expo a) (* -1 n))))
1720
(y (expt 2 (expo a)))
1722
:rule-classes :linear))
1725
(defthm abs-less-than-lemma
1726
(implies (and (equal (- a b) d)
1736
;; (defthm abs-less-than-lemma-2
1737
;; (implies (and (< x b)
1747
(defthm local-expt-2-expand
1748
(implies (and (rationalp x)
1750
(equal (EXPT 2 (+ 1 (EXPO X) (* -1 N)))
1751
(* 2 (EXPT 2 (+ (expo x) (* -1 N))))))
1752
:hints (("Goal" :use ((:instance a15 (i 2) (j1 1) (j2 (+ (expo x)
1757
(defthm near-boundary-lemma-1-lemma
1758
(implies (and (rationalp x)
1770
(< (abs (- (+ a (* -1
1774
(abs (- (near x n) x))))
1775
:hints (("Goal" :in-theory (disable a-is-n-exact
1777
:use ((:instance a-is-n-exact
1784
(:instance abs-less-than-lemma
1789
(c (+ a (expt 2 (+ (expo a)
1791
(d (expt 2 (+ (expo a) (* -1 n))))
1796
;; (implies (and (exactp y n)
1801
;; (>= (abs (- x y)) (abs (- x (near x n)))))
1802
;; :hints (("Goal" :cases ((not (> x 0)))
1803
;; :in-theory (enable near-minus trunc-minus away-minus
1805
;; ("Subgoal 2" :use ((:instance near2-lemma-futher)))
1806
;; ("Subgoal 1" :use ((:instance near2-lemma-futher
1808
;; (y (* -1 y)))))))
1811
(defthm near-boundary-lemma-1
1812
(implies (and (rationalp x)
1824
:hints (("Goal" :in-theory (disable a-is-n-exact
1827
((:instance near-boundary-lemma-1-lemma)
1828
(:instance a-is-n-exact (x a))
1834
:rule-classes :linear))
1838
(defthm abs-less-than-lemma-2
1839
(implies (and (equal (- a b) d)
1852
(abs (- near-y y))))
1857
;; (implies (and (rationalp x)
1862
;; (equal (fp- (fp+ x n) n)
1866
(defthm near-boundary-lemma-2-lemma
1867
(implies (and (rationalp a)
1872
(+ a (expt 2 (+ (expo a)
1878
(< (abs (- (+ a (expt 2 (+ (expo a)
1881
(abs (- (near y n) y))))
1882
:hints (("Goal" :in-theory (disable a-is-n-exact
1884
:use ((:instance b-is-n-exact
1886
(:instance a-is-n-exact
1889
(x (+ a (* -1 (expt 2 (+ (expo a)
1893
(x (+ a (expt 2 (+ (expo a)
1896
(:instance abs-less-than-lemma-2
1898
(b (- a (expt 2 (+ (expo a)
1900
(c (+ a (expt 2 (+ (expo a)
1902
(d (expt 2 (+ (expo a) (* -1 n))))
1907
(defthm near-boundary-lemma-2
1908
(implies (and (rationalp y)
1916
(<= (+ a (expt 2 (+ (expo a)
1919
:hints (("Goal" :in-theory (disable a-is-n-exact
1922
((:instance near-boundary-lemma-2-lemma)
1923
(:instance b-is-n-exact (x a))
1926
(y (+ a (expt 2 (+ (expo a)
1928
:rule-classes :linear))
1932
(defthm near-boundary
1933
(implies (and (rationalp x)
1943
(< (near x n) (near y n)))
1948
;; Thu Oct 12 17:22:29 2006. New.
1951
;----------------------------------------------------------------------
1953
;; (defthm near-exact
1954
;; (implies (and (rationalp x)
1957
;; (exactp x (1+ n))
1958
;; (not (exactp x n)))
1959
;; (exactp (near x n) (1- n)))
1960
;; :hints (("Goal" :cases ((not (equal x 0)))
1961
;; :in-theory (enable near-minus))
1962
;; ("Subgoal 2" :in-theory (enable exactp))
1963
;; ("Subgoal 1" :cases ((not (> x 0))))
1964
;; ("Subgoal 1.2" :use near-exact---rtl-rel5-support)
1965
;; ("Subgoal 1.1" :use ((:instance near-exact---rtl-rel5-support
1967
;; :rule-classes ())
1970
;; (defund near+ (x n)
1971
;; (if (< (re (* (expt 2 (1- n)) (sig x)))
1977
;; (defthm near+-choice
1978
;; (or (= (near+ x n) (trunc x n))
1979
;; (= (near+ x n) (away x n)))
1980
;; :rule-classes ())
1983
;; (defthm near+<=away
1984
;; (implies (and (rationalp x)
1988
;; (<= (near+ x n) (away x n)))
1989
;; :rule-classes ())
1992
;; (defthm near+>=trunc
1993
;; (implies (and (rationalp x)
1997
;; (>= (near+ x n) (trunc x n)))
1998
;; :rule-classes ())
2001
;; (defthmd near+-shift
2002
;; (implies (and (rationalp x)
2005
;; (= (near+ (* x (expt 2 k)) n)
2006
;; (* (near+ x n) (expt 2 k)))))
2009
;; (defthmd near+-minus
2010
;; (= (near+ (* -1 x) n) (* -1 (near+ x n))))
2012
(defthm near+-positive
2013
(implies (and (rationalp x)
2018
:rule-classes :linear)
2020
(defthm near+-negative
2021
(implies (and (< x 0)
2026
:rule-classes :linear)
2029
;; (equal (near+ 0 n) 0))
2031
;; (defthm near+-0-0
2032
;; (implies (and (case-split (< 0 n))
2033
;; (case-split (rationalp x))
2034
;; (case-split (integerp n)))
2035
;; (equal (equal (near+ x n) 0)
2037
;; :rule-classes ())
2039
;; > (DEFTHM SGN-NEAR+
2040
;; (IMPLIES (AND (RATIONALP X) (INTEGERP N) (> N 0))
2042
;; (* (SGN X) (NEAR+ (ABS X) N))))
2043
;; :RULE-CLASSES NIL)
2045
;; (defthm sgn-near+
2046
;; (implies (and (rationalp x)
2049
;; (equal (sgn (near+ x n))
2051
;; :hints (("Goal" :use ((:instance sgn-near+---rtl-rel5-support)))))
2053
;; (i-am-here) ;; Fri Oct 13 09:45:43 2006
2055
;; (defthm near+-exactp-a
2056
;; (implies (and (rationalp x)
2059
;; (exactp (near+ x n) n))
2060
;; :hints (("Goal" :use ((:instance near+-exactp-b---rtl-rel5-support)))))
2063
;; (defthm near+-exactp-b
2064
;; (implies (and (rationalp x)
2067
;; (iff (= x (near+ x n))
2069
;; :hints (("Goal" :use ((:instance near+-exactp-a---rtl-rel5-support))))
2070
;; :rule-classes ())
2073
;; (defthm near+-exactp-d
2074
;; (implies (and (rationalp x)
2080
;; (<= a (near+ x n)))
2081
;; :hints (("Goal" :cases ((not (equal x 0))))
2082
;; ("Subgoal 2" :in-theory (enable near+))
2083
;; ("Subgoal 1" :cases ((not (> x 0))))
2084
;; ("Subgoal 1.2" :use ((:instance near+-exactp-d---rtl-rel5-support)))
2085
;; ("Subgoal 1.1" :use ((:instance near+-exactp-c---rtl-rel5-support
2086
;; (x (* -1 x)) (a (* -1 a))))
2087
;; :in-theory (e/d (near+ trunc-minus away-minus fl-minus
2088
;; sig-minus) ()))))
2091
;; ACL2 !>(expo (near+ (+ 1/4 1/8) 0))
2093
;; ACL2 !>(expo (+ 1/4 1/8))
2096
;; :hints (("Goal" :cases ((equal (near x n) (trunc x n))))
2097
;; ("Subgoal 2" :use ((:instance near-choice)
2099
; (:instance expo-away))))
2101
;; (i-am-here) ;; Thu Oct 12 18:15:18 2006
2105
(defthm fl-1/2-sig-x-is-zero-specific
2106
(implies (rationalp x)
2107
(equal (fl (* 1/2 (sig x)))
2109
:hints (("Goal" :use ((:instance sig-upper-bound)
2110
(:instance sig-lower-bound))))))
2113
(implies (and (rationalp x)
2115
(not (= (abs (near+ x n)) (expt 2 (1+ (expo x))))))
2116
(equal (expo (near+ x n))
2118
:hints (("Goal" :in-theory (e/d (near+ sgn
2119
expo-trunc expo-away re
2122
:cases ((equal (near+ x n) (trunc x n))))
2123
("Subgoal 1" :cases ((equal n 0)))
2124
("Subgoal 1.1" :cases ((not (equal x 0)))))
2128
;----------------------------------------------------------------------
2131
;; (defthm near+1-a-1
2132
;; (implies (and (rationalp x)
2135
;; (< (abs (- x (trunc x n))) (abs (- (away x n) x))))
2136
;; (= (near+ x n) (trunc x n)))
2137
;; :hints (("Goal" :cases ((not (equal x 0)))
2138
;; :in-theory (enable trunc-minus near+-minus trunc-upper-pos
2141
;; ("Subgoal 1" :cases ((not (> x 0))))
2142
;; ("Subgoal 1.2" :use ((:instance near+1-a---rtl-rel5-support)))
2143
;; ("Subgoal 1.1" :use ((:instance near+1-a---rtl-rel5-support
2145
;; (:instance trunc-upper-pos
2147
;; (:instance away-lower-pos
2149
;; (:instance trunc-exactp-b)
2150
;; (:instance away-exactp-b))))
2151
;; :rule-classes ())
2154
;; (defthm near+1-b-1
2155
;; (implies (and (rationalp x)
2158
;; (> (abs (- x (trunc x n))) (abs (- (away x n) x))))
2159
;; (= (near+ x n) (away x n)))
2160
;; :hints (("Goal" :cases ((not (equal x 0)))
2161
;; :in-theory (enable trunc-minus near+-minus trunc-upper-pos
2164
;; ("Subgoal 1" :cases ((not (> x 0))))
2165
;; ("Subgoal 1.2" :use ((:instance near+1-b---rtl-rel5-support)))
2166
;; ("Subgoal 1.1" :use ((:instance near+1-b---rtl-rel5-support
2168
;; (:instance trunc-upper-pos
2170
;; (:instance away-lower-pos
2172
;; (:instance trunc-exactp-b)
2173
;; (:instance away-exactp-b))))
2174
;; :rule-classes ())
2181
;; (defthm fl-1/2-sig-x-is-zero-lemma
2182
;; (implies (and (rationalp x)
2186
;; (equal (fl (* (sig x) y))
2188
;; :hints (("Goal" :use ((:instance sig-upper-bound)
2189
;; (:instance sig-lower-bound))))))
2193
;; (defthm fl-1/2-sig-x-is-zero-lemma-2
2194
;; (implies (and (rationalp x)
2196
;; (not (equal x 0))
2199
;; (equal (fl (* -1 (sig x) y))
2201
;; :hints (("Goal" :in-theory (enable sig fl-minus)
2202
;; :use ((:instance fl-1/2-sig-x-is-zero-lemma))))))
2206
;; (defthm expt-merge
2207
;; (implies (and (rationalp x)
2209
;; (equal (* (expt 2 (expo x))
2210
;; (EXPT 2 (+ -1 N))
2211
;; (EXPT 2 (* -1 (EXPO X))))
2212
;; (expt 2 (+ -1 n))))
2213
;; :hints (("Goal" :in-theory (enable a15)))))
2215
;; (local (defthm expt-fact-1
2216
;; (implies (and (integerp n)
2218
;; (<= (* 2 (EXPT 2 (+ -1 N))) 1))
2219
;; :hints (("Goal" :use ((:instance expt-weak-monotone-linear
2222
;; :rule-classes :linear))
2225
;; (defthm fl-is-zero-if-n-less-than-minus-1
2226
;; (implies (and (rationalp x)
2230
;; (equal (FL (* -1 X (EXPT 2 (+ -1 N))
2231
;; (EXPT 2 (* -1 (EXPO X)))))
2233
;; :hints (("Goal" :in-theory (e/d (expo-shift sgn)
2234
;; (fl-1/2-sig-x-is-zero-lemma-2))
2235
;; :use ((:instance fp-rep (x x))
2236
;; (:instance fl-1/2-sig-x-is-zero-lemma-2
2237
;; (y (expt 2 (+ -1 n)))))))))
2240
;; (defthm fl-is-zero-if-n-less-than-zero
2241
;; (implies (and (rationalp x)
2245
;; (equal (FL (* X (EXPT 2 (+ -1 N))
2246
;; (EXPT 2 (* -1 (EXPO X)))))
2248
;; :hints (("Goal" :in-theory (e/d (expo-shift sgn)
2249
;; (fl-1/2-sig-x-is-zero-lemma))
2250
;; :use ((:instance fp-rep (x x))
2251
;; (:instance fl-1/2-sig-x-is-zero-lemma
2252
;; (y (expt 2 (+ -1 n)))))))))
2258
;; (local (defthm expt-fact-2
2259
;; (implies (and (integerp n)
2261
;; (<= (* 4 (EXPT 2 (+ -1 N))) 1))
2262
;; :hints (("Goal" :use ((:instance expt-weak-monotone-linear
2265
;; :rule-classes :linear))
2268
;; (defthm arith-hack
2269
;; (implies (and (< sig-x 2)
2279
;; (defthm less-than-1-if-n-is-negative
2280
;; (implies (and (rationalp x)
2284
;; (< (* 2 X (EXPT 2 (+ -1 N))
2285
;; (EXPT 2 (* -1 (EXPO X))))
2287
;; :hints (("Goal" :in-theory (e/d (expo-shift sgn) ())
2288
;; :use ((:instance fp-rep (x x))
2289
;; (:instance sig-upper-bound)
2290
;; (:instance arith-hack
2292
;; (y (expt 2 (+ -1 n)))))))
2293
;; :rule-classes :linear))
2298
;; (defthm local-expt-expand
2299
;; (implies (rationalp x)
2300
;; (equal (EXPT 2 (+ 1 (EXPO X)))
2301
;; (* 2 (expt 2 (expo x)))))
2302
;; :hints (("Goal" :use ((:instance a15 (i 2) (j1 1) (j2 (expo x))))))))
2304
;; (defthm x-lower-bound
2305
;; (implies (and (rationalp x)
2307
;; (>= (* 2 X) (EXPT 2 (+ 1 (EXPO X)))))
2308
;; :hints (("Goal" :use ((:instance expo-lower-bound))))
2309
;; :rule-classes :linear)))
2313
;; ;;;; these 4 are important!!!
2315
;; (defthm fl-is-zero-if-n-less-than-minus-1
2316
;; (implies (and (rationalp x)
2320
;; (equal (FL (* -1 X (EXPT 2 (+ -1 N))
2321
;; (EXPT 2 (* -1 (EXPO X)))))
2325
;; (defthm fl-is-zero-if-n-less-than-zero
2326
;; (implies (and (rationalp x)
2330
;; (equal (FL (* X (EXPT 2 (+ -1 N))
2331
;; (EXPT 2 (* -1 (EXPO X)))))
2334
;; (defthm less-than-1-if-n-is-negative
2335
;; (implies (and (rationalp x)
2339
;; (< (* 2 X (EXPT 2 (+ -1 N))
2340
;; (EXPT 2 (* -1 (EXPO X))))
2342
;; :rule-classes :linear)
2344
;; (defthm x-lower-bound
2345
;; (implies (and (rationalp x)
2347
;; (>= (* 2 X) (EXPT 2 (+ 1 (EXPO X)))))
2348
;; :rule-classes :linear)))
2351
;; (defthm near+1-a-2-2
2352
;; (implies (and (rationalp x)
2356
;; (< (abs (- x (trunc x n))) (abs (- (away x n) x))))
2357
;; (= (near+ x n) (trunc x n)))
2358
;; :hints (("Goal" :in-theory (enable near+ sgn cg away trunc sig re)
2359
;; :cases ((equal n 0))))
2360
;; :rule-classes ()))
2364
;; (local (defthm x-upper-bound-1
2365
;; (implies (and (rationalp x)
2369
;; (> (EXPT 2 (+ 1 (EXPO X) (* -1 N))) X))
2370
;; :rule-classes :linear
2371
;; :hints (("Goal" :in-theory (enable expo-upper-bound)
2372
;; :use ((:instance expt-strong-monotone-linear
2373
;; (n (+ 1 (expo x)))
2374
;; (m (+ 1 (expo x) (* -1 n)))))))))
2377
;; (local (defthm x-upper-bound-2
2378
;; (implies (and (rationalp x)
2382
;; (>= (EXPT 2 (+ 1 (EXPO X) (* -1 N))) (* 2 X)))
2383
;; :rule-classes :linear
2384
;; :hints (("Goal" :in-theory (enable expo-upper-bound)
2385
;; :use ((:instance expt-weak-monotone-linear
2386
;; (n (+ 2 (expo x)))
2387
;; (m (+ 1 (expo x) (* -1 n))))
2388
;; (:instance a15 (i 2)
2389
;; (j1 1) (j2 (+ 1 (expo x)))))))))
2392
;; (local (defthm x-upper-bound-3
2393
;; (implies (and (rationalp x)
2395
;; (> (EXPT 2 (+ 1 (EXPO X))) x))
2396
;; :rule-classes :linear
2397
;; :hints (("Goal" :in-theory (enable expo-upper-bound)))))
2404
;; ;; (defthm fl-is-zero-if-n-less-than-zero
2405
;; ;; (implies (and (rationalp x)
2409
;; ;; (equal (FL (* X (EXPT 2 (+ -1 N))
2410
;; ;; (EXPT 2 (* -1 (EXPO X)))))
2415
;; (local (defthm x-upper-bound-4
2416
;; (implies (and (rationalp x)
2418
;; (<= 1 (* X (EXPT 2 (* -1 (EXPO X))))))
2419
;; :rule-classes :linear
2420
;; :hints (("Goal" :use ((:instance fp-rep))
2421
;; :in-theory (enable sgn a15 sig-lower-bound
2428
;; (defthm fl-is-zero-if-n-less-than-zero-2
2429
;; (implies (and (rationalp x)
2431
;; (equal (FL (* 1/2 X
2432
;; (EXPT 2 (* -1 (EXPO X)))))
2434
;; :hints (("Goal" :use ((:instance fl-is-zero-if-n-less-than-zero
2436
;; :in-theory (disable fl-is-zero-if-n-less-than-zero)))))
2440
;; (defthm near+1-b-2-2
2441
;; (implies (and (rationalp x)
2445
;; (> (abs (- x (trunc x n))) (abs (- (away x n) x))))
2446
;; (= (near+ x n) (away x n)))
2447
;; :hints (("Goal" :in-theory (enable away-lower-pos trunc-upper-pos
2448
;; near+ sgn cg away trunc sig re)
2449
;; :cases ((equal n 0))))
2450
;; :rule-classes ()))
2454
;; (defthm near+1-a-2
2455
;; (implies (and (rationalp x)
2458
;; (< (abs (- x (trunc x n))) (abs (- (away x n) x))))
2459
;; (= (near+ x n) (trunc x n)))
2460
;; :hints (("Goal" :cases ((not (equal x 0)))
2461
;; :in-theory (enable trunc-minus near+-minus trunc-upper-pos
2464
;; ("Subgoal 1" :cases ((not (> x 0))))
2465
;; ("Subgoal 1.2" :use ((:instance near+1-a-2-2)))
2466
;; ("Subgoal 1.1" :use ((:instance near+1-a-2-2
2468
;; :rule-classes ())
2470
;; (defthm near+1-b-2
2471
;; (implies (and (rationalp x)
2474
;; (> (abs (- x (trunc x n))) (abs (- (away x n) x))))
2475
;; (= (near+ x n) (away x n)))
2476
;; :hints (("Goal" :cases ((not (equal x 0)))
2477
;; :in-theory (enable trunc-minus near+-minus trunc-upper-pos
2480
;; ("Subgoal 1" :cases ((not (> x 0))))
2481
;; ("Subgoal 1.2" :use ((:instance near+1-b-2-2)))
2482
;; ("Subgoal 1.1" :use ((:instance near+1-b-2-2
2484
;; :rule-classes ()))
2491
;; (implies (and (rationalp x)
2493
;; (< (abs (- x (trunc x n))) (abs (- (away x n) x))))
2494
;; (= (near+ x n) (trunc x n)))
2495
;; :hints (("Goal" :cases ((not (> n 0))))
2496
;; ("Subgoal 2" :use ((:instance near+1-a-1)))
2497
;; ("Subgoal 1" :use ((:instance near+1-a-2))))
2498
;; :rule-classes ())
2502
;; (implies (and (rationalp x)
2504
;; (> (abs (- x (trunc x n))) (abs (- (away x n) x))))
2505
;; (= (near+ x n) (away x n)))
2506
;; :hints (("Goal" :cases ((not (> n 0))))
2507
;; ("Subgoal 2" :use ((:instance near+1-b-1)))
2508
;; ("Subgoal 1" :use ((:instance near+1-b-2))))
2509
;; :rule-classes ())
2512
;----------------------------------------------------------------------
2514
;; (i-am-here) ;; Fri Oct 13 11:19:13 2006
2520
;; (defthm equal-diff-trunc-away-1
2521
;; (implies (and (exactp y n)
2524
;; (case-split (<= x y))
2526
;; (equal (abs (- x (trunc x n))) (abs (- (away x n)
2530
;; (>= (abs (- x y)) (abs (- x (near+ x n)))))
2531
;; :hints (("Goal" :use ((:instance trunc-upper-pos)
2532
;; (:instance near+-choice)
2533
;; (:instance away-lower-pos)
2534
;; (:instance away-exactp-c
2539
;; (defthm equal-diff-trunc-away-2
2540
;; (implies (and (exactp y n)
2543
;; (case-split (<= y x))
2545
;; (equal (abs (- x (trunc x n))) (abs (- (away x n)
2549
;; (>= (abs (- x y)) (abs (- x (near+ x n)))))
2550
;; :hints (("Goal" :in-theory (disable NEAR+-EXACTP-D)
2551
;; :use ((:instance near+-choice)
2552
;; (:instance trunc-upper-pos)
2553
;; (:instance away-lower-pos)
2554
;; (:instance trunc-exactp-c
2560
;; (defthm near2+-lemma
2561
;; (implies (and (exactp y n)
2565
;; (case-split (not (equal (abs (- x (trunc x n))) (abs (- (away x n)
2569
;; (>= (abs (- x y)) (abs (- x (near+ x n)))))
2570
;; :hints (("Goal" :cases ((not (> (abs (- x (trunc x n))) (abs (- (away x n)
2572
;; :in-theory (disable near+-exactp-d))
2573
;; ("Subgoal 2" :cases ((not (< x y))))
2574
;; ("Subgoal 2.2" :use ((:instance near+1-b)
2575
;; (:instance trunc-upper-pos)
2576
;; (:instance away-lower-pos)
2577
;; (:instance away-exactp-c
2579
;; ("Subgoal 2.1" :use ((:instance near+1-b)
2580
;; (:instance trunc-upper-pos)
2581
;; (:instance away-lower-pos)
2582
;; (:instance trunc-exactp-c
2584
;; ("Subgoal 1" :cases ((not (< x y))))
2585
;; ("Subgoal 1.2" :use ((:instance near+1-a)
2586
;; (:instance trunc-upper-pos)
2587
;; (:instance away-lower-pos)
2588
;; (:instance away-exactp-c
2590
;; ("Subgoal 1.1" :use ((:instance near+1-a)
2591
;; (:instance trunc-upper-pos)
2592
;; (:instance away-lower-pos)
2593
;; (:instance trunc-exactp-c
2598
;; ;; (defthm exactp-equal-trunc-equal
2599
;; ;; (implies (and (exactp x n)
2601
;; ;; (rationalp x))
2602
;; ;; (equal (trunc x n) x))
2603
;; ;; :hints (("Goal" :in-theory (enable exactp trunc)
2604
;; ;; :use ((:instance fp-rep)
2605
;; ;; (:instance a15
2608
;; ;; (j2 (+ 1 (EXPO X) (* -1 N))))))))
2613
;; ;; (defthm exactp-equal-away-equal
2614
;; ;; (implies (and (exactp x n)
2616
;; ;; (rationalp x))
2617
;; ;; (equal (away x n) x))
2618
;; ;; :hints (("Goal" :in-theory (enable cg exactp away)
2619
;; ;; :use ((:instance fp-rep)
2620
;; ;; (:instance a15
2623
;; ;; (j2 (+ 1 (EXPO X) (* -1 N))))))))
2627
;; (defthm near2+-lemma-futher
2628
;; (implies (and (exactp y n)
2634
;; (>= (abs (- x y)) (abs (- x (near+ x n)))))
2635
;; :hints (("Goal" :cases ((equal (abs (- x (trunc x n))) (abs (- (away x n)
2637
;; ("Subgoal 2" :use ((:instance near2+-lemma)))
2638
;; ("Subgoal 1" :cases ((not (< x y))))
2639
;; ("Subgoal 1.2" :use ((:instance equal-diff-trunc-away-1)))
2640
;; ("Subgoal 1.1" :use ((:instance equal-diff-trunc-away-2))))))
2645
;; (implies (and (exactp y n)
2650
;; (>= (abs (- x y)) (abs (- x (near+ x n)))))
2651
;; :hints (("Goal" :cases ((not (> x 0)))
2652
;; :in-theory (enable near+-minus trunc-minus away-minus
2654
;; ("Subgoal 2" :use ((:instance near2+-lemma-futher)))
2655
;; ("Subgoal 1" :use ((:instance near2+-lemma-futher
2658
;; :rule-classes ())
2661
;; (i-am-here) ;; Fri Oct 13 11:38:14 2006
2665
;; (defthm fl-1/2-sig-x-is-zero-specific
2666
;; (implies (rationalp x)
2667
;; (equal (fl (* 1/2 (sig x)))
2669
;; :hints (("Goal" :use ((:instance sig-upper-bound)
2670
;; (:instance sig-lower-bound))))))
2674
;; (defthm near+-monotone-lemma1
2675
;; (implies (and (<= x y)
2678
;; (<= (near+ x 0) (near+ y 0)))
2679
;; :hints (("Goal" :in-theory (enable near+ sgn away-minus)
2680
;; :cases ((not (equal x 0))))
2681
;; ("Subgoal 2" :use ((:instance away-negative
2682
;; (x (* -1 y)) (n 0))))
2683
;; ("Subgoal 1" :cases ((not (> x 0))))
2684
;; ("Subgoal 1.2" :use ((:instance sig-lower-bound (x y))
2685
;; (:instance expt-weak-monotone-linear
2686
;; (n (+ 1 (expo x)))
2687
;; (m (+ 1 (expo y))))
2688
;; (:instance expo-monotone)))
2689
;; ("Subgoal 1.1" :cases ((not (> y 0)))
2690
;; :in-theory (enable away near+ sgn cg))
2692
;; :use ((:instance expt-weak-monotone-linear
2693
;; (n (+ 1 (expo y)))
2694
;; (m (+ 1 (expo x))))
2695
;; (:instance expo-monotone
2697
;; (:instance sig-lower-bound))))))
2700
;; (defthm near+-monotone
2701
;; (implies (and (<= x y)
2706
;; (<= (near+ x n) (near+ y n)))
2707
;; :hints (("Goal" :cases ((not (equal n 0)))
2708
;; :in-theory (enable near+-minus))
2709
;; ("Subgoal 2" :use ((:instance near+-monotone-lemma1)))
2710
;; ("Subgoal 1" :cases ((not (equal x 0))))
2711
;; ("Subgoal 1.2" :use ((:instance near+-negative
2713
;; ("Subgoal 1.1" :cases ((not (> x 0))))
2714
;; ("Subgoal 1.1.2" :use ((:instance
2715
;; near+-monotone---rtl-rel5-support)))
2716
;; ("Subgoal 1.1.1" :use ((:instance near+-monotone---rtl-rel5-support
2718
;; (y (* -1 x)))))))
2722
;----------------------------------------------------------------------
2725
(local (include-book "../../arithmetic/top"))
2727
(defthm z-integerp-not-integer
2728
(implies (and (not (integerp x))
2731
(equal (+ x (* -1 (fl x))) 1/2))))
2734
(defthm integerp-x-integerp-2*x
2735
(implies (and (integerp (* x (expt 2 n)))
2737
(integerp (* 2 x (expt 2 (+ -1 n)))))
2739
:use ((:instance a15
2744
(defthm near+-midpoint
2745
(implies (and (rationalp x)
2749
(equal (near+ x n) (away x n)))
2750
:hints (("Goal" :in-theory (enable exactp near+)
2751
:use ((:instance z-integerp-not-integer
2753
(expt 2 (+ -1 n))))))))
2756
;----------------------------------------------------------------------
2758
;; (defthm near-power-a
2759
;; (implies (and (rationalp x) (> x 0)
2760
;; (integerp n) (> n 1)
2761
;; (>= (+ x (expt 2 (- (expo x) n)))
2762
;; (expt 2 (1+ (expo x)))))
2764
;; (expt 2 (1+ (expo x)))))
2765
;; :rule-classes ())
2768
;; (defthm near-power-b
2769
;; (implies (and (rationalp x) (> x 0)
2770
;; (integerp n) (> n 1)
2771
;; (>= (+ x (expt 2 (- (expo x) n)))
2772
;; (expt 2 (1+ (expo x)))))
2773
;; (= (trunc (+ x (expt 2 (- (expo x) n))) n)
2774
;; (expt 2 (1+ (expo x)))))
2775
;; :rule-classes ())
2778
;; (defthm near+-power
2779
;; (implies (and (rationalp x) (> x 0)
2780
;; (integerp n) (> n 1)
2781
;; (>= (+ x (expt 2 (- (expo x) n)))
2782
;; (expt 2 (1+ (expo x)))))
2784
;; (expt 2 (1+ (expo x)))))
2785
;; :rule-classes ())
2788
;----------------------------------------------------------------------
2791
;; referring to the folllowing
2792
;; Fri Oct 13 12:05:54 2006
2793
;; (defthm plus-trunc
2794
;; (implies (and (rationalp x)
2799
;; (exactp x (+ k (- (expo x) (expo y)))))
2800
;; (= (+ x (trunc y k))
2801
;; (trunc (+ x y) (+ k (- (expo (+ x y)) (expo y))))))
2802
;; :rule-classes ())
2806
;; (defthm plus-away
2807
;; (implies (and (exactp x (+ k (- (expo x) (expo y))))
2813
;; (= (+ x (away y k))
2815
;; (+ k (- (expo (+ x y)) (expo y))))))
2816
;; :rule-classes ())
2818
;; (local (include-book "../../arithmetic/top"))
2820
;; Following the steps in Lemma 5.3.33. on
2821
;; http://www.russinoff.com/libman/top.html
2825
(fl (* (sig y) (expt 2 (+ -1 k))))))
2829
(- (* (expt 2 (+ -1 k)) (sig y)) (z y k))))
2832
(defthm re-equal-if-f-equal
2833
(implies (equal (f y1 k1)
2835
(equal (re (* (expt 2 (+ -1 k1)) (sig y1)))
2836
(re (* (expt 2 (+ -1 k2)) (sig y2)))))
2840
(defthm integerp-1/2-integerp
2841
(implies (and (integerp d)
2843
(iff (integerp (+ d x))
2847
(defthm evenp-perserved-by-plus-even
2848
(implies (and (evenp d)
2851
(and (iff (evenp (+ x d))
2858
(defthm evenp-iff-difference
2859
(implies (and (evenp (- z1 z2))
2864
:hints (("Goal" :use ((:instance evenp-perserved-by-plus-even
2870
(defthm evenp-iff-difference-specific
2871
(implies (evenp (+ (z y k) (* -1 (z (+ x y) (+ k (expo (+ x y)) (* -1 (expo y)))))))
2872
(iff (evenp (fl (* (sig (+ x y)) (expt 2 (+ -1 k (* -1 (expo y)) (expo (+ x y)))))))
2873
(evenp (fl (* (sig y) (expt 2 (+ -1 k)))))))
2874
:hints (("Goal" :in-theory (disable evenp EVENP-IFF-DIFFERENCE)
2875
:use ((:instance evenp-iff-difference
2877
(z2 (z (+ x y) (+ k (expo (+ x y)) (* -1 (expo y)))))))))))
2881
(defthm near-plus-lemma-if-fl-equal
2882
(implies (and (exactp x (1- (+ k (- (expo x) (expo y)))))
2884
(f (+ x y) (+ k (expo (+ x y)) (* -1 (expo y)))))
2886
(* -1 (z (+ x y) (+ k (* -1 (expo y)) (expo (+ x y)))))))
2894
(+ k (- (expo (+ x y)) (expo y))))))
2895
:hints (("Goal" :in-theory (e/d (near exactp-<=) (evenp z f re))
2896
:use ((:instance plus-trunc)
2897
(:instance plus-away)
2898
(:instance evenp-iff-difference-specific)
2899
(:instance re-equal-if-f-equal
2901
(y2 (+ x y)) (k2 (+ k (- (expo (+ x y)) (expo y))))))))
2904
;; > (DEFTHM FL+INT-REWRITE
2905
;; (IMPLIES (AND (INTEGERP N) (RATIONALP X))
2906
;; (EQUAL (FL (+ X N)) (+ (FL X) N))))
2909
(defthm f-equal-if-difference-integerp
2910
(implies (and (integerp (+ (* (sig y1) (expt 2 (+ -1 k1)))
2911
(* -1 (sig y2) (expt 2 (+ -1 k2)))))
2916
:use ((:instance fl+int-rewrite
2917
(x (* (sig y2) (expt 2 (+ -1 k2))))
2918
(n (+ (* (sig y1) (expt 2 (+ -1 k1)))
2919
(* -1 (sig y2) (expt 2 (+ -1 k2)))))))))
2923
(defthm z-difference-evenp-evenp
2924
(implies (equal (f y1 k1)
2928
(+ (* (sig y1) (expt 2 (+ -1 k1)))
2929
(* -1 (sig y2) (expt 2 (+ -1 k2))))))
2933
(defthm expo-normalize
2934
(implies (rationalp x)
2935
(equal (EXPO (* (SGN X)
2939
:hints (("Goal" :use ((:instance fp-rep))))))
2942
(defthm sig-multiply-normalize
2943
(implies (and (rationalp x)
2947
(equal (* (sig x) (expt 2 (+ v w (expo x))))
2948
(* x (expt 2 (+ v w)))))
2949
:hints (("Goal" :in-theory (enable sgn)
2950
:use ((:instance fp-rep (x x))
2951
(:instance a15 (i 2)
2957
(defthm sig-y1-y2-equal
2958
(implies (and (rationalp y)
2963
(equal (+ (* (sig (+ x y))
2964
(expt 2 (+ -1 k (* -1 (expo y))
2966
(* -1 (sig y) (expt 2 (+ -1 k))))
2967
(* x (expt 2 (+ -1 k (* -1 (expo y)))))))
2968
:hints (("Goal" :in-theory (enable sgn)
2969
:cases ((not (equal (* (sig (+ x y))
2970
(expt 2 (+ -1 k (* -1 (expo y))
2973
(expt 2 (+ -1 k (* -1 (expo y)))))))
2974
(not (equal (* (sig y)
2976
(* y (expt 2 (+ -1 k (* -1 (expo y)))))))))
2977
("Subgoal 2" :use ((:instance sig-multiply-normalize
2980
(w (+ K (* -1 (EXPO Y)))))))
2981
("Subgoal 1" :use ((:instance fp-rep (x y))
2982
(:instance a15 (i 2) (j1 (expo y))
2983
(j2 (+ -1 K (* -1 (EXPO Y))))))))))
2988
(defthm local-expt-2-expand
2989
(implies (and (rationalp x)
2991
(equal (EXPT 2 (+ -1 K (* -1 (EXPO Y))))
2992
(* 2 (EXPT 2 (+ -2 K (* -1 (EXPO Y)))))))
2993
:hints (("Goal" :use ((:instance a15 (i 2) (j1 1)
2994
(j2 (+ -2 K (* -1 (EXPO Y))))))))))
2997
(defthm integerp-x-expt-k
2998
(implies (and (exactp x (1- (+ k (- (expo x) (expo y)))))
3001
(integerp (* x (expt 2 (+ -1 k (* -1 (expo y)))))))
3002
:hints (("Goal" :use ((:instance exactp2 (x x)
3003
(n (1- (+ k (- (expo x) (expo y)))))))))))
3007
(defthm evenp-x-expt-k
3008
(implies (and (exactp x (1- (+ k (- (expo x) (expo y)))))
3011
(evenp (* x (expt 2 (+ -1 k (* -1 (expo y)))))))
3012
:hints (("Goal" :use ((:instance exactp2 (x x)
3013
(n (1- (+ k (- (expo x) (expo y)))))))))))
3016
(defthm integerp-minus
3017
(implies (acl2-numberp x)
3018
(iff (integerp (* -1 x))
3020
:hints (("Goal" :in-theory (disable a2)
3021
:cases ((equal (* -1 x) (- x)))))))
3026
(implies (acl2-numberp x)
3027
(iff (evenp (* -1 x))
3029
:hints (("Goal" :in-theory (disable a2 a5)
3030
:cases ((equal (* -1 x) (- x)))))))
3033
(implies (and (exactp x (1- (+ k (- (expo x) (expo y)))))
3041
(+ k (- (expo (+ x y)) (expo y))))))
3042
:hints (("Goal" :in-theory (disable evenp z f
3046
SIG-Y1-Y2-EQUAL near)
3047
:use ((:instance near-plus-lemma-if-fl-equal)
3048
(:instance f-equal-if-difference-integerp
3049
(k1 k) (k2 (+ k (expo (+ x y)) (* -1 (expo y))))
3050
(y1 y) (y2 (+ x y)))
3051
(:instance z-difference-evenp-evenp
3052
(k1 k) (k2 (+ k (expo (+ x y)) (* -1 (expo y))))
3053
(y1 y) (y2 (+ x y)))
3054
(:instance sig-y1-y2-equal)
3055
(:instance integerp-x-expt-k)
3056
(:instance evenp-x-expt-k))))
3063
(defthm near+-plus-lemma-if-fl-equal
3064
(implies (and (exactp x (+ k (- (expo x) (expo y))))
3066
(f (+ x y) (+ k (expo (+ x y)) (* -1 (expo y)))))
3072
(= (+ x (near+ y k))
3074
(+ k (- (expo (+ x y)) (expo y))))))
3075
:hints (("Goal" :in-theory (e/d (near+ exactp-<=) (evenp z f re))
3076
:use ((:instance plus-trunc)
3077
(:instance plus-away)
3078
(:instance re-equal-if-f-equal
3080
(y2 (+ x y)) (k2 (+ k (- (expo (+ x y)) (expo y))))))))
3086
(defthm integerp-x-expt-k-2
3087
(implies (and (exactp x (+ k (- (expo x) (expo y))))
3090
(integerp (* x (expt 2 (+ -1 k (* -1 (expo y)))))))
3091
:hints (("Goal" :use ((:instance exactp2 (x x)
3092
(n (+ k (- (expo x) (expo y))))))))))
3096
(implies (and (exactp x (+ k (- (expo x) (expo y))))
3102
(= (+ x (near+ y k))
3104
(+ k (- (expo (+ x y)) (expo y))))))
3105
:hints (("Goal" :in-theory (disable evenp z f
3108
SIG-Y1-Y2-EQUAL near+)
3109
:use ((:instance near+-plus-lemma-if-fl-equal)
3110
(:instance f-equal-if-difference-integerp
3111
(k1 k) (k2 (+ k (expo (+ x y)) (* -1 (expo y))))
3112
(y1 y) (y2 (+ x y)))
3113
(:instance sig-y1-y2-equal)
3114
(:instance integerp-x-expt-k-2))))
3119
;----------------------------------------------------------------------
3121
;----------------------------------------------------------------------
3123
;; (defthm near-trunc
3124
;; (implies (and (rationalp x) (> x 0)
3125
;; (integerp n) (> n 1))
3127
;; (if (and (exactp x (1+ n)) (not (exactp x n)))
3128
;; (trunc (+ x (expt 2 (- (expo x) n))) (1- n))
3129
;; (trunc (+ x (expt 2 (- (expo x) n))) n))))
3130
;; :rule-classes ())
3133
;; (defthm near+trunc
3134
;; (implies (and (rationalp x)
3139
;; (trunc (+ x (expt 2 (- (expo x) n))) n)))
3140
;; :rule-classes ())
3142
;----------------------------------------------------------------------
3146
;; (implies (and (rationalp x)
3154
;; (>= y (fp+ x n)))
3155
;; :rule-classes ())
3158
(local (include-book "../../arithmetic/expt"))
3159
;; we just want expt-weak-monotone-linear
3163
(+ (trunc x (+ 1 m))
3164
(expt 2 (+ (* -1 m) (expo x))))))
3171
;; (+ (trunc x (+ 1 m))
3172
;; (expt 2 (+ -1 (* -1 m) (expo x))))))
3176
;; (defthm expo-trunc
3177
;; (implies (and (< 0 n)
3180
;; (equal (expo (trunc x n))
3185
(defthm expt-2-less-than-specific
3186
(implies (and (rationalp x)
3190
(<= (expt 2 (+ (expo x) (* -1 M)))
3193
(EXPO (+ (TRUNC X (+ 1 M))
3194
(EXPT 2 (+ (EXPO X) (* -1 M)))))))))
3195
:hints (("Goal" :use ((:instance trunc-lower-bound
3197
(:instance expo-monotone
3198
(x (trunc x (+ 1 m)))
3199
(y (+ (trunc x (+ 1 m))
3200
(EXPT 2 (+ (EXPO X) (* -1 M))))))
3201
(:instance expt-weak-monotone-linear
3202
(n (+ (EXPO X) (* -1 M)))
3204
(EXPO (+ (TRUNC X (+ 1 M))
3205
(EXPT 2 (+ (EXPO X) (* -1 M)))))))))))
3206
:rule-classes :linear))
3211
;; (defthm expt-2-less-than-specific
3212
;; (implies (and (rationalp x)
3216
;; (<= (expt 2 (+ (expo x) (* -1 M)))
3219
;; (EXPO (+ (TRUNC X (+ 1 M))
3220
;; (EXPT 2 (+ -1 (EXPO X) (* -1 M)))))))))
3221
;; :hints (("Goal" :use ((:instance trunc-lower-bound
3222
;; (x x) (n (+ 1 m)))
3223
;; (:instance expo-monotone
3224
;; (x (trunc x (+ 1 m)))
3225
;; (y (+ (trunc x (+ 1 m))
3226
;; (EXPT 2 (+ -1 (EXPO X) (* -1 M))))))
3227
;; (:instance expt-weak-monotone-linear
3228
;; (n (+ (EXPO X) (* -1 M)))
3230
;; (EXPO (+ (TRUNC X (+ 1 M))
3231
;; (EXPT 2 (+ -1 (EXPO X) (* -1 M)))))))))))
3232
;; :rule-classes :linear))
3235
(defthm trunc-less-than
3236
(implies (and (rationalp x)
3239
(< (trunc (+ x (expt 2 (+ (* -1 m) (expo x)))) m)
3240
(fp+ (y x m) (+ 1 m))))
3241
:hints (("Goal" :use ((:instance trunc-upper-pos
3242
(x (+ x (expt 2 (+ (* -1 m) (expo x)))))
3244
(:instance trunc-lower-bound
3247
(:instance expt-2-less-than-specific))))))
3253
;; (defthm trunc-less-than
3254
;; (implies (and (rationalp x)
3257
;; (< (trunc (+ x (expt 2 (+ (* -1 m) (expo x)))) m)
3258
;; (fp+ (y x m) (+ 1 m))))
3259
;; :hints (("Goal" :use ((:instance trunc-upper-pos
3260
;; (x (+ x (expt 2 (+ (* -1 m) (expo x)))))
3262
;; (:instance trunc-lower-bound
3265
;; (:instance expt-2-less-than-specific))))))
3271
(implies (and (rationalp x)
3274
(EXACTP (TRUNC (+ X (EXPT 2 (+ (EXPO X) (* -1 M))))
3277
:hints (("Goal" :in-theory (enable trunc-exactp-a)
3278
:use ((:instance exactp-<=
3280
(x (TRUNC (+ X (EXPT 2 (+ (EXPO X) (* -1 M))))
3287
(defthm exactp-fact-1
3288
(implies (and (rationalp x)
3291
(EXACTP (TRUNC (+ X (EXPT 2 (+ (EXPO X) (* -1 M))))
3294
:hints (("Goal" :in-theory (enable trunc-exactp-a)
3295
:use ((:instance exactp-<=
3297
(x (TRUNC (+ X (EXPT 2 (+ (EXPO X) (* -1 M))))
3304
(defthm exactp-fact-2
3305
(implies (and (rationalp x)
3309
(EXACTP (+ (TRUNC X (+ 1 M))
3310
(EXPT 2 (+ (EXPO X) (* -1 M))))
3312
:hints (("Goal" :use ((:instance fp+1
3313
(x (TRUNC X (+ 1 M)))
3320
(defthm trunc-m+1-plus-is-trunc-plus-C-lemma
3321
(implies (and (integerp m)
3326
(trunc (+ x (expt 2 (+ (* -1 m) (expo x)))) m)))
3327
:hints (("Goal" :in-theory (disable fp+)
3328
:use ((:instance fp+2
3329
(y (trunc (+ x (expt 2 (+ (* -1 m) (expo x)))) m))
3332
(:instance trunc-less-than))))))
3338
;; (+ (trunc x (+ 1 m))
3339
;; (expt 2 (+ (* -1 m) (expo x))))))
3345
(defthm trunc-m+1-plus-is-trunc-plus-C
3346
(implies (and (integerp m)
3350
(= (trunc (y x m) m)
3351
(trunc (+ x (expt 2 (+ (* -1 m) (expo x)))) m)))
3352
:hints (("Goal" :in-theory (disable fp+)
3353
:use ((:instance trunc-m+1-plus-is-trunc-plus-C-lemma)
3354
(:instance trunc-exactp-c
3355
(a (trunc (+ x (expt 2 (+ (* -1 m) (expo x)))) m))
3358
(:instance trunc-monotone
3360
(y (+ x (expt 2 (+ (* -1 m) (expo x)))))
3362
(:instance trunc-upper-pos
3367
;; (defthm near+trunc
3368
;; (implies (and (rationalp x)
3373
;; (trunc (+ x (expt 2 (- (expo x) n))) n)))
3374
;; :rule-classes ())
3377
(defthm near+-trunc-cor-lemma
3378
(implies (and (rationalp x)
3382
(= (near+ (trunc x (+ 1 m)) m)
3384
:hints (("Goal" :in-theory (enable trunc-trunc)
3385
:use ((:instance near+trunc
3386
(x (trunc x (+ 1 m)))
3388
(:instance near+trunc
3391
(:instance trunc-m+1-plus-is-trunc-plus-C))))
3395
(defthm near+-trunc-cor-lemma-2
3396
(implies (and (rationalp x)
3399
(= (near+ (trunc x (+ 1 m)) m)
3401
:hints (("Goal" :cases ((not (equal x 0)))
3402
:in-theory (enable trunc-minus near+-minus))
3403
("Subgoal 1" :cases ((not (> x 0))))
3404
("Subgoal 1.2" :use ((:instance near+-trunc-cor-lemma)))
3405
("Subgoal 1.1" :use ((:instance near+-trunc-cor-lemma
3410
(defthm near+-trunc-cor
3411
(implies (and (rationalp x)
3416
(= (near+ (trunc x n) m)
3418
:hints (("Goal" :cases ((not (> n (+ 1 m)))))
3419
("Subgoal 2" :use ((:instance near+-trunc-cor-lemma-2
3422
(:instance near+-trunc-cor-lemma-2
3425
(:instance trunc-trunc
3429
("Subgoal 1" :use ((:instance near+-trunc-cor-lemma-2))))
3434
;----------------------------------------------------------------------
3436
;;;**********************************************************************
3438
;;;**********************************************************************
3441
;; (defund sticky (x n)
3442
;; (cond ((exactp x (1- n)) x)
3443
;; (t (+ (trunc x (1- n))
3444
;; (* (sgn x) (expt 2 (1+ (- (expo x) n))))))))
3450
(defthm sgn-x-plus-y
3451
(implies (and (equal (sgn x) (sgn y))
3454
(equal (sgn (+ x y))
3456
:hints (("Goal" :in-theory (enable sgn)))))
3460
(equal (sgn (sgn x))
3462
:hints (("Goal" :in-theory (enable sgn)))))
3466
(equal (SGN (EXPT 2 n))
3468
:hints (("Goal" :in-theory (enable sgn)))))
3471
(implies (and (rationalp x)
3474
(equal (sgn (sticky x n))
3476
:hints (("Goal" :in-theory (enable sticky
3479
:cases ((not (> n 1))))
3481
:use ((:instance sgn-x-plus-y
3482
(x (trunc x (+ -1 n)))
3484
(EXPT 2 (+ 1 (EXPO X) (* -1 N))))))))))
3487
(defthm positive-sgn-1
3488
(implies (rationalp x)
3489
(iff (equal (sgn x) 1)
3491
:hints (("Goal" :in-theory (enable sgn)))))
3494
(defthmd sticky-positive
3495
(implies (and (< 0 x)
3500
:hints (("Goal" :use ((:instance sgn-sticky)
3501
(:instance positive-sgn-1
3503
(:instance positive-sgn-1
3504
(x (sticky x n))))))
3505
:rule-classes :linear)
3508
(defthm positive-sgn-2
3509
(implies (rationalp x)
3510
(iff (equal (sgn x) -1)
3512
:hints (("Goal" :in-theory (enable sgn)))))
3515
(defthmd sticky-negative
3516
(implies (and (< x 0)
3521
:hints (("Goal" :use ((:instance sgn-sticky)
3522
(:instance positive-sgn-2
3524
(:instance positive-sgn-2
3525
(x (sticky x n))))))
3526
:rule-classes :linear)
3529
;; (equal (sticky 0 n) 0))
3532
;; (defthmd sticky-minus
3533
;; (equal (sticky (* -1 x) n) (* -1 (sticky x n))))
3536
;; (defthm sticky-shift
3537
;; (implies (and (rationalp x)
3538
;; (integerp n) (> n 0)
3540
;; (= (sticky (* (expt 2 k) x) n)
3541
;; (* (expt 2 k) (sticky x n))))
3542
;; :rule-classes ())
3545
;; (defthm expo-sticky
3546
;; (implies (and (rationalp x) (> x 0)
3547
;; (integerp n) (> n 0))
3548
;; (= (expo (sticky x n))
3550
;; :rule-classes ())
3554
(defthm sticky-exactp-a-lemma
3555
(implies (and (rationalp x)
3557
(integerp n) (> n 0))
3558
(exactp (sticky x n) n))
3559
:hints (("Goal" :in-theory (enable sgn exactp-2**n sticky)
3560
:cases ((not (equal n 1))))
3562
:use ((:instance trunc-exactp-a (n (- 1 n)))
3564
(x (trunc x (+ -1 n)))
3566
(:instance exactp-<=
3569
(x (trunc x (+ -1 n))))
3570
(:instance exactp-<=
3577
(defthm sticky-exactp-a
3578
(implies (and (rationalp x)
3579
(integerp n) (> n 0))
3580
(exactp (sticky x n) n))
3581
:hints (("Goal" :cases ((not (equal x 0)))
3582
:in-theory (enable sticky-minus))
3583
("Subgoal 2" :in-theory (enable sticky exactp))
3584
("Subgoal 1" :cases ((not (> x 0))))
3585
("Subgoal 1.2" :use ((:instance sticky-exactp-a-lemma)))
3586
("Subgoal 1.1" :use ((:instance sticky-exactp-a-lemma
3593
(implies (and (rationalp x)
3595
(iff (equal (EXPT 2 (EXPO X)) x)
3596
(INTEGERP (SIG X))))
3597
:hints (("Goal" :use ((:instance fp-rep)
3598
(:instance sig-lower-bound)
3599
(:instance sig-upper-bound))
3600
:in-theory (enable sgn))
3601
("Subgoal 1" :cases ((not (< 1 (sig x))))))))
3605
(defthm sticky-exactp-b-lemma
3606
(implies (and (rationalp x)
3610
(iff (= x (sticky x n))
3612
:hints (("Goal" :in-theory (enable expo-trunc
3616
exactp-2**n sticky sgn)
3617
:cases ((not (exactp x (+ -1 n)))))
3618
("Subgoal 2" :use ((:instance exactp-<=
3622
("Subgoal 1" :cases ((not (equal n 1))))
3623
("Subgoal 1.2" :in-theory (enable exactp
3626
("Subgoal 1.1" :use ((:instance trunc-midpoint
3630
(x (trunc x (+ -1 n)))
3632
(:instance exactp-<=
3635
(x (trunc x (+ -1 n)))))))
3639
(defthm sticky-exactp-b
3640
(implies (and (rationalp x)
3643
(iff (= x (sticky x n))
3645
:hints (("Goal" :cases ((not (equal x 0)))
3646
:in-theory (enable sticky-minus))
3647
("Subgoal 2" :in-theory (enable sticky exactp))
3648
("Subgoal 1" :cases ((not (> x 0))))
3649
("Subgoal 1.2" :use ((:instance sticky-exactp-b-lemma)))
3650
("Subgoal 1.1" :use ((:instance sticky-exactp-b-lemma
3655
;; (defthm fl-1/2-sig-x-is-zero-lemma
3656
;; (implies (and (rationalp x)
3660
;; (equal (fl (* (sig x) y))
3662
;; :hints (("Goal" :use ((:instance sig-upper-bound)
3663
;; (:instance sig-lower-bound))))))
3668
;; (defthm |1/2-sig-x-not-integerp-lemma|
3669
;; (implies (and (rationalp x)
3670
;; (not (equal x 0))
3674
;; (not (integerp (* (sig x) y))))
3675
;; :hints (("Goal" :use ((:instance sig-upper-bound)
3676
;; (:instance sig-lower-bound))))))
3679
;; (local (include-book "../../arithmetic/expt"))
3682
;; (defthm exactp-minus-fact
3683
;; (implies (and (integerp n)
3685
;; (not (equal x 0))
3687
;; (not (exactp x n)))
3688
;; :hints (("Goal" :in-theory (enable exactp)
3689
;; :use ((:instance sig-upper-bound)
3690
;; (:instance sig-lower-bound)
3691
;; (:instance |1/2-sig-x-not-integerp-lemma|
3692
;; (y (expt 2 (+ -1 n))))
3693
;; (:instance expt-weak-monotone-linear
3697
;; (defthmd sticky-monotone
3698
;; (implies (and (<= x y)
3702
;; (<= (sticky x n) (sticky y n)))
3703
;; :hints (("Goal" :cases ((not (equal n 0)))
3704
;; :in-theory (enable sticky sgn))
3705
;; ("Subgoal 2" :cases ((not (equal y 0))))
3706
;; ("Subgoal 2.1" :use ((:instance expo-monotone
3709
;; (:instance expo-monotone
3712
;; (:instance expt-weak-monotone-linear
3713
;; (n (+ 1 (expo y)))
3714
;; (m (+ 1 (expo x))))
3715
;; (:instance expt-weak-monotone-linear
3716
;; (n (+ 1 (expo x)))
3717
;; (m (+ 1 (expo y))))))
3718
;; ("Subgoal 1" :use ((:instance sticky-monotone---rtl-rel5-support))))
3719
;; :rule-classes :linear)
3722
;; (defthm sticky-exactp-m
3723
;; (implies (and (rationalp x)
3728
;; (iff (exactp (sticky x n) m)
3730
;; :rule-classes ())
3734
;; (defthm trunc-sticky
3735
;; (implies (and (rationalp x)
3736
;; (integerp m) (> m 0)
3737
;; (integerp n) (> n m))
3738
;; (= (trunc (sticky x n) m)
3740
;; :hints (("Goal" :cases ((not (equal x 0))))
3741
;; ("Subgoal 1" :cases ((not (> x 0))))
3742
;; ("Subgoal 1.2" :use ((:instance trunc-sticky---rtl-rel5-support)))
3743
;; ("Subgoal 1.1" :use ((:instance trunc-sticky---rtl-rel5-support
3745
;; :in-theory (enable trunc-minus sticky-minus)))
3746
;; :rule-classes ())
3749
;; (defthm away-sticky
3750
;; (implies (and (rationalp x)
3751
;; (integerp m) (> m 0)
3752
;; (integerp n) (> n m))
3753
;; (= (away (sticky x n) m)
3755
;; :hints (("Goal" :cases ((not (equal x 0))))
3756
;; ("Subgoal 1" :cases ((not (> x 0))))
3757
;; ("Subgoal 1.2" :use ((:instance away-sticky---rtl-rel5-support)))
3758
;; ("Subgoal 1.1" :use ((:instance away-sticky---rtl-rel5-support
3760
;; :in-theory (enable away-minus sticky-minus)))
3761
;; :rule-classes ())
3764
;; (defthm near-sticky
3765
;; (implies (and (rationalp x)
3766
;; (integerp m) (> m 0)
3767
;; (integerp n) (> n (1+ m)))
3768
;; (= (near (sticky x n) m)
3770
;; :hints (("Goal" :cases ((not (equal x 0))))
3771
;; ("Subgoal 1" :cases ((not (> x 0))))
3772
;; ("Subgoal 1.2" :use ((:instance near-sticky---rtl-rel5-support)))
3773
;; ("Subgoal 1.1" :use ((:instance near-sticky---rtl-rel5-support
3775
;; :in-theory (enable near-minus sticky-minus)))
3776
;; :rule-classes ())
3779
;----------------------------------------------------------------------
3782
;; (defthm near+-sticky
3783
;; (implies (and (rationalp x)
3784
;; (integerp m) (> m 0)
3785
;; (integerp n) (> n (1+ m)))
3786
;; (= (near+ (sticky x n) m)
3788
;; :hints (("Goal" :use ((:instance near+-trunc-cor
3792
;; (:instance trunc-sticky
3794
;; (:instance near+-trunc-cor
3798
;; :rule-classes ())
3800
;----------------------------------------------------------------------
3802
;; (defthm sticky-sticky
3803
;; (implies (and (rationalp x)
3808
;; (= (sticky (sticky x n) m)
3810
;; :rule-classes ())
3812
;----------------------------------------------------------------------
3815
;; sticky-plus---rtl-rel5-support
3816
;; (implies (and (rationalp x)
3821
;; (= k1 (+ k (- (expo x) (expo y))))
3822
;; (= k2 (+ k (- (expo (+ x y)) (expo y))))
3826
;; (exactp x (1- k1)))
3827
;; (= (+ x (sticky y k))
3828
;; (sticky (+ x y) k2)))
3829
;; :hints (("Goal" :by sticky-plus))
3830
;; :rule-classes ())
3832
;; doesn't support well. Tue Jan 31 12:56:09 2006
3835
;; (defthm trunc-plus-minus
3836
;; (implies (and (rationalp x)
3840
;; (not (= (+ x y) 0))
3843
;; (= k1 (+ k (- (expo x) (expo y))))
3844
;; (= k2 (+ k (expo (+ x y)) (* -1 (expo y))))
3847
;; (equal (+ x (trunc y k))
3848
;; (if (= (sgn (+ x y)) (sgn y))
3849
;; (trunc (+ x y) k2)
3850
;; (away (+ x y) k2))))
3857
(defthm exactp-fact-1
3858
(implies (and (EXACTP X (+ -1 K (EXPO X) (* -1 (EXPO Y))))
3862
(iff (exactp (+ x y) (+ -1 K (* -1 (EXPO Y))
3864
(exactp y (+ -1 k))))
3865
:hints (("Goal" :in-theory (enable exactp2)))))
3870
(defthm local-expt-2-expand
3871
(implies (and (rationalp x)
3873
(equal (EXPT 2 (+ 2 (EXPO Y) (* -1 K)))
3874
(* 2 (EXPT 2 (+ 1 (EXPO Y) (* -1 k))))))
3875
:hints (("Goal" :use ((:instance a15 (i 2) (j1 1)
3880
(implies (and (rationalp x)
3885
(= k1 (+ k (- (expo x) (expo y))))
3886
(= k2 (+ k (- (expo (+ x y)) (expo y))))
3891
(= (+ x (sticky y k))
3892
(sticky (+ x y) k2)))
3893
:hints (("Goal" :cases ((not (exactp y (+ -1 k))))
3894
:in-theory (enable sticky))
3895
("Subgoal 1" :use ((:instance trunc-plus-minus
3896
(k1 (+ -1 k (expo x) (* -1 (expo y))))
3897
(k2 (+ -1 k (* -1 (expo y)) (expo (+
3901
("Subgoal 1.1" :cases ((not (> (+ x y) 0))))
3902
("Subgoal 1.1.2" :use ((:instance trunc-away
3904
(n (+ -1 K (* -1 (EXPO Y))
3906
:in-theory (enable sgn expo-minus trunc-minus away-minus))
3907
("Subgoal 1.1.1" :use ((:instance trunc-away
3909
(n (+ -1 K (* -1 (EXPO Y))
3911
:in-theory (enable sgn expo-minus trunc-minus away-minus)))
3916
;;;**********************************************************************
3918
;;;**********************************************************************
3920
;; (i-am-here);; Fri Oct 13 15:10:44 2006
3927
(defthmd inf-lower-bound
3928
(implies (and (case-split (rationalp x))
3929
(case-split (integerp n)))
3931
:hints (("Goal" :use ((:instance trunc-upper-bound)
3932
(:instance away-lower-bound)))
3933
("Subgoal 1" :cases ((not (equal x 0)))))
3934
:rule-classes :linear)
3937
;; (defun minf (x n)
3942
(defthmd minf-lower-bound
3943
(implies (and (case-split (rationalp x))
3944
(case-split (integerp n)))
3946
:hints (("Goal" :use ((:instance trunc-upper-bound)
3947
(:instance away-lower-bound))))
3948
:rule-classes :linear)
3950
;; (defund IEEE-mode-p (mode)
3951
;; (member mode '(trunc inf minf near)))
3954
;; (defun common-rounding-mode-p (mode)
3955
;; (or (IEEE-mode-p mode) (equal mode 'away) (equal mode 'near+)))
3957
;; (defthmd ieee-mode-p-implies-common-rounding-mode-p
3958
;; (implies (IEEE-mode-p mode)
3959
;; (common-rounding-mode-p mode)))
3961
;; (defund rnd (x mode n)
3963
;; (away (away x n))
3964
;; (near+ (near+ x n))
3965
;; (trunc (trunc x n))
3967
;; (minf (minf x n))
3968
;; (near (near x n))
3972
;; (defthm rationalp-rnd
3973
;; (rationalp (rnd x mode n))
3974
;; :rule-classes (:type-prescription))
3978
(implies (and (rationalp x)
3980
(common-rounding-mode-p mode))
3981
(or (= (rnd x mode n) (trunc x n))
3982
(= (rnd x mode n) (away x n))))
3983
:hints (("Goal" :use ((:instance near+-choice)
3984
(:instance near-choice))
3985
:in-theory (enable rnd IEEE-mode-p)))
3990
;; (defthm not-rational-rnd-redcue-to-zero
3991
;; (implies (not (rationalp x))
3992
;; (equal (rnd x mode n) 0))
3993
;; :hints (("Goal" :in-theory (enable away near sig trunc near+ rnd)))))
3996
;; (defthm not-rational-sgn-redcue-to-zero
3997
;; (implies (not (rationalp x))
3998
;; (equal (sgn x) 0))
3999
;; :hints (("Goal" :in-theory (enable sgn)))))
4003
;; (implies (and (common-rounding-mode-p mode)
4006
;; (equal (sgn (rnd x mode n))
4008
;; :hints (("Goal" :cases ((not (rationalp x)))
4010
;; (enable sgn-away sgn-trunc
4011
;; sgn-near rnd IEEE-mode-p)))))
4015
(defthm rnd-positive
4016
(implies (and (< 0 x)
4020
(common-rounding-mode-p mode))
4021
(> (rnd x mode n) 0))
4024
(enable rnd IEEE-mode-p)))
4025
:rule-classes (:type-prescription))
4027
(defthm rnd-negative
4028
(implies (and (< x 0)
4032
(common-rounding-mode-p mode))
4033
(< (rnd x mode n) 0))
4036
(enable rnd near IEEE-mode-p)))
4037
:rule-classes (:type-prescription))
4040
;; (equal (rnd 0 mode n)
4043
; Unlike the above, we leave the following two as rewrite rules because we may
4044
; want to use the rewriter to relieve their hypotheses.
4046
;; (defthm rnd-non-pos
4047
;; (implies (<= x 0)
4048
;; (<= (rnd x mode n) 0))
4049
;; :rule-classes (:rewrite :type-prescription :linear))
4051
;; (defthm rnd-non-neg
4052
;; (implies (<= 0 x)
4053
;; (<= 0 (rnd x mode n)))
4054
;; :rule-classes (:rewrite :type-prescription :linear))
4062
;; (defthm ieee-mode-p-flip
4063
;; (implies (ieee-mode-p m)
4064
;; (ieee-mode-p (flip m))))
4067
;; (defthm common-rounding-mode-p-flip
4068
;; (implies (common-rounding-mode-p m)
4069
;; (common-rounding-mode-p (flip m))))
4072
;; (defthmd rnd-minus
4073
;; (equal (rnd (* -1 x) mode n)
4074
;; (* -1 (rnd x (flip mode) n))))
4079
;; (defthm rnd-exactp-a
4081
;; (exactp (rnd x mode n) n))
4082
;; :hints (("Goal" :by rnd-exactp-b---rtl-rel5-support)))
4085
;; (defthm rnd-exactp-b
4086
;; (implies (and (rationalp x)
4087
;; (common-rounding-mode-p mode)
4090
;; (equal (equal x (rnd x mode n))
4092
;; :hints (("Goal" :use ((:instance rnd-exactp-a---rtl-rel5-support)))))
4095
;; (defthmd rnd-exactp-c
4096
;; (implies (and (rationalp x)
4097
;; (common-rounding-mode-p mode)
4103
;; (>= a (rnd x mode n)))
4104
;; :hints (("Goal" :in-theory (enable trunc-minus
4105
;; ieee-mode-p flip rnd)
4106
;; :use ((:instance trunc-exactp-c
4107
;; (x (* -1 x)) (a (* -1 a)))
4108
;; (:instance away-exactp-c)
4109
;; (:instance near-exactp-c)
4110
;; (:instance near+-exactp-c)))))
4113
;; (defthmd rnd-exactp-d
4114
;; (implies (and (rationalp x)
4115
;; (common-rounding-mode-p mode)
4121
;; (<= a (rnd x mode n)))
4122
;; :hints (("Goal" :in-theory (enable away-minus
4123
;; ieee-mode-p flip rnd)
4124
;; :use ((:instance trunc-exactp-c)
4125
;; (:instance away-exactp-c
4126
;; (x (* -1 x)) (a (* -1 a)))
4127
;; (:instance near-exactp-d)
4128
;; (:instance near+-exactp-d)))))
4131
;; (defthm rnd<=away
4132
;; (implies (and (rationalp x)
4134
;; (common-rounding-mode-p mode)
4136
;; (<= (rnd x mode n) (away x n)))
4137
;; :hints (("Goal" :in-theory (enable ieee-mode-p
4143
;; :rule-classes ())
4147
;; (defthm rnd>=trunc
4148
;; (implies (and (rationalp x)
4150
;; (common-rounding-mode-p mode)
4152
;; (>= (rnd x mode n) (trunc x n)))
4153
;; :hints (("Goal" :in-theory (enable ieee-mode-p
4156
;; common-rounding-mode-p
4160
;; :rule-classes ())
4163
;; (defthmd rnd-diff
4164
;; (implies (and (rationalp x)
4167
;; (common-rounding-mode-p mode))
4168
;; (< (abs (- x (rnd x mode n))) (expt 2 (- (1+ (expo x)) n))))
4169
;; :hints (("Goal" :use ((:instance rnd-diff---rtl-rel5-support)))))
4171
;; (i-am-here) ;; Fri Oct 13 15:29:42 2006
4174
;; (implies (and (rationalp x)
4177
;; (common-rounding-mode-p mode)
4178
;; (not (= (abs (rnd x mode n))
4179
;; (expt 2 (1+ (expo x))))))
4180
;; (= (expo (rnd x mode n))
4182
;; :hints (("Goal" :use ((:instance expo-rnd---rtl-rel5-support))))
4183
;; :rule-classes ())
4189
;; (defthm |Subgoal 5|
4190
;; (IMPLIES (AND (RATIONALP X)
4196
;; (<= (TRUNC X N) (AWAY Y N)))
4197
;; :hints (("Goal" :cases ((not (equal y 0)))
4198
;; :in-theory (enable trunc-negative sgn
4200
;; :rule-classes :linear))
4204
;; ;; (defthm near+-monotone
4205
;; ;; (implies (and (<= x y)
4208
;; ;; (< 0 x) ;;; not good enough!!!
4211
;; ;; (<= (near+ x n) (near+ y n))))
4214
;; (defthmd rnd-monotone
4215
;; (implies (and (<= x y)
4218
;; (common-rounding-mode-p mode)
4221
;; (<= (rnd x mode n) (rnd y mode n)))
4222
;; :hints (("Goal" :in-theory (enable ieee-mode-p
4223
;; common-rounding-mode-p
4233
;; :use ((:instance away-monotone)))))
4238
;; (defthm rnd-shift
4239
;; (implies (and (rationalp x)
4241
;; (common-rounding-mode-p mode)
4243
;; (= (rnd (* x (expt 2 k)) mode n)
4244
;; (* (rnd x mode n) (expt 2 k))))
4245
;; :hints (("Goal" :use ((:instance rnd-shift---rtl-rel5-support))))
4246
;; :rule-classes ())
4250
;; (implies (and (rationalp x)
4255
;; (exactp x (+ -1 k (- (expo x) (expo y))))
4256
;; (common-rounding-mode-p mode))
4257
;; (= (+ x (rnd y mode k))
4260
;; (+ k (- (expo (+ x y)) (expo y))))))
4261
;; :hints (("Goal" :use ((:instance plus-rnd---rtl-rel5-support))))
4262
;; :rule-classes ())
4265
;; (defthmd rnd-sticky
4266
;; (implies (and (common-rounding-mode-p mode)
4272
;; (equal (rnd (sticky x n) mode m)
4274
;; :hints (("Goal" :cases ((not (equal x 0)))
4275
;; :in-theory (enable rnd-minus flip rnd sticky-minus))
4276
;; ("Subgoal 1" :cases ((not (> x 0))))
4278
;; :use ((:instance rnd-sticky---rtl-rel5-support
4281
;; :use ((:instance rnd-sticky---rtl-rel5-support
4283
;; (mode (flip mode))
4284
;; (x (* -1 x)))))))
4289
;; (defun rnd-const (e mode n)
4291
;; ((near near+) (expt 2 (- e n)))
4292
;; ((inf away) (1- (expt 2 (1+ (- e n)))))
4296
;; (defthm rnd-const-thm
4297
;; (implies (and (common-rounding-mode-p mode)
4303
;; (= (rnd x mode n)
4304
;; (if (and (eql mode 'near)
4305
;; (exactp x (1+ n))
4306
;; (not (exactp x n)))
4307
;; (trunc (+ x (rnd-const (expo x) mode n)) (1- n))
4308
;; (trunc (+ x (rnd-const (expo x) mode n)) n))))
4309
;; :hints (("Goal" :use rnd-const-thm---rtl-rel5-support))
4310
;; :rule-classes ())
4313
;; (defun roundup (x mode n)
4315
;; (near+ (= (bitn x (- (expo x) n)) 1))
4316
;; (near (and (= (bitn x (- (expo x) n)) 1)
4317
;; (or (not (exactp x (1+ n)))
4318
;; (= (bitn x (- (1+ (expo x)) n)) 1))))
4319
;; ((inf away) (not (exactp x n)))
4323
;; (defthm roundup-thm
4324
;; (implies (and (common-rounding-mode-p mode)
4330
;; (= (rnd x mode n)
4331
;; (if (roundup x mode n)
4332
;; (fp+ (trunc x n) n)
4334
;; :hints (("Goal" :use roundup-thm---rtl-rel5-support))
4335
;; :rule-classes ())
4338
;;; very nice theorems!! good!! Tue Jan 31 16:37:49 2006
4339
;;; relating bits and their rounded values!!
4342
;;; Sun Oct 15 16:41:11 2006
4344
;; (i-am-here) ;; Sun Oct 15 17:00:23 2006
4346
;;;**********************************************************************
4347
;;; Denormal Rounding
4348
;;;**********************************************************************
4350
;;; because of the drnd definition changed, we abandon all the proofs in
4353
;;; we could prove that two definitions are the same thus reuse the older
4356
(defund drnd (x mode p q)
4357
(rnd x mode (+ p (expo x) (- (expo (spn q))))))
4360
(equal (drnd (* -1 x) mode p q)
4361
(* -1 (drnd x (flip mode) p q)))
4362
:hints (("Goal" :in-theory (enable drnd expo-minus rnd-minus))))
4364
;----------------------------------------------------------------------
4369
(include-book "../../arithmetic/expt")
4371
(defthm fl-1/2-sig-x-is-zero-lemma
4372
(implies (and (rationalp x)
4376
(equal (fl (* (sig x) y))
4378
:hints (("Goal" :use ((:instance sig-upper-bound)
4379
(:instance sig-lower-bound))))))
4381
;; we really need these two lemma
4382
(defthm fl-1/2-sig-x-is-zero-lemma-2
4383
(implies (and (rationalp x)
4388
(equal (fl (* -1 (sig x) y))
4390
:hints (("Goal" :in-theory (enable sig fl-minus)
4391
:use ((:instance fl-1/2-sig-x-is-zero-lemma)))))
4393
(defthm expt-2-no-greater-than-1
4394
(implies (and (<= (+ p (expo x))
4400
(* -1 (EXPO (SPN Q))))))
4402
:hints (("Goal" :use ((:instance expt-weak-monotone-linear
4404
(* -1 (EXPO (SPN Q)))))
4406
:rule-classes :linear)
4408
(defthm fl-1/2-sig-x-is-zero
4409
(implies (and (rationalp x)
4410
(case-split (not (equal x 0)))
4414
(equal (FL (* (SIG X)
4417
(* -1 (EXPO (SPN Q)))))))
4419
:hints (("Goal" :use ((:instance fl-1/2-sig-x-is-zero-lemma
4422
(* -1 (EXPO (SPN q)))))))))))
4425
(defthm fl-1/2-sig-x-is-zero-2
4426
(implies (and (rationalp x)
4427
(case-split (not (equal x 0)))
4431
(equal (FL (* -1 (SIG X)
4434
(* -1 (EXPO (SPN Q)))))))
4436
:hints (("Goal" :use ((:instance fl-1/2-sig-x-is-zero-lemma-2
4439
(* -1 (EXPO (SPN q)))))))))))))
4442
;----------------------------------------------------------------------
4447
;;; prove the first condition in drepp
4449
;;L d (DEFUN DREPP (X P Q)
4450
;; (AND (RATIONALP X)
4452
;; (<= (- 2 P) (+ (EXPO X) (BIAS Q)))
4453
;; (<= (+ (EXPO X) (BIAS Q)) 0)
4454
;; (EXACTP X (+ -2 P (EXPT 2 (- Q 1)) (EXPO X)))))
4456
(local (encapsulate ()
4458
;;;; (<= (+ (EXPO X) (BIAS Q)) 0) if x < (spn q)
4461
(defthm expo-less-than-minus-1-lemma
4462
(IMPLIES (AND (< N (EXPO X))
4466
(<= (EXPT 2 (+ 1 N)) X))
4467
:hints (("Goal" :use ((:instance expt-weak-monotone-linear
4470
(:instance expo-lower-bound))))))
4473
(defthm expo-less-than-minus-1
4474
(implies (and (< 0 x)
4477
(< X (EXPT 2 (+ 1 n))))
4479
:hints (("Goal" :cases ((> (expo x) n))))
4480
:rule-classes :linear))
4482
(defthm less-than-spn-implies-expo-less
4483
(implies (and (< (abs x) (spn q))
4488
(>= 0 (+ (bias q) (expo x))))
4489
:hints (("Goal" :in-theory (enable spn expo-minus)
4490
:use ((:instance expo-monotone (x (abs x)) (y (spn q))))))
4491
:rule-classes :linear))
4493
) ;;; END OF (<= (+ (EXPO X) (BIAS Q)) 0) if x < (spn q)
4496
(local (encapsulate ()
4499
;;; (EXACTP X (+ -2 P (EXPT 2 (- Q 1)) (EXPO X)))))
4502
(defthm exactp-drnd-specific
4503
(implies (and (rationalp x)
4509
(EXACTP (DRND X MODE P Q)
4510
(+ -2 P (EXPO X) (EXPT 2 (+ -1 Q)))))
4511
:hints (("Goal" :in-theory (enable drnd spn bias)
4512
:use ((:instance RND-EXACTP-A
4514
(n (+ -1 P (BIAS Q) (EXPO X)))))))))
4515
) ;;; END OF (EXACTP X (+ -2 P (EXPT 2 (- Q 1)) (EXPO X)))))
4519
(local (encapsulate ()
4522
(defthm expt-equal-specific-lemma
4523
(implies (and (EQUAL 0 (+ y x))
4526
(equal (expt 2 (+ 1 x))
4527
(expt 2 (+ 1 (* -1 y)))))
4528
:hints (("Goal" :cases ((equal x (* -1 y)))))))
4531
(defthm expt-equal-specific
4532
(implies (and (EQUAL 0 (+ (BIAS Q) (EXPO X)))
4536
(equal (expt 2 (+ 1 (expo x)))
4537
(expt 2 (+ 1 (* -1 (bias q))))))
4538
:hints (("Goal" :cases ((equal (expo x)
4539
(* -1 (bias q)))))))
4540
)) ;; don't know why we need this.
4545
(local (encapsulate ()
4547
(defthm minus-expt-reduce
4548
(implies (and (integerp p)
4552
(equal (+ -1 P (EXPO X) (EXPT 2 (+ -1 Q)))
4553
(+ 1 p (expo x) (* -1 (expo (spn q))))))
4554
:hints (("Goal" :in-theory (enable spn bias expo-2**n))))
4559
(local (encapsulate ()
4561
;;; (<= (- 2 P) (+ (EXPO X) (BIAS Q)))
4563
(defthm p-expo-x-expo-spn
4564
(implies (and (> (+ p (expo x))
4570
(>= (+ (BIAS Q) (EXPO x))
4572
:hints (("Goal" :in-theory (enable spn)))
4573
:rule-classes :linear))
4575
) ;;; END OF (<= (- 2 P) (+ (EXPO X) (BIAS Q)))
4579
(defthm drnd-exactp-a-lemma
4580
(implies (and (rationalp x)
4581
(< (EXPO (SPN Q)) (+ P (EXPO X)))
4588
(common-rounding-mode-p mode))
4589
(or (drepp (drnd x mode p q) p q)
4590
(= (drnd x mode p q) 0)
4591
(= (drnd x mode p q) (* (sgn x) (spn q)))))
4593
:hints (("Goal" :in-theory (e/d (drepp rnd) ())
4594
:do-not '(fertilize)
4595
:cases ((not (equal (expo (drnd x mode p q)) (expo x)))))
4596
("Subgoal 2" :use ((:instance less-than-spn-implies-expo-less)))
4597
("Subgoal 1" :in-theory (enable drepp exactp-2**n)
4598
:cases ((not (equal (drnd x mode p q) (expt 2 (+ 1 (expo x)))))))
4599
("Subgoal 1.2" :cases ((not (equal (expo x) (* -1 (bias q))))))
4600
("Subgoal 1.2.2" :in-theory (enable sgn spn))
4601
("Subgoal 1.2.1" :use ((:instance less-than-spn-implies-expo-less)))
4602
("Subgoal 1.1" :in-theory (enable drnd)
4603
:use ((:instance expo-rnd
4604
(n (+ P (EXPO X) (- (EXPO (SPN Q)))))))))))
4608
(implies (and (rationalp x)
4611
(equal (drepp (* -1 x) p q)
4613
:hints (("Goal" :in-theory (enable expo-minus drepp))))
4617
(defthm bias-expo-reduce
4618
(implies (and (integerp q)
4620
(equal (+ (bias q) (expo (spn q)))
4622
:hints (("Goal" :in-theory (enable spn)))))
4625
(defthm integerp-less-than
4626
(implies (and (integerp p)
4630
(<= (+ 1 (BIAS Q) (* -1 P) (EXPO (SPN Q))) 0))
4631
:hints (("Goal" :in-theory (enable spn)))
4632
:rule-classes :linear))
4636
(implies (and (integerp p)
4640
(EXACTP (EXPT 2 (+ 1 (* -1 P) (EXPO (SPN Q))))
4641
(+ -1 (EXPO (SPN Q))
4642
(EXPT 2 (+ -1 Q)))))
4643
:hints (("Goal" :in-theory (enable spn exactp-2**n bias)))))
4648
(defthm expt-2-no-greater-than-2
4649
(implies (and (integerp q)
4654
:hints (("Goal" :use ((:instance expt-weak-monotone-linear
4657
:rule-classes :linear))
4659
(defthm exactp-spn-p
4660
(implies (and (integerp p)
4665
:hints (("Goal" :in-theory (enable spn
4672
(defthm local-rewrite-hack
4673
(implies (and (equal (+ x (spn q)) 0)
4674
(< (EXPO (SPN Q)) (+ P (EXPO X)))
4675
(common-rounding-mode-p mode)
4683
(* -1 (EXPO (SPN Q))))))
4685
:hints (("Goal" :cases ((not (equal x (* -1 (spn
4687
:in-theory (enable rnd-exactp-b
4693
(defthm drnd-exactp-a1
4694
(implies (and (rationalp x)
4695
(<= (abs x) (spn q))
4700
(common-rounding-mode-p mode))
4701
(or (drepp (drnd x mode p q) p q)
4702
(= (drnd x mode p q) 0)
4703
(= (drnd x mode p q) (* (sgn x) (spn q)))))
4704
:hints (("Goal" :in-theory (enable rnd-minus drepp-minus
4706
flip drnd rnd-exactp-b
4707
expo-minus sgn-minus)
4708
:cases ((not (<= (+ p (expo x) (- (expo (spn q))))
4710
("Subgoal 2" :in-theory (enable drepp expo-minus sgn
4713
("Subgoal 1" :cases ((not (equal x 0))))
4714
("Subgoal 1.2" :in-theory (enable drnd))
4715
("Subgoal 1.1" :cases ((not (> x 0))))
4716
("Subgoal 1.1.2" :use ((:instance drnd-exactp-a-lemma)))
4717
("Subgoal 1.1.1" :use ((:instance drnd-exactp-a-lemma
4721
(:instance rnd-exactp-b
4723
(mode (flip mode))))))
4728
(defthm drnd-exactp-a
4729
(implies (and (rationalp x)
4730
(<= (abs x) (spn q))
4735
(common-rounding-mode-p mode))
4736
(or (drepp (drnd x mode p q) p q)
4737
(= (drnd x mode p q) 0)
4738
(= (drnd x mode p q) (* (sgn x) (spn q)))))
4739
:hints (("Goal" :cases ((not (equal (abs x) (spn q))))
4740
:in-theory (enable sgn drnd rnd-minus expo-minus))
4741
("Subgoal 2" :cases ((equal x (spn q))
4742
(equal x (* -1 (spn q)))))
4743
("Subgoal 1" :use drnd-exactp-a1))
4747
) ;; end of drnd-exactp-a
4750
;;; extremely bad proof!!
4752
;;; We could resolve to mid-range, small-range, large range.
4755
(defthmd drnd-exactp-b
4756
(implies (and (rationalp x)
4762
(common-rounding-mode-p mode))
4763
(equal (drnd x mode p q)
4765
:hints (("Goal" :in-theory (e/d (drepp spn bias drnd)
4766
(common-rounding-mode-p))
4767
:use ((:instance rnd-exactp-b
4768
(n (+ P (EXPO X) (- (EXPO (SPN Q))))))))))
4771
;----------------------------------------------------------------------
4776
(implies (and (integerp p)
4781
(<= (abs x) (spn q)))
4782
(<= (abs (drnd x 'trunc p q))
4784
:hints (("Goal" :in-theory (enable drnd rnd)
4785
:use ((:instance trunc-upper-bound
4787
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))))))
4790
(implies (and (integerp p)
4795
(<= (abs x) (spn q)))
4796
(>= (abs (drnd x 'away p q))
4798
:hints (("Goal" :in-theory (enable drnd rnd)
4799
:use ((:instance away-lower-bound
4801
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))))))
4804
(implies (and (integerp p)
4809
(<= (abs x) (spn q)))
4810
(<= (drnd x 'minf p q)
4812
:hints (("Goal" :in-theory (enable drnd rnd)
4813
:use ((:instance minf-lower-bound
4815
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))))))
4820
(implies (and (integerp p)
4825
(<= (abs x) (spn q)))
4826
(>= (drnd x 'inf p q)
4828
:hints (("Goal" :in-theory (enable drnd rnd)
4829
:use ((:instance inf-lower-bound
4831
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))))))
4835
;----------------------------------------------------------------------
4839
(defthm exactp-c-lemma-1
4840
(IMPLIES (AND (RATIONALP X)
4850
(<= (TRUNC X (+ P (EXPO X) (* -1 (EXPO (SPN Q)))))
4853
:use ((:instance trunc-upper-bound
4855
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q)))))))))
4856
:rule-classes :linear))
4859
;; (i-am-here) ;; Sun Oct 15 17:16:34 2006
4867
(local (include-book "float-extra2"))
4869
(implies (and (integerp p)
4875
(= m (/ r (spd p q))))
4879
(< m (expt 2 (1- p)))))))))
4883
(implies (and (integerp p)
4888
(EXPT 2 (+ 1 (* -1 P) (EXPO (SPN Q))))))
4889
:hints (("Goal" :in-theory (enable spd spn bias)))))
4892
(defund denormal-norm (r p q)
4896
(defthm spd-mult-specific
4897
(implies (and (integerp p)
4903
(= r (* (denormal-norm r p q) (spd p q))))
4904
:hints (("Goal" :in-theory (enable denormal-norm)))
4908
(defthm drepp-implies-denormal-norm-integerp
4909
(implies (and (drepp r p q)
4916
(integerp (denormal-norm r p q)))
4917
:hints (("Goal" :use ((:instance spd-mult
4918
(m (denormal-norm r p q)))
4919
(:instance spd-mult-specific))))
4920
:rule-classes :type-prescription))
4924
(defthm drepp-implies-denormal-norm-less-than
4925
(implies (and (drepp r p q)
4932
(<= (denormal-norm r p q)
4933
(+ -1 (expt 2 (+ -1 p)))))
4934
:hints (("Goal" :use ((:instance spd-mult
4935
(m (denormal-norm r p q)))
4936
(:instance spd-mult-specific))))
4937
:rule-classes :linear))
4940
(defthm denormal-normal-monotone
4941
(implies (and (< r1 r2)
4942
(integerp (denormal-norm r1 p q))
4943
(integerp (denormal-norm r2 p q)))
4944
(<= (+ 1 (denormal-norm r1 p q))
4945
(denormal-norm r2 p q)))
4946
:hints (("Goal" :in-theory (enable spd denormal-norm)))
4947
:rule-classes :linear))
4951
(implies (and (rationalp r1)
4961
(<= (+ r2 (EXPT 2 (+ 1 (* -1 P) (EXPO (SPN Q)))))
4963
:hints (("Goal" :use ((:instance spd-mult-specific
4965
(:instance spd-mult-specific
4967
(:instance denormal-normal-monotone
4975
(implies (and (integerp p)
4978
(equal (* (EXPT 2 (+ -1 P))
4979
(EXPT 2 (+ 2 (* -1 P) (* -1 (BIAS Q)))))
4980
(expt 2 (+ 1 (* -1 (bias q))))))
4981
:hints (("Goal" :in-theory (enable a15)))))
4986
(local (include-book "../../arithmetic/basic"))
4987
(defthm arithm-hack-specific
4988
(implies (and (<= (DENORMAL-NORM R P Q)
4989
(+ -1 (EXPT 2 (+ -1 P))))
4994
(<= (+ (EXPT 2 (+ 1 (* -1 P) (EXPO (SPN Q))))
4995
(* (EXPT 2 (+ 1 (* -1 P) (EXPO (SPN Q))))
4996
(denormal-norm r p q)))
4998
:hints (("Goal" :in-theory (e/d (spn denormal-norm
5000
:rule-classes nil)))
5003
(defthm maximal-drepp
5004
(implies (and (drepp r p q)
5011
(<= (+ r (EXPT 2 (+ 1 (* -1 P) (EXPO (SPN Q)))))
5013
:hints (("Goal" :use ((:instance drepp-implies-denormal-norm-less-than)
5014
(:instance spd-mult-specific)
5015
(:instance arithm-hack-specific))))
5016
:rule-classes :linear)
5020
(implies (and (rationalp r1)
5030
(<= (+ r2 (EXPT 2 (+ 1 (* -1 P) (EXPO (SPN Q)))))
5032
:hints (("Goal" :use ((:instance spd-mult-specific
5034
(:instance spd-mult-specific
5036
(:instance denormal-normal-monotone
5050
(defthm spd-spd-less-than
5051
(implies (and (integerp p)
5055
(iff (<= (SPD P Q) A)
5056
(<= (EXPT 2 (+ 1 (* -1 P) (EXPO (SPN Q))))
5058
:hints (("Goal" :in-theory (enable spn spd)))))
5060
(defthm exactp-c-lemma-2
5061
(implies (and (integerp p)
5070
(<= (abs x) (spn q)))
5071
(<= (AWAY X (+ P (EXPO X) (* -1 (EXPO (SPN Q)))))
5073
:hints (("Goal" :cases ((not (>= (+ p (expo x)) (expo (spn q))))))
5075
:in-theory (enable drnd rnd sgn positive-spd)
5076
:use ((:instance drnd-exactp-a
5078
(:instance away-upper-bound
5080
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))
5081
(:instance drepp-diff
5083
(r1 (AWAY X (+ P (EXPO X)
5084
(* -1 (EXPO (SPN Q)))))))))
5085
("Subgoal 1" :in-theory (enable drnd rnd away cg sgn)
5086
:use ((:instance smallest-spd (r a)))))
5087
:rule-classes :linear)))
5091
(defthmd drnd-exactp-c-lemma
5092
(implies (and (rationalp x)
5094
(<= (abs x) (spn q))
5102
(common-rounding-mode-p mode))
5103
(>= a (drnd x mode p q)))
5104
:hints (("Goal" :in-theory (enable sgn drnd rnd))
5106
:use ((:instance near-choice
5108
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))))
5110
:use ((:instance near+-choice
5112
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q)))))))))))
5118
(defthm exactp-d-lemma-1
5119
(IMPLIES (AND (RATIONALP X)
5129
(<= A (AWAY X (+ P (EXPO X) (* -1 (EXPO (SPN Q)))))))
5131
:use ((:instance away-lower-bound
5133
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q)))))))))
5134
:rule-classes :linear))
5139
;; (defthm never-zero-drepp
5140
;; (not (DREPP 0 P Q))
5141
;; :hints (("Goal" :in-theory (enable drepp)))))
5145
(defthm x-less-than-spd-if-negative
5146
(implies (and (<= (+ P (EXPO X) (* -1 (EXPO (SPN Q)))) 0)
5153
:hints (("Goal" :in-theory (enable spd spn)
5154
:use ((:instance expo-monotone
5159
(defthm exactp-d-lemma-2
5160
(IMPLIES (AND (RATIONALP X)
5172
(+ P (EXPO X) (* -1 (EXPO (SPN Q)))))))
5173
:hints (("Goal" :cases ((not (> (+ p (expo x)) (expo (spn q))))))
5175
:in-theory (enable drnd rnd sgn positive-spd)
5176
:use ((:instance drnd-exactp-a
5178
(:instance trunc-lower-bound
5180
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))
5181
(:instance drepp-diff
5183
(r2 (trunc X (+ P (EXPO X)
5184
(* -1 (EXPO (SPN Q)))))))))
5185
("Subgoal 1" :in-theory (enable drnd rnd spd trunc sgn)
5186
:use ((:instance smallest-spd (r a))
5187
(:instance x-less-than-spd-if-negative))))
5188
:rule-classes :linear))
5191
(defthmd drnd-exactp-d-lemma
5192
(implies (and (rationalp x)
5193
(<= (abs x) (spn q))
5202
(common-rounding-mode-p mode))
5203
(<= a (drnd x mode p q)))
5204
:hints (("Goal" :in-theory (enable ieee-mode-p drnd rnd))
5206
:use ((:instance near+-choice
5208
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))))
5210
:use ((:instance near-choice
5212
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))))))
5217
(defthmd drnd-exactp-c
5218
(implies (and (rationalp x)
5219
(<= (abs x) (spn q))
5227
(common-rounding-mode-p mode))
5228
(>= a (drnd x mode p q)))
5229
:hints (("Goal" :cases ((not (equal x 0)))
5230
:in-theory (enable drnd-minus flip drepp-minus))
5231
("Subgoal 2" :in-theory (enable drnd rnd))
5232
("Subgoal 1" :cases ((not (> x 0))))
5233
("Subgoal 1.2" :use ((:instance drnd-exactp-c-lemma)))
5234
("Subgoal 1.1" :use ((:instance drnd-exactp-d-lemma
5237
(mode (flip mode)))))))
5241
(defthmd drnd-exactp-d
5242
(implies (and (rationalp x)
5243
(<= (abs x) (spn q))
5251
(common-rounding-mode-p mode))
5252
(<= a (drnd x mode p q)))
5253
:hints (("Goal" :cases ((not (equal x 0)))
5254
:in-theory (enable drnd-minus flip drepp-minus))
5255
("Subgoal 2" :in-theory (enable drnd rnd))
5256
("Subgoal 1" :cases ((not (> x 0))))
5257
("Subgoal 1.2" :use ((:instance drnd-exactp-d-lemma)))
5258
("Subgoal 1.1" :use ((:instance drnd-exactp-c-lemma
5261
(mode (flip mode)))))))
5265
;----------------------------------------------------------------------
5272
(implies (and (integerp p)
5277
(EXPT 2 (+ 1 (* -1 P) (EXPO (SPN Q))))))
5278
:hints (("Goal" :in-theory (enable spd spn bias)))))
5281
(defthm x-less-than-spd-if-negative
5282
(implies (and (<= (+ P (EXPO X) (* -1 (EXPO (SPN Q)))) 0)
5289
:hints (("Goal" :in-theory (enable spd spn)
5290
:use ((:instance expo-monotone
5294
(defthm drnd-non-negative
5295
(implies (and (< 0 x)
5301
(common-rounding-mode-p mode))
5302
(>= (drnd x mode p q) 0))
5303
:hints (("Goal" :in-theory (enable ieee-mode-p near near+ drnd rnd)))
5304
:rule-classes (:type-prescription :linear))
5308
(defthm drnd-diff-lemma
5309
(implies (and (rationalp x)
5316
(common-rounding-mode-p mode))
5317
(< (abs (- x (drnd x mode p q))) (spd p q)))
5318
:hints (("Goal" :cases ((not (> (+ p (expo x)) (expo (spn q))))))
5319
("Subgoal 2" :in-theory (enable drnd)
5320
:use ((:instance rnd-diff
5321
(n (+ P (EXPO X) (* -1 (EXPO (SPN
5324
:use ((:instance drnd-exactp-c
5326
(:instance drepp-spd)
5327
(:instance x-less-than-spd-if-negative)))))))
5330
(implies (and (rationalp x)
5331
(<= (abs x) (spn q))
5336
(common-rounding-mode-p mode))
5337
(< (abs (- x (drnd x mode p q))) (spd p q)))
5338
:hints (("Goal" :cases ((not (equal x 0))))
5339
("Subgoal 2" :in-theory (enable drnd rnd spd))
5340
("Subgoal 1" :cases ((not (> x 0))))
5341
("Subgoal 1.2" :use ((:instance drnd-diff-lemma)))
5342
("Subgoal 1.1" :in-theory (enable flip drnd drnd-minus)
5343
:use ((:instance drnd-diff-lemma
5345
(mode (flip mode)))))))
5349
;----------------------------------------------------------------------
5354
(defthm drnd-near-est-lemma-1
5355
(implies (and (rationalp x)
5356
(equal (expo a) (expo x))
5364
(>= (abs (- x a)) (abs (- x (drnd x 'near p q)))))
5366
:in-theory (enable rnd drnd bias DREPP spn)
5367
:use ((:instance near2
5369
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q)))))))))))
5374
(defthm rationalp-drepp
5375
(implies (drepp a p q)
5377
:hints (("Goal" :in-theory (enable drepp)))
5378
:rule-classes :forward-chaining))
5381
(defthm drnd-near-est-lemma-2-1
5382
(implies (and (rationalp x)
5384
(equal (- x (trunc x (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))
5385
(- (away x (+ P (EXPO X) (* -1 (EXPO (SPN Q))))) x))
5393
(>= (abs (- x a)) (abs (- x (drnd x 'near p q)))))
5394
:hints (("Goal" :in-theory (enable drnd rnd)
5395
:use ((:instance near-choice (x x)
5396
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q)))))))))))
5400
(defthm drnd-near-est-lemma-2-2
5401
(implies (and (rationalp x)
5403
(not (equal (expo x) (expo a)))
5404
(< (- x (trunc x (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))
5405
(- (away x (+ P (EXPO X) (* -1 (EXPO (SPN Q))))) x))
5413
(>= (abs (- x a)) (abs (- x (drnd x 'near p q)))))
5414
:hints (("Goal" :in-theory (enable drnd rnd)
5415
:do-not '(fertilize)
5416
:use ((:instance near1-a
5417
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))
5418
(:instance trunc-upper-bound
5419
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q)))))))))))
5425
(defthm drnd-near-est-lemma-2-3
5426
(implies (and (rationalp x)
5428
(not (equal (expo x) (expo a)))
5429
(> (- x (trunc x (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))
5430
(- (away x (+ P (EXPO X) (* -1 (EXPO (SPN Q))))) x))
5438
(>= (abs (- x a)) (abs (- x (drnd x 'near p q)))))
5439
:hints (("Goal" :in-theory (enable drnd rnd)
5440
:do-not '(fertilize)
5441
:use ((:instance near1-b
5442
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))
5443
(:instance away-lower-bound
5444
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q)))))))))))
5451
(defthm drnd-near-est-lemma-2
5452
(implies (and (rationalp x)
5454
(not (equal (expo a) (expo x)))
5462
(>= (abs (- x a)) (abs (- x (drnd x 'near p q)))))
5463
:hints (("Goal" :cases ((not (equal (- x (trunc x (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))
5464
(- (away x (+ P (EXPO X) (* -1 (EXPO (SPN
5466
:in-theory (disable abs drnd))
5467
("Subgoal 2" :use ((:instance drnd-near-est-lemma-2-1)))
5468
("Subgoal 1" :cases ((not (< (- x (trunc x (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))
5469
(- (away x (+ P (EXPO X) (* -1 (EXPO (SPN
5471
("Subgoal 1.2" :use ((:instance drnd-near-est-lemma-2-2)))
5472
("Subgoal 1.1" :use ((:instance drnd-near-est-lemma-2-3))))))
5478
(defthm drnd-near-est-lemma-3
5479
(implies (and (rationalp x)
5481
(not (equal (expo a) (expo x)))
5489
(>= (abs (- x a)) (abs (- x (drnd x 'near p q)))))
5490
:hints (("Goal" :use ((:instance smallest-spd (r a))
5491
(:instance drnd-diff
5497
(defthm never-zero-drepp
5499
:hints (("Goal" :in-theory (enable drepp)))))
5502
(defthm drnd-near-est-lemma
5503
(implies (and (rationalp x)
5511
(>= (abs (- x a)) (abs (- x (drnd x 'near p q)))))
5512
:hints (("Goal" :cases ((not (equal (expo a) (expo x)))))
5513
("Subgoal 2" :use ((:instance drnd-near-est-lemma-1)))
5514
("Subgoal 1":cases ((not (equal a 0))))
5515
("Subgoal 1.1":cases ((not (> a 0))))
5516
("Subgoal 1.1.2":use ((:instance drnd-near-est-lemma-2)))
5517
("Subgoal 1.1.1":use ((:instance drnd-near-est-lemma-3))))))
5519
(defthm drnd-near-est
5520
(implies (and (rationalp x)
5521
(<= (abs x) (spn q))
5527
(>= (abs (- x a)) (abs (- x (drnd x 'near p q)))))
5528
:hints (("Goal" :cases ((not (equal x 0))))
5529
("Subgoal 2" :in-theory (enable drnd rnd))
5530
("Subgoal 1" :cases ((not (> x 0))))
5531
("Subgoal 1.2" :use ((:instance drnd-near-est-lemma)))
5532
("Subgoal 1.1" :use ((:instance drnd-near-est-lemma
5535
:in-theory (enable drnd-minus))))
5539
;----------------------------------------------------------------------
5544
(defthm drnd-near+-est-lemma-1
5545
(implies (and (rationalp x)
5546
(equal (expo a) (expo x))
5554
(>= (abs (- x a)) (abs (- x (drnd x 'near+ p q)))))
5556
:in-theory (enable rnd drnd bias DREPP spn)
5557
:use ((:instance near+2
5559
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q)))))))))))
5565
(defthm rationalp-drepp
5566
(implies (drepp a p q)
5568
:hints (("Goal" :in-theory (enable drepp)))
5569
:rule-classes :forward-chaining))
5574
(defthm drnd-near+-est-lemma-2-1
5575
(implies (and (rationalp x)
5577
(equal (- x (trunc x (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))
5578
(- (away x (+ P (EXPO X) (* -1 (EXPO (SPN Q))))) x))
5586
(>= (abs (- x a)) (abs (- x (drnd x 'near+ p q)))))
5587
:hints (("Goal" :in-theory (enable drnd rnd)
5588
:use ((:instance near+-choice (x x)
5589
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q)))))))))))
5592
;----------------------------------------------------------------------
5597
(defthm drnd-near+-est-lemma-2-2
5598
(implies (and (rationalp x)
5600
(not (equal (expo x) (expo a)))
5601
(< (- x (trunc x (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))
5602
(- (away x (+ P (EXPO X) (* -1 (EXPO (SPN Q))))) x))
5610
(>= (abs (- x a)) (abs (- x (drnd x 'near+ p q)))))
5611
:hints (("Goal" :in-theory (enable drnd rnd)
5612
:do-not '(fertilize)
5613
:use ((:instance near+1-a
5614
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))
5615
(:instance trunc-upper-bound
5616
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q)))))))))))
5619
(defthm drnd-near+-est-lemma-2-3
5620
(implies (and (rationalp x)
5622
(not (equal (expo x) (expo a)))
5623
(> (- x (trunc x (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))
5624
(- (away x (+ P (EXPO X) (* -1 (EXPO (SPN Q))))) x))
5632
(>= (abs (- x a)) (abs (- x (drnd x 'near+ p q)))))
5633
:hints (("Goal" :in-theory (enable drnd rnd)
5634
:do-not '(fertilize)
5635
:use ((:instance near+1-b
5636
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))
5637
(:instance away-lower-bound
5638
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q)))))))))))
5642
(defthm drnd-near+-est-lemma-2
5643
(implies (and (rationalp x)
5645
(not (equal (expo a) (expo x)))
5653
(>= (abs (- x a)) (abs (- x (drnd x 'near+ p q)))))
5654
:hints (("Goal" :cases ((not (equal (- x (trunc x (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))
5655
(- (away x (+ P (EXPO X) (* -1 (EXPO (SPN
5657
:in-theory (disable abs drnd))
5658
("Subgoal 2" :use ((:instance drnd-near+-est-lemma-2-1)))
5659
("Subgoal 1" :cases ((not (< (- x (trunc x (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))
5660
(- (away x (+ P (EXPO X) (* -1 (EXPO (SPN
5662
("Subgoal 1.2" :use ((:instance drnd-near+-est-lemma-2-2)))
5663
("Subgoal 1.1" :use ((:instance drnd-near+-est-lemma-2-3))))))
5666
;----------------------------------------------------------------------
5669
(defthm drnd-near+-est-lemma-3
5670
(implies (and (rationalp x)
5672
(not (equal (expo a) (expo x)))
5680
(>= (abs (- x a)) (abs (- x (drnd x 'near+ p q)))))
5681
:hints (("Goal" :use ((:instance smallest-spd (r a))
5682
(:instance drnd-diff
5687
(defthm never-zero-drepp
5689
:hints (("Goal" :in-theory (enable drepp)))))
5694
(defthm drnd-near+-est-lemma
5695
(implies (and (rationalp x)
5703
(>= (abs (- x a)) (abs (- x (drnd x 'near+ p q)))))
5704
:hints (("Goal" :cases ((not (equal (expo a) (expo x)))))
5705
("Subgoal 2" :use ((:instance drnd-near+-est-lemma-1)))
5706
("Subgoal 1":cases ((not (equal a 0))))
5707
("Subgoal 1.1":cases ((not (> a 0))))
5708
("Subgoal 1.1.2":use ((:instance drnd-near+-est-lemma-2)))
5709
("Subgoal 1.1.1":use ((:instance drnd-near+-est-lemma-3))))))
5711
(defthm drnd-near+-est
5712
(implies (and (rationalp x)
5713
(<= (abs x) (spn q))
5719
(>= (abs (- x a)) (abs (- x (drnd x 'near+ p q)))))
5720
:hints (("Goal" :cases ((not (equal x 0))))
5721
("Subgoal 2" :in-theory (enable drnd rnd))
5722
("Subgoal 1" :cases ((not (> x 0))))
5723
("Subgoal 1.2" :use ((:instance drnd-near+-est-lemma)))
5724
("Subgoal 1.1" :use ((:instance drnd-near+-est-lemma
5727
:in-theory (enable drnd-minus))))
5732
;; Sat Feb 4 12:35:01 2006 finally!
5734
;----------------------------------------------------------------------
5740
(local (encapsulate ()
5742
(defthm fl-expt-n-minus-1-minus-1
5743
(implies (and (rationalp x)
5744
(case-split (not (equal x 0)))
5747
(equal (fl (* -1 (sig x) (expt 2 (+ -1 n))))
5749
:hints (("Goal" :use ((:instance fl-1/2-sig-x-is-zero-lemma-2
5750
(y (expt 2 (+ -1 n))))
5751
(:instance expt-weak-monotone-linear
5756
(defthm n-zero-away-reduce
5757
(implies (and (rationalp x)
5762
(EXPT 2 (+ 1 (EXPO X) (* -1 n)))))
5763
:hints (("Goal" :in-theory (enable sgn away cg))))
5766
(defthm drnd-lemma-trunc-small
5767
(implies (and (natp p)
5773
(<= (+ p (expo x)) (expo (spn q))))
5774
(equal (drnd x 'trunc p q) 0))
5775
:hints (("Goal" :in-theory (enable drnd rnd))))
5778
(defthm drnd-lemma-away-small
5779
(implies (and (natp p)
5785
(<= (+ p (expo x)) (expo (spn q))))
5786
(equal (drnd x 'away p q)
5787
(expt 2 (+ 1 (EXPO (SPN Q)) (* -1 p)))))
5788
:hints (("Goal" :in-theory (enable drnd rnd))))
5792
(defthm drnd-lemma-minf-small
5793
(implies (and (natp p)
5799
(<= (+ p (expo x)) (expo (spn q))))
5800
(equal (drnd x 'minf p q) 0))
5801
:hints (("Goal" :in-theory (enable drnd rnd))))
5805
(defthm drnd-lemma-inf-small
5806
(implies (and (natp p)
5812
(<= (+ p (expo x)) (expo (spn q))))
5813
(equal (drnd x 'inf p q)
5814
(expt 2 (+ 1 (EXPO (SPN Q)) (* -1 p)))))
5815
:hints (("Goal" :in-theory (enable drnd rnd))))
5820
(defthm local-expt-expand
5821
(implies (and (integerp p)
5824
(equal (EXPT 2 (+ 1 (* -1 P) (EXPO (SPN Q))))
5825
(* 2 (expt 2 (+ (* -1 p) (expo (spn q)))))))
5826
:hints (("Goal" :use ((:instance a15 (i 2) (j1 1)
5827
(j2 (+ (* -1 P) (EXPO (SPN Q))))))))))
5830
(defthm drnd-lemma-near-small-1
5831
(implies (and (natp p)
5837
(< x (expt 2 (+ (* -1 p) (expo (spn q)))))
5838
(<= (+ p (expo x)) (expo (spn q))))
5839
(equal (drnd x 'near p q)
5841
:hints (("Goal" :in-theory (enable drnd rnd)
5842
:use ((:instance near1-a (n (+ p (expo x) (* -1 (expo (spn
5846
(defthm drnd-lemma-near-small-2
5847
(implies (and (natp p)
5853
(> x (expt 2 (+ (* -1 p) (expo (spn q)))))
5854
(<= (+ p (expo x)) (expo (spn q))))
5855
(equal (drnd x 'near p q)
5856
(expt 2 (+ 1 (EXPO (SPN Q)) (* -1 p)))))
5857
:hints (("Goal" :in-theory (enable drnd rnd)
5858
:use ((:instance near1-b (n (+ p (expo x) (* -1 (expo (spn q))))))))))
5863
(defthm drnd-lemma-near+-small-1
5864
(implies (and (natp p)
5870
(< x (expt 2 (+ (* -1 p) (expo (spn q)))))
5871
(<= (+ p (expo x)) (expo (spn q))))
5872
(equal (drnd x 'near+ p q)
5874
:hints (("Goal" :in-theory (enable drnd rnd)
5875
:use ((:instance near+1-a (n (+ p (expo x) (* -1 (expo (spn
5879
(defthm drnd-lemma-near+-small-2
5880
(implies (and (natp p)
5886
(> x (expt 2 (+ (* -1 p) (expo (spn q)))))
5887
(<= (+ p (expo x)) (expo (spn q))))
5888
(equal (drnd x 'near+ p q)
5889
(expt 2 (+ 1 (EXPO (SPN Q)) (* -1 p)))))
5890
:hints (("Goal" :in-theory (enable drnd rnd)
5891
:use ((:instance near+1-b (n (+ p (expo x) (* -1 (expo (spn q))))))))))
5896
(defthm spd-/2-rewrite
5897
(implies (and (integerp p)
5900
(equal (/ (spd p q) 2)
5901
(expt 2 (+ (* -1 p) (expo (spn q))))))
5902
:hints (("Goal" :in-theory (enable spd spn)
5903
:use ((:instance a15 (i 2) (j1 1)
5904
(j2 (+ 1 (* -1 P) (* -1 (BIAS Q))))))))))
5907
(defthm less-than-1/2-spd-implies-expo-x-small
5908
(implies (and (< x (expt 2 (+ (* -1 p) (expo (spn q)))))
5914
(<= (+ p (expo x)) (expo (spn q))))
5915
:hints (("Goal" :use ((:instance expo-monotone
5917
(y (expt 2 (+ (* -1 p) (expo (spn
5919
:in-theory (enable expo-2**n)))))
5921
(defthm drnd-tiny-equal-lemma
5922
(implies (and (common-rounding-mode-p mode)
5929
(< x (/ (spd p q) 2))
5932
(< y (/ (spd p q) 2)))
5933
(equal (drnd x mode p q)
5935
:hints (("Goal" :in-theory (enable ieee-mode-p)))
5939
(defthm sticky-never-increase-over-expt
5940
(implies (and (< x (expt 2 k))
5948
:hints (("Goal" :use ((:instance expo-sticky)
5949
(:instance expo-monotone
5952
(:instance expt-weak-monotone-linear
5955
(:instance expo-lower-bound
5958
(defthm sticky-preserves-inequality
5959
(implies (and (< x (expt 2 (+ (* -1 p) (expo (spn q)))))
5969
(expt 2 (+ (* -1 p) (expo (spn q))))))
5970
:hints (("Goal" :use ((:instance sticky-never-increase-over-expt
5972
(expo (spn q)))))))))
5974
(defthm greater-than-1/2-spd-implies-n-no-less-than-2
5975
(implies (and (> x (expt 2 (+ (* -1 p) (expo (spn q)))))
5982
(>= n (+ p (expo x) (- (expo (spn q))) 2))
5986
:hints (("Goal" :use ((:instance expo-monotone
5987
(x (expt 2 (+ (* -1 p) (expo (spn q)))))
5989
:in-theory (enable expo-2**n)))
5993
(defthm trunc-1-m-is-1
5994
(implies (and (integerp n)
5998
:hints (("Goal" :in-theory (enable trunc a15)))))
6001
(implies (and (integerp n)
6004
(equal (trunc (expt 2 n) m)
6006
:hints (("Goal" :use ((:instance trunc-shift
6010
:in-theory (enable trunc))))
6013
(defthm sticky-preserves-inequality-2-strong
6014
(implies (and (> x (expt 2 (+ (* -1 p) (expo (spn q)))))
6021
(>= n (+ p (expo x) (- (expo (spn q))) 2))
6025
(expt 2 (+ (* -1 p) (expo (spn q))))))
6026
:hints (("Goal" :in-theory (enable sticky trunc-shift sgn)
6027
:use ((:instance trunc-monotone
6028
(x (expt 2 (+ (* -1 p) (expo (spn q)))))
6031
(:instance greater-than-1/2-spd-implies-n-no-less-than-2)))))
6034
(defthm exactp-expt-2-1
6035
(implies (and (integerp n)
6038
(exactp (expt 2 m) n))
6039
:hints (("Goal" :in-theory (enable a15 sig exactp))))
6042
(defthm equal-x-1/2-spd-sticky-n-1/2-spd
6043
(implies (and (integerp p)
6049
(equal (sticky (expt 2 (+ (* -1 p) (expo (spn q)))) n)
6050
(expt 2 (+ (* -1 p) (expo (spn q))))))
6051
:hints (("Goal" :in-theory (e/d (expo-2**n sticky)
6053
:use ((:instance exactp-expt-2-1
6054
(m (+ (* -1 P) (EXPO (SPN Q))))
6058
(defthm expo-sticky-strong
6059
(implies (and (rationalp x)
6060
(integerp n) (> n 0))
6061
(= (expo (sticky x n))
6063
:hints (("Goal" :cases ((not (> x 0)))
6064
:in-theory (enable expo-minus sticky-minus))
6065
("Subgoal 2" :use ((:instance expo-sticky)))
6066
("Subgoal 1" :use ((:instance expo-sticky
6070
;----------------------------------------------------------------------
6072
(defthm n-equal-zero-implies-ultra-small
6073
(implies (and (>= 0 (+ p (expo x) (- (expo (spn q))) 2))
6080
(< x (expt 2 (+ -1 (* -1 p) (expo (spn q))))))
6081
:hints (("Goal" :use ((:instance expo-upper-bound)
6082
(:instance expt-weak-monotone-linear
6084
(m (+ -1 (* -1 p) (expo (spn q)))))))))
6087
;; (i-am-here) ;; Sun Oct 15 18:19:29 2006
6091
(defthm sticky-0-reduce
6092
(implies (and (> x 0)
6095
(EXPT 2 (1+ (EXPO X)))))
6096
:hints (("Goal" :in-theory (e/d (sticky exactp sgn)
6099
:use ((:instance sig-lower-bound)
6100
(:instance sig-upper-bound)))))
6104
(defthm small-fl-is-minus-1
6105
(implies (and (rationalp x)
6112
(< x (expt 2 (+ -1 (* -1 p) (expo (spn q))))))
6113
(equal (FL (* -1 (SIG X)
6116
(* -1 (EXPO (SPN Q)))))))
6118
:hints (("Goal" :use ((:instance fl-1/2-sig-x-is-zero-2)
6119
(:instance expo-monotone
6121
(y (expt 2 (+ -1 (* -1 p) (expo (spn q))))))))))
6124
(defthm small-fl-is-zero-1
6125
(implies (and (rationalp x)
6132
(< x (expt 2 (+ -1 (* -1 p) (expo (spn q))))))
6133
(equal (FL (* (SIG X)
6136
(* -1 (EXPO (SPN Q)))))))
6138
:hints (("Goal" :use ((:instance fl-1/2-sig-x-is-zero)
6139
(:instance expo-monotone
6141
(y (expt 2 (+ -1 (* -1 p) (expo (spn q))))))))))
6146
(defthm small-fl-is-minus-1-v2
6147
(implies (and (rationalp x)
6154
(< x (expt 2 (+ -1 (* -1 p) (expo (spn q))))))
6155
(equal (FL (* -1 (SIG (EXPT 2 (+ 1 (EXPO X))))
6157
(+ P (EXPO X) (* -1 (EXPO (SPN Q)))))))
6159
:hints (("Goal" :use ((:instance fl-1/2-sig-x-is-zero-2
6160
(x (expt 2 (+ 1 (expo x)))))
6161
(:instance expo-monotone
6163
(y (expt 2 (+ -1 (* -1 p) (expo (spn q))))))))))
6167
(defthm small-fl-is-zero-1-v2
6168
(implies (and (rationalp x)
6175
(< x (expt 2 (+ -1 (* -1 p) (expo (spn q))))))
6176
(equal (FL (* (SIG (EXPT 2 (+ 1 (EXPO X))))
6178
(+ P (EXPO X) (* -1 (EXPO (SPN Q)))))))
6180
:hints (("Goal" :use ((:instance fl-1/2-sig-x-is-zero
6181
(x (expt 2 (+ 1 (expo x)))))
6182
(:instance expo-monotone
6184
(y (expt 2 (+ -1 (* -1 p) (expo (spn q))))))))))
6187
;; (defthm expo-monotone-strong
6188
;; (implies (and (< x (expt 2 n))
6193
(defthm small-small-lemma
6194
(implies (<= (+ 2 P (EXPO X)) (EXPO (SPN Q)))
6195
(<= (+ -1 p (expo x) (* -1 (expo (spn q))))
6198
(defthm small-small-lemma-2
6199
(implies (<= (+ 2 P (EXPO X)) (EXPO (SPN Q)))
6200
(<= (+ p (expo x) (* -1 (expo (spn q))))
6203
(defthm small-is-small
6204
(implies (and (>= 0 (+ p (expo x) (- (expo (spn q))) 2))
6216
(* -1 (EXPO (SPN q))))))))
6217
:hints (("Goal" :use ((:instance sig-upper-bound)
6218
(:instance expt-weak-monotone-linear
6220
(* -1 (EXPO (SPN q)))))
6222
:rule-classes :linear)
6226
(defthm sig-expt-fact
6227
(implies (integerp n)
6228
(equal (sig (expt 2 n)) 1))
6229
:hints (("Goal" :in-theory (enable sig a15)))))
6231
(defthm small-is-small-v2
6232
(implies (and (>= 0 (+ p (expo x) (- (expo (spn q))) 2))
6241
(* 2 (SIG (EXPT 2 (+ 1 (EXPO X))))
6243
(+ P (EXPO X) (* -1 (EXPO (SPN Q))))))))
6244
:hints (("Goal" :use ((:instance expt-weak-monotone-linear
6246
(* -1 (EXPO (SPN q)))))
6248
:rule-classes :linear))
6253
(defthm extra-small-drnd-is-equal
6254
(implies (and (< x (expt 2 (+ -1 (* -1 p) (expo (spn q)))))
6255
(>= 0 (+ p (expo x) (- (expo (spn q))) 2))
6263
(equal (drnd (sticky x 0) mode p q)
6265
:hints (("Goal" :in-theory (enable drnd trunc sgn cg near+ near away rnd sticky))))
6268
(defthm drnd-sticky-lemma
6269
(implies (and (common-rounding-mode-p mode)
6279
(>= n (+ p (expo x) (- (expo (spn q))) 2)))
6280
(equal (drnd (sticky x n) mode p q)
6282
:hints (("Goal" :cases ((not (> (+ p (expo x)) (expo (spn q))))))
6283
("Subgoal 2" :cases ((not (equal n 0))))
6284
("Subgoal 2.1" :use ((:instance rnd-sticky
6286
(- (expo (spn q)))))))
6287
:in-theory (enable drnd))
6288
("Subgoal 1" :in-theory (e/d (common-rounding-mode-p
6289
sticky-positive ieee-mode-p)
6291
:cases ((not (equal x (expt 2 (+ (* -1 p)
6292
(expo (spn q))))))))
6293
("Subgoal 1.1" :cases ((not (equal n 0))))
6294
("Subgoal 1.1.2" :use ((:instance extra-small-drnd-is-equal)
6296
n-equal-zero-implies-ultra-small)))
6297
("Subgoal 1.1.1" :cases ((not (> x (expt 2 (+ (* -1 p)
6298
(expo (spn q)))))))))
6299
:rule-classes nil)))
6303
(implies (and (common-rounding-mode-p mode)
6309
(<= (abs x) (spn q))
6311
(>= n (+ p (expo x) (- (expo (spn q))) 2)))
6312
(equal (drnd (sticky x n) mode p q)
6315
:hints (("Goal" :cases ((not (equal x 0)))
6316
:in-theory (enable sticky-minus expo-minus
6318
("Subgoal 1" :cases ((not (> x 0))))
6319
("Subgoal 1.2" :use ((:instance drnd-sticky-lemma)))
6320
("Subgoal 1.1" :use ((:instance drnd-sticky-lemma
6322
(mode (flip mode)))))))
6327
(defthm drnd-tiny-equal
6328
(implies (and (common-rounding-mode-p mode)
6335
(< (abs x) (/ (spd p q) 2))
6338
(< (abs y) (/ (spd p q) 2)))
6339
(equal (drnd x mode p q)
6341
:hints (("Goal" :use ((:instance drnd-tiny-equal-lemma))))
6346
;----------------------------------------------------------------------
6349
(local (encapsulate ()
6352
;; (implies (and (rationalp x)
6357
;; (exactp x (+ -1 k (- (expo x) (expo y))))
6358
;; (common-rounding-mode-p mode))
6359
;; (= (+ x (rnd y mode k))
6362
;; (+ k (- (expo (+ x y)) (expo y))))))
6363
;; :hints (("Goal" :use ((:instance plus-rnd---rtl-rel5-support))))
6364
;; :rule-classes ())
6366
(defthm exactp-spn-fact
6367
(implies (and (integerp p)
6371
(EXACTP (SPN Q) (+ -1 P)))
6372
:hints (("Goal" :in-theory (enable spn exactp-2**n))))
6374
(defthm exactp-spn-fact-2
6375
(implies (and (integerp p)
6380
:hints (("Goal" :in-theory (enable spn exactp-2**n))))
6382
(defthm exactp-spn-fact-3
6383
(implies (and (integerp p)
6387
(EXACTP (* 2 (SPN Q)) P))
6388
:hints (("Goal" :in-theory (enable spn exactp-2**n)
6389
:use ((:instance a15 (i 2) (j1 1) (j2 (+ 1 (* -1 (BIAS Q)))))))))
6392
;; (defthm expo-unique
6393
;; (implies (and (<= (expt 2 n) (abs x))
6394
;; (< (abs x) (expt 2 (1+ n)))
6397
;; (equal n (expo x)))
6398
;; :rule-classes ())
6403
(defthm local-expt-expand
6404
(implies (integerp n)
6405
(equal (EXPT 2 (+ 1 n))
6407
:hints (("Goal" :use ((:instance a15 (i 2) (j1 1)
6410
(defthm expo-x-plus-spn-equal-expo-spn-lemma
6411
(implies (and (rationalp x)
6415
(equal (expo (+ x (expt 2 n)))
6417
:hints (("Goal" :use ((:instance expo-unique
6418
(x (+ x (expt 2 n)))
6420
:in-theory (enable expo-2**n
6425
(defthm expo-x-plus-spn-equal-expo-spn
6426
(implies (and (rationalp x)
6431
(equal (expo (+ x (spn q)))
6433
:hints (("Goal" :in-theory (e/d (spn expo-2**n) ())
6434
:use ((:instance expo-x-plus-spn-equal-expo-spn-lemma
6435
(n (expo (spn q))))))))
6440
(defthmd drnd-rewrite-lemma
6441
(implies (and (rationalp x)
6444
(common-rounding-mode-p mode)
6449
(equal (drnd x mode p q)
6450
(- (rnd (+ x (* (sgn x) (spn q))) mode p)
6451
(* (sgn x) (spn q)))))
6452
:hints (("Goal" :cases ((not (equal x (spn q)))))
6453
("Subgoal 2" :in-theory (e/d (drnd sgn)
6455
:use ((:instance rnd-exactp-b (x (spn q))
6457
(:instance rnd-exactp-b (x (* 2 (spn q)))
6459
("Subgoal 1" :use ((:instance
6463
(k (+ p (expo x) (* -1 (expo (spn q)))))))
6464
:in-theory (e/d (drnd sgn bias exactp-2**n) (common-rounding-mode-p)))))
6467
(defthm collect-neg-specific
6468
(equal (+ (* -1 X) (* -1 (SGN X) (SPN Q)))
6469
(* -1 (+ x (* (sgn x) (spn q))))))))
6471
(defthmd drnd-rewrite
6472
(implies (and (rationalp x)
6473
(<= (abs x) (spn q))
6474
(common-rounding-mode-p mode)
6479
(equal (drnd x mode p q)
6480
(- (rnd (+ x (* (sgn x) (spn q))) mode p)
6481
(* (sgn x) (spn q)))))
6482
:hints (("Goal" :cases ((not (>= x 0))))
6483
("Subgoal 2" :use ((:instance drnd-rewrite-lemma)))
6484
("Subgoal 1" :use ((:instance drnd-rewrite-lemma
6486
(mode (flip mode))))
6487
:in-theory (enable drnd-minus sgn-minus
6488
rnd-minus expo-minus flip))))
6492
;----------------------------------------------------------------------