← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/rtl/rel6/support/lib1/round.lisp

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/rtl/rel6/support/lib1/round.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
(set-enforce-redundancy t)
 
4
 
 
5
(local (include-book "../support/top"))
 
6
 
 
7
(include-book "reps")
 
8
 
 
9
(set-inhibit-warnings "theory") ; avoid warning in the next event
 
10
(local (in-theory nil))
 
11
;(set-inhibit-warnings) ; restore theory warnings (optional)
 
12
 
 
13
 
 
14
;;;**********************************************************************
 
15
;;;                            TRUNC
 
16
;;;**********************************************************************
 
17
 
 
18
(defund trunc (x n)
 
19
  (declare (xargs :guard (integerp n)))
 
20
  (* (sgn x) (fl (* (expt 2 (1- n)) (sig x))) (expt 2 (- (1+ (expo x)) n))))
 
21
 
 
22
(defthmd trunc-rewrite
 
23
    (implies (and (rationalp x)
 
24
                  (integerp n)
 
25
                  (> n 0))
 
26
             (equal (trunc x n)
 
27
                    (* (sgn x) 
 
28
                       (fl (* (expt 2 (- (1- n) (expo x))) (abs x))) 
 
29
                       (expt 2 (- (1+ (expo x)) n))))))
 
30
 
 
31
;replaces trunc-pos
 
32
;BOZO now a rewrite rule too; okay?
 
33
(defthm trunc-positive
 
34
   (implies (and (< 0 x)
 
35
                 (case-split (rationalp x))
 
36
                 (case-split (integerp n))
 
37
                 (case-split (< 0 n))
 
38
                 )
 
39
            (< 0 (trunc x n)))
 
40
   :rule-classes (:rewrite :linear))
 
41
 
 
42
;replaces trunc-neg
 
43
;BOZO now a rewrite rule too; okay?
 
44
(defthm trunc-negative
 
45
  (implies (and (< x 0)
 
46
                (case-split (rationalp x))
 
47
                (case-split (integerp n))
 
48
                (case-split (< 0 n)))
 
49
           (< (trunc x n) 0))
 
50
  :rule-classes (:rewrite :linear))
 
51
 
 
52
(defthm trunc-0
 
53
  (equal (trunc 0 n) 0))
 
54
 
 
55
(defthmd sgn-trunc
 
56
    (implies (and (< 0 n)
 
57
                  (rationalp x)
 
58
                  (integerp n)
 
59
                  )
 
60
             (equal (sgn (trunc x n))
 
61
                    (sgn x))))
 
62
 
 
63
(defthmd trunc-minus
 
64
  (equal (trunc (* -1 x) n)
 
65
         (* -1 (trunc x n))))
 
66
 
 
67
(defthmd abs-trunc
 
68
  (equal (abs (trunc x n))
 
69
         (* (fl (* (expt 2 (1- n)) (sig x))) (expt 2 (- (1+ (expo x)) n)))))
 
70
 
 
71
 
 
72
(defthm trunc-exactp-a
 
73
  (exactp (trunc x n) n))
 
74
 
 
75
(defthm trunc-exactp-b
 
76
    (implies (and (rationalp x)
 
77
                  (integerp n) 
 
78
                  (> n 0))
 
79
             (iff (= x (trunc x n))
 
80
                  (exactp x n)))
 
81
  :rule-classes ())
 
82
 
 
83
(defthmd trunc-exactp-c
 
84
    (implies (and (exactp a n)
 
85
                  (<= a x)
 
86
                  (rationalp x)
 
87
                  (integerp n)
 
88
                  (rationalp a)
 
89
                  )
 
90
             (<= a (trunc x n))))
 
91
 
 
92
;we called int-trunc
 
93
(defthmd trunc-integer-type-prescription
 
94
  (implies (and (>= (expo x) n)
 
95
                (case-split (integerp n))
 
96
                )
 
97
           (integerp (trunc x n)))
 
98
  :rule-classes :type-prescription)
 
99
 
 
100
(defthmd trunc-upper-bound
 
101
    (implies (and (rationalp x)
 
102
                  (integerp n))
 
103
             (<= (abs (trunc x n)) (abs x)))
 
104
  :rule-classes :linear)
 
105
 
 
106
(defthmd trunc-upper-pos
 
107
    (implies (and (<= 0 x)
 
108
                  (rationalp x)
 
109
                  (integerp n))
 
110
             (<= (trunc x n) x))
 
111
  :rule-classes :linear)
 
112
 
 
113
(defthmd trunc-lower-1
 
114
    (implies (and (rationalp x)
 
115
                  (integerp n))
 
116
             (> (abs (trunc x n)) (- (abs x) (expt 2 (- (1+ (expo x)) n)))))
 
117
  :rule-classes :linear)
 
118
 
 
119
(defthmd trunc-lower-pos
 
120
    (implies (and (rationalp x)
 
121
                  (> x 0)
 
122
                  (integerp n)
 
123
                  (> n 0))
 
124
             (> (trunc x n) (* x (- 1 (expt 2 (- 1 n))))))
 
125
  :rule-classes :linear)
 
126
 
 
127
(defthmd trunc-lower-3
 
128
    (implies (and (rationalp x)
 
129
                  (integerp n)
 
130
                  (> n 0))
 
131
             (>= (abs (trunc x n)) (* (abs x) (- 1 (expt 2 (- 1 n))))))
 
132
  :rule-classes :linear)
 
133
 
 
134
(defthmd trunc-lower-4
 
135
    (implies (and (rationalp x)
 
136
                  (integerp n)
 
137
                  (> n 0))
 
138
             (>= (trunc x n) (- x (* (abs x) (expt 2 (- 1 n))))))
 
139
  :rule-classes :linear)
 
140
 
 
141
(defthm trunc-diff
 
142
    (implies (and (rationalp x)
 
143
                  (integerp n)
 
144
                  (> n 0))
 
145
             (< (abs (- x (trunc x n))) (expt 2 (- (1+ (expo x)) n))))
 
146
  :rule-classes ())
 
147
 
 
148
(defthm trunc-diff-pos
 
149
    (implies (and (rationalp x)
 
150
                  (>= x 0)
 
151
                  (integerp n)
 
152
                  (> n 0))
 
153
             (< (- x (trunc x n)) (expt 2 (- (1+ (expo x)) n))))
 
154
  :rule-classes ())
 
155
 
 
156
(defthm trunc-diff-expo
 
157
    (implies (and (rationalp x)
 
158
                  (not (exactp x n))
 
159
                  (integerp n)
 
160
                  (> n 0))
 
161
             (<= (expo (- x (trunc x n))) (- (expo x) n)))
 
162
  :rule-classes ())
 
163
 
 
164
(defthmd trunc-monotone
 
165
  (implies (and (<= x y)
 
166
                (rationalp x)
 
167
                (rationalp y)
 
168
                (integerp n)
 
169
                )
 
170
           (<= (trunc x n) (trunc y n)))
 
171
  :rule-classes :linear)
 
172
 
 
173
(defthmd trunc-shift
 
174
  (implies (integerp n)
 
175
           (equal (trunc (* x (expt 2 k)) n)
 
176
                  (* (trunc x n) (expt 2 k)))))
 
177
 
 
178
(defthm expo-trunc
 
179
    (implies (and (< 0 n)
 
180
                  (rationalp x)
 
181
                  (integerp n)
 
182
                  )
 
183
             (equal (expo (trunc x n))
 
184
                    (expo x))))
 
185
 
 
186
(defthmd trunc-trunc
 
187
    (implies (and (>= n m)
 
188
                  (integerp n)
 
189
                  (integerp m)
 
190
                  )
 
191
             (equal (trunc (trunc x n) m)
 
192
                    (trunc x m))))
 
193
 
 
194
(defthm plus-trunc
 
195
    (implies (and (rationalp x)
 
196
                  (>= x 0)
 
197
                  (rationalp y)
 
198
                  (>= y 0)
 
199
                  (integerp k)
 
200
                  (exactp x (+ k (- (expo x) (expo y)))))
 
201
             (= (+ x (trunc y k))
 
202
                (trunc (+ x y) (+ k (- (expo (+ x y)) (expo y))))))
 
203
  :rule-classes ())
 
204
 
 
205
(defthm plus-trunc-alt
 
206
  (implies (and (exactp x (+ j (expo x) (- (expo (+ x y)))))
 
207
                (rationalp x)
 
208
                (>= x 0)
 
209
                (rationalp y)
 
210
                (>= y 0)
 
211
                (integerp j))
 
212
           (= (trunc (+ x y) j)
 
213
              (+ x
 
214
                 (trunc y (+ j (- (expo (+ x y))) (expo y))))))
 
215
  :rule-classes ())
 
216
 
 
217
(defthmd plus-trunc-corollary
 
218
  (implies (and (< y (expt 2 (- (1+ (expo x)) n)))
 
219
                (exactp x n)
 
220
                (rationalp x)
 
221
                (> x 0)
 
222
                (rationalp y)
 
223
                (>= y 0)
 
224
                (integerp n))
 
225
           (= (trunc (+ x y) n) x)))
 
226
 
 
227
(defthm trunc-plus
 
228
    (implies (and (rationalp y)
 
229
                  (> y 0)
 
230
                  (integerp e)
 
231
                  (< y (expt 2 e))
 
232
                  (integerp m)
 
233
                  (> m 0)
 
234
                  (integerp k)
 
235
                  (> k 0)
 
236
                  (<= m (1+ k)))
 
237
             (= (trunc (+ (expt 2 e) (trunc y k)) m)
 
238
                (trunc (+ (expt 2 e) y) m)))
 
239
  :rule-classes ())
 
