← 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/rename.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/rename.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
;; The rename books are arranged like this:
 
4
;;
 
5
;;          rename-top
 
6
;;             /  \
 
7
;; rename-unique  rename-sound
 
8
;;             \  /
 
9
;;            rename
 
10
;;
 
11
;; This book (rename) has the main definitions and some
 
12
;; preservation-of-property theorems.  The top definition
 
13
;; is (rename-all f), which renames all bound variables
 
14
;; (left-to-right, in separate passes) to unique new
 
15
;; variable names.
 
16
 
 
17
(include-book "wfftype")
 
18
 
 
19
;;===================== step-wise rename
 
20
 
 
21
;; Function rename-bound (f old new) renames the first bound occurrence
 
22
;; of old to new.  Safeness of "new" is not checked.
 
23
 
 
24
(defun rename-bound (f old new)
 
25
  (declare (xargs :guard (and (wff f)
 
26
                              (variable-term old)
 
27
                              (variable-term new))))
 
28
  (cond ((wfnot f) (list 'not (rename-bound (a1 f) old new)))
 
29
        ((wfbinary f) (if (bound-occurrence old (a1 f))
 
30
                          (list (car f)
 
31
                                (rename-bound (a1 f) old new)
 
32
                                (a2 f))
 
33
                          (list (car f)
 
34
                                (a1 f)
 
35
                                (rename-bound (a2 f) old new))))
 
36
        ((wfquant f) (if (equal (a1 f) old)
 
37
                         (list (car f)
 
38
                               new
 
39
                               (subst-free (a2 f) (a1 f) new))
 
40
                         (list (car f)
 
41
                               (a1 f)
 
42
                               (rename-bound (a2 f) old new))))
 
43
        (t f)))
 
44
 
 
45
(defthm rename-bound-wff
 
46
  (implies (and (wff f)
 
47
                (variable-term new))
 
48
           (wff (rename-bound f old new))))
 
49
 
 
50
(defthm rename-bound-preserves-car
 
51
  (equal (car (rename-bound f old new)) (car f)))
 
52
 
 
53
(defthm rename-bound-preserves-nnfp
 
54
  (implies (nnfp f)
 
55
           (nnfp (rename-bound f x y))))
 
56
 
 
57
;;===============================================
 
58
;; Function rename-bunch (f oldvars newvars) renames the members of oldvars
 
59
;; to the corresponding members of newvars.
 
60
 
 
61
(defun rename-bunch (f oldvars newvars)
 
62
  (declare (xargs :guard (and (wff f) (var-list oldvars) (var-list newvars)
 
63
                              (equal (len oldvars) (len newvars)))))
 
64
  (if (or (atom oldvars) (atom newvars))
 
65
      f
 
66
      (rename-bunch (rename-bound f (car oldvars) (car newvars))
 
67
                    (cdr oldvars) (cdr newvars))))
 
68
 
 
69
(defthm rename-bunch-wff
 
70
  (implies (and (wff f)
 
71
                (var-list newvars))
 
72
           (wff (rename-bunch f oldvars newvars))))
 
73
 
 
74
(defthm rename-bunch-preserves-nnfp
 
75
  (implies (nnfp f)
 
76
           (nnfp (rename-bunch f old new))))
 
77
 
 
78
;; Function (all-safe vars f) is true if no member of vars has a
 
79
;; bound or free occurrence in formula f.
 
80
 
 
81
(defun all-safe (vars f)
 
82
  (declare (xargs :guard (and (wff f) (var-list vars))))
 
83
  (cond ((atom vars) t)
 
84
        ((bound-occurrence (car vars) f) nil)
 
85
        ((free-occurrence (car vars) f) nil)
 
86
        (t (all-safe (cdr vars) f))))
 
87
 
 
88
;;------------------------------------------------
 
89
;; Now what should the newvars be?
 
90
;;
 
91
;; Get the gensym book, define a function to get a list of new
 
92
;; symbols, and prove some properties.
 
93
 
 
94
(include-book "gensym-e")
 
95
 
 
96
(defun gen-symbols (n sym lst)
 
97
  (declare (xargs :guard (and (natp n)
 
98
                              (symbolp sym)
 
99
                              (symbol-listp lst))))
 
100
  (if (zp n)
 
101
      nil
 
102
    (let ((newsym (gen-symbol sym lst)))
 
103
      (cons newsym (gen-symbols (1- n) sym (cons newsym lst))))))
 
104
 
 
105
(defthm gen-symbols-ok
 
106
  (implies (symbolp sym)
 
107
           (disjoint (gen-symbols n sym lst) lst)))
 
108
 
 
109
(defthm gen-symbols-len
 
110
  (implies (natp n)
 
111
           (equal (len (gen-symbols n sym lst)) n)))
 
112
 
 
113
(defthm member-member-not-disjoint
 
114
  (implies (and (member-equal x a)
 
115
                (member-equal x b))
 
116
           (not (disjoint a b)))
 
117
  :rule-classes nil)
 
118
 
 
119
(defthm gen-symbols-member
 
120
  (implies (symbolp sym)
 
121
           (not (member-equal a (gen-symbols n sym (cons a lst)))))
 
122
  :hints (("Goal"
 
123
           :use ((:instance member-member-not-disjoint
 
124
                            (x a)
 
125
                            (a (gen-symbols n sym (cons a lst)))
 
126
                            (b (cons a lst)))))))
 
127
 
 
128
(defthm gen-symbols-setp
 
129
  (implies (symbolp sym)
 
130
           (setp (gen-symbols n sym lst))))
 
131
 
 
132
;;------------------------------------------------
 
133
 
 
134
(defthm var-list-symbol-listp
 
135
  (implies (var-list lst)
 
136
           (symbol-listp lst)))
 
137
 
 
138
(defun safe-list (f)
 
139
  (declare (xargs :guard (wff f)))
 
140
  (gen-symbols (len (quantified-vars f))
 
141
               'v
 
142
               (append (quantified-vars f) (free-vars f))))
 
143
 
 
144
(defthm free-free-append
 
145
  (implies (free-occurrence x f)
 
146
           (member-equal x (append (quantified-vars f)
 
147
                                   (free-vars f))))
 
148
  :hints (("Goal"
 
149
         :use ((:instance free-free)))))
 
150
 
 
151
(defthm bound-bound-append
 
152
  (implies (bound-occurrence x f)
 
153
           (member-equal x (append (quantified-vars f)
 
154
                                   (free-vars f))))
 
155
  :hints (("Goal"
 
156
         :use ((:instance quantified-iff-bound)))))
 
157
 
 
158
(defthm disjoint-all-safe
 
159
  (implies (disjoint a (append (quantified-vars f) (free-vars f)))
 
160
           (all-safe a f)))
 
161
 
 
162
(defthm safe-list-all-safe
 
163
  (all-safe (safe-list f) f))
 
164
 
 
165
(defmacro var-set (vars)
 
166
  (list 'and (list 'var-list vars) (list 'setp vars)))
 
167
 
 
168
(defthm gen-symbols-var-list
 
169
  (var-list (gen-symbols n sym lst)))
 
170
 
 
171
(defthm safe-list-varset
 
172
  (var-set (safe-list f)))
 
173
 
 
174
;;---------------------------------
 
175
;; Function (rename-all f) renames all bound variables.
 
176
 
 
177
(defthm var-list-append
 
178
  (implies (and (var-list qvs0)
 
179
                (var-list qvs))
 
180
           (var-list (append qvs0 qvs))))
 
181
 
 
182
(defun rename-all (f)
 
183
  (declare (xargs :guard (wff f)))
 
184
  (rename-bunch f (quantified-vars f) (safe-list f)))
 
185
 
 
186
(defthm rename-all-wff
 
187
  (implies (wff f)
 
188
           (wff (rename-all f))))
 
189
 
 
190
(defthm rename-all-preserves-nnfp
 
191
  (implies (nnfp f)
 
192
           (nnfp (rename-all f))))
 
193
 
 
194
;;------------------------------------------------
 
195
;; Prove that the rename functions preserve free-vars
 
196
 
 
197
(defthm rename-bound-preserves-free-vars
 
198
  (implies (and (variable-term y)
 
199
                (not (bound-occurrence y f))
 
200
                (not (free-occurrence y f)))
 
201
           (equal (free-vars (rename-bound f x y))
 
202
                  (free-vars f))))
 
203
 
 
204
(defthm rename-bound-doesnt-introduce-free-vars
 
205
  (implies (not (free-occurrence z f))
 
206
           (not (free-occurrence z (rename-bound f x y)))))
 
207
 
 
208
(defthm rename-bound-still-safe
 
209
  (implies (and (all-safe new2 f)
 
210
                (not (member-equal new1 new2))
 
211
                (not (bound-occurrence new1 f))
 
212
                (not (free-occurrence new1 f)))
 
213
           (all-safe new2 (rename-bound f old1 new1))))
 
214
 
 
215
(defthm rename-bunch-preserves-free-vars
 
216
  (implies (and (all-safe new f)
 
217
                (var-set new))
 
218
           (equal (free-vars (rename-bunch f old new))
 
219
                  (free-vars f)))
 
220
  :hints (("Goal"
 
221
           :induct (rename-bunch f old new))))
 
222
 
 
223
(defthm rename-all-preserves-free-vars
 
224
  (equal (free-vars (rename-all f))
 
225
         (free-vars f)))