← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/rtl/rel6/support/support/oddr-proofs.lisp

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

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/rtl/rel6/support/support/oddr-proofs.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
;;;***************************************************************
 
4
;;;An ACL2 Library of Floating Point Arithmetic
 
5
 
 
6
;;;David M. Russinoff
 
7
;;;Advanced Micro Devices, Inc.
 
8
;;;February, 1998
 
9
;;;***************************************************************
 
10
 
 
11
;(include-book "near")
 
12
(local (include-book "../../arithmetic/top"))
 
13
(local (include-book "float"))
 
14
(local (include-book "trunc"))
 
15
(local (include-book "away"))
 
16
(local (include-book "near"))
 
17
 
 
18
;; Necessary functions:
 
19
 
 
20
(defund fl (x)
 
21
  (declare (xargs :guard (real/rationalp x)))
 
22
  (floor x 1))
 
23
 
 
24
(defund cg (x)
 
25
  (declare (xargs :guard (real/rationalp x)))
 
26
  (- (fl (- x))))
 
27
 
 
28
(defun expo-measure (x)
 
29
;  (declare (xargs :guard (and (real/rationalp x) (not (equal x 0)))))
 
30
  (cond ((not (rationalp x)) 0)
 
31
        ((< x 0) '(2 . 0))
 
32
        ((< x 1) (cons 1 (fl (/ x))))
 
33
        (t (fl x))))
 
34
 
 
35
(defund expo (x)
 
36
  (declare (xargs :guard t
 
37
                  :measure (expo-measure x)))
 
38
  (cond ((or (not (rationalp x)) (equal x 0)) 0)
 
39
        ((< x 0) (expo (- x)))
 
40
        ((< x 1) (1- (expo (* 2 x))))
 
41
        ((< x 2) 0)
 
42
        (t (1+ (expo (/ x 2))))))
 
43
 
 
44
;could redefine to divide by the power of 2 (instead of making it a negative power of 2)...
 
45
(defund sig (x)
 
46
  (declare (xargs :guard t))
 
47
  (if (rationalp x)
 
48
      (if (< x 0)
 
49
          (- (* x (expt 2 (- (expo x)))))
 
50
        (* x (expt 2 (- (expo x)))))
 
51
    0))
 
52
 
 
53
;make defund?
 
54
(defun sgn (x)
 
55
  (declare (xargs :guard t))
 
56
  (if (or (not (rationalp x)) (equal x 0))
 
57
      0
 
58
    (if (< x 0)
 
59
        -1
 
60
      1)))
 
61
 
 
62
(defund exactp (x n)
 
63
;  (declare (xargs :guard (and (real/rationalp x) (integerp n))))
 
64
  (integerp (* (sig x) (expt 2 (1- n)))))
 
65
 
 
66
(defund trunc (x n)
 
67
  (declare (xargs :guard (integerp n)))
 
68
  (* (sgn x) (fl (* (expt 2 (1- n)) (sig x))) (expt 2 (- (1+ (expo x)) n))))
 
69
 
 
70
(defund away (x n)
 
71
  (* (sgn x) (cg (* (expt 2 (1- n)) (sig x))) (expt 2 (- (1+ (expo x)) n))))
 
72
 
 
73
(defund re (x)
 
74
  (- x (fl x)))
 
75
 
 
76
(defund near (x n)
 
77
  (let ((z (fl (* (expt 2 (1- n)) (sig x))))
 
78
        (f (re (* (expt 2 (1- n)) (sig x)))))
 
79
    (if (< f 1/2)
 
80
        (trunc x n)
 
81
      (if (> f 1/2)
 
82
          (away x n)
 
83
        (if (evenp z)
 
84
            (trunc x n)
 
85
          (away x n))))))
 
86
 
 
87
;;
 
88
;; New stuff:
 
89
;;
 
90
 
 
91
(defund oddr (x n)
 
92
  (let ((z (fl (* (expt 2 (1- n)) (sig x)))))
 
93
    (if (evenp z)
 
94
        (* (sgn x) (1+ z) (expt 2 (- (1+ (expo x)) n)))
 
95
      (* (sgn x) z (expt 2 (- (1+ (expo x)) n))))))
 
96
 
 
97
(defthm oddr-pos
 
98
  (implies (and (< 0 x)
 
99
                (rationalp x)
 
100
                (integerp n)
 
101
                (> n 0))
 
102
           (< 0 (oddr x n)))
 
103
  :rule-classes ()
 
104
  :otf-flg t
 
105
  :hints (("Goal" :in-theory (e/d (oddr) ( SIG-LESS-THAN-1-MEANS-X-0 sig-lower-bound))
 
106
           :use ((:instance sig-lower-bound)))))
 
107
 
 
108
(defthm oddr>=trunc
 
109
    (implies (and (rationalp x)
 
110
                  (> x 0)
 
111
                  (integerp n)
 
112
                  (> n 0))
 
113
             (>= (oddr x n) (trunc x n)))
 
114
  :rule-classes ()
 
115
  :hints (("Goal" :in-theory (enable oddr)
 
116
                  :use ((:instance trunc)
 
117
                        ))))
 
118
 
 
119
;BOZO just opens up ODDR when x is positive
 
120
;leave disabled!
 
121
(defthmd oddr-rewrite
 
122
    (implies (and (< 0 x) ;note this hyp
 
123
                  (rationalp x)
 
124
                  (integerp n)
 
125
                  (< 0 n))
 
126
             (equal (oddr x n)
 
127
                    (let ((z (fl (* (expt 2 (- (1- n) (expo x))) x))))
 
128
                      (if (evenp z)
 
129
                          (* (1+ z) (expt 2 (- (1+ (expo x)) n)))
 
130
                        (* z (expt 2 (- (1+ (expo x)) n)))))))
 
131
  :hints (("Goal" :in-theory (enable sig sgn oddr expt-split))))
 
132
 
 
133
(local 
 
134
 (defthm hack2
 
135
    (implies (and (integerp n)
 
136
                  (rationalp x))
 
137
             (= (fl (* 1/2 x (expt 2 n)))
 
138
                (fl (* x (expt 2 (1- n))))))
 
139
    :hints (("Goal" :in-theory (enable expt)))
 
140
  :rule-classes ()))
 
141
 
 
142
(local
 
143
 (defthm oddr-other-1
 
144
    (implies (and (rationalp x)
 
145
                 (> x 0)
 
146
                 (integerp n)
 
147
                 (> n 1))
 
148
             (= (trunc x (1- n))
 
149
                (* (fl (/ (* (expt 2 (- (1- n) (expo x))) x) 2))
 
150
                   (expt 2 (- (+ 2 (expo x)) n)))))
 
151
  :rule-classes ()
 
152
  :hints (("Goal" :in-theory (enable trunc-pos-rewrite)           
 
153
                  :use ((:instance hack2 (n (- (1- n) (expo x)))))))))
 
154
 
 
155
(local
 
156
 (defthm oddr-other-2
 
157
    (implies (and (rationalp x)
 
158
                 (> x 0)
 
159
                 (integerp n)
 
160
                 (> n 1))
 
161
             (= (trunc x (1- n))
 
162
                (* (fl (/ (fl (* (expt 2 (- (1- n) (expo x))) x)) 2))
 
163
                   (expt 2 (- (+ 2 (expo x)) n)))))
 
164
  :rule-classes ()
 
165
  :hints (("Goal" :in-theory (disable fl/int-rewrite)
 
166
                  :use ((:instance oddr-other-1)
 
167
                        (:instance fl/int-rewrite (x (* (expt 2 (- (1- n) (expo x))) x)) (n 2)))))))
 
168
 
 
169
;move!
 
170
(defthm fl/2
 
171
  (implies (integerp z)
 
172
           (= (fl (/ z 2))
 
173
              (if (evenp z)
 
174
                  (/ z 2)
 
175
                (/ (1- z) 2))))
 
176
  :hints (("Goal" :in-theory (enable evenp)))
 
177
  :rule-classes ())
 
178
 
 
179
(local
 
180
 (defthm oddr-other-3
 
181
    (implies (and (rationalp x)
 
182
                  (> x 0)
 
183
                  (integerp n) 
 
184
                  (> n 1)
 
185
                  (= z (fl (* (expt 2 (- (1- n) (expo x))) x)))
 
186
                  (evenp z))
 
187
             (= (trunc x (1- n))
 
188
                (* z (expt 2 (- (1+ (expo x)) n)))))
 
189
  :rule-classes ()
 
190
  :hints (("Goal" :use ((:instance fl/2)
 
191
                        (:instance expt-split (r 2) (j (- (1+ (expo x)) n)) (i 1))
 
192
                        (:instance oddr-other-2))))))
 
193
 
 
194
(local
 
195
 (defthm oddr-other-4
 
196
    (implies (and (rationalp x)
 
197
                  (> x 0)
 
198
                  (integerp n) 
 
199
                  (> n 1)
 
200
                  (= z (fl (* (expt 2 (- (1- n) (expo x))) x)))
 
201
                  (not (evenp z)))
 
202
             (= (* (fl (/ (fl (* (expt 2 (- (1- n) (expo x))) x)) 2))
 
203
                   (expt 2 (- (+ 2 (expo x)) n)))
 
204
                (* (fl (/ z 2)) (expt 2 (- (+ 2 (expo x)) n)))))
 
205
  :rule-classes ()))
 
206
 
 
207
(local
 
208
 (defthm oddr-other-5
 
209
    (implies (and (rationalp x)
 
210
                  (> x 0)
 
211
                  (integerp n) 
 
212
                  (> n 1)
 
213
                  (= z (fl (* (expt 2 (- (1- n) (expo x))) x)))
 
214
                  (not (evenp z)))
 
215
             (= (trunc x (1- n))
 
216
                (* (fl (/ z 2)) (expt 2 (- (+ 2 (expo x)) n)))))
 
217
  :rule-classes ()
 
218
  :hints (("Goal" :use ((:instance oddr-other-2)
 
219
                        (:instance oddr-other-4))))))
 
220
 
 
221
(local 
 
222
 (defthm hack3
 
223
    (implies (and (rationalp x)
 
224
                  (rationalp y)
 
225
                  (rationalp z)
 
226
                  (equal x y))
 
227
             (= (* x z) (* y z)))
 
228
  :rule-classes ()))
 
229
 
 
230
(local
 
231
 (defthm oddr-other-6
 
232
    (implies (and (rationalp x)
 
233
                  (> x 0)
 
234
                  (integerp n)
 
235
                  (> n 1)
 
236
                  (= z (fl (* (expt 2 (- (1- n) (expo x))) x)))
 
237
                  (not (evenp z)))
 
238
             (= (trunc x (1- n))
 
239
                (* (/ (1- z) 2) (expt 2 (- (+ 2 (expo x)) n)))))
 
240
  :rule-classes ()
 
241
  :hints (("Goal" :use ((:instance fl/2)
 
242
                        (:instance oddr-other-5)
 
243
                        (:instance hack3
 
244
                                   (x (/ (1- z) 2))
 
245
                                   (y (fl (/ z 2)))
 
246
                                   (z (expt 2 (- (+ 2 (expo x)) n)))))))))
 
247
 
 
248
(local
 
249
 (defthm oddr-other-7
 
250
   (implies (and (rationalp x)
 
251
                 (> x 0)
 
252
                 (integerp n)
 
253
                 (> n 1)
 
254
                 (= z (fl (* (expt 2 (- (1- n) (expo x))) x)))
 
255
                 (not (evenp z)))
 
256
            (= (trunc x (1- n))
 
257
               (* (1- z) (expt 2 (- (1+ (expo x)) n)))))
 
258
   :rule-classes ()
 
259
   :hints (("Goal" :in-theory (enable expt-split)
 
260
            :use ((:instance oddr-other-6)
 
261
                  (:instance expt-split (r 2) (j (- (1+ (expo x)) n)) (i 1)))))))
 
262
 
 
263
(defthm oddr-other
 
264
    (implies (and (rationalp x)
 
265
                  (> x 0)
 
266
                  (integerp n) 
 
267
                  (> n 1))
 
268
             (= (oddr x n)
 
269
                (+ (trunc x (1- n))
 
270
                   (expt 2 (- (1+ (expo x)) n)))))
 
271
  :rule-classes ()
 
272
  :hints (("Goal" :use ((:instance oddr-other-3 (z (fl (* (expt 2 (- (1- n) (expo x))) x))))
 
273
                        (:instance oddr-other-7 (z (fl (* (expt 2 (- (1- n) (expo x))) x))))
 
274
                        (:instance oddr-rewrite)))))
 
275
 
 
276
(local
 
277
 (defthm expo-oddr-1
 
278
    (implies (and (rationalp x)
 
279
                  (integerp n)
 
280
                  (> x 0)
 
281
                  (> n 0))
 
282
             (< (trunc x n) (expt 2 (1+ (expo x)))))
 
283
  :rule-classes ()
 
284
  :hints (("Goal" :in-theory (e/d () ( expo-trunc abs-trunc))
 
285
                  :use ((:instance expo-trunc)
 
286
;                       (:instance trunc-pos)
 
287
                        (:instance expo-upper-bound (x (trunc x n))))))))
 
288
 
 
289
(local
 
290
 (defthm expo-oddr-2
 
291
    (implies (and (rationalp x)
 
292
                  (integerp n)
 
293
                  (> x 0)
 
294
                  (> n 1))
 
295
             (< (oddr x n) (expt 2 (1+ (expo x)))))
 
296
  :rule-classes ()
 
297
  :hints (("Goal" :in-theory (e/d (expt-split) ( expo-trunc abs-trunc))
 
298
                  :use ((:instance expo-oddr-1 (n (1- n)))
 
299
                        (:instance oddr-other)
 
300
                        (:instance exactp-2**n (m (1- n)) (n (1+ (expo x))))
 
301
                        (:instance expo-trunc (n (1- n)))
 
302
                        (:instance expt-strong-monotone (n (- (1+ (expo x)) n)) (m (- (1+ (expo x)) (1- n))))
 
303
;                       (:instance trunc-pos (n (1- n)))
 
304
                        (:instance fp+2 (n (1- n)) (x (trunc x (1- n))) (y (expt 2 (1+ (expo x))))))))))
 
305
 
 
306
(local
 
307
 (defthm expo-oddr-3
 
308
    (implies (and (rationalp x)
 
309
                  (integerp n)
 
310
                  (> x 0)
 
311
                  (> n 1))
 
312
             (<= (expo (oddr x n)) (expo x)))
 
313
  :rule-classes ()
 
314
  :hints (("Goal" :use ((:instance expo-oddr-2)
 
315
                        (:instance oddr-pos)
 
316
                        (:instance expo-upper-2 (x (oddr x n)) (n (1+ (expo x)))))))))
 
317
 
 
318
(defthm expo-oddr
 
319
    (implies (and (rationalp x)
 
320
                  (integerp n)
 
321
                  (> x 0)
 
322
                  (> n 1))
 
323
             (equal (expo (oddr x n)) (expo x)))
 
324
  :hints (("Goal" :in-theory (e/d ( expt-split ) (EXPO-COMPARISON-REWRITE-TO-BOUND
 
325
                                                  EXPO-COMPARISON-REWRITE-TO-BOUND-2))
 
326
                  :use ((:instance expo-oddr-3)
 
327
                        (:instance oddr-other)
 
328
;                       (:instance expt-pos (x (- (1+ (expo x)) n)))
 
329
                        (:instance expo-monotone (y (oddr x n)) (x (trunc x (1- n))))
 
330
                        (:instance oddr-pos)
 
331
;                       (:instance trunc-pos (n (1- n)))
 
332
                        ))))
 
333
 
 
334
(local
 
335
 (defthm exactp-oddr-1
 
336
    (implies (and (rationalp x)
 
337
                  (integerp n)
 
338
                  (> x 0)
 
339
                  (> n 1))
 
340
             (= (* (+ (trunc x (1- n))
 
341
                      (expt 2 (- (1+ (expo x)) n)))
 
342
                   (expt 2 (- (1- n) (expo x))))
 
343
                (1+ (* (trunc x (1- n)) (expt 2 (- (1- n) (expo x)))))))
 
344
             :rule-classes ()
 
345
  :hints (("Goal" :in-theory (disable ;expt-pos
 
346
                                      abs-trunc)
 
347
                  :use ((:instance expt-split (r 2) (j (- (1- n) (expo x))) (i (- (1+ (expo x)) n))))))))
 
348
 
 
349
(local
 
350
 (defthm exactp-oddr-2
 
351
    (implies (and (rationalp x)
 
352
                  (integerp n)
 
353
                  (> x 0)
 
354
                  (> n 1))
 
355
             (= (* (oddr x n) (expt 2 (- (1- n) (expo x))))
 
356
                (1+ (* (trunc x (1- n)) (expt 2 (- (1- n) (expo x)))))))
 
357
             :rule-classes ()
 
358
  :hints (("Goal" :in-theory (disable ;expt-pos
 
359
                                      abs-trunc)
 
360
                  :use ((:instance oddr-other)
 
361
                        (:instance exactp-oddr-1))))))
 
362
 
 
363
(local
 
364
 (defthm exactp-oddr-3
 
365
    (implies (and (rationalp x)
 
366
                  (integerp n))
 
367
             (= (expt 2 (- (1- n) (expo x)))
 
368
                (* 2 (expt 2 (- (- n 2) (expo x))))))
 
369
  :rule-classes ()
 
370
  :hints (("Goal" :use ((:instance expt-split (r 2) (j (- (- n 2) (expo x))) (i 1)))))))
 
371
 
 
372
(local
 
373
 (defthm exactp-oddr-4
 
374
    (implies (and (rationalp x)
 
375
                  (rationalp y)
 
376
                  (integerp n))
 
377
             (= (* y 2 (expt 2 (- (- n 2) (expo x))))
 
378
                (* 2 y (expt 2 (- (- n 2) (expo x))))))
 
379
  :rule-classes ()))
 
380
 
 
381
(local
 
382
 (defthm exactp-oddr-5
 
383
    (implies (and (rationalp x)
 
384
                  (integerp n))
 
385
             (= (* (trunc x (1- n)) (expt 2 (- (1- n) (expo x))))
 
386
                (* 2 (trunc x (1- n)) (expt 2 (- (- n 2) (expo x))))))
 
387
  :rule-classes ()
 
388
  :hints (("Goal" :use ((:instance exactp-oddr-3)
 
389
                        (:instance exactp-oddr-4 (y (trunc x (1- n)))))))))
 
390
 
 
391
(local
 
392
 (defthm exactp-oddr-6
 
393
    (implies (and (rationalp x)
 
394
                  (integerp n)
 
395
                  (> x 0)
 
396
                  (> n 1))
 
397
             (= (* (oddr x n) (expt 2 (- (1- n) (expo x))))
 
398
                (1+ (* 2 (* (trunc x (1- n)) (expt 2 (- (- n 2) (expo x))))))))
 
399
             :rule-classes ()
 
400
  :hints (("Goal" :in-theory (disable ;expt-pos
 
401
                                      abs-trunc)
 
402
                  :use ((:instance exactp-oddr-2)
 
403
                        (:instance exactp-oddr-5))))))
 
404
 
 
405
(defthm exactp-oddr
 
406
    (implies (and (rationalp x)
 
407
                  (integerp n)
 
408
                  (> x 0)
 
409
                  (> n 1))
 
410
             (exactp (oddr x n) n))
 
411
             :rule-classes ()
 
412
  :hints (("Goal" :in-theory (disable ;expt-pos
 
413
                                      abs-trunc)
 
414
                  :use ((:instance exactp-oddr-6)
 
415
                        (:instance exactp2 (x (oddr x n)))
 
416
                        (:instance exactp2 (x (trunc x (1- n))) (n (1- n)))))))
 
417
(local
 
418
 (defthm not-exactp-oddr-1
 
419
    (implies (and (rationalp x)
 
420
                  (integerp n)
 
421
                  (> x 0)
 
422
                  (> n 1))
 
423
             (= (* (+ (trunc x (1- n)) (expt 2 (- (1+ (expo x)) n)))
 
424
                   (expt 2 (- (- n 2) (expo x))))
 
425
                (+ (* (trunc x (1- n)) (expt 2 (- (- n 2) (expo x)))) 1/2)))
 
426
             :rule-classes ()
 
427
             :hints (("Goal" :use ((:instance expt-split (r 2) (i (- (- n 2) (expo x))) (j (- (1+ (expo x)) n))))))))
 
428
 
 
429
(local
 
430
 (defthm not-exactp-oddr-2
 
431
    (implies (and (rationalp x)
 
432
                  (integerp n)
 
433
                  (> x 0)
 
434
                  (> n 1))
 
435
             (= (* (oddr x n)
 
436
                   (expt 2 (- (- n 2) (expo x))))
 
437
                (+ (* (trunc x (1- n)) (expt 2 (- (- n 2) (expo x)))) 1/2)))
 
438
             :rule-classes ()
 
439
  :hints (("Goal" :use ((:instance oddr-other)
 
440
                        (:instance not-exactp-oddr-1))))))
 
441
 
 
442
(defthm not-exactp-oddr
 
443
    (implies (and (rationalp x)
 
444
                  (integerp n)
 
445
                  (> x 0)
 
446
                  (> n 1))
 
447
             (not (exactp (oddr x n) (1- n))))
 
448
             :rule-classes ()
 
449
  :hints (("Goal" :in-theory (disable ;expt-pos
 
450
                              EQUAL-MULTIPLY-THROUGH-BY-inverted-factor-FROM-RIGHT-HAND-SIDE
 
451
                                      abs-trunc)
 
452
                  :use ((:instance not-exactp-oddr-2)
 
453
                        (:instance exactp2 (x (oddr x n)) (n (1- n)))
 
454
                        (:instance exactp2 (x (trunc x (1- n))) (n (1- n)))))))
 
455
 
 
456
(local
 
457
 (defthm trunc-oddr-1
 
458
    (implies (and (rationalp x)
 
459
                  (> x 0)
 
460
                  (integerp n)
 
461
                  (> n 1))
 
462
             (= (trunc (oddr x n) (1- n))
 
463
                (* (fl (* (expt 2 (- (- n 2) (expo x))) 
 
464
                          (+ (* (fl (* (expt 2 (- (- n 2) (expo x)))
 
465
                                       x))
 
466
                                (expt 2 (- (+ (expo x) 2) n)))
 
467
                             (expt 2 (- (1+ (expo x)) n)))))
 
468
                   (expt 2 (- (+ (expo x) 2) n)))))
 
469
  :rule-classes ()
 
470
  :hints (("Goal" :in-theory (enable trunc-pos-rewrite)
 
471
                  :use ((:instance oddr-other)
 
472
                        (:instance oddr-pos))))))
 
473
 
 
474
(local
 
475
 (defthm trunc-oddr-2
 
476
    (implies (and (rationalp x)
 
477
                  (> x 0)
 
478
                  (integerp n)
 
479
                  (> n 1))
 
480
             (= (trunc (oddr x n) (1- n))
 
481
                (* (fl (+ (fl (* (expt 2 (- (- n 2) (expo x)))
 
482
                                 x))
 
483
                          1/2))
 
484
                   (expt 2 (- (+ (expo x) 2) n)))))
 
485
  :rule-classes ()
 
486
  :hints (("Goal" :in-theory (enable a15)
 
487
           :use ((:instance trunc-oddr-1)
 
488
                        (:instance expt-split (r 2) (i (- (- n 2) (expo x))) (j (- (+ (expo x) 2) n)))
 
489
                        (:instance expt-split (r 2) (i (- (- n 2) (expo x))) (j (- (+ (expo x) 1) n))))))))
 
490
 
 
491
(local
 
492
 (defthm trunc-oddr-3
 
493
    (implies (and (rationalp x)
 
494
                  (> x 0)
 
495
                  (integerp n)
 
496
                  (> n 1))
 
497
             (= (trunc (oddr x n) (1- n))
 
498
                (* (fl (* (expt 2 (- (- n 2) (expo x)))
 
499
                          x))
 
500
                   (expt 2 (- (+ (expo x) 2) n)))))
 
501
  :rule-classes ()
 
502
  :hints (("Goal" :use ((:instance trunc-oddr-2))))))
 
503
 
 
504
(local
 
505
 (defthm trunc-oddr-4
 
506
    (implies (and (rationalp x)
 
507
                  (> x 0)
 
508
                  (integerp n)
 
509
                  (> n 1))
 
510
             (= (trunc (oddr x n) (1- n))
 
511
                (trunc x (1- n))))
 
512
  :rule-classes ()
 
513
  :hints (("Goal" :in-theory (enable trunc-pos-rewrite)
 
514
                  :use ((:instance trunc-oddr-3))))))
 
515
 
 
516
(defthm trunc-oddr
 
517
    (implies (and (rationalp x)
 
518
                  (> x 0)
 
519
                  (integerp n)
 
520
                  (integerp m)
 
521
                  (> m 0)
 
522
                  (> n m))
 
523
             (= (trunc (oddr x n) m)
 
524
                (trunc x m)))
 
525
  :rule-classes ()
 
526
  :hints (("Goal" :in-theory (disable trunc-trunc)
 
527
           :use ((:instance trunc-oddr-4)
 
528
                        (:instance oddr-pos)
 
529
                        (:instance trunc-trunc (n (1- n)))
 
530
                        (:instance trunc-trunc (n (1- n)) (x (oddr x n)))
 
531
                        ))))
 
532
 
 
533
(defun kp (k x y)
 
534
  (+ k (- (expo (+ x y)) (expo y))))
 
535
 
 
536
(defthm oddr-plus
 
537
    (implies (and (rationalp x)
 
538
                  (rationalp y)
 
539
                  (integerp k)
 
540
                  (> x 0)
 
541
                  (> y 0)
 
542
                  (> k 1)
 
543
                  (> (+ (1- k) (- (expo x) (expo y))) 0)
 
544
                  (exactp x (+ (1- k) (- (expo x) (expo y)))))
 
545
             (= (+ x (oddr y k))
 
546
                (oddr (+ x y) (kp k x y))))
 
547
  :rule-classes ()
 
548
  :hints (("Goal" :use ((:instance oddr-other (n k) (x y))
 
549
                        (:instance expo-monotone (x y) (y (+ x y)))
 
550
                        (:instance plus-trunc (k (1- k)))
 
551
                        (:instance oddr-other (x (+ x y)) (n (kp k x y)))))))
 
552
 
 
553
(defthm trunc-trunc-oddr
 
554
    (implies (and (rationalp x)
 
555
                  (rationalp y)
 
556
                  (integerp m)
 
557
                  (integerp k)
 
558
                  (> x y)
 
559
                  (> y 0)
 
560
                  (> k 0)
 
561
                  (>= (- m 2) k))
 
562
             (>= (trunc x k) (trunc (oddr y m) k)))
 
563
  :rule-classes ()
 
564
  :hints (("Goal" :use ((:instance trunc-oddr (x y) (m k) (n m))
 
565
                        (:instance trunc-monotone (x y) (y x) (n k))))))
 
566
 
 
567
(local
 
568
 (defthm away-away-oddr-1
 
569
    (implies (and (rationalp x)
 
570
                  (rationalp y)
 
571
                  (integerp m)
 
572
                  (integerp k)
 
573
                  (> x y)
 
574
                  (> y 0)
 
575
                  (> k 0)
 
576
                  (>= (- m 2) k))
 
577
             (> (away x k) (trunc y (1- m))))
 
578
  :rule-classes ()
 
579
  :hints (("Goal" :use ((:instance away-lower-pos (n k))
 
580
                        (:instance trunc-upper-pos (x y) (n (1- m))))))))
 
581
 
 
582
(local
 
583
 (defthm away-away-oddr-2
 
584
    (implies (and (rationalp x)
 
585
                  (rationalp y)
 
586
                  (integerp m)
 
587
                  (integerp k)
 
588
                  (> x y)
 
589
                  (> y 0)
 
590
                  (> k 0)
 
591
                  (>= (- m 2) k))
 
592
             (>= (away x k) (+ (trunc y (1- m)) (expt 2 (- (+ (expo y) 2) m)))))
 
593
  :rule-classes ()
 
594
  :hints (("Goal" :use ((:instance away-away-oddr-1)
 
595
                        (:instance fp+2 (x (trunc y (1- m))) (y (away x k)) (n (1- m)))
 
596
                        (:instance expo-trunc (x y) (n (1- m)))
 
597
                        (:instance trunc-exactp-a (x y) (n (1- m)))
 
598
                        (:instance away-exactp-a (n k))
 
599
;                       (:instance trunc-pos (x y) (n (1- m)))
 
600
                        (:instance exactp-<= (x (away x k)) (m k) (n (1- m))))))))
 
601
 
 
602
(local
 
603
 (defthm away-away-oddr-3
 
604
   (implies (and (rationalp x)
 
605
                 (rationalp y)
 
606
                 (integerp m)
 
607
                 (integerp k)
 
608
                 (> x y)
 
609
                 (> y 0)
 
610
                 (> k 0)
 
611
                 (>= (- m 2) k))
 
612
            (> (away x k) (oddr y m)))
 
613
   :rule-classes ()
 
614
   :hints (("Goal" :in-theory (disable EXPT-COMPARE)
 
615
            :use ((:instance away-away-oddr-2)
 
616
                  (:instance oddr-other (x y) (n m))
 
617
                  (:instance expt-strong-monotone (n (- (1+ (expo y)) m)) (m (- (+ (expo y) 2) m))))))))
 
618
 
 
619
(defthm away-away-oddr
 
620
    (implies (and (rationalp x)
 
621
                  (rationalp y)
 
622
                  (integerp m)
 
623
                  (integerp k)
 
624
                  (> x y)
 
625
                  (> y 0)
 
626
                  (> k 0)
 
627
                  (>= (- m 2) k))
 
628
             (>= (away x k) (away (oddr y m) k)))
 
629
  :rule-classes ()
 
630
  :hints (("Goal" :use ((:instance away-away-oddr-3)
 
631
                        (:instance oddr-pos (x y) (n m))
 
632
                        (:instance away-exactp-c (a (away x k)) (x (oddr y m)) (n k))
 
633
                        (:instance away-exactp-a (n k))))))
 
634
 
 
635
(defthm near-near-oddr
 
636
    (implies (and (rationalp x)
 
637
                  (rationalp y)
 
638
                  (integerp m)
 
639
                  (integerp k)
 
640
                  (> x y)
 
641
                  (> y 0)
 
642
                  (> k 0)
 
643
                  (>= (- m 2) k))
 
644
             (>= (near x k) (near (oddr y m) k)))
 
645
  :rule-classes ()
 
646
  :hints (("Goal" :use ((:instance trunc-exactp-a (n (1- m)) (x y))
 
647
                        (:instance oddr-pos (x y) (n m))
 
648
;                       (:instance trunc-pos (x y) (n (1- m)))
 
649
                        (:instance trunc-upper-pos (x y) (n (1- m)))
 
650
                        (:instance expo-trunc (x y) (n (1- m)))
 
651
                        (:instance oddr-other (x y) (n m))
 
652
                        (:instance expt-strong-monotone 
 
653
                                   (n (- (1+ (expo y)) m)) 
 
654
                                   (m (- (+ 2 (expo y)) m)))
 
655
                        (:instance near-near
 
656
                                   (n (- m 2))
 
657
                                   (a (trunc y (1- m)))
 
658
                                   (y (oddr y m)))))))
 
 
b'\\ No newline at end of file'