240
 
 
241
(defthm trunc-n+k
 
242
    (implies (and (rationalp x)
 
243
                  (> x 0)
 
244
                  (integerp k)
 
245
                  (> k 0)
 
246
                  (integerp n)
 
247
                  (>= n k)
 
248
                  ;;this isn't really needed, but it won't hurt me.
 
249
                  (not (exactp x n))          
 
250
                  (= e (- (1+ (expo x)) n))
 
251
                  (= z (trunc (- x (trunc x n)) n)))
 
252
             (= (- (trunc x (+ n k)) (trunc x n))
 
253
                (* (1- (sig (trunc (+ (expt 2 e) z) (1+ k))))
 
254
                   (expt 2 e))))
 
255
  :rule-classes ())
 
256
 
 
257
 
 
258
(defthm bits-trunc
 
259
  (implies (and (= n (1+ (expo x)))
 
260
                (>= x 0)
 
261
                (integerp k)
 
262
                (> k 0)
 
263
                )
 
264
           (= (trunc x k)
 
265
              (* (expt 2 (- n k))
 
266
                 (bits x (1- n) (- n k)))))
 
267
  :rule-classes ())
 
268
 
 
269
(defthm trunc-land
 
270
    (implies (and (>= x (expt 2 (1- n)))
 
271
                  (< x (expt 2 n))
 
272
                  (integerp x) (> x 0)
 
273
                  (integerp m) (>= m n)
 
274
                  (integerp n) (> n k)
 
275
                  (integerp k) (> k 0)
 
276
                  )
 
277
             (= (trunc x k)
 
278
                (land x (- (expt 2 m) (expt 2 (- n k))) n)))
 
279
  :rule-classes ())
 
280
 
 
281
 
 
282
(defthm trunc-away-a
 
283
    (implies (and (integerp n) (> n 0)
 
284
                  (rationalp x) (> x 0)
 
285
                  (exactp x (1+ n))
 
286
                  (not (exactp x n)))
 
287
             (= (- x (expt 2 (- (expo x) n)))
 
288
                (trunc x n)))
 
289
  :rule-classes ())
 
290
 
 
291
(defthmd trunc-split
 
292
  (implies (and (= n (1+ (expo x)))
 
293
                (>= x 0)
 
294
                (integerp m)
 
295
                (> m k)
 
296
                (integerp k)
 
297
                (> k 0))
 
298
           (equal (trunc x m)
 
299
                  (+ (trunc x k)
 
300
                     (* (expt 2 (- n m))
 
301
                        (bits x (1- (- n k)) (- n m)))))))
 
302
 
 
303
;;;**********************************************************************
 
304
;;;                            AWAY
 
305
;;;**********************************************************************
 
306
 
 
307
(defund away (x n)
 
308
  (* (sgn x) (cg (* (expt 2 (1- n)) (sig x))) (expt 2 (- (1+ (expo x)) n))))
 
309
 
 
310
(defthmd away-rewrite
 
311
    (implies (and (rationalp x)
 
312
                  (integerp n)
 
313
                  (> n 0))
 
314
             (equal (away x n)
 
315
                    (* (sgn x) 
 
316
                       (cg (* (expt 2 (- (1- n) (expo x))) (abs x))) 
 
317
                       (expt 2 (- (1+ (expo x)) n))))))
 
318
 
 
319
;replaces away-pos
 
320
;BOZO wasn't a rewrite rule..
 
321
(defthm away-positive
 
322
  (implies (and (< 0 x)
 
323
                (case-split (rationalp x))
 
324
                )
 
325
           (< 0 (away x n)))
 
326
  :rule-classes (:rewrite :linear))
 
327
 
 
328
;replaces away-neg
 
329
;BOZO wasn't a rewrite rule..
 
330
(defthm away-negative
 
331
    (implies (and (< x 0)
 
332
                  (case-split (rationalp x))
 
333
                  )
 
334
             (< (away x n) 0))
 
335
    :rule-classes (:rewrite :linear))
 
336
 
 
337
(defthm away-0
 
338
  (equal (away 0 n) 0))
 
339
 
 
340
(defthmd sgn-away
 
341
  (equal (sgn (away x n))
 
342
         (sgn x)))
 
343
 
 
344
(defthmd away-minus
 
345
  (= (away (* -1 x) n) (* -1 (away x n))))
 
346
 
 
347
(defthmd abs-away
 
348
    (implies (and (rationalp x)
 
349
                  (integerp n))
 
350
             (equal (abs (away x n)) 
 
351
                    (* (cg (* (expt 2 (1- n)) (sig x))) (expt 2 (- (1+ (expo x)) n))))))
 
352
 
 
353
 
 
354
 
 
355
(defthm away-exactp-a
 
356
    (implies (case-split (< 0 n))
 
357
             (exactp (away x n) n)))
 
358
 
 
359
(defthm away-exactp-b
 
360
    (implies (and (rationalp x)
 
361
                  (integerp n) 
 
362
                  (> n 0))
 
363
             (iff (= x (away x n))
 
364
                  (exactp x n)))
 
365
  :rule-classes ())
 
366
 
 
367
 
 
368
(defthmd away-exactp-c
 
369
    (implies (and (exactp a n)
 
370
                  (>= a x)
 
371
                  (rationalp x)
 
372
                  (integerp n)
 
373
                  (> n 0)
 
374
                  (rationalp a)
 
375
                  )
 
376
             (>= a (away x n))))
 
377
 
 
378
(defthmd away-lower-bound
 
379
    (implies (and (case-split (rationalp x))
 
380
                  (case-split (integerp n)))
 
381
             (>= (abs (away x n)) (abs x)))
 
382
  :rule-classes :linear)
 
383
 
 
384
(defthmd away-lower-pos
 
385
    (implies (and (>= x 0)
 
386
                  (case-split (rationalp x))
 
387
                  (case-split (integerp n)))
 
388
             (>= (away x n) x))
 
389
  :rule-classes :linear)
 
390
 
 
391
;; ;; (defthmd expo-away-lower-bound
 
392
;; ;;     (implies (and (rationalp x)
 
393
;; ;;             (integerp n)
 
394
;; ;;             (> n 0))
 
395
;; ;;        (>= (expo (away x n)) (expo x)))
 
396
;; ;;   :rule-classes :linear)
 
397
 
 
398
 
 
399
(defthmd expo-away-lower-bound
 
400
    (implies (and (rationalp x)
 
401
                  (natp n))
 
402
             (>= (expo (away x n)) (expo x)))
 
403
  :rule-classes :linear)
 
404
 
 
405
 
 
406
(defthmd away-upper-1
 
407
    (implies (and (rationalp x)
 
408
                  (integerp n)
 
409
                  (> n 0))
 
410
             (< (abs (away x n)) (+ (abs x) (expt 2 (- (1+ (expo x)) n)))))
 
411
  :rule-classes :linear)
 
412
 
 
413
(defthmd away-upper-2
 
414
    (implies (and (rationalp x)
 
415
                  (not (= x 0))
 
416
                  (integerp n)
 
417
                  (> n 0))
 
418
             (< (abs (away x n)) (* (abs x) (+ 1 (expt 2 (- 1 n))))))
 
419
  :rule-classes :linear)
 
420
 
 
421
(defthmd away-upper-3
 
422
    (implies (and (rationalp x)
 
423
                  (integerp n)
 
424
                  (> n 0))
 
425
             (<= (abs (away x n)) (* (abs x) (+ 1 (expt 2 (- 1 n))))))
 
426
  :rule-classes :linear)
 
427
 
 
428
(defthmd away-diff
 
429
    (implies (and (rationalp x)
 
430
                  (integerp n)
 
431
                  (> n 0))
 
432
             (< (abs (- (away x n) x)) (expt 2 (- (1+ (expo x)) n))))
 
433
  :rule-classes :linear)
 
434
 
 
435
(defthmd away-diff-pos
 
436
    (implies (and (rationalp x)
 
437
                  (>= x 0)
 
438
                  (integerp n)
 
439
                  (> n 0))
 
440
             (< (- (away x n) x) (expt 2 (- (1+ (expo x)) n))))
 
441
  :rule-classes :linear)
 
442
 
 
443
(defthmd away-diff-expo
 
444
    (implies (and (rationalp x)
 
445
                  (not (exactp x n))
 
446
                  (integerp n)
 
447
                  (> n 0))
 
448
             (<= (expo (- (away x n) x)) (- (expo x) n)))
 
449
  :rule-classes :linear)
 
450
 
 
451
(defthm away-exactp-d
 
452
    (implies (and (rationalp x)
 
453
                  (not (= x 0))
 
454
                  (integerp n)
 
455
                  (> n 0))
 
456
             (<= (abs (away x n)) (expt 2 (1+ (expo x)))))
 
457
  :rule-classes ())
 
458
 
 
459
 
 
460
(defthm expo-away
 
461
    (implies (and (rationalp x)
 
462
                  (natp n)
 
463
                  (not (= (abs (away x n)) (expt 2 (1+ (expo x))))))
 
464
             (equal (expo (away x n))
 
465
                    (expo x))))
 
466
 
 
467
 
 
468
;; (defthm expo-away
 
469
;;     (implies (and (rationalp x)
 
470
;;                (not (= x 0))
 
471
;;                (integerp n)
 
472
;;                (> n 0)
 
473
;;                (not (= (abs (away x n)) (expt 2 (1+ (expo x))))))
 
474
;;           (equal (expo (away x n))
 
475
;;                    (expo x)))
 
476
;;   :rule-classes ())
 
477
 
 
478
 
 
479
(defthmd away-monotone
 
480
    (implies (and (rationalp x)
 
481
                  (rationalp y)
 
482
                  (integerp n)
 
483
                  (<= x y))
 
484
             (<= (away x n) (away y n)))
 
485
  :rule-classes :linear)
 
