← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/data-structures/array1.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/data-structures/array1.lisp
1
1
; array1.lisp -- a book about one-dimensional arrays
2
2
; Copyright (C) 1997  Computational Logic, Inc.
3
 
 
4
 
; This book is free software; you can redistribute it and/or modify
5
 
; it under the terms of the GNU General Public License as published by
6
 
; the Free Software Foundation; either version 2 of the License, or
7
 
; (at your option) any later version.
8
 
 
9
 
; This book is distributed in the hope that it will be useful,
10
 
; but WITHOUT ANY WARRANTY; without even the implied warranty of
11
 
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
12
 
; GNU General Public License for more details.
13
 
 
14
 
; You should have received a copy of the GNU General Public License
15
 
; along with this book; if not, write to the Free Software
16
 
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
 
3
; License: A 3-clause BSD license.  See the LICENSE file distributed with ACL2.
17
4
 
18
5
; Written by:  Bishop Brock
19
6
; Computational Logic, Inc.
20
7
; 1717 West Sixth Street, Suite 290
21
8
; Austin, TX 78703-4776 U.S.A.
22
9
 
23
 
;;;~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
24
 
;;;
25
 
;;;    array1.lisp
26
 
;;;
27
 
;;;    Characterization of 1-dimensional arrays.
28
 
;;;
29
 
;;;    This book requires nothing more than the ACL2 boot-strap theory for
30
 
;;;    its certification.
31
 
;;;    
32
 
;;;   
33
 
;;;~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
34
 
;;;
35
 
;;;    Note: This book was originally developed in a version of ACL2 where
36
 
;;;    guards were part of the logic. It is technically possible to weaken
37
 
;;;    the hypotheses of many of the lemmas, but time has not permitted us to
38
 
;;;    do this.
 
10
; Note: This book was originally developed in a version of ACL2 where guards
 
11
; were part of the logic. It is technically possible to weaken the hypotheses
 
12
; of many of the lemmas, but time has not permitted us to do this.
 
13
 
 
14
; Modified by Jared Davis, September 2014, to port documentation to xdoc.
39
15
 
40
16
(in-package "ACL2")
41
 
(include-book "doc-section")
42
 
 
43
 
(deflabel array1
44
 
  :doc ":doc-section data-structures
45
 
  
46
 
  A book of lemmas that characterize 1-dimensional arrays.
47
 
  ~/
48
 
 
49
 
  Because many of the functions characterized by this book are non-recursive,
50
 
  one should always DISABLE the theory ARRAY1-FUNCTIONS after including this
51
 
  book, or the lemmas will not be applicable. 
52
 
   ~/
53
 
 
54
 
  The lemmas exported by this book should completely characterize
55
 
  1-dimensional arrays for most purposes.  Given the lemmas exported by this
56
 
  book, it should not be necessary to ENABLE any of the 1-dimensional array
57
 
  functions except under special circumstances.
58
 
 
59
 
  This book defines a function RESET-ARRAY1 that clears an array, effectively
60
 
  resetting each element of the array to the default value.  This book also
61
 
  includes a macro, DEFARRAY1TYPE, which defines recognizers and supporting
62
 
  lemmas for 1-dimensional arrays whose elements are all of a fixed type.~/")
63
 
 
64
 
(defdoc array1-lemmas
65
 
  ":doc-section array1
66
 
  A theory of all ENABLEd rules exported by the \"array1\" book.
67
 
  ~/
68
 
  Note that in order for these rules to be applicable you will first need to
69
 
  DISABLE the theory ARRAY1-FUNCTIONS.  The following rules are found in this
70
 
  theory: 
71
 
  ~/~/ ")
72
 
 
73
 
 
 
17
(include-book "xdoc/top" :dir :system)
 
18
 
 
19
(defxdoc array1
 
20
  :parents (data-structures)
 
21
  :short "A book of lemmas that characterize 1-dimensional arrays."
 
22
  :long "<p>Because many of the functions characterized by this book are
 
23
non-recursive, one should always @(see DISABLE) the theory
 
24
@('ARRAY1-FUNCTIONS') after including this book, or the lemmas will not be
 
25
applicable.</p>
 
26
 
 
27
<p>The lemmas exported by this book should completely characterize
 
28
1-dimensional arrays for most purposes.  Given the lemmas exported by this
 
29
book, it should not be necessary to @(see ENABLE) any of the 1-dimensional
 
30
array functions except under special circumstances.</p>
 
31
 
 
32
<p>This book defines a function @(see RESET-ARRAY1) that clears an array,
 
33
effectively resetting each element of the array to the default value.  This
 
34
book also includes a macro, @(see DEFARRAY1TYPE), which defines recognizers and
 
35
supporting lemmas for 1-dimensional arrays whose elements are all of a fixed
 
36
type.</p>")
 
37
 
 
38
 
74
39
;;;****************************************************************************
75
40
;;;
76
41
;;;    These are general lemmas about ALISTs and ALIST functions.  None of
77
42
;;;    these lemmas are exported by this book.  Perhaps someday they will
78
 
;;;    appear in an ALIST book.   
 
43
;;;    appear in an ALIST book.
79
44
;;;
80
45
;;;****************************************************************************
81
46
 
82
 
;;;  EQLABLE-ALISTP
83
 
 
84
 
(local
85
 
 (defthm eqlable-alistp-implies-alistp
86
 
  (implies
87
 
   (eqlable-alistp l)
88
 
   (alistp l))
89
 
  :rule-classes (:rewrite :forward-chaining)))
90
 
 
91
 
;;;  ASSOC
92
 
 
93
 
(local
94
 
 (defthm assoc-properties
95
 
  (implies
96
 
   (and (eqlable-alistp l)
97
 
        (assoc x l))
98
 
   (and (consp (assoc x l))
99
 
        (equal (car (assoc x l)) x)))))
100
 
 
101
 
(local
102
 
 (defthm eqlablep-car-assoc
103
 
   (implies
104
 
    (and (eqlable-alistp l)
105
 
         (assoc x l))
106
 
    (eqlablep (car (assoc x l))))))
107
 
 
108
 
;;;  ASSOC-EQ
109
 
 
110
 
(local
111
 
 (defthm assoc-eq-properties
112
 
   (implies
113
 
    (and (alistp l)
114
 
         (assoc-eq x l))
115
 
    (and (consp (assoc-eq x l))
116
 
         (equal (car (assoc-eq x l)) x)))))
117
 
 
118
 
;;;  BOUNDED-INTEGER-ALISTP
119
 
 
120
 
(local
121
 
 (defthm bounded-integer-alistp-eqlable-alistp
122
 
  (implies
123
 
   (bounded-integer-alistp l n)
124
 
   (eqlable-alistp l))
125
 
  :rule-classes (:rewrite :forward-chaining)))
126
 
 
127
 
(local
128
 
 (defthm bounded-integer-alistp-car-assoc-properties
129
 
   (implies
130
 
    (and (bounded-integer-alistp l n)
131
 
         (assoc i l)
132
 
         (not (equal (car (assoc i l)) :header)))
133
 
    (and (integerp (car (assoc i l)))
134
 
         (>= (car (assoc i l)) 0)
135
 
         (< (car (assoc i l)) n)))))
136
 
 
137
 
 
 
47
(local (defthm eqlable-alistp-implies-alistp
 
48
         (implies (eqlable-alistp l)
 
49
                  (alistp l))
 
50
         :rule-classes (:rewrite :forward-chaining)))
 
51
 
 
52
(local (defthm assoc-properties
 
53
         (implies (and (eqlable-alistp l)
 
54
                       (assoc x l))
 
55
                  (and (consp (assoc x l))
 
56
                       (equal (car (assoc x l)) x)))))
 
57
 
 
58
(local (defthm eqlablep-car-assoc
 
59
         (implies (and (eqlable-alistp l)
 
60
                       (assoc x l))
 
61
                  (eqlablep (car (assoc x l))))))
 
62
 
 
63
(local (defthm assoc-eq-properties
 
64
         (implies (and (alistp l)
 
65
                       (assoc-eq x l))
 
66
                  (and (consp (assoc-eq x l))
 
67
                       (equal (car (assoc-eq x l)) x)))))
 
68
 
 
69
(local (defthm bounded-integer-alistp-eqlable-alistp
 
70
         (implies (bounded-integer-alistp l n)
 
71
                  (eqlable-alistp l))
 
72
         :rule-classes (:rewrite :forward-chaining)))
 
73
 
 
74
(local (defthm bounded-integer-alistp-car-assoc-properties
 
75
         (implies (and (bounded-integer-alistp l n)
 
76
                       (assoc i l)
 
77
                       (not (equal (car (assoc i l)) :header)))
 
78
                  (and (integerp (car (assoc i l)))
 
79
                       (>= (car (assoc i l)) 0)
 
80
                       (< (car (assoc i l)) n)))))
 
81
 
 
82
 
138
83
;;;****************************************************************************
139
84
;;;
140
85
;;;    Local array1 events.
175
120
      (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))))))
176
121
   :rule-classes :forward-chaining))
177
122
 
178
 
(local
179
 
 (defthm array1p-header-exists
180
 
   (implies
181
 
    (array1p name l)
182
 
    (assoc-eq :header l))))
 
123
(local (defthm array1p-header-exists
 
124
         (implies (array1p name l)
 
125
                  (assoc-eq :header l))))
183
126
 
