← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2006/greve/nary/nth-rules.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/workshops/2006/greve/nary/nth-rules.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
(defthm equal-cons-cases
 
4
  (equal (equal (cons a b) c)
 
5
         (and (consp c)
 
6
              (equal a (car c))
 
7
              (equal b (cdr c)))))
 
8
 
 
9
(defun lastatom (x)
 
10
  (if (consp x) (lastatom (cdr x))
 
11
    x))
 
12
 
 
13
(defthm lastatom-update-nth-<
 
14
  (implies
 
15
   (< (nfix a) (len x))
 
16
   (equal (lastatom (update-nth a v x))
 
17
          (lastatom x))))
 
18
 
 
19
(defthm lastatom-update-nth->
 
20
  (implies
 
21
   (not (< (nfix a) (len x)))
 
22
   (equal (lastatom (update-nth a v x))
 
23
          nil)))
 
24
 
 
25
(defthm lastatom-update-nth
 
26
  (equal (lastatom (update-nth a v x))
 
27
         (if (< (nfix a) (len x))
 
28
             (lastatom x)
 
29
           nil)))
 
30
 
 
31
(defun nfix-equiv (a b)
 
32
  (equal (nfix a)
 
33
         (nfix b)))
 
34
 
 
35
(defthmd equal-nfix-rewrite
 
36
  (iff (equal (nfix a) b)
 
37
       (and (natp b)
 
38
            (nfix-equiv a b))))
 
39
 
 
40
(theory-invariant 
 
41
 (incompatible 
 
42
  (:definition nfix-equiv)
 
43
  (:rewrite equal-nfix-rewrite)
 
44
  ))
 
45
 
 
46
(defequiv nfix-equiv)
 
47
 
 
48
(defcong nfix-equiv equal (nth a x) 1
 
49
  :hints (("goal" :in-theory (enable nth))))
 
50
 
 
51
(defcong nfix-equiv equal (update-nth a v x) 1
 
52
  :hints (("goal" :in-theory (enable update-nth))))
 
53
 
 
54
(defun nmx-induction (n m x)
 
55
  (if (zp n) x
 
56
    (if (zp m) n
 
57
      (nmx-induction (1- n) (1- m) (cdr x)))))
 
58
 
 
59
(defthm update-nth-of-update-nth
 
60
  (implies
 
61
   (nfix-equiv a b)
 
62
   (equal (update-nth a v (update-nth b w x))
 
63
          (update-nth a v x)))
 
64
  :hints (("Goal" :induct (nmx-induction a b x)
 
65
           :in-theory (enable update-nth))))
 
66
 
 
67
(defthm update-nth-over-update-nth
 
68
  (implies
 
69
   (not (nfix-equiv a b))
 
70
   (equal (update-nth a v (update-nth b w x))
 
71
          (update-nth b w (update-nth a v x))))
 
72
  :hints (("Goal" :induct (nmx-induction a b x)
 
73
           :in-theory (enable update-nth))))
 
74
 
 
75
(defthm nfix-equiv-nfix
 
76
  (nfix-equiv (nfix x) x))
 
77
 
 
78
(defund clr-nth (a x)
 
79
  (update-nth a nil x))
 
80
 
 
81
(defthm lastatom-clr-nth
 
82
  (equal (lastatom (clr-nth a x))
 
83
         (if (< (nfix a) (len x))
 
84
             (lastatom x)
 
85
           nil))
 
86
  :hints (("Goal" :in-theory (enable clr-nth))))
 
87
 
 
88
(defthm len-clr-nth
 
89
  (equal (len (clr-nth a x))
 
90
         (max (1+ (nfix a)) (len x)))
 
91
  :hints (("Goal" :in-theory (enable clr-nth))))
 
92
 
 
93
(defcong nfix-equiv equal (clr-nth a x) 1
 
94
  :hints (("goal" :in-theory (enable clr-nth))))
 
