← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2006/swords-cook/lcsoundness/LambdaCalcBasis.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/2006/swords-cook/lcsoundness/LambdaCalcBasis.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
(set-ignore-ok :warn)
 
4
 
 
5
(include-book "data-structures/list-theory" :dir :system)
 
6
(include-book "defsum")
 
7
(local (include-book "defsum-thms"))
 
8
 
 
9
;; stype ::= bool | type -> type
 
10
(defsum stype
 
11
  (bool)
 
12
  (fun (stype-p domain) (stype-p range)))
 
13
 
 
14
;; A varname is a paired symbol and natural, so that we have a simple way of
 
15
;; generating new unique ones.
 
16
(defsum varname
 
17
  (VN (symbolp name) (natp num)))
 
18
 
 
19
;; type of a list of varnames
 
20
(deflist varname-listp (l)
 
21
  (declare (xargs :guard t))
 
22
  varname-p)
 
23
 
 
24
(defthm acl2-numberp-varname-num
 
25
  (implies (varname-p x)
 
26
           (acl2-numberp (vn-num x)))
 
27
  :hints (("Goal" :use varname-possibilities
 
28
           :in-theory (disable varname-possibilities))))
 
29
 
 
30
 
 
31
;; expression ::= TRUE | FALSE |
 
32
;;                LAMBDA varname : type . expression |
 
33
;;                APP expression expression |
 
34
;;                VAR varname |
 
35
;;                IFELSE expression expression expression
 
36
(defsum expression
 
37
    (TRUE)
 
38
    (FALSE)
 
39
    (LAM (varname-p var) (stype-p type) (expression-p body))
 
40
    (APP (expression-p fun) (expression-p arg))
 
41
    (VAR (varname-p name))
 
42
    (IFELSE (expression-p cond) 
 
43
            (expression-p case1) 
 
44
            (expression-p case2)))
 
45
 
 
46
 
 
47
;; Typing derivations, checked by valid-typing.
 
48
;; The type of the argument in an application needs to be specified for T-APP;
 
49
;; everything else is syntax-driven.
 
50
(defsum type-deriv
 
51
  (T-TRUE)
 
52
  (T-FALSE)
 
53
  (T-VAR)
 
54
  (T-ABS (type-deriv-p body))
 
55
  (T-APP (stype-p argtype) 
 
56
         (type-deriv-p fun) 
 
57
         (type-deriv-p arg))
 
58
  (T-IF (type-deriv-p cond)
 
59
        (type-deriv-p case1)
 
60
        (type-deriv-p case2)))
 
61
 
 
62
;; Evaluation derivations, checked by valid-evaluation.
 
63
(defsum eval-deriv
 
64
  (E-AppAbs)
 
65
  (E-APP1 (eval-deriv-p fun))
 
66
  (E-APP2 (eval-deriv-p arg))
 
67
  (E-IFCOND (eval-deriv-p cond))
 
68
  (E-IFTRUE)
 
69
  (E-IFFALSE))
 
70
 
 
71
 
 
72
 
 
73
;; An environment is an alist associating variable names with types.
 
74
(defun environment-p (env)
 
75
  (declare (xargs :guard t))
 
76
  (if (and (consp env) (consp (car env)))
 
77
      (and (varname-p (caar env))
 
78
           (stype-p (cdar env))
 
79
           (environment-p (cdr env)))
 
80
    (null env)))
 
81
 
 
82
;; Various lemmas about environments.
 
83
(defthm environment-assoc
 
84
        (implies (environment-p env)
 
85
                 (alistp env)))
 
86
 
 
87
(defthm alistp-assoc-cons
 
88
  (implies (and (alistp a)
 
89
                (assoc-equal k a))
 
90
           (consp (assoc-equal k a))))
 
91
 
 
92
 
 
93
(defthm environment-p-assoc-type
 
94
  (implies (and (environment-p env)
 
95
                (assoc-equal key env))
 
96
           (stype-p (cdr (assoc-equal key env)))))
 
97
 
 
98
 
 
99
 
 
100
;; These functions and lemmas mainly form the basis for the weakening
 
101
;; and alpha-substitution lemmas.  We're concerned with environments
 
102
;; that get modified up to a certain suffix, beyond which we don't
 
103
;; care.
 
104
 
 
105
;; Is suf a suffix of env?
 
106
(defun is-suffix (suf env)
 
107
  (if (equal suf env)
 
108
      t
 
109
    (if (atom env)
 
110
        nil
 
111
      (is-suffix suf (cdr env)))))
 
112
 
 
113
 
 
114
(defthm is-suffix-len
 
115
  (implies (< (len env) (len suffix))
 
116
           (not (is-suffix suffix env)))
 
117
  :rule-classes nil)
 
118
 
 
119
(defthm is-suffix-not-equal-cons
 
120
  (not (is-suffix (cons a x) x))
 
121
  :hints (("Goal" :use (:instance is-suffix-len
 
122
                                 (env x)
 
123
                                 (suffix (cons a x))))))
 