184
127
; ARRAY1P-CONS (in a slightly different format) is part of the
185
128
; BOOT-STRAP-THEORY of ACL2.
186
129
 
187
 
(local
188
 
 (defthm our-array1p-cons
189
 
   (implies
190
 
    (and (array1p name l)
191
 
         (integerp n)
192
 
         (>= n 0)
193
 
         (< n (car (dimensions name l))))
194
 
    (array1p name (cons (cons n x) l)))))
 
130
(local (defthm our-array1p-cons
 
131
         (implies (and (array1p name l)
 
132
                       (integerp n)
 
133
                       (>= n 0)
 
134
                       (< n (car (dimensions name l))))
 
135
                  (array1p name (cons (cons n x) l)))))
195
136
 
196
137
(local (in-theory (disable array1p)))
197
138
 
198
139
;;;  Now, we prove everthing we need to know about COMPRESS11, and then use
199
140
;;;  these lemmas to characterize COMPRESS1.
200
141
 
201
 
(local
202
 
 (defthm eqlable-alistp-compress11
203
 
   (implies
204
 
    (and (array1p name l)
205
 
         (integerp i)
206
 
         (integerp n)
207
 
         (<= i n))
208
 
    (eqlable-alistp (compress11 name l i n default)))))
209
 
 
210
 
(local
211
 
 (defthm bounded-integer-alistp-compress11
212
 
   (implies
213
 
    (and (array1p name l)
214
 
         (integerp i)
215
 
         (integerp n)
216
 
         (>= i 0)
217
 
         (<= i n))
218
 
    (bounded-integer-alistp (compress11 name l i n default) n))))
219
 
 
220
 
(local
221
 
 (defthm compress11-assoc-property-0
222
 
   (implies
223
 
    (and (array1p name l)
224
 
         (integerp i)
225
 
         (integerp n)
226
 
         (<= i n)
227
 
         (integerp j)
228
 
         (assoc j l)
229
 
         (assoc j (compress11 name l i n default)))
230
 
    (equal (assoc j (compress11 name l i n default))
231
 
           (assoc j l)))))
232
 
 
233
 
(local
234
 
 (defthm compress11-assoc-property-1
235
 
   (implies
236
 
    (and (array1p name l)
237
 
         (not (assoc j (compress11 name l i n default))) ;Free vars!
238
 
         (integerp i)
239
 
         (integerp n)
240
 
         (<= i n)
241
 
         (integerp j)
242
 
         (<= i j)
243
 
         (< j n)
244
 
         (assoc j l))
245
 
    (equal (cdr (assoc j l))
246
 
           default))))
247
 
 
248
 
(local
249
 
 (defthm compress11-assoc-property-2
250
 
   (implies
251
 
    (and (array1p name l)
252
 
         (integerp i)
253
 
         (integerp n)
254
 
         (<= i n)
255
 
         (integerp j)
256
 
         (not (assoc j l)))
257
 
    (not (assoc j (compress11 name l i n default))))))
 
142
(local (defthm eqlable-alistp-compress11
 
143
         (implies (and (array1p name l)
 
144
                       (integerp i)
 
145
                       (integerp n)
 
146
                       (<= i n))
 
147
                  (eqlable-alistp (compress11 name l i n default)))))
 
148
 
 
149
(local (defthm bounded-integer-alistp-compress11
 
150
         (implies (and (array1p name l)
 
151
                       (integerp i)
 
152
                       (integerp n)
 
153
                       (>= i 0)
 
154
                       (<= i n))
 
155
                  (bounded-integer-alistp (compress11 name l i n default) n))))
 
156
 
 
157
(local (defthm compress11-assoc-property-0
 
158
         (implies (and (array1p name l)
 
159
                       (integerp i)
 
160
                       (integerp n)
 
161
                       (<= i n)
 
162
                       (integerp j)
 
163
                       (assoc j l)
 
164
                       (assoc j (compress11 name l i n default)))
 
165
                  (equal (assoc j (compress11 name l i n default))
 
166
                         (assoc j l)))))
 
167
 
 
168
(local (defthm compress11-assoc-property-1
 
169
         (implies (and (array1p name l)
 
170
                       (not (assoc j (compress11 name l i n default))) ;Free vars!
 
171
                       (integerp i)
 
172
                       (integerp n)
 
173
                       (<= i n)
 
174
                       (integerp j)
 
175
                       (<= i j)
 
176
                       (< j n)
 
177
                       (assoc j l))
 
178
                  (equal (cdr (assoc j l))
 
179
                         default))))
 
180
 
 
181
(local (defthm compress11-assoc-property-2
 
182
         (implies (and (array1p name l)
 
183
                       (integerp i)
 
184
                       (integerp n)
 
185
                       (<= i n)
 
186
                       (integerp j)
 
187
                       (not (assoc j l)))
 
188
                  (not (assoc j (compress11 name l i n default))))))
258
189
 
259
190
; Start events added by Matt K. for Version 3.1, 7/1/06, to support proof of
260
191
; compress1-assoc-property-0 in light of addition of reverse-sorted and
261
192
; unsorted ACL2 arrays.
262
193
 
263
 
(local
264
 
 (defthm assoc-revappend-1
265
 
   (implies (not (member key (strip-cars alist1)))
266
 
            (equal (assoc key (revappend alist1 alist2))
267
 
                   (assoc key alist2)))))
268
 
 
269
 
(local
270
 
 (defthm assoc-revappend
271
 
   (implies (and (force (no-duplicatesp (strip-cars alist1)))
272
 
                 (force (alistp alist1)))
273
 
            (equal (assoc key (revappend alist1 alist2))
274
 
                   (or (assoc key alist1)
275
 
                       (assoc key alist2))))))
276
 
 
277
 
(local
278
 
 (defun ordered-alistp (x)
279
 
   (cond
280
 
    ((atom x)
281
 
     (null x))
282
 
    ((atom (cdr x))
283
 
     (and (consp (car x))
284
 
          (rationalp (caar x))
285
 
          (null (cdr x))))
286
 
    (t (and (consp (car x))
287
 
            (rationalp (caar x))
288
 
            (< (caar x) (caadr x))
289
 
            (ordered-alistp (cdr x)))))))
290
 
 
291
 
(local
292
 
 (defthm no-duplicatesp-strip-cars-ordered-alistp-1
293
 
   (implies (and (< key (caar x))
294
 
                 (ordered-alistp x))
295
 
            (not (member key
296
 
                         (strip-cars x))))))
297
 
 
298
 
(local
299
 
 (defthm no-duplicatesp-strip-cars-ordered-alistp
300
 
   (implies (ordered-alistp x)
301
 
            (no-duplicatesp (strip-cars x)))))
302
 
 
303
 
(local
304
 
 (defthm consp-assoc-rewrite
305
 
   (implies (and key
306
 
                 (assoc key alist))
307
 
            (consp (assoc key alist)))))
308
 
 
309
 
(local
310
 
 (defthm car-assoc
311
 
   (implies (assoc key alist)
312
 
            (equal (car (assoc key alist))
313
 
                   key))))
314
 
 
315
 
(local
316
 
 (defthm <-caar-compress11
317
 
   (implies (and (< i j)
318
 
                 (consp (compress11 name l j n default)))
319
 
            (< i (caar (compress11 name l j n default))))))
320
 
 
321
 
(local
322
 
 (defthm ordered-alistp-compress11
323
 
   (implies (and (integerp i)
324
 
                 (integerp n))
325
 
            (ordered-alistp (compress11 name l i n default)))))
326
 
 
327
 
(local
328
 
 (defthm not-member-strip-cars-compress11
329
 
   (implies
330
 
    (< i j)
331
 
    (not (member i
332
 
                 (strip-cars (compress11 name l j n default)))))))
333
 
 
334
 
(local
335
 
 (defthm no-duplicatesp-strip-cars-compress11
336
 
   (no-duplicatesp (strip-cars (compress11 name l i n default)))))
 
194
(local (defthm assoc-revappend-1
 
195
         (implies (not (member key (strip-cars alist1)))
 
196
                  (equal (assoc key (revappend alist1 alist2))
 
197
                         (assoc key alist2)))))
 
198
 
 
199
(local (defthm assoc-revappend
 
200
         (implies (and (force (no-duplicatesp (strip-cars alist1)))
 
201
                       (force (alistp alist1)))
 
202
                  (equal (assoc key (revappend alist1 alist2))
 
203
                         (or (assoc key alist1)
 
204
                             (assoc key alist2))))))
 
205
 
 
206
(local (defun ordered-alistp (x)
 
207
         (cond ((atom x)
 
208
                (null x))
 
209
               ((atom (cdr x))
 
210
                (and (consp (car x))
 
211
                     (rationalp (caar x))
 
212
                     (null (cdr x))))
 
213
               (t (and (consp (car x))
 
214
                       (rationalp (caar x))
 
215
                       (< (caar x) (caadr x))
 
216
                       (ordered-alistp (cdr x)))))))
 
217
 
 
218
(local (defthm no-duplicatesp-strip-cars-ordered-alistp-1
 
219
         (implies (and (< key (caar x))
 
220
                       (ordered-alistp x))
 
221
                  (not (member key
 
222
                               (strip-cars x))))))
 
223
 
 
224
(local (defthm no-duplicatesp-strip-cars-ordered-alistp
 
225
         (implies (ordered-alistp x)
 
226
                  (no-duplicatesp (strip-cars x)))))
 