95
 
 
96
(defthm clr-nth-defn
 
97
  (equal (clr-nth n x)
 
98
         (if (zp n) (cons nil (cdr x))
 
99
           (cons (car x)
 
100
                 (clr-nth (1- n) (cdr x)))))
 
101
  :hints (("Goal" :in-theory (enable clr-nth update-nth)))
 
102
  :rule-classes (:definition))
 
103
 
 
104
(defthm open-clr-nth
 
105
  (and
 
106
   (implies
 
107
    (not (zp n))
 
108
    (equal (clr-nth n x)
 
109
           (cons (car x)
 
110
                 (clr-nth (1- n) (cdr x)))))
 
111
   (implies
 
112
    (zp n)
 
113
    (equal (clr-nth n x)
 
114
           (cons nil (cdr x))))))
 
115
 
 
116
(defthm open-update-nth
 
117
  (and
 
118
   (implies
 
119
    (not (zp n))
 
120
    (equal (update-nth n v x)
 
121
           (cons (car x)
 
122
                 (update-nth (1- n) v (cdr x)))))
 
123
   (implies
 
124
    (zp n)
 
125
    (equal (update-nth n v x)
 
126
           (cons v (cdr x))))))
 
127
 
 
128
(defthm clr-nth-update-nth
 
129
  (equal (clr-nth a (update-nth b v x))
 
130
         (if (nfix-equiv a b) (clr-nth a x)
 
131
           (update-nth b v (clr-nth a x))))
 
132
  :hints (("Goal" :in-theory (enable clr-nth))))
 
133
 
 
134
(defthm clr-nth-of-clr-nth
 
135
  (equal (clr-nth a (clr-nth a x))
 
136
         (clr-nth a x))
 
137
  :hints (("goal" :in-theory (enable clr-nth))))
 
138
 
 
139
(defthm clr-nth-over-clr-nth
 
140
  (equal (clr-nth a (clr-nth b x))
 
141
         (clr-nth b (clr-nth a x)))
 
142
  :hints (("goal" :in-theory (enable clr-nth))))
 
143
 
 
144
(defthm nth-clr-nth
 
145
  (equal (nth a (clr-nth b x))
 
146
         (if (nfix-equiv a b) nil
 
147
           (nth a x)))
 
148
  :hints (("Goal" :in-theory (enable clr-nth))))
 
149
 
 
150
(defun equal-nth-conclusion (a x y)
 
151
  (and (equal (lastatom x) (lastatom y))
 
152
       (equal (len x) (len y))
 
153
       (equal (nth a x) (nth a y))
 
154
       (equal (clr-nth a x)
 
155
              (clr-nth a y))))
 
156
 
 
157
(defthm open-equal-nth-conclusion
 
158
  (equal (equal-nth-conclusion n x y)
 
159
         (if (zp n) (if (and (consp x) (consp y))
 
160
                        (and (equal (car x) (car y))
 
161
                             (equal (cdr x) (cdr y)))
 
162
                      (equal x y))
 
163
           (if (and (consp x)
 
164
                    (consp y))
 
165
               (and (equal (car x) (car y))
 
166
                    (equal-nth-conclusion (1- n) (cdr x) (cdr y)))
 
167
             (equal x y))))
 
168
  :rule-classes (:definition))
 
169
  
 
170
(defun equal-nth-conclusion-fn (n x y)
 
171
  (if (zp n) (if (and (consp x) (consp y))
 
172
                 (and (equal (car x) (car y))
 
173
                      (equal (cdr x) (cdr y)))
 
174
               (equal x y))
 
175
    (if (and (consp x)
 
176
             (consp y))
 
177
        (and (equal (car x) (car y))
 
178
             (equal-nth-conclusion-fn (1- n) (cdr x) (cdr y)))
 
179
      (equal x y))))
 
180
 
 
181
(defthmd equal-nth-conclusion-fn-to-equal-nth-conclusion
 
182
  (equal (equal-nth-conclusion n x y)
 
183
         (equal-nth-conclusion-fn n x y)))
 
184
 
 
185
(defthm equal-nth-conclusion-fn-to-equal
 
186
  (equal (equal-nth-conclusion-fn n x y)
 
187
         (equal x y)))
 
