← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/rtl/rel6/arithmetic/fp.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/arithmetic/fp.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
;Rename this book, since the guts have been ripped out?
 
4
;BOZO clean up this book?
 
5
;BOZO move these lemmas to extra?
 
6
#|
 
7
 
 
8
This book contains a few lemmas which are exported in lib/arith but which aren't needed in support/ or
 
9
arithmetic/.  
 
10
 
 
11
|#
 
12
 
 
13
(local (include-book "fp2"))
 
14
 
 
15
(defthm rearrange-fractional-coefs-<
 
16
  (and
 
17
   (implies (and (case-split (rationalp c))
 
18
                 (case-split (rationalp z))
 
19
                 (case-split (rationalp x))
 
20
                 (< 0 c))
 
21
            (equal (< (* (/ c) x) z)
 
22
                   (< x (* c z))))
 
23
   (implies (and (case-split (rationalp c))
 
24
                 (case-split (rationalp z))
 
25
                 (case-split (rationalp x))
 
26
                 (case-split (rationalp y))
 
27
                 (< 0 c))
 
28
            (equal (< (+ (* (/ c) x) y) z)
 
29
                   (< (+ x (* c y)) (* c z))))
 
30
   (implies (and (case-split (rationalp c))
 
31
                 (case-split (rationalp z))
 
32
                 (case-split (rationalp x))
 
33
                 (case-split (rationalp y))
 
34
                 (< 0 c))
 
35
            (equal (< (+ y (* (/ c) x)) z)
 
36
                   (< (+ (* c y) x) (* c z))))
 
37
   (implies (and (case-split (rationalp c))
 
38
                 (case-split (rationalp z))
 
39
                 (case-split (rationalp x))
 
40
                 (case-split (rationalp y1))
 
41
                 (case-split (rationalp y2))
 
42
                 (< 0 c))
 
43
            (equal (< (+ y1 y2 (* (/ c) x)) z)
 
44
                   (< (+ (* c y1) (* c y2) x) (* c z))))
 
45
   (implies (and (case-split (rationalp c))
 
46
                 (case-split (rationalp z))
 
47
                 (case-split (rationalp x))
 
48
                 (case-split (rationalp y1))
 
49
                 (case-split (rationalp y2))
 
50
                 (case-split (rationalp y3))
 
51
                 (< 0 c))
 
52
            (equal (< (+ y1 y2 y3 (* (/ c) x)) z)
 
53
                   (< (+ (* c y1) (* c y2) (* c y3) x) (* c z))))
 
54
   (implies (and (case-split (rationalp c))
 
55
                 (case-split (rationalp z))
 
56
                 (case-split (rationalp x))
 
57
                 (< 0 c))
 
58
            (equal (< z (* (/ c) x))
 
59
                   (< (* c z) x)))
 
60
   (implies (and (case-split (rationalp c))
 
61
                 (case-split (rationalp z))
 
62
                 (case-split (rationalp x))
 
63
                 (case-split (rationalp y))
 
64
                 (< 0 c))
 
65
            (equal (< z (+ (* (/ c) x) y))
 
66
                   (< (* c z) (+ x (* c y)))))
 
67
   (implies (and (case-split (rationalp c))
 
68
                 (case-split (rationalp z))
 
69
                 (case-split (rationalp x))
 
70
                 (case-split (rationalp y))
 
71
                 (< 0 c))
 
72
            (equal (< z (+ y (* (/ c) x)))
 
73
                   (< (* c z) (+ (* c y) x))))
 
74
   (implies (and (case-split (rationalp c))
 
75
                 (case-split (rationalp z))
 
76
                 (case-split (rationalp x))
 
77
                 (case-split (rationalp y1))
 
78
                 (case-split (rationalp y2))
 
79
                 (< 0 c))
 
80
            (equal (< z (+ y1 y2 (* (/ c) x)))
 
81
                   (< (* c z) (+ (* c y1) (* c y2) x))))
 
82
   (implies (and (case-split (rationalp c))
 
83
                 (case-split (rationalp z))
 
84
                 (case-split (rationalp x))
 
85
                 (case-split (rationalp y1))
 
86
                 (case-split (rationalp y2))
 
87
                 (case-split (rationalp y3))
 
88
                 (< 0 c))
 
89
            (equal (< z (+ y1 y2 y3 (* (/ c) x)))
 
90
                   (< (* c z) (+ (* c y1) (* c y2) (* c y3) x))))))
 
