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
|
; Intersection$ Lemmas
; Copyright (C) 2013 Kookamara LLC
;
; Contact:
;
; Kookamara LLC
; 11410 Windermere Meadows
; Austin, TX 78759, USA
; http://www.kookamara.com/
;
; License: (An MIT/X11-style license)
;
; Permission is hereby granted, free of charge, to any person obtaining a
; copy of this software and associated documentation files (the "Software"),
; to deal in the Software without restriction, including without limitation
; the rights to use, copy, modify, merge, publish, distribute, sublicense,
; and/or sell copies of the Software, and to permit persons to whom the
; Software is furnished to do so, subject to the following conditions:
;
; The above copyright notice and this permission notice shall be included in
; all copies or substantial portions of the Software.
;
; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
; IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
; FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
; AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
; LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
; FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
; DEALINGS IN THE SOFTWARE.
;
; Original author: Jared Davis <jared@kookamara.com>
(in-package "ACL2")
(include-book "list-defuns")
(include-book "xdoc/top" :dir :system)
(local (include-book "sets"))
(local (in-theory (enable intersection$ intersectp)))
(defsection std/lists/intersection$
:parents (std/lists intersection$)
:short "Lemmas about @(see intersection$) available in the @(see std/lists)
library."
"<p>We'll take @(see intersectp) as the desired normal form for asking
whether intersections are empty.</p>"
(defthm intersection$-under-iff
(iff (intersection$ x y)
(intersectp x y)))
(defthm consp-of-intersection$
(equal (consp (intersection$ x y))
(intersectp x y)))
"<p>Basic atom/cons rules.</p>"
(defthm intersection$-when-atom-left
(implies (atom x)
(equal (intersection$ x y)
nil)))
(defthm intersection$-of-cons-left
(equal (intersection$ (cons a x) y)
(if (member a y)
(cons a (intersection$ x y))
(intersection$ x y))))
(defthm intersection$-when-atom-right
(implies (atom y)
(equal (intersection$ x y)
nil)))
"<p>We don't have a very nice rule for @(see cons) on the right if we're
trying to maintain @('equal'), because we don't know where in @('x') the
element occurs. However, if we're only maintaining @(see set-equiv), then we
can just put the element on the front and we get a perfectly nice rule:</p>"
(defthm intersection$-of-cons-right-under-set-equiv
(set-equiv (intersection$ x (cons a y))
(if (member a x)
(cons a (intersection$ x y))
(intersection$ x y)))
:hints(("Goal" :in-theory (enable set-equiv))))
"<h5>Basic set reasoning</h5>"
(defthm member-of-intersection$
(iff (member a (intersection$ x y))
(and (member a x)
(member a y))))
(defthm subsetp-equal-of-intersection$-1
(subsetp-equal (intersection$ x y) x))
(defthm subsetp-equal-of-intersection$-2
(subsetp-equal (intersection$ x y) y))
(defthm subsetp-intersection-equal
(iff (subsetp a (intersection-equal b c))
(and (subsetp a b)
(subsetp a c))))
(defthm intersection$-commutes-under-set-equiv
(set-equiv (intersection$ x y)
(intersection$ y x))
:hints(("Goal" :in-theory (enable set-equiv))))
;; These are redundant with sets.lisp
(defcong set-equiv equal (intersection-equal x y) 2)
(defcong set-equiv set-equiv (intersection-equal x y) 1)
"<h5>Length bound</h5>
<p>Here is a nice bounding theorem. Note that there is no analogous rule for
@('-right'), because, e.g., X could have multiple copies of some member in Y,
and if so we end up reproducing them. Consider for instance:</p>
@({ (intersection$ '(a a a) '(a)) ==> '(a a a) })"
(defthm len-of-intersection$-upper-bound
(<= (len (intersection$ x y))
(len x))
:rule-classes ((:rewrite) (:linear))))
|