188
 
 
189
(defthmd equal-to-nth-reduction
 
190
  (equal (equal x y)
 
191
         (equal-nth-conclusion n x y))
 
192
  :hints (("Goal" :in-theory '(equal-nth-conclusion-fn-to-equal-nth-conclusion
 
193
                               equal-nth-conclusion-fn-to-equal))))
 
194
 
 
195
(defthm equal-update-nth-reduction
 
196
  (equal (equal (update-nth n v x) y)
 
197
         (and (< (nfix n) (len y))
 
198
              (equal v (nth n y))
 
199
              (equal (clr-nth n x)
 
200
                     (clr-nth n y))))
 
201
  :hints (("Goal" :use (:instance equal-to-nth-reduction
 
202
                                  (x (update-nth n v x))))))
 
203
 
 
204
(defthm update-nth-nth
 
205
  (implies
 
206
   (< (nfix n) (len x))
 
207
   (equal (update-nth n (nth n x) x) x)))
 
208
 
 
209
#| nil-list
 
210
 
 
211
(defun nil-list (n v)
 
212
  (if (zp n) (list v)
 
213
    (cons nil (nil-list (1- n) v))))
 
214
 
 
215
(defthm update-nth-to-append
 
216
  (implies
 
217
   (<= (len x) (nfix n))
 
218
   (equal (update-nth n v x)
 
219
          (append x (nil-list (- (nfix n) (len x)) v))))
 
220
  :hints (("Goal" :in-theory (enable append update-nth))))
 
221
 
 
222
(defthm nth-nil-list-nfix-equiv
 
223
  (implies
 
224
   (nfix-equiv a m)
 
225
   (equal (nth a (nil-list m v)) v))
 
226
  :hints (("Goal" :in-theory (enable nth))))
 
227
 
 
228
(defthm nth-nil-list-not-nfix-equiv
 
229
  (implies
 
230
   (not (nfix-equiv a m))
 
231
   (equal (nth a (nil-list m v)) nil))
 
232
  :hints (("Goal" :induct (nm-induction a m)
 
233
           :in-theory (enable nth))))
 
234
 
 
235
(defthm nth-nil-list
 
236
  (equal (nth a (nil-list m v))
 
237
         (if (nfix-equiv a m) v
 
238
           nil))
 
239
  :hints (("Goal" :in-theory 
 
240
           '(nth-nil-list-not-nfix-equiv 
 
241
             nth-nil-list-nfix-equiv))))
 
242
 
 
243
(defthm nthcdr-nil-list
 
244
  (equal (nthcdr n (nil-list m v))
 
245
         (if (<= (nfix n) (nfix m))
 
246
             (nil-list (- (nfix m) (nfix n)) v)
 
247
           nil))
 
248
  :hints (("Goal" :induct (nm-induction n m)
 
249
           :in-theory (enable nthcdr))))
 
250
 
 
251
(xxinclude-book "basic" :dir :lists)
 
252
 
 
253
(defthm firstn-nil-list
 
254
  (implies
 
255
   (not (zp n))
 
256
   (equal (firstn n (nil-list m v))
 
257
          (if (<= (nfix n) (nfix m))
 
258
              (nil-list (1- (nfix n)) nil)
 
259
            (nil-list m v))))
 
260
  :hints (("Goal" :induct (nm-induction n m)
 
261
           :in-theory (enable firstn))))
 
262
 
 
263
(defthm car-nil-list-nil
 
264
  (equal (car (nil-list n nil))
 
265
         nil))
 
266
 
 
267
|#
 
268
 
 
269
#| equal append rules ..
 
270
 
 
271
(defthm equal-append-append-tail-equal
 
272
  (equal (equal (append x y) (append z y))
 
273
         (list::equiv x z))
 
274
  :hints (("goal" :induct (list::len-len-induction x z)
 
275
           :in-theory (enable append))))
 