124
 
 
125
 
 
126
;; Substitute all bindings of v1 for v2 up to suffix.
 
127
(defun env-subst-up-to (v1 v2 suff env)
 
128
  (declare (xargs :guard (alistp env)))
 
129
  (if (equal suff env)
 
130
      env
 
131
    (if (atom env)
 
132
        env
 
133
      (cons 
 
134
       (if (equal (caar env) v1)
 
135
           (cons v2 (cdar env))
 
136
         (car env))
 
137
       (env-subst-up-to v1 v2 suff (cdr env))))))
 
138
 
 
139
 
 
140
(defthm env-subst-up-to-assoc-other
 
141
  (implies (and (not (equal v v1))
 
142
                (not (equal v v2)))
 
143
           (equal (assoc-equal v (env-subst-up-to v1 v2 suff env))
 
144
                  (assoc-equal v env))))
 
145
 
 
146
;; Insert a binding of k to v just before suffix.
 
147
(defun insert-assoc (k v suffix alist)
 
148
  (declare (xargs :guard (alistp alist)))
 
149
  (if (equal suffix alist)
 
150
      (cons (cons k v) alist)
 
151
    (if (atom alist)
 
152
        alist
 
153
      (cons (car alist)
 
154
            (insert-assoc k v suffix (cdr alist))))))
 
155
 
 
156
(defthm assoc-insert-assoc
 
157
  (implies (not (equal key k))
 
158
           (equal (assoc-equal key (insert-assoc k v suffix alist))
 
159
                  (assoc-equal key alist))))
 
160
 
 
161
(defthm cons-insert-assoc
 
162
  (implies (is-suffix suffix alist)
 
163
           (equal (cons a (insert-assoc k v suffix alist))
 
164
                  (insert-assoc k v suffix (cons a alist)))))
 
165
 
 
166
;; Is the key bound before the suffix?
 
167
(defun is-bound-before-suffix (key suff alist)
 
168
  (declare (xargs :guard (alistp alist)))
 
169
  (if (equal suff alist)
 
170
      nil
 
171
    (if (atom alist)
 
172
        nil
 
173
      (or (equal (caar alist) key)
 
174
          (is-bound-before-suffix key suff (cdr alist))))))
 
175
 
 
176
 
 
177
 
 
178
(defthm is-bound-before-suffix-env-subst-up-to
 
179
  (implies (and (is-bound-before-suffix v suff env)
 
180
                (not (is-bound-before-suffix v2 suff env)))
 
181
           (equal (cdr (assoc-equal v2 (env-subst-up-to v v2 suff env)))
 
182
                  (cdr (assoc-equal v env)))))
 
183
            
 
184
 
 
185
(defthm is-bound-before-suffix-env-subst-assoc1
 
186
  (implies (and (is-bound-before-suffix v suff env)
 
187
                (not (is-bound-before-suffix v2 suff env)))
 
188
           (assoc-equal v2 (env-subst-up-to v v2 suff env))))
 
189
 
 
190
 
 
191
 
 
192
 
 
193
;; This sums up all the requirements for alpha substitution to work
 
194
;; with a given environment.
 
195
(defun alpha-subst-env-okp (v1 v2 suffix env)
 
196
  (and (is-bound-before-suffix v1 suffix env)
 
197
       (not (is-bound-before-suffix v2 suffix env))
 
198
       (is-suffix suffix env)))
 
199
 
 
200
(defthm alpha-subst-env-okp-base
 
201
  (implies (not (equal v1 v2))
 
202
           (alpha-subst-env-okp v1 v2 env (cons (cons v1 typ) env))))
 
203
 
 
204
(defthm alpha-subst-env-okp-cons
 
205
  (implies (and (not (equal v v2))
 
206
                (alpha-subst-env-okp v1 v2 env1 env2))
 
207
           (alpha-subst-env-okp v1 v2 env1 (cons (cons v typ) env2))))
 
208
 
 
209
(defthm alpha-subst-env-okp-implies-assoc-env-subst-up-to
 
210
  (implies (alpha-subst-env-okp v1 v2 suffix env)
 
211
           (assoc-equal v2 (env-subst-up-to v1 v2 suffix env))))
 
212
 
 
213
(defthm alpha-subst-env-okp-cdr-assocs-env-subst
 
214
  (implies (alpha-subst-env-okp v1 v2 suffix env)
 
215
           (equal (cdr (assoc-equal v2 (env-subst-up-to v1 v2 suffix env)))
 
216
                  (cdr (assoc-equal v1 env)))))
 
217
 
 
218
(defthm alpha-subst-env-okp-suffix-not-cons
 
219
  (not (alpha-subst-env-okp v1 v2 (cons a env) env)))
 
