blob: 0eb39f859ea441662b2880b9f2a50952496130bb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
|
(in-package "ACL2")
;; This book contains the syntactic correctness theorem for
;; (rename-all f): (setp (quantified-vars (rename-all f))).
(include-book "rename")
;; I think this book could use some cleaning up. All we need is
;; the last theorem, and I think it can be proved with a lot less work.
;------------------------------------------------
(defthm rename-bound-introduces-new-variable
(implies (and (bound-occurrence x f)
(variable-term y))
(member-equal y (quantified-vars (rename-bound f x y)))))
(defthm rename-bound-introduces-new-variable-2
(implies (and (member-equal x (quantified-vars f))
(variable-term y))
(member-equal y (quantified-vars (rename-bound f x y))))
:hints (("Goal"
:use ((:instance quantified-is-bound)))))
(defthm rename-bound-doesnt-change-other-variables
(implies (and (member-equal v (quantified-vars f))
(variable-term y)
(not (equal v x)))
(member-equal v (quantified-vars (rename-bound f x y)))))
(defthm rename-bunch-introduces-new-variables
(implies (and (member-equal x (quantified-vars g))
(var-list new)
(not (member-equal x old)))
(member-equal x (quantified-vars (rename-bunch g old new))))
:hints (("Goal"
:do-not generalize)))
(defthm bound-is-quantified ;; disabled below
(implies (bound-occurrence x f)
(member-equal x (quantified-vars f)))
:hints (("Goal"
:use ((:instance quantified-iff-bound)))))
(defthm not-bound-is-not-quantified ;; disabled below
(implies (not (bound-occurrence x f))
(not (member-equal x (quantified-vars f))))
:hints (("Goal"
:use ((:instance quantified-iff-bound)))))
;;----------------------------
;; Bring in subbag, because there can be duplicates in the list of
;; original quantified variables. Also, we will use permutation.
(include-book "permutations")
(defthm subbag-member-remove1-equal-append-lemma
(implies (and (not (member-equal x f3))
(subbag (remove1-equal x f5) q))
(subbag (remove1-equal x (append f3 f5)) (append f3 q))))
(defthm subbag-remove1-equal-qvars-lemma-1
(implies (variable-term y)
(subbag (remove1-equal x (quantified-vars f))
(quantified-vars (rename-bound f x y)))))
(in-theory (disable bound-is-quantified not-bound-is-not-quantified))
(defthm subbag-remove1-equal-qvars-lemma-2
(implies (and (subbag vars (remove1-equal x (quantified-vars f)))
(variable-term y))
(subbag vars (quantified-vars (rename-bound f x y))))
:hints (("Goal"
:do-not-induct t
:use ((:instance subbag-trans
(a vars)
(b (remove1-equal x (quantified-vars f)))
(c (quantified-vars (rename-bound f x y))))))))
(defthm disjoint-cons
(implies (not (disjoint a b))
(not (disjoint a (cons x b)))))
(defthm new-vars-really-get-there-lemma
(implies (and (subbag old (quantified-vars f))
(equal (len old) (len new))
(disjoint new old)
(var-list new))
(subsetp-equal new (quantified-vars (rename-bunch f old new))))
:hints (("Goal"
:induct (rename-bunch f old new)
:expand ((subbag (cons old1 old2) (quantified-vars f)))
)))
(defthm all-safe-vars-are-disjoint-from-quantified-vars
(implies (all-safe vars f)
(disjoint vars (quantified-vars f))))
(defthm safe-list-vars-are-disjoint-from-quantified-vars
(disjoint (safe-list f)
(quantified-vars f))
:hints (("Goal"
:in-theory (disable safe-list))))
(defthm len-qvars-equal-len-safe-vars
(equal (len (safe-list f))
(len (quantified-vars f))))
(defthm new-vars-really-get-there
(subsetp-equal (safe-list f)
(quantified-vars (rename-all f)))
:hints (("Goal"
:in-theory (disable safe-list))))
; Now, use the fact that the new variables are a setp with the
; same length as the set of variables after the renaming to
; show that the permutation relation holds. (Actually, it should
; be equal, but I couldn't see how to prove that.)
(defthm setp-subset-equal-length-perm
(implies (and (setp new)
(subsetp-equal new q)
(equal (len new) (len q)))
(perm new q))
:hints (("Goal"
:induct (perm new q)))
:rule-classes nil)
;-----------------------
; When I wrote len-append-left and len-append right positively,
; I got a segmentation fault, I guess because of a rewrite loop.
(defthm len-append-left ;; disabled below
(implies (not (equal (len (append b a)) (len (append b c))))
(not (equal (len a) (len c)))))
(defun double-list-induct (a b)
(declare (xargs :guard t))
(if (or (atom a) (atom b))
nil
(double-list-induct (cdr a) (cdr b))))
(defthm len-append-right ;; disabled below
(implies (not (equal (len (append a b)) (len (append c b))))
(not (equal (len a) (len c))))
:hints (("Goal"
:induct (double-list-induct a c))))
(defthm rename-bound-preserves-len-of-qvars
(implies (variable-term y)
(equal (len (quantified-vars (rename-bound f x y)))
(len (quantified-vars f)))))
(in-theory (disable len-append-left len-append-right))
(defthm rename-bunch-preserves-len-of-qvars
(implies (var-list new)
(equal (len (quantified-vars (rename-bunch f old new)))
(len (quantified-vars f)))))
;-----------------------
(defthm safe-list-is-perm-of-qvars-rename-all
(perm (safe-list f)
(quantified-vars (rename-all f)))
:hints (("Goal"
:do-not-induct t
:use ((:instance setp-subset-equal-length-perm
(new (safe-list f))
(q (quantified-vars (rename-all f))))))))
;; The main event.
(defthm rename-all-setp-qvars
(setp (quantified-vars (rename-all f)))
:hints (("Goal"
:in-theory (disable rename-all safe-list perm-implies-iff-setp-1)
:use ((:instance perm-setp-setp
(a (safe-list f))
(b (quantified-vars (rename-all f))))))))
|