276
 
 
277
(defthmd equal-to-equiv
 
278
  (equal (equal x y)
 
279
         (and
 
280
          (list::equiv x y)
 
281
          (equal (lastatom x) (lastatom y))))
 
282
  :hints (("goal" :induct (list::len-len-induction x y))))
 
283
 
 
284
(defun equal-append-append-case (x a y b)
 
285
  (and (list::equiv x (firstn (len x) a))
 
286
       (list::equiv (firstn (- (len a) (len x)) y)
 
287
                    (nthcdr (len x) a))
 
288
       (equal (nthcdr (- (len a) (len x)) y)
 
289
              b)))
 
290
 
 
291
(defthm equiv-append-reduction-1
 
292
  (equal (list::equiv (append x y) z)
 
293
         (and (list::equiv x (firstn (len x) z))
 
294
              (list::equiv y (nthcdr (len x) z))))
 
295
  :hints (("Goal" :in-theory (e/d (LIST::EQUAL-APPEND-REDUCTION! list::equiv)
 
296
                                  (LIST::LIST-EQUIV-HACK LIST::EQUAL-OF-FIXES)))))
 
297
 
 
298
(defthm equiv-append-reduction-2
 
299
  (equal (list::equiv z (append x y))
 
300
         (and (list::equiv x (firstn (len x) z))
 
301
              (list::equiv y (nthcdr (len x) z))))
 
302
  :hints (("Goal" :in-theory (e/d (LIST::EQUAL-APPEND-REDUCTION! list::equiv)
 
303
                                  (LIST::LIST-EQUIV-HACK LIST::EQUAL-OF-FIXES)))))
 