220
 
 
221
 
 
222
(in-theory (disable alpha-subst-env-okp))  
 
223
 
 
224
 
 
225
 
 
226
 
 
227
 
 
228
 
 
229
 
 
230
;; This describes the requirements for the permutation lemma;
 
231
;; env-same-bindings checks whether each variable bound in env1 has
 
232
;; the same binding in env1 and env2.
 
233
(defun env-same-bindings1 (tail full env2)
 
234
  (declare (xargs :guard (and (alistp tail)
 
235
                              (alistp full)
 
236
                              (alistp env2))))
 
237
  (if (atom tail)
 
238
      t
 
239
    (and (equal (assoc-equal (caar tail) full)
 
240
                (assoc-equal (caar tail) env2))
 
241
         (env-same-bindings1 (cdr tail) full env2))))
 
242
 
 
243
(defthm env-same-bindings1-assoc-equal
 
244
  (implies (and (env-same-bindings1 tail full env2)
 
245
                (assoc-equal x tail))
 
246
           (equal (assoc-equal x full)
 
247
                  (assoc-equal x env2))))
 
248
           
 
249
(defthm env-same-bindings1-cons2
 
250
  (implies (env-same-bindings1 tail full env2)
 
251
           (env-same-bindings1 tail (cons x full) (cons x env2))))
 
252
 
 
253
 
 
254
(defthm env-same-bindings1-refl
 
255
  (env-same-bindings1 a b b))
 
256
 
 
257
(defthm env-same-bindings1-cons-twice
 
258
  (implies (not (equal (car a) (car b)))
 
259
           (env-same-bindings1 
 
260
            tail (list* a b env) (list* b a env))))
 
261
 
 
262
(defthm env-same-bindings1-cons-redundant
 
263
  (implies (equal t1 t2)
 
264
           (env-same-bindings1 tail (list* (cons v t1)
 
265
                                           (cons v t3)
 
266
                                           env)
 
267
                               (list* (cons v t2)
 
268
                                      env))))
 
269
           
 
270
(defun env-same-bindings (env1 env2)
 
271
  (declare (xargs :guard (and (alistp env1) (alistp env2))))
 
272
  (env-same-bindings1 env1 env1 env2))
 
273
 
 
274
(defthm env-same-bindings-assoc-equal
 
275
  (implies (and (env-same-bindings env1 env2)
 
276
                (assoc-equal x env1))
 
277
           (equal (assoc-equal x env2)
 
278
                  (assoc-equal x env1))))
 
279
 
 
280
(defthm env-same-bindings-cons
 
281
  (implies (env-same-bindings env1 env2)
 
282
           (env-same-bindings (cons x env1) (cons x env2))))
 
283
 
 
284
(defthm env-same-bindings-cons-twice
 
285
  (implies (not (equal (car a) (car b)))
 
286
           (env-same-bindings (list* a b env) (list* b a env))))
 
287
 
 
288
(defthm env-same-bindings-cons-redundant
 
289
  (implies (equal t1 t2)
 
290
           (env-same-bindings (list* (cons v t1)
 
291
                                     (cons v t3)
 
292
                                     env)
 
293
                              (list* (cons v t2)
 
294
                                     env))))
 
295
                              
 
296
 
 
297
 
 
298
(defthm same-bindings1-insert-assoc
 
299
  (implies (is-suffix suffix env)
 
300
           (env-same-bindings1 tail (cons (cons k v) env)
 
301
                               (cons (cons k v)
 
302
                                     (insert-assoc k v2 suffix env))))
 
303
  :hints (("Goal" :induct (env-same-bindings1 tail env env)
 
304
           :in-theory (disable cons-insert-assoc))))
 
305
 
 
306
(defthm same-bindings1-insert-assoc1
 
307
  (implies (is-suffix suffix env)
 
308
           (env-same-bindings1 tail (cons (cons k v) env)
 
309
                               (insert-assoc k v2 suffix 
 
310
                                             (cons (cons k v) env))))
 
311
  :hints (("Goal" :use same-bindings1-insert-assoc
 
312
           :in-theory (disable same-bindings1-insert-assoc))))
 
313
 
 
314
(defthm same-bindings-insert-assoc
 
315
  (implies (is-suffix suffix env)
 
316
           (env-same-bindings (cons (cons k v) env)
 
317
                              (insert-assoc k v2 suffix
 
318
                                            (cons (cons k v) env)))))
 
319
 
 
320
(in-theory (disable env-same-bindings))
 
321
 
 
322
 
 
323
 
 
324
 
 
325
(defun forcelist-fn (hyps)
 
326
  (declare (xargs :mode :program))
 
327
  (if (atom hyps)
 
328
      nil
 
329
    (cons `(force ,(car hyps))
 
330
          (forcelist-fn (cdr hyps)))))
 
331
 
 
332
(defmacro force-and (&rest hyps)
 
333
  (cons 'and (forcelist-fn hyps)))