227
 
 
228
(local (defthm consp-assoc-rewrite
 
229
         (implies (and key
 
230
                       (assoc key alist))
 
231
                  (consp (assoc key alist)))))
 
232
 
 
233
(local (defthm car-assoc
 
234
         (implies (assoc key alist)
 
235
                  (equal (car (assoc key alist))
 
236
                         key))))
 
237
 
 
238
(local (defthm <-caar-compress11
 
239
         (implies (and (< i j)
 
240
                       (consp (compress11 name l j n default)))
 
241
                  (< i (caar (compress11 name l j n default))))))
 
242
 
 
243
(local (defthm ordered-alistp-compress11
 
244
         (implies (and (integerp i)
 
245
                       (integerp n))
 
246
                  (ordered-alistp (compress11 name l i n default)))))
 
247
 
 
248
(local (defthm not-member-strip-cars-compress11
 
249
         (implies (< i j)
 
250
                  (not (member i
 
251
                               (strip-cars (compress11 name l j n default)))))))
 
252
 
 
253
(local (defthm no-duplicatesp-strip-cars-compress11
 
254
         (no-duplicatesp (strip-cars (compress11 name l i n default)))))
337
255
 
338
256
; End events added by Matt K. for Version 3.1, 7/1/06, to support proof of
339
257
; compress1-assoc-property-0 in light of addition of reverse-sorted and
340
258
; unsorted ACL2 arrays.
341
259
 
342
 
(local
343
 
 (defthm compress1-assoc-property-0
344
 
  (implies
345
 
   (and (array1p name l)
346
 
        (integerp n)
347
 
        (>= n 0)
348
 
        (< n (car (dimensions name l))) 
349
 
        (assoc n l)
350
 
        (assoc n (compress1 name l)))
351
 
   (equal (cdr (assoc n (compress1 name l)))
352
 
          (cdr (assoc n l))))))
353
 
 
354
 
(local
355
 
 (defthm compress1-assoc-property-1
356
 
   (implies
357
 
    (and (array1p name l)
358
 
         (integerp n)
359
 
         (>= n 0)
360
 
         (< n (car (dimensions name l))) 
361
 
         (assoc n l)
362
 
         (not (assoc n (compress1 name l))))
363
 
    (equal (cdr (assoc n l))
364
 
           (cadr (assoc-keyword :default (cdr (assoc-eq :header l))))))))
365
 
 
366
 
(local
367
 
 (defthm compress1-assoc-property-2
368
 
   (implies
369
 
    (and (array1p name l)
370
 
         (integerp n)
371
 
         (>= n 0)
372
 
         (< n (car (dimensions name l))) 
373
 
         (not (assoc n l)))
374
 
    (not (assoc n (compress1 name l))))))
375
 
 
376
 
(local
377
 
 (defthm header-compress1-crock
378
 
   (implies
379
 
    (array1p name l)
380
 
    (equal (assoc-eq :header (compress1 name l))
381
 
           (assoc-eq :header l)))))
382
 
 
383
 
 
 
260
(local (defthm compress1-assoc-property-0
 
261
         (implies (and (array1p name l)
 
262
                       (integerp n)
 
263
                       (>= n 0)
 
264
                       (< n (car (dimensions name l)))
 
265
                       (assoc n l)
 
266
                       (assoc n (compress1 name l)))
 
267
                  (equal (cdr (assoc n (compress1 name l)))
 
268
                         (cdr (assoc n l))))))
 
269
 
 
270
(local (defthm compress1-assoc-property-1
 
271
         (implies (and (array1p name l)
 
272
                       (integerp n)
 
273
                       (>= n 0)
 
274
                       (< n (car (dimensions name l)))
 
275
                       (assoc n l)
 
276
                       (not (assoc n (compress1 name l))))
 
277
                  (equal (cdr (assoc n l))
 
278
                         (cadr (assoc-keyword :default (cdr (assoc-eq :header l))))))))
 
279
 
 
280
(local (defthm compress1-assoc-property-2
 
281
         (implies
 
282
          (and (array1p name l)
 
283
               (integerp n)
 
284
               (>= n 0)
 
285
               (< n (car (dimensions name l)))
 
286
               (not (assoc n l)))
 
287
          (not (assoc n (compress1 name l))))))
 
288
 
 
289
(local (defthm header-compress1-crock
 
290
         (implies (array1p name l)
 
291
                  (equal (assoc-eq :header (compress1 name l))
 
292
                         (assoc-eq :header l)))))
 
293
 
 
294
 
 
295
(defsection-progn array1-lemmas
 
296
  :parents (array1)
 
297
  :short "A @(see theory) of all @(see enable)d rules exported by the @(see
 
298
array1) book."
 
299
 
 
300
  :long "<p>Note that in order for these rules to be applicable you will first
 
301
need to @(see DISABLE) the theory @(see ARRAY1-FUNCTIONS).</p>"
 
302
 
384
303
;;;****************************************************************************
385
304
;;;
386
305
;;;    Exported Events.
394
313
; support proof of compress1-assoc-property-0 in light of addition of
395
314
; reverse-sorted and unsorted ACL2 arrays.
396
315
 
397
 
(local
398
 
 (defthm alistp-revappend
399
 
   (implies (alistp x)
400
 
            (equal (alistp (revappend x y))
401
 
                   (alistp y)))))
402
 
 
403
 
(local
404
 
 (defthm bounded-integer-alistp-revappend
405
 
   (implies (bounded-integer-alistp x n) 
406
 
            (equal (bounded-integer-alistp (revappend x y) n)
407
 
                   (bounded-integer-alistp y n)))))
408
 
 
409
 