91
 
 
92
 
 
93
(defthm rearrange-fractional-coefs-equal
 
94
  (and
 
95
   (implies (and (case-split (rationalp c))
 
96
                 (case-split (rationalp z))
 
97
                 (case-split (rationalp x))
 
98
                 (< 0 c))
 
99
            (equal (equal (* (/ c) x) z)
 
100
                 (equal x (* c z))))
 
101
   (implies (and (case-split (rationalp c))
 
102
                 (case-split (rationalp z))
 
103
                 (case-split (rationalp x))
 
104
                 (case-split (rationalp y))
 
105
                 (< 0 c))
 
106
            (equal (equal (+ (* (/ c) x) y) z)
 
107
                 (equal (+ x (* c y)) (* c z))))
 
108
   (implies (and (case-split (rationalp c))
 
109
                 (case-split (rationalp z))
 
110
                 (case-split (rationalp x))
 
111
                 (case-split (rationalp y))
 
112
                 (< 0 c))
 
113
            (equal (equal (+ y (* (/ c) x)) z)
 
114
                 (equal (+ (* c y) x) (* c z))))
 
115
   (implies (and (case-split (rationalp c))
 
116
                 (case-split (rationalp z))
 
117
                 (case-split (rationalp x))
 
118
                 (case-split (rationalp y1))
 
119
                 (case-split (rationalp y2))
 
120
                 (< 0 c))
 
121
            (equal (equal (+ y1 y2 (* (/ c) x)) z)
 
122
                 (equal (+ (* c y1) (* c y2) x) (* c z))))
 
123
   (implies (and (case-split (rationalp c))
 
124
                 (case-split (rationalp z))
 
125
                 (case-split (rationalp x))
 
126
                 (case-split (rationalp y1))
 
127
                 (case-split (rationalp y2))
 
128
                 (case-split (rationalp y3))
 
129
                 (< 0 c))
 
130
            (equal (equal (+ y1 y2 y3 (* (/ c) x)) z)
 
131
                 (equal (+ (* c y1) (* c y2) (* c y3) x) (* c z))))))
 
132
 
 
133
 
 
134
 
 
135
; We now prove a bunch of bounds theorems for *.  We are concerned with bounding the
 
136
; product of a and b given intervals for a and b.  We consider three kinds of intervals.
 
137
; We discuss only the a case.
 
138
 
 
139
; abs intervals mean (abs a) < amax or -amax < a < amax, where amax is positive.
 
140
 
 
141
; nonneg-open intervals mean 0<=a<amax.
 
142
 
 
143
; nonneg-closed intervals mean 0<=a<=amax, where amax is positive.
 
144
 
 
145
; We now prove theorems with names like abs*nonneg-open, etc. characterizing
 
146
; the product of two elements from two such interals.  All of these theorems
 
147
; are made with :rule-classes nil because I don't know how to control their
 
148
; use.
 
149
 
 
150
(encapsulate nil
 
151
  (local 
 
152
   (defthm renaming
 
153
    (implies (and (rationalp a)
 
154
                  (rationalp xmax)
 
155
                  (rationalp b)
 
156
                  (rationalp bmax)
 
157
                  (< (- xmax) a)
 
158
                  (<= a xmax)
 
159
                  (< 0 xmax)
 
160
                  (<= 0 b)
 
161
                  (< b bmax))
 
162
             (and (< (- (* xmax bmax)) (* a b))
 
163
                  (< (* a b) (* xmax bmax))))
 
164
    :hints (("Goal" :cases ((equal b 0))))))
 
165
 
 
166
; This lemma is for lookup * d and lookup * away.  We don't need to consider 0
 
167
; < b for the d case because we have 0 < 1 <= d and the conclusion of the new
 
168
; lemma would be no different.
 
169
 
 
170
  (defthm abs*nonneg-open
 
171
    (implies (and (rationalp a)
 
172
                  (rationalp amax)
 
173
                  (rationalp b)
 
174
                  (rationalp bmax)
 
175
                  (< (- amax) a)
 
176
                  (<= a amax)       ; (< a amax) is all we'll ever use, I bet.
 
177
                  (< 0 amax)
 
178
                  (<= 0 b)
 
179
                  (< b bmax))
 
180
             (and (< (- (* amax bmax)) (* a b))
 
181
                  (< (* a b) (* amax bmax))))
 
182
    :hints (("Goal" :by renaming))
 
183
    :rule-classes nil))
 
184
 
 
185
(defthm abs*nonneg-closed
 
186
  (implies (and (rationalp a)
 
187
                (rationalp amax)
 
188
                (rationalp b)
 
189
                (rationalp bmax)
 
190
                (< (- amax) a)
 
191
                (< a amax)
 
192
                (< 0 amax)
 
193
                (<= 0 b)
 
194
                (<= b bmax)
 
195
                (< 0 bmax))
 
196
           (and (< (- (* amax bmax)) (* a b))
 
197
                (< (* a b) (* amax bmax))))
 
198
  :hints (("Goal" :cases ((equal b 0))))
 
199
  :rule-classes nil)
 
