← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/coi/alists/equiv.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/coi/alists/equiv.lisp
1
 
#|-*-Lisp-*-=================================================================|#
2
 
#|                                                                           |#
3
 
#| coi: Computational Object Inference                                       |#
4
 
#|                                                                           |#
5
 
#|===========================================================================|#
 
1
; Computational Object Inference
 
2
; Copyright (C) 2005-2014 Kookamara LLC
 
3
;
 
4
; Contact:
 
5
;
 
6
;   Kookamara LLC
 
7
;   11410 Windermere Meadows
 
8
;   Austin, TX 78759, USA
 
9
;   http://www.kookamara.com/
 
10
;
 
11
; License: (An MIT/X11-style license)
 
12
;
 
13
;   Permission is hereby granted, free of charge, to any person obtaining a
 
14
;   copy of this software and associated documentation files (the "Software"),
 
15
;   to deal in the Software without restriction, including without limitation
 
16
;   the rights to use, copy, modify, merge, publish, distribute, sublicense,
 
17
;   and/or sell copies of the Software, and to permit persons to whom the
 
18
;   Software is furnished to do so, subject to the following conditions:
 
19
;
 
20
;   The above copyright notice and this permission notice shall be included in
 
21
;   all copies or substantial portions of the Software.
 
22
;
 
23
;   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 
24
;   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 
25
;   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 
26
;   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 
27
;   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 
28
;   FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
 
29
;   DEALINGS IN THE SOFTWARE.
 
30
 
6
31
;; equiv.lisp
7
32
;; Primitive alist fixing and equivalence relations.
8
33
 
33
58
;          (assoc x y)))
34
59
 
35
60
;; Interpreting Objects as Conses (consfix)
36
 
;; 
 
61
;;
37
62
;; We can think of a mapping between all ACL2 objects and conses, so that any
38
63
;; atom is mapped to (nil . nil) and any cons is mapped to itself.  The
39
64
;; function consfix applies this mapping for us, i.e., it interprets any ACL2
47
72
      x
48
73
    (cons nil nil)))
49
74
 
50
 
(local 
51
 
 (encapsulate 
 
75
(local
 
76
 (encapsulate
52
77
  ()
53
78
  ;; Here we check to make sure that our type prescription rule is as strong as
54
79
  ;; we think it is.  Don't remove this event even though it has no effect on
55
80
  ;; the logical world.
56
81
  (local (defthm test-type-prescription-of-consfix
57
82
           (consp (consfix x))
58
 
           :hints(("Goal" 
 
83
           :hints(("Goal"
59
84
                   :in-theory (union-theories '((:type-prescription consfix))
60
85
                                              (theory 'minimal-theory))))))))
61
86
 
67
92
 
68
93
(defthm consfix-when-consp
69
94
  (implies (consp x)
70
 
           (equal (consfix x) 
 
95
           (equal (consfix x)
71
96
                  x))
72
97
  :hints(("Goal" :in-theory (enable consfix))))
73
98
 
76
101
         (consp x))
77
102
  :hints(("Goal" :in-theory (enable consfix))))
78
103
 
79
 
(defthm consfix-of-cons 
 
104
(defthm consfix-of-cons
80
105
  (equal (consfix (cons a b))
81
106
         (cons a b)))
82
107
 
93
118
;; (defthm consfix-of-cdr
94
119
;;   (equal (cdr (consfix a))
95
120
;;          (cdr a)))
96
 
         
97
 
         
 
121
 
 
122
 
98
123
 
99
124
 
100
125
 
114
139
  :hints(("Goal" :in-theory (enable cons-equiv))))
115
140
 
116
141
(defthm consfix-in-cons-equiv
117
 
  (cons-equiv (consfix x) 
 
142
  (cons-equiv (consfix x)
118
143
              x)
119
144
  :hints(("Goal" :in-theory (enable cons-equiv))))
120
145
 
215
240
 
216
241
(defthm alistfix-type-non-consp
217
242
  (implies (not (consp x))
218
 
           (equal (alistfix x) 
 
243
           (equal (alistfix x)
219
244
                  nil))
220
245
  :rule-classes :type-prescription
221
246
  :hints(("Goal" :in-theory (enable alistfix))))
231
256
 
232
257
(defthm alistfix-when-non-consp
233
258
  (implies (not (consp alist))
234
 
           (equal (alistfix alist) 
 
259
           (equal (alistfix alist)
235
260
                  nil)))
236
261
 
237
262
(defthm alistfix-when-alist
238
263
  (implies (alistp x)
239
 
           (equal (alistfix x) 
 
264
           (equal (alistfix x)
240
265
                  x))
241
266
  :hints(("Goal" :in-theory (enable alistfix))))
242
267
 
319
344
  :hints(("Goal" :in-theory (enable alist-equiv))))
320
345
 
321
346
(defrefinement list::equiv alist-equiv
322
 
  :hints(("Goal" 
 
347
  :hints(("Goal"
323
348
          :in-theory (enable alist-equiv)
324
349
          :induct (list::len-len-induction ACL2::x ACL2::y))))
325
350
 
327
352
  :hints(("Goal" :in-theory (enable alist-equiv))))
328
353
 
329
354
(defcong alist-equiv equal (len x) 1
330
 
  :hints(("Goal" 
 
355
  :hints(("Goal"
331
356
          :in-theory (enable alist-equiv)
332
357
          :induct (list::len-len-induction x x-equiv))))
333
358
 
352
377
;; should work.
353
378
 
354
379
(defcong alist-equiv cons-equiv (car x) 1
355
 
  :hints(("Goal" 
 
380
  :hints(("Goal"
356
381
          :in-theory (e/d (alist-equiv alistfix)
357
382
                          (alistfix-type-consp)))))
358
383
 
359
384
(defthm alistfix-in-alist-equiv
360
 
  (alist-equiv (alistfix a) 
 
385
  (alist-equiv (alistfix a)
361
386
               a)
362
387
  :hints(("Goal" :in-theory (enable alist-equiv))))
363
388
 
374
399
  :hints(("Goal" :in-theory (enable alist-equiv))))
375
400
 
376
401
(theory-invariant (incompatible (:rewrite equal-of-alist-fixes)
377
 
                                (:definition alist-equiv)))
 
402
                                (:definition alist-equiv)))
 
 
b'\\ No newline at end of file'