← 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/pull.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/pull.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
;; The pull books are arranged like this:
 
4
;;
 
5
;;        pull-top
 
6
;;          /  \
 
7
;; pull-pulls  pull-sound
 
8
;;          \  /
 
9
;;          pull
 
10
;;
 
11
;; This book (pull) has the main definitions and some
 
12
;; preservation-of-property theorems.  The top definition
 
13
;; is (pull-quants f), which pulls quantifiers to the
 
14
;; top of a formula.
 
15
 
 
16
(include-book "wfftype")
 
17
(include-book "permutations")
 
18
        
 
19
;;--------------------------------------
 
20
;; Function pull (f) moves quantifiers toward the root of a formula
 
21
;; as much as possible, using rules like
 
22
;; (or p (all x q)) <=> (all x (or p q)) if x is not free in p.
 
23
;; Bound variables are NOT renamed.  If all bound variables are
 
24
;; unique, the formula is closed nnf, then all quantifiers should
 
25
;; come to the top.  (That property proved elsewhere.)  Here,
 
26
;; we define the functions and prove soundness.
 
27
;;
 
28
;; Pull-top-left pulls quantifiers up from the left side, and
 
29
;; pull-top-right from the right side.
 
30
;; 
 
31
;; The first functions I wrote were a little simpler than these.
 
32
;; Originally, when pull-top right got to the base case, it called
 
33
;; pull-top-left.  Now, they are independent (and the same except for
 
34
;; left/right):  we first pull-top-left, then call down-right,
 
35
;; which goes back down to the 'and or 'or and calls pull-top-right.
 
36
;; 
 
37
;;     or                      q1                   q1
 
38
;;    / \           ->         q2        ->         q2
 
39
;;   q1 q3    pull-top-left    or    down-right     q3
 
40
;;   q2 q4                    / \  (pull-top-right) q4
 
41
;;   A   B                   A  q3                  or
 
42
;;                              q4                 / \
 
43
;;                               B                A   B
 
44
;; 
 
45
;; I changed to the current version, because I had trouble getting
 
46
;; a soundness proof for the original.
 
47
 
 
48
(defun pull-top-right (op f g)
 
49
  (declare (xargs :guard (and (or (equal op 'and) (equal op 'or))
 
50
                              (wff f) (nnfp f)
 
51
                              (wff g) (nnfp g))))
 
52
  (if (and (or (equal op 'and) (equal op 'or))
 
53
           (wfquant g)
 
54
           (not (free-occurrence (a1 g) f)))
 
55
      (list (car g) (a1 g) (pull-top-right op f (a2 g)))
 
56
      (list op f g)))
 
57
 
 
58
(defun pull-top-left (op f g)                    
 
59
  (declare (xargs :guard (and (or (equal op 'and) (equal op 'or))
 
60
                              (wff f) (nnfp f)
 
61
                              (wff g) (nnfp f))))
 
62
  (if (and (or (equal op 'and) (equal op 'or))
 
63
           (wfquant f)
 
64
           (not (free-occurrence (a1 f) g)))
 
65
      (list (car f) (a1 f) (pull-top-left op (a2 f) g))
 
66
      (list op f g)))
 
67
 
 
68
(defun down-right (f)
 
69
  (declare (xargs :guard (and (wff f) (nnfp f))))
 
70
  (cond ((wfquant f) (list (car f) (a1 f) (down-right (a2 f))))
 
71
        ((or (wfand f)
 
72
             (wfor f)) (pull-top-right (car f) (a1 f) (a2 f)))
 
73
        (t f)))
 
74
 
 
75
;; Beware!  Something about pull, I don't know what, causes
 
76
;; rewrite explosions.  Even to get guards verified, I had to
 
77
;; disable pull.  In other proofs below, down-right is disabled,
 
78
;; which helps somewhat.
 
79
 
 
80
(defun pull (f)
 
81
  (declare (xargs :guard (and (wff f) (nnfp f))
 
82
                  :verify-guards nil))
 
83
  (cond ((or (wfand f)
 
84
             (wfor f)) (down-right (pull-top-left (car f)
 
85
                                                  (pull (a1 f))
 
86
                                                  (pull (a2 f)))))
 
87
        ((wfquant f) (list (car f) (a1 f) (pull (a2 f))))
 
88
        (t f)))
 
