← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/1999/ste/run.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/1999/ste/run.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
(include-book "state")
 
4
 
 
5
 
 
6
(deflisttyped r-p s-p)
 
7
 
 
8
; Added by Matt K. for v2-9, upon introduction of rewrite-solidify-plus for
 
9
; making a second pass of rewriting for relieving hypotheses, upon seeing
 
10
; dominant usage in ste-thm-backward (file fundamental.lisp) with
 
11
; show-accumulated-persistence.
 
12
(in-theory (disable r-p-car))
 
13
 
 
14
(defuntyped r-nmp  ((r-p r) (naturalp n) (naturalp m)) t
 
15
  booleanp nil
 
16
  (if (and (consp r) (< 0 n))
 
17
      (and (equal (len (car r)) m)
 
18
           (r-nmp (cdr r) (1- n) m))
 
19
    (and (equal r nil)
 
20
         (equal n 0))))
 
21
 
 
22
(defthm r-nmp-nil
 
23
  (implies
 
24
   (and (equal n 0)
 
25
        (equal m 0))
 
26
   (r-nmp nil n m)))
 
27
 
 
28
(defthm r-nmp-cons
 
29
  (implies (and ;(r-p r)
 
30
                (s-p s)
 
31
                (positivep n)
 
32
                (r-nmp r (1- n) m)
 
33
                (equal (len s) m))
 
34
           (r-nmp (cons s r) n m)))
 
35
;;;
 
36
;;; R_MAKE def and facts
 
37
;;;
 
38
(defuntyped r-make ((naturalp n) (s-p s)) t
 
39
  r-p nil
 
40
  (if (positivep n)
 
41
      (cons s (r-make (1- n) s))
 
42
    nil))
 
43
 
 
44
(defthm r-make-len
 
45
  (implies (and (s-p s)
 
46
                (naturalp n))
 
47
           (equal (len (r-make n s)) n)))
 
48
 
 
49
(defthm r-make-r-nmp
 
50
  (implies (and (positivep n)
 
51
                (s-p s)
 
52
                (equal (len s) m))
 
53
           (r-nmp (r-make n s) n m)))
 
54
;;;
 
55
;;; R-LUB
 
56
;;;
 
57
(defuntyped r-lub (r1 r2) t
 
58
  r-p nil
 
59
  (if (and (r-p r1) (r-p r2))
 
60
      (if (consp r1)
 
61
          (if (consp r2)
 
62
              (cons (s-lub (car r1) (car r2))
 
63
                    (r-lub (cdr r1) (cdr r2)))
 
64
            r1)
 
65
        r2)
 
66
    nil))
 
67
 
 
68
 
 
69
(defthm r-lub-len
 
70
  (implies (and (r-p r1)
 
71
                (r-p r2)
 
72
                )
 
73
           (equal (len (r-lub r1 r2))
 
74
                  (max (len r1) (len r2)))))
 
75
 
 
76
(defthm r-nmp-r-lub
 
77
  (implies (and (r-nmp r1 n m)
 
78
                (r-nmp r2 n m))
 
79
           (r-nmp (r-lub r1 r2) n m)))
 
80
 
 
81
(defthm r-lub-commutes
 
82
  (equal (r-lub r1 r2) (r-lub r2 r1))
 
83
  :rule-classes nil)
 
84
 
 
85
;;;
 
86
;;; R-LTE
 
87
;;;
 
88
(defuntyped r-lte ((r-p r1) (r-p r2)) t
 
89
  booleanp nil
 
90
  (if (and (consp r1) (consp r2))
 
91
      (and (s-lte (car r1) (car r2))
 
92
           (r-lte (cdr r1) (cdr r2)))
 
93
    (and (equal r1 nil)
 
94
         (equal r2 nil))))
 
95
 
 
96
(defthm r-lte-reflexive
 
97
  (implies (r-p r)
 
98
           (r-lte r r)))
 
99
 
 
100
(defthm r-lte-antisymmetric
 
101
  (implies (and (r-p a)
 
102
                (r-p b)
 
103
                (r-lte a b)
 
104
                (r-lte b a))
 
105
           (equal a b))
 
106
  :rule-classes nil)
 
107
 
 
108
(defthm r-lte-transitive
 
109
  (implies (and (r-p a)
 
110
                (r-p b)
 
111
                (r-lte a b)
 
112
                (r-lte b c))
 
113
           (r-lte a c)))
 
114
;;;
 
115
;;;
 
116
;;;
 
117
 
 
118
 
 
119
 
 
120
(defthm r-lte-r-lub-r1
 
121
  (implies (and (r-nmp r1 n m)
 
122
                (r-nmp r2 n m))
 
123
           (r-lte r1 (r-lub r1 r2)))  )
 