486
 
 
487
(defthmd away-shift
 
488
    (implies (integerp n)
 
489
             (= (away (* x (expt 2 k)) n)
 
490
                (* (away x n) (expt 2 k)))))
 
491
 
 
492
(defthmd away-away
 
493
    (implies (and (rationalp x)
 
494
                  (>= x 0)
 
495
                  (integerp n)
 
496
                  (integerp m)
 
497
                  (> m 0)
 
498
                  (>= n m))
 
499
             (equal (away (away x n) m)
 
500
                    (away x m))))
 
501
 
 
502
(defthm away-imp
 
503
    (implies (and (rationalp x)
 
504
                  (> x 0)
 
505
                  (integerp n)
 
506
                  (> n 0)
 
507
                  (integerp m)
 
508
                  (>= m n)
 
509
                  (exactp x m))
 
510
             (= (away x n)
 
511
                (trunc (+ x
 
512
                          (expt 2 (- (1+ (expo x)) n))
 
513
                          (- (expt 2 (- (1+ (expo x)) m))))
 
514
                       n)))
 
515
  :rule-classes ())
 
516
 
 
517
(defthm plus-away
 
518
  (implies (and (exactp x (+ k (- (expo x) (expo y))))
 
519
                (rationalp x)
 
520
                (>= x 0)
 
521
                (rationalp y)
 
522
                (>= y 0)
 
523
                (integerp k))
 
524
           (= (+ x (away y k))
 
525
              (away (+ x y)
 
526
                    (+ k (- (expo (+ x y)) (expo y))))))
 
527
  :rule-classes ())
 
528
 
 
529
(defthm plus-away-alt
 
530
  (implies (and (exactp x (+ j (expo x) (- (expo (+ x y)))))
 
531
                (rationalp x)
 
532
                (>= x 0)
 
533
                (rationalp y)
 
534
                (>= y 0)
 
535
                (integerp j))
 
536
           (= (away (+ x y) j)
 
537
              (+ x
 
538
                 (away y (+ j (- (expo (+ x y))) (expo y))))))
 
539
  :rule-classes ())
 
540
 
 
541
(defthmd plus-away-corollary
 
542
  (implies (and (< y (expt 2 (- (1+ (expo x)) n)))
 
543
                (rationalp x)
 
544
                (> x 0)
 
545
                (rationalp y)
 
546
                (> y 0)
 
547
                (integerp n)
 
548
                (exactp x n))
 
549
           (= (away (+ x y) n)
 
550
              (fp+ x n))))
 
551
 
 
552
(defthm trunc-away-b
 
553
    (implies (and (integerp n) (> n 0)
 
554
                  (rationalp x) (> x 0)
 
555
                  (exactp x (1+ n))
 
556
                  (not (exactp x n)))
 
557
             (= (away x n)
 
558
                (+ x (expt 2 (- (expo x) n)))))
 
559
  :rule-classes ())
 
560
 
 
561
(defthm trunc-away
 
562
    (implies (and (rationalp x) (> x 0)
 
563
                  (integerp n) (> n 0)
 
564
                  (not (exactp x n)))
 
565
             (= (away x n)
 
566
                (+ (trunc x n)
 
567
                   (expt 2 (+ (expo x) 1 (- n))))))             
 
568
  :rule-classes ())
 
569
 
 
570
;bad name?
 
571
(defthm minus-trunc-4
 
572
    (implies (and (rationalp x)
 
573
                  (> x 0)
 
574
                  (rationalp y)
 
575
                  (> y 0)
 
576
                  (< y x)
 
577
                  (integerp k)
 
578
                  (> k 0)
 
579
                  (> (+ k (- (expo (- x y)) (expo y))) 0)
 
580
                  (= n (+ k (- (expo x) (expo y))))
 
581
                  (exactp x n))
 
582
             (equal (- x (trunc y k))
 
583
                    (away (- x y) (+ k (- (expo (- x y)) (expo y))))))
 
584
  :rule-classes ())
 
585
 
 
586
;BOZO move to away section?
 
587
(defthm minus-trunc-5
 
588
    (implies (and (rationalp x)
 
589
                  (> x 0)
 
590
                  (rationalp y)
 
591
                  (> y 0)
 
592
                  (< x y)
 
593
                  (integerp k)
 
594
                  (> k 0)
 
595
                  (> (+ k (- (expo (- x y)) (expo y))) 0)
 
596
                  (= n (+ k (- (expo x) (expo y))))
 
597
                  (exactp x n))
 
598
             (equal (- x (trunc y k))
 
599
                    (- (trunc (- y x) (+ k (- (expo (- x y)) (expo y)))))))
 
600
  :rule-classes ())
 
601
 
 
602
 
 
603
;;;**********************************************************************
 
604
;;;                            NEAR
 
605
;;;**********************************************************************
 
606
 
 
607
(defun re (x)
 
608
  (- x (fl x)))
 
609
 
 
610
(defund near (x n)
 
611
  (let ((z (fl (* (expt 2 (1- n)) (sig x))))
 
612
        (f (re (* (expt 2 (1- n)) (sig x)))))
 
613
    (if (< f 1/2)
 
614
        (trunc x n)
 
615
      (if (> f 1/2)
 
616
          (away x n)
 
617
        (if (evenp z)
 
618
            (trunc x n)
 
619
          (away x n))))))
 
620
 
 
621
 
 
622
(defthm near1-a
 
623
  (implies (and (< (abs (- x (trunc x n)))
 
624
                   (abs (- (away x n) x)))
 
625
                (rationalp x)
 
626
                (integerp n))
 
627
           (equal (near x n)
 
628
                  (trunc x n)))
 
629
  :rule-classes ())
 
630
 
 
631
 
 
632
(defthm near1-b
 
633
  (implies (and (> (abs (- x (trunc x n))) (abs (- (away x n) x)))
 
634
                (rationalp x)
 
635
                (integerp n))
 
636
           (equal (near x n)
 
637
                  (away x n)))
 
638
  :rule-classes ())
 
639
 
 
640
(defthm near-choice
 
641
    (or (= (near x n) (trunc x n))
 
642
        (= (near x n) (away x n)))
 
643
  :rule-classes ())
 
644
 
 
645
(defthm near-pos
 
646
    (implies (and (< 0 x)
 
647
                  (< 0 n)
 
648
                  (rationalp x)
 
649
                  (integerp n))
 
650
             (< 0 (near x n)))
 
651
  :rule-classes (:TYPE-PRESCRIPTION :LINEAR))
 
652
 
 
653
(defthmd near-neg
 
654
  (implies (and (< x 0)
 
655
                (< 0 n)
 
656
                (rationalp x)
 
657
                (integerp n)
 
658
                )
 
659
           (< (near x n) 0))
 
660
  :rule-classes (:TYPE-PRESCRIPTION :LINEAR))
 
661
 
 
662
(defthm near-0
 
663
  (equal (near 0 n) 
 
664
         0))
 
665
 
 
666
(defthmd sgn-near-2
 
667
    (implies (and (rationalp x)
 
668
                  (integerp n)
 
669
                  (> n 0))
 
670
             (equal (sgn (near x n))
 
671
                    (sgn x))))
 
672
 
 
673
(defthmd near-minus
 
674
  (equal (near (* -1 x) n)
 
675
         (* -1 (near x n))))
 
676
 
 
677
(defthm near-exactp-b
 
678
    (implies (and (rationalp x)
 
679
                  (integerp n) 
 
680
                  (> n 0))
 
681
             (iff (= x (near x n))
 
682
                  (exactp x n)))
 
683
  :rule-classes ())
 
684
 
 
685
(defthm near-exactp-a
 
686
    (implies (< 0 n)
 
687
             (exactp (near x n) n)))
 
688
 
 
689
(defthmd near-exactp-c
 
690
    (implies (and (exactp a n)
 
691
                  (>= a x)
 
692
                  (rationalp x)
 
693
                  ;; (> x 0)
 
694
                  (integerp n)
 
695
                  (> n 0)
 
696
                  (rationalp a)
 
697
                  )
 
698
             (>= a (near x n))))
 
699
 
 
700
(defthmd near-exactp-d
 
701
    (implies (and (rationalp x)
 
702
                  ;;(> x 0)
 
703
                  (integerp n)
 
704
                  (> n 0)
 
705
                  (rationalp a)
 
706
                  (exactp a n)
 
707
                  (<= a x))
 
708
             (<= a (near x n))))
 
709
 
 
710
(defthm near<=away
 
711
    (implies (and (rationalp x)
 
712
                  (> x 0)
 
713
                  (integerp n)
 
714
                  (> n 0))
 
715
             (<= (near x n) (away x n)))
 
716
  :rule-classes ())
 
717
 
 
718
(defthm near>=trunc
 
719
    (implies (and (rationalp x)
 
720
                  (> x 0)
 
721
                  (integerp n)
 
722
                  (> n 0))
 
723
             (>= (near x n) (trunc x n)))
 
724
  :rule-classes ())
 
725
 
 
726
;was called monotone-near
 
727
(defthm near-monotone
 
728
    (implies (and (<= x y)
 
729
                  (rationalp x)
 
730
                  (rationalp y)
 
731
                  ;; (< 0 x)
 
732
                  (integerp n)
 
733
                  (> n 0))
 
734
             (<= (near x n) (near y n))))
 
735
 
 
736
(defthmd near-shift
 
737
    (implies (and (rationalp x)
 
738
                  (integerp n)
 
739
                  (integerp k))
 
740
             (= (near (* x (expt 2 k)) n)
 
741
                (* (near x n) (expt 2 k)))))
 