89
 
 
90
;;---------------
 
91
;; Prove the the pull functions preserve wff and nnfp, and finally
 
92
;; verify guards for pull.
 
93
 
 
94
(defthm pull-top-right-wff
 
95
  (implies (and (wff f)
 
96
                (wff g)
 
97
                (or (equal op 'and) (equal op 'or)
 
98
                    (equal op 'imp) (equal op 'iff)))
 
99
           (wff (pull-top-right op f g))))
 
100
                                                 
 
101
(defthm pull-top-right-nnfp
 
102
  (implies (and (nnfp f)
 
103
                (nnfp g)
 
104
                (or (equal op 'and) (equal op 'or)))
 
105
           (nnfp (pull-top-right op f g)))
 
106
  :hints (("Goal"
 
107
           :induct (pull-top-right op f g))))
 
108
                                                 
 
109
(defthm pull-top-left-wff
 
110
  (implies (and (wff f)
 
111
                (wff g)
 
112
                (or (equal op 'and) (equal op 'or)
 
113
                    (equal op 'imp) (equal op 'iff)))
 
114
           (wff (pull-top-left op f g))))
 
115
                                                 
 
116
(defthm pull-top-left-nnfp
 
117
  (implies (and (nnfp f)
 
118
                (nnfp g)
 
119
                (or (equal op 'and) (equal op 'or)))
 
120
           (nnfp (pull-top-left op f g)))
 
121
  :hints (("Goal"
 
122
           :induct (pull-top-left op f g))))
 
123
                                                 
 
124
(defthm down-right-wff
 
125
  (implies (wff f)
 
126
           (wff (down-right f))))
 
127
 
 
128
(defthm down-right-nnfp
 
129
  (implies (nnfp f)
 
130
           (nnfp (down-right f)))
 
131
  :hints (("Goal"
 
132
           :induct (down-right f))))
 
133
 
 
134
(defthm pull-wff
 
135
  (implies (wff f)
 
136
           (wff (pull f)))
 
137
  :hints (("Goal"
 
138
           :in-theory (disable down-right))))
 
139
 
 
140
(defthm pull-nnfp
 
141
  (implies (nnfp f)
 
142
           (nnfp (pull f)))
 
143
  :hints (("Goal"
 
144
           :in-theory (disable down-right))))
 
145
 
 
146
(verify-guards pull
 
147
  :hints (("Goal"
 
148
           :in-theory (disable pull))))
 
149
 
 
150
;;----------------------------------------
 
151
;; Here is a wrapper for pull.  This checks the (unnecessary I think) setp
 
152
;; condition in the soundness theorem.
 
153
 
 
154
(defun pull-quants (f)
 
155
  (declare (xargs :guard (and (wff f) (nnfp f))))
 
156
  (if (setp (quantified-vars f))
 
157
      (pull f)
 
158
    f))
 
159
 
 
160
(defthm pull-quants-wff
 
161
  (implies (wff f)
 
162
           (wff (pull-quants f)))
 
163
  :hints (("Goal"
 
164
           :in-theory (disable pull))))
 
165
 
 
166
(defthm pull-quants-nnfp
 
167
  (implies (nnfp f)
 
168
           (nnfp (pull-quants f)))
 
169
  :hints (("Goal"
 
170
           :in-theory (disable pull))))
 
171
 
 
172
;;---------------
 
173
;; Show that each pull functions preserves the set of free variables.
 
174
 
 
175
(defthm ptr-preserves-free-vars
 
176
  (implies (or (equal op 'and) (equal op 'or))
 
177
           (equal (free-vars (pull-top-right op f g))
 
178
                  (union-equal (free-vars f) (free-vars g))))
 
179
  :hints (("Goal"
 
180
           :induct (pull-top-right op f g))))
 
181
 
 
182
(defthm ptl-preserves-free-vars
 
183
  (implies (or (equal op 'and) (equal op 'or))
 
184
           (equal (free-vars (pull-top-left op f g))
 
185
                  (union-equal (free-vars f) (free-vars g))))
 
186
  :hints (("Goal"
 
187
           :induct (pull-top-left op f g))))
 