124
 
 
125
(defthm r-lte-r-lub-r2
 
126
  (implies (and (r-nmp r1 n m)
 
127
                (r-nmp r2 n m))
 
128
           (r-lte r2 (r-lub r1 r2)))  )
 
129
 
 
130
;;
 
131
;;;
 
132
;;
 
133
 
 
134
(defthm r-nmp-lte-0
 
135
  (IMPLIES (AND (R-P R1)
 
136
              (NOT R2)
 
137
              (CONSP R1)
 
138
              (R-NMP R1 N1 M1)
 
139
              (R-NMP R1 N M))
 
140
         (<= N1 N)))
 
141
 
 
142
(defthm consp-r-lub-5
 
143
  (implies (and (r-p r1)
 
144
                (r-p r2)
 
145
                (or (consp r1)
 
146
                    (consp r2))
 
147
                )
 
148
           (consp (r-lub r1 r2))))
 
149
 
 
150
(defthm b-p-nth-car-r-lub-cons-6
 
151
  (IMPLIES (AND (INTEGERP L3)
 
152
                (<= 0 L3)
 
153
                (S-P R3)
 
154
                (R-P R4)
 
155
                (R-P R2)
 
156
                (EQUAL (NTH L3 R3) 'TOP))
 
157
           (B-P (NTH L3 (CAR (R-LUB (CONS R3 R4) R2))))))
 
158
 
 
159
(defthm consp-r-lub-cons-4
 
160
  (implies (and (s-p s1)
 
161
                (r-p r1)
 
162
                (r-p r2)
 
163
            )
 
164
           (consp (r-lub (cons s1 r1) r2)))
 
165
  :hints (("Goal" :expand ((r-lub (cons s1 r1) r2))))
 
166
  )
 
167
 
 
168
(defthm cons-r-make-collapse
 
169
  (implies (and (naturalp n)
 
170
                )
 
171
           (equal (cons (s-make m v)
 
172
                        (r-make n (s-make m v)))
 
173
                  (r-make (1+ n) (s-make m v)))))
 
174
 
 
175
 
 
176
(defthm equal-r-make-bottom
 
177
  (implies (and (naturalp m)
 
178
                (r-p r)
 
179
                (r-lte r (r-make (len r) (s-make m 'x)))
 
180
                )
 
181
           (equal (r-make (len r) (s-make m 'x)) r))
 
182
  :hints (("Goal" :induct (r-p r)
 
183
           ;; r-p-car re-enabled by Matt K. to compensate for v2-9 change of
 
184
           ;; disabling this rule near the top of this file.
 
185
           :in-theory (enable r-p-car))
 
186
          ("Subgoal *1/2.2'" :use ((:instance s-lte-implies-len-equal
 
187
                                              (s1 r1) (s2 (s-make m 'x)))))))
 
188
 
 
189
(defthm r-lte-implies-len-equal
 
190
  (implies (r-lte r1 r2)
 
191
           (equal (len r1) (len r2)))
 
192
  :rule-classes nil)
 
193
 
 
194
(defthm equal-r-make-bottom-2
 
195
  (implies (and (naturalp n)
 
196
                (naturalp m)
 
197
                (r-lte r (r-make n (s-make m 'x)))
 
198
                )
 
199
           (equal (r-make n (s-make m 'x)) r))
 
200
  :hints (("Goal" :do-not-induct t
 
201
           :use ((:instance equal-r-make-bottom)
 
202
                 (:instance r-lte-implies-len-equal (r1 r) (r2 (r-make n (s-make m 'x)))) )
 
203
           ))
 
204
  )
 
205
 
 
206
(defthm r-lub-same
 
207
  (implies (r-p r)
 
208
           (equal (r-lub r r) r)))
 
209
 
 
210
(defthm r-make-1
 
211
  (implies (s-p s)
 
212
           (equal (r-make 1 s)
 
213
                  (list s)))
 
214
  :hints (("Goal" :expand ((r-make 1 s)))))
 
215
 
 
216
(defuntyped s-consistent ((s-p s)) t
 
217
  booleanp nil
 
218
  (if (consp s)
 
219
      (and (not (equal (car s) 'top))
 
220
           (s-consistent (cdr s)))
 
221
    t))
 
222
 
 
223
(defuntyped r-consistent ((r-p r)) t
 
224
  booleanp nil
 
225
  (if (consp r)
 
226
      (and (s-consistent (car r))
 
227
           (r-consistent (cdr r)))
 
228
    t))
 
229
 
 
230
(defthm  consp-r-make-plus-1
 
231
  (implies (and (s-p s)
 
232
                (naturalp n)
 
233
                )
 
234
           (consp (r-make (+ 1 n) s))))
 
235
 
 
236
 
 
237
 
 
238
 
 
239
(defthm r-lub-r-lte-r-lub
 
240
  (implies (and (r-p r1)
 
241
                (r-p r2)
 
242
                (r-p r3)
 
243
                (r-p r4)
 
244
                (r-lte r1 r3)
 
245
                (r-lte r2 r4))
 
246
           (r-lte (r-lub r1 r2)
 
247
                  (r-lub r3 r4))))
 
248
 
 
249
 
 
250
(defthm r-lub-r-lte-rewrite-1
 
251
  (implies (and (r-p r)
 
252
                (r-p r1)
 
253
                (r-lte r1 r))
 
254
           (equal (r-lub r r1) r)))
 
255
 
 
256
(defthm r-lub-r-lte-rewrite-2
 
257
  (implies (and (r-p r)
 
258
                (r-p r1)
 
259
                (r-lte r1 r))
 
260
           (equal (r-lub r1 r) r)))
 
261
 
 
262
 
 
263
(defthm r-lte-r-make-s-make-cons
 
264
  (IMPLIES (AND (CONSP (CONS R1 R2))
 
265
              (INTEGERP N)
 
266
              (< 0 N)
 
267
              (R-LTE (R-MAKE (+ -1 N) (S-MAKE (LEN R1) 'X))
 
268
                     R2)
 
269
              (S-P R1)
 
270
              (R-P R2)
 
271
              (R-NMP R2 (+ -1 N) (LEN R1))
 
272
              (< 0 (LEN R1)))
 
273
         (R-LTE (R-MAKE N (S-MAKE (LEN R1) 'X))
 
274
                (CONS R1 R2))))
 
275
 
 
276
(defthm r-lte-r-make
 
277
  (implies (and (r-p r)
 
278
                (naturalp n)
 
279
                (naturalp m)
 
280
                (r-nmp r n m))
 
281
           (r-lte (r-make n (s-make m 'x)) r))
 
282
  )
 
283
 
 
284
(defthm r-lub-r-lte-r-lub-r-1
 
285
  (implies (and (r-p r)
 
286
                (r-p r3)
 
287
                (r-p r4)
 
288
                (r-lte r r3)
 
289
                (r-lte r r4))
 
290
           (r-lte r
 
291
                  (r-lub r3 r4)))
 
292
   :hints (("Goal" :use ((:instance r-lub-r-lte-r-lub (r1 r) (r2 r))))))
 
293
 
 
294
(defthm r-lub-r-lte-r-lub-r-2
 
295
  (implies (and (r-p r1)
 
296
                (r-p r2)
 
297
                (r-p r)
 
298
                (r-lte r1 r)
 
299
                (r-lte r2 r))
 
300
           (r-lte (r-lub r1 r2)
 
301
                  r))
 
302
  :hints (("Goal" :use ((:instance r-lub-r-lte-r-lub (r3 r) (r4 r))))) )
 
303
 
 
304
(defthm r-lte-both-implies-r-lte-r-lub
 
305
  (implies (and (r-p r)
 
306
                (r-p r1)
 
307
                (r-p r2)
 
308
                (r-lte r1 r)
 
309
                (r-lte r2 r)
 
310
                )
 
311
           (r-lte (r-lub r1 r2) r)))
 
312
(defthm not-r-lte-1-implies-not-r-lte-r-lub
 
313
  (implies 
 
314
   (and (r-p r)
 
315
        (r-p r1)
 
316
        (r-p r2)
 
317
        (naturalp n)
 
318
        (naturalp m)
 
319
        (r-nmp r1 n m)
 
320
        (r-nmp r2 n m)
 
321
        (r-nmp r  n m)
 
322
        (not (r-lte r1 r))
 
323
        )
 
324
   (not (r-lte (r-lub r1 r2) r)))
 
325
  :hints (("Goal" :do-not '(generalize fertilize) )) )
 
326
 
 
327
(defthm not-r-lte-2-implies-not-r-lte-r-lub
 
328
  (implies 
 
329
   (and (r-p r)
 
330
        (r-p r1)
 
331
        (r-p r2)
 
332
        (naturalp n)
 
333
        (naturalp m)
 
334
        (r-nmp r1 n m)
 
335
        (r-nmp r2 n m)
 
336
        (r-nmp r  n m)
 
337
        (not (r-lte r2 r))
 
338
        )
 
339
   (not (r-lte (r-lub r1 r2) r)))
 
340
  :hints (("Goal" 
 
341
           :use ((:instance not-r-lte-1-implies-not-r-lte-r-lub
 
342
                            (r1 r2) (r2 r1))
 
343
                 (:instance r-lub-commutes))
 
344
           )) )