742
 
 
743
(defthm near2
 
744
  (implies (and (exactp y n)
 
745
                (rationalp x)
 
746
                (rationalp y)
 
747
                (integerp n)
 
748
                (> n 0))
 
749
           (>= (abs (- x y)) (abs (- x (near x n)))))
 
750
  :rule-classes ())
 
751
 
 
752
(defund near-witness (x y n)
 
753
  (if (= (expo x) (expo y))
 
754
      (/ (+ (near x n) (near y n)) 2)
 
755
    (expt 2 (expo y))))
 
756
 
 
757
(defthm near-near-lemma
 
758
    (implies (and (rationalp x)
 
759
                  (rationalp y)
 
760
                  (< 0 x)
 
761
                  (< x y)
 
762
                  (integerp n)
 
763
                  (> n 0)
 
764
                  (not (= (near x n) (near y n))))
 
765
             (and (<= x (near-witness x y n))
 
766
                  (<= (near-witness x y n) y)
 
767
                  (exactp (near-witness x y n) (1+ n))))
 
768
  :rule-classes ())
 
769
 
 
770
(defthm near-near
 
771
    (implies (and (rationalp x)
 
772
                  (rationalp y)
 
773
                  (rationalp a)
 
774
                  (integerp n)
 
775
                  (integerp k)
 
776
                  (> k 0)
 
777
                  (>= n k)                
 
778
                  (< 0 a)
 
779
                  (< a x)
 
780
                  (< 0 y)
 
781
                  (< y (fp+ a (1+ n)))
 
782
                  (exactp a (1+ n)))
 
783
             (<= (near y k) (near x k)))
 
784
  :rule-classes ())
 
785
 
 
786
(defthm near-est
 
787
    (implies (and (integerp n) (> n 0)
 
788
                  (rationalp x) )
 
789
                  ;;(> x 0))
 
790
             (<= (abs (- x (near x n)))
 
791
                 (expt 2 (- (expo x) n))))
 
792
  :rule-classes ())
 
793
 
 
794
(defthm near-a-a
 
795
    (implies (and (rationalp x) (> x 0)
 
796
                  (rationalp a) (> a 0)
 
797
                  (integerp n) (> n 0)
 
798
                  (exactp a n)
 
799
                  (> x (+ a (expt 2 (- (expo a) n)))))
 
800
             (>= (near x n) (+ a (expt 2 (- (1+ (expo a)) n)))))
 
801
  :rule-classes ())
 
802
 
 
803
(defthm near-a-b
 
804
    (implies (and (rationalp x) (> x 0)
 
805
                  (rationalp a) (> a 0)
 
806
                  (integerp n) (> n 0)
 
807
                  (exactp a n)
 
808
                  (< x (+ a (expt 2 (- (expo a) n)))))
 
809
             (<= (near x n) a))
 
810
  :rule-classes ())
 
811
 
 
812
(defthm near-a-c
 
813
    (implies (and (rationalp x) (> x 0)
 
814
                  (rationalp a) (> a 0)
 
815
                  (integerp n) (> n 0)
 
816
                  (exactp a n)
 
817
                  (< x a)
 
818
                  (> x (- a (expt 2 (- (expo x) n)))))
 
819
             (>= (near x n) a))
 
820
  :rule-classes ())
 
821
 
 
822
(defthm near-exact
 
823
    (implies (and (rationalp x) ;; (> x 0)
 
824
                  (integerp n) (> n 1)
 
825
                  (exactp x (1+ n))
 
826
                  (not (exactp x n)))
 
827
             (exactp (near x n) (1- n)))
 
828
  :rule-classes ())
 
829
 
 
830
(defthm near-power-a
 
831
    (implies (and (rationalp x) (> x 0)
 
832
                  (integerp n) (> n 1)
 
833
                  (>= (+ x (expt 2 (- (expo x) n)))
 
834
                      (expt 2 (1+ (expo x)))))
 
835
             (= (near x n)
 
836
                (expt 2 (1+ (expo x)))))
 
837
  :rule-classes ())
 
838
 
 
839
(defthm near-power-b
 
840
    (implies (and (rationalp x) (> x 0)
 
841
                  (integerp n) (> n 1)
 
842
                  (>= (+ x (expt 2 (- (expo x) n)))
 
843
                      (expt 2 (1+ (expo x)))))
 
844
             (= (trunc (+ x (expt 2 (- (expo x) n))) n)
 
845
                (expt 2 (1+ (expo x)))))
 
846
  :rule-classes ())
 
847
 
 
848
(defthm near-trunc
 
849
    (implies (and (rationalp x) (> x 0)
 
850
                  (integerp n) (> n 1))
 
851
             (= (near x n)
 
852
                (if (and (exactp x (1+ n)) (not (exactp x n)))
 
853
                    (trunc (+ x (expt 2 (- (expo x) n))) (1- n))
 
854
                  (trunc (+ x (expt 2 (- (expo x) n))) n))))
 
855
  :rule-classes ())
 
856
 
 
857
 
 
858
;;;**********************************************************************
 
859
;;;                            NEAR+
 
860
;;;**********************************************************************
 
861
 
 
862
(defund near+ (x n)
 
863
  (if (< (re (* (expt 2 (1- n)) (sig x)))
 
864
         1/2)
 
865
      (trunc x n)
 
866
    (away x n)))
 
867
 
 
868
(defthm near+trunc
 
869
    (implies (and (rationalp x)
 
870
                  (> x 0)
 
871
                  (integerp n)
 
872
                  (> n 0))
 
873
             (= (near+ x n)
 
874
                (trunc (+ x (expt 2 (- (expo x) n))) n)))               
 
875
  :rule-classes ())
 
876
 
 
877
(defthm sgn-near+-2
 
878
    (implies (and (rationalp x)
 
879
                  (integerp n)
 
880
                  (> n 0))
 
881
             (= (near+ x n)
 
882
                (* (sgn x) (near+ (abs x) n))))
 
883
  :rule-classes ())
 
884
 
 
885
(defthm sgn-near+
 
886
    (implies (and (rationalp x)
 
887
                  (integerp n)
 
888
                  (> n 0))
 
889
             (equal (sgn (near+ x n))
 
890
                    (sgn x))))
 
891
 
 
892
(defthm near+-pos
 
893
  (implies (and (rationalp x)
 
894
                (> x 0)
 
895
                (integerp n)
 
896
                (> n 0))
 
897
           (> (near+ x n) 0))
 
898
  :rule-classes :linear)
 
899
 
 
900
;BOZO make :t-p?
 
901
(defthm near+-neg
 
902
    (implies (and (< x 0)
 
903
                  (rationalp x)
 
904
                  (integerp n)
 
905
                  (> n 0))
 
906
             (< (near+ x n) 0))
 
907
  :rule-classes :linear)
 
908
 
 
909
(defthm near+-0-0
 
910
  (implies (and (case-split (< 0 n))
 
911
                (case-split (rationalp x))
 
912
                (case-split (integerp n))
 
913
                )
 
914
           (equal (equal (near+ x n) 0)
 
915
                  (equal x 0)))
 
916
  :rule-classes ())
 
917
 
 
918
(defthm near+-0
 
919
  (equal (near+ 0 n) 0))
 
920
 
 
921
(defthmd near+-minus
 
922
  (= (near+ (* -1 x) n) (* -1 (near+ x n))))
 
923
 
 
924
(defthmd near+-shift
 
925
    (implies (and (rationalp x)
 
926
                  (integerp n)
 
927
                  (integerp k))
 
928
             (= (near+ (* x (expt 2 k)) n)
 
929
                (* (near+ x n) (expt 2 k)))))
 
930
 
 
931
 
 
932
(defthm near+-choice
 
933
    (or (= (near+ x n) (trunc x n))
 
934
        (= (near+ x n) (away x n)))
 
935
  :rule-classes ())
 
936
 
 
937
(defthm near+1-a
 
938
    (implies (and (rationalp x)
 
939
                  (integerp n)
 
940
                  (< (abs (- x (trunc x n))) (abs (- (away x n) x))))
 
941
             (= (near+ x n) (trunc x n)))
 
942
  :rule-classes ())
 
943
 
 
944
(defthm near+1-b
 
945
    (implies (and (rationalp x)
 
946
                  (integerp n)
 
947
                  (> (abs (- x (trunc x n))) (abs (- (away x n) x))))
 
948
             (= (near+ x n) (away x n)))
 
949
  :rule-classes ())
 
950
 
 
951
(defthm near+<=away
 
952
    (implies (and (rationalp x)
 
953
                  (> x 0)
 
954
                  (integerp n)
 
955
                  (> n 0))
 
956
             (<= (near+ x n) (away x n)))
 
957
  :rule-classes ())
 
958
 
 
959
(defthm near+>=trunc
 
960
    (implies (and (rationalp x)
 
961
                  (> x 0)
 
962
                  (integerp n)
 
963
                  (> n 0))
 
964
             (>= (near+ x n) (trunc x n)))
 
965
  :rule-classes ())
 
966
 
 
967
 
 
968
(defthm near+2
 
969
  (implies (and (exactp y n)
 
970
                (rationalp x)
 
971
                (rationalp y)
 
972
                (integerp n)
 
973
                (> n 0))
 
974
           (>= (abs (- x y)) (abs (- x (near+ x n)))))
 
975
  :rule-classes ())
 
976
 
 
977
 
 
978
(defthm near+-est
 
979
    (implies (and (integerp n) 
 
980
                  (> n 0)
 
981
                  (rationalp x))
 
982
             (<= (abs (- x (near+ x n)))
 
983
                 (expt 2 (- (expo x) n))))
 
984
    :rule-classes ())
 
985
 
 
986
 
 
987
;was called monotone-near+
 
