← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/arithmetic-3/extra/ext.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/arithmetic-3/extra/ext.lisp
 
1
; Contributed by Alex Spiridonov, with helpful consulting from Robert Krug.
 
2
 
 
3
(in-package "ACL2")
 
4
 
 
5
; Theorems from arithmetic/top-with-meta
 
6
(encapsulate
 
7
  ()
 
8
 
 
9
  (local (include-book "arithmetic/top-with-meta" :dir :system))
 
10
 
 
11
  ; Theorems about inequalities
 
12
  (defthm /-inverts-order-1
 
13
    (implies (and (< 0 x)
 
14
                  (< x y)
 
15
                  (rationalp x)
 
16
                  (rationalp y))
 
17
             (< (/ y) (/ x))))
 
18
  
 
19
  (defthm /-inverts-order-2
 
20
    (implies (and (< y 0)
 
21
                  (< x y)
 
22
                  (rationalp x)
 
23
                  (rationalp y))
 
24
             (< (/ y) (/ x))))
 
25
 
 
26
  (defthm /-inverts-weak-order
 
27
    (implies (and (< 0 x)
 
28
                  (<= x y)
 
29
                  (rationalp x)
 
30
                  (rationalp y))
 
31
             (not (< (/ x) (/ y)))))
 
32
 
 
33
  ; Theorems about equalities
 
34
  (defthm equal-*-x-y-x
 
35
    (equal (equal (* x y) x)
 
36
           (or (equal x 0)
 
37
               (and (equal y 1)
 
38
                    (acl2-numberp x)))))
 
39
 
 
40
  (defthm equal-*-x-y-y
 
41
    (equal (equal (* x y) y)
 
42
           (or (equal y 0)
 
43
               (and (equal x 1)
 
44
                    (acl2-numberp y)))))
 
45
 
 
46
  (defthm equal-/
 
47
   (implies (and (acl2-numberp x)
 
48
                 (not (equal 0 x)))
 
49
            (equal (equal (/ x) y)
 
50
                   (equal 1 (* x y)))))
 
51
 
 
52
; From rtl/rel5/arithmetic
 
53
; Originally written as (mod (binary-* k x) (binary-* y k)), but we write is
 
54
; this way because arithmetic-3 will rewrite (binary-* y k) to (binary-* k y).
 
55
  (defthm mod-cancel-special-1-ext
 
56
    (implies (if (acl2-numberp x)
 
57
                 (if (rationalp k)
 
58
                     (if (acl2-numberp y)
 
59
                         (if (not (equal y '0))
 
60
                             (not (equal k '0))
 
61
                             'nil)
 
62
                         'nil)
 
63
                     'nil)
 
64
                 'nil)
 
65
             (equal (mod (binary-* k x) (binary-* k y))
 
66
                    (binary-* k (mod x y)))))
 
67
 
 
68
)
 
69
 
 
70
; Theorems from ihs
 
71
(encapsulate
 
72
  ()
 
73
 
 
74
  (local (include-book "ihs/ihs-definitions" :dir :system))
 
75
  (local (include-book "ihs/ihs-lemmas" :dir :system))
 
76
  (local (minimal-ihs-theory))
 
77
 
 
78
  (defthm integerp-i/j-integerp-forward
 
79
    (implies
 
80
     (and (integerp (/ i j))
 
81
          (real/rationalp i)
 
82
          (integerp j)
 
83
          (not (zerop j)))
 
84
     (integerp i))
 
85
    :rule-classes
 
86
    ((:forward-chaining
 
87
      :corollary
 
88
      (implies
 
89
       (and (integerp (/ i j))
 
90
            (force (real/rationalp i))
 
91
            (integerp j)
 
92
            (force (not (equal 0 j))))
 
93
       (integerp i)))
 
94
     (:forward-chaining
 
95
      :corollary
 
96
      (implies
 
97
       (and (integerp (* (/ j) i))
 
98
            (force (real/rationalp i))
 
99
            (integerp j)
 
100
            (force (not (equal 0 j))))
 
101
       (integerp i)))))
 
102
 
 
103
  (defthm justify-floor-recursion-ext
 
104
    (implies
 
105
     (and (force (real/rationalp x))
 
106
          (force (real/rationalp y))
 
107
          (force (not (equal 0 y))))
 
108
     (and
 
109
      (implies
 
110
       (and (< 0 x)
 
111
            (< 1 y))
 
112
       (< (floor x y) x))
 
113
      (implies
 
114
       (and (< x -1)
 
115
            (<= 2 y))
 
116
       (< x (floor x y))))))
 
117
 
 
118
; From arithmetic-2
 
119
; Alternative: mod-x-y-=-x+y from IHS
 
120
  (defthm mod-x-y-=-x-+-y-ext
 
121
    (implies (and (rationalp x)
 
122
                  (rationalp y)
 
123
                (not (equal y 0))
 
124
                (if (< 0 y)
 
125
                    (and (< x 0)
 
126
                         (<= (- x) y))
 
127
                  (and (< 0 x)
 
128
                       (<= y (- x)))))
 
129
             (equal (mod x y) (+ x y)))
 
130
    :rule-classes ((:rewrite :backchain-limit-lst 0)
 
131
                   (:rewrite
 
132
                    :corollary
 
133
                    (implies (and (rationalp x)
 
134
                                  (rationalp y)
 
135
                                  (not (equal y 0)))
 
136
                             (equal (equal (mod x y) (+ x y))
 
137
                                    (if (< 0 y)
 
138
                                        (and (< x 0)
 
139
                                             (<= (- x) y))
 
140
                                      (and (< 0 x)
 
141
                                           (<= y (- x)))))))))
 
142
 
 
143
  (defthm mod-x-i*j
 
144
    (implies
 
145
     (and (> i 0)
 
146
          (> j 0)
 
147
          (force (integerp i))
 
148
          (force (integerp j))
 
149
          (force (real/rationalp x)))
 
150
     (equal (mod x (* i j))
 
151
            (+ (mod x i) (* i (mod (floor x i) j))))))
 
152
 
 
153
  (defthm floor-x+i*k-i*j
 
154
    (implies
 
155
     (and (force (real/rationalp x))
 
156
          (force (integerp i))
 
157
          (force (integerp j))
 
158
          (force (integerp k))
 
159
          (< 0 i)
 
160
          (< 0 j)
 
161
          (<= 0 x)
 
162
          (< x i))
 
163
     (equal (floor (+ x (* i k)) (* i j))
 
164
            (floor k j))))
 
165
 
 
166
  (defthm mod-x+i*k-i*j
 
167
    (implies
 
168
     (and (force (real/rationalp x))
 
169
          (force (integerp i))
 
170
          (force (integerp j))
 
171
          (force (integerp k))
 
172
          (< 0 i)
 
173
          (< 0 j)
 
174
          (<= 0 x)
 
175
          (< x i))
 
176
     (equal (mod (+ x (* i k)) (* i j))
 
177
            (+ x (* i (mod k j))))))
 
178
 
 
179
)
 
180
 
 
181
; An encapsulate for rtl/rel6/arithmetic.
 
182
(encapsulate
 
183
  ()
 
184
 
 
185
  (local (include-book "rtl/rel6/arithmetic/top" :dir :system))
 
186
 
 
187
  (defthm x*/y=1->x=y-ext
 
188
    (implies (and (rationalp x)
 
189
                  (rationalp y)
 
190
                  (not (equal x 0))
 
191
                  (not (equal y 0)))
 
192
             (equal (equal (* x (/ y)) 1)
 
193
                    (equal x y))))
 
194
 
 
195
  ; From arithmetc-2
 
196
  (defthm ratio-theory-of-1-f
 
197
    (implies (and (real/rationalp x)
 
198
                  (real/rationalp y)
 
199
                  (<= 0 x)
 
200
                  (< x (- y)))
 
201
             (and (<= (/ x y) 0)
 
202
                  (< -1 (/ x y))))
 
203
    :rule-classes :linear)
 
204
 
 
205
  ; From arithmetc-2
 
206
  (defthm x*y>1-positive-stronger
 
207
   (implies (and (or (and (< 1 x)
 
208
                          (<= 1 y))
 
209
                     (and (<= 1 x)
 
210
                          (< 1 y)))
 
211
                 (real/rationalp x)
 
212
                 (real/rationalp y))
 
213
    (< 1 (* x y)))
 
214
   :rule-classes (:linear :rewrite))
 
215
 
 
216
   ; From arithmetc-2
 
217
   (defthm nintegerp-/
 
218
     (implies (and (real/rationalp x)
 
219
                   (< 1 x))
 
220
              (not (integerp (/ x))))
 
221
   :rule-classes :type-prescription)
 
222
 
 
223
  (defthm mod-even
 
224
    (implies (rationalp x)
 
225
             (equal (integerp (* 1/2 (mod x 2)))
 
226
                    (integerp (* 1/2 x)))))
 
227
  
 
228
  (defthm mod-1-integerp
 
229
    (implies (case-split (acl2-numberp x))
 
230
             (equal (integerp (mod x 1))
 
231
                    (integerp x))))
 
232
 
 
233
  (defthm mod-prod
 
234
    (implies (and (rationalp m)
 
235
                  (rationalp n)
 
236
                  (rationalp k))
 
237
             (equal (mod (* k m) (* k n))
 
238
                    (* k (mod m n)))))
 
239
 
 
240
  (defthm mod-mult-n
 
241
    (equal (mod (* a n) n)
 
242
           (* n (mod a 1))))
 
243
 
 
244
  (defthm mod-when-y-is-complex-rationalp
 
245
    (implies (complex-rationalp y)
 
246
             (equal (mod x y)
 
247
                  (if (not (complex-rationalp x))
 
248
                      (fix x)
 
249
                    (if (not (rationalp (/ x y)))
 
250
                        x
 
251
                      (if (integerp (/ x y))
 
252
                          0 
 
253
                        (+ x (* -1 y (floor (* x (/ y)) 1)))
 
254
                        ))))))
 
255
 
 
256
  (defthm mod-when-y-is-an-inverse
 
257
    (implies (and (integerp (/ y))
 
258
                  (integerp x)
 
259
                  (case-split (< 0 y))
 
260
                  )
 
261
             (equal (mod x y)
 
262
                    0)))
 
263
 
 
264
  (defthm rationalp-mod-ext
 
265
    (implies (case-split (rationalp x))
 
266
             (rationalp (mod x y)))
 
267
    :rule-classes (:rewrite :type-prescription))
 
268
 
 
269
  (defthm mod-integerp-when-y-is-power-of-2
 
270
    (implies (integerp x)
 
271
             (integerp (mod x (expt 2 i))))
 
272
    :rule-classes (:rewrite :type-prescription))
 
273
 
 
274
  (defthm mod-of-mod
 
275
    (implies (and (case-split (natp k))
 
276
                  (case-split (natp n)))
 
277
             (equal (mod (mod x (* k n)) n)
 
278
                    (mod x n))))
 
279
 
 
280
  (defthm mod-sum
 
281
    (implies (and (rationalp a)
 
282
                  (rationalp b)
 
283
                  )
 
284
             (equal (mod (+ a (mod b n)) n)
 
285
                    (mod (+ a b) n))))
 
286
 
 
287
  (defthm mod-mod-sum
 
288
    (implies (and (rationalp a)
 
289
                  (rationalp b)
 
290
                  )
 
291
             (equal (mod (+ (mod a n) (mod b n)) n)
 
292
                    (mod (+ a b) n))))
 
293
 
 
294
  (defthm mod-diff
 
295
    (implies (and (case-split (rationalp a))
 
296
                  (case-split (rationalp b))
 
297
                  )
 
298
             (equal (mod (- a (mod b n)) n)
 
299
                    (mod (- a b) n))))
 
300
 
 
301
  (defthm mod-does-nothing
 
302
    (implies (and (< m n)
 
303
                  (<= 0 m)
 
304
                  (case-split (rationalp m)))
 
305
             (equal (mod m n)
 
306
                    m)))
 
307
 
 
308
   (defthm mod-bnd-2
 
309
     (implies (and (<= 0 m)
 
310
                   (case-split (rationalp m))
 
311
                   )
 
312
              (<= (mod m n) m))  
 
313
     :rule-classes :linear)
 
314
 
 
315
  (defthm mod-sums-cancel-1
 
316
    (implies (and (case-split (<= 0 y))
 
317
                  (case-split (rationalp k))
 
318
                  (case-split (rationalp y))
 
319
                  (case-split (rationalp x1))
 
320
                  (case-split (rationalp x2)))
 
321
             (equal (equal (mod (+ k x1) y) (mod (+ k x2) y))
 
322
                    (equal (mod x1 y) (mod x2 y)))))
 
323
 
 
324
; We write (mod (+ k x) y) rather than (mod (+ x k) y); otherwise it ;
 
325
; gets re-written by |(+ x y)|
 
326
  (defthm mod-sums-cancel-5-ext
 
327
    (implies (and (case-split (<= 0 y))
 
328
                  (case-split (rationalp k))
 
329
                  (case-split (rationalp y))
 
330
                  (case-split (rationalp x)))
 
331
             (equal (equal (mod k y) (mod (+ k x) y))
 
332
                    (equal 0 (mod x y)))))
 
333
 
 
334
  (defthm mod-mod-2-thm
 
335
    (implies (and (<= y1 y2)
 
336
                  (case-split (< 0 y1))
 
337
                  (case-split (acl2-numberp x))
 
338
                  (case-split (rationalp y1))
 
339
                  (case-split (rationalp y2))
 
340
                  (case-split (not (equal y1 0))))
 
341
             (equal (mod (mod x y1) y2)
 
342
                    (mod x y1))))
 
343
 
 
344
  (defthm mod-mod-2-not-equal-ext
 
345
    (implies (acl2-numberp m)
 
346
             (not (equal (mod m 2) (mod (1+ m) 2))))
 
347
   :hints (("Goal" :use ((:instance mod-mod-2-not-equal)))))
 
348
 
 
349
  (defthm mod-quotient-integerp
 
350
    (implies (and (integerp (* y k))
 
351
                  (rationalp x)
 
352
                  (rationalp y)
 
353
                  (rationalp k))
 
354
             (equal (integerp (* k (mod x y)))
 
355
                    (integerp (* k x)))))
 
356
 
 
357
  (defthm mod-1-sum-integer
 
358
    (implies (and (rationalp x)
 
359
                  (rationalp y))
 
360
             (equal (integerp (+ x (mod y 1)))
 
361
                    (integerp (+ x y)))))
 
362
 
 
363
  (defthm mod-mod-e
 
364
    (implies (and (integerp (/ y1 y2))
 
365
                  (case-split (not (equal y2 0)))
 
366
                  (case-split (rationalp y1))
 
367
                  (case-split (rationalp y2)))
 
368
             (equal (mod (mod x y1) y2)
 
369
                    (mod x y2))))
 
370
 
 
371
  (defthm mod-sum-elim-second
 
372
    (implies (and (case-split (not (complex-rationalp x1)))
 
373
                  (case-split (not (complex-rationalp x2))) 
 
374
                  )
 
375
             (equal (mod (+ x1 (mod x2 y)) y)
 
376
                    (mod (+ x1 x2) y))))
 
377
 
 
378
  (defthm mod-sum-elim-second-gen
 
379
    (implies (and (integerp (/ y2 y))
 
380
                  (case-split (not (complex-rationalp x1)))
 
381
                  (case-split (not (complex-rationalp x2))) 
 
382
                  (case-split (not (equal y 0)))
 
383
                  (case-split (rationalp y))
 
384
                  )
 
385
             (equal (mod (+ x1 (mod x2 y2)) y)
 
386
                    (mod (+ x1 x2) y))))
 
387
 
 
388
  (defthm mod-sum-elim-both
 
389
    (implies (and (case-split (not (complex-rationalp a)))
 
390
                  (case-split (not (complex-rationalp b)))
 
391
                  )
 
392
             (equal (mod (+ (mod a y) (mod b y)) y)
 
393
                    (mod (+ a b) y))))
 
394
 
 
395
  (defthm mod-drop-irrelevant-first-term
 
396
    (implies (and (integerp (* k (/ y)))
 
397
                  (case-split (not (equal y 0)))
 
398
                  (case-split (rationalp y))
 
399
                  (case-split (not (complex-rationalp x)))
 
400
                  )
 
401
             (equal (mod (+ k x) y)
 
402
                    (mod x y))))
 
403
 
 
404
  (defthm mod-mult-ext
 
405
    (implies (and (integerp a)
 
406
                  (case-split (not (complex-rationalp x)))
 
407
                  (case-split (not (complex-rationalp y)))
 
408
                  )
 
409
             (equal (mod (+ x (* a y)) y)
 
410
                    (mod x y))))
 
411
 
 
412
  (defthm mod-complex-rationalp-rewrite
 
413
    (implies (case-split (rationalp y))
 
414
             (equal (complex-rationalp (mod x y))
 
415
                    (complex-rationalp x))))
 
416
  
 
417
  (defthm mod-upper-bound-less-tight-rewrite
 
418
    (implies (and (case-split (< 0 y))
 
419
                  (case-split (not (complex-rationalp x)))
 
420
                  (case-split (not (complex-rationalp y)))
 
421
                  )
 
422
             (<= (mod x y) y)))
 
423
 
 
424
  (defthm mod-upper-bound-3
 
425
    (implies (and (<= y z)
 
426
                  (case-split (< 0 y))
 
427
                  (case-split (not (complex-rationalp x)))
 
428
                  (case-split (not (complex-rationalp y)))
 
429
                  )
 
430
             (< (mod x y) z)))
 
431
 
 
432
  (defthm mod-non-negative-linear
 
433
    (implies (and (case-split (< 0 y))
 
434
                  (case-split (not (complex-rationalp x)))
 
435
                  (case-split (not (complex-rationalp y)))
 
436
                  )
 
437
             (<= 0 (mod x y)))
 
438
    :rule-classes ((:linear :trigger-terms ((mod x y)))))
 
439
 
 
440
  (defthm mod-integerp-2
 
441
    (implies (and (integerp y)
 
442
                  (case-split (acl2-numberp x)))
 
443
             (equal (integerp (mod x y))
 
444
                    (integerp x))))
 
445
 
 
446
  (defthm mod-rational-when-y-is-rational-rewrite
 
447
    (implies (and (rationalp y)
 
448
                  (case-split (acl2-numberp x)))
 
449
             (equal (rationalp (mod x y))
 
450
                    (rationalp x))))
 
451
 
 
452
  (defthm mod-force-equal-ext ; rule-classes nil
 
453
    (implies (and (< (abs (- a b)) n)
 
454
                  (rationalp a)
 
455
                  (rationalp b)
 
456
                  (integerp n))
 
457
             (iff (equal (mod a n) (mod b n))
 
458
                  (equal a b)))
 
459
    :hints (("Goal" :use ((:instance mod-force-equal)))))
 
460
 
 
461
  (defthm mod-equal-int-ext ; rule-classes nil
 
462
    (implies (and (equal (mod a n) (mod b n))
 
463
                  (rationalp a)
 
464
                  (rationalp b))
 
465
             ;(integerp (/ (- a b) n)))
 
466
             ; arithmetic-3 rewrites the above line to this one
 
467
             (integerp (+ (* a (/ n)) (- (* b (/ n))))))
 
468
    :hints (("Goal" :use ((:instance mod-equal-int)))))
 
469
 
 
470
  (defthm mod-equal-int-reverse-ext ; rule-classes nil
 
471
    (implies (and ; (integerp (/ (- a b) n))
 
472
                  ; arithmetic-3 rewrites the above line to this one
 
473
                  (integerp (+ (* a (/ n)) (- (* b (/ n)))))
 
474
                  (rationalp a)
 
475
                  (rationalp b)
 
476
                  (rationalp n)
 
477
                  (< 0 n))
 
478
             (equal (mod a n) (mod b n)))
 
479
    :hints (("Goal" :use ((:instance mod-equal-int-reverse)))))
 
480
 
 
481
  (defthm even-odd-5
 
482
    (implies (and (rationalp x)
 
483
                  (integerp (* 1/2 x)))
 
484
             (and (integerp (- x 1))
 
485
                  (not (integerp (* 1/2 (- x 1)))))))
 
486
 
 
487
  (defthm expt-2-is-not-odd
 
488
    (implies (and (evenp x)
 
489
                  (< 0 i)
 
490
                  (integerp i))
 
491
             (equal (equal (expt 2 i)
 
492
                           (+ 1 x))
 
493
                    nil)))
 
494
 
 
495
  (defthm expt2-integer
 
496
    (implies (case-split (integerp i))
 
497
             (equal (integerp (expt 2 i))
 
498
                    (<= 0 i))))
 
499
 
 
500
  (defthm expt-bigger-than-i
 
501
    (implies (integerp i)
 
502
             (< i (expt 2 i))))
 
503
 
 
504
  (defthm expt2-inverse-integer
 
505
    (implies (case-split (integerp i))
 
506
             (equal (integerp (/ (expt 2 i)))
 
507
                    (<= i 0))))
 
508
 
 
509
  (defthm expt2-1-to-1
 
510
    (implies (and (integerp i1)
 
511
                  (integerp i2))
 
512
             (equal (equal (expt 2 i1) (expt 2 i2))
 
513
                    (equal i1 i2))))
 
514
 
 
515
  (defthm expt-between-one-and-two
 
516
    (implies (and (<= 1 (expt 2 i))
 
517
                  (< (expt 2 i) 2))
 
518
             (equal (expt 2 i) 1)))
 
519
 
 
520
  (defthm expt-prod-integer-3-terms-2-ext
 
521
    (implies (and (<= (+ j l) i)
 
522
                  (integerp i)
 
523
                  (integerp j)
 
524
                  (integerp l)
 
525
                  )
 
526
             (integerp (* (expt 2 i) (/ (expt 2 j)) (/ (expt 2 l))))))
 
527
 
 
528
  (defthm complex-rationalp-prod
 
529
    (implies (and (rationalp k)
 
530
                  (case-split (not (equal k 0)))
 
531
                  )
 
532
             (and (equal (complex-rationalp (* k x))
 
533
                         (complex-rationalp x))
 
534
                  (equal (complex-rationalp (* x k))
 
535
                         (complex-rationalp x)))))
 
536
 
 
537
  (defthm product-greater-than-zero-ext
 
538
    (implies (or (case-split (not (complex-rationalp x)))
 
539
                 (case-split (not (complex-rationalp y))))
 
540
             (equal (< 0 (* x y))
 
541
                    (or (and (< 0 x) (< 0 y))
 
542
                        (and (< y 0) (< x 0))))))
 
543
 
 
544
  (defthm product-less-than-zero
 
545
    (implies (case-split (or (not (complex-rationalp x))
 
546
                             (not (complex-rationalp y))))
 
547
             (equal (< (* x y) 0)
 
548
                    (if (< x 0)
 
549
                        (< 0 y)
 
550
                      (if (equal 0 x)
 
551
                          nil
 
552
                        (if (not (acl2-numberp x))
 
553
                            nil
 
554
                          (< y 0)))))))
 
555
 
 
556
   (defthm quotient-not-integerp
 
557
     (implies (and (< i j)
 
558
                   (<= 0 i)
 
559
                   (<= 0 j)
 
560
                   (case-split (< 0 i))
 
561
                   (case-split (< 0 j))
 
562
                   (case-split (rationalp j)))
 
563
              (not (integerp (/ i j)))))
 
564
 
 
565
   (defthm rationalp-product-when-one-arg-is-rational
 
566
     (implies (and (rationalp x)
 
567
                   (case-split (not (equal x 0)))
 
568
                   (case-split (acl2-numberp y))
 
569
                   )
 
570
              (and (equal (rationalp (* x y))
 
571
                          (rationalp y))
 
572
                   (equal (rationalp (* y x))
 
573
                          (rationalp y)))))
 
574
 
 
575
   (defthm rationalp-sum-when-one-arg-is-rational
 
576
     (implies (and (rationalp x)
 
577
                   (case-split (acl2-numberp y)))
 
578
              (and (equal (rationalp (+ x y))
 
579
                          (rationalp y))
 
580
                   (equal (rationalp (+ y x))
 
581
                          (rationalp y)))))
 
582
   
 
583
   (defthm rationalp-unary-divide
 
584
     (implies (case-split (acl2-numberp x))
 
585
              (equal (rationalp (/ x))
 
586
                     (rationalp x))))
 
587
 
 
588
   (defthm complex-rationalp-+-when-second-term-is-not-complex
 
589
     (implies (not (complex-rationalp y))
 
590
              (equal (complex-rationalp (+ x y))
 
591
                     (complex-rationalp x))))
 
592
 
 
593
   (defthm complex-rationalp-+-when-first-term-is-not-complex
 
594
     (implies (not (complex-rationalp x))
 
595
              (equal (complex-rationalp (+ x y))
 
596
                     (complex-rationalp y))))
 
597
 
 
598
   (defthm fraction-less-than-1
 
599
     (implies (and (< (abs m) (abs n))
 
600
                   (rationalp m)
 
601
                   (rationalp n))
 
602
              (<= (* m (/ n)) 1)))
 
603
 
 
604
   ; Floor theorems
 
605
   (defthm floor-with-i-not-rational
 
606
     (implies (not (rationalp i))
 
607
              (equal (floor i j)
 
608
                     (if (and (complex-rationalp i) (complex-rationalp j) (rationalp (/ i j)))
 
609
                         (floor (/ i j) 1)
 
610
                       0))))
 
611
 
 
612
   (defthm floor-with-j-not-rational
 
613
     (implies (not (rationalp j))
 
614
              (equal (floor i j)
 
615
                     (if (and (complex-rationalp i) (complex-rationalp j) (rationalp (/ i j)))
 
616
                         (floor (/ i j) 1)
 
617
                       0))))
 
618
   
 
619
   (defthm floor-of-rational-and-complex
 
620
     (implies (and (rationalp i)
 
621
                   (not (rationalp j))
 
622
                   (case-split (acl2-numberp j)))
 
623
              (and (equal (floor i j)
 
624
                          0)
 
625
                   (equal (floor j i)
 
626
                          0))))
 
627
   
 
628
   (defthm floor-when-arg-quotient-isnt-rational
 
629
     (implies (not (rationalp (* i (/ j))))
 
630
              (equal (floor i j) 0)))
 
631
 
 
632
   (defthm floor-non-negative-integerp-type-prescription
 
633
     (implies (and (<= 0 i)
 
634
                   (<= 0 j)
 
635
                   (case-split (not (complex-rationalp j)))
 
636
                   )
 
637
              (and (<= 0 (floor i j))
 
638
                   (integerp (floor i j))))
 
639
     :rule-classes (:type-prescription))
 
640
 
 
641
   (defthm floor-non-negative
 
642
     (implies (and (<= 0 i)
 
643
                   (<= 0 j)
 
644
                   (case-split (not (complex-rationalp i)))
 
645
                   )
 
646
              (<= 0 (floor i j))))
 
647
 
 
648
   (defthm floor-equal-i-over-j-rewrite
 
649
     (implies (and (case-split (not (equal j 0)))
 
650
                   (case-split (rationalp i))
 
651
                   (case-split (rationalp j))
 
652
                   )
 
653
              (equal (equal (* j (floor i j)) i)
 
654
                     (integerp (* i (/ j))))))
 
655
 
 
656
   (defthm integerp-sum-of-odds-over-2
 
657
     (implies (and (rationalp x)
 
658
                   (rationalp y)
 
659
                   (integerp (* 2 x))
 
660
                   (not (integerp x))
 
661
                 )
 
662
              (equal (integerp (+ x y))
 
663
                     (and (integerp (* 2 y))
 
664
                          (not (integerp y))
 
665
                          ))))
 
666
   
 
667
  (defthm mod-bnd-3
 
668
    (implies (and (< m (+ (* a n) r))
 
669
                  (<= (* a n) m)
 
670
                  (integerp a)
 
671
                  (case-split (rationalp m))
 
672
                  (case-split (rationalp n))
 
673
                  )
 
674
             (< (mod m n) r))
 
675
  :rule-classes :linear)
 
676
 
 
677
  ; rule-classes nil
 
678
  (defthm mod-force-ext
 
679
    (implies (and (<= (* a n) m)
 
680
                  (< m (* (1+ a) n))
 
681
                  (integerp a)
 
682
                  (rationalp m)
 
683
                  (rationalp n)
 
684
                  )
 
685
             (= (mod m n) (- m (* a n))))
 
686
    :hints (("Goal" :use ((:instance mod-force)))))
 
687
 
 
688
  (defthm mod-equal-0-ext
 
689
    (implies (and (case-split (rationalp y))
 
690
                  (case-split (not (equal y 0))))
 
691
             (equal (equal (mod x y) 0)
 
692
                    (integerp (* (/ y) x))))
 
693
    :hints (("Goal" :in-theory (enable mod-equal-0))))
 
694
 
 
695
  (defthm mod-integerp-2-2
 
696
    (implies (and (integerp y)
 
697
                  (integerp x))
 
698
             (integerp (mod x (/ y)))))
 
699
 
 
700
  (local (include-book "rtl/rel6/arithmetic/extra-rules" :dir :system)) ; for exp-invert
 
701
  ; rule-classes nil
 
702
  (defthm exp-invert-ext
 
703
    (implies (and (integerp n)
 
704
                  (<= n -1))
 
705
             (<= (/ (- 1 (expt 2 n)))
 
706
                 (1+ (expt 2 (1+ n)))))
 
707
    :hints (("Goal" :use ((:instance exp-invert)))))
 
708
 
 
709
  (defthm mod-integerp-when-y-is-an-inverse
 
710
    (implies (and (integerp (/ y))
 
711
                  (integerp x))
 
712
             (integerp (mod x y))))
 
713
 
 
714
#| ; expensive: more than doubles execution time!
 
715
  (defthm x-2xx-ext
 
716
    (implies (and (rationalp x)
 
717
                  (integerp (* 2 x x)))
 
718
             (integerp x))
 
719
    :hints (("Goal" :use ((:instance x-2xx)))))
 
720
|#
 
721
 
 
722
)
 
723
 
 
724
(encapsulate
 
725
  ()
 
726
 
 
727
  (local (include-book "arithmetic-2/meta/expt" :dir :system))
 
728
  (local (include-book "arithmetic-2/meta/integerp" :dir :system))
 
729
  
 
730
  (defthm expt-1-linear-b
 
731
    (implies (and (<= 0 x)
 
732
                  (< x 1)
 
733
                  (< 0 i)
 
734
                  (real/rationalp x)
 
735
                  (integerp i))
 
736
             (< (expt x i) 1))
 
737
    :rule-classes :linear)
 
738
 
 
739
  (defthm expt-1-linear-d
 
740
    (implies (and (<= 0 x)
 
741
                  (<= x 1)
 
742
                  (<= 0 i)
 
743
                  (real/rationalp x)
 
744
                  (integerp i))
 
745
             (<= (expt x i) 1))
 
746
    :rule-classes :linear)
 
747
 
 
748
  (defthm expt-1-linear-h
 
749
    (implies (and (< 0 x)
 
750
                  (<= x 1)
 
751
                  (< i 0)
 
752
                  (real/rationalp x)
 
753
                  (integerp i))
 
754
             (<= 1 (expt x i)))
 
755
    :rule-classes :linear)
 
756
 
 
757
  (defthm nintegerp-expt
 
758
    (implies (and (real/rationalp x)
 
759
                  (< 1 x)
 
760
                  (integerp n)
 
761
                  (< n 0))
 
762
             (not (integerp (expt x n))))
 
763
    :hints (("Goal" :use nintegerp-expt-helper))
 
764
    :rule-classes :type-prescription)
 
765
 
 
766
)
 
767
 
 
768
#|
 
769
(encapsulate
 
770
  ()
 
771
 
 
772
  ; Expensive: adds ~9 seconds to test suite. Gain: 1.
 
773
  (local (include-book "arithmetic-3/bind-free/top" :dir :system))
 
774
  (local (include-book "arithmetic-3/floor-mod/floor-mod" :dir :system))
 
775
  
 
776
  (defthm mod-x-y-=-x---y
 
777
    (implies (and (and (rationalp x)
 
778
                       (rationalp y)
 
779
                       (not (equal y 0)))
 
780
                  (if (< 0 y)
 
781
                      (and (<= y x)
 
782
                           (< x (* 2 y)))
 
783
                    (and (<= x y)
 
784
                         (< (* 2 y) x))))
 
785
             (equal (mod x y) (- x y)))
 
786
    :hints ((nonlinearp-default-hint stable-under-simplificationp hist pspv))
 
787
    :rule-classes ((:rewrite :backchain-limit-lst 0)
 
788
                   (:rewrite
 
789
                    :corollary
 
790
                    (implies (and (rationalp x)
 
791
                                  (rationalp y)
 
792
                                  (not (equal y 0)))
 
793
                             (equal (equal (mod x y) (- x y))
 
794
                                    (if (< 0 y)
 
795
                                        (and (<= y x)
 
796
                                             (< x (* 2 y)))
 
797
                                      (and (<= x y)
 
798
                                           (< (* 2 y) x))))))))
 
799
)
 
800
|#