#|
Fully Ordered Finite Sets, Version 0.91
Copyright (C) 2003-2006 by Jared Davis
This program 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 program 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 Lic-
ense along with this program; if not, write to the Free Soft-
ware Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
02111-1307, USA.
sets.lisp
This is the top level file, which you should include to use the
ordered set theory library.
|#
(in-package "SETS")
(set-verify-guards-eagerness 2)
; We need some program-mode definitions which are used in order to
; automate the pick-a-point strategies.
(include-book "computed-hints")
; The definitions in this file are redundant from the local include
; books. This approach has several advantages.
;
; - it gives a better event order than simply including the books
; one by one
;
; - this file is also faster to include than all of the local books
; below, and allows the "ugliness" of auxilliary lemmas to be
; hidden away
;
; - it makes clear that these theorems are public, and entirely
; prevents the use of "internal" lemmas and theorems.
(local (include-book "primitives"))
(local (include-book "membership"))
(local (include-book "fast"))
(local (include-book "outer"))
(local (include-book "sort"))
; We begin with the definitions of the set theory functions and a
; few trivial type prescriptions.
(defund << (a b)
(declare (xargs :guard t))
(and (lexorder a b)
(not (equal a b)))))
(defund setp (X)
(declare (xargs :guard t))
(if (atom X)
(null X)
(or (null (cdr X))
(and (consp (cdr X))
(<< (car X) (cadr X))
(setp (cdr X))))))
(defthm setp-type
(or (equal (setp X) t)
(equal (setp X) nil))
:rule-classes :type-prescription)
(defund empty (X)
(declare (xargs :guard (setp X)))
(mbe :logic (or (null X)
(not (setp X)))
:exec (null X)))
(defthm empty-type
(or (equal (empty X) t)
(equal (empty X) nil))
:rule-classes :type-prescription)
(defund sfix (X)
(declare (xargs :guard (setp X)))
(mbe :logic (if (empty X) nil X)
:exec X))
(defund head (X)
(declare (xargs :guard (and (setp X)
(not (empty X)))))
(mbe :logic (car (sfix X))
:exec (car X)))
(defund tail (X)
(declare (xargs :guard (and (setp X)
(not (empty X)))))
(mbe :logic (cdr (sfix X))
:exec (cdr X)))
(defund insert (a X)
(declare (xargs :guard (setp X)))
(cond ((empty X) (list a))
((equal (head X) a) X)
((<< a (head X)) (cons a X))
(t (cons (head X) (insert a (tail X))))))
(defun in (a X)
(declare (xargs :guard (setp X)))
(and (not (empty X))
(or (equal a (head X))
(in a (tail X)))))
(defthm in-type
(or (equal (in a X) t)
(equal (in a X) nil))
:rule-classes :type-prescription)
(defund fast-subset (X Y)
(declare (xargs :guard (and (setp X) (setp Y))))
(cond ((empty X) t)
((empty Y) nil)
((<< (head X) (head Y)) nil)
((equal (head X) (head Y)) (fast-subset (tail X) (tail Y)))
(t (fast-subset X (tail Y)))))
(defun subset (X Y)
(declare (xargs :guard (and (setp X) (setp Y))))
(mbe :logic (if (empty X)
t
(and (in (head X) Y)
(subset (tail X) Y)))
:exec (fast-subset X Y)))
(defthm subset-type
(or (equal (subset X Y) t)
(equal (subset X Y) nil))
:rule-classes :type-prescription)
(defund fast-measure (X Y)
(+ (acl2-count X) (acl2-count Y)))
(defun fast-union (x y acc)
(declare (xargs :measure (fast-measure X Y)
:guard (and (setp x)
(setp y)
(true-listp acc))))
(cond
((empty x) (revappend acc y))
((empty y) (revappend acc x))
((equal (head x) (head y))
(fast-union (tail x) (tail y) (cons (head x) acc)))
((<< (head x) (head y))
(fast-union (tail x) y (cons (head x) acc)))
(t
(fast-union x (tail y) (cons (head y) acc)))))
(defun fast-intersect (X Y acc)
(declare (xargs :measure (fast-measure X Y)
:guard (and (setp X) (setp Y) (true-listp acc))))
(cond ((empty X) (reverse acc))
((empty Y) (reverse acc))
((equal (head X) (head Y))
(fast-intersect (tail X)
(tail Y)
(cons (head X) acc)))
((<< (head X) (head Y))
(fast-intersect (tail X) Y acc))
(t (fast-intersect X (tail Y) acc))))
(defun fast-difference (X Y acc)
(declare (xargs :measure (fast-measure X Y)
:guard (and (setp X) (setp Y) (true-listp acc))))
(cond ((empty X) (reverse acc))
((empty Y) (revappend acc X))
((equal (head X) (head Y))
(fast-difference (tail X) (tail Y) acc))
((<< (head X) (head Y))
(fast-difference (tail X) Y (cons (head X) acc)))
(t (fast-difference X (tail Y) acc))))
(defun delete (a X)
(declare (xargs :guard (setp X)))
(cond ((empty X) nil)
((equal a (head X)) (tail X))
(t (insert (head X) (delete a (tail X))))))
(defun union (X Y)
(declare (xargs :guard (and (setp X) (setp Y))))
(mbe :logic (if (empty X)
(sfix Y)
(insert (head X) (union (tail X) Y)))
:exec (fast-union X Y nil)))
(defun intersect (X Y)
(declare (xargs :guard (and (setp X) (setp Y))))
(mbe :logic (cond ((empty X) (sfix X))
((in (head X) Y)
(insert (head X) (intersect (tail X) Y)))
(t (intersect (tail X) Y)))
:exec (fast-intersect X Y nil)))
(defun difference (X Y)
(declare (xargs :guard (and (setp X) (setp Y))))
(mbe :logic (cond ((empty X) (sfix X))
((in (head X) Y) (difference (tail X) Y))
(t (insert (head X) (difference (tail X) Y))))
:exec (fast-difference X Y nil)))
(defun cardinality (X)
(declare (xargs :guard (setp X)))
(mbe :logic (if (empty X)
0
(1+ (cardinality (tail X))))
:exec (length X)))
(defund split-list (x acc acc2)
(declare (xargs :guard (true-listp x)))
(cond ((endp x)
(mv acc acc2))
((endp (cdr x))
(mv (cons (car x) acc) acc2))
(t (split-list (cddr x)
(cons (car x) acc)
(cons (cadr x) acc2)))))
(defun in-list (a x)
(declare (xargs :guard (true-listp x)))
(if (endp x)
nil
(or (equal a (car x))
(in-list a (cdr x)))))
(defun mergesort-exec (x)
(declare (xargs :guard (true-listp x)))
(cond ((endp x) nil)
((endp (cdr x)) (insert (car x) nil))
(t (mv-let (part1 part2)
(split-list x nil nil)
(union (mergesort-exec part1) (mergesort-exec part2))))))
(defun mergesort (x)
(declare (xargs :guard (true-listp x)))
(mbe :logic (if (endp x)
nil
(insert (car x)
(mergesort (cdr x))))
:exec (mergesort-exec x)))
; "High Powered" Strategies
;
; We put these at the beginning of the file so that they are tried
; as a last resort when simple methods have failed.
(encapsulate
(((predicate *) => *))
(local (defun predicate (x) x)))
(defun all (set-for-all-reduction)
(declare (xargs :guard (setp set-for-all-reduction)))
(if (empty set-for-all-reduction)
t
(and (predicate (head set-for-all-reduction))
(all (tail set-for-all-reduction)))))
(encapsulate
(((all-hyps) => *)
((all-set) => *))
(local (defun all-hyps () nil))
(local (defun all-set () nil))
(defthmd membership-constraint
(implies (all-hyps)
(implies (in arbitrary-element (all-set))
(predicate arbitrary-element))))
)
(defthmd all-by-membership
(implies (all-hyps)
(all (all-set))))
(defund subset-trigger (X Y)
(declare (xargs :guard (and (setp X) (setp Y))))
(subset X Y))
(defthm pick-a-point-subset-strategy
(implies (and (syntaxp (rewriting-goal-lit mfc state))
(syntaxp (rewriting-conc-lit `(subset ,X ,Y) mfc state)))
(equal (subset X Y)
(subset-trigger X Y))))
(COMPUTED-HINTS::automate-instantiation
:new-hint-name pick-a-point-subset-hint
:generic-theorem all-by-membership
:generic-predicate predicate
:generic-hyps all-hyps
:generic-collection all-set
:generic-collection-predicate all
:actual-collection-predicate subset
:actual-trigger subset-trigger
:predicate-rewrite (((predicate ?x ?y) (in ?x ?y)))
:tagging-theorem pick-a-point-subset-strategy
)
(defthm double-containment
(implies (and (setp X)
(setp Y))
(equal (equal X Y)
(and (subset X Y)
(subset Y X)))))
; -------------------------------------------------------------------
; Primitive Level Theorems
(defthm sets-are-true-lists
(implies (setp X)
(true-listp X)))
(defthm tail-count
(implies (not (empty X))
(< (acl2-count (tail X)) (acl2-count X)))
:rule-classes :linear)
(defthm head-count
(implies (not (empty X))
(< (acl2-count (head X)) (acl2-count X)))
:rule-classes :linear)
(defthm tail-count-built-in
(implies (not (empty X))
(o< (acl2-count (tail X)) (acl2-count X)))
:rule-classes :built-in-clause)
(defthm head-count-built-in
(implies (not (empty X))
(o< (acl2-count (head X)) (acl2-count X)))
:rule-classes :built-in-clause)
(defthm insert-insert
(equal (insert a (insert b X))
(insert b (insert a X)))
:rule-classes ((:rewrite :loop-stopper ((a b)))))
(defthm sfix-produces-set
(setp (sfix X)))
(defthm tail-produces-set
(setp (tail X)))
(defthm insert-produces-set
(setp (insert a X)))
(defthm insert-never-empty
(not (empty (insert a X))))
(defthm tail-preserves-empty
(implies (empty X)
(empty (tail X))))
(defthm nonempty-means-set
(implies (not (empty X)) (setp X)))
(defthm sfix-set-identity
(implies (setp X) (equal (sfix X) X)))
(defthm empty-sfix-cancel
(equal (empty (sfix X)) (empty X)))
(defthm head-sfix-cancel
(equal (head (sfix X)) (head X)))
(defthm tail-sfix-cancel
(equal (tail (sfix X)) (tail X)))
(defthm insert-head-tail
(implies (not (empty X))
(equal (insert (head X) (tail X)) X)))
(defthm repeated-insert
(equal (insert a (insert a X))
(insert a X)))
(defthm insert-sfix-cancel
(equal (insert a (sfix X)) (insert a X)))
(defthm head-insert-empty
(implies (empty X)
(equal (head (insert a X)) a)))
(defthm tail-insert-empty
(implies (empty X)
(empty (tail (insert a X)))))
; -------------------------------------------------------------------
; Membership Level Theorems
(defthm not-in-self
(not (in x x)))
(defthm in-sfix-cancel
(equal (in a (sfix X)) (in a X)))
(defthm never-in-empty
(implies (empty X) (not (in a X))))
(defthm in-set
(implies (in a X) (setp X)))
(defthm in-tail
(implies (in a (tail X)) (in a X)))
(defthm in-tail-or-head
(implies (and (in a X) (not (in a (tail X))))
(equal (head X) a)))
(defthm in-head
(equal (in (head X) X)
(not (empty X))))
(defthm head-unique
(not (in (head X) (tail X))))
(defthm insert-identity
(implies (in a X) (equal (insert a X) X)))
(defthm in-insert
(equal (in a (insert b X))
(or (in a X)
(equal a b))))
(defthm subset-transitive
(implies (and (subset X Y) (subset Y Z))
(subset X Z)))
(defthm subset-insert-X
(equal (subset (insert a X) Y)
(and (subset X Y)
(in a Y))))
(defthm subset-sfix-cancel-X
(equal (subset (sfix X) Y) (subset X Y)))
(defthm subset-sfix-cancel-Y
(equal (subset X (sfix Y)) (subset X Y)))
(defthm subset-in
(implies (and (subset X Y) (in a X))
(in a Y)))
(defthm subset-in-2
(implies (and (subset X Y) (not (in a Y)))
(not (in a X))))
(defthm empty-subset
(implies (empty X) (subset X Y)))
(defthm empty-subset-2
(implies (empty Y)
(equal (subset X Y) (empty X))))
(defthm subset-reflexive
(subset X X))
(defthm subset-insert
(subset X (insert a X)))
(defthm subset-tail
(subset (tail X) X)
:rule-classes ((:rewrite)
(:forward-chaining :trigger-terms ((tail x)))))
; -------------------------------------------------------------------
; Weakly Inducting over Insertions
(defthm weak-insert-induction-helper-1
(implies (and (not (in a X))
(not (equal (head (insert a X)) a)))
(equal (head (insert a X)) (head X))))
(defthm weak-insert-induction-helper-2
(implies (and (not (in a X))
(not (equal (head (insert a X)) a)))
(equal (tail (insert a X)) (insert a (tail X)))))
(defthm weak-insert-induction-helper-3
(implies (and (not (in a X))
(equal (head (insert a X)) a))
(equal (tail (insert a X)) (sfix X))))
(defun weak-insert-induction (a X)
(declare (xargs :guard (setp X)))
(cond ((empty X) nil)
((in a X) nil)
((equal (head (insert a X)) a) nil)
(t (list (weak-insert-induction a (tail X))))))
(defthm use-weak-insert-induction t
:rule-classes ((:induction
:pattern (insert a X)
:scheme (weak-insert-induction a X))))
; -------------------------------------------------------------------
; Outer Level Theorems
(defthm delete-delete
(equal (delete a (delete b X))
(delete b (delete a X)))
:rule-classes ((:rewrite :loop-stopper ((a b)))))
(defthm delete-set
(setp (delete a X)))
(defthm delete-preserves-empty
(implies (empty X)
(empty (delete a X))))
(defthm delete-in
(equal (in a (delete b X))
(and (in a X)
(not (equal a b)))))
(defthm delete-sfix-cancel
(equal (delete a (sfix X))
(delete a X)))
(defthm delete-nonmember-cancel
(implies (not (in a X))
(equal (delete a X) (sfix X))))
(defthm repeated-delete
(equal (delete a (delete a X))
(delete a X)))
(defthm delete-insert-cancel
(equal (delete a (insert a X))
(delete a X)))
(defthm insert-delete-cancel
(equal (insert a (delete a X))
(insert a X)))
(defthm subset-delete
(subset (delete a X) X))
(defthm union-symmetric
(equal (union X Y) (union Y X))
:rule-classes ((:rewrite :loop-stopper ((X Y)))))
(defthm union-commutative
(equal (union X (union Y Z))
(union Y (union X Z)))
:rule-classes ((:rewrite :loop-stopper ((X Y)))))
(defthm union-insert-X
(equal (union (insert a X) Y)
(insert a (union X Y))))
(defthm union-insert-Y
(equal (union X (insert a Y))
(insert a (union X Y))))
(defthm union-delete-X
(equal (union (delete a X) Y)
(if (in a Y)
(union X Y)
(delete a (union X Y)))))
(defthm union-delete-Y
(equal (union X (delete a Y))
(if (in a X)
(union X Y)
(delete a (union X Y)))))
(defthm union-set
(setp (union X Y)))
(defthm union-sfix-cancel-X
(equal (union (sfix X) Y) (union X Y)))
(defthm union-sfix-cancel-Y
(equal (union X (sfix Y)) (union X Y)))
(defthm union-empty-X
(implies (empty X)
(equal (union X Y) (sfix Y))))
(defthm union-empty-Y
(implies (empty Y)
(equal (union X Y) (sfix X))))
(defthm union-empty
(equal (empty (union X Y))
(and (empty X) (empty Y))))
(defthm union-in
(equal (in a (union X Y))
(or (in a X) (in a Y))))
(defthm union-subset-X
(subset X (union X Y)))
(defthm union-subset-Y
(subset Y (union X Y)))
(defthm union-self
(equal (union X X) (sfix X)))
(defthm union-associative
(equal (union (union X Y) Z)
(union X (union Y Z))))
(defthm union-outer-cancel
(equal (union X (union X Z))
(union X Z)))
(defthm intersect-symmetric
(equal (intersect X Y) (intersect Y X))
:rule-classes ((:rewrite :loop-stopper ((X Y)))))
(defthm intersect-insert-X
(implies (not (in a Y))
(equal (intersect (insert a X) Y)
(intersect X Y))))
(defthm intersect-insert-Y
(implies (not (in a X))
(equal (intersect X (insert a Y))
(intersect X Y))))
(defthm intersect-delete-X
(equal (intersect (delete a X) Y)
(delete a (intersect X Y))))
(defthm intersect-delete-Y
(equal (intersect X (delete a Y))
(delete a (intersect X Y))))
(defthm intersect-set
(setp (intersect X Y)))
(defthm intersect-sfix-cancel-X
(equal (intersect (sfix X) Y) (intersect X Y)))
(defthm intersect-sfix-cancel-Y
(equal (intersect X (sfix Y)) (intersect X Y)))
(defthm intersect-empty-X
(implies (empty X) (empty (intersect X Y))))
(defthm intersect-empty-Y
(implies (empty Y) (empty (intersect X Y))))
(defthm intersect-in
(equal (in a (intersect X Y))
(and (in a Y) (in a X))))
(defthm intersect-subset-X
(subset (intersect X Y) X))
(defthm intersect-subset-Y
(subset (intersect X Y) Y))
(defthm intersect-self
(equal (intersect X X) (sfix X)))
(defthm intersect-associative
(equal (intersect (intersect X Y) Z)
(intersect X (intersect Y Z))))
(defthmd union-over-intersect
(equal (union X (intersect Y Z))
(intersect (union X Y) (union X Z))))
(defthm intersect-over-union
(equal (intersect X (union Y Z))
(union (intersect X Y) (intersect X Z))))
(defthm intersect-commutative
(equal (intersect X (intersect Y Z))
(intersect Y (intersect X Z)))
:rule-classes ((:rewrite :loop-stopper ((X Y)))))
(defthm intersect-outer-cancel
(equal (intersect X (intersect X Z))
(intersect X Z)))
(defthm difference-set
(setp (difference X Y)))
(defthm difference-sfix-X
(equal (difference (sfix X) Y) (difference X Y)))
(defthm difference-sfix-Y
(equal (difference X (sfix Y)) (difference X Y)))
(defthm difference-empty-X
(implies (empty X)
(equal (difference X Y) (sfix X))))
(defthm difference-empty-Y
(implies (empty Y)
(equal (difference X Y) (sfix X))))
(defthm difference-in
(equal (in a (difference X Y))
(and (in a X)
(not (in a Y)))))
(defthm difference-subset-X
(subset (difference X Y) X))
(defthm subset-difference
(equal (empty (difference X Y))
(subset X Y)))
(defthm difference-over-union
(equal (difference X (union Y Z))
(intersect (difference X Y) (difference X Z))))
(defthm difference-over-intersect
(equal (difference X (intersect Y Z))
(union (difference X Y) (difference X Z))))
(defthm difference-insert-X
(equal (difference (insert a X) Y)
(if (in a Y)
(difference X Y)
(insert a (difference X Y)))))
(defthm difference-insert-Y
(equal (difference X (insert a Y))
(delete a (difference X Y))))
(defthm difference-delete-X
(equal (difference (delete a X) Y)
(delete a (difference X Y))))
(defthm difference-delete-Y
(equal (difference X (delete a Y))
(if (in a X)
(insert a (difference X Y))
(difference X Y))))
(defthm difference-preserves-subset
(implies (subset X Y)
(subset (difference X Z)
(difference Y Z))))
(defthm cardinality-type
(and (integerp (cardinality X))
(<= 0 (cardinality X)))
:rule-classes :type-prescription)
(defthm cardinality-zero-empty
(equal (equal (cardinality x) 0)
(empty x)))
(defthm cardinality-sfix-cancel
(equal (cardinality (sfix X)) (cardinality X)))
(defthm insert-cardinality
(equal (cardinality (insert a X))
(if (in a X)
(cardinality X)
(1+ (cardinality X)))))
(defthm delete-cardinality
(equal (cardinality (delete a X))
(if (in a X)
(1- (cardinality X))
(cardinality X))))
(defthm subset-cardinality
(implies (subset X Y)
(<= (cardinality X) (cardinality Y)))
:rule-classes (:rewrite :linear))
(defthmd equal-cardinality-subset-is-equality
(implies (and (setp X)
(setp Y)
(subset X Y)
(equal (cardinality X) (cardinality Y)))
(equal (equal X Y) t)))
(defthm intersect-cardinality-X
(<= (cardinality (intersect X Y)) (cardinality X))
:rule-classes :linear)
(defthm intersect-cardinality-Y
(<= (cardinality (intersect X Y)) (cardinality Y))
:rule-classes :linear)
(defthm expand-cardinality-of-union
(equal (cardinality (union X Y))
(- (+ (cardinality X) (cardinality Y))
(cardinality (intersect X Y))))
:rule-classes :linear)
(defthm expand-cardinality-of-difference
(equal (cardinality (difference X Y))
(- (cardinality X)
(cardinality (intersect X Y))))
:rule-classes :linear)
(defthm intersect-cardinality-subset
(implies (subset X Y)
(equal (cardinality (intersect X Y))
(cardinality X)))
:rule-classes (:rewrite :linear))
(defthm intersect-cardinality-non-subset
(implies (not (subset x y))
(< (cardinality (intersect x y))
(cardinality x)))
:rule-classes :linear)
(defthm intersect-cardinality-subset-2
(equal (equal (cardinality (intersect X Y)) (cardinality X))
(subset X Y)))
(defthm intersect-cardinality-non-subset-2
(equal (< (cardinality (intersect x y)) (cardinality x))
(not (subset x y))))
; -------------------------------------------------------------------
; Mergesort Theorems
(defthm in-list-cons
(equal (in-list a (cons b x))
(or (equal a b)
(in-list a x))))
(defthm in-list-append
(equal (in-list a (append x y))
(or (in-list a x)
(in-list a y))))
(defthm in-list-revappend
(equal (in-list a (revappend x y))
(or (in-list a x)
(in-list a y))))
(defthm in-list-reverse
(equal (in-list a (reverse x))
(in-list a x)))
(defthm in-list-on-set
(implies (setp X)
(equal (in-list a X)
(in a X))))
(defthm mergesort-set
(setp (mergesort x)))
(defthm in-mergesort
(equal (in a (mergesort x))
(in-list a x)))))
(defthm mergesort-set-identity
(implies (setp X)
(equal (mergesort X) X)))