← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/std/alists/fal-all-boundp.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/std/alists/fal-all-boundp.lisp
 
1
; Standard Association Lists Library
 
2
; Copyright (C) 2013-2014 Centaur Technology
 
3
;
 
4
; Contact:
 
5
;   Centaur Technology Formal Verification Group
 
6
;   7600-C N. Capital of Texas Highway, Suite 300, Austin, TX 78731, USA.
 
7
;   http://www.centtech.com/
 
8
;
 
9
; License: (An MIT/X11-style license)
 
10
;
 
11
;   Permission is hereby granted, free of charge, to any person obtaining a
 
12
;   copy of this software and associated documentation files (the "Software"),
 
13
;   to deal in the Software without restriction, including without limitation
 
14
;   the rights to use, copy, modify, merge, publish, distribute, sublicense,
 
15
;   and/or sell copies of the Software, and to permit persons to whom the
 
16
;   Software is furnished to do so, subject to the following conditions:
 
17
;
 
18
;   The above copyright notice and this permission notice shall be included in
 
19
;   all copies or substantial portions of the Software.
 
20
;
 
21
;   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 
22
;   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 
23
;   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 
24
;   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 
25
;   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 
26
;   FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
 
27
;   DEALINGS IN THE SOFTWARE.
 
28
;
 
29
; Original authors: Jared Davis <jared@centtech.com>
 
30
;                   Sol Swords <sswords@centtech.com>
 
31
 
 
32
(in-package "ACL2")
 
33
(include-book "std/util/define" :dir :system)
 
34
(include-book "alist-equiv")
 
35
(include-book "worth-hashing")
 
36
(local (include-book "std/lists/sets" :dir :system))
 
37
(local (include-book "hons-assoc-equal"))
 
38
 
 
39
(define fal-all-boundp-fast (keys alist)
 
40
  :parents (fal-all-boundp)
 
41
  (if (atom keys)
 
42
      t
 
43
    (and (hons-get (car keys) alist)
 
44
         (fal-all-boundp-fast (cdr keys) alist))))
 
45
 
 
46
(define fal-all-boundp-slow (keys alist)
 
47
  :parents (fal-all-boundp)
 
48
  (if (atom keys)
 
49
      t
 
50
    (and (hons-assoc-equal (car keys) alist)
 
51
         (fal-all-boundp-slow (cdr keys) alist))))
 
52
 
 
53
(define fal-all-boundp (keys alist)
 
54
  :parents (std/alists)
 
55
  :short "@(call fal-all-boundp) determines if every key in @('keys') is bound
 
56
in the alist @('alist')."
 
57
  :long "<p>The @('alist') need not be fast.  If it is not fast, it may be made
 
58
temporarily fast, depending on its length.</p>"
 
59
  :returns bool
 
60
  (declare (xargs :guard t :verify-guards nil))
 
61
  (mbe :logic
 
62
       (if (atom keys)
 
63
           t
 
64
         (and (hons-assoc-equal (car keys) alist)
 
65
              (fal-all-boundp (cdr keys) alist)))
 
66
       :exec
 
67
       (if (atom keys)
 
68
           t
 
69
         (if (and (worth-hashing keys)
 
70
                  (worth-hashing alist))
 
71
             (with-fast-alist alist
 
72
               (fal-all-boundp-fast keys alist))
 
73
           (fal-all-boundp-slow keys alist))))
 
74
  ///
 
75
  (defthm fal-all-boundp-fast-removal
 
76
    (equal (fal-all-boundp-fast keys alist)
 
77
           (fal-all-boundp keys alist))
 
78
    :hints(("Goal" :in-theory (enable fal-all-boundp-fast))))
 
79
 
 
80
  (defthm fal-all-boundp-slow-removal
 
81
    (equal (fal-all-boundp-slow keys alist)
 
82
           (fal-all-boundp keys alist))
 
83
    :hints(("Goal" :in-theory (enable fal-all-boundp-slow))))
 
84
 
 
85
  (verify-guards fal-all-boundp)
 
86
 
 
87
  (defthm fal-all-boundp-when-atom
 
88
    (implies (atom keys)
 
89
             (equal (fal-all-boundp keys alist)
 
90
                    t)))
 
91
 
 
92
  (defthm fal-all-boundp-of-cons
 
93
    (equal (fal-all-boundp (cons a keys) alist)
 
94
           (and (hons-get a alist)
 
95
                (fal-all-boundp keys alist))))
 
96
 
 
97
  (encapsulate
 
98
    ()
 
99
    (local (defthm l0
 
100
             (implies (and (fal-all-boundp y alist)
 
101
                           (member-equal a y))
 
102
                      (hons-assoc-equal a alist))))
 
103
 
 
104
    (local (defthm l1
 
105
             (implies (and (fal-all-boundp y alist)
 
106
                           (subsetp-equal x y))
 
107
                      (fal-all-boundp x alist))
 
108
             :hints(("Goal" :induct (len x)))))
 
109
 
 
110
    (defcong set-equiv equal (fal-all-boundp x alist) 1
 
111
      :hints(("Goal" :in-theory (e/d (set-equiv)
 
112
                                     (l1))
 
113
              :use ((:instance l1 (x x) (y x-equiv))
 
114
                    (:instance l1 (x x-equiv) (y x)))))))
 
115
 
 
116
  (defcong alist-equiv equal (fal-all-boundp x alist) 2)
 
117
 
 
118
  (defthm fal-all-boundp-of-list-fix
 
119
    ;; BOZO silly to prove this?  Just a consequence of the set-equiv
 
120
    (equal (fal-all-boundp (list-fix x) alist)
 
121
           (fal-all-boundp x alist)))
 
122
 
 
123
  (defthm fal-all-boundp-of-rev
 
124
    ;; BOZO silly to prove this?  Just a consequence of the set-equiv
 
125
    (equal (fal-all-boundp (rev x) alist)
 
126
           (fal-all-boundp x alist)))
 
127
 
 
128
  (defthm fal-all-boundp-of-append
 
129
    (equal (fal-all-boundp (append x y) alist)
 
130
           (and (fal-all-boundp x alist)
 
131
                (fal-all-boundp y alist))))
 
132
 
 
133
  (defthm fal-all-boundp-of-revappend
 
134
    ;; BOZO silly to prove this?  Trivial via the set-equiv and append rules
 
135
    (equal (fal-all-boundp (revappend x y) alist)
 
136
           (and (fal-all-boundp x alist)
 
137
                (fal-all-boundp y alist)))))
 
 
b'\\ No newline at end of file'