diff options
author | Camm Maguire <camm@debian.org> | 2017-05-08 12:58:52 -0400 |
---|---|---|
committer | Camm Maguire <camm@debian.org> | 2017-05-08 12:58:52 -0400 |
commit | 092176848cbfd27b96c323cc30c54dff4c4a6872 (patch) | |
tree | 91b91b4db76805fd2a09de0745b22080a9ebd335 /books/workshops/2002/kaufmann-sumners/support |
Import acl2_7.4dfsg.orig.tar.gz
[dgit import orig acl2_7.4dfsg.orig.tar.gz]
Diffstat (limited to 'books/workshops/2002/kaufmann-sumners/support')
3 files changed, 1625 insertions, 0 deletions
diff --git a/books/workshops/2002/kaufmann-sumners/support/records.lisp b/books/workshops/2002/kaufmann-sumners/support/records.lisp new file mode 100644 index 0000000..5fdaf9d --- /dev/null +++ b/books/workshops/2002/kaufmann-sumners/support/records.lisp @@ -0,0 +1,306 @@ +; Rob Sumners + +(in-package "ACL2") + +#| + +We define properties of a generic record accessor function and updater +function. The basic functions are (g a r) and (s a v r) where a is an +address/key, v is a value, r is a record, and (g a r) returns the value set to +address a in record r, and (s a v r) returns a new record with address a set to +value v in record r. + +The following main lemmas are "exported" about record (g)et and (s)et: + +(defthm g-same-s + (equal (g a (s a v r)) + v)) + +(defthm g-diff-s + (implies (not (equal a b)) + (equal (g a (s b v r)) + (g a r)))) + +(defthm s-same-g + (equal (s a (g a r) r) + r)) + +(defthm s-same-s + (equal (s a y (s a x r)) + (s a y r))) + +(defthm s-diff-s + (implies (not (equal a b)) + (equal (s b y (s a x r)) + (s a x (s b y r)))) + :rule-classes ((:rewrite :loop-stopper ((b a s))))) + +We also include some auxiliary lemmas which have proven useful. + +(defthm access-of-nil-is-nil + (not (g a nil))) + +(defthm record-set-cannot-be-nil + (implies v (s a v r))) + +(defthm record-get-non-nil-cannot-be-nil + (implies (g a r) r)) + +We normalize the record structures (which allows the 'equal-ity based rewrite +rules) as alists where the keys (cars) are ordered using the total-order added +to ACL2 and defined in the included book. We define a set of "-aux" functions +which assume well-formed records -- defined by rcdp -- and then prove the +desired properties using hypothesis assuming well-formed records. + +We then remove these well-formed record hypothesis by defining an invertible +mapping (acl2->rcd) taking any ACL2 object and returning a well-formed +record. We then prove the desired properties using the proper translations of +the -aux functions to the acl2 objects, and subsequently remove the +well-formed record hypothesis. + +|# + +(include-book "../../../../misc/total-order") + +;; BEGIN records definitions. + +(defun rcdp (x) + (declare (xargs :guard t)) + (or (null x) + (and (consp x) + (consp (car x)) + (rcdp (cdr x)) + (cdar x) + (or (null (cdr x)) + (<< (caar x) (caadr x)))))) + +(defthm rcdp-implies-alistp + (implies (rcdp x) (alistp x))) + +(defun ifrp (x) ;; ill-formed rcdp + (declare (xargs :guard t)) + (or (not (rcdp x)) + (and (consp x) + (null (cdr x)) + (consp (car x)) + (null (caar x)) + (ifrp (cdar x))))) + +(defun acl2->rcd (x) ;; function mapping acl2 objects to well-formed records. + (declare (xargs :guard t)) + (if (ifrp x) (list (cons nil x)) x)) + +(defun rcd->acl2 (x) ;; inverse of acl2->rcd. + (declare (xargs :guard (rcdp x))) + (if (ifrp x) (cdar x) x)) + +(defun g-aux (a x) ;; record g(et) when x is a well-formed record. + (declare (xargs :guard (rcdp x))) + (cond ((or (endp x) + (<< a (caar x))) + nil) + ((equal a (caar x)) + (cdar x)) + (t + (g-aux a (cdr x))))) + +;; we use the name g-aux in this book, but used rcd-access in the paper for +;; presentation reasons. Here we simply document their equivalence using the +;; following macro. +(defmacro rcd-access (a r) + `(g-aux ,a ,r)) + +(defun g (a x) ;; the generic record g(et) which works on any ACL2 object. + (declare (xargs :guard t)) + (g-aux a (acl2->rcd x))) + +(defun acons-if (a v x) + (declare (xargs :guard (rcdp x))) + (if v (acons a v x) x)) + +(defun s-aux (a v r) ;; record s(et) when x is a well-formed record. + (declare (xargs :guard (rcdp r))) + (cond ((or (endp r) + (<< a (caar r))) + (acons-if a v r)) + ((equal a (caar r)) + (acons-if a v (cdr r))) + (t + (cons (car r) (s-aux a v (cdr r)))))) + +;; we use the name s-aux in this book, but used rcd-update in the paper for +;; presentation reasons. Here we simply document their equivalence using the +;; following macro. +(defmacro rcd-update (a v r) + `(s-aux ,a ,v ,r)) + +;; we need the following theorems in order to get the guard for s to verify. + +(local +(defthm s-aux-is-bounded + (implies (and (rcdp r) + (s-aux a v r) + (<< e a) + (<< e (caar r))) + (<< e (caar (s-aux a v r)))))) + +(local +(defthm s-aux-preserves-rcdp + (implies (rcdp r) + (rcdp (s-aux a v r))))) + +(defun s (a v x) ;; the generic record s(et) which works on any ACL2 object. + (declare (xargs :guard t)) + (rcd->acl2 (rcd-update a v (acl2->rcd x)))) + + +;;;; basic property of records ;;;; + +(local +(defthm rcdp-implies-true-listp + (implies (rcdp x) + (true-listp x)) + :rule-classes (:forward-chaining + :rewrite))) + + +;;;; initial properties of s-aux and g-aux ;;;; + +(local +(defthm g-aux-same-s-aux + (implies (rcdp r) + (equal (g-aux a (s-aux a v r)) + v)))) + +(local +(defthm g-aux-diff-s-aux + (implies (and (rcdp r) + (not (equal a b))) + (equal (g-aux a (s-aux b v r)) + (g-aux a r))))) + +(local +(defthm s-aux-same-g-aux + (implies (rcdp r) + (equal (s-aux a (g-aux a r) r) + r)))) + +(local +(defthm s-aux-same-s-aux + (implies (rcdp r) + (equal (s-aux a y (s-aux a x r)) + (s-aux a y r))))) + +(local +(defthm s-aux-diff-s-aux + (implies (and (rcdp r) + (not (equal a b))) + (equal (s-aux b y (s-aux a x r)) + (s-aux a x (s-aux b y r)))) + :rule-classes ((:rewrite :loop-stopper ((b a s)))))) + +(local +(defthm s-aux-non-nil-cannot-be-nil + (implies (and v (rcdp r)) + (s-aux a v r)))) + +(local +(defthm g-aux-is-nil-for-<< + (implies (and (rcdp r) + (<< a (caar r))) + (equal (g-aux a r) nil)))) + + +;;;; properties of acl2->rcd and rcd->acl2 ;;;; + +(local +(defthm acl2->rcd-rcd->acl2-of-rcdp + (implies (rcdp x) + (equal (acl2->rcd (rcd->acl2 x)) + x)))) + +(local +(defthm acl2->rcd-returns-rcdp + (rcdp (acl2->rcd x)))) + +(local +(defthm acl2->rcd-preserves-equality + (iff (equal (acl2->rcd x) (acl2->rcd y)) + (equal x y)))) + +(local +(defthm rcd->acl2-acl2->rcd-inverse + (equal (rcd->acl2 (acl2->rcd x)) x))) + +(local +(defthm rcd->acl2-of-record-non-nil + (implies (and r (rcdp r)) + (rcd->acl2 r)))) + +(in-theory (disable acl2->rcd rcd->acl2)) + + +;;;; final (exported) properties of record g(et) and s(et) ;;;; + +;; NOTE that these theorems basically follow from the "equivalent" properties +;; for s-aux and g-aux with rcdp hypothesis, and the lemmas about the acl2->rcd +;; and its inverse rcd->acl2. If the user wanted to add to the following set of +;; exported theorems, they should add the corresponding lemma about s-aux and +;; g-aux using rcdp hypothesis and then add the theorem here about the generic +;; s(et) and g(et) they wish to export from the book. + +(defthm g-same-s + (equal (g a (s a v r)) + v)) + +(defthm g-diff-s + (implies (not (equal a b)) + (equal (g a (s b v r)) + (g a r)))) + +;;;; NOTE: The following can be used instead of the above rules to force ACL2 +;;;; to do a case-split. We disable this rule by default since it can lead to +;;;; an expensive case explosion, but in many cases, this rule may be more +;;;; effective than two rules above and should be enabled. + +(defthm g-of-s-redux + (equal (g a (s b v r)) + (if (equal a b) v (g a r)))) + +(in-theory (disable g-of-s-redux)) + +(defthm s-same-g + (equal (s a (g a r) r) + r)) + +(defthm s-same-s + (equal (s a y (s a x r)) + (s a y r))) + +(defthm s-diff-s + (implies (not (equal a b)) + (equal (s b y (s a x r)) + (s a x (s b y r)))) + :rule-classes ((:rewrite :loop-stopper ((b a s))))) + +;; the following theorems are less relevant but have been useful in dealing +;; with a default record of NIL. + +(defthm g-of-nil-is-nil + (not (g a nil))) + +(defthm s-non-nil-cannot-be-nil + (implies v (s a v r)) + :hints (("Goal" + :in-theory (disable rcd->acl2-of-record-non-nil) + :use (:instance rcd->acl2-of-record-non-nil + (r (s-aux a v (acl2->rcd r))))))) + +(defthm non-nil-if-g-non-nil + (implies (g a r) r) + :rule-classes :forward-chaining) + +;; We disable s and g, assuming the rules proven in this book are sufficient to +;; manipulate record terms which are encountered. + +(in-theory (disable s g)) diff --git a/books/workshops/2002/kaufmann-sumners/support/records0.lisp b/books/workshops/2002/kaufmann-sumners/support/records0.lisp new file mode 100644 index 0000000..50aee49 --- /dev/null +++ b/books/workshops/2002/kaufmann-sumners/support/records0.lisp @@ -0,0 +1,427 @@ +; Matt Kaufmann and Rob Sumners + +(in-package "ACL2") + +#| + +We define properties of a generic record accessor function and updater +function. The basic functions are (g a r) and (s a v r) where a is an +address/key, v is a value, r is a record, and (g a r) returns the value set to +address a in record r, and (s a v r) returns a new record with address a set to +value v in record r. + +The following main lemma are "exported" about record (g)et and (s)et: + +(defthm g-same-s + (equal (g a (s a v r)) + v)) + +(defthm g-diff-s + (implies (not (equal a b)) + (equal (g a (s b v r)) + (g a r)))) + +(defthm s-same-g + (equal (s a (g a r) r) + r)) + +(defthm s-same-s + (equal (s a y (s a x r)) + (s a y r))) + +(defthm s-diff-s + (implies (not (equal a b)) + (equal (s b y (s a x r)) + (s a x (s b y r)))) + :rule-classes ((:rewrite :loop-stopper ((b a s))))) + + +we also include some auxiliary lemmas which have proven useful, + +(defthm access-of-nil-is-nil + (not (g a nil))) + +(defthm record-set-cannot-be-nil + (implies v (s a v r))) + +(defthm record-get-non-nil-cannot-be-nil + (implies (g a r) r)) + +(defthm s-preserves-recordp + (implies (rcdp r) + (rcdp (s a v r)))) + + +and we include a theorem formerly from record-equality.lisp + +(defthm rcdp-equality-sufficiency + (implies (and (rcdp r1) (rcdp r2)) + (equal (equal r1 r2) + (let ((field (bad-field r1 r2))) + (implies (symbolp field) + (equal (g field r1) + (g field r2))))))) + +Main idea of how this all works: + +A record is an ordered alist whose values are all non-nil. + +A lookup structure is the cons of a record onto any object, such that this +object is (recursively) not a lookup structure. + +So, the cdr of a lookup structure is "junk", while the car is the record that +holds the values. However, if we have other than a lookup structure then we +view its entirety as "junk." + +G ("get") returns nil on a non-lookup structure, else looks up in the record +part (the car). + +S ("set") would "like" simply to set the value in the record part. However, it +respects the form of the lookup structure, so for example it has to delete an +existing key if it wants to set a key's value to nil. + +|# + +(include-book "../../../../misc/total-order") + +(defun rcdp (x) + +; This is the recognizer for an ordered alist with no nil cdrs. + + (declare (xargs :guard t)) + (if (atom x) (null x) + (and (consp (car x)) + (cdar x) + (if (atom (cdr x)) + (null (cdr x)) + (and (rcdp (cdr x)) + (<< (caar x) (caadr x))))))) + +(defun lsp (x) + +; This is the recognizer for a lookup structure (see earlier comment). + + (declare (xargs :guard t)) + (or (rcdp x) + (and (consp x) + (not (lsp (cdr x))) + (rcdp (car x)) + (car x)))) + +(defun g (a x) + +; Get the value of a in x. + + (declare (xargs :guard t)) + (cond ((rcdp x) + (cdr (assoc-equal a x))) + ((lsp x) + (cdr (assoc-equal a (car x)))) + (t nil))) + +(defun s-aux (a v r) + +; Update record r by binding a to a non-nil value, v. + + (declare (xargs :guard (rcdp r))) + (cond ((endp r) + (cons (cons a v) nil)) + ((equal a (caar r)) + (cons (cons a v) (cdr r))) + ((<< a (caar r)) + (cons (cons a v) r)) + (t (cons (car r) (s-aux a v (cdr r)))))) + +(defun delete-key (key alist) + (declare (xargs :guard (rcdp alist))) + (cond ((endp alist) alist) + ((equal key (caar alist)) + (cdr alist)) + (t (cons (car alist) + (delete-key key (cdr alist)))))) + +(defun s (a v x) + (declare (xargs :guard t)) + (cond ((rcdp x) + (if (null v) + (delete-key a x) + (s-aux a v x))) + ((not (lsp x)) + (if v + ;; then make x into the cdr of the returned lookup structure + (cons (list (cons a v)) x) + ;; else x already is an appropriate result + x)) + ;; else we have (cons record junk) + ((null v) + (if (and (null (cdr (car x))) + (equal (caar (car x)) a)) + ;; then return the junk; there is nothing left of the record + (cdr x) + ;; else delete the key, a, from the record portion + (cons (delete-key a (car x)) + (cdr x)))) + (t + ;; since (lsp x) and v is non-nil, we simply update the record portion + (cons (s-aux a v (car x)) + (cdr x))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;; Interaction properties for s and g; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(local +(defthm delete-key-no-op + (implies (and (rcdp alist) + (not (assoc-equal key alist))) + (equal (delete-key key alist) alist)))) + +(local +(defthm values-not-nil + (implies (rcdp alist) + ;; The order below ooks dangerous, but apparently the prover's + ;; heuristics save us. + (iff (assoc-equal key alist) + (cdr (assoc-equal key alist)))))) + +(local +(defthm key-order-lemma + (implies (and (rcdp alist) + (<< a (caar alist))) + (not (cdr (assoc-equal a alist)))))) + +(local +(defthm s-aux-to-same + (implies (and (rcdp alist) + (cdr (assoc-equal a alist))) + (equal (s-aux a (cdr (assoc-equal a alist)) + alist) + alist)))) + +;;;; we can now prove s-same-g +;;;; (equal (s a (g a r) r) +;;;; r)) + +(local +(defthm value-s-aux + (implies (rcdp alist) + (equal (cdr (assoc-equal a (s-aux a v alist))) + v)))) + +(local +(defthm s-aux-preserves-rcdp + (implies (and (rcdp x) + v) + (rcdp (s-aux a v x))))) + +(local +(defthm cdr-assoc-equal-delete-key + (implies (rcdp x) + (not (cdr (assoc-equal a (delete-key a x))))))) + +; G-diff-s should go here, but I forgot it on the first pass, so I'll put +; it at the end where more lemmas are available. + +(local +(defthm rcdp-delete-key + (implies (rcdp alist) + (rcdp (delete-key a alist))))) + +;;;; we can now prove g-same-s +;;;; (equal (g a (s a v r)) +;;;; v)) + +(local +(defthm s-aux-s-aux-same + (implies (rcdp alist) + (equal (s-aux a v (s-aux a w alist)) + (s-aux a v alist))))) + +(local +(defthm delete-key-s-aux-same + (implies (rcdp alist) + (equal (delete-key a (s-aux a v alist)) + (delete-key a alist))))) + +(local +(defthm <<-s-aux + (implies (and (rcdp alist) + (<< b (caar alist)) + (not (<< a b)) + (not (equal a b))) + (<< b (caar (s-aux a v alist)))))) + +(local +(defthm value-nil-sufficiency + (implies (and (rcdp alist) + (<< a (caar alist))) + (equal (cdr (assoc-equal a alist)) + nil)))) + +(local +(defthm caar-delete-key + (implies (rcdp alist) + (equal (caar (delete-key a alist)) + (if (eq a (caar alist)) + (caadr alist) + (caar alist)))))) + +(local +(defthm s-aux-delete-key + (implies (rcdp alist) + (equal (s-aux a x (delete-key a alist)) + (s-aux a x alist))))) + +(local +(defthm <<-hack + (implies (and (<< r6 r9) + (not (<< r4 r9)) + (not (equal r6 r4))) + (<< r6 r4)) + :hints (("Goal" :in-theory (disable <<-trichotomy) + :use ((:instance <<-trichotomy + (x r6) (y r4))))))) + +;;;; we can now prove s-same-s +;;;; (equal (s a y (s a x r)) +;;;; (s a y r))) + +(local +(defthm s-aux-diff-s-aux + (implies (and (not (equal a b)) + (rcdp r) + x + y) + (equal (s-aux b y (s-aux a x r)) + (s-aux a x (s-aux b y r)))) + :rule-classes ((:rewrite :loop-stopper ((b a s-aux)))))) + +(local +(defthm rcdp-s-aux + (implies (and (rcdp x) + v) + (rcdp (s-aux a v x))))) + +(local +(defthm consp-delete-key + (implies (rcdp alist) + (equal (consp (delete-key a alist)) + (or (consp (cdr alist)) + (and (consp alist) + (not (equal a (caar alist))))))))) + +(local +(defthm delete-key-delete-key + (implies (rcdp r) + (equal (delete-key b (delete-key a r)) + (delete-key a (delete-key b r)))) + :rule-classes ((:rewrite :loop-stopper ((b a delete-key)))))) + +(local +(defthm delete-key-s-aux + (implies (and (not (equal a b)) + (rcdp r) + x) + (equal (delete-key b (s-aux a x r)) + (s-aux a x (delete-key b r)))))) + +(local +(defthm delete-key-nil + (implies (not (delete-key a x)) + (not (delete-key a (delete-key b x)))))) + +;;;; we can now prove s-diff-s +;;;; (implies (not (equal a b)) +;;;; (equal (s b y (s a x r)) +;;;; (s a x (s b y r)))) + +(local +(defthm assoc-equal-s-aux-different + (implies (not (equal a b)) + (equal (assoc-equal a (s-aux b v alist)) + (assoc-equal a alist))))) + +(local +(defthm assoc-equal-delete-key-different + (implies (not (equal a b)) + (equal (assoc-equal a (delete-key b alist)) + (assoc-equal a alist))))) + +(defun bad-field (r1 r2) + (declare (xargs :guard (and (rcdp r1) (rcdp r2)))) + (cond ((endp r1) (caar r2)) + ((endp r2) (caar r1)) + ((equal (car r1) (car r2)) + (bad-field (cdr r1) (cdr r2))) + ((<< (caar r1) (caar r2)) + (caar r1)) + (t (caar r2)))) + +(local +(defthm assoc-eq-symbol-< + (implies (and (rcdp s) + (<< field (caar s))) + (equal (assoc-equal field s) nil)))) + +;;;; we can now prove g-diff-s +;;;; (implies (not (equal a b)) +;;;; (equal (g a (s b v r)) +;;;; (g a r)))) + +;;;;;;;;;;; THE MAIN (exported) THEOREMS ;;;;;;;;;;;; + +(defthm access-of-nil-is-nil + (not (g a nil))) + +(defthm record-set-cannot-be-nil + (implies v (s a v r))) + +(defthm record-get-non-nil-cannot-be-nil + (implies (g a r) r) + :rule-classes :forward-chaining) + +(defthm s-same-g + (equal (s a (g a r) r) + r)) + +(defthm g-same-s + (equal (g a (s a v r)) + v)) + +(defthm s-same-s + (equal (s a y (s a x r)) + (s a y r))) + +(defthm s-diff-s + (implies (not (equal a b)) + (equal (s b y (s a x r)) + (s a x (s b y r)))) + :rule-classes ((:rewrite :loop-stopper ((b a s))))) + +(defthm g-diff-s + (implies (not (equal a b)) + (equal (g a (s b v r)) + (g a r)))) + +(defthm s-preserves-recordp + (implies (rcdp r) + (rcdp (s a v r))) + :rule-classes ((:forward-chaining + :trigger-terms ((s a v r))) + :rewrite)) + +(defthm rcdp-equality-sufficiency + (implies (and (rcdp r1) (rcdp r2)) + (equal (equal r1 r2) + (let ((field (bad-field r1 r2))) + (equal (g field r1) + (g field r2))))) + :hints (("Goal" :induct (bad-field r1 r2)))) + +; We will almost surely never care about the definition of bad-field, other +; than the rule above. We also disable s and g, assuming the rules proven in +; this book are sufficient to manipulate record terms which are encountered. +; Finally, we disable rcdp-equality-sufficiency, since it can be an expensive +; rewrite rule (because it is hung on equal). + +(in-theory (disable s g bad-field rcdp-equality-sufficiency)) diff --git a/books/workshops/2002/kaufmann-sumners/support/sets.lisp b/books/workshops/2002/kaufmann-sumners/support/sets.lisp new file mode 100644 index 0000000..970be0d --- /dev/null +++ b/books/workshops/2002/kaufmann-sumners/support/sets.lisp @@ -0,0 +1,892 @@ +; Rob Sumners + +(in-package "ACL2") + +#| + +We define the common boolean operations (and a few other common useful notions) +on sets canonicalized as ordered lists using Pete's total ordering of all ACL2 +objects. Further, the functions have been defined with a normalization of all +ACL2 objects as appropriate sets (we define a 1-1 function which maps any ACL2 +object to a corresponding well-formed set) and using this normal (and its +inverse), we can prove properties about normalized set operations which use +equal-ity instead of set-equality and require no backtracking to relieve +well-formed set hypotheses. + +EXPORTED logic functions: + + (in e x) -- set membership predicate, is element e a member of set x + (subset x y) -- subset predicate, is set x a subset of set y + (isect x y) -- the set intersection of set x and set y + (unite x y) -- the set union of set x and set y + (sdiff x y) -- the set of elements in set x but not in set y + (card x) -- returns the number of objects in the set x + (s1 e) -- the singleton set consisting only of the element e + (scar x) -- the least (by <<) element in the set x, nil if x is empty + () -- NIL is unique representative value for empty set, + so use NULL or NOT to test a set for emptiness + +EXPORTED theorems provided at the end of this file. + +I have removed all of the subgoal hints except for those introduced by the +macro defthm-ternary-sets. These subgoal hints are reasonable since they are +introduced in the context of a provided induction scheme and they help speed +the proofs through considerably by avoiding the problem in ACL2 of +free-variable matching in the application of <<-transitive. + +|# + +(include-book "../../../../misc/total-order") + +;; i needed to add the following forward-chaining rule to make better use +;; of <<-trichotomy from the included order book. + +(local +(defthm <<-trichotomy-forward-chain1 + (implies (and (not (<< x y)) + (not (equal x y))) + (<< y x)) + :rule-classes :forward-chaining)) + +(defun setp (x) + (or (null x) + (and (consp x) + (setp (rest x)) + (or (null (rest x)) + (<< (first x) (second x)))))) + +(defun ifsp (x) ;; ill-formed setp + (or (not (setp x)) + (and (consp x) + (null (cdr x)) + (ifsp (car x))))) + +(defun norm->set (x) + (if (ifsp x) (list x) x)) + +(defun set->norm (x) + (if (ifsp x) (first x) x)) + +(defun in-aux (e x) + (and (not (endp x)) + (or (equal e (first x)) + (and (<< (first x) e) + (in-aux e (rest x)))))) + +(defun in (e x) + (in-aux e (norm->set x))) + +(defun subset-aux (x y) + (or (endp x) + (and (not (endp y)) + (cond ((equal (first x) (first y)) + (subset-aux (rest x) (rest y))) + ((<< (first y) (first x)) + (subset-aux x (rest y))) + (t nil))))) + +(defun subset (x y) + (subset-aux (norm->set x) (norm->set y))) + +(defun isect-aux (x y) + (declare (xargs :measure (+ (acl2-count x) + (acl2-count y)))) + (cond ((endp x) ()) + ((endp y) ()) + ((equal (first x) (first y)) + (cons (first x) + (isect-aux (rest x) (rest y)))) + ((<< (first x) (first y)) + (isect-aux (rest x) y)) + (t + (isect-aux x (rest y))))) + +(defun isect (x y) + (set->norm (isect-aux (norm->set x) (norm->set y)))) + +(defun unite-aux (x y) + (declare (xargs :measure (+ (acl2-count x) + (acl2-count y)))) + (cond ((endp x) y) + ((endp y) x) + ((equal (first x) (first y)) + (cons (first x) + (unite-aux (rest x) (rest y)))) + ((<< (first x) (first y)) + (cons (first x) + (unite-aux (rest x) y))) + (t + (cons (first y) + (unite-aux x (rest y)))))) + +(defun unite (x y) + (set->norm (unite-aux (norm->set x) (norm->set y)))) + +(defun sdiff-aux (x y) + (declare (xargs :measure (+ (acl2-count x) + (acl2-count y)))) + (cond ((endp x) ()) + ((endp y) x) + ((equal (first x) (first y)) + (sdiff-aux (rest x) (rest y))) + ((<< (first x) (first y)) + (cons (first x) + (sdiff-aux (rest x) y))) + (t + (sdiff-aux x (rest y))))) + +(defun sdiff (x y) + (set->norm (sdiff-aux (norm->set x) (norm->set y)))) + +(defun s1 (e) + (set->norm (list e))) + +(defun card (x) + (len (norm->set x))) + +(defun scar (x) + (if (ifsp x) x (first x))) + +(defmacro empty-set () + `()) + + +;;; some useful auxiliary macros which could be removed if +;;; needed (e.g. if the names conflict with existing fns) + +(defmacro sadd (e x) + `(unite (s1 ,e) ,x)) + +(defmacro sdrop (e x) + `(sdiff ,x (s1 ,e))) + +(defmacro scdr (x) + `(sdrop (scar ,x) ,x)) + +(defmacro satom (x) + `(not ,x)) + +(defmacro common (x y) + `(not (satom (isect ,x ,y)))) + + +;;;; properties of setp ;;;; + +(local +(defthm setp-implies-true-listp + (implies (setp x) + (true-listp x)) + :rule-classes (:forward-chaining + :rewrite))) + + +;;;; properties of norm->set and set->norm ;;;; + +(local +(defthm norm->set-set->norm-of-setp + (implies (setp x) + (equal (norm->set (set->norm x)) + x)))) + +(local +(defthm norm->set-of-wf-setp + (implies (not (ifsp x)) + (equal (norm->set x) x)))) + +(local +(defthm norm->set-of-if-setp + (implies (ifsp x) + (equal (norm->set x) (list x))))) + +(local +(defthm norm->set-returns-setp + (setp (norm->set x)))) + +(local +(defthm norm->set-preserves-equality + (iff (equal (norm->set x) (norm->set y)) + (equal x y)))) + +(local +(defthm set->norm-norm->set-inverse + (equal (set->norm (norm->set x)) x))) + +(local +(defthm set->norm-nil-iff-passed-nil + (implies (setp x) + (iff (set->norm x) x)))) + +(local +(defthm norm->set-of-x-is-consp-or-not-x + (iff (consp (norm->set x)) x) + :rule-classes nil)) + +(local +(defthm norm->set-is-true-listp + (true-listp (norm->set x)) + :rule-classes :type-prescription)) + +(in-theory (disable set->norm norm->set)) + + +;;;; bounded properties ;;;; + +(local +(defthm unite-aux-bounded-<< + (implies (and (<< a (first x)) + (<< a (first y))) + (<< a (first (unite-aux x y)))))) + +(local +(defthm isect-aux-bounded-<< + (implies (and (or (<< a (first x)) + (<< a (first y))) + (isect-aux x y)) + (<< a (first (isect-aux x y)))))) + +(local +(defthm sdiff-aux-bounded-<< + (implies (and (setp x) + (<< a (first x)) + (sdiff-aux x y)) + (<< a (first (sdiff-aux x y)))))) + + +;;;; type-correctness properties ;;;; + +(local +(defthm unite-aux-preserves-setp + (implies (and (setp x) (setp y)) + (setp (unite-aux x y))) + :rule-classes ((:forward-chaining + :trigger-terms ((unite-aux x y))) + :rewrite))) + +(local +(defthm isect-aux-preserves-setp + (implies (and (setp x) (setp y)) + (setp (isect-aux x y))) + :rule-classes ((:forward-chaining + :trigger-terms ((isect-aux x y))) + :rewrite))) + +(local +(defthm sdiff-aux-preserves-setp + (implies (setp x) + (setp (sdiff-aux x y))) + :rule-classes ((:forward-chaining + :trigger-terms ((sdiff-aux x y))) + :rewrite))) + + +;;;; properties of membership-aux ;;;; + +(local +(defthm in-aux-isect-aux-reduce + (equal (in-aux e (isect-aux x y)) + (and (in-aux e x) (in-aux e y))))) + +(local +(defthm in-aux-unite-aux-reduce + (equal (in-aux e (unite-aux x y)) + (or (in-aux e x) (in-aux e y))))) + +(local +(defthm in-aux-implies-bounded + (implies (and (setp x) + (<< a (first x))) + (not (in-aux a x))))) + +(local +(defthm in-aux-sdiff-aux-reduce + (implies (setp x) + (equal (in-aux e (sdiff-aux x y)) + (and (in-aux e x) (not (in-aux e y))))))) + +(local +(defthm in-aux-subset-aux-transits + (implies (and (in-aux e x) + (subset-aux x y)) + (in-aux e y)))) + + +;;;; ternary variable induction scheme and strategy ;;;; + +;; the following function defines an induction scheme used in theorems +;; involving three free variables (like associativity proofs). + +(local +(defun ternary-induct (x y z) + (declare (xargs :measure (+ (acl2-count x) + (acl2-count y) + (acl2-count z)))) + (if (or (endp x) + (endp y) + (endp z)) + ; The following was changed to avoid SBCL warning, "Asserted type NUMBER + ; conflicts with derived type (VALUES LIST &OPTIONAL)." + (list x y z) + (cond ((<< (first x) (first y)) + (cond ((<< (first x) (first z)) + (ternary-induct (rest x) y z)) + ((equal (first x) (first z)) + (ternary-induct (rest x) y (rest z))) + ((and (<< (first z) (first x)) + (<< (first z) (first y))) + (ternary-induct x y (rest z))))) + ((equal (first x) (first y)) + (cond ((<< (first x) (first z)) + (ternary-induct (rest x) (rest y) z)) + ((equal (first x) (first z)) + (ternary-induct (rest x) (rest y) (rest z))) + ((<< (first z) (first x)) + (ternary-induct x y (rest z))))) + ((<< (first y) (first x)) + (cond ((<< (first y) (first z)) + (ternary-induct x (rest y) z)) + ((equal (first y) (first z)) + (ternary-induct x (rest y) (rest z))) + ((and (<< (first z) (first y)) + (<< (first z) (first x))) + (ternary-induct x y (rest z))))))))) + +;; the following macro defines an effective strategy for inducting based on the +;; scheme ternary-induct. + +(defmacro defthm-ternary-sets (name body) + `(defthm ,name ,body + :hints (("Goal" + :induct (ternary-induct x y z) + :in-theory (disable <<-transitive)) + ("Subgoal *1/13" + :in-theory (enable <<-transitive)) + ("Subgoal *1/5" + :in-theory (enable <<-transitive))))) + + +;;;; properties of subset-aux ;;;; + +(local +(defthm unite-aux-x<y-expansion + (implies (and (consp x) + (consp y) + (<< (car x) (car y))) + (equal (unite-aux x y) + (cons (car x) + (unite-aux (cdr x) y)))))) + +(local +(defthm subset-aux-x<y-reduces-nil + (implies (and (consp x) + (consp y) + (<< (car x) (car y))) + (equal (subset-aux x y) + nil)))) + +(local +(defthm atom-unite-aux-implies-atom-params + (implies (not (consp (unite-aux x y))) + (and (not (consp x)) + (not (consp y)))))) + +(local +(defthm-ternary-sets subset-aux-unite-aux-reduction + (equal (subset-aux (unite-aux x y) z) + (and (subset-aux x z) + (subset-aux y z))))) + +(local +(in-theory (disable unite-aux-x<y-expansion))) + +(local +(defthm subset-aux-is-reflexive + (subset-aux x x))) + +(local +(defthm subset-aux-unite-aux-property + (implies (setp x) + (subset-aux x (unite-aux x y))))) + +(local +(defthm <<-irreflexive-rewrite + (implies (<< x y) + (not (equal x y))))) + +(local +(defthm-ternary-sets subset-aux-isect-aux-reduction + (equal (subset-aux x (isect-aux y z)) + (and (subset-aux x y) + (subset-aux x z))))) + +(local +(defthm subset-aux-isect-aux-property + (implies (setp x) + (subset-aux (isect-aux x y) x)))) + +(local +(defthm subset-aux-sdiff-aux-property + (implies (setp x) + (subset-aux (sdiff-aux x y) x)))) + +(local +(defthm-ternary-sets subset-aux-is-transitive + (implies (and (subset-aux x y) + (subset-aux y z)) + (subset-aux x z)))) + +(local +(defthm subset-aux-is-total-on-sets + (implies (and (setp x) (setp y) + (subset-aux x y)) + (equal (subset-aux y x) + (equal x y))))) + +(local +(defthm subset-length-property + (implies (and (setp x) + (setp y) + (subset-aux x y)) + (<= (len x) (len y))))) + +(local +(defthm len<-reduce-when-subset + (implies (and (setp x) + (setp y) + (subset-aux x y)) + (equal (< (len x) (len y)) + (not (equal x y)))))) + + +;;;; properties of unite-aux ;;;; + +(local +(defthm unite-aux-commutes + (implies (and (setp x) (setp y)) + (equal (unite-aux x y) + (unite-aux y x))))) + +(local +(defthm unite-aux-x<y-expansion-flip + (implies (and (consp x) + (consp y) + (<< (car x) (car y))) + (equal (unite-aux y x) + (cons (car x) + (unite-aux y (cdr x))))))) + +(local +(in-theory (enable unite-aux-x<y-expansion))) + +(local +(defthm-ternary-sets unite-aux-associates + (implies (and (setp x) (setp y) (setp z)) + (equal (unite-aux (unite-aux x y) z) + (unite-aux x (unite-aux y z)))))) + +(local +(in-theory (disable unite-aux-x<y-expansion-flip + unite-aux-x<y-expansion))) + +(local +(defthm unite-aux-subset-aux-property + (equal (equal (unite-aux x y) y) + (subset-aux x y)))) + +(local +(defthm length-of-unite-aux-property + (implies (and (setp x) (setp y)) + (equal (len (unite-aux x y)) + (+ (len x) + (len (sdiff-aux y x))))))) + +(local +(defthm set-norm-equality-transfer + (implies (setp x) + (equal (equal (set->norm x) y) + (equal x (norm->set y)))))) + + +;;;; properties of isect-aux ;;;; + +(local +(defthm isect-aux-commutes + (implies (and (setp x) (setp y)) + (equal (isect-aux x y) (isect-aux y x))))) + +(local +(defthm isect-aux-x<y-expansion + (implies (and (consp x) + (consp y) + (<< (car x) (car y))) + (equal (isect-aux y x) + (isect-aux y (cdr x)))))) + +(local +(defthm-ternary-sets isect-aux-associates + (implies (and (setp x) (setp y) (setp z)) + (equal (isect-aux (isect-aux x y) z) + (isect-aux x (isect-aux y z)))))) + +(local +(in-theory (disable isect-aux-commutes + unite-aux-commutes))) + +(local +(defthm isect-aux-bounded-then-not-equal + (implies (and (consp z) + (or (<< (car z) (car x)) + (<< (car z) (car y)))) + (not (equal (isect-aux x y) z))))) + +(local +(defthm isect-aux-subset-aux-property + (implies (and (setp x) (setp y)) + (equal (equal (isect-aux x y) x) + (subset-aux x y))))) + +(local +(defthm <<-irreflexive-rewrite-flip + (implies (<< x y) + (not (equal y x))))) + +(local +(defthm-ternary-sets isect-aux-unite-aux-distributes + (implies (and (setp x) (setp y) (setp z)) + (equal (isect-aux (unite-aux x y) z) + (unite-aux (isect-aux x z) + (isect-aux y z)))))) + +(local +(defthm-ternary-sets isect-aux-sdiff-aux-distributes + (implies (and (setp x) (setp y) (setp z)) + (equal (isect-aux (sdiff-aux x y) z) + (sdiff-aux (isect-aux x z) y))))) + + +;;;; properties of sdiff-aux ;;;; + +(local +(defthm sdiff-aux-subset-aux-property + (implies (and (setp x) (setp y)) + (iff (sdiff-aux x y) + (not (subset-aux x y)))))) + +(local +(defthm length-of-sdiff-aux-property + (implies (and (setp x) (setp y)) + (equal (len (sdiff-aux x y)) + (- (len x) + (len (isect-aux x y))))))) + +(local +(defthm-ternary-sets sdiff-aux-unite-aux-distributes + (implies (and (setp x) (setp y) (setp z)) + (equal (sdiff-aux (unite-aux x y) z) + (unite-aux (sdiff-aux x z) + (sdiff-aux y z)))))) + +(local +(defthm-ternary-sets sdiff-aux-unite-aux-reduction + (implies (and (setp x) (setp y) (setp z)) + (equal (sdiff-aux x (unite-aux y z)) + (sdiff-aux (sdiff-aux x y) z))))) + + +;;;; properties of s1-aux -- i.e. list ;;;; + +(local +(defthm subset-aux-reduces-to-membership + (implies (setp x) + (equal (subset-aux (list e) x) + (in-aux e x))))) + +(local +(defthm subset-aux-of-singleton + (implies (and (setp x) x + (subset-aux x (list e))) + (equal (equal x (list e)) t)))) + +(local +(defthm isect-aux-of-singleton + (implies (setp x) + (equal (isect-aux (list e) x) + (if (in-aux e x) (list e) ()))))) + +(local +(defthm sdiff-aux-of-singleton + (implies (setp x) + (equal (sdiff-aux (list e) x) + (if (in-aux e x) () (list e)))))) + + +;;;; EXPORTED THEOREMS ;;;; +;; Note, the order of the these theorems below is relevant for the +;; order in which ACL2 applies them (later ones first). This is why +;; the associativity and commutativity theorems are first since +;; restructuring unite and isect can have the detrimental effect of +;; disabling the application of other rules. + +(local +(in-theory (enable unite-aux-commutes + isect-aux-commutes))) + + +;;;; EXPORTED associative and commutative properties ;;;; + +(defthm unite-commutes + (equal (unite x y) + (unite y x))) + +(defthm unite-associates + (equal (unite (unite x y) z) + (unite x (unite y z)))) + +(defthm isect-commutes + (equal (isect x y) + (isect y x))) + +(defthm isect-associates + (equal (isect (isect x y) z) + (isect x (isect y z)))) + + +;;;; EXPORTED properties of membership ;;;; + +(defthm in-isect-reduce + (equal (in e (isect x y)) + (and (in e x) (in e y)))) + +(defthm in-unite-reduce + (equal (in e (unite x y)) + (or (in e x) (in e y)))) + +(defthm in-sdiff-reduce + (equal (in e (sdiff x y)) + (and (in e x) (not (in e y))))) + +(defthm in-subset-transits + (implies (and (in e x) + (subset x y)) + (in e y))) + + +;;;; EXPORTED properties of susbet ;;;; + +(defthm subset-unite-reduction + (equal (subset (unite x y) z) + (and (subset x z) + (subset y z)))) + +(defthm subset-unite-property + (subset x (unite x y))) + +(defthm subset-isect-reduction + (equal (subset x (isect y z)) + (and (subset x y) + (subset x z)))) + +(defthm subset-isect-property + (subset (isect x y) x)) + +(defthm subset-sdiff-property + (subset (sdiff x y) x)) + +(defthm subset-is-reflexive + (subset x x)) + +(defthm subset-is-transitive + (implies (and (subset x y) + (subset y z)) + (subset x z))) + +(defthm subset-is-total-order + (implies (subset x y) + (equal (subset y x) + (equal x y)))) + +(defthm subset-card-property + (implies (subset x y) + (<= (card x) (card y)))) + +(defthm card<-reduce-when-subset + (implies (subset x y) + (equal (< (card x) (card y)) + (not (equal x y))))) + + +;;;; EXPORTED reductions of unite ;;;; + +(defthm unite-subset-property + (equal (equal (unite x y) y) + (subset x y))) + +(defthm unite-card-property + (equal (card (unite x y)) + (+ (card x) + (card (sdiff y x))))) + + +;;;; EXPORTED reductions of isect ;;;; + +(defthm isect-subset-property + (equal (equal (isect x y) x) + (subset x y))) + +(defthm isect-unite-distributes-1 + (equal (isect (unite x y) z) + (unite (isect x z) + (isect y z)))) + +(defthm isect-unite-distributes-2 + (equal (isect z (unite x y)) + (unite (isect x z) + (isect y z))) + :hints (("Goal" :in-theory (disable isect-aux-commutes) + :use (:instance isect-aux-commutes + (x (norm->set z)) + (y (unite-aux (norm->set x) + (norm->set y))))))) + +(defthm isect-sdiff-distributes-1 + (equal (isect (sdiff x y) z) + (sdiff (isect x z) y))) + +(defthm isect-sdiff-distributes-2 + (equal (isect z (sdiff x y)) + (sdiff (isect x z) y)) + :hints (("Goal" :in-theory (disable isect-aux-commutes) + :use (:instance isect-aux-commutes + (x (norm->set z)) + (y (sdiff-aux (norm->set x) + (norm->set y))))))) + + +;;;; EXPORTED reductions of sdiff ;;;; + +(defthm sdiff-subset-property + (iff (sdiff x y) + (not (subset x y)))) + +(defthm sdiff-card-property + (equal (card (sdiff x y)) + (- (card x) + (card (isect x y))))) + +(defthm sdiff-unite-distributes + (equal (sdiff (unite x y) z) + (unite (sdiff x z) + (sdiff y z)))) + +(defthm sdiff-unite-reduction + (equal (sdiff x (unite y z)) + (sdiff (sdiff x y) z))) + + +;;;; EXPORTED reductions of s1 ;;;; + +(defthm s1-membership-property + (equal (in a (s1 b)) + (equal a b))) + +(defthm s1-subset-property-1 + (equal (subset (s1 e) x) + (in e x))) + +(defthm s1-subset-property-2 + (implies (and (subset x (s1 e)) x) + (equal x (s1 e))) + :hints (("Goal" :use + (:instance norm->set-of-x-is-consp-or-not-x))) + :rule-classes :forward-chaining) + +(defthm s1-isect-property-1 + (equal (isect (s1 e) x) + (if (in e x) (s1 e) ()))) + +(defthm s1-isect-property-2 + (equal (isect x (s1 e)) + (if (in e x) (s1 e) ())) + :hints (("Goal" :in-theory (disable isect-aux-commutes) + :use (:instance isect-aux-commutes + (x (norm->set x)) + (y (list e)))))) + +(defthm s1-sdiff-property + (equal (sdiff (s1 e) x) + (if (in e x) () (s1 e)))) + +(defthm s1-card-property + (equal (card (s1 e)) 1)) + + +;;;; EXPORTED properties of empty-set ;;;; + +(defthm membership-empty-set + (not (in e (empty-set)))) + +(defthm empty-set-is-subset + (subset (empty-set) x)) + +(defthm empty-set-is-only-superset-self + (equal (subset x (empty-set)) + (not x))) + +(defthm unite-empty-set-property-1 + (equal (unite x (empty-set)) x)) + +(defthm unite-empty-set-property-2 + (equal (unite (empty-set) x) x)) + +(defthm isect-empty-set-property-1 + (equal (isect (empty-set) x) (empty-set))) + +(defthm isect-empty-set-property-2 + (equal (isect x (empty-set)) (empty-set))) + +(defthm sdiff-of-empty-set-1 + (equal (sdiff (empty-set) x) (empty-set))) + +(defthm sdiff-of-empty-set-2 + (equal (sdiff x (empty-set)) x)) + +(defthm s1-is-not-empty-set + (s1 e) + :hints (("Goal" :in-theory (enable set->norm))) + :rule-classes :type-prescription) + +(defthm card-of-empty-set + (iff (not x) + (equal (card x) 0)) + :hints (("Goal" :in-theory (enable norm->set))) + :rule-classes :type-prescription) + + +;;;; EXPORTED properties of scar ;;;; + +(defthm scar-membership-property + (iff (in (scar x) x) x)) + +(defthm scar-is-least-member + (implies (and (in e x) + (not (equal e (scar x)))) + (<< (scar x) e))) + +(defthm scar-returns-nil-for-empty-set + (equal (scar (empty-set)) nil)) + + +;; we now disable the top-level functions to keep their +;; definitions from being expanded + +(in-theory (disable in subset isect unite sdiff card s1 scar)) + +;; the following macro will enable/disable the executable-counterparts + +(defmacro ec-sets (x) + `(in-theory (,(if x 'enable 'disable) + (in) (subset) (isect) (unite) + (sdiff) (card) (s1) (scar)))) + +;; we will begin with the executable-counterparts disabled + +(ec-sets nil) |