188
 
 
189
(defthm down-right-preserves-free-vars
 
190
  (equal (free-vars (down-right f))
 
191
         (free-vars f))
 
192
  :hints (("Goal"
 
193
           :induct (down-right f))))
 
194
 
 
195
(defthm pull-preserves-free-vars
 
196
  (equal (free-vars (pull f))
 
197
         (free-vars f))
 
198
  :hints (("Goal"
 
199
           :induct (pull f))))
 
200
 
 
201
(defthm pull-quants-preserves-free-vars
 
202
  (equal (free-vars (pull-quants f))
 
203
         (free-vars f))
 
204
  :hints (("Goal"
 
205
           :do-not-induct t
 
206
           :in-theory (disable pull))))
 
207
 
 
208
;;------------------------------------
 
209
;; The various operations preserve the set of quantified variables.
 
210
;; Note equality for pull-top-right, permutation for the rest.
 
211
;; (If the original formula is closed nnf with unique quantified
 
212
;; variables, all quantifiers come to the top, then does equality hold.
 
213
;; If I had proved this, some later things would have been simpler.)
 
214
 
 
215
(defthm ptl-preserves-qvars
 
216
  (implies (and (or (equal op 'and) (equal op 'or)))
 
217
           (equal (quantified-vars (pull-top-left op f g))
 
218
                  (append (quantified-vars f)
 
219
                          (quantified-vars g)))))
 
220
 
 
221
(defthm ptr-unique-qvars-2
 
222
  (implies (or (equal op 'and) (equal op 'or))
 
223
           (perm (quantified-vars (pull-top-right op f g))
 
224
                 (append (quantified-vars f)
 
225
                         (quantified-vars g)))))
 
226
 
 
227
(defthm down-right-unique-vars-2
 
228
  (perm (quantified-vars (down-right f))
 
229
        (quantified-vars f)))
 
230
 
 
231
(defthm pull-unique-vars-2
 
232
  (perm (quantified-vars (pull f))
 
233
        (quantified-vars f))
 
234
  :hints (("Goal"
 
235
           :in-theory (disable down-right set-equal))))
 
236
 
 
237
;;---------------------------
 
238
;; The pull operations preserve exists-count.
 
239
 
 
240
(defthm ptl-preserves-exists-count
 
241
  (implies (or (equal op 'and) (equal op 'or))
 
242
           (equal (exists-count (pull-top-left op f g))
 
243
                  (+ (exists-count f) (exists-count g))))
 
244
  :hints (("Goal"
 
245
           :induct (pull-top-left op f g))))
 
246
 
 
247
(defthm ptr-preserves-exists-count
 
248
  (implies (or (equal op 'and) (equal op 'or))
 
249
           (equal (exists-count (pull-top-right op f g))
 
250
                  (+ (exists-count f) (exists-count g))))
 
251
  :hints (("Goal"
 
252
           :induct (pull-top-right op f g))))
 
253
 
 
254
(defthm down-right-preserves-exists-count
 
255
  (equal (exists-count (down-right f))
 
256
         (exists-count f))
 
257
  :hints (("Goal"
 
258
           :induct (down-right f))))
 
259
 
 
260
(defthm pull-preserves-exists-count
 
261
  (equal (exists-count (pull f))
 
262
         (exists-count f))
 
263
  :hints (("Goal"
 
264
           :in-theory (disable pull-top-left pull-top-right down-right))))
 
265
 
 
266
(defthm pull-quants-preserves-exists-count
 
267
  (equal (exists-count (pull-quants f))
 
268
         (exists-count f))
 
269
  :hints (("Goal"
 
270
           :in-theory (disable pull-top-left pull-top-right down-right))))
 
271
 
 
272
;;------------
 
273
 
 
274
(defthm pull-quants-setp
 
275
  (implies (setp (quantified-vars f))
 
276
           (setp (quantified-vars (pull-quants f))))
 
277
  :hints (("Goal"
 
278
           :in-theory (disable pull))))