988
 
 
989
;; (defthm near+-monotone
 
990
;;   (implies (and (<= x y)
 
991
;;                 (rationalp x)
 
992
;;                 (rationalp y)
 
993
;;                 (< 0 x)
 
994
;;                 (integerp n)
 
995
;;                 (> n 0))
 
996
;;            (<= (near+ x n) (near+ y n))))
 
997
 
 
998
(defthm near+-monotone
 
999
   (implies (and (<= x y)
 
1000
                (rationalp x)
 
1001
                (rationalp y)
 
1002
                ;(integerp n)
 
1003
                (natp n))
 
1004
           (<= (near+ x n) (near+ y n))))
 
1005
 
 
1006
 
 
1007
(defthm near+-power
 
1008
    (implies (and (rationalp x) (> x 0)
 
1009
                  (integerp n) (> n 1)
 
1010
                  (>= (+ x (expt 2 (- (expo x) n)))
 
1011
                      (expt 2 (1+ (expo x)))))
 
1012
             (= (near+ x n)
 
1013
                (expt 2 (1+ (expo x)))))
 
1014
  :rule-classes ())
 
1015
 
 
1016
(defthm near+-exactp-b
 
1017
    (implies (and (rationalp x)
 
1018
                  (integerp n) 
 
1019
                  (> n 0))
 
1020
             (iff (= x (near+ x n))
 
1021
                  (exactp x n)))
 
1022
  :rule-classes ())
 
1023
 
 
1024
(defthm near+-exactp-a
 
1025
    (implies (and (rationalp x)
 
1026
                  (integerp n)
 
1027
                  (> n 0))
 
1028
             (exactp (near+ x n) n)))
 
1029
 
 
1030
(defthm near+-exactp-c
 
1031
  (implies (and (rationalp x)
 
1032
                (integerp n)
 
1033
                (> n 0)
 
1034
                (rationalp a)
 
1035
                (exactp a n)
 
1036
                (>= a x))
 
1037
           (>= a (near+ x n))))
 
1038
 
 
1039
(defthm near+-exactp-d
 
1040
  (implies (and (rationalp x)
 
1041
                (integerp n)
 
1042
                (> n 0)
 
1043
                (rationalp a)
 
1044
                (exactp a n)
 
1045
                (<= a x))
 
1046
           (<= a (near+ x n))))
 
1047
 
 
1048
;; (defthm near+-exactp-c
 
1049
;;     (implies (and (rationalp x)
 
1050
;;                (> x 0)
 
1051
;;                (integerp n)
 
1052
;;                (> n 0)
 
1053
;;                (rationalp a)
 
1054
;;                (exactp a n)
 
1055
;;                (>= a x))
 
1056
;;           (>= a (near+ x n))))
 
1057
 
 
1058
;; (defthm near+-exactp-d
 
1059
;;     (implies (and (rationalp x)
 
1060
;;                (> x 0)
 
1061
;;                (integerp n)
 
1062
;;                (> n 0)
 
1063
;;                (rationalp a)
 
1064
;;                (exactp a n)
 
1065
;;                (<= a x))
 
1066
;;           (<= a (near+ x n))))
 
1067
 
 
1068
 
 
1069
;;;**********************************************************************
 
1070
;;;                           STICKY
 
1071
;;;**********************************************************************
 
1072
 
 
1073
(defund sticky (x n)
 
1074
  (cond ((exactp x (1- n)) x)
 
1075
        (t (+ (trunc x (1- n))
 
1076
              (* (sgn x) (expt 2 (1+ (- (expo x) n))))))))
 
1077
 
 
1078
(defthm sticky-1
 
1079
  (implies (rationalp x)
 
1080
           (equal (sticky x 1)
 
1081
                  (* (sgn x) (expt 2 (expo x))))))
 
1082
 
 
1083
(defthmd sticky-pos
 
1084
    (implies (and (< 0 x)
 
1085
                  (rationalp x) 
 
1086
                  (integerp n)
 
1087
                  (> n 0))
 
1088
             (> (sticky x n) 0))
 
1089
  :rule-classes :linear)
 
1090
 
 
1091
(defthm sticky-0
 
1092
  (equal (sticky 0 n) 0))
 
1093
 
 
1094
(defthmd sticky-minus
 
1095
  (equal (sticky (* -1 x) n) (* -1 (sticky x n))))
 
1096
 
 
1097
(defthm sticky-shift
 
1098
    (implies (and (rationalp x)
 
1099
                  (integerp n) (> n 0)
 
1100
                  (integerp k))
 
1101
             (= (sticky (* (expt 2 k) x) n)
 
1102
                (* (expt 2 k) (sticky x n))))           
 
1103
  :rule-classes ())
 
1104
 
 
1105
(defthm sticky-exactp
 
1106
    (implies (and (rationalp x) ;; (>= x 0)
 
1107
                  (integerp n) (> n 0))
 
1108
             (exactp (sticky x n) n))
 
1109
  :rule-classes ())
 
1110
 
 
1111
(defthm sticky-exactp-m
 
1112
    (implies (and (rationalp x)
 
1113
                  (integerp m)
 
1114
                  (integerp n) 
 
1115
                  (> n m)
 
1116
                  (> m 0))
 
1117
             (iff (exactp (sticky x n) m)
 
1118
                  (exactp x m)))
 
1119
  :rule-classes ())
 
1120
 
 
1121
(defthm expo-sticky
 
1122
    (implies (and (rationalp x) ;; (> x 0)
 
1123
                  (integerp n) (> n 0))
 
1124
             (= (expo (sticky x n))
 
1125
                (expo x)))
 
1126
  :rule-classes ())
 
1127
 
 
1128
(defthm trunc-sticky
 
1129
    (implies (and (rationalp x) ;; (> x 0)
 
1130
                  (integerp m) (> m 0)
 
1131
                  (integerp n) (> n m))
 
1132
             (= (trunc (sticky x n) m)
 
1133
                (trunc x m)))
 
1134
  :rule-classes ())
 
1135
 
 
1136
(defthm away-sticky
 
1137
    (implies (and (rationalp x) ;; (> x 0)
 
1138
                  (integerp m) (> m 0)
 
1139
                  (integerp n) (> n m))
 
1140
             (= (away (sticky x n) m)
 
1141
                (away x m)))
 
1142
  :rule-classes ())
 
1143
 
 
1144
(defthm away-sticky
 
1145
    (implies (and (rationalp x) ;; (> x 0)
 
1146
                  (integerp m) (> m 0)
 
1147
                  (integerp n) (> n m))
 
1148
             (= (away (sticky x n) m)
 
1149
                (away x m)))
 
1150
  :rule-classes ())
 
1151
 
 
1152
 
 
1153
(defthm near-sticky
 
1154
    (implies (and (rationalp x) ;; (> x 0)
 
1155
                  (integerp m) (> m 0)
 
1156
                  (integerp n) (> n (1+ m)))
 
1157
             (= (near (sticky x n) m)
 
1158
                (near x m)))
 
1159
  :rule-classes ())
 
1160
 
 
1161
 
 
1162
(defthm near+-sticky
 
1163
    (implies (and (rationalp x) 
 
1164
                  (integerp m) (> m 0)
 
1165
                  (integerp n) (> n (1+ m)))
 
1166
             (= (near+ (sticky x n) m)
 
1167
                (near+ x m)))
 
1168
  :rule-classes ())
 
1169
 
 
1170
 
 
1171
(defthm sticky-sticky
 
1172
    (implies (and (rationalp x)
 
1173
                  (integerp m)
 
1174
                  (> m 1)
 
1175
                  (integerp n)
 
1176
                  (>= n m))
 
1177
             (= (sticky (sticky x n) m)
 
1178
                (sticky x m)))
 
1179
  :rule-classes ())
 
1180
 
 
1181
 
 
1182
(defthm sticky-plus-original ;; Fri Oct 13 14:40:05 2006
 
1183
    (implies (and (rationalp x)
 
1184
                  (> x 0)
 
1185
                  (rationalp y)
 
1186
                  (> y 0)
 
1187
                  (integerp k)
 
1188
                  (= k1 (+ k (- (expo x) (expo y))))
 
1189
                  (= k2 (+ k (- (expo (+ x y)) (expo y))))
 
1190
                  (> k 1)
 
1191
                  (> k1 1)
 
1192
                  (> k2 1)
 
1193
                  (exactp x (1- k1)))
 
1194
             (= (+ x (sticky y k))
 
1195
                (sticky (+ x y) k2)))
 
1196
  :rule-classes ())
 
1197
 
 
1198
(defthm minus-sticky
 
1199
    (implies (and (rationalp x)
 
1200
                  (> x 0)
 
1201
                  (rationalp y)
 
1202
                  (> y 0)
 
1203
                  (integerp k)
 
1204
                  (= k1 (+ k (- (expo x) (expo y))))
 
1205
                  (= k2 (+ k (- (expo (- x y)) (expo y))))
 
1206
                  (> k 1)
 
1207
                  (> k1 1)
 
1208
                  (> k2 1)
 
1209
                  (exactp x (1- k1)))
 
1210
             (= (- x (sticky y k))
 
1211
                (sticky (- x y) k2)))
 
1212
  :rule-classes ())
 
1213
 
 
1214
(defthm sticky-lemma
 
1215
    (implies (and (rationalp x)
 
1216
                  (> x 0)
 
1217
                  (rationalp y)
 
1218
                  (integerp k)
 
1219
                  (= k1 (+ k (- (expo x) (expo y))))
 
1220
                  (= k2 (+ k (- (expo (+ x y)) (expo y))))
 
1221
                  (> k 1)
 
1222
                  (> k1 1)
 
1223
                  (> k2 1)
 
1224
                  (exactp x (1- k1)))
 
1225
             (= (+ x (sticky y k))
 
1226
                (sticky (+ x y) k2)))
 
1227
  :rule-classes ())
 