(defthm array1p-compress1
410
 
  (implies
411
 
   (array1p name l)
412
 
   (array1p name (compress1 name l)))
413
 
  :hints
414
 
  (("Goal"
415
 
    :in-theory (enable array1p)
416
 
    :use array1p-header-exists))
417
 
  :doc ":doc-section array1-lemmas
418
 
  Rewrite: (ARRAY1P name (COMPRESS1 name l)).
419
 
  ~/~/~/")
420
 
 
421
 
(defthm array1p-compress1-properties
422
 
  (implies
423
 
   (array1p name l)
424
 
   (and
425
 
    (equal (header name (compress1 name l))
426
 
           (header name l))
427
 
    (equal (dimensions name (compress1 name l))
428
 
           (dimensions name l))
429
 
    (equal (maximum-length name (compress1 name l))
430
 
           (maximum-length name l))
431
 
    (equal (default name (compress1 name l))
432
 
           (default name l))))
433
 
  :doc ":doc-section array1-lemmas
434
 
  Rewrite: 
435
 
  (HEADER name (COMPRESS1 name l))         = (HEADER name l).
436
 
  (DIMENSIONS name (COMPRESS1 name l))     = (DIMENSIONS name l).
437
 
  (MAXIMUM-LENGTH name (COMPRESS1 name l)) = (MAXIMUM-LENGTH name l).
438
 
  (DEFAULT name (COMPRESS1 name l))        = (DEFAULT name l).
439
 
  ~/~/~/")
440
 
 
441
 
;  COMPRESS1 is now fully characterized, so we DISABLE it and start proving
442
 
;  the interesting theorems.
443
 
 
444
 
(local (in-theory (disable compress1)))
445
 
 
446
 
(defthm array1p-aset1
447
 
  (implies
448
 
   (and (array1p name l)
449
 
        (integerp n)
450
 
        (>= n 0)
451
 
        (< n (car (dimensions name l))))
452
 
   (array1p name (aset1 name l n val)))
453
 
  :doc ":doc-section array1-lemmas
454
 
  Rewrite: (ARRAY1P name (ASET1 name l n val)).
455
 
  ~/~/~/")
456
 
 
457
 
(defthm array1p-aset1-properties
458
 
  (implies
459
 
   (and (array1p name l)
460
 
        (integerp n)
461
 
        (>= n 0)
462
 
        (< n (car (dimensions name l))))
463
 
   (and
464
 
    (equal (header name (aset1 name l n val))
465
 
           (header name l))
466
 
    (equal (dimensions name (aset1 name l n val))
467
 
           (dimensions name l))
468
 
    (equal (maximum-length name (aset1 name l n val))
469
 
           (maximum-length name l))
470
 
    (equal (default name (aset1 name l n val))
471
 
           (default name l))))
472
 
  :doc ":doc-section array1-lemmas
473
 
  Rewrite: 
474
 
  (HEADER name         (ASET1 name l n val))  = (HEADER name l).
475
 
  (DIMENSIONS name     (ASET1 name l n val))  = (DIMENSIONS name l).
476
 
  (MAXIMUM-LENGTH name (ASET1 name l n val))  = (MAXIMUM-LENGTH name l).
477
 
  (DEFAULT name        (ASET1 name l n val))  = (DEFAULT name l).
478
 
  ~/~/~/")
479
 
 
480
 
(defthm aref1-compress1
481
 
  (implies
482
 
   (and (array1p name l)
483
 
        (integerp n)
484
 
        (>= n 0)
485
 
        (< n (car (dimensions name l))))
486
 
   (equal (aref1 name (compress1 name l) n)
487
 
          (aref1 name l n)))
488
 
  :doc ":doc-section array1-lemmas
489
 
  Rewrite: (AREF1 name (COMPRESS1 name l) n) = (AREF name l n).
490
 
  ~/~/~/")
491
 
 
492
 
(defthm array1p-acons-properties
493
 
  (implies
494
 
   (integerp n)
495
 
   (and
496
 
    (equal (header name (cons (cons n val) l))
497
 
           (header name l))
498
 
    (equal (dimensions name (cons (cons n val) l))
499
 
           (dimensions name l))
500
 
    (equal (maximum-length name (cons (cons n val) l))
501
 
           (maximum-length name l))
502
 
    (equal (default name (cons (cons n val) l))
503
 
           (default name l))))
504
 
  :doc ":doc-section array1-lemmas
505
 
  Rewrite:
506
 
  (HEADER name         (CONS n val) l) = (HEADER l)        , for integers n. 
507
 
  (DIMENSIONS name     (CONS n val) l) = (DIMENSIONS l)    , for integers n. 
508
 
  (MAXIMUM-LENGTH name (CONS n val) l) = (MAXIMUM-LENGTH l), for integers n. 
509
 
  (DEFAULT name        (CONS n val) l) = (DEFAULT l)       , for integers n. 
510
 
  ~/~/~/")
511
 
 
512
 
(defthm array1p-consp-header
513
 
  (implies
514
 
   (array1p name l)
515
 
   (consp (header name l)))
516
 
  :rule-classes :type-prescription
517
 
  :doc ":doc-section array1-lemmas
518
 
  Type-Prescription: (CONSP (HEADER name l)).
519
 
  ~/~/~/")
520
 
 
521
 
(defthm array1p-car-header
522
 
  (implies
523
 
   (array1p name l)
524
 
   (equal (car (header name l))
525
 
          :header))
526
 
  :doc ":doc-section array1-lemmas
527
 
  Rewrite: (CAR (HEADER name l)) = :HEADER.
528
 
  ~/~/~/")
 
316
  (local
 
317
   (defthm alistp-revappend
 
318
     (implies (alistp x)
 
319
              (equal (alistp (revappend x y))
 
320
                     (alistp y)))))
 
321
 
 
322
  (local
 
323
   (defthm bounded-integer-alistp-revappend
 
324
     (implies (bounded-integer-alistp x n)
 
325
              (equal (bounded-integer-alistp (revappend x y) n)
 
326
                     (bounded-integer-alistp y n)))))
 
327
 
 
328
  (defthm array1p-compress1
 
329
    (implies (array1p name l)
 
330
             (array1p name (compress1 name l)))
 
331
    :hints (("Goal"
 
332
             :in-theory (enable array1p)
 
333
             :use array1p-header-exists)))
 
334
 
 
335
  (defthm array1p-compress1-properties
 
336
    (implies (array1p name l)
 
337
             (and
 
338
              (equal (header name (compress1 name l))
 
339
                     (header name l))
 
340
              (equal (dimensions name (compress1 name l))
 
341
                     (dimensions name l))
 
342
              (equal (maximum-length name (compress1 name l))
 
343
                     (maximum-length name l))
 
344
              (equal (default name (compress1 name l))
 
345
                     (default name l)))))
 
346
 
 
347
; COMPRESS1 is now fully characterized, so we DISABLE it and start proving
 
348
; the interesting theorems.
 
349
 
 
350
  (local (in-theory (disable compress1)))
 
351
 
 
352
  (defthm array1p-aset1
 
353
    (implies (and (array1p name l)
 
354
                  (integerp n)
 
355
                  (>= n 0)
 
356
                  (< n (car (dimensions name l))))
 
357
             (array1p name (aset1 name l n val))))
 
358
 
 
359
  (defthm array1p-aset1-properties
 
360
    (implies (and (array1p name l)
 
361
                  (integerp n)
 
362
                  (>= n 0)
 
363
                  (< n (car (dimensions name l))))
 
364
             (and (equal (header name (aset1 name l n val))
 
365
                         (header name l))
 
366
                  (equal (dimensions name (aset1 name l n val))
 
367
                         (dimensions name l))
 
368
                  (equal (maximum-length name (aset1 name l n val))
 
369
                         (maximum-length name l))
 
370
                  (equal (default name (aset1 name l n val))
 
371
                         (default name l)))))
 
372
 
 
373
  (defthm aref1-compress1
 
374
    (implies (and (array1p name l)
 
375
                  (integerp n)
 
376
                  (>= n 0)
 
377
                  (< n (car (dimensions name l))))
 
378
             (equal (aref1 name (compress1 name l) n)
 
379
                    (aref1 name l n))))
 
380
 
 
381
  (defthm array1p-acons-properties
 
382
    (implies (integerp n)
 
383
             (and (equal (header name (cons (cons n val) l))
 
384
                         (header name l))
 
385
                  (equal (dimensions name (cons (cons n val) l))
 
386
                         (dimensions name l))
 
387
                  (equal (maximum-length name (cons (cons n val) l))
 
388
                         (maximum-length name l))
 
389
                  (equal (default name (cons (cons n val) l))
 
390
                         (default name l)))))
 
391
 
 
392
  (defthm array1p-consp-header
 
393
    (implies (array1p name l)
 
394
             (consp (header name l)))
 
395
    :rule-classes :type-prescription)
 
396
 
 
397
  (defthm array1p-car-header
 
398
    (implies (array1p name l)
 
399
             (equal (car (header name l))
 
400
                    :header)))
529
401
 
530
402
;  These two theorems for the AREF1-ASET1 cases are used to prove a
531
403
;  combined result, and then exported DISABLEd.
532
404
 
533
 
(defthm aref1-aset1-equal
534
 
  (implies
535
 
   (and (array1p name l)
536
 
        (integerp n)
537
 
        (>= n 0)
538
 
        (< n (car (dimensions name l))))
539
 
   (equal (aref1 name (aset1 name l n val) n)
540
 
          val))
541
 
  :doc ":doc-section array1-lemmas
542
 
  Rewrite: (AREF1 name (ASET1 name l n val) n) = val.~/
543
 
  Note that this rule is exported DISABLEd by default in favor of
544
 
  AREF1-ASET1.
545
 
  ~/~/")
546
 
 
547
 
(defthm aref1-aset1-not-equal
548
 
  (implies
549
 
   (and (array1p name l)
550
 
        (integerp n1)
551
 
        (>= n1 0)
552
 
        (< n1 (car (dimensions name l)))
553
 
        (integerp n2)
554
 
        (>= n2 0)
555
 
        (< n2 (car (dimensions name l)))
556
 
        (not (equal n1 n2)))
557
 
   (equal (aref1 name (aset1 name l n1 val) n2)
558
 
          (aref1 name l n2)))
559
 
  :doc ":doc-section array1-lemmas
560
 
  Rewrite: (AREF1 name (ASET1 name l n1 val) n2) = (AREF1 name l n2),
561
 
           when n1 /= n2.~/
562
 
  Note that this rule is exported DISABLEd by default in favor of
563
 
  AREF1-ASET1.
564
 
  ~/~/")
565
 
 
566
 
(defthm aref1-aset1
567
 
  (implies
568
 
   (and (array1p name l)
569
 
        (integerp n1)
570
 
        (>= n1 0)
571
 
        (< n1 (car (dimensions name l)))
572
 
        (integerp n2)
573
 
        (>= n2 0)
574
 
        (< n2 (car (dimensions name l))))
575
 
   (equal (aref1 name (aset1 name l n1 val) n2)
576
 
          (if (equal n1 n2)
577
 
              val
578
 
            (aref1 name l n2))))
579
 
  :hints
580
 
  (("Goal"
581
 
    :in-theory (disable aref1 aset1)))
582
 
  :doc ":doc-section array1-lemmas
583
 
  Rewrite: (AREF1 name (ASET1 name l n1 val) n2) = 
584
 
              (IF (EQUAL n1 n2) val (AREF1 name l n2)).
585
 
  ~/
586
 
  Note that this lemma forces the decision of the equality of n1 and n2.  If
587
 
  this causes problems, then DISABLE this lemma and
588
 
  (ENABLE AREF1-ASET1-EQUAL AREF1-ASET1-NOT-EQUAL).~/~/")
589
 
 
590
 
(in-theory (disable aref1-aset1-equal aref1-aset1-not-equal))
 
405
  (defthm aref1-aset1-equal
 
406
    ;; Note that this rule is exported DISABLEd by default in favor of
 
407
    ;; AREF1-ASET1.
 
408
    (implies (and (array1p name l)
 
409
                  (integerp n)
 
410
                  (>= n 0)
 
411
                  (< n (car (dimensions name l))))
 
412
             (equal (aref1 name (aset1 name l n val) n)
 
413
                    val)))
 
414
 
 
415
  (defthm aref1-aset1-not-equal
 
416
    ;; Note that this rule is exported DISABLEd by default in favor of
 
417
    ;; AREF1-ASET1.
 
418
    (implies (and (array1p name l)
 
419
                  (integerp n1)
 
420
                  (>= n1 0)
 
421
                  (< n1 (car (dimensions name l)))
 
422
                  (integerp n2)
 
423
                  (>= n2 0)
 
424
                  (< n2 (car (dimensions name l)))
 
425
                  (not (equal n1 n2)))
 
426
             (equal (aref1 name (aset1 name l n1 val) n2)
 
427
                    (aref1 name l n2))))
 
428
 
 
429
  (defthm aref1-aset1
 
430
    ;; Note that this lemma forces the decision of the equality of n1 and n2.  If
 
431
    ;; this causes problems, then DISABLE this lemma and (ENABLE
 
432
    ;; AREF1-ASET1-EQUAL AREF1-ASET1-NOT-EQUAL)
 
433
    (implies (and (array1p name l)
 
434
                  (integerp n1)
 
435
                  (>= n1 0)
 
436
                  (< n1 (car (dimensions name l)))
 
437
                  (integerp n2)
 
438
                  (>= n2 0)
 
439
                  (< n2 (car (dimensions name l))))
 
440
             (equal (aref1 name (aset1 name l n1 val) n2)
 
441
                    (if (equal n1 n2)
 
442
                        val
 
443
                      (aref1 name l n2))))
 
444
    :hints (("Goal" :in-theory (disable aref1 aset1))))
 
445
 
 
446
  (in-theory (disable aref1-aset1-equal aref1-aset1-not-equal))
591
447
 
592
448
;;;  The final form of the :FORWARD-CHAINING lemma for ARRAY1P.
593
449
 
594
 
(defthm array1p-forward-modular
595
 
  (implies
596
 
   (array1p name l)
597
 
   (and (symbolp name)
598
 
        (alistp l)
599
 
        (keyword-value-listp (cdr (header name l)))
600
 
        (true-listp (dimensions name l))
601
 
        (equal (length (dimensions name l)) 1)
602
 
        (integerp (car (dimensions name l)))
603
 
        (integerp (maximum-length name l))
604
 
        (< 0 (car (dimensions name l)))
605
 
        (<= (car (dimensions name l)) (maximum-length name l))
606
 
        (<= (maximum-length name l) *maximum-positive-32-bit-integer*)
607
 
        (bounded-integer-alistp l (car (dimensions name l)))))
608
 
  :rule-classes :forward-chaining
609
 
  :hints
610
 
  (("Goal"
611
 
    :in-theory (disable length)))
612
 
  :doc ":doc-section array1-lemmas
613
 
  Forward Chaining: A forward definition of (ARRAY1P name l), in terms of
614
 
  HEADER, DIMENSIONS, and MAXIMUM-LENGTH.
615
 
  ~/
616
 
  Note that ACL2 also defines a lemma ARRAY1P-FORWARD, but that lemma
617
 
  is in terms of the expansions of HEADER, DIMENSIONS, and MAXIMUM-LENGTH.
618
 
  ~/
619
 
  One should normaly DISABLE ARRAY1P in favor of this :FORWARD-CHAINING rule.
620
 
  If allowed to open, ARRAY1P can cause severe performance degradation due to
621
 
  its large size and many recursive functions.  This lemma is designed to be
622
 
  used with the ARRAY1-FUNCTIONS theory DISABLEd.~/")
623
 
 
624
 
 
 
450
  (defthm array1p-forward-modular
 
451
    ;;  Forward Chaining: A forward definition of (ARRAY1P name l), in terms of
 
452
    ;;  HEADER, DIMENSIONS, and MAXIMUM-LENGTH.
 
453
    ;;
 
454
    ;;  Note that ACL2 also defines a lemma ARRAY1P-FORWARD, but that lemma
 
455
    ;;  is in terms of the expansions of HEADER, DIMENSIONS, and MAXIMUM-LENGTH.
 
456
    ;;
 
457
    ;;  One should normaly DISABLE ARRAY1P in favor of this :FORWARD-CHAINING rule.
 
458
    ;;  If allowed to open, ARRAY1P can cause severe performance degradation due to
 
459
    ;;  its large size and many recursive functions.  This lemma is designed to be
 
460
    ;;  used with the ARRAY1-FUNCTIONS theory DISABLEd.
 
461
    (implies (array1p name l)
 
462
             (and (symbolp name)
 
463
                  (alistp l)
 
464
                  (keyword-value-listp (cdr (header name l)))
 
465
                  (true-listp (dimensions name l))
 
466
                  (equal (length (dimensions name l)) 1)
 
467
                  (integerp (car (dimensions name l)))
 
468
                  (integerp (maximum-length name l))
 
469
                  (< 0 (car (dimensions name l)))
 
470
                  (<= (car (dimensions name l)) (maximum-length name l))
 
471
                  (<= (maximum-length name l) *maximum-positive-32-bit-integer*)
 
472
                  (bounded-integer-alistp l (car (dimensions name l)))))
 
473
    :rule-classes :forward-chaining
 
474
    :hints (("Goal" :in-theory (disable length))))
 
475
 
 
476
 
625
477
;;;++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
626
478
;;;
627
479
;;;  RESET-ARRAY1 name l
630
482
 
631
483
;  The proofs for RESET-ARRAY1 require a few LOCAL facts.
632
484
 
633
 
(local
634
 
 (defthm car-header
635
 
   (implies
636
 
    (array1p name l)
637
 
    (equal (car (header name l))
638
 
           :header))))
639
 
 
640
 
(local
641
 
 (defthm array1p-list-header
642
 
   (implies
643
 
    (array1p name l)
644
 
    (array1p name (list (header name l))))
645
 
   :hints
646
 
   (("Goal"
647
 
     :in-theory (enable array1p)))))
648
 
 
649
 
(local
650
 
 (defthm header-list-header
651
 
  (implies
652
 
   (array1p name l)
653
 
   (equal (header name (list (header name l)))
654
 
          (header name l)))))
655
 
 
656
 
(local
657
 
 (defthm dimensions-list-header
658
 
  (implies
659
 
   (array1p name l)
660
 
   (equal (dimensions name (list (header name l)))
661
 
          (dimensions name l)))))
662
 
 
663
 
(local
664
 
 (defthm default-cons-header
665
 
  (implies
666
 
   (array1p name l)
667
 
   (equal (default name (cons (header name l) x))
668
 
          (default name l)))))
669
 
 
670
 
(local
671
 
 (defthm symbol-alistp-list-header
672
 
  (implies
673
 
   (array1p name l)
674
 
   (symbol-alistp (list (header name l))))))
675
 
 
676
 
(local
677
 
 (defthm symbol-alistp-not-assoc-integer
678
 
  (implies
679
 
   (and (symbol-alistp l)
680
 
        (integerp i))
681
 
   (not (assoc i l)))))
682
 
 
683
 
(local
684
 
 (defthm symbol-alistp-not-compress11
685
 
  (implies
686
 
   (and (symbol-alistp l)
687
 
        (integerp i)
688
 
        (integerp n))
689
 
   (not (compress11 name l i n default)))))
 
485
  (local
 
486
   (defthm car-header
 
487
     (implies (array1p name l)
 
488
              (equal (car (header name l))
 
489
                     :header))))
 
490
 
 
491
  (local
 
492
   (defthm array1p-list-header
 
493
     (implies (array1p name l)
 
494
              (array1p name (list (header name l))))
 
495
     :hints (("Goal" :in-theory (enable array1p)))))
 
496
 
 
497
  (local
 
498
   (defthm header-list-header
 
499
     (implies (array1p name l)
 
500
              (equal (header name (list (header name l)))
 
501
                     (header name l)))))
 
502
 
 
503
  (local
 
504
   (defthm dimensions-list-header
 
505
     (implies (array1p name l)
 
506
              (equal (dimensions name (list (header name l)))
 
507
                     (dimensions name l)))))
 
508
 
 
509
  (local
 
510
   (defthm default-cons-header
 
511
     (implies (array1p name l)
 
512
              (equal (default name (cons (header name l) x))
 
513
                     (default name l)))))
 
514
 
 
515
  (local
 
516
   (defthm symbol-alistp-list-header
 
517
     (implies (array1p name l)
 
518
              (symbol-alistp (list (header name l))))))
 
519
 
 
520
  (local
 
521
   (defthm symbol-alistp-not-assoc-integer
 
522
     (implies (and (symbol-alistp l)
 
523
                   (integerp i))
 
524
              (not (assoc i l)))))
 
525
 
 
526
  (local
 
527
   (defthm symbol-alistp-not-compress11
 
528
     (implies (and (symbol-alistp l)
 
529
                   (integerp i)
 
530
                   (integerp n))
 
531
              (not (compress11 name l i n default))))))
 
532
 
690
533
 
691
534
;  HEADER, DEFAULT, and DIMENSIONS are characterized, so we DISABLE them.
692
535
 
693
536
(local (in-theory (disable header default dimensions)))
694
537
 
695
 
(defun reset-array1 (name l)
696
 
  ":doc-section array1
697
 
  Clear an 1-dimensional array.
698
 
  ~/~/
699
 
  The function (RESET-ARRAY1 name l) returns a 1-dimensional array whose
700
 
  alist is simply the HEADER of l.  This has the effect of resetting the
701
 
  array, i.e., reading the new array at any address will return the default
702
 
  value.  The implementation is simply to redefine the array as the HEADER of
703
 
  the old array.  Thus all of the HEADER information is carried over to the
704
 
  new array. 
705
 
 
706
 
  Note that an alternate definition is available as the lemma RESET-ARRAY1*.
707
 
  ~/" 
708
 
 
709
 
  (declare (xargs :guard (array1p name l)))
710
 
 
711
 
  (compress1 name (list (header name l))))
712
 
 
713
 
(defthm reset-array1*
714
 
  (implies
715
 
   (array1p name l)
716
 
   (equal (reset-array1 name l)
717
 
          (list (header name l))))
718
 
  :hints
719
 
  (("Goal"
720
 
    :in-theory (enable compress1 compress11)))
721
 
  :doc ":doc-section reset-array1
722
 
  Rewrite: (RESET-ARRAY1 name l) = (LIST (HEADER name l)).
723
 
  ~/~/
724
 
  This definition of RESET-ARRAY1 is logically equivalent to the actual
725
 
  definition. The actual definition, which includes a COMPRESS1 call, has the
726
 
  run-time side-effect of re-installing the new array.  The COMPRESS1 is
727
 
  logically redundant, however.
728
 
 
729
 
  This lemma is exported DISABLED, however this is the preferred definition
730
 
  to use to reason about RESET-ARRAY1. ~/ ")
 
538
(defsection reset-array1
 
539
  :parents (array1)
 
540
  :short "Clear an 1-dimensional array."
 
541
  :long "<p>The function (RESET-ARRAY1 name l) returns a 1-dimensional array
 
542
whose alist is simply the HEADER of l.  This has the effect of resetting the
 
543
array, i.e., reading the new array at any address will return the default
 
544
value.  The implementation is simply to redefine the array as the HEADER of the
 
545
old array.  Thus all of the HEADER information is carried over to the new
 
546
array.</p>
 
547
 
 
548
<p>Note that an alternate definition is available as the lemma
 
549
RESET-ARRAY1*.</p>"
 
550
 
 
551
  (defun reset-array1 (name l)
 
552
    (declare (xargs :guard (array1p name l)))
 
553
    (compress1 name (list (header name l)))))
 
554
 
 
555
(defsection reset-array1*
 
556
  :parents (reset-array1)
 
557
  :short "Rewrite: (RESET-ARRAY1 name l) = (LIST (HEADER name l))."
 
558
  :long "<p>This definition of RESET-ARRAY1 is logically equivalent to the
 
559
actual definition. The actual definition, which includes a COMPRESS1 call, has
 
560
the run-time side-effect of re-installing the new array.  The COMPRESS1 is
 
561
logically redundant, however.</p>
 
562
 
 
563
<p>This lemma is exported DISABLED, however this is the preferred definition to
 
564
use to reason about RESET-ARRAY1.</p>"
 
565
 
 
566
  (defthm reset-array1*
 
567
    (implies (array1p name l)
 
568
             (equal (reset-array1 name l)
 
569
                    (list (header name l))))
 
570
    :hints (("Goal" :in-theory (enable compress1 compress11)))))
731
571
 
732
572
;  We can now reason with the simple definition RESET-ARRAY1*.
733
573
 
734
574
(local (in-theory (disable reset-array1)))
735
575
 
736
 
(defthm array1p-reset-array1
737
 
  (implies
738
 
   (array1p name l)
739
 
   (array1p name (reset-array1 name l)))
740
 
  :doc ":doc-section array1-lemmas
741
 
  Rewrite: (ARRAY1P name (RESET-ARRAY1 name l)).
742
 
  ~/~/~/")
743
 
 
744
 
(defthm array1p-reset-array1-properties
745
 
  (implies
746
 
   (array1p name l)
747
 
   (and
748
 
    (equal (header name (reset-array1 name l))
749
 
           (header name l))
750
 
    (equal (dimensions name (reset-array1 name l))
751
 
           (dimensions name l))
752
 
    (equal (maximum-length name (reset-array1 name l))
753
 
           (maximum-length name l))
754
 
    (equal (default name (reset-array1 name l))
755
 
           (default name l))))
756
 
  :doc ":doc-section array1-lemmas
757
 
  Rewrite:
758
 
  (HEADER name         (RESET-ARRAY1 name l)) = (HEADER name l).
759
 
  (DIMENSIONS name     (RESET-ARRAY1 name l)) = (DIMENSIONS name l).
760
 
  (MAXIMUM-LENGTH name (RESET-ARRAY1 name l)) = (MAXIMUM-LENGTH name l).
761
 
  (DEFAULT name        (RESET-ARRAY1 name l)) = (DEFAULT name l).
762
 
  ~/~/~/")
763
 
 
764
 
(defthm aref1-reset-array1
765
 
  (implies
766
 
   (and (array1p name l)
767
 
        (integerp index))
768
 
   (equal (aref1 name (reset-array1 name l) index)
769
 
          (default name l))))
 
576
(defsection-progn reset-array1-lemmas
 
577
  :extension reset-array1
 
578
 
 
579
  (defthm array1p-reset-array1
 
580
    (implies (array1p name l)
 
581
             (array1p name (reset-array1 name l))))
 
582
 
 
583
  (defthm array1p-reset-array1-properties
 
584
    (implies (array1p name l)
 
585
             (and (equal (header name (reset-array1 name l))
 
586
                         (header name l))
 
587
                  (equal (dimensions name (reset-array1 name l))
 
588
                         (dimensions name l))
 
589
                  (equal (maximum-length name (reset-array1 name l))
 
590
                         (maximum-length name l))
 
591
                  (equal (default name (reset-array1 name l))
 
592
                         (default name l)))))
 
593
 
 
594
  (defthm aref1-reset-array1
 
595
    (implies (and (array1p name l)
 
596
                  (integerp index))
 
597
             (equal (aref1 name (reset-array1 name l) index)
 
598
                    (default name l)))))
770
599
 
771
600
(in-theory (disable reset-array1*))
772
601
 
773
 
 
 
602
 
774
603
;;;****************************************************************************
775
604
;;;
776
605
;;;  Theories
777
606
;;;
778
607
;;;****************************************************************************
779
608
 
780
 
(deftheory array1-functions 
781
 
  '(array1p aset1 aref1 compress1 header dimensions maximum-length
782
 
            default reset-array1)
783
 
  :doc ":doc-section array1
784
 
  A theory of all functions specific to 1-dimensional arrays.
785
 
  ~/
786
 
  This theory must be DISABLEd in order for the lemmas exported by the
787
 
  \"array1\" book to be applicable.~/~/")
788
 
 
789
 
(deftheory array1-lemmas 
 
609
(defsection array1-functions
 
610
  :parents (array1)
 
611
  :short "A theory of all functions specific to 1-dimensional arrays."
 
612
  :long "<p>This theory must be DISABLEd in order for the lemmas exported by
 
613
the \"array1\" book to be applicable.</p>"
 
614
 
 
615
  (deftheory array1-functions
 
616
    '(array1p aset1 aref1 compress1 header dimensions maximum-length
 
617
              default reset-array1)))
 
618
 
 
619
(deftheory array1-lemmas
790
620
  '(array1p-compress1
791
621
    array1p-compress1-properties
792
622
    array1p-aset1 array1p-aset1-properties
796
626
    array1p-reset-array1 array1p-reset-array1-properties
797
627
    aref1-reset-array1))
798
628
 
799
 
(deftheory array1-disabled-lemmas
800
 
  '(aref1-aset1-equal aref1-aset1-not-equal reset-array1*)
801
 
  :doc ":doc-section array1
802
 
 
803
 
  A theory of all rules exported DISABLEd by the \"array1\" book.
804
 
  ~/ 
805
 
 
806
 
  Note that in order for these rules to be applicable you will first need to
807
 
  (DISABLE ARRAY1-FUNCTIONS).  Look at the :DOC for each lemma for an
808
 
  explanation of why the lemma is exported DISABLEd. The following rules are
809
 
  found in this theory:~/~/ 
810
 
 
811
 
  :cite aref1-aset1-equal
812
 
  :cite aref1-aset1-not-equal
813
 
  :cite reset-array1*")
814
 
 
815
 
 
 
629
(defsection array1-disabled-lemmas
 
630
  :short "A theory of all rules exported DISABLEd by the \"array1\" book."
 
631
  :long "<p>Note that in order for these rules to be applicable you will first
 
632
need to disable @(see array1-functions).  Look at the :DOC for each lemma for
 
633
an explanation of why the lemma is exported DISABLEd.</p>"
 
634
 
 
635
  (deftheory array1-disabled-lemmas
 
636
    '(aref1-aset1-equal aref1-aset1-not-equal reset-array1*)))
 
637
 
 
638
 
816
639
;;;****************************************************************************
817
640
;;;
818
641
;;;    DEFARRAY1TYPE
819
642
;;;
820
643
;;;****************************************************************************
821
 
        
 
644
 
 
645
(defsection defarray1type
 
646
  :parents (array1)
 
647
  :short "Characterize 1-dimensional arrays with a fixed element type."
 
648
  :long "<p>Example form:</p>
 
649
 
 
650
@({
 
651
  (DEFARRAY1TYPE INTEGERP-ARRAY1P INTEGERP)
 
652
})
 
653
 
 
654
<p>The above example defines a recognizer, INTEGERP-ARRAYP, for 1-dimensional
 
655
arrays whose elements are all INTEGERP.</p>
 
656
 
 
657
<p>General form:</p>
 
658
 
 
659
@({
 
660
  (DEF1ARRAYTYPE recognizer predicate
 
661
                 &key size doc
 
662
                      (aref1-lemma-rule-classes ':REWRITE)
 
663
                      (aset1-lemma-rule-classes ':REWRITE))
 
664
})
 
665
 
 
666
<p>DEFARRAY1TYPE defines a recognizer for 1-dimensional arrays whose elements
 
667
are all of a single type.  The recognizer argument is a symbol that is used as
 
668
the name of the recognizer.  The predicate argument should be a 1-argument,
 
669
unguarded Boolean function that recognizes objects of the desired type.  The
 
670
predicate may either be a symbol (the name of the predicate), or a LAMBDA
 
671
expression.</p>
 
672
 
 
673
<p>If :SIZE is specified it should be a variable-free term that will evaluate
 
674
to a positive integer.  If specified, then the recognizer will only recognize
 
675
1-dimensional arrays of the given type and of a fixed size.</p>
 
676
 
 
677
<p>If :DOC is specified it should be a string, and it will be inserted as the
 
678
documentation string in the recognizer.</p>
 
679
 
 
680
<p>DEFARRAY1TYPE defines a recognizer:</p>
 
681
 
 
682
@({ (recognizer NAME L) })
 
683
 
 
684
<p>and proves 4 useful theorems about it.  If the :SIZE is not specified then
 
685
the three theorems will be:</p>
 
686
 
 
687
@({
 
688
  1. (IMPLIES (recognizer NAME L)
 
689
              (ARRAY1P NAME L))
 
690
 
 
691
  2. (IMPLIES (AND (recognizer NAME L)
 
692
                   (INTEGERP N))
 
693
              (predicate (AREF1 NAME L N)))
 
694
 
 
695
  3. (IMPLIES (AND (recognizer NAME L)
 
696
                   (< N (CAR (DIMENSIONS NAME L)))
 
697
                   (INTEGERP N)
 
698
                   (>= N 0)
 
699
                   (predicate VAL))
 
700
              (recognizer NAME (ASET1 NAME L N VAL)))
 
701
 
 
702
  4. (IMPLIES (recognizer NAME l)
 
703
              (recognizer NAME (RESET-ARRAY1 name l)))
 
704
})
 
705
 
 
706
<p>If :SIZE is specified then the first and third theorems become:</p>
 
707
 
 
708
@({
 
709
  1. (IMPLIES (recognizer NAME L)
 
710
              (AND (ARRAY1P NAME L)
 
711
                   (EQUAL (CAR (DIMENSIONS name l))
 
712
                          size)))
 
713
 
 
714
  3. (IMPLIES (AND (recognizer NAME L)
 
715
                   (< N size)
 
716
                   (INTEGERP N)
 
717
                   (>= N 0)
 
718
                   (predicate VAL))
 
719
              (recognizer NAME (ASET1 NAME L N VAL)))
 
720
})
 
721
 
 
722
<p>The first theorem is stored as both :REWRITE and :FORWARD-CHAINING rules.
 
723
The :RULE-CLASSES of the second and third lemmas default to :REWRITE, but are
 
724
selectable by the user by means of the :AREF1-LEMMA-RULE-CLASSES and
 
725
:ASET1-LEMMA-RULE-CLASSSES arguments to DEFARRAY1TYPE (respectively).  If
 
726
using :RULE-CLASSES other than :REWRITE the user should bear in mind the
 
727
documented restrictions on the applicability of :TYPE-PRESCRIPTION and
 
728
:FORWARD-CHAINING rules.  The fourth rule is always a :REWRITE rule.</p>
 
729
 
 
730
<p>Note the the recognizer is a very strong recognizer that specifies that the
 
731
array alist is a BOUNDED-INTEGER-ALISTP whose elements all satisfy the type
 
732
predicate.  The recognizer also specifies that the default element of the array
 
733
satisfies the predicate as well.</p>
 
734
 
 
735
<p>WARNING: The recognizer is defined in terms of a recursive recognizer, named
 
736
@('<recognizer>-FN').  THE RECURSIVE RECOGNIZER SHOULD BE COMPILED BEFORE YOU
 
737
TRY TO EXECUTE IT, OR IT MAY CAUSE A STACK OVERFLOW.  Also note that the
 
738
recognizer will be DISABLEd after execution of this macro.  The user must
 
739
insure that the recognizer remains DISABLEd, otherwise the above lemmas will
 
740
never be applied.</p>
 
741
 
 
742
<p>DEFARRAY1TYPE proves the generated lemmas in a minimal, ENCAPSULATEd theory
 
743
that should guarantee that the proofs always succeed.  If one should encounter
 
744
a case where a proof fails (as opposed to a translation or other syntax
 
745
failure), please notify the author.</p>")
 
746
 
822
747
(defmacro defarray1type
823
748
  (recognizer predicate &key
824
749
              size doc
825
750
              (aref1-lemma-rule-classes ':REWRITE)
826
751
              (aset1-lemma-rule-classes ':REWRITE))
827
752
 
828
 
  ":doc-section array1
829
 
  
830
 
  Characterize 1-dimensional arrays with a fixed element type.
831
 
  ~/
832
 
 
833
 
  Example form:
834
 
 
835
 
  (DEFARRAY1TYPE INTEGERP-ARRAY1P INTEGERP)
836
 
 
837
 
  The above example defines a recognizer, INTEGERP-ARRAYP, for 1-dimensional
838
 
  arrays whose elements are all INTEGERP.~/
839
 
 
840
 
  General form:
841
 
 
842
 
  (DEF1ARRAYTYPE recognizer predicate 
843
 
                 &key size doc
844
 
                      (aref1-lemma-rule-classes ':REWRITE)
845
 
                      (aset1-lemma-rule-classes ':REWRITE))
846
 
 
847
 
  DEFARRAY1TYPE defines a recognizer for 1-dimensional arrays whose elements
848
 
  are all of a single type.  The recognizer argument is a symbol that is used
849
 
  as the name of the recognizer.  The predicate argument should be a
850
 
  1-argument, unguarded Boolean function that recognizes objects of the
851
 
  desired type.  The predicate may either be a symbol (the name of the
852
 
  predicate), or a LAMBDA expression.  
853
 
 
854
 
  If :SIZE is specified it should be a variable-free term that will evaluate
855
 
  to a positive integer.  If specified, then the recognizer will only
856
 
  recognize 1-dimensional arrays of the given type and of a fixed size.
857
 
 
858
 
  If :DOC is specified it should be a string, and it will be inserted as the
859
 
  documentation string in the recognizer.
860
 
 
861
 
  DEFARRAY1TYPE defines a recognizer:
862
 
 
863
 
  (recognizer NAME L),
864
 
 
865
 
  and proves 4 useful theorems about it.  If the :SIZE is not specified then
866
 
  the three theorems will be:
867
 
 
868
 
  1. (IMPLIES
869
 
       (recognizer NAME L)
870
 
       (ARRAY1P NAME L))
871
 
 
872
 
  2. (IMPLIES
873
 
      (AND (recognizer NAME L)
874
 
           (INTEGERP N))
875
 
      (predicate (AREF1 NAME L N)))
876
 
 
877
 
  3. (IMPLIES
878
 
      (AND (recognizer NAME L)
879
 
           (< N (CAR (DIMENSIONS NAME L)))
880
 
           (INTEGERP N)
881
 
           (>= N 0)
882
 
           (predicate VAL))
883
 
      (recognizer NAME (ASET1 NAME L N VAL)))
884
 
 
885
 
  4. (IMPLIES
886
 
      (recognizer NAME l)
887
 
      (recognizer NAME (RESET-ARRAY1 name l)))
888
 
 
889
 
  If :SIZE is specified then the first and third theorems become:
890
 
 
891
 
  1. (IMPLIES
892
 
      (recognizer NAME L)
893
 
      (AND (ARRAY1P NAME L)
894
 
           (EQUAL (CAR (DIMENSIONS name l))
895
 
                  size)))
896
 
 
897
 
  3. (IMPLIES
898
 
      (AND (recognizer NAME L)
899
 
           (< N size)
900
 
           (INTEGERP N)
901
 
           (>= N 0)
902
 
           (predicate VAL))
903
 
      (recognizer NAME (ASET1 NAME L N VAL)))
904
 
 
905
 
  The first theorem is stored as both :REWRITE and :FORWARD-CHAINING rules.
906
 
  The :RULE-CLASSES of the second and third lemmas default to :REWRITE, but
907
 
  are selectable by the user by means of the :AREF1-LEMMA-RULE-CLASSES and
908
 
  :ASET1-LEMMA-RULE-CLASSSES arguments to DEFARRAY1TYPE (respectively).  If
909
 
  using :RULE-CLASSES other than :REWRITE the user should bear in mind the
910
 
  documented restrictions on the applicability of :TYPE-PRESCRIPTION and
911
 
  :FORWARD-CHAINING rules.  The fourth rule is always a :REWRITE rule.
912
 
 
913
 
  Note the the recognizer is a very strong recognizer that specifies that the
914
 
  array alist is a BOUNDED-INTEGER-ALISTP whose elements all satisfy the type
915
 
  predicate.  The recognizer also specifies that the default element of the
916
 
  array satisfies the predicate as well.
917
 
 
918
 
  WARNING: The recognizer is defined in terms of a recursive recoignizer,
919
 
  named <recognizer>-FN.  THE RECURSIVE RECOGNIZER SHOULD BE COMPILED BEFORE
920
 
  YOU TRY TO EXECUTE IT, OR IT MAY CAUSE A STACK OVERFLOW.  Also note that
921
 
  the recognizer will be DISABLEd after execution of this macro.  The user
922
 
  must insure that the recognizer remains DISABLEd, otherwise the above
923
 
  lemmas will never be applied.
924
 
 
925
 
  DEFARRAY1TYPE proves the generated lemmas in a minimal, ENCAPSULATEd theory
926
 
  that should guarantee that the proofs always succeed.  If one should
927
 
  encounter a case where a proof fails (as opposed to a translation or other
928
 
  syntax failure), please notify the author.~/"
929
 
 
930
753
  (declare (xargs :guard (and (symbolp recognizer)
931
754
                              (pseudo-termp predicate)
932
755
                              (implies doc (stringp doc)))))
941
764
       recognizer))
942
765
     (recognizer-lemma
943
766
      (intern-in-package-of-symbol
944
 
       (coerce (packn1 (list recognizer '-array1p)) 'string) 
 
767
       (coerce (packn1 (list recognizer '-array1p)) 'string)
945
768
       recognizer))
946
769
     (aref1-lemma
947
770
      (intern-in-package-of-symbol
948
 
       (coerce (packn1 (list recognizer '-aref1)) 'string) 
 
771
       (coerce (packn1 (list recognizer '-aref1)) 'string)
949
772
       recognizer))
950
773
     (aset1-lemma
951
774
      (intern-in-package-of-symbol
952
 
       (coerce (packn1 (list recognizer '-aset1)) 'string) 
 
775
       (coerce (packn1 (list recognizer '-aset1)) 'string)
953
776
       recognizer))
954
777
     (reset-array1-lemma
955
778
      (intern-in-package-of-symbol
956
 
       (coerce (packn1 (list recognizer '-reset-array1)) 'string) 
 
779
       (coerce (packn1 (list recognizer '-reset-array1)) 'string)
957
780
       recognizer)))
958
781
 
959
782
    `(ENCAPSULATE ()
960
783
 
961
784
       ;;  Set up a theory guaranteed to admit the functions and prove the
962
785
       ;;  lemmas.  We assume that the "array1" book has been loaded!
963
 
       
 
786
 
964
787
       (LOCAL (IN-THEORY (THEORY 'GROUND-ZERO)))
965
788
       (LOCAL (IN-THEORY (DISABLE ARRAY1-FUNCTIONS)))
966
789
       (LOCAL (IN-THEORY (ENABLE ARRAY1-LEMMAS)))
997
820
 
998
821
       (LOCAL
999
822
        (DEFTHM DEFARRAY1TYPE-ASSOC-PROPERTIES
1000
 
         (IMPLIES
1001
 
          (AND (,recognizer-fn L N)
1002
 
               (ASSOC I L)
1003
 
               (INTEGERP I))
1004
 
          (AND (CONSP (ASSOC I L))
1005
 
               (INTEGERP (CAR (ASSOC I L)))
1006
 
               (>= (CAR (ASSOC I L)) 0)
1007
 
               (< (CAR (ASSOC I L)) N)
1008
 
               (,predicate (CDR (ASSOC I L)))))))
 
823
          (IMPLIES (AND (,recognizer-fn L N)
 
824
                        (ASSOC I L)
 
825
                        (INTEGERP I))
 
826
                   (AND (CONSP (ASSOC I L))
 
827
                        (INTEGERP (CAR (ASSOC I L)))
 
828
                        (>= (CAR (ASSOC I L)) 0)
 
829
                        (< (CAR (ASSOC I L)) N)
 
830
                        (,predicate (CDR (ASSOC I L)))))))
1009
831
 
1010
832
       (LOCAL
1011
833
        (DEFTHM DEFARRAY1TYPE-CONS-HEADER
1012
 
         (IMPLIES
1013
 
          (ARRAY1P NAME L)
1014
 
          (EQUAL (,recognizer-fn (CONS (HEADER NAME L) X) MAX)
1015
 
                 (,recognizer-fn X MAX)))))
 
834
          (IMPLIES (ARRAY1P NAME L)
 
835
                   (EQUAL (,recognizer-fn (CONS (HEADER NAME L) X) MAX)
 
836
                          (,recognizer-fn X MAX)))))
1016
837
 
1017
838
       (LOCAL
1018
839
        (DEFTHM DEFARRAY1TYPE-COMPRESS11
1019
 
         (IMPLIES
1020
 
          (AND (,recognizer-fn L N)
1021
 
               (INTEGERP I)
1022
 
               (INTEGERP N))
1023
 
          (,recognizer-fn (COMPRESS11 NAME L I N DEFAULT)
1024
 
                          N))))
 
840
          (IMPLIES (AND (,recognizer-fn L N)
 
841
                        (INTEGERP I)
 
842
                        (INTEGERP N))
 
843
                   (,recognizer-fn (COMPRESS11 NAME L I N DEFAULT)
 
844
                                   N))))
1025
845
 
1026
846
       (LOCAL
1027
847
        (DEFTHM DEFARRAY1TYPE-ASET1
1028
 
          (IMPLIES
1029
 
           (AND (ARRAY1P NAME L)
1030
 
                (EQUAL SIZE (CAR (DIMENSIONS NAME L)))
1031
 
                (,recognizer-fn L SIZE)
1032
 
                (,predicate (DEFAULT NAME L))
1033
 
                (INTEGERP N)
1034
 
                (,predicate VAL)
1035
 
                (NOT (< N 0))
1036
 
                (< N SIZE))
1037
 
           (,recognizer-fn (ASET1 NAME L N VAL) SIZE))
1038
 
          :HINTS
1039
 
          (("GOAL"
1040
 
            :IN-THEORY (ENABLE COMPRESS1 ASET1)))))
 
848
          (IMPLIES (AND (ARRAY1P NAME L)
 
849
                        (EQUAL SIZE (CAR (DIMENSIONS NAME L)))
 
850
                        (,recognizer-fn L SIZE)
 
851
                        (,predicate (DEFAULT NAME L))
 
852
                        (INTEGERP N)
 
853
                        (,predicate VAL)
 
854
                        (NOT (< N 0))
 
855
                        (< N SIZE))
 
856
                   (,recognizer-fn (ASET1 NAME L N VAL) SIZE))
 
857
          :HINTS (("GOAL" :IN-THEORY (ENABLE COMPRESS1 ASET1)))))
1041
858
 
1042
859
       (LOCAL
1043
860
        (DEFTHM DEFARRAY1TYPE-RESET-ARRAY1
1044
 
          (IMPLIES
1045
 
           (ARRAY1P NAME L)
1046
 
           (,recognizer-fn (RESET-ARRAY1 NAME L) N))
1047
 
          :HINTS
1048
 
          (("Goal"
1049
 
            :IN-THEORY (ENABLE RESET-ARRAY1*)))))
 
861
          (IMPLIES (ARRAY1P NAME L)
 
862
                   (,recognizer-fn (RESET-ARRAY1 NAME L) N))
 
863
          :HINTS (("Goal" :IN-THEORY (ENABLE RESET-ARRAY1*)))))
1050
864
 
1051
865
       ;; The recognizer lemma.
1052
866
 
1053
867
       (DEFTHM ,recognizer-lemma
1054
 
         (IMPLIES
1055
 
          (,recognizer NAME L)
1056
 
          (AND (ARRAY1P NAME L)
1057
 
               ,@(if size (list `(EQUAL (CAR (DIMENSIONS NAME L)) ,size))
1058
 
                   NIL)))
 
868
         (IMPLIES (,recognizer NAME L)
 
869
                  (AND (ARRAY1P NAME L)
 
870
                       ,@(if size (list `(EQUAL (CAR (DIMENSIONS NAME L)) ,size))
 
871
                           NIL)))
1059
872
         :RULE-CLASSES (:REWRITE :FORWARD-CHAINING))
1060
873
 
1061
874
       ;; AREF1 returns objects of the proper type.
1062
875
 
1063
876
       (DEFTHM ,aref1-lemma
1064
 
         (IMPLIES
1065
 
          (AND (,recognizer NAME L)
1066
 
               (INTEGERP N))
1067
 
          (,predicate (AREF1 NAME L N)))
 
877
         (IMPLIES (AND (,recognizer NAME L)
 
878
                       (INTEGERP N))
 
879
                  (,predicate (AREF1 NAME L N)))
1068
880
         :RULE-CLASSES ,aref1-lemma-rule-classes
1069
 
         :HINTS
1070
 
         (("Goal"
1071
 
           :IN-THEORY (ENABLE AREF1))))
 
881
         :HINTS (("Goal" :IN-THEORY (ENABLE AREF1))))
1072
882
 
1073
883
       ;;  ASET1 returns arrays of the proper type.
1074
884
 
1075
885
       (DEFTHM ,aset1-lemma
1076
 
         (IMPLIES
1077
 
          (AND (,recognizer NAME L)
1078
 
               (< N ,size-form)
1079
 
               (INTEGERP N)
1080
 
               (>= N 0)
1081
 
               (,predicate VAL))
1082
 
          (,recognizer NAME (ASET1 NAME L N VAL)))
 
886
         (IMPLIES (AND (,recognizer NAME L)
 
887
                       (< N ,size-form)
 
888
                       (INTEGERP N)
 
889
                       (>= N 0)
 
890
                       (,predicate VAL))
 
891
                  (,recognizer NAME (ASET1 NAME L N VAL)))
1083
892
         :RULE-CLASSES ,aset1-lemma-rule-classes)
1084
893
 
1085
894
       ;;  RESET-ARRAY1 returns arrays of the proper type.
1086
895
 
1087
896
       (defthm ,reset-array1-lemma
1088
 
         (implies
1089
 
          (,recognizer name l)
1090
 
          (,recognizer name (reset-array1 name l))))
 
897
         (implies (,recognizer name l)
 
898
                  (,recognizer name (reset-array1 name l))))
1091
899
 
1092
900
       ;;  DISABLE the recognizer.
1093
901
 
1094
902
       (IN-THEORY (DISABLE ,recognizer)))))
1095
 
 
1096
 
        
1097
 
       
1098
 
     
 
 
b'\\ No newline at end of file'