← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/1999/ivy/ivy-v2/ivy-sources/sk-step.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/ivy/ivy-v2/ivy-sources/sk-step.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
;; This book contains the definitions of the "step" functions
 
4
;; for Skolemization.  Instead of Skolemizing all existential
 
5
;; quantifiers in one pass, we repeatedly ("step-by-step")
 
6
;; Skolemize the leftmost existential until done.
 
7
;;
 
8
;; Function step-sk Skolemizes the leftmost existential quantifier.
 
9
;; To prove soundness of step-sk, we use a companion function
 
10
;; step-ex, which extends an interpretaion with a Skolem function.
 
11
;; The guts of step-ex are the mutually recursive pair build-sk/build-sk-d,
 
12
;; which have recursion similar to the evaluation function feval/feval-d.
 
13
;;
 
14
;; Also, we also prove some preservation-of-property lemmas for step-sk.
 
15
 
 
16
(include-book "stage")
 
17
(include-book "sk-misc-lemmas")
 
18
(local (include-book "../../../../../ordinals/e0-ordinal"))
 
19
 
 
20
;;---------------------------------------------------------------
 
21
;; (step-sk f vars fsym) tries to skolemize the left-most
 
22
;; existential quantifier.
 
23
 
 
24
(defun step-sk (f vars fsym)
 
25
  (declare (xargs :guard (and (wff f)
 
26
                              (nnfp f)
 
27
                              (var-list vars)
 
28
                              (function-symbol fsym))))
 
29
  (cond ((or (wfand f) (wfor f))
 
30
         (if (> (exists-count (a1 f)) 0)
 
31
             (list (car f) (step-sk (a1 f) vars fsym) (a2 f))
 
32
             (list (car f) (a1 f) (step-sk (a2 f) vars fsym))))
 
33
                   
 
34
        ((wfall f) (list 'all (a1 f) (step-sk (a2 f)
 
35
                                              (append vars (list (a1 f)))
 
36
                                              fsym)))
 
37
        ((wfexists f)
 
38
         (subst-free (a2 f) (a1 f) (cons fsym vars)))
 
39
        (t f)))
 
40
 
 
41
;;---------------
 
42
 
 
43
(defthm step-sk-preserves-wff
 
44
  (implies (and (wff f)
 
45
                (var-list vars)
 
46
                (function-symbol fsym))
 
47
           (wff (step-sk f vars fsym))))
 
48
 
 
49
(defthm step-sk-preserves-nnfp
 
50
  (implies (nnfp f)
 
51
           (nnfp (step-sk f vars fsym))))
 
52
 
 
53
;;---------------
 
54
;; (step-sk-arity f n):  Get the arity for the Skolem function for
 
55
;; the leftmost existential quantifier.  Parameter n counts
 
56
;; universals along the way.  Return nil if there are no existentials.
 
57
 
 
58
(defun step-sk-arity (f n)
 
59
  (declare (xargs :guard (and (wff f)
 
60
                              (nnfp f)
 
61
                              (natp n))))
 
62
  (cond ((or (wfand f) (wfor f))
 
63
         (if (> (exists-count (a1 f)) 0)
 
64
             (step-sk-arity (a1 f) n)
 
65
             (step-sk-arity (a2 f) n)))
 
66
        ((wfall f) (step-sk-arity (a2 f) (+ 1 n)))
 
67
        ((wfexists f) n)
 
68
        (t nil)))
 
69
 
 
70
;;---------------------------------------------------------------
 
71
;; (val-or-0 p x dom i) is the first member of dom that makes p
 
72
;; true when substituted for x.  If there is none, 0 is returned.
 
73
 
 
74
(defun validator (p x dom i)  ;; return a domain element or nil
 
75
  (declare (xargs :guard (and (wff p)
 
76
                              (variable-term x)
 
77
                              (domain-term-list (fringe dom)))))
 
78
  (if (atom dom)
 
79
      (if (feval (subst-free p x dom) i)
 
80
          dom
 
81
        nil)
 
82
    (if (validator p x (car dom) i)
 
83
        (validator p x (car dom) i)
 
84
      (validator p x (cdr dom) i))))
 