1228
 
 
1229
(defthmd sticky-monotone
 
1230
  (implies (and (<= x y)
 
1231
                (rationalp x)
 
1232
                (rationalp y)
 
1233
                (natp n))
 
1234
           (<= (sticky x n) (sticky y n)))
 
1235
  :rule-classes :linear)
 
1236
 
 
1237
;;;**********************************************************************
 
1238
;;;                              ODDR 
 
1239
;;;**********************************************************************
 
1240
 
 
1241
;was called "odd" but that name conflicted with another function we wanted (a recursive version of oddp)
 
1242
(defund oddr (x n)
 
1243
  (let ((z (fl (* (expt 2 (1- n)) (sig x)))))
 
1244
    (if (evenp z)
 
1245
        (* (sgn x) (1+ z) (expt 2 (- (1+ (expo x)) n)))
 
1246
      (* (sgn x) z (expt 2 (- (1+ (expo x)) n))))))
 
1247
 
 
1248
(defthm oddr-pos
 
1249
    (implies (and (< 0 x)
 
1250
                  (rationalp x)
 
1251
                  (integerp n)
 
1252
                  (> n 0))
 
1253
             (< 0 (oddr x n)))
 
1254
  :rule-classes ())
 
1255
 
 
1256
(defthm oddr>=trunc
 
1257
    (implies (and (rationalp x)
 
1258
                  (> x 0)
 
1259
                  (integerp n)
 
1260
                  (> n 0))
 
1261
             (>= (oddr x n) (trunc x n)))
 
1262
  :rule-classes ())
 
1263
 
 
1264
;keep disabled..
 
1265
(defthmd oddr-rewrite
 
1266
    (implies (and (< 0 x)
 
1267
                  (rationalp x)
 
1268
                  (integerp n)
 
1269
                  (< 0 n))
 
1270
             (equal (oddr x n)
 
1271
                    (let ((z (fl (* (expt 2 (- (1- n) (expo x))) x))))
 
1272
                      (if (evenp z)
 
1273
                          (* (1+ z) (expt 2 (- (1+ (expo x)) n)))
 
1274
                        (* z (expt 2 (- (1+ (expo x)) n))))))))
 
1275
 
 
1276
(defthm oddr-other
 
1277
    (implies (and (rationalp x)
 
1278
                  (> x 0)
 
1279
                  (integerp n) 
 
1280
                  (> n 1))
 
1281
             (= (oddr x n)
 
1282
                (+ (trunc x (1- n))
 
1283
                   (expt 2 (- (1+ (expo x)) n)))))
 
1284
  :rule-classes ())
 
1285
 
 
1286
(defthm expo-oddr
 
1287
    (implies (and (rationalp x)
 
1288
                  (integerp n)
 
1289
                  (> x 0)
 
1290
                  (> n 1))
 
1291
             (equal (expo (oddr x n)) (expo x))))
 
1292
 
 
1293
(defthm exactp-oddr
 
1294
    (implies (and (rationalp x)
 
1295
                  (integerp n)
 
1296
                  (> x 0)
 
1297
                  (> n 1))
 
1298
             (exactp (oddr x n) n))
 
1299
  :rule-classes ())
 
1300
 
 
1301
(defthm not-exactp-oddr
 
1302
    (implies (and (rationalp x)
 
1303
                  (integerp n)
 
1304
                  (> x 0)
 
1305
                  (> n 1))
 
1306
             (not (exactp (oddr x n) (1- n))))
 
1307
  :rule-classes ())
 
1308
 
 
1309
(defthm trunc-oddr
 
1310
    (implies (and (rationalp x)
 
1311
                  (> x 0)
 
1312
                  (integerp n)
 
1313
                  (integerp m)
 
1314
                  (> m 0)
 
1315
                  (> n m))
 
1316
             (= (trunc (oddr x n) m)
 
1317
                (trunc x m)))
 
1318
  :rule-classes ())
 
1319
 
 
1320
(defun kp (k x y)
 
1321
  (+ k (- (expo (+ x y)) (expo y))))
 
1322
 
 
1323
(defthm oddr-plus
 
1324
    (implies (and (rationalp x)
 
1325
                  (rationalp y)
 
1326
                  (integerp k)
 
1327
                  (> x 0)
 
1328
                  (> y 0)
 
1329
                  (> k 1)
 
1330
                  (> (+ (1- k) (- (expo x) (expo y))) 0)
 
1331
                  (exactp x (+ (1- k) (- (expo x) (expo y)))))
 
1332
             (= (+ x (oddr y k))
 
1333
                (oddr (+ x y) (kp k x y))))
 
1334
  :rule-classes ())
 
1335
 
 
1336
(defthm trunc-trunc-oddr
 
1337
    (implies (and (rationalp x)
 
1338
                  (rationalp y)
 
1339
                  (integerp m)
 
1340
                  (integerp k)
 
1341
                  (> x y)
 
1342
                  (> y 0)
 
1343
                  (> k 0)
 
1344
                  (>= (- m 2) k))
 
1345
             (>= (trunc x k) (trunc (oddr y m) k)))
 
1346
  :rule-classes ())
 
1347
 
 
1348
(defthm away-away-oddr
 
1349
    (implies (and (rationalp x)
 
1350
                  (rationalp y)
 
1351
                  (integerp m)
 
1352
                  (integerp k)
 
1353
                  (> x y)
 
1354
                  (> y 0)
 
1355
                  (> k 0)
 
1356
                  (>= (- m 2) k))
 
1357
             (>= (away x k) (away (oddr y m) k)))
 
1358
  :rule-classes ())
 
1359
 
 
1360
(defthm near-near-oddr
 
1361
    (implies (and (rationalp x)
 
1362
                  (rationalp y)
 
1363
                  (integerp m)
 
1364
                  (integerp k)
 
1365
                  (> x y)
 
1366
                  (> y 0)
 
1367
                  (> k 0)
 
1368
                  (>= (- m 2) k))
 
1369
             (>= (near x k) (near (oddr y m) k)))
 
1370
  :rule-classes ())
 
1371
 
 
1372
 
 
1373
;;;**********************************************************************
 
1374
;;;        IEEE Rounding (most theorems also apply to AWAY and NEAR+) 
 
1375
;;;**********************************************************************
 
1376
 
 
1377
(defun inf (x n)
 
1378
  (if (>= x 0)
 
1379
      (away x n)
 
1380
    (trunc x n)))
 
1381
 
 
1382
(defun minf (x n)
 
1383
  (if (>= x 0)
 
1384
      (trunc x n)
 
1385
    (away x n)))
 
