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
|
; set-defuns.lisp -- definitions in the theory of sets
; Copyright (C) 1997 Computational Logic, Inc.
; This book is free software; you can redistribute it and/or modify
; it under the terms of the GNU General Public License as published by
; the Free Software Foundation; either version 2 of the License, or
; (at your option) any later version.
; This book is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
; GNU General Public License for more details.
; You should have received a copy of the GNU General Public License
; along with this book; if not, write to the Free Software
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
; Written by: Bill Bevier (bevier@cli.com)
; Computational Logic, Inc.
; 1717 West Sixth Street, Suite 290
; Austin, TX 78703-4776 U.S.A.
(in-package "ACL2")
;
; This theory includes functions which treat lists as sets.
; In the theory of lists and the theory of alists, we
; provide three versions of each function based on three different
; notions of equality: EQL, EQ and EQUAL. In this theory, however,
; we provide only the EQUAL version. The main reason for this is
; mundane: Many of the function names (e.g. UNION and INTERSECTION)
; are not defined in ACL2, but are blocked from our use because they're
; in the Common Lisp package.
; ------------------------------------------------------------
; Functions
; ------------------------------------------------------------
; Function Name In Result
; (supporting function) ACL2 Type
; ---------------------- ---- -----
;
; adjoin-equal N set
; intersection-equal N set
; set-difference-equal Y set
; union-equal Y set
;
; memberp-equal N boolean
; subsetp-equal Y boolean
; set-equal N boolean
; setp N boolean
(defun adjoin-equal (x l)
(declare (xargs :guard (true-listp l)))
(if (member-equal x l)
l
(cons x l)))
(defun memberp-equal (x l)
(DECLARE (XARGS :GUARD (TRUE-LISTP L)))
(consp (member-equal x l)))
(defun intersection-equal (x y)
(declare (xargs :guard (and (true-listp x) (true-listp y))))
(cond ((endp x) nil)
((member-equal (car x) y)
(cons (car x) (intersection-equal (cdr x) y)))
(t (intersection-equal (cdr x) y))))
(defun set-equal (a b)
(declare (xargs :guard (and (true-listp a)
(true-listp b))))
(and (subsetp-equal a b)
(subsetp-equal b a)))
(defun setp-equal (l)
(declare (xargs :verify-guards t))
(and (true-listp l)
(no-duplicatesp-equal l)))
|