304
 
 
305
(defthmd equal-append-append-reduction2!
 
306
  (equal (equal (append x y) (append a b))
 
307
         (if (< (len x) (len a))
 
308
             (equal-append-append-case x a y b)
 
309
           (equal-append-append-case a x b y)))
 
310
  :hints (("goal" :in-theory '(LIST::EQUAL-APPEND-REDUCTION!))
 
311
          (and stable-under-simplificationp
 
312
               '(:in-theory (current-theory :here)))
 
313
          (and stable-under-simplificationp
 
314
               '(:in-theory '(LIST::EQUAL-APPEND-REDUCTION!)))
 
315
          (and stable-under-simplificationp
 
316
               '(:in-theory (current-theory :here)))))
 
317
 
 
318
|#
 
319
 
 
320
(in-theory (disable nfix nfix-equiv))
 
321
(in-theory (enable equal-nfix-rewrite))
 
322
(in-theory (disable nth update-nth))
 
323
 
 
324
(defun nfix-list (list)
 
325
  (if (consp list)
 
326
      (cons (nfix (car list))
 
327
            (nfix-list (cdr list)))
 
328
    nil))
 
329
 
 
330
(defun nfix-list-equiv (x y)
 
331
  (equal (nfix-list x)
 
332
         (nfix-list y)))
 
333
 
 
334
(defequiv nfix-list-equiv)
 
335
 
 
336
(defthm open-nfix-list-equiv 
 
337
  (and
 
338
   (implies
 
339
    (consp x)
 
340
    (equal (nfix-list-equiv x y)
 
341
           (and (consp y)
 
342
                (equal (nfix (car x))
 
343
                       (nfix (car y)))
 
344
                (nfix-list-equiv (cdr x) (cdr y)))))
 
345
   (implies
 
346
    (not (consp x))
 
347
    (equal (nfix-list-equiv x y)
 
348
           (not (consp y))))))
 
349
  
 
350
(in-theory (disable nfix-list-equiv))
 
351
 
 
352
 
 
353
(defun nth* (list st)
 
354
  (if (consp list)
 
355
      (cons (nth (car list) st)
 
356
            (nth* (cdr list) st))
 
357
    nil))
 
358
 
 
359
(defund nth*-equiv (list st1 st2)
 
360
  (equal (nth* list st1)
 
361
         (nth* list st2)))
 
362
 
 
363
(defthm nth*-equiv-def
 
364
  (equal (nth*-equiv list st1 st2)
 
365
         (if (consp list)
 
366
             (and (equal (nth (car list) st1)
 
367
                         (nth (car list) st2))
 
368
                  (nth*-equiv (cdr list) st1 st2))
 
369
           t))
 
370
  :hints (("Goal" :in-theory (enable nth*-equiv)))
 
371
  :rule-classes (:definition))
 
372
 
 
373
(defun clr-nth* (list st)
 
374
  (if (consp list)
 
375
      (clr-nth (car list)
 
376
               (clr-nth* (cdr list) st))
 
377
    st))
 
378
 
 
379
(defthm open-clr-nth*
 
380
  (implies
 
381
   (consp list)
 
382
   (equal (clr-nth* list st)
 
383
          (clr-nth (car list)
 
384
                   (clr-nth* (cdr list) st)))))
 
385
 
 
386
(defthm clr-nth-clr-nth*
 
387
  (equal (clr-nth* list (clr-nth a st))
 
388
         (clr-nth a (clr-nth* list st)))
 
389
  :hints (("Subgoal *1/1" :cases ((nfix-equiv a (car list))))))
 
390
 
 
391
(defun equal-nth*-conclusion (list x y)
 
392
  (and (equal (lastatom x) (lastatom y))
 
393
       (equal (len x) (len y))
 
394
       (nth*-equiv list x y)
 
395
       (equal (clr-nth* list x)
 
396
              (clr-nth* list y))))
 
397
 
 
398
(defthm nth*-equiv-over-clr-nth-backchaining
 
399
  (implies
 
400
   (nth*-equiv list x y)
 
401
   (nth*-equiv list (clr-nth a x) (clr-nth a y)))
 
402
  :hints (("Goal" :in-theory (enable nth*-equiv))))
 
403
 
 
404
(defthm nth*-equiv-identity
 
405
  (nth*-equiv list x x)
 
406
  :hints (("Goal" :in-theory (enable nth*-equiv))))
 
407
 
 
408
(defun equal-nth*-induction (list x y)
 
409
  (if (consp list)
 
410
      (equal-nth*-induction (cdr list) 
 
411
                            (clr-nth (car list) x)
 
412
                            (clr-nth (car list) y))
 
413
    (list x y)))
 
414
 
 
415
(defthmd equal-nth*-reduction
 
416
  (equal (equal x y)
 
417
         (equal-nth*-conclusion list x y))
 
418
  :hints (("Goal" :induct (equal-nth*-induction list x y)
 
419
           :in-theory (disable equal-nth*-conclusion lastatom-clr-nth len-clr-nth))
 
420
          ("Subgoal *1/2" :in-theory (enable equal-nth*-conclusion))
 
421
          ("Subgoal *1/1" :in-theory (enable equal-nth*-conclusion)
 
422
           :use ((:instance equal-to-nth-reduction
 
423
                            (n (car list)))))))
 
424
 
 
425
 
 
426
(defun copy-nth* (list st1 st2)
 
427
  (if (consp list)
 
428
      (update-nth (car list)
 
429
                  (nth (car list) st1)
 
430
                  (copy-nth* (cdr list) st1 st2))
 
431
    st2))
 
432
 
 
433
;;
 
434
;; Does the default ordering go the wrong way?
 
435
;;
 
436
(defthm clr-nth-thru-clr-nth*
 
437
  (equal (clr-nth ZZZZ (clr-nth* list (update-nth ZZZZ v x)))
 
438
         (clr-nth ZZZZ (clr-nth* list x))))
 
439
 
 
440
(defthm nth*-clr-copy-nth*
 
441
  (equal (clr-nth* list (copy-nth* list st1 st2))
 
442
         (clr-nth* list st2)))
 
443
 
 
444
(defund nth*-copy-equiv (list x y z)
 
445
  (equal (copy-nth* list x z)
 
446
         (copy-nth* list y z)))
 
447
 
 
448
 
 
449
(encapsulate
 
450
    ()
 
451
  
 
452
  (defun maxval-p (a list)
 
453
    (if (consp list)
 
454
        (if (< (nfix a) (nfix (car list))) nil
 
455
          (maxval-p a (cdr list)))
 
456
      t))
 
457
  
 
458
  (defun maxval (list)
 
459
    (if (consp list)
 
460
        (if (maxval-p (car list) (cdr list))
 
461
            (nfix (car list))
 
462
          (maxval (cdr list)))
 
463
      0))
 
464
  
 
465
  (defthm maxval-p-maxval-prop
 
466
    (IMPLIES (AND (NOT (MAXVAL-P A Z))
 
467
                  (MAXVAL-P X Z)
 
468
                  (< (NFIX X) (NFIX A)))
 
469
             (< (NFIX X) (MAXVAL Z)))
 
470
    :rule-classes (:linear :rewrite))
 
471
  
 
472
  (defthm not-maxval-p-maxval-prop-2
 
473
    (implies
 
474
     (not (maxval-p x list))
 
475
     (< (nfix x) (maxval list)))
 
476
    :rule-classes (:rewrite :linear))
 
477
  
 
478
  (defthm maxval-p-maxval-prop-3
 
479
    (implies
 
480
     (maxval-p x list)
 
481
     (<= (maxval list) (nfix x)))
 
482
    :rule-classes (:rewrite :linear))
 
483
  
 
484
  (defund maxsize (list)
 
485
    (if (consp list)
 
486
        (1+ (maxval list))
 
487
      0))
 
488
  
 
489
  (local
 
490
   (defthm max-maxsize
 
491
     (equal (max (1+ (nfix x)) (maxsize list))
 
492
            (if (maxval-p x list) (1+ (nfix x))
 
493
              (maxsize list)))
 
494
     :hints (("Goal" :in-theory (enable maxsize)))))
 
495
  
 
496
  (local
 
497
   (defthm open-maxsize
 
498
     (implies
 
499
      (consp list)
 
500
      (equal (maxsize list)
 
501
             (if (maxval-p (car list) (cdr list))
 
502
                 (1+ (nfix (car list)))
 
503
               (maxsize (cdr list)))))
 
504
     :hints (("goal" :in-theory (enable maxsize)))))
 
505
  
 
506
  (local
 
507
   (defthm equal-max-reduction
 
508
     (implies (equal (max a b) d)
 
509
              (iff (equal (max a (max b c))
 
510
                          (max d c)) t))))
 
511
 
 
512
  (defthm len-copy-nth*
 
513
    (equal (len (copy-nth* list x y))
 
514
           (max (maxsize list) (len y)))
 
515
    :hints (("Goal" :induct (copy-nth* list x y)
 
516
             :in-theory (disable max))
 
517
            ("Subgoal *1/2" :in-theory (enable maxsize max))))
 
518
 
 
519
  )
 
520
  
 
521
 
 
522
(defthm nth*-copy-equiv-reduction
 
523
  (equal (nth*-copy-equiv list x y z)
 
524
         (equal-nth*-conclusion list (copy-nth* list x z) (copy-nth* list y z)))
 
525
  :hints (("Goal" :in-theory (enable nth*-copy-equiv)
 
526
           :use (:instance equal-nth*-reduction
 
527
                           (x (copy-nth* list x z))
 
528
                           (y (copy-nth* list y z))
 
529
                           (list list)))))
 
530
 
 
531
(defthm nth*-equiv-update-nth-chaining
 
532
  (implies
 
533
   (and
 
534
    (nth*-equiv list x y)
 
535
    (equal v (nth a y)))
 
536
   (nth*-equiv list (update-nth a v x) y))
 
537
  :hints (("goal" :induct (len list))))
 
538
 
 
539
(defthm nth*-equiv-copy-nth*
 
540
  (nth*-equiv list (copy-nth* list x y) x))
 
541
 
 
542
(defthm nth*-copy-nth*
 
543
  (equal (nth* list (copy-nth* list x y))
 
544
         (nth* list x))
 
545
  :hints (("Goal" :in-theory `(nth*-equiv)
 
546
           :use (:instance nth*-equiv-copy-nth*))))
 
547
 
 
548
(defthm nth*-equiv-copy-nth*-copy-nth*
 
549
  (equal (nth*-equiv list (copy-nth* list x a)
 
550
                     (copy-nth* list y b))
 
551
         (nth*-equiv list x y))
 
552
  :hints (("Goal" :in-theory (enable nth*-equiv))))
 
553
 
 
554
(defthm lastatom-copy-nth*
 
555
  (equal (lastatom (copy-nth* list x y))
 
556
         (if (or (not (consp list)) (< (maxval list) (len y)))
 
557
             (lastatom y)
 
558
           nil))
 
559
  :hints (("Goal" :in-theory (enable maxsize)))
 
560
  :otf-flg t)
 
561
 
 
562
(defthm nth*-equiv-reduction
 
563
  (equal (nth*-equiv list x y)
 
564
         (nth*-copy-equiv list x y z)))
 
565
 
 
566
(defun use (list st)
 
567
  (copy-nth* list st nil))
 
568
 
 
569
(defthm nth-use
 
570
  (implies
 
571
   (member (nfix n) (nfix-list list))
 
572
   (equal (nth n (use list x))
 
573
          (nth n x)))
 
574
  :hints (("Goal" :in-theory (enable use))))
 
575
 
 
576
(defthm nth*-get-copy-equivalence
 
577
  (equal (equal (nth* list x)
 
578
                (nth* list y))
 
579
         (equal (use list x)
 
580
                (use list y)))
 
581
  :hints (("goal" :in-theory '(use
 
582
                               nth*-equiv
 
583
                               nth*-copy-equiv)
 
584
           :use (:instance nth*-equiv-reduction
 
585
                           (z nil)))))
 
586
 
 
587
(defthm nth-copy-nth*
 
588
  (equal (nth a (copy-nth* list x y))
 
589
         (if (member (nfix a) (nfix-list list)) (nth a x)
 
590
           (nth a y))))
 
591
 
 
592
(defthm update-nth-nil-reduction
 
593
  (equal (update-nth a nil x)
 
594
         (clr-nth a x))
 
595
  :hints (("Goal" :in-theory (enable clr-nth))))
 
596
 
 
597
(defthm clr-nth-copy-nth*-member
 
598
  (implies
 
599
   (member (nfix a) (nfix-list list))
 
600
   (equal (clr-nth a (copy-nth* list x y))
 
601
          (copy-nth* list (clr-nth a x) y)))
 
602
  :hints (("Goal" :in-theory (disable EQUAL-UPDATE-NTH-REDUCTION))))
 
603
 
 
604
(defthm clr-nth-copy-nth*-non-member
 
605
  (implies
 
606
   (not (member (nfix a) (nfix-list list)))
 
607
   (equal (clr-nth a (copy-nth* list x y))
 
608
          (copy-nth* list x (clr-nth a y))))
 
609
  :hints (("Goal" :in-theory (disable EQUAL-UPDATE-NTH-REDUCTION))))
 
610
 
 
611
(defthm clr-nth*-copy-nth*
 
612
  (equal (clr-nth a (copy-nth* list x y))
 
613
         (if (member (nfix a) (nfix-list list)) (copy-nth* list (clr-nth a x) y)
 
614
           (copy-nth* list x (clr-nth a y)))))
 
615
 
 
616
(defthm update-nth-thru-copy-nth*
 
617
  (equal (update-nth a v (copy-nth* list (update-nth a w x) y))
 
618
         (update-nth a v (copy-nth* list x y))))
 
619
 
 
620
(defthm copy-nth*-update-nth-member
 
621
  (implies
 
622
   (member (nfix a) (nfix-list list))
 
623
   (equal (copy-nth* list (update-nth a v x) z)
 
624
          (update-nth a v (copy-nth* list x z))))
 
625
  :hints (("Goal" :in-theory (disable EQUAL-UPDATE-NTH-REDUCTION))))
 
626
 
 
627
(defthm copy-nth*-update-nth-non-member
 
628
  (implies
 
629
   (not (member (nfix a) (nfix-list list)))
 
630
   (equal (copy-nth* list (update-nth a v x) z)
 
631
          (copy-nth* list x z)))
 
632
  :hints (("Goal" :in-theory (disable EQUAL-UPDATE-NTH-REDUCTION))))
 
633
 
 
634
(defthm copy-nth*-update-nth
 
635
  (equal (copy-nth* list (update-nth a v x) z)
 
636
         (if (member (nfix a) (nfix-list list))
 
637
             (update-nth a v (copy-nth* list x z))
 
638
           (copy-nth* list x z)))
 
639
  :hints (("Goal" :in-theory '(copy-nth*-update-nth-member
 
640
                               copy-nth*-update-nth-non-member
 
641
                               ))))
 
642
 
 
643
(defthm use-update-nth-non-member
 
644
  (implies
 
645
   (not (member (nfix a) (nfix-list list)))
 
646
   (equal (use list (update-nth a v x))
 
647
          (use list x))))
 
648
 
 
649
(defthmd use-update-nth-member
 
650
  (implies
 
651
   (member (nfix a) (nfix-list list))
 
652
   (equal (use list (update-nth a v x))
 
653
          (update-nth a v (use list x)))))
 
654
 
 
655
(defthmd use-update-nth
 
656
  (equal (use list (update-nth a v x))
 
657
         (if (member (nfix a) (nfix-list list))
 
658
             (update-nth a v (use list x))
 
659
           (use list x)))
 
660
  :hints (("Goal" :in-theory '(use-update-nth-non-member
 
661
                               use-update-nth-member
 
662
                               ))))
 
663
 
 
664
(defthm use-use
 
665
  (equal (use list (use list x))
 
666
         (use list x)))
 
667
 
 
668
(defthm member-append
 
669
  (iff (member x (append y z))
 
670
       (or (member x y)
 
671
           (member x z))))
 
672
 
 
673
(defthm nfix-list-append
 
674
  (equal (nfix-list (append x y))
 
675
         (append (nfix-list x) (nfix-list y))))
 
676
 
 
677
(defthmd open-use
 
678
  (and
 
679
   (implies
 
680
    (consp list)
 
681
    (equal (use list x)
 
682
           (update-nth (car list) (nth (car list) x)
 
683
                       (use (cdr list) x))))
 
684
   (implies
 
685
    (not (consp list))
 
686
    (equal (use list x) nil)))
 
687
  :hints (("Goal" :in-theory (e/d (use) (EQUAL-UPDATE-NTH-REDUCTION)))))
 
688
 
 
689
 
 
690
(defun subset (x y)
 
691
  (if (consp x)
 
692
      (and (member (car x) y)
 
693
           (subset (cdr x) y))
 
694
    t))
 
695
 
 
696
(defthm nth*-use
 
697
  (implies
 
698
   (subset list listx)
 
699
   (equal (nth* list (use listx st))
 
700
          (nth* list st)))
 
701
  :hints (("Goal" :in-theory (e/d (use)
 
702
                                  (NTH*-GET-COPY-EQUIVALENCE)))))
 
703
 
 
704
(defthm subset-append
 
705
  (subset list (append list y)))
 
706
 
 
707
(defthm equal-nth*-append-reduction
 
708
  (equal (equal (nth* (append x y) a)
 
709
                (nth* (append x y) b))
 
710
         (and (equal (nth* x a)
 
711
                     (nth* x b))
 
712
              (equal (nth* y a)
 
713
                     (nth* y b))))
 
714
  :hints (("Goal" :in-theory (disable 
 
715
                              NTH*-GET-COPY-EQUIVALENCE
 
716
                              ))))
 
717
 
 
718
(defthm clr-nth-use
 
719
  (implies
 
720
   (member (nfix a) (nfix-list list))
 
721
   (equal (clr-nth a (use list x))
 
722
          (use list (clr-nth a x))))
 
723
  :hints (("Goal" :in-theory (enable use))))
 
724
 
 
725
(in-theory (disable OPEN-UPDATE-NTH))
 
726