1386
 
 
1387
(defund ieee-mode-p (mode)
 
1388
  (member mode '(trunc inf minf near)))
 
1389
 
 
1390
(defun common-rounding-mode-p (mode)
 
1391
  (or (IEEE-mode-p mode) (equal mode 'away) (equal mode 'near+)))
 
1392
 
 
1393
(defthmd ieee-mode-p-implies-common-rounding-mode-p
 
1394
  (implies (IEEE-mode-p mode)
 
1395
           (common-rounding-mode-p mode)))
 
1396
 
 
1397
(defund rnd (x mode n)
 
1398
  (case mode
 
1399
    (away (away x n))
 
1400
    (near+ (near+ x n))
 
1401
    (trunc (trunc x n))
 
1402
    (inf (inf x n))
 
1403
    (minf (minf x n))
 
1404
    (near (near x n))
 
1405
    (otherwise 0)))
 
1406
 
 
1407
(defthm rationalp-rnd
 
1408
  (rationalp (rnd x mode n))
 
1409
  :rule-classes (:type-prescription))
 
1410
 
 
1411
; Unlike the above, we leave the following two as rewrite rules because we may
 
1412
; want to use the rewriter to relieve their hypotheses.
 
1413
 
 
1414
(defthm rnd-non-pos
 
1415
    (implies (<= x 0)
 
1416
             (<= (rnd x mode n) 0))
 
1417
  :rule-classes (:rewrite :type-prescription :linear))
 
1418
 
 
1419
(defthm rnd-non-neg
 
1420
    (implies (<= 0 x)
 
1421
             (<= 0 (rnd x mode n)))
 
1422
  :rule-classes (:rewrite :type-prescription :linear))
 
1423
 
 
1424
(defthm rnd-pos
 
1425
  (implies (and (< 0 x)
 
1426
                (rationalp x)
 
1427
                (integerp n)
 
1428
                (> n 0)
 
1429
                (common-rounding-mode-p mode))
 
1430
           (> (rnd x mode n) 0))
 
1431
  :RULE-CLASSES (:TYPE-PRESCRIPTION))
 
1432
 
 
1433
(defthm rnd-neg
 
1434
    (implies (and (< x 0)
 
1435
                  (rationalp x)
 
1436
                  (integerp n)
 
1437
                  (> n 0)
 
1438
                  (common-rounding-mode-p mode))
 
1439
             (< (rnd x mode n) 0))
 
1440
  :RULE-CLASSES (:TYPE-PRESCRIPTION))
 
1441
 
 
1442
(defthm rnd-0
 
1443
  (equal (rnd 0 mode n)
 
1444
         0))
 
1445
 
 
1446
(defthmd sgn-rnd
 
1447
    (implies (and; (rationalp x)
 
1448
                  (common-rounding-mode-p mode)
 
1449
                  (integerp n)
 
1450
                  (> n 0))
 
1451
             (equal (sgn (rnd x mode n))
 
1452
                    (sgn x))))
 
1453
 
 
1454
(defund flip (m)
 
1455
  (case m
 
1456
    (inf 'minf)
 
1457
    (minf 'inf)
 
1458
    (t m)))
 
1459
 
 
1460
(defthm ieee-mode-p-flip
 
1461
    (implies (ieee-mode-p m)
 
1462
             (ieee-mode-p (flip m))))
 
1463
 
 
1464
(defthm common-rounding-mode-p-flip
 
1465
    (implies (common-rounding-mode-p m)
 
1466
             (common-rounding-mode-p (flip m))))
 
1467
 
 
1468
;a very similar rule was called rnd-flip
 
1469
;enable?
 
1470
(defthmd rnd-minus
 
1471
  (equal (rnd (* -1 x) mode n)
 
1472
         (* -1 (rnd x (flip mode) n))))
 
1473
 
 
1474
(defthm rnd-exactp-b
 
1475
  (implies (and (rationalp x)
 
1476
                (common-rounding-mode-p mode)
 
1477
                (integerp n) 
 
1478
                (> n 0))
 
1479
           (equal (equal x (rnd x mode n))
 
1480
                  (exactp x n))))
 
1481
 
 
1482
(defthm rnd-exactp-a
 
1483
    (implies (< 0 n)
 
1484
             (exactp (rnd x mode n) n)))
 
1485
 
 
1486
(defthmd rnd-exactp-c
 
1487
    (implies (and (rationalp x)
 
1488
                  ;(> x 0)
 
1489
                  (common-rounding-mode-p mode)
 
1490
                  (integerp n)
 
1491
                  (> n 0)
 
1492
                  (rationalp a)
 
1493
                  (exactp a n)
 
1494
                  (>= a x))
 
1495
             (>= a (rnd x mode n))))
 
1496
 
 
1497
(defthmd rnd-exactp-d
 
1498
    (implies (and (rationalp x)
 
1499
                  ;(> x 0)
 
1500
                  (common-rounding-mode-p mode)
 
1501
                  (integerp n)
 
1502
                  (> n 0)
 
1503
                  (rationalp a)
 
1504
                  (exactp a n)
 
1505
                  (<= a x))
 
1506
             (<= a (rnd x mode n))))
 
1507
 
 
1508
(defthm rnd<=away
 
1509
    (implies (and (rationalp x)
 
1510
                  (>= x 0)
 
1511
                  (common-rounding-mode-p mode)
 
1512
                  (natp n))
 
1513
             (<= (rnd x mode n) (away x n)))
 
1514
  :rule-classes ())
 
1515
 
 
1516
(defthm rnd>=trunc
 
1517
    (implies (and (rationalp x)
 
1518
                  (> x 0)
 
1519
                  (common-rounding-mode-p mode)
 
1520
                  (integerp n)
 
1521
                  (> n 0))
 
1522
             (>= (rnd x mode n) (trunc x n)))
 
1523
  :rule-classes ())
 
1524
 
 
1525
 
 
1526
(defthmd rnd-monotone
 
1527
    (implies (and (<= x y)
 
1528
                  (rationalp x)
 
1529
                  (rationalp y)
 
1530
                  (common-rounding-mode-p mode)
 
1531
                  (integerp n)
 
1532
                  (> n 0))
 
1533
             (<= (rnd x mode n) (rnd y mode n))))
 
1534
 
 
1535
(defthm exactp-rnd
 
1536
    (implies (and (rationalp x)
 
1537
                  (common-rounding-mode-p mode)
 
1538
                  (integerp n)
 
1539
                  (> n 0))
 
1540
             (exactp (rnd x mode n) n)))
 
1541
 
 
1542
(defthm rnd-shift
 
1543
    (implies (and (rationalp x)
 
1544
                  (integerp n)
 
1545
                  (common-rounding-mode-p mode)
 
1546
                  (integerp k))
 
1547
             (= (rnd (* x (expt 2 k)) mode n)
 
1548
                (* (rnd x mode n) (expt 2 k))))
 
1549
  :rule-classes ())
 
1550
 
 
1551
(defthm expo-rnd
 
1552
    (implies (and (rationalp x)
 
1553
                  ;; (not (= x 0))
 
1554
                  (integerp n)
 
1555
                  (> n 0)
 
1556
                  (common-rounding-mode-p mode)
 
1557
                  (not (= (abs (rnd x mode n))
 
1558
                          (expt 2 (1+ (expo x))))))
 
1559
             (= (expo (rnd x mode n))
 
1560
                (expo x)))
 
1561
  :rule-classes ())
 
1562
 
 
1563
(defthm expo-rnd-bnd
 
1564
    (implies (and (rationalp x)
 
1565
                  (integerp n)
 
1566
                  (> n 0)
 
1567
                  (common-rounding-mode-p mode))
 
1568
             (>= (expo (rnd x mode n))
 
1569
                 (expo x)))
 
1570
  :rule-classes ())
 
1571
 
 
1572
(defun rnd-const (e mode n)
 
1573
  (case mode
 
1574
    ((near near+) (expt 2 (- e n)))
 
1575
    ((inf away) (1- (expt 2 (1+ (- e n)))))
 
1576
    (otherwise 0)))
 
1577
 
 
1578
(defthm rnd-const-thm
 
1579
    (implies (and (common-rounding-mode-p mode)
 
1580
                  (integerp n)
 
1581
                  (> n 1)
 
1582
                  (integerp x)
 
1583
                  (> x 0)
 
1584
                  (>= (expo x) n))
 
1585
             (= (rnd x mode n)
 
1586
                (if (and (eql mode 'near)
 
1587
                         (exactp x (1+ n))
 
1588
                         (not (exactp x n)))
 
1589
                    (trunc (+ x (rnd-const (expo x) mode n)) (1- n))
 
1590
                  (trunc (+ x (rnd-const (expo x) mode n)) n))))
 
1591
  :rule-classes ())
 
1592
 
 
1593
(defun roundup (x mode n)
 
1594
; Returns T when we should add an ulp after truncating x to n digits.
 
1595
  (case mode
 
1596
    (near+ (= (bitn x (- (expo x) n)) 1))
 
1597
    (near (and (= (bitn x (- (expo x) n)) 1)
 
1598
               (or (not (exactp x (1+ n)))
 
1599
                   (= (bitn x (- (1+ (expo x)) n)) 1))))
 
1600
    ((inf away) (not (exactp x n)))
 
1601
    (otherwise ())))
 
1602
 
 
1603
(defthm roundup-thm
 
1604
    (implies (and (common-rounding-mode-p mode)
 
1605
                  (integerp n)
 
1606
                  (> n 1)
 
1607
                  (integerp x)
 
1608
                  (> x 0)
 
1609
                  (>= (expo x) n))
 
1610
             (= (rnd x mode n)
 
1611
                (if (roundup x mode n)
 
1612
                    (fp+ (trunc x n) n)
 
1613
                  (trunc x n))))
 
1614
  :rule-classes ())
 
1615
 
 
1616
(defthmd rnd-sticky
 
1617
  (implies (and (common-rounding-mode-p mode)
 
1618
                (rationalp x)
 
1619
                (integerp m) 
 
1620
                (> m 0)
 
1621
                (integerp n) 
 
1622
                (>= n (+ m 2)))
 
1623
           (equal (rnd (sticky x n) mode m)
 
1624
                  (rnd x mode m))))
 
1625
 
 
1626
(defthmd rnd-diff
 
1627
  (implies (and (rationalp x)
 
1628
                (integerp n)
 
1629
                (> n 0)
 
1630
                (common-rounding-mode-p mode))
 
1631
           (< (abs (- x (rnd x mode n))) (expt 2 (- (1+ (expo x)) n)))))
 
1632
 
 
1633
(defthm plus-rnd
 
1634
  (implies (and (rationalp x)
 
1635
                (>= x 0)
 
1636
                (rationalp y)
 
1637
                (>= y 0)
 
1638
                (integerp k)
 
1639
                (exactp x (+ -1 k (- (expo x) (expo y))))
 
1640
                (common-rounding-mode-p mode))
 
1641
           (= (+ x (rnd y mode k))
 
1642
              (rnd (+ x y)
 
1643
                   mode
 
1644
                   (+ k (- (expo (+ x y)) (expo y))))))
 
1645
  :rule-classes ())
 
1646
 
 
1647
 
 
1648
 
 
1649
;;;**********************************************************************
 
1650
;;;                         Denormal Rounding 
 
1651
;;;**********************************************************************
 
1652
 
 
1653
(defund drnd-original (x mode n k)
 
1654
  (- (rnd (+ x (* (sgn x) (expt 2 (- 2 (expt 2 (1- k)))))) mode n)
 
1655
     (* (sgn x) (expt 2 (- 2 (expt 2 (1- k)))))))
 
1656
 
 
1657
(defthm drnd-original-0
 
1658
  (equal (drnd-original 0 mode n k)
 
1659
         0))
 
1660
 
 
1661
; a very similar rule was called drnd-original-flip
 
1662
(defthmd drnd-original-minus
 
1663
  (equal (drnd-original (* -1 x) mode n k)
 
1664
         (* -1 (drnd-original x (flip mode) n k))))
 
1665
 
 
1666
(defthm drnd-original-sticky
 
1667
    (implies (and (common-rounding-mode-p mode)
 
1668
                  (natp n)
 
1669
                  (> n 0)
 
1670
                  (natp m)
 
1671
                  (> m 1)
 
1672
                  (natp k)
 
1673
                  (> k 0)
 
1674
                  (rationalp x)
 
1675
                  (<= (expo x) (- 1 (expt 2 (1- k))))
 
1676
                  (<= (expo x) (- m (+ n (expt 2 (1- k))))))
 
1677
             (equal (drnd-original (sticky x m) mode n k)
 
1678
                    (drnd-original x mode n k)))
 
1679
  :rule-classes ())
 
1680
 
 
1681
(defthm drnd-original-tiny-equal
 
1682
    (implies (and (ieee-mode-p m)
 
1683
                  (natp n)
 
1684
                  (> n 0)
 
1685
                  (natp k)
 
1686
                  (> k 0)
 
1687
                  (rationalp x)
 
1688
                  (< (abs x) (expt 2 (- 2 (+ n (expt 2 (1- k))))))
 
1689
                  (rationalp y)
 
1690
                  (< (abs y) (expt 2 (- 2 (+ n (expt 2 (1- k))))))
 
1691
                  (equal (sgn x) (sgn y)))
 
1692
             (equal (drnd-original x m n k)
 
1693
                    (drnd-original y m n k)))
 
1694
  :rule-classes ())
 
1695
 
 
1696
 
 
1697
(defund spn (q)
 
1698
  (expt 2 (- 1 (bias q))))
 
1699
 
 
1700
;;These next three show that spn really is what it claims to be
 
1701
 
 
1702
(defthm positive-spn
 
1703
  (> (spn q) 0)
 
1704
  :rule-classes ( :linear))
 
1705
 
 
1706
 
 
1707
(defthmd nrepp-spn
 
1708
  (implies (and (integerp p)
 
1709
                (> p 0)
 
1710
                (integerp q)
 
1711
                (> q 1))
 
1712
           (nrepp (spn q) p q)))
 
1713
 
 
1714
 
 
1715
 
 
1716
(defund spd (p q)
 
1717
     (expt 2 (+ 2 (- (bias q)) (- p))))
 
1718
 
 
1719
;;These next three show that spd really is what it claims to be
 
1720
 
 
1721
(defthm positive-spd
 
1722
  (implies (and (integerp p)
 
1723
                (> p 1)
 
1724
                (> q 0))
 
1725
           (> (spd p q) 0))
 
1726
  :rule-classes :linear)
 
1727
 
 
1728
;; (defthm positive-spd
 
1729
;;   (implies (and (integerp p)
 
1730
;;                 (> p 1)
 
1731
;;                 (integerp q)
 
1732
;;                 (> q 0))
 
1733
;;            (> (spd p q) 0))
 
1734
;;     :rule-classes  :linear)
 
1735
 
 
1736
(defthm drepp-spd
 
1737
  (implies (and (integerp p)
 
1738
                (> p 1)
 
1739
                (integerp q)
 
1740
                (> q 0))
 
1741
           (drepp (spd p q) p q)))
 
1742
 
 
1743
(defthm smallest-spd
 
1744
  (implies (and (integerp p)
 
1745
                (> p 1)
 
1746
                (integerp q)
 
1747
                (> q 0)
 
1748
                (drepp r p q))
 
1749
           (>= (abs r) (spd p q))))
 
1750
 
 
1751
;DRND returns a denormal, or zero, or the smallest normal:
 
1752
 
 
1753
(defthm drnd-original-type
 
1754
  (implies (and (rationalp x)
 
1755
                (<= (abs x) (spn k))
 
1756
                (integerp n)
 
1757
                (> n 1)
 
1758
                (integerp k)
 
1759
                (> k 0)
 
1760
                (common-rounding-mode-p mode))
 
1761
           (or (drepp (drnd-original x mode n k) n k)
 
1762
               (= (drnd-original x mode n k) 0)
 
1763
               (= (drnd-original x mode n k) (* (sgn x) (spn k)))))
 
1764
  :rule-classes ())
 
1765
 
 
1766
(defthmd drnd-original-rewrite
 
1767
  (implies (and (rationalp x)
 
1768
                (<= (abs x) (spn k))
 
1769
                (common-rounding-mode-p mode)
 
1770
                (integerp n)
 
1771
                (> n 1)
 
1772
                (integerp k)
 
1773
                (> k 0))
 
1774
           (equal (drnd-original x mode n k)
 
1775
                  (rnd x 
 
1776
                       mode
 
1777
                       (+ n 
 
1778
                          (- (expo (spn k))) 
 
1779
                          (expo x))))))
 
1780
 
 
1781
(defthm drnd-original-of-drepp-is-NOP
 
1782
  (implies (and (drepp x n k)
 
1783
                (integerp n)
 
1784
                (> n 1)
 
1785
                (integerp k)
 
1786
                (> k 0)
 
1787
                (common-rounding-mode-p mode))
 
1788
           (equal (drnd-original x mode n k)
 
1789
                  x)))
 
1790
 
 
1791
(defthm drnd-original-spn-is-spn-general
 
1792
  (implies (and (= (abs x) (spn k))
 
1793
                (common-rounding-mode-p mode)
 
1794
                (integerp n)
 
1795
                (>= n 1)
 
1796
                (integerp k)
 
1797
                (> k 0)
 
1798
                (rationalp x))
 
1799
           (= (drnd-original x mode n k) x)))
 
1800
 
 
1801
(defthm drnd-original-trunc-never-goes-away-from-zero
 
1802
  (implies (and (integerp n)
 
1803
                (> n 1)
 
1804
                (integerp k)
 
1805
                (> k 0)
 
1806
                (rationalp x)
 
1807
                (<= (abs x) (spn k)))
 
1808
           (<= (abs (drnd-original x 'trunc n k))
 
1809
               (abs x))))
 
1810
 
 
1811
(defthm drnd-original-away-never-goes-toward-zero
 
1812
  (implies (and (integerp n)
 
1813
                (> n 1)
 
1814
                (integerp k)
 
1815
                (> k 0)
 
1816
                (rationalp x)
 
1817
                (<= (abs x) (spn k)))
 
1818
           (>= (abs (drnd-original x 'away n k))
 
1819
               (abs x))))
 
1820
 
 
1821
(defthm drnd-original-inf-never-goes-down
 
1822
  (implies (and (integerp n)
 
1823
                (> n 1)
 
1824
                (integerp k)
 
1825
                (> k 0)
 
1826
                (rationalp x)
 
1827
                (<= (abs x) (spn k)))
 
1828
           (>= (drnd-original x 'inf n k)
 
1829
               x)))
 
1830
 
 
1831
(defthm drnd-original-minf-never-goes-up
 
1832
  (implies (and (integerp n)
 
1833
                (> n 1)
 
1834
                (integerp k)
 
1835
                (> k 0)
 
1836
                (rationalp x)
 
1837
                (<= (abs x) (spn k)))
 
1838
           (<= (drnd-original x 'minf n k)
 
1839
               x)))
 
1840
 
 
1841
(defthm drnd-original-trunc-skips-no-denormals
 
1842
  (implies (and (integerp n)
 
1843
                (> n 1)
 
1844
                (integerp k)
 
1845
                (> k 0)
 
1846
                (rationalp x)
 
1847
                (<= (abs x) (spn k))
 
1848
                (drepp a n k)
 
1849
                (<= (abs a) (abs x))
 
1850
                )
 
1851
           (<= (abs a)
 
1852
               (abs (drnd-original x 'trunc n k)))))
 
1853
 
 
1854
(defthm drnd-original-away-skips-no-denormals
 
1855
  (implies (and (integerp n)
 
1856
                (> n 1)
 
1857
                (integerp k)
 
1858
                (> k 0)
 
1859
                (rationalp x)
 
1860
                (<= (abs x) (spn k))
 
1861
                (drepp a n k)
 
1862
                (>= (abs a) (abs x))
 
1863
                )
 
1864
           (>= (abs a) (abs (drnd-original x 'away n k)))))
 
1865
 
 
1866
 
 
1867
(defthm drnd-original-inf-skips-no-denormals
 
1868
  (implies (and (integerp n)
 
1869
                (> n 1)
 
1870
                (integerp k)
 
1871
                (> k 0)
 
1872
                (rationalp x)
 
1873
                (<= (abs x) (spn k))
 
1874
                (drepp a n k)
 
1875
                (>= a x))
 
1876
           (>= a (drnd-original x 'inf n k))))
 
1877
 
 
1878
(defthm drnd-original-minf-skips-no-denormals
 
1879
  (implies (and (integerp n)
 
1880
                (> n 1)
 
1881
                (integerp k)
 
1882
                (> k 0)
 
1883
                (rationalp x)
 
1884
                (<= (abs x) (spn k))
 
1885
                (drepp a n k)
 
1886
                (<= a x))
 
1887
           (<= a (drnd-original x 'minf n k))))
 
1888
 
 
1889
(defthm drnd-original-diff
 
1890
  (implies (and (rationalp x)
 
1891
                (<= (ABS X) (SPN K))
 
1892
                (integerp n)
 
1893
                (> n 1)
 
1894
                (integerp k)
 
1895
                (> k 0)
 
1896
                (common-rounding-mode-p mode))
 
1897
           (< (abs (- x (drnd-original x mode n k))) (spd n k))))
 
1898
 
 
1899
(defund next-denormal (x n k)
 
1900
  (+ x (spd n k)))
 
1901
 
 
1902
;;NEXT-DENORMAL behaves as expected:
 
1903
 
 
1904
(defthm denormal-spacing
 
1905
  (implies (and (integerp n)
 
1906
                (integerp k)
 
1907
                (> k 0)
 
1908
                (> n 1)
 
1909
                (drepp x n k)
 
1910
                (drepp x+ n k)
 
1911
                (>= x 0)
 
1912
                (> x+ x))
 
1913
           (>= x+ (next-denormal x n k))))
 
1914
 
 
1915
(defthm no-denormal-is-closer-than-what-drnd-original-near-returns
 
1916
  (implies (and (rationalp x)
 
1917
                (<= (abs x) (spn k))
 
1918
                (integerp n)
 
1919
                (> n 1)
 
1920
                (integerp k)
 
1921
                (> k 0)
 
1922
                (drepp a n k))
 
1923
           (>= (abs (- x a)) (abs (- x (drnd-original x 'near n k))))))
 
1924
 
 
1925