200
 
 
201
(defthm nonneg-closed*abs
 
202
  (implies (and (rationalp a)
 
203
                (rationalp amax)
 
204
                (rationalp b)
 
205
                (rationalp bmax)
 
206
                (< (- amax) a)
 
207
                (< a amax)
 
208
                (< 0 amax)
 
209
                (<= 0 b)
 
210
                (<= b bmax)
 
211
                (< 0 bmax))
 
212
           (and (< (- (* amax bmax)) (* b a))
 
213
                (< (* b a) (* amax bmax))))
 
214
  :hints (("Goal" :use abs*nonneg-closed))
 
215
  :rule-classes nil)
 
216
 
 
217
(defthm nonneg-open*abs
 
218
  (implies (and (rationalp a)
 
219
                (rationalp amax)
 
220
                (rationalp b)
 
221
                (rationalp bmax)
 
222
                (< (- amax) a)
 
223
                (<= a amax) ; (< a amax) is all we'll ever use, I bet.
 
224
                (< 0 amax)
 
225
                (<= 0 b)
 
226
                (< b bmax))
 
227
           (and (< (- (* bmax amax)) (* a b))
 
228
                (< (* a b) (* bmax amax))))
 
229
    :hints (("Goal" :use abs*nonneg-open))
 
230
    :rule-classes nil)
 
231
 
 
232
; The next three, which handle nonnegative open intervals in the first argument,
 
233
; can actually be seen as uses of the abs intervals above.  Simply observe that
 
234
; if 0<=a<amax then -amax<a<amax.
 
235
 
 
236
(defthm nonneg-open*nonneg-closed
 
237
  (implies (and (rationalp a)
 
238
                (rationalp amax)
 
239
                (rationalp b)
 
240
                (rationalp bmax)
 
241
                (<= 0 a)
 
242
                (< a amax)
 
243
                (<= 0 b)
 
244
                (<= b bmax)
 
245
                (< 0 bmax))
 
246
           (and (<= 0 (* a b))
 
247
                (< (* a b) (* amax bmax))))
 
248
  :hints (("Goal" :use abs*nonneg-closed))
 
249
  :rule-classes nil)
 
250
 
 
251
(defthm nonneg-open*nonneg-open
 
252
  (implies (and (rationalp a)
 
253
                (rationalp amax)
 
254
                (rationalp b)
 
255
                (rationalp bmax)
 
256
                (<= 0 a)
 
257
                (< a amax)
 
258
                (<= 0 b)
 
259
                (< b bmax))
 
260
           (and (<= 0 (* a b))
 
261
                (< (* a b) (* amax bmax))))
 
262
  :hints (("Goal" :use abs*nonneg-open))
 
263
  :rule-classes nil)
 
264
 
 
265
; and the commuted version
 
266
(defthm nonneg-closed*nonneg-open
 
267
  (implies (and (rationalp a)
 
268
                (rationalp amax)
 
269
                (rationalp b)
 
270
                (rationalp bmax)
 
271
                (<= 0 a)
 
272
                (< a amax)
 
273
                (<= 0 b)
 
274
                (<= b bmax)
 
275
                (< 0 bmax))
 
276
           (and (<= 0 (* b a))
 
277
                (< (* b a) (* amax bmax))))
 
278
  :hints (("Goal" :use nonneg-open*nonneg-closed))
 
279
  :rule-classes nil)
 
280
 
 
281
(defthm nonneg-closed*nonneg-closed
 
282
  (implies (and (rationalp a)
 
283
                (rationalp amax)
 
284
                (rationalp b)
 
285
                (rationalp bmax)
 
286
                (<= 0 a)
 
287
                (<= a amax)
 
288
                (< 0 amax)
 
289
                (<= 0 b)
 
290
                (<= b bmax)
 
291
                (< 0 bmax))
 
292
           (and (<= 0 (* a b))
 
293
                (<= (* a b) (* amax bmax))))
 
294
  :rule-classes nil)
 
295
 
 
296
(defthm abs*abs
 
297
  (implies (and (rationalp a)
 
298
                (rationalp amax)
 
299
                (rationalp b)
 
300
                (rationalp bmax)
 
301
                (< (- amax) a)
 
302
                (< a amax)
 
303
                (< 0 amax)
 
304
                (< (- bmax) b)
 
305
                (<= b bmax)
 
306
                (< 0 bmax))
 
307
           (and (< (- (* amax bmax)) (* a b))
 
308
                (< (* a b) (* amax bmax))))
 
309
  :hints (("Goal" :cases ((< b 0) (> b 0))))
 
310
  :rule-classes nil)