← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/projects/hybrid-systems/phi-properties.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/projects/hybrid-systems/phi-properties.lisp
 
1
; Copyright (C) 2007 by Shant Harutunian
 
2
; License: A 3-clause BSD license.  See the LICENSE file distributed with ACL2.
 
3
 
 
4
(in-package "ACL2")
 
5
 
 
6
(include-book "arith-nsa4")
 
7
(include-book "abs")
 
8
(include-book "eexp")
 
9
(include-book "phi-exists")
 
10
(include-book "computed-hints")
 
11
(include-book "tm-floor")
 
12
 
 
13
(in-theory (disable i-large))
 
14
(in-theory (disable standard-part-<=))
 
15
 
 
16
;; Cuong Chau: Some proofs failed when I left the following lemmas enable.
 
17
 
 
18
(local
 
19
 (in-theory (disable EPS-N-FUN-RW-1-THM
 
20
                     EPS-N-FUN-RW-2-THM
 
21
                     EPS-N-FUN-RW-3-THM
 
22
                     EPS-N-FUN-RW-4-THM)))
 
23
 
 
24
(defun f-sum (x n eps)
 
25
  (cond
 
26
   ((zp n) 0)
 
27
   (t (+ (* eps (f (run x (- n 1) eps)))
 
28
         (f-sum x (- n 1) eps)))))
 