85
 
 
86
(defmacro val-or-0 (p x dom i)
 
87
  (list 'if (list 'validator p x dom i)
 
88
        (list 'validator p x dom i)
 
89
        '0))
 
90
 
 
91
;;--------------------
 
92
;; (build-sk f vals i) builds a Skolem function (that is, an alist of
 
93
;; tuple-value pairs) for the left-most existential quantifier.
 
94
 
 
95
(mutual-recursion
 
96
 
 
97
 (defun build-sk (f vals i)
 
98
   (declare (xargs :measure (cons (cons (wff-count f) 2) 0)
 
99
                   :guard (and (wff f)
 
100
                               (nnfp f)
 
101
                               (domain-term-list vals))
 
102
                   :verify-guards nil))
 
103
   (cond
 
104
    ((or (wfand f) (wfor f))
 
105
     (if (> (exists-count (a1 f)) 0)
 
106
         (build-sk (a1 f) vals i)
 
107
       (build-sk (a2 f) vals i)))
 
108
    ((wfexists f) (list (cons vals (val-or-0 (a2 f) (a1 f) (domain i) i))))
 
109
    ((wfall f) (build-sk-d f vals (domain i) i)) ;; recurse-on-domain
 
110
    (t nil)))
 
111
 
 
112
 (defun build-sk-d (f vals dom i)
 
113
   (declare (xargs :measure (cons (cons (wff-count f) 1) (acl2-count dom))
 
114
                   :guard (and (wff f)
 
115
                               (nnfp f)
 
116
                               (domain-term-list vals)
 
117
                               (domain-term-list (fringe dom))
 
118
                               (subsetp-equal (fringe dom)
 
119
                                              (fringe (domain i))))))
 
120
   (cond ((wfall f)
 
121
          (if (atom dom)
 
122
              (build-sk (subst-free (a2 f) (a1 f) dom)
 
123
                        (append vals (list dom)) i)
 
124
              (append (build-sk-d f vals (car dom) i)
 
125
                      (build-sk-d f vals (cdr dom) i))))
 
126
         (t nil)))
 
127
 
 
128
 )  ;; end of mutual recursion
 
129
 
 
130
;;------------------
 
131
;; build-sk-i is an induction scheme corresponding to build-sk.
 
132
 
 
133
(defun build-sk-i (flg f vals dom i)
 
134
  (declare (xargs :measure (cons (cons (wff-count f)
 
135
                                       (if flg 2 1))
 
136
                                 (acl2-count dom))
 
137
                  :guard (and (wff f)
 
138
                              (domain-term-list vals)
 
139
                              (implies (not flg)
 
140
                                       (domain-term-list (fringe dom))))
 
141
                  :verify-guards nil))
 
142
  (if flg
 
143
      (cond ((or (wfand f) (wfor f))
 
144
             (if (> (exists-count (a1 f)) 0)
 
145
                 (build-sk-i t (a1 f) vals 'junk i)
 
146
                 (build-sk-i t (a2 f) vals 'junk i)))
 
147
            ((wfexists f) nil)
 
148
            ((wfall f) (build-sk-i nil f vals (domain i) I))
 
149
            (t nil))
 
150
    (cond ((wfall f) (if (atom dom)
 
151
                         (build-sk-i t
 
152
                                    (subst-free (a2 f) (a1 f) dom)
 
153
                                    (append vals (list dom))
 
154
                                    'junk
 
155
                                    i)
 
156
                       (append (build-sk-i nil f vals (car dom) i)
 
157
                               (build-sk-i nil f vals (cdr dom) i))))
 
158
          (t nil))))
 
159
 
 
160
;;---------------------
 
161
;; Verify the guard for build-sk and build-sk-i.
 
162
 
 
163
(defthm build-sk-true-listp-flg
 
164
  (if flg
 
165
      (true-listp (build-sk f vals i))
 
166
      (true-listp (build-sk-d f vals dom i)))
 
167
  :hints (("Goal"
 
168
           :induct (build-sk-i flg f vals dom i)))
 
169
  :rule-classes nil)
 
170
 
 
171
(defthm build-sk-d-true-listp
 
172
  (true-listp (build-sk-d f vals dom i))
 
173
  :hints (("Goal"
 
174
           :by (:instance build-sk-true-listp-flg (flg nil)))))
 
175
 
 
176
(defthm build-sk-i-true-listp
 
177
  (true-listp (build-sk-i flg f vals dom i)))
 
178
 
 
179
(verify-guards build-sk)
 
180
 
 
181
(verify-guards build-sk-i)
 
182
 
 
183
;;---------------------
 
184
;; After we build the skolem function, we have to be able to insert it
 
185
;; into an interpretation.  It is useful to have two versions, step-ex
 
186
;; and step-ex-d, corresponding to the two mutually recursive build
 
187
;; functions.
 
188
 
 
189
(defun insert-func-into-interp (fsym-arity func i)
 
190
  (declare (xargs :guard (alistp func)))
 
191
  (if (consp fsym-arity)
 
192
      (cons (domain i)
 
193
            (cons (relations i)
 
194
                  (cons (cons fsym-arity func) (functions i))))
 
195
    i))
 
196
 
 
197
(defthm build-sk-alistp-flg  ;; for step-sk guard
 
198
  (if flg
 
199
      (alistp (build-sk f vals i))
 
200
      (alistp (build-sk-d f vals dom i)))
 
201
  :hints (("Goal"
 
202
           :induct (build-sk-i flg f vals dom i)))
 
203
  :rule-classes nil)
 
204
 
 
205
(defthm build-sk-alistp  ;; for step-sk guard
 
206
  (alistp (build-sk f vals i))
 
207
  :hints (("Goal"
 
208
           :by (:instance build-sk-alistp-flg (flg t)))))
 
209
 
 
210
(defthm build-sk-d-alistp  ;; for step-sk guard
 
211
  (alistp (build-sk-d f vals dom i))
 
212
  :hints (("Goal"
 
213
           :by (:instance build-sk-alistp-flg (flg nil)))))
 
214
 
 
215
(defun step-ex (f fsym vals i)
 
216
  (declare (xargs :guard (and (wff f) (nnfp f) (function-symbol fsym)
 
217
                              (domain-term-list vals))))
 
218
  (insert-func-into-interp (cons fsym (step-sk-arity f (len vals)))
 
219
                           (build-sk f vals i) i))
 
220
 
 
221
(defun step-ex-d (f fsym vals dom i)
 
222
  (declare (xargs :guard (and (wff f) (nnfp f) (function-symbol fsym)
 
223
                              (domain-term-list vals)
 
224
                              (domain-term-list (fringe dom))
 
225
                              (subsetp-equal (fringe dom)
 
226
                                             (fringe (domain i))))))
 
227
  (insert-func-into-interp (cons fsym (step-sk-arity f (len vals)))
 
228
                           (build-sk-d f vals dom i) i))
 
229
 
 
230
;;---------
 
231
;; The following induction scheme is useful when proving things
 
232
;; involving both step-sk and step-sk-sym.  The recursion on f
 
233
;; is similar to both; the vars argument is like step-sk, and the n
 
234
;; argument is like step-sk-sym.
 
235
 
 
236
(defun step-sk-sym-i2 (f vars n)
 
237
  (declare (xargs :guard (and (wff f)
 
238
                              (nnfp f)
 
239
                              (var-list vars)
 
240
                              (natp n))))
 
241
  (cond ((or (wfand f) (wfor f))
 
242
         (if (> (exists-count (a1 f)) 0)
 
243
             (step-sk-sym-i2 (a1 f) vars n)
 
244
             (step-sk-sym-i2 (a2 f) vars n)))
 
245
        ((wfall f) (step-sk-sym-i2 (a2 f)
 
246
                                   (append vars (list (a1 f)))
 
247
                                   (+ 1 n)))
 
248
        (t nil)))
 
249
 
 
250
(defthm step-sk-without-exists
 
251
  (implies (equal (exists-count f) 0)
 
252
           (equal (step-sk f vars fsym) f)))
 
253
 
 
254
;;---------------------------------------------------------
 
255
;; step-sk-preserves-closedness
 
256
 
 
257
(defthm not-var-occurrence-append-list
 
258
  (implies (and (not (var-occurrence-term-list x vars))
 
259
                (variable-term y)
 
260
                (not (equal x y)))
 
261
           (not (var-occurrence-term-list x (append vars (list y))))))
 
262
 
 
263
(defthm not-var-occurrence-subst-term-list
 
264
  (implies (and (variable-term y)
 
265
                (var-list vars)
 
266
                (not (var-occurrence-term-list x l))
 
267
                (not (var-occurrence-term-list x vars)))
 
268
           (not (var-occurrence-term-list
 
269
                 x
 
270
                 (subst-term-list l y (cons fsym vars))))))
 
271
 
 
272
(defthm not-free-occurrence-subst-free
 
273
  (implies (and (variable-term y)
 
274
                (var-list vars)
 
275
                (not (free-occurrence x f))
 
276
                (not (var-occurrence-term-list x vars)))
 
277
           (not (free-occurrence x (subst-free f y (cons fsym vars)))))
 
278
  :hints (("Goal"
 
279
           :induct (free-occurrence x f))))
 
280
 
 
281
(defthm not-var-ococurrence-list-tm
 
282
  (implies (and (var-list vars)
 
283
                (not (var-occurrence-term-list x vars)))
 
284
           (not (var-occurrence-term-list x (list (cons fsym vars))))))
 
285
 
 
286
(defthm not-free-occurrence-list-tm
 
287
  (implies (and (var-list vars)
 
288
                (not (var-occurrence-term-list x vars)))
 
289
           (not (free-occurrence x (subst-free f x (cons fsym vars)))))
 
290
  :hints (("Goal"
 
291
           :induct (free-occurrence x (subst-free f x (cons fsym vars))))))
 
292
 
 
293
(defthm step-sk-preserves-closedness-h1
 
294
  (implies (and (not (free-occurrence x f))
 
295
                (var-list vars)
 
296
                (not (var-occurrence-term-list x vars)))
 
297
           (not (free-occurrence x (step-sk f vars fsym)))))
 
298
 
 
299
(defthm step-sk-preserves-closedness-h2
 
300
  (implies (not (free-occurrence x f))
 
301
           (not (free-occurrence x (step-sk f nil fsym)))))
 
302
 
 
303
(defthm step-sk-preserves-closedness-h3
 
304
  (implies (not (member-equal x (free-vars f)))
 
305
           (not (member-equal x (free-vars (step-sk f nil fsym)))))
 
306
  :hints (("Goal"
 
307
           :use ((:instance free-free)
 
308
                 (:instance free-free (f (step-sk f nil fsym)))))))
 
309
 
 
310
(defthm step-sk-preserves-closedness
 
311
  (implies (not (free-vars f))
 
312
           (not (free-vars (step-sk f nil fsym))))
 
313
  :hints (("Goal"
 
314
           :do-not-induct t
 
315
           :use ((:instance consp-has-member-equal
 
316
                            (x (free-vars (step-sk f nil fsym))))))))
 
317