← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/rtl/rel6/lib/arith.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/lib/arith.lisp
 
1
; This file is based on the old "fp book", which was initially created by J
 
2
; Moore and Matt Kaufmann in 1995 in support of their proof of the AMD-K5
 
3
; division code.    Here, we have moved
 
4
; non-local in-theory events to the end.  All events should be redundant, so we
 
5
; have deleted all local in-theory events and added (local (in-theory nil)) to
 
6
; the beginning.
 
7
 
 
8
(in-package "ACL2")
 
9
 
 
10
(set-enforce-redundancy t)
 
11
 
 
12
(local (include-book "../arithmetic/fp"))
 
13
(local (include-book "../arithmetic/fp2"))
 
14
(local (include-book "../arithmetic/fl"))
 
15
(local (include-book "../arithmetic/expt"))
 
16
(local (include-book "../arithmetic/expo"))
 
17
(local (include-book "../arithmetic/extra-rules"))
 
18
(local (include-book "../support/support/ash"))
 
19
 
 
20
;; (local (include-book "../support/top/top"))
 
21
 
 
22
;; these already have lib1.delta1's
 
23
;; arith.lisp!!  deftheory??? 
 
24
;; Why I can't do that?? 
 
25
 
 
26
 
 
27
(set-inhibit-warnings "theory") ; avoid warning in the next event
 
28
(local (in-theory nil))
 
29
;(set-inhibit-warnings) ; restore theory warnings (optional)
 
30
 
 
31
(defthm a1 (equal (+ x (+ y z)) (+ y (+ x z))))
 
32
(defthm a2 (equal (- x) (* -1 x)))
 
33
 
 
34
(defthm a3
 
35
  (and
 
36
   (implies
 
37
    (syntaxp (and (quotep c1) (quotep c2)))
 
38
    (and (equal (+ (* c1 x) (* c2 x)) (* (+ c1 c2) x))
 
39
         (equal (+ (* c1 x) (+ (* c2 x) y)) (+ (* (+ c1 c2) x) y))))
 
40
   (implies
 
41
    (syntaxp (quotep c2))
 
42
    (and (equal (+ x (* c2 x)) (* (+ 1 c2) x))
 
43
         (equal (+ x (+ (* c2 x) y1)) (+ (* (+ 1 c2) x) y1))
 
44
         (equal (+ x (+ y1 (* c2 x))) (+ (* (+ 1 c2) x) y1))
 
45
         (equal (+ x (+ y1 (+ (* c2 x) y2))) (+ (* (+ 1 c2) x) y1 y2))
 
46
         (equal (+ x (+ y1 (+ y2 (* c2 x)))) (+ (* (+ 1 c2) x) y1 y2))
 
47
         (equal (+ x (+ y1 (+ y2 (+ y3 (* c2 x)))))
 
48
                (+ (* (+ 1 c2) x) y1 y2 y3))
 
49
         (equal (+ x (+ y1 (+ y2 (+ (* c2 x) y3))))
 
50
                (+ (* (+ 1 c2) x) y1 y2 y3))))
 
51
   (and (equal (+ x x) (* 2 x))
 
52
        (equal (+ x (+ x y1)) (+ (* 2 x) y1)))))
 
53
(defthm a4
 
54
  (implies (syntaxp (and (quotep c1) (quotep c2)))
 
55
           (equal (+ c1 (+ c2 y1)) (+ (+ c1 c2) y1))))
 
56
(defthm a5
 
57
  (implies (syntaxp (and (quotep c1) (quotep c2)))
 
58
           (equal (* c1 (* c2 y1)) (* (* c1 c2) y1))))
 
59
 
 
60
 
 
61
 
 
62
 
 
63
 
 
64
(defthm a6
 
65
  (equal (/ (/ x)) (fix x)))
 
66
(defthm a7
 
67
  (equal (/ (* x y)) (* (/ x) (/ y))))
 
68
 
 
69
;replaced force with case-split
 
70
(defthm a8
 
71
  (implies (and (case-split (acl2-numberp x))
 
72
                (case-split (not (equal x 0))))
 
73
           (and (equal (* x (* (/ x) y)) (fix y))
 
74
                (equal (* x (/ x)) 1))))
 
75
 
 
76
(defthm a9
 
77
  (and (equal (* 0 x) 0)
 
78
       (equal (* x (* y z)) (* y (* x z)))
 
79
       (equal (* x (+ y z)) (+ (* x y) (* x z)))
 
80
       (equal (* (+ y z) x) (+ (* y x) (* z x)))))
 
81
 
 
82
(defun fl (x)
 
83
  (declare (xargs :guard (real/rationalp x)))
 
84
  (floor x 1))
 