29
 
 
30
(defthm run-f-sum-thm
 
31
  (implies
 
32
   (and
 
33
    (realp x)
 
34
    (realp eps)
 
35
    (< 0 eps))
 
36
   (equal (run x n eps)
 
37
          (+ x (f-sum x n eps))))
 
38
  :rule-classes nil
 
39
  :hints (("Goal" :do-not '(generalize))
 
40
          ("Subgoal *1/2" :in-theory (disable step-run-thm)
 
41
           :use ((:instance
 
42
                  step-run-thm (n (- n 1)))))))
 
43
 
 
44
(defun resid (x n eps)
 
45
  (- (f-sum x n eps) (* n eps (f x))))
 
46
 
 
47
(defthm f-sum-type
 
48
  (implies
 
49
   (and
 
50
    (realp x)
 
51
    (realp eps))
 
52
   (realp (f-sum x n eps)))
 
53
  :rule-classes :type-prescription)
 
54
 
 
55
(defthm run-type
 
56
  (implies
 
57
   (and
 
58
    (realp x)
 
59
    (realp eps))
 
60
   (realp (run x n eps)))
 
61
  :rule-classes :type-prescription)
 
62
 
 
63
(defthm run-limited-thm
 
64
  (implies
 
65
   (and
 
66
    (realp x)
 
67
    (i-limited x)
 
68
    (realp eps)
 
69
    (integerp n)
 
70
    (< 0 eps)
 
71
    (<= 0 n)
 
72
    (i-limited (* eps n)))
 
73
   (i-limited (run x n eps)))
 
74
  :rule-classes ((:type-prescription) (:rewrite))
 
75
  :hints (("Goal" :in-theory (disable abs
 
76
                                      run
 
77
                                      run-n-limit
 
78
                                      i-large
 
79
                                      plus-limited
 
80
                                      times-limited
 
81
                                      divide-limited)
 
82
           :use ((:instance run-limit-eexpt-thm)
 
83
                 (:instance run-n-limit-limited-thm)
 
84
                 (:instance limited-bound-x-implies-limited-x-thm
 
85
                            (y (run-n-limit x n eps))
 
86
                            (x (run x n eps)))))))
 
87
 
 
88
(defthm resid-limited-thm
 
89
  (implies
 
90
   (and
 
91
    (realp x)
 
92
    (i-limited x)
 
93
    (integerp n)
 
94
    (<= 0 n)
 
95
    (realp eps)
 
96
    (< 0 eps)
 
97
    (i-limited (* eps n)))
 
98
   (i-limited (resid x n eps)))
 
99
  :rule-classes :type-prescription
 
100
  :hints (("Goal" :in-theory (disable i-large)
 
101
           :use ((:instance run-f-sum-thm)
 
102
                 (:instance run-limited-thm)))
 
103
          ("Goal'''" :use ((:instance times-limited
 
104
                                      (x (* eps n))
 
105
                                      (y (f x)))
 
106
                           (:instance plus-limited
 
107
                                      (x (+ X (F-SUM X N EPS)))
 
108
                                      (y (- x)))))))
 
109
 
 
110
(defthm resid-standard-thm
 
111
  (implies
 
112
   (and
 
113
    (realp x)
 
114
    (i-limited x)
 
115
    (integerp n)
 
116
    (<= 0 n)
 
117
    (realp eps)
 
118
    (< 0 eps)
 
119
    (i-limited (* eps n)))
 
120
   (standard-numberp (standard-part (resid x n eps))))
 
121
  :hints (("Goal" :in-theory (disable i-large resid)
 
122
           :use ((:instance resid-limited-thm)))))
 
123
 
 
124
(defthm resid-std-thm
 
125
  (IMPLIES
 
126
   (AND (STANDARD-NUMBERP X)
 
127
        (STANDARD-NUMBERP TM)
 
128
        (REALP X)
 
129
        (REALP TM)
 
130
        (<= 0 TM))
 
131
   (STANDARD-NUMBERP (STANDARD-PART
 
132
                      (resid X
 
133
                             (FLOOR1 (* (I-LARGE-INTEGER) TM))
 
134
                             (/ (I-LARGE-INTEGER))))))
 
135
  :hints (("Goal" :in-theory (disable i-large)
 
136
           :use ((:instance resid-standard-thm
 
137
                            (n (floor1 (* tm (i-large-integer))))
 
138
                            (eps (/ (i-large-integer))))))))
 
139
 
 
140
(in-theory (disable resid))
 
141
 
 
142
(defun-std resid-tm (x tm)
 
143
  (cond
 
144
   ((not (and (realp x)
 
145
              (realp tm)
 
146
              (<= 0 tm))) 0)
 
147
   (t (standard-part (resid x
 
148
                            (floor1 (* tm (i-large-integer)))
 
149
                            (/ (i-large-integer)))))))
 
150
 
 
151
(in-theory (enable resid))
 
152
 
 
153
(defthm f-run-bound-hint-1
 
154
  (implies
 
155
   (and
 
156
    (realp x)
 
157
    (realp eps)
 
158
    (< 0 eps))
 
159
   (equal (f (step1 x eps))
 
160
          (+ (f x) (- (f (step1 x eps)) (f x)))))
 
161
  :rule-classes nil)
 
162
 
 
163
(defthm f-run-bound-hint-2
 
164
  (implies
 
165
   (and
 
166
    (realp x)
 
167
    (realp eps)
 
168
    (< 0 eps))
 
169
   (<= (abs (f (step1 x eps)))
 
170
       (* (+ 1 (* eps (L))) (abs (f x)))))
 
171
  :rule-classes nil
 
172
  :hints (("Goal" :in-theory (disable abs)
 
173
                  :use ((:instance f-run-bound-hint-1)
 
174
                        (:instance abs-triangular-inequality-thm
 
175
                                   (x (f x))
 
176
                                   (y (- (f (step1 x eps)) (f x))))
 
177
                        (:instance f-lim-thm
 
178
                                   (x1 (step1 x eps))
 
179
                                   (x2 x))))))
 
180
 
 
181
(defthm f-run-bound-thm
 
182
  (implies
 
183
   (and
 
184
    (realp x)
 
185
    (realp eps)
 
186
    (< 0 eps)
 
187
    (integerp n)
 
188
    (<= 0 n))
 
189
   (<= (abs (f (run x n eps)))
 
190
       (* (eexp (* n eps (L))) (abs (f x)))))
 
191
  :hints (("Goal" :in-theory (disable abs step1)
 
192
           :do-not '(generalize))
 
193
          ("Subgoal *1/5" :use ((:instance pos-factor-<=-thm
 
194
                                           (x (abs (f (step1 x eps))))
 
195
                                           (y (* (+ 1 (* eps (L))) (abs (f x))))
 
196
                                           (a (EEXP (+ (* -1 (L) EPS)
 
197
                                                       (* (L) EPS N)))))
 
198
                                (:instance pos-factor-<=-thm
 
199
                                           (x (+ 1 (* eps (L))))
 
200
                                           (y (eexp (* eps (L))))
 
201
                                           (a (* (EEXP (+ (* -1 (L) EPS)
 
202
                                                          (* (L) EPS N)))
 
203
                                                 (abs (f x)))))
 
204
                                (:instance  f-run-bound-hint-2)
 
205
                                (:instance  1+x-<=eexp-thm
 
206
                                            (x (* eps (L))))))))
 
207
 
 
208
(defthm f-sum-exp-bound-thm
 
209
  (implies
 
210
   (and
 
211
    (realp x)
 
212
    (realp eps)
 
213
    (< 0 eps)
 
214
    (integerp n)
 
215
    (<= 0 n))
 
216
   (<= (abs (f-sum x n eps))
 
217
       (* n eps (eexp (* eps n (L))) (abs (f x)))))
 
218
  :rule-classes nil
 
219
  :hints (("Goal" :induct (f-sum x n eps)
 
220
           :do-not-induct t
 
221
           :in-theory (disable abs <-*-LEFT-CANCEL)
 
222
           :do-not '(generalize))
 
223
          ("Subgoal *1/2" :use ((:instance f-run-bound-thm (n (- n 1)))
 
224
                                (:instance pos-factor-<=-thm
 
225
                                           (x  (abs (f (run x (- n 1) eps))))
 
226
                                           (y (* (eexp (* (- n 1) eps (L)))
 
227
                                                 (abs (f x))))
 
228
                                           (a eps))
 
229
                                (:instance abs-triangular-inequality-thm
 
230
                                           (x (F-SUM X (+ -1 N) EPS))
 
231
                                           (y (* EPS (F (RUN X (+ -1 N) EPS)))))
 
232
                                (:instance pos-factor-<=-thm
 
233
                                           (x 1)
 
234
                                           (y (EEXP (* (L) EPS)))
 
235
                                           (a (* EPS N (ABS (F X))
 
236
                                                 (EEXP (+ (* -1 (L) EPS)
 
237
                                                          (* (L) EPS N)))))
 
238
                                           )))))
 
239
 
 
240
(defthm f-sum-diff-thm
 
241
  (implies
 
242
   (and
 
243
    (realp x)
 
244
    (realp eps)
 
245
    (< 0 eps)
 
246
    (integerp n)
 
247
    (integerp m)
 
248
    (<= 0 n)
 
249
    (<= n m))
 
250
   (equal (- (f-sum x m eps)
 
251
             (f-sum x n eps))
 
252
          (f-sum (run x n eps) (- m n) eps))))
 
253
 
 
254
(defthm f-run-diff-eq-f-sum-thm
 
255
  (implies
 
256
   (and
 
257
    (realp x)
 
258
    (realp eps)
 
259
    (< 0 eps)
 
260
    (integerp n)
 
261
    (integerp m)
 
262
    (<= 0 n)
 
263
    (<= n m))
 
264
   (equal (- (run x m eps)
 
265
             (run x n eps))
 
266
          (f-sum (run x n eps) (- m n) eps)))
 
267
  :hints (("Goal" :do-not-induct t
 
268
           :use ((:instance run-f-sum-thm (n m))
 
269
                 (:instance run-f-sum-thm)
 
270
                 (:instance f-sum-diff-thm)))))
 
271
 
 
272
(defthm pos-*-<=-thm
 
273
  (implies
 
274
   (and
 
275
    (realp a)
 
276
    (realp b)
 
277
    (realp x)
 
278
    (realp y)
 
279
    (<= 0 a)
 
280
    (<= 0 b)
 
281
    (<= a x)
 
282
    (<= b y))
 
283
   (<= (* a b) (* x y)))
 
284
  :hints (("Goal" :use ((:instance pos-factor-<=-thm
 
285
                                   (x a)
 
286
                                   (y x)
 
287
                                   (a b))
 
288
                        (:instance pos-factor-<=-thm
 
289
                                   (x b)
 
290
                                   (y y)
 
291
                                   (a x))))))
 
292
 
 
293
(defthm  f-run-diff-tm-thm-hint
 
294
  (implies
 
295
   (and
 
296
    (realp eps)
 
297
    (< 0 eps)
 
298
    (integerp m)
 
299
    (integerp n)
 
300
    (<= n m))
 
301
   (<= 0 (* (- m n) eps (eexp (* (- m n) (L) eps)))))
 
302
  :rule-classes nil
 
303
  :hints (("Goal" :in-theory (disable distributivity
 
304
                                      distributivity-left)
 
305
           :use ((:instance pos-factor-<=-thm
 
306
                            (x 0)
 
307
                            (y (- m n))
 
308
                            (a (* eps
 
309
                                  (eexp (* (- m n)
 
310
                                           (L)
 
311
                                           eps))))
 
312
                            )))))
 
313
 
 
314
(defthm f-run-diff-tm-thm
 
315
  (implies
 
316
   (and
 
317
    (realp x)
 
318
    (realp eps)
 
319
    (< 0 eps)
 
320
    (integerp n)
 
321
    (integerp m)
 
322
    (<= 0 n)
 
323
    (<= n m))
 
324
   (<= (abs (- (run x m eps)
 
325
               (run x n eps)))
 
326
       (* (- m n) eps (eexp (* eps m (L))) (abs (f x)))))
 
327
  :hints (("Goal" :do-not-induct t
 
328
           :in-theory (disable abs)
 
329
           :use ((:instance f-run-diff-tm-thm-hint)
 
330
                 (:instance f-run-diff-eq-f-sum-thm)
 
331
                 (:instance f-sum-exp-bound-thm
 
332
                            (x (run x n eps))
 
333
                            (n (- m n)))
 
334
                 (:instance f-run-bound-thm)
 
335
                 (:instance pos-factor-<=-thm
 
336
                            (x (abs (f (run x n eps))))
 
337
                            (y (* (eexp (* n eps (L))) (abs (f x))))
 
338
                            (a (* (- m n)
 
339
                                  eps
 
340
                                  (eexp (* eps
 
341
                                           (- m n)
 
342
                                           (L))))))))))
 
343
 
 
344
;; Cuong Chau: I need this lemma to prove some theorems in this book.
 
345
 
 
346
(defthm standard-number-is-limited
 
347
  (implies (standard-numberp r)
 
348
           (i-limited r)))
 
349
 
 
350
(defthm run-diff-tm-standard-part-thm
 
351
  (implies
 
352
   (and
 
353
    (realp x)
 
354
    (standard-numberp x)
 
355
    (integerp n)
 
356
    (integerp m)
 
357
    (realp eps)
 
358
    (< 0 eps)
 
359
    (<= 0 n)
 
360
    (<= 0 m)
 
361
    (i-limited (* eps n))
 
362
    (i-limited (* eps m))
 
363
    (equal (standard-part (* m eps))
 
364
           (standard-part (* n eps))))
 
365
   (equal (- (standard-part (run x m eps))
 
366
             (standard-part (run x n eps)))
 
367
          0))
 
368
  :hints ((standard-part-hint stable-under-simplificationp clause)
 
369
          ("Goal" :in-theory (e/d (EPS-N-FUN-RW-1-THM
 
370
                                   EPS-N-FUN-RW-3-THM)
 
371
                                  (abs))
 
372
           :cases ((<= n m) (< m n))
 
373
           :do-not-induct t)
 
374
          ("Subgoal 2" :use ((:instance f-run-diff-tm-thm)))
 
375
          ("Subgoal 1" :use ((:instance f-run-diff-tm-thm
 
376
                                        (m n)
 
377
                                        (n m))))))
 
378
 
 
379
(defthm floor1-large-1<=
 
380
  (implies
 
381
   (and
 
382
    (realp x)
 
383
    (< 0 x)
 
384
    (standard-numberp x))
 
385
   (i-large (* (i-large-integer) x)))
 
386
  :hints (("Goal" :in-theory (enable i-large))))
 
387
 
 
388
(defthm large-gt-1
 
389
  (implies
 
390
   (and
 
391
    (realp x)
 
392
    (< 0 x)
 
393
    (i-large x))
 
394
   (< 1 x))
 
395
  :hints ((standard-part-hint stable-under-simplificationp clause)
 
396
          ("Goal" :in-theory (enable i-large)
 
397
           :use ((:instance standard-part-<=
 
398
                            (x 1)
 
399
                            (y (/ x)))))))
 
400
 
 
401
(defthm standard-diff-*-large-thm
 
402
  (implies
 
403
   (and
 
404
    (realp x)
 
405
    (realp y)
 
406
    (standard-numberp x)
 
407
    (standard-numberp y)
 
408
    (< x y))
 
409
   (<= (+ (* (i-large-integer) x) 1)
 
410
       (* (i-large-integer) y)))
 
411
  :hints (("Goal" :use ((:instance floor1-large-1<= (x (- y x)))
 
412
                        (:instance large-gt-1
 
413
                                   (x (+ (* -1 (I-LARGE-INTEGER) X)
 
414
                                         (* (I-LARGE-INTEGER) Y))))
 
415
                        (:instance pos-factor-<-thm
 
416
                                   (x 0)
 
417
                                   (y (- y x))
 
418
                                   (a (i-large-integer)))))))
 
419
 
 
420
(defthm abs-standard-numberp
 
421
  (implies
 
422
   (and
 
423
    (realp x)
 
424
    (standard-numberp x))
 
425
   (standard-numberp (abs x))))
 
426
 
 
427
(defthm-std phi-diff-tm-thm
 
428
  (implies
 
429
   (and
 
430
    (realp x)
 
431
    (realp tm1)
 
432
    (realp tm2)
 
433
    (<= 0 tm1)
 
434
    (<= tm1 tm2))
 
435
   (<= (abs (- (phi x tm2)
 
436
               (phi x tm1)))
 
437
       (* (- tm2 tm1) (eexp (* tm2 (L))) (abs (f x)))))
 
438
  :rule-classes nil
 
439
  :hints ((standard-part-hint stable-under-simplificationp clause)
 
440
          ("Goal" :in-theory (disable abs <-CANCEL-DIVISORS)
 
441
           :use ((:instance f-run-diff-tm-thm
 
442
                            (eps (/ (i-large-integer)))
 
443
                            (n (floor1 (* tm1 (i-large-integer))))
 
444
                            (m (floor1 (* tm2 (i-large-integer)))))
 
445
                 (:instance L-STANDARD-THM)
 
446
                 (:instance F-STANDARD-THM)
 
447
                 (:instance standard-diff-*-large-thm
 
448
                            (x TM1)
 
449
                            (y TM2))))))
 
450
 
 
451
;; ----------------------------------------------
 
452
;; The following is the theorem which states
 
453
;; that phi is continuous with respect to time
 
454
;; ----------------------------------------------
 
455
 
 
456
(defthm phi-tm-continuous-thm
 
457
  (implies
 
458
   (and
 
459
    (realp x)
 
460
    (standard-numberp x)
 
461
    (realp tm1)
 
462
    (<= 0 tm1)
 
463
    (i-limited tm1))
 
464
   (equal (standard-part (phi x tm1))
 
465
          (phi x (standard-part tm1))))
 
466
  :hints ((standard-part-hint stable-under-simplificationp clause)
 
467
          ("Goal" :in-theory (disable abs)
 
468
           :cases ((<= tm1 (standard-part tm1))
 
469
                   (< (standard-part tm1) tm1)))
 
470
          ("Subgoal 2" :use ((:instance phi-diff-tm-thm
 
471
                                        (tm1 tm1)
 
472
                                        (tm2 (standard-part tm1)))))
 
473
          ("Subgoal 1" :use ((:instance phi-diff-tm-thm
 
474
                                        (tm2 tm1)
 
475
                                        (tm1 (standard-part tm1)))))))
 
476
 
 
477
(defthm run-plus-thm
 
478
  (implies
 
479
   (and
 
480
    (integerp m)
 
481
    (integerp n)
 
482
    (<= 0 m)
 
483
    (<= 0 n))
 
484
   (equal (run (run x n eps) m eps)
 
485
          (run x (+ m n) eps))))
 
486
 
 
487
(defthm phi-diff-hint-1
 
488
  (implies
 
489
   (and
 
490
    (standard-numberp x1)
 
491
    (standard-numberp x2)
 
492
    (standard-numberp tm)
 
493
    (realp x1)
 
494
    (realp x2)
 
495
    (realp tm)
 
496
    (<= 0 tm))
 
497
   (equal (STANDARD-PART (* (EEXP (* (L) (/ (I-LARGE-INTEGER))
 
498
                                     (FLOOR1 (* (I-LARGE-INTEGER) TM))))
 
499
                            (ABS (+ X1 (* -1 X2)))))
 
500
          (* (EEXP (* (L) TM))
 
501
             (ABS (+ X1 (* -1 X2))))))
 
502
  :rule-classes nil
 
503
  :hints (("Goal" :in-theory (disable *-commut-3way)
 
504
           :use (:instance L-STANDARD-THM))))
 
505
 
 
506
(defthm-std phi-x-diff-thm
 
507
  (implies
 
508
   (and
 
509
    (realp x1)
 
510
    (realp x2)
 
511
    (realp tm)
 
512
    (<= 0 tm))
 
513
   (<= (abs (- (phi x1 tm) (phi x2 tm)))
 
514
       (* (abs (- x1 x2)) (eexp (* tm (L))))))
 
515
  :rule-classes nil
 
516
  :hints ((standard-part-hint stable-under-simplificationp clause)
 
517
          ("Goal" :in-theory (disable abs i-large )
 
518
           :use ((:instance run-diff-limit-eexp-thm
 
519
                            (n (floor1 (* tm (i-large-integer))))
 
520
                            (eps (/ (i-large-integer))))
 
521
                 (:instance phi-diff-hint-1)))))
 
522
 
 
523
(defthm run-x-continuous-thm
 
524
  (implies
 
525
   (and
 
526
    (realp eps)
 
527
    (< 0 eps)
 
528
    (realp x)
 
529
    (i-limited x)
 
530
    (integerp n)
 
531
    (i-limited (* eps n))
 
532
    (<= 0 n))
 
533
   (equal (standard-part (run (standard-part x) n eps))
 
534
          (standard-part (run x n eps))))
 
535
  :hints ((standard-part-hint stable-under-simplificationp clause)
 
536
          ("Goal" :in-theory (disable abs)
 
537
           :do-not-induct t
 
538
           :use ((:instance run-diff-limit-eexp-thm
 
539
                            (x1 x)
 
540
                            (x2 (standard-part x)))))))
 
541
 
 
542
;; -------------------------------------------
 
543
;; The following is the theorem which states
 
544
;; that phi is continuous with respect to x
 
545
;; -------------------------------------------
 
546
 
 
547
(defthm phi-x-continuous-thm
 
548
  (implies
 
549
   (and
 
550
    (realp x)
 
551
    (i-limited x)
 
552
    (realp tm)
 
553
    (standard-numberp tm)
 
554
    (<= 0 tm))
 
555
   (equal (standard-part (phi x tm))
 
556
          (phi (standard-part x) tm)))
 
557
  :hints ((standard-part-hint stable-under-simplificationp clause)
 
558
          ("Goal" :in-theory (disable abs)
 
559
           :use ((:instance phi-x-diff-thm
 
560
                            (x1 x)
 
561
                            (x2 (standard-part x)))))))
 
562
 
 
563
(defthm phi-plus-hint1
 
564
  (implies
 
565
   (and
 
566
    (realp tm1)
 
567
    (realp tm2))
 
568
   (equal (standard-part (* (+ (FLOOR1 (* (I-LARGE-INTEGER) TM1))
 
569
                               (FLOOR1 (* (I-LARGE-INTEGER) TM2)))
 
570
                            (/ (I-LARGE-INTEGER))))
 
571
          (standard-part (* (floor1 (* (i-large-integer) (+ tm1 tm2)))
 
572
                            (/ (i-large-integer))))))
 
573
  :hints ((standard-part-hint stable-under-simplificationp clause)
 
574
          ("Goal" :in-theory (disable <-CANCEL-DIVISORS)
 
575
           :use ((:instance pos-factor-<-thm
 
576
                            (x (+ (* (I-LARGE-INTEGER) TM1)
 
577
                                  (* (I-LARGE-INTEGER) TM2)
 
578
                                  -2))
 
579
                            (y (+ (FLOOR1 (* (I-LARGE-INTEGER) TM1))
 
580
                                  (FLOOR1 (* (I-LARGE-INTEGER) TM2))))
 
581
                            (a (/ (i-large-integer))))
 
582
                 (:instance pos-factor-<=-thm
 
583
                            (x (+ (FLOOR1 (* (I-LARGE-INTEGER) TM1))
 
584
                                  (FLOOR1 (* (I-LARGE-INTEGER) TM2))))
 
585
                            (y (+ (* (I-LARGE-INTEGER) TM1)
 
586
                                  (* (I-LARGE-INTEGER) TM2)))
 
587
                            (a (/ (i-large-integer))))
 
588
                 (:instance pos-factor-<-thm
 
589
                            (x (+ (* (i-large-integer) (+ tm1 tm2)) -1))
 
590
                            (y (floor1 (* (i-large-integer) (+ tm1 tm2))))
 
591
                            (a (/ (i-large-integer))))
 
592
                 (:instance pos-factor-<=-thm
 
593
                            (x (floor1 (* (i-large-integer) (+ tm1 tm2))))
 
594
                            (y (* (i-large-integer) (+ tm1 tm2)))
 
595
                            (a (/ (i-large-integer))))))))
 
596
 
 
597
(defthm tm1+tm2-limited-thm
 
598
  (implies
 
599
   (and
 
600
    (standard-numberp tm1)
 
601
    (standard-numberp tm2)
 
602
    (realp tm1)
 
603
    (realp tm2))
 
604
   (i-limited (* (/ (i-large-integer))
 
605
                 (floor1 (* (i-large-integer) (+ tm1 tm2))))))
 
606
  :rule-classes nil
 
607
  :hints (("Goal" :use ((:instance phi-plus-hint1)
 
608
                        (:instance standard+small->i-limited
 
609
                                   (x (standard-part
 
610
                                       (* (/ (i-large-integer))
 
611
                                          (floor1 (* (i-large-integer)
 
612
                                                     (+ tm1 tm2))))))
 
613
                                   (eps (- (* (/ (i-large-integer))
 
614
                                              (floor1 (* (i-large-integer)
 
615
                                                         (+ tm1 tm2))))
 
616
                                           (standard-part
 
617
                                            (* (/ (i-large-integer))
 
618
                                               (floor1 (* (i-large-integer)
 
619
                                                          (+ tm1 tm2)))))))
 
620
                                   )))))
 
621
 
 
622
;; -------------------------------------------
 
623
;; The following is the theorem which states
 
624
;; that phi is time invariant
 
625
;; -------------------------------------------
 
626
 
 
627
(defthm-std phi-plus-thm
 
628
  (implies
 
629
   (and
 
630
    (realp x)
 
631
    (realp tm1)
 
632
    (realp tm2)
 
633
    (<= 0 tm1)
 
634
    (<= 0 tm2))
 
635
   (equal (phi (phi x tm1) tm2)
 
636
          (phi x (+ tm1 tm2))))
 
637
  :hints (("Goal" :in-theory (disable i-large run-plus-thm)
 
638
           :use ((:instance phi-plus-hint1)
 
639
                 (:instance  tm1+tm2-limited-thm)
 
640
                 (:instance run-plus-thm (n (floor1 (* tm1
 
641
                                                       (i-large-integer))))
 
642
                            (m (floor1 (* tm2
 
643
                                          (i-large-integer))))
 
644
                            (eps (/ (i-large-integer))))
 
645
                 (:instance run-diff-tm-standard-part-thm
 
646
                            (eps (/ (i-large-integer)))
 
647
                            (m (+ (floor1 (* (i-large-integer) tm1))
 
648
                                  (floor1 (* (i-large-integer) tm2))))
 
649
                            (n (floor1 (* (i-large-integer) (+ tm1 tm2)))))
 
650
                 (:instance phi-x-continuous-thm
 
651
                            (x (RUN X
 
652
                                    (FLOOR1 (* (I-LARGE-INTEGER) TM1))
 
653
                                    (/ (I-LARGE-INTEGER))))
 
654
                            (tm tm2))))))
 
655
 
 
656
;; For some reason, enabling the following rule as a
 
657
;; linear lemma may cause ACL2 to stall during simplification
 
658
 
 
659
(defthm floor1-1-thm
 
660
  (implies
 
661
   (and (realp x)
 
662
        (<= 1 x))
 
663
   (< 0 (floor1 x)))
 
664
  :rule-classes nil)
 
665
 
 
666
;; For some reason, enabling the following rewrite rule
 
667
;; may cause ACL2 to stall during simplification
 
668
 
 
669
(defthm floor1-0-thm
 
670
  (implies
 
671
   (and (realp x)
 
672
        (<= 0 x)
 
673
        (< x 1))
 
674
   (equal (floor1 x) 0))
 
675
  :rule-classes nil)
 
676
 
 
677
(defun tm-m (tm eps)
 
678
  (cond
 
679
   ((not (and
 
680
          (realp eps)
 
681
          (< 0 eps)
 
682
          (realp tm)
 
683
          (<= eps tm))) 0)
 
684
   (t (floor1 (/ tm eps)))))
 
685
 
 
686
(defun phi-run (x tm eps)
 
687
  (declare (xargs :measure (tm-m tm eps)
 
688
                  :hints (("Subgoal 1.2"
 
689
                           :use ((:instance floor1-1-thm
 
690
                                            (x (* (/ eps) tm))))))))
 
691
  (cond
 
692
   ((not (and (realp eps)
 
693
              (< 0 eps)
 
694
              (<= eps tm)
 
695
              (realp tm))) (phi x tm))
 
696
   (t (phi-run (phi x eps) (- tm eps) eps))))
 
697
 
 
698
(defthm phi-run-eq-phi-thm
 
699
  (implies
 
700
   (and
 
701
    (realp x)
 
702
    (realp tm)
 
703
    (<= 0 tm)
 
704
    (< 0 eps)
 
705
    (realp eps))
 
706
   (equal (phi-run x tm eps)
 
707
          (phi x tm)))
 
708
  :rule-classes nil)
 
709
 
 
710
(defthm run-equal-thm
 
711
  (implies
 
712
   (and
 
713
    (realp x)
 
714
    (realp eps)
 
715
    (< 0 eps)
 
716
    (integerp n)
 
717
    (<= 0 n))
 
718
   (equal (+ x (* eps n (f x)) (- (f-sum x n eps) (* n eps (f x))))
 
719
          (run x n eps)))
 
720
  :hints (("Goal" :use ((:instance run-f-sum-thm)))))
 
721
 
 
722
(defthm-std phi-equal-thm
 
723
  (implies
 
724
   (and
 
725
    (realp x)
 
726
    (realp tm)
 
727
    (<= 0 tm))
 
728
   (equal (+ x (* tm (f x)) (resid-tm x tm))
 
729
          (phi x tm)))
 
730
  :hints (("Goal" :use ((:instance F-STANDARD-THM)
 
731
                        (:instance run-f-sum-thm
 
732
                                   (eps (/ (i-large-integer)))
 
733
                                   (n (floor1 (* tm (i-large-integer))))
 
734
                                   )))))
 
735
 
 
736
(defthm step-resid-thm
 
737
  (implies
 
738
   (and
 
739
    (realp x)
 
740
    (realp eps)
 
741
    (< 0 eps)
 
742
    (integerp n)
 
743
    (<= 0 n))
 
744
   (equal (+ (resid x n eps)
 
745
             (- (* eps (f (run x n eps)))
 
746
                (* eps (f x))))
 
747
          (resid x (+ n 1) eps))))
 
748
 
 
749
(defthm resid-type
 
750
  (implies
 
751
   (and
 
752
    (realp x)
 
753
    (realp eps)
 
754
    (integerp n))
 
755
   (realp (resid x n eps)))
 
756
  :rule-classes :type-prescription)
 
757
 
 
758
(defthm-std resid-tm-type
 
759
  (implies
 
760
   (and
 
761
    (realp x)
 
762
    (realp tm))
 
763
   (realp (resid-tm x tm)))
 
764
  :rule-classes :type-prescription)
 
765
 
 
766
(defthm step-resid-bound-thm
 
767
  (implies
 
768
   (and
 
769
    (realp x)
 
770
    (realp eps)
 
771
    (< 0 eps)
 
772
    (integerp n)
 
773
    (< 0 n))
 
774
   (<= (abs (resid x n eps))
 
775
       (+ (abs (resid x (- n 1) eps))
 
776
          (* eps eps (L) (- n 1)
 
777
             (eexp (* eps (- n 1) (L)))
 
778
             (abs (f x))))))
 
779
  :rule-classes nil
 
780
  :hints (("Goal" :in-theory (disable abs step-resid-thm resid)
 
781
           :use ((:instance f-sum-exp-bound-thm (n (- n 1)))
 
782
                 (:instance abs-triangular-inequality-thm
 
783
                            (x (RESID X (+ -1 N) EPS))
 
784
                            (y (- (* eps (f (run x (- n 1) eps)))
 
785
                                  (* eps (f x)))))
 
786
                 (:instance abs-pos-*-left-thm
 
787
                            (x eps)
 
788
                            (y (+ (* -1 (F X))
 
789
                                  (* (F (RUN X (+ -1 N) EPS))))))
 
790
                 (:instance f-lim-thm (x1 (run x (- n 1) eps))
 
791
                            (x2 x))
 
792
                 (:instance pos-factor-<=-thm
 
793
                            (x (ABS (+ (* -1 (F X))
 
794
                                       (* (F (RUN X (+ -1 N) EPS))))))
 
795
                            (y (* (L)
 
796
                                  (ABS (+ (* -1 X)
 
797
                                          (RUN X (+ -1 N) EPS)))))
 
798
                            (a eps))
 
799
                 (:instance run-f-sum-thm (n (- n 1)))
 
800
                 (:instance step-resid-thm (n (- n 1)))
 
801
                 (:instance pos-factor-<=-thm
 
802
                            (x (abs (f-sum x (- n 1) eps)))
 
803
                            (y (* (- n 1)
 
804
                                  eps
 
805
                                  (eexp (* eps (- n 1) (L)))
 
806
                                  (abs (f x))))
 
807
                            (a (* eps (L))))))))
 
808
 
 
809
(defthm resid-bound-thm
 
810
  (implies
 
811
   (and
 
812
    (realp x)
 
813
    (realp eps)
 
814
    (< 0 eps)
 
815
    (integerp n)
 
816
    (<= 0 n))
 
817
   (<= (abs (resid x n eps))
 
818
       (* n n eps eps (L) (eexp (* n eps (L))) (abs (f x)))))
 
819
  :rule-classes nil
 
820
  :hints (("Goal" :in-theory (disable abs)
 
821
           :do-not '(generalize)
 
822
           :do-not-induct t
 
823
           :induct (f-sum x n eps))
 
824
          ("Subgoal *1/2" :in-theory (disable abs resid
 
825
                                              <-*-LEFT-CANCEL)
 
826
           :use ((:instance step-resid-bound-thm)
 
827
                 (:instance pos-factor-<=-thm
 
828
                            (x 0)
 
829
                            (y (- n 1))
 
830
                            (a (* (L) eps)))
 
831
                 (:instance pos-factor-<=-thm
 
832
                            (x 1)
 
833
                            (y (eexp (* eps (L))))
 
834
                            (a (* (L) EPS EPS N N
 
835
                                  (ABS (F X))
 
836
                                  (EEXP (+ (* -1 (L) EPS)
 
837
                                           (* (L) EPS N)))))
 
838
                            )))))
 
839
 
 
840
(defthm tm-fun-rw-5-thm
 
841
  (implies
 
842
   (and
 
843
    (realp a)
 
844
    (realp b)
 
845
    (realp c)
 
846
    (realp tm)
 
847
    (standard-numberp tm))
 
848
   (equal (* (/ (I-LARGE-INTEGER)) a b
 
849
             (FLOOR1 (* (I-LARGE-INTEGER) TM)) c)
 
850
          (* (tm-fun tm) a b c)))
 
851
  :hints (("Goal" :in-theory (e/d (tm-fun) (tm-fun-rw-1-thm
 
852
                                            tm-fun-rw-2-thm
 
853
                                            tm-fun-rw-3-thm
 
854
                                            tm-fun-rw-4-thm)))))
 
855
 
 
856
(defthm tm-fun-rw-6-thm
 
857
  (implies
 
858
   (and
 
859
    (realp a)
 
860
    (realp b)
 
861
    (realp c)
 
862
    (realp d)
 
863
    (realp tm)
 
864
    (standard-numberp tm))
 
865
   (equal (* (/ (I-LARGE-INTEGER)) a b c
 
866
             (FLOOR1 (* (I-LARGE-INTEGER) TM)) d)
 
867
          (* (tm-fun tm) a b c d)))
 
868
  :hints (("Goal" :in-theory (e/d (tm-fun) (tm-fun-rw-1-thm
 
869
                                            tm-fun-rw-2-thm
 
870
                                            tm-fun-rw-3-thm
 
871
                                            tm-fun-rw-4-thm
 
872
                                            tm-fun-rw-5-thm)))))
 
873
 
 
874
(defthm-std resid-tm-bound-thm
 
875
  (implies
 
876
   (and
 
877
    (realp x)
 
878
    (realp tm)
 
879
    (<= 0 tm))
 
880
   (<= (abs (resid-tm x tm))
 
881
       (* tm tm (L) (eexp (* tm (L))) (abs (f x)))))
 
882
  :hints ((standard-part-hint stable-under-simplificationp clause)
 
883
          ("Goal" :in-theory (disable abs <-CANCEL-DIVISORS)
 
884
           :use ((:instance F-STANDARD-THM)
 
885
                 (:instance L-STANDARD-THM)
 
886
                 (:instance resid-bound-thm
 
887
                            (eps (/ (i-large-integer)))
 
888
                            (n (floor1 (* tm (i-large-integer)))))))))
 
889
 
 
890
(defthm tm-floor-0-thm
 
891
  (implies
 
892
   (and
 
893
    (realp tm)
 
894
    (realp eps)
 
895
    (<= 0 tm)
 
896
    (< 0 eps)
 
897
    (< tm eps))
 
898
   (equal (FLOOR1 (* (/ EPS) TM))  0))
 
899
  :hints (("Goal" :use ((:instance floor1-0-thm (x (/ tm eps)))))))
 
900
 
 
901
(defthm-std phi-0-thm
 
902
  (implies
 
903
   (realp x)
 
904
   (equal (phi x 0)
 
905
          x)))
 
906
 
 
907
(defun tm-induct (tm eps)
 
908
  (declare (xargs :measure (tm-m tm eps)
 
909
                  :hints (("Subgoal 1.2"
 
910
                           :use ((:instance floor1-1-thm
 
911
                                            (x (* (/ eps) tm))))))))
 
912
  (cond
 
913
   ((not (and
 
914
          (realp eps)
 
915
          (< 0 eps)
 
916
          (realp tm)
 
917
          (<= eps tm))) tm)
 
918
   (t (tm-induct (- tm eps)
 
919
                 eps))))
 
920
 
 
921
(defthm phi-eps-step-thm
 
922
  (implies
 
923
   (and
 
924
    (realp x1)
 
925
    (realp x2)
 
926
    (realp eps)
 
927
    (< 0 eps))
 
928
   (<= (abs (- (phi x1 eps) (step1 x2 eps)))
 
929
       (+ (* (abs (- x1 x2)) (+ 1 (* eps (L))))
 
930
          (* eps eps (L) (eexp (* eps (L))) (abs (f x1))))))
 
931
  :rule-classes nil
 
932
  :hints (("Goal" :in-theory (disable abs)
 
933
           :do-not '(generalize)
 
934
           :do-not-induct t
 
935
           :use ((:instance phi-equal-thm (x x1) (tm eps))
 
936
                 (:instance abs-triangular-inequality-thm
 
937
                            (x (+ X1 (* -1 X2)))
 
938
                            (y (+(RESID-TM X1 EPS)
 
939
                                 (* EPS (F X1))
 
940
                                 (* -1 EPS (F X2)))))
 
941
                 (:instance abs-triangular-inequality-thm
 
942
                            (x (RESID-TM X1 EPS))
 
943
                            (y (+ (* EPS (F X1))
 
944
                                  (* -1 EPS (F X2)))))
 
945
                 (:instance resid-tm-bound-thm
 
946
                            (tm eps)
 
947
                            (x x1))
 
948
                 (:instance abs-pos-*-left-thm
 
949
                            (x eps)
 
950
                            (y (- (F X1)
 
951
                                  (F X2))))
 
952
                 (:instance f-lim-thm)
 
953
                 (:instance pos-factor-<=-thm
 
954
                            (x (abs (- (f x1) (f x2))))
 
955
                            (y (* (L) (abs (- x1 x2))))
 
956
                            (a eps))))))
 
957
 
 
958
(defthm phi-phi-run-thm
 
959
  (implies
 
960
   (and
 
961
    (realp eps)
 
962
    (realp x)
 
963
    (realp tm)
 
964
    (<= 0 tm)
 
965
    (<= eps tm)
 
966
    (< 0 eps))
 
967
   (equal (phi (phi-run x
 
968
                        (+ (* -1 EPS)
 
969
                           (* EPS
 
970
                              (FLOOR1 (* (/ EPS) TM))))
 
971
                        eps) eps)
 
972
          (phi-run x (* eps (floor1 (/ tm eps))) eps)))
 
973
  :hints (("Goal" :induct (phi-run x tm eps)
 
974
           :do-not '(generalize))
 
975
          ("Subgoal *1/4" :use ((:instance floor1-1-thm
 
976
                                           (x (/ tm eps)))
 
977
                                (:instance pos-factor-<=-thm
 
978
                                           (x 1)
 
979
                                           (y (floor1 (/ tm eps)))
 
980
                                           (a eps))))
 
981
          ("Subgoal *1/2" :use ((:instance floor1-1-thm (x (/ tm eps)))
 
982
                                (:instance pos-factor-<=-thm
 
983
                                           (x 1)
 
984
                                           (y (floor1 (/ tm eps)))
 
985
                                           (a eps))))
 
986
          ("Subgoal *1/1" :use ((:instance tm-floor-0-thm
 
987
                                           (tm (- tm eps)))
 
988
                                (:instance distributivity
 
989
                                           (y (FLOOR1 (* (/ EPS) TM)))
 
990
                                           (z -1)
 
991
                                           (x eps))))))
 
992
 
 
993
(defthm f-standard-part-thm
 
994
  (implies
 
995
   (and
 
996
    (realp x)
 
997
    (i-limited x))
 
998
   (equal (standard-part (f x))
 
999
          (f (standard-part x))))
 
1000
  :hints ((standard-part-hint stable-under-simplificationp clause)
 
1001
          ("Goal" :in-theory (disable abs STANDARDP-STANDARD-PART)
 
1002
           :use ((:instance F-STANDARD-THM
 
1003
                            (x (standard-part x)))
 
1004
                 (:instance f-lim-thm
 
1005
                            (x1 (standard-part x))
 
1006
                            (x2 x))
 
1007
                 (:instance standardp-standard-part)))))
 
1008
 
 
1009
(defthm-std f-phi-bound-thm
 
1010
  (implies
 
1011
   (and
 
1012
    (realp x)
 
1013
    (realp tm)
 
1014
    (<= 0 tm))
 
1015
   (<= (abs (f (phi x tm)))
 
1016
       (* (eexp (* tm (L))) (abs (f x)))))
 
1017
  :hints ((standard-part-hint stable-under-simplificationp clause)
 
1018
          ("Goal" :in-theory (disable abs)
 
1019
           :use ((:instance L-STANDARD-THM)
 
1020
                            (:instance f-run-bound-thm
 
1021
                            (eps (/ (i-large-integer)))
 
1022
                            (n (floor1 (* tm (i-large-integer))))
 
1023
                            )))))
 
1024
 
 
1025
(defthm phi-eps-arith-hint
 
1026
  (implies
 
1027
   (and
 
1028
    (realp tm)
 
1029
    (< 0 eps)
 
1030
    (realp eps))
 
1031
   (equal
 
1032
    (* (EEXP (* (L) EPS))
 
1033
       (FLOOR1 (* (/ EPS) TM))
 
1034
       (EEXP (+ (* -1 (L) EPS)
 
1035
                (* (L) EPS (FLOOR1 (* (/ EPS) TM))))))
 
1036
    (* (FLOOR1 (* (/ EPS) TM))
 
1037
       (EEXP (* (L) EPS (FLOOR1 (* (/ EPS) TM)))))))
 
1038
  :hints (("Goal" :in-theory (disable *-commut-3way)
 
1039
           :use ((:instance *-commut-3way
 
1040
                            (x (EEXP (* (L) EPS)))
 
1041
                            (y (FLOOR1 (* (/ EPS) TM)))
 
1042
                            (z (EEXP (+ (* -1 (L) EPS)
 
1043
                                        (* (L) EPS
 
1044
                                           (FLOOR1 (* (/ EPS) TM))))))
 
1045
                            )))))
 
1046
 
 
1047
(defthm phi-eps-thm
 
1048
  (implies
 
1049
   (and
 
1050
    (realp x)
 
1051
    (realp tm)
 
1052
    (realp eps)
 
1053
    (<= 0 tm)
 
1054
    (< 0 eps))
 
1055
   (<= (abs (- (phi-run x
 
1056
                        (* eps (floor1 (/ tm eps)))
 
1057
                        eps)
 
1058
               (run x
 
1059
                    (floor1 (/ tm eps))
 
1060
                    eps)))
 
1061
       (* eps eps
 
1062
          (floor1 (/ tm eps))
 
1063
          (L)
 
1064
          (abs (f x))
 
1065
          (eexp (* eps (floor1 (/ tm eps)) (L))))))
 
1066
  :rule-classes nil
 
1067
  :hints (("Goal" :in-theory (disable abs)
 
1068
           :induct (tm-induct tm eps)
 
1069
           :do-not '(generalize))
 
1070
          ("Subgoal *1/2" :in-theory (disable abs run step1)
 
1071
           :use ((:instance floor1-1-thm (x (/ tm eps)))
 
1072
                 (:instance pos-factor-<=-thm
 
1073
                            (x 1)
 
1074
                            (y (floor1 (/ tm eps)))
 
1075
                            (a eps))))
 
1076
          ("Subgoal *1/2.1" :in-theory (disable abs run step1
 
1077
                                                <-*-left-cancel
 
1078
                                                <-cancel-divisors)
 
1079
           :use ((:instance phi-run-eq-phi-thm
 
1080
                            (tm (+ (* -1 EPS)
 
1081
                                   (* EPS (FLOOR1 (* (/ EPS) TM))))))
 
1082
                 (:instance phi-run-eq-phi-thm
 
1083
                            (tm (* EPS (FLOOR1 (* (/ EPS) TM)))))
 
1084
                 (:instance 1+x-<=eexp-thm (x (* eps (L))))
 
1085
                 (:instance phi-eps-arith-hint)
 
1086
                 (:instance pos-factor-<=-thm
 
1087
                            (x (+ 1 (* eps (L))))
 
1088
                            (y (eexp (* eps (L))))
 
1089
                            (a (ABS (+ (* -1
 
1090
                                          (RUN X
 
1091
                                               (+ -1
 
1092
                                                  (FLOOR1
 
1093
                                                   (* (/ EPS) TM)))
 
1094
                                               EPS))
 
1095
                                       (PHI-RUN X
 
1096
                                                (+ (* -1 EPS)
 
1097
                                                   (* EPS
 
1098
                                                      (FLOOR1
 
1099
                                                       (* (/ EPS) TM))))
 
1100
                                                EPS)))))
 
1101
                 (:instance pos-factor-<=-thm
 
1102
                            (x (ABS (+ (* -1
 
1103
                                          (RUN X
 
1104
                                               (+ -1 (FLOOR1
 
1105
                                                      (* (/ EPS) TM)))
 
1106
                                               EPS))
 
1107
                                       (PHI-RUN X
 
1108
                                                (+ (* -1 EPS)
 
1109
                                                   (* EPS
 
1110
                                                      (FLOOR1
 
1111
                                                       (* (/ EPS) TM))))
 
1112
                                                EPS))))
 
1113
                            (y (+ (* -1 (L)
 
1114
                                     EPS EPS (ABS (F X))
 
1115
                                     (EEXP (+ (* -1 (L) EPS)
 
1116
                                              (* (L) EPS
 
1117
                                                 (FLOOR1
 
1118
                                                  (* (/ EPS) TM))))))
 
1119
                                  (* (L)
 
1120
                                     EPS EPS (ABS (F X))
 
1121
                                     (FLOOR1 (* (/ EPS) TM))
 
1122
                                     (EEXP (+ (* -1 (L) EPS)
 
1123
                                              (* (L) EPS
 
1124
                                                 (FLOOR1
 
1125
                                                  (* (/ EPS) TM)))))
 
1126
                                     )))
 
1127
                            (a (EEXP (* (L) EPS))))
 
1128
                 (:instance pos-factor-<=-thm
 
1129
                            (x (ABS (F (PHI X
 
1130
                                            (+ (* -1 EPS)
 
1131
                                               (* EPS
 
1132
                                                  (FLOOR1
 
1133
                                                   (* (/ EPS) TM))))
 
1134
                                            ))))
 
1135
                            (y (* (ABS (F X))
 
1136
                                  (EEXP (+ (* -1 (L) EPS)
 
1137
                                           (* (L) EPS
 
1138
                                              (FLOOR1
 
1139
                                               (* (/ EPS) TM))
 
1140
                                              )))))
 
1141
                            (a (* (L) EPS EPS (EEXP (* (L) EPS)))))
 
1142
                 (:instance phi-eps-step-thm
 
1143
                            (x1 (phi-run x
 
1144
                                         (* eps
 
1145
                                            (- (floor1 (/ tm eps)) 1))
 
1146
                                         eps))
 
1147
                            (x2 (run x (- (floor1
 
1148
                                           (/ tm eps)) 1) eps)))
 
1149
                 (:instance f-phi-bound-thm
 
1150
                            (tm (+ (* -1 EPS)
 
1151
                                   (* EPS (FLOOR1 (* (/ EPS) TM)))))
 
1152
                            )))))
 
1153
 
 
1154
(defthm phi-any-small-eps-thm
 
1155
  (implies
 
1156
   (and
 
1157
    (realp x)
 
1158
    (realp tm)
 
1159
    (standard-numberp x)
 
1160
    (standard-numberp tm)
 
1161
    (realp eps)
 
1162
    (<= 0 tm)
 
1163
    (< 0 eps)
 
1164
    (i-small eps))
 
1165
   (equal (standard-part (phi x tm))
 
1166
          (standard-part (run x (floor1 (/ tm eps)) eps))))
 
1167
  :hints ((standard-part-hint stable-under-simplificationp clause)
 
1168
          ("Goal" :in-theory (disable abs phi)
 
1169
           :use ((:instance small-are-limited (x eps))
 
1170
                 (:instance phi-eps-thm)
 
1171
                 (:instance phi-run-eq-phi-thm
 
1172
                            (tm (* EPS (FLOOR1 (* (/ EPS) TM)))))))))
 
1173
 
 
1174
;; ----------------------------------------------
 
1175
;; The following is the theorem which states
 
1176
;; that run, hence phi, is independent of the
 
1177
;; choice of eps.
 
1178
;; ----------------------------------------------
 
1179
 
 
1180
(defthm run-any-small-eps-thm
 
1181
  (implies
 
1182
   (and
 
1183
    (realp x)
 
1184
    (realp tm)
 
1185
    (standard-numberp x)
 
1186
    (standard-numberp tm)
 
1187
    (realp eps)
 
1188
    (<= 0 tm)
 
1189
    (< 0 eps)
 
1190
    (i-small eps))
 
1191
   (equal (standard-part (run x
 
1192
                              (floor1 (* tm (i-large-integer)))
 
1193
                              (/ (i-large-integer))))
 
1194
          (standard-part (run x
 
1195
                              (floor1 (/ tm eps))
 
1196
                              eps))))
 
1197
  :hints (("Goal" :use ((:instance  phi-any-small-eps-thm)))))