85
 
 
86
 
 
87
 
 
88
(defthm a10
 
89
  (and (implies (integerp i) (equal (fl i) i))
 
90
       (implies (and (integerp i)
 
91
                     (case-split (rationalp x1)) ;can actually drop this
 
92
                     )
 
93
                (and (equal (fl (+ i x1)) (+ i (fl x1)))
 
94
                     (equal (fl (+ x1 i)) (+ i (fl x1)))))
 
95
       (implies (and (integerp i)
 
96
                     (case-split (rationalp x1))
 
97
                     (case-split (rationalp x2)))
 
98
                (and (equal (fl (+ x1 (+ i x2))) (+ i (fl (+ x1 x2))))
 
99
                     (equal (fl (+ x1 (+ x2 i))) (+ i (fl (+ x1 x2))))))
 
100
       (implies (and (integerp i)
 
101
                     (case-split (rationalp x1))
 
102
                     (case-split (rationalp x2))
 
103
                     (case-split (rationalp x3)))
 
104
                (and (equal (fl (+ x1 (+ x2 (+ i x3))))
 
105
                            (+ i (fl (+ x1 x2 x3))))
 
106
                     (equal (fl (+ x1 (+ x2 (+ x3 i))))
 
107
                            (+ i (fl (+ x1 x2 x3))))))
 
108
       (implies (and (integerp i)
 
109
                     (case-split (rationalp x1))
 
110
                     (case-split (rationalp x2))
 
111
                     (case-split (rationalp x3))
 
112
                     (case-split (rationalp x4)))
 
113
                (and (equal (fl (+ x1 (+ x2 (+ x3 (+ i x4)))))
 
114
                            (+ i (fl (+ x1 x2 x3 x4))))
 
115
                     (equal (fl (+ x1 (+ x2 (+ x3 (+ x4 i)))))
 
116
                            (+ i (fl (+ x1 x2 x3 x4))))))))
 
117
 
 
118
(defthm a12
 
119
  (implies (and (integerp i)
 
120
                (integerp j)
 
121
                (< 1 j)
 
122
                (< j i))
 
123
           (and (< (acl2-count (fl (/ i j))) (acl2-count i))
 
124
                (< (acl2-count (fl (* (/ j) i))) (acl2-count i))))
 
125
  :rule-classes :linear)
 
126
 
 
127
 
 
128
;replaced force with case-split                
 
129
;later, drop the hyp completely
 
130
(defthm a13
 
131
  (implies (case-split (rationalp x)) ;drop!
 
132
           (and (< (1- x) (fl x))
 
133
                (<= (fl x) x)))
 
134
  :rule-classes :linear)
 
135
 
 
136
(defthm a14
 
137
  (and
 
138
   (implies (and (integerp i)
 
139
                 (<= 0 i)
 
140
                 (<= 0 j))
 
141
            (and (integerp (expt i j))
 
142
                 (<= 0 (expt i j))))
 
143
   (implies (and (rationalp i)
 
144
                 (not (equal i 0)))
 
145
            (not (equal (expt i j) 0))))
 
146
  :rule-classes
 
147
  ((:type-prescription
 
148
    :corollary
 
149
    (implies (and (integerp i)
 
150
                  (<= 0 i)
 
151
                  (<= 0 j))
 
152
             (and (integerp (expt i j))
 
153
                  (<= 0 (expt i j)))))
 
154
   (:type-prescription
 
155
    :corollary
 
156
    (implies (and (rationalp i)
 
157
                  (not (equal i 0)))
 
158
             (not (equal (expt i j) 0))))))
 
159
 
 
160
(defthm a15
 
161
  (implies (and (rationalp i)
 
162
                (not (equal i 0))
 
163
                (integerp j1)
 
164
                (integerp j2))
 
165
           (and (equal (* (expt i j1) (expt i j2))
 
166
                       (expt i (+ j1 j2)))
 
167
                (equal (* (expt i j1) (* (expt i j2) x))
 
168
                       (* (expt i (+ j1 j2)) x)))))
 
169
(defthm a16
 
170
  (equal (expt (* a b) i)
 
171
         (* (expt a i) (expt b i))))
 
172
 
 
173
(defthm /-weakly-monotonic
 
174
  (implies (and (<= y y+)
 
175
                (< 0 y)
 
176
                (case-split (rationalp y))
 
177
                (case-split (rationalp y+))
 
178
                )
 
179
           (<= (/ y+) (/ y)))
 
180
  :rule-classes
 
181
  ((:forward-chaining :trigger-terms ((/ y+) (/ y))) :linear))
 
182
 
 
183
(defthm /-strongly-monotonic
 
184
  (implies (and (< y y+)
 
185
                (< 0 y)
 
186
                (case-split (rationalp y))
 
187
                (case-split (rationalp y+))
 
188
                )
 
189
           (< (/ y+) (/ y)))
 
190
  :rule-classes
 
191
  ((:forward-chaining :trigger-terms ((/ y+) (/ y))) :linear))
 
192
         
 
193
(defthm *-weakly-monotonic
 
194
  (implies (and (<= y y+)
 
195
                (<= 0 x)
 
196
                (case-split (rationalp x)) ; This does not hold if x, y, and z are complex!
 
197
                )
 
198
           (<= (* x y) (* x y+)))
 
199
  :rule-classes
 
200
  ((:forward-chaining :trigger-terms ((* x y) (* x y+)))
 
201
   (:linear)
 
202
   (:forward-chaining
 
203
    :trigger-terms ((* y x) (* y+ x))
 
204
    :corollary
 
205
    (implies (and (<= y y+)
 
206
                  (<= 0 x)
 
207
                  (case-split (rationalp x))
 
208
                  )
 
209
             (<= (* y x) (* y+ x))))
 
210
   (:linear
 
211
    :corollary
 
212
    (implies (and (<= y y+)
 
213
                  (<= 0 x)
 
214
                  (case-split (rationalp x))
 
215
                  )
 
216
             (<= (* y x) (* y+ x))))))
 
217
 
 
218
#| Here is the complex counterexample to which we alluded above.
 
219
 
 
220
(let ((y  #c(1 -1))
 
221
      (y+ #c(1 1))
 
222
      (x  #c(1 1)))
 
223
    (implies (and (<= y y+)
 
224
                  (<= 0 x))
 
225
             (<= (* x y) (* x y+))))
 
226
|#
 
227
 
 
228
(defthm *-strongly-monotonic
 
229
  (implies (and (< y y+)
 
230
                (< 0 x)
 
231
                (case-split (rationalp x))
 
232
                )
 
233
           (< (* x y) (* x y+)))
 
234
  :rule-classes
 
235
  ((:forward-chaining :trigger-terms ((* x y) (* x y+)))
 
236
   (:linear)
 
237
   (:forward-chaining
 
238
    :trigger-terms ((* y x) (* y+ x))
 
239
    :corollary
 
240
    (implies (and (< y y+)
 
241
                  (< 0 x)
 
242
                  (case-split (rationalp x))
 
243
                  )
 
244
             (< (* y x) (* y+ x))))
 
245
   (:linear
 
246
    :corollary
 
247
    (implies (and (< y y+)
 
248
                  (< 0 x)
 
249
                  (case-split (rationalp x))
 
250
                  )
 
251
             (< (* y x) (* y+ x))))))
 
252
 
 
253
(defthm *-weakly-monotonic-negative-multiplier
 
254
  (implies (and (<= y y+)
 
255
               (< x 0)
 
256
               (case-split (rationalp x))
 
257
               )
 
258
           (<= (* x y+) (* x y)))
 
259
  :rule-classes
 
260
  ((:forward-chaining :trigger-terms ((* x y) (* x y+)))
 
261
   (:linear)
 
262
   (:forward-chaining
 
263
    :trigger-terms ((* y x) (* y+ x))
 
264
    :corollary
 
265
    (implies (and (<= y y+)
 
266
                  (< x 0)
 
267
                  (case-split (rationalp x))
 
268
                  )
 
269
             (<= (* y+ x) (* y x))))
 
270
   (:linear
 
271
    :corollary
 
272
    (implies (and (<= y y+)
 
273
                  (< x 0)
 
274
                  (case-split (rationalp x))
 
275
                  )
 
276
             (<= (* y+ x) (* y x))))))
 
277
 
 
278
(defthm *-strongly-monotonic-negative-multiplier
 
279
  (implies (and (< y y+)
 
280
                (< x 0)
 
281
                (case-split (rationalp x))
 
282
                )
 
283
           (< (* x y+) (* x y)))
 
284
  :rule-classes
 
285
  ((:forward-chaining :trigger-terms ((* x y) (* x y+)))
 
286
   (:linear)
 
287
   (:forward-chaining
 
288
    :trigger-terms ((* y x) (* y+ x))
 
289
    :corollary
 
290
    (implies (and (< y y+)
 
291
                  (< x 0)
 
292
                  (case-split (rationalp x))
 
293
                  )
 
294
             (< (* y+ x) (* y x))))
 
295
   (:linear
 
296
    :corollary
 
297
    (implies (and (< y y+)
 
298
                  (< x 0)
 
299
                  (case-split (rationalp x))
 
300
                  )
 
301
             (< (* y+ x) (* y x))))))
 
302
 
 
303
(defthm fl-weakly-monotonic
 
304
  (implies (and (<= y y+)
 
305
                (case-split (rationalp y)) ;drop?
 
306
                (case-split (rationalp y+)) ;drop?
 
307
                )
 
308
           (<= (fl y) (fl y+)))
 
309
  :rule-classes ((:forward-chaining :trigger-terms ((fl y) (fl y+)))
 
310
                 (:linear)
 
311
                 (:forward-chaining
 
312
                  :trigger-terms ((fl y) (fl y+))
 
313
                  :corollary (implies (and (< y y+)
 
314
                                           (case-split (rationalp y))
 
315
                                           (case-split (rationalp y+)))
 
316
                                      (<= (fl y) (fl y+))))
 
317
                 (:linear
 
318
                  :corollary (implies (and (< y y+)
 
319
                                           (case-split (rationalp y))
 
320
                                           (case-split (rationalp y+)))
 
321
                                      (<= (fl y) (fl y+))))))
 
322
 
 
323
(deftheory arith-fc-monotonicity
 
324
  '((:forward-chaining /-weakly-monotonic)
 
325
    (:forward-chaining /-strongly-monotonic)
 
326
    (:forward-chaining *-weakly-monotonic . 1)
 
327
    (:forward-chaining *-weakly-monotonic . 2)
 
328
    (:forward-chaining *-strongly-monotonic . 1)
 
329
    (:forward-chaining *-strongly-monotonic . 2)
 
330
    (:forward-chaining *-weakly-monotonic-negative-multiplier . 1)
 
331
    (:forward-chaining *-weakly-monotonic-negative-multiplier . 2)
 
332
    (:forward-chaining *-strongly-monotonic-negative-multiplier . 1)
 
333
    (:forward-chaining *-strongly-monotonic-negative-multiplier . 2)
 
334
    (:forward-chaining fl-weakly-monotonic . 1)
 
335
    (:forward-chaining fl-weakly-monotonic . 2)
 
336
    ))
 
337
 
 
338
; We now prove a bunch of bounds theorems for *.  We are concerned with bounding the
 
339
; product of a and b given intervals for a and b.  We consider three kinds of intervals.
 
340
; We discuss only the a case.
 
341
 
 
342
; abs intervals mean (abs a) < amax or -amax < a < amax, where amax is positive.
 
343
 
 
344
; nonneg-open intervals mean 0<=a<amax.
 
345
 
 
346
; nonneg-closed intervals mean 0<=a<=amax, where amax is positive.
 
347
 
 
348
; We now prove theorems with names like abs*nonneg-open, etc. characterizing
 
349
; the product of two elements from two such intervals.  All of these theorems
 
350
; are made with :rule-classes nil because I don't know how to control their
 
351
; use.
 
352
 
 
353
; This lemma is for lookup * d and lookup * away.  We don't need to consider 0
 
354
; < b for the d case because we have 0 < 1 <= d and the conclusion of the new
 
355
; lemma would be no different.
 
356
 
 
357
(defthm abs*nonneg-open
 
358
  (implies (and (rationalp a)
 
359
                (rationalp amax)
 
360
                (rationalp b)
 
361
                (rationalp bmax)
 
362
                (< (- amax) a)
 
363
                (<= a amax) ; (< a amax) is all we'll ever use, I bet.
 
364
                (< 0 amax)
 
365
                (<= 0 b)
 
366
                (< b bmax))
 
367
           (and (< (- (* amax bmax)) (* a b))
 
368
                (< (* a b) (* amax bmax))))
 
369
  :rule-classes nil)
 
370
 
 
371
 
 
372
 
 
373
(defthm abs*nonneg-closed
 
374
  (implies (and (rationalp a)
 
375
                (rationalp amax)
 
376
                (rationalp b)
 
377
                (rationalp bmax)
 
378
                (< (- amax) a)
 
379
                (< a amax)
 
380
                (< 0 amax)
 
381
                (<= 0 b)
 
382
                (<= b bmax)
 
383
                (< 0 bmax))
 
384
           (and (< (- (* amax bmax)) (* a b))
 
385
                (< (* a b) (* amax bmax))))
 
386
  :rule-classes nil)
 
387
 
 
388
(defthm nonneg-closed*abs
 
389
  (implies (and (rationalp a)
 
390
                (rationalp amax)
 
391
                (rationalp b)
 
392
                (rationalp bmax)
 
393
                (< (- amax) a)
 
394
                (< a amax)
 
395
                (< 0 amax)
 
396
                (<= 0 b)
 
397
                (<= b bmax)
 
398
                (< 0 bmax))
 
399
           (and (< (- (* amax bmax)) (* b a))
 
400
                (< (* b a) (* amax bmax))))
 
401
  :rule-classes nil)
 
402
 
 
403
(defthm nonneg-open*abs
 
404
  (implies (and (rationalp a)
 
405
                (rationalp amax)
 
406
                (rationalp b)
 
407
                (rationalp bmax)
 
408
                (< (- amax) a)
 
409
                (<= a amax) ; (< a amax) is all we'll ever use, I bet.
 
410
                (< 0 amax)
 
411
                (<= 0 b)
 
412
                (< b bmax))
 
413
           (and (< (- (* bmax amax)) (* a b))
 
414
                (< (* a b) (* bmax amax))))
 
415
  :rule-classes nil)
 
416
 
 
417
; The next three, which handle nonnegative open intervals in the first argument,
 
418
; can actually be seen as uses of the abs intervals above.  Simply observe that
 
419
; if 0<=a<amax then -amax<a<amax.
 
420
 
 
421
(defthm nonneg-open*nonneg-closed
 
422
  (implies (and (rationalp a)
 
423
                (rationalp amax)
 
424
                (rationalp b)
 
425
                (rationalp bmax)
 
426
                (<= 0 a)
 
427
                (< a amax)
 
428
                (<= 0 b)
 
429
                (<= b bmax)
 
430
                (< 0 bmax))
 
431
           (and (<= 0 (* a b))
 
432
                (< (* a b) (* amax bmax))))
 
433
  :rule-classes nil)
 
434
 
 
435
(defthm nonneg-open*nonneg-open
 
436
  (implies (and (rationalp a)
 
437
                (rationalp amax)
 
438
                (rationalp b)
 
439
                (rationalp bmax)
 
440
                (<= 0 a)
 
441
                (< a amax)
 
442
                (<= 0 b)
 
443
                (< b bmax))
 
444
           (and (<= 0 (* a b))
 
445
                (< (* a b) (* amax bmax))))
 
446
  :rule-classes nil)
 
447
 
 
448
; and the commuted version
 
449
(defthm nonneg-closed*nonneg-open
 
450
  (implies (and (rationalp a)
 
451
                (rationalp amax)
 
452
                (rationalp b)
 
453
                (rationalp bmax)
 
454
                (<= 0 a)
 
455
                (< a amax)
 
456
                (<= 0 b)
 
457
                (<= b bmax)
 
458
                (< 0 bmax))
 
459
           (and (<= 0 (* b a))
 
460
                (< (* b a) (* amax bmax))))
 
461
  :rule-classes nil)
 
462
 
 
463
(defthm nonneg-closed*nonneg-closed
 
464
  (implies (and (rationalp a)
 
465
                (rationalp amax)
 
466
                (rationalp b)
 
467
                (rationalp bmax)
 
468
                (<= 0 a)
 
469
                (<= a amax)
 
470
                (< 0 amax)
 
471
                (<= 0 b)
 
472
                (<= b bmax)
 
473
                (< 0 bmax))
 
474
           (and (<= 0 (* a b))
 
475
                (<= (* a b) (* amax bmax))))
 
476
  :rule-classes nil)
 
477
 
 
478
(defthm abs*abs
 
479
  (implies (and (rationalp a)
 
480
                (rationalp amax)
 
481
                (rationalp b)
 
482
                (rationalp bmax)
 
483
                (< (- amax) a)
 
484
                (< a amax)
 
485
                (< 0 amax)
 
486
                (< (- bmax) b)
 
487
                (<= b bmax)
 
488
                (< 0 bmax))
 
489
           (and (< (- (* amax bmax)) (* a b))
 
490
                (< (* a b) (* amax bmax))))
 
491
  :rule-classes nil)  
 
492
 
 
493
(defthm rearrange-negative-coefs-<
 
494
  (and (equal (< (* (- c) x) z)
 
495
              (< 0 (+ (* c x) z)))
 
496
       (equal (< (+ (* (- c) x) y) z)
 
497
              (< y (+ (* c x) z)))
 
498
       (equal (< (+ y (* (- c) x)) z)
 
499
              (< y (+ (* c x) z)))
 
500
       (equal (< (+ y1 y2 (* (- c) x)) z)
 
501
              (< (+ y1 y2) (+ (* c x) z)))
 
502
       (equal (< (+ y1 y2 y3 (* (- c) x)) z)
 
503
              (< (+ y1 y2 y3) (+ (* c x) z)))
 
504
       (equal (< z (+ (* (- c) x) y))
 
505
              (< (+ (* c x) z) y))
 
506
       (equal (< z (+ y (* (- c) x)))
 
507
              (< (+ (* c x) z) y))
 
508
       (equal (< z (+ y1 y2 (* (- c) x)))
 
509
              (< (+ (* c x) z) (+ y1 y2)))
 
510
       (equal (< z (+ y1 y2 y3 (* (- c) x)))
 
511
              (< (+ (* c x) z) (+ y1 y2 y3)))))
 
512
 
 
513
(defthm rearrange-negative-coefs-equal
 
514
  (and (implies (and (case-split (rationalp c))
 
515
                     (case-split (rationalp x))
 
516
                     (case-split (rationalp z)))
 
517
                (equal (equal (* (- c) x) z)
 
518
                       (equal 0 (+ (* c x) z))))
 
519
       (implies (and (case-split (rationalp c))
 
520
                     (case-split (rationalp x))
 
521
                     (case-split (rationalp y))
 
522
                     (case-split (rationalp z)))
 
523
                (equal (equal (+ (* (- c) x) y) z)
 
524
                       (equal y (+ (* c x) z))))
 
525
       (implies (and (case-split (rationalp c))
 
526
                     (case-split (rationalp x))
 
527
                     (case-split (rationalp y))
 
528
                     (case-split (rationalp z)))
 
529
                (equal (equal (+ y (* (- c) x)) z)
 
530
                       (equal y (+ (* c x) z))))
 
531
       (implies (and (case-split (rationalp c))
 
532
                     (case-split (rationalp x))
 
533
                     (case-split (rationalp y1))
 
534
                     (case-split (rationalp y2))
 
535
                     (case-split (rationalp z)))
 
536
                (equal (equal (+ y1 y2 (* (- c) x)) z)
 
537
                       (equal (+ y1 y2) (+ (* c x) z))))
 
538
       (implies (and (case-split (rationalp c))
 
539
                     (case-split (rationalp x))
 
540
                     (case-split (rationalp y1))
 
541
                     (case-split (rationalp y2))
 
542
                     (case-split (rationalp y3))
 
543
                     (case-split (rationalp z)))
 
544
                (equal (equal (+ y1 y2 y3 (* (- c) x)) z)
 
545
                       (equal (+ y1 y2 y3) (+ (* c x) z))))
 
546
       (implies (and (case-split (rationalp c))
 
547
                     (case-split (rationalp x))
 
548
                     (case-split (rationalp y))
 
549
                     (case-split (rationalp z)))
 
550
                (equal (equal z (+ (* (- c) x) y))
 
551
                       (equal (+ (* c x) z) y)))
 
552
       (implies (and (case-split (rationalp c))
 
553
                     (case-split (rationalp x))
 
554
                     (case-split (rationalp y))
 
555
                     (case-split (rationalp z)))
 
556
                (equal (equal z (+ y (* (- c) x)))
 
557
                       (equal (+ (* c x) z) y)))
 
558
       (implies (and (case-split (rationalp c))
 
559
                     (case-split (rationalp x))
 
560
                     (case-split (rationalp y1))
 
561
                     (case-split (rationalp y2))
 
562
                     (case-split (rationalp z)))
 
563
                (equal (equal z (+ y1 y2 (* (- c) x)))
 
564
                       (equal (+ (* c x) z) (+ y1 y2))))
 
565
       (implies (and (case-split (rationalp c))
 
566
                     (case-split (rationalp x))
 
567
                     (case-split (rationalp y1))
 
568
                     (case-split (rationalp y2))
 
569
                     (case-split (rationalp y3))
 
570
                     (case-split (rationalp z)))
 
571
                (equal (equal z (+ y1 y2 y3 (* (- c) x)))
 
572
                       (equal (+ (* c x) z) (+ y1 y2 y3))))))
 
573
 
 
574
(defthm rearrange-fractional-coefs-<
 
575
  (and
 
576
   (implies (and (case-split (rationalp c))
 
577
                 (case-split (rationalp z))
 
578
                 (case-split (rationalp x))
 
579
                 (< 0 c))
 
580
            (equal (< (* (/ c) x) z)
 
581
                   (< x (* c z))))
 
582
   (implies (and (case-split (rationalp c))
 
583
                 (case-split (rationalp z))
 
584
                 (case-split (rationalp x))
 
585
                 (case-split (rationalp y))
 
586
                 (< 0 c))
 
587
            (equal (< (+ (* (/ c) x) y) z)
 
588
                   (< (+ x (* c y)) (* c z))))
 
589
   (implies (and (case-split (rationalp c))
 
590
                 (case-split (rationalp z))
 
591
                 (case-split (rationalp x))
 
592
                 (case-split (rationalp y))
 
593
                 (< 0 c))
 
594
            (equal (< (+ y (* (/ c) x)) z)
 
595
                   (< (+ (* c y) x) (* c z))))
 
596
   (implies (and (case-split (rationalp c))
 
597
                 (case-split (rationalp z))
 
598
                 (case-split (rationalp x))
 
599
                 (case-split (rationalp y1))
 
600
                 (case-split (rationalp y2))
 
601
                 (< 0 c))
 
602
            (equal (< (+ y1 y2 (* (/ c) x)) z)
 
603
                   (< (+ (* c y1) (* c y2) x) (* c z))))
 
604
   (implies (and (case-split (rationalp c))
 
605
                 (case-split (rationalp z))
 
606
                 (case-split (rationalp x))
 
607
                 (case-split (rationalp y1))
 
608
                 (case-split (rationalp y2))
 
609
                 (case-split (rationalp y3))
 
610
                 (< 0 c))
 
611
            (equal (< (+ y1 y2 y3 (* (/ c) x)) z)
 
612
                   (< (+ (* c y1) (* c y2) (* c y3) x) (* c z))))
 
613
   (implies (and (case-split (rationalp c))
 
614
                 (case-split (rationalp z))
 
615
                 (case-split (rationalp x))
 
616
                 (< 0 c))
 
617
            (equal (< z (* (/ c) x))
 
618
                   (< (* c z) x)))
 
619
   (implies (and (case-split (rationalp c))
 
620
                 (case-split (rationalp z))
 
621
                 (case-split (rationalp x))
 
622
                 (case-split (rationalp y))
 
623
                 (< 0 c))
 
624
            (equal (< z (+ (* (/ c) x) y))
 
625
                   (< (* c z) (+ x (* c y)))))
 
626
   (implies (and (case-split (rationalp c))
 
627
                 (case-split (rationalp z))
 
628
                 (case-split (rationalp x))
 
629
                 (case-split (rationalp y))
 
630
                 (< 0 c))
 
631
            (equal (< z (+ y (* (/ c) x)))
 
632
                   (< (* c z) (+ (* c y) x))))
 
633
   (implies (and (case-split (rationalp c))
 
634
                 (case-split (rationalp z))
 
635
                 (case-split (rationalp x))
 
636
                 (case-split (rationalp y1))
 
637
                 (case-split (rationalp y2))
 
638
                 (< 0 c))
 
639
            (equal (< z (+ y1 y2 (* (/ c) x)))
 
640
                   (< (* c z) (+ (* c y1) (* c y2) x))))
 
641
   (implies (and (case-split (rationalp c))
 
642
                 (case-split (rationalp z))
 
643
                 (case-split (rationalp x))
 
644
                 (case-split (rationalp y1))
 
645
                 (case-split (rationalp y2))
 
646
                 (case-split (rationalp y3))
 
647
                 (< 0 c))
 
648
            (equal (< z (+ y1 y2 y3 (* (/ c) x)))
 
649
                   (< (* c z) (+ (* c y1) (* c y2) (* c y3) x))))))
 
650
 
 
651
(defthm rearrange-fractional-coefs-equal
 
652
  (and
 
653
   (implies (and (case-split (rationalp c))
 
654
                 (case-split (rationalp z))
 
655
                 (case-split (rationalp x))
 
656
                 (< 0 c))
 
657
            (equal (equal (* (/ c) x) z)
 
658
                   (equal x (* c z))))
 
659
   (implies (and (case-split (rationalp c))
 
660
                 (case-split (rationalp z))
 
661
                 (case-split (rationalp x))
 
662
                 (case-split (rationalp y))
 
663
                 (< 0 c))
 
664
            (equal (equal (+ (* (/ c) x) y) z)
 
665
                   (equal (+ x (* c y)) (* c z))))
 
666
   (implies (and (case-split (rationalp c))
 
667
                 (case-split (rationalp z))
 
668
                 (case-split (rationalp x))
 
669
                 (case-split (rationalp y))
 
670
                 (< 0 c))
 
671
            (equal (equal (+ y (* (/ c) x)) z)
 
672
                   (equal (+ (* c y) x) (* c z))))
 
673
   (implies (and (case-split (rationalp c))
 
674
                 (case-split (rationalp z))
 
675
                 (case-split (rationalp x))
 
676
                 (case-split (rationalp y1))
 
677
                 (case-split (rationalp y2))
 
678
                 (< 0 c))
 
679
            (equal (equal (+ y1 y2 (* (/ c) x)) z)
 
680
                   (equal (+ (* c y1) (* c y2) x) (* c z))))
 
681
   (implies (and (case-split (rationalp c))
 
682
                 (case-split (rationalp z))
 
683
                 (case-split (rationalp x))
 
684
                 (case-split (rationalp y1))
 
685
                 (case-split (rationalp y2))
 
686
                 (case-split (rationalp y3))
 
687
                 (< 0 c))
 
688
            (equal (equal (+ y1 y2 y3 (* (/ c) x)) z)
 
689
                   (equal (+ (* c y1) (* c y2) (* c y3) x) (* c z))))))
 
690
 
 
691
(defthm x*/y=1->x=y
 
692
  (implies (and (rationalp x)
 
693
                (rationalp y)
 
694
                (not (equal x 0))
 
695
                (not (equal y 0)))
 
696
           (equal (equal (* x (/ y)) 1)
 
697
                  (equal x y)))
 
698
  :rule-classes nil)
 
699
                
 
700
(defun point-right-measure (x)
 
701
  (floor (if (and (rationalp x) (< 0 x)) (/ x) 0) 1))
 
702
 
 
703
(defun point-left-measure (x)
 
704
  (floor (if (and (rationalp x) (> x 0)) x 0) 1))
 
705
 
 
706
(include-book "ordinals/e0-ordinal" :dir :system)
 
707
(set-well-founded-relation e0-ord-<)
 
708
 
 
709
(defthm recursion-by-point-right
 
710
  (and (e0-ordinalp (point-right-measure x))
 
711
       (implies (and (rationalp x)
 
712
                     (< 0 x)
 
713
                     (< x 1))
 
714
                (e0-ord-< (point-right-measure (* 2 x))
 
715
                          (point-right-measure x)))))
 
716
 
 
717
(defthm recursion-by-point-left
 
718
  (and (e0-ordinalp (point-left-measure x))
 
719
       (implies (and (rationalp x)
 
720
                     (>= x 2))
 
721
                (e0-ord-< (point-left-measure (* 1/2 x))
 
722
                          (point-left-measure x)))))
 
723
 
 
724
(defthm x<x*y<->1<y
 
725
  (implies (and (rationalp x)
 
726
                (< 0 x)
 
727
                (rationalp y))
 
728
           (equal (< x (* x y)) (< 1 y)))
 
729
  :rule-classes nil)
 
730
 
 
731
(defthm cancel-equal-*
 
732
  (implies (and (rationalp r)
 
733
                (rationalp s)
 
734
                (rationalp a)
 
735
                (not (equal a 0)))
 
736
           (equal (equal (* a r) (* a s))
 
737
                  (equal r s)))
 
738
  :rule-classes nil)
 
739
 
 
740
(defthmd expt-split
 
741
  (implies (and (integerp i)
 
742
                (integerp j)
 
743
                (case-split (acl2-numberp r)) ;(integerp r)
 
744
                (case-split (not (equal r 0)))
 
745
                )
 
746
           (equal (expt r (+ i j))
 
747
                  (* (expt r i) (expt r j)))))
 
748
 
 
749
(defthm cancel-<-*
 
750
  (implies (and (rationalp r)
 
751
                (rationalp s)
 
752
                (rationalp a)
 
753
                (< 0 a))
 
754
           (equal (< (* a r) (* a s))
 
755
                  (< r s)))
 
756
  :rule-classes nil)
 
757
 
 
758
(in-theory (disable fl
 
759
                    inverse-of-*
 
760
                    point-right-measure point-left-measure))
 
761
 
 
762
 
 
763
;;;**********************************************************************
 
764
;;;                       EXPONENTIATION
 
765
;;;**********************************************************************
 
766
 
 
767
(defthm expt-2-positive-rational-type
 
768
  (and (rationalp (expt 2 i))
 
769
       (< 0 (expt 2 i)))
 
770
  :rule-classes (:rewrite (:type-prescription :typed-term (expt 2 i))))
 
771
 
 
772
(defthm expt-2-positive-integer-type
 
773
  (implies (<= 0 i)
 
774
           (and (integerp (expt 2 i))
 
775
                (< 0 (expt 2 i))))
 
776
  :rule-classes (:type-prescription))
 
777
 
 
778
(defthm expt-2-type-linear
 
779
  (implies (<= 0 i)
 
780
           (<= 1 (expt 2 i)))
 
781
  :rule-classes ((:linear :trigger-terms ((expt 2 i)))))
 
782
 
 
783
(defthmd expt-weak-monotone
 
784
  (implies (and (integerp n)
 
785
                (integerp m))
 
786
           (equal (<= (expt 2 n) (expt 2 m))
 
787
                  (<= n m))))
 
788
 
 
789
(defthmd expt-strong-monotone
 
790
  (implies (and (integerp n)
 
791
                (integerp m))
 
792
           (equal (< (expt 2 n) (expt 2 m))
 
793
                  (< n m))))
 
794
 
 
795
(defthmd expt-inverse
 
796
  (equal (/ (expt 2 i))
 
797
         (expt 2 (* -1 i))))
 
798
 
 
799
(defthm ash-rewrite
 
800
    (implies (integerp n)
 
801
             (equal (ash n i)
 
802
                    (fl (* n (expt 2 i))))))
 
803
 
 
804
(defthm exp+1
 
805
    (implies (and (integerp m)
 
806
                  (integerp n)
 
807
                  (<= n m))
 
808
             (> (* (- 1 (expt 2 m)) (- 1 (expt 2 n)))
 
809
                (- 1 (expt 2 (1+ m)))))
 
810
  :rule-classes ())
 
811
 
 
812
(defthm exp+2
 
813
    (implies (and (integerp n)
 
814
                  (integerp m)
 
815
                  (<= n m)
 
816
                  (<= m 0))
 
817
             (< (* (1+ (expt 2 m)) (1+ (expt 2 n)))
 
818
                (1+ (expt 2 (+ m 2)))))
 
819
  :rule-classes ())
 
820
 
 
821
(defthm exp-invert
 
822
    (implies (and (integerp n)
 
823
                  (<= n -1))
 
824
             (<= (/ (- 1 (expt 2 n)))
 
825
                 (1+ (expt 2 (1+ n)))))
 
826
  :rule-classes ())