summaryrefslogtreecommitdiff
path: root/books/workshops/2002/manolios-kaufmann/support
diff options
context:
space:
mode:
authorCamm Maguire <camm@debian.org>2017-05-08 12:58:52 -0400
committerCamm Maguire <camm@debian.org>2017-05-08 12:58:52 -0400
commit092176848cbfd27b96c323cc30c54dff4c4a6872 (patch)
tree91b91b4db76805fd2a09de0745b22080a9ebd335 /books/workshops/2002/manolios-kaufmann/support
Import acl2_7.4dfsg.orig.tar.gz
[dgit import orig acl2_7.4dfsg.orig.tar.gz]
Diffstat (limited to 'books/workshops/2002/manolios-kaufmann/support')
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify-original.lsp27
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify-total-ord-original.lsp5
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify-total-ord.lsp5
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify.lsp27
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory-original.acl224
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory-original.lisp3318
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory.acl224
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory.lisp3232
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/finite-set-theory/total-ordering-original.lisp267
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/finite-set-theory/total-ordering.lisp165
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/records/certify-original.lsp2
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/records/certify.lsp4
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/records/records-original.lisp380
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/records/records.lisp287
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/records/total-order.lisp28
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/sorting/certify.lsp10
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/sorting/insertion-sort.lisp104
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/sorting/perm-order.lisp39
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/sorting/perm.lisp107
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/sorting/quicksort.lisp107
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/sorting/total-order.lisp29
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/total-order/README11
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/total-order/cert_pl_exclude10
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/total-order/certify.lsp6
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/total-order/soundness.lisp205
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/total-order/total-order-easy-direction.lisp98
-rw-r--r--books/workshops/2002/manolios-kaufmann/support/total-order/total-order.lisp239
27 files changed, 8760 insertions, 0 deletions
diff --git a/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify-original.lsp b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify-original.lsp
new file mode 100644
index 0000000..bca7312
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify-original.lsp
@@ -0,0 +1,27 @@
+(lp)
+(in-package "ACL2")
+
+(certify-book "total-ordering-original" 0)
+:u
+
+(defpkg "S"
+ (set-difference-equal
+ (union-eq '(PACK
+ ORDINARYP
+ <<
+ <<-IRREFLEXIVITY
+ <<-TRICHOTOMY
+ <<-MUTUAL-EXCLUSION
+ <<-TRANSITIVITY
+ FAST-<<-TRICHOTOMY
+ FAST-<<-MUTUAL-EXCLUSION
+ FAST-<<-TRANSITIVITY
+ FAST-<<-RULES
+ SLOW-<<-RULES
+ <<-RULES)
+ (union-eq *acl2-exports*
+ *common-lisp-symbols-from-main-lisp-package*))
+ '(union intersection subsetp add-to-set functionp = apply)))
+
+(certify-book "set-theory-original" 1)
+:u :u
diff --git a/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify-total-ord-original.lsp b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify-total-ord-original.lsp
new file mode 100644
index 0000000..41a77ce
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify-total-ord-original.lsp
@@ -0,0 +1,5 @@
+(lp)
+(in-package "ACL2")
+
+(certify-book "total-ordering-original" 0)
+:u
diff --git a/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify-total-ord.lsp b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify-total-ord.lsp
new file mode 100644
index 0000000..8386126
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify-total-ord.lsp
@@ -0,0 +1,5 @@
+(lp)
+(in-package "ACL2")
+
+(certify-book "total-ordering" 0)
+:u
diff --git a/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify.lsp b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify.lsp
new file mode 100644
index 0000000..4d65db8
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify.lsp
@@ -0,0 +1,27 @@
+(lp)
+(in-package "ACL2")
+
+(certify-book "total-ordering" 0)
+:u
+
+(defpkg "S"
+ (set-difference-equal
+ (union-eq '(PACK
+ ORDINARYP
+ <<
+ <<-IRREFLEXIVITY
+ <<-TRICHOTOMY
+ <<-MUTUAL-EXCLUSION
+ <<-TRANSITIVITY
+ FAST-<<-TRICHOTOMY
+ FAST-<<-MUTUAL-EXCLUSION
+ FAST-<<-TRANSITIVITY
+ FAST-<<-RULES
+ SLOW-<<-RULES
+ <<-RULES)
+ (union-eq *acl2-exports*
+ *common-lisp-symbols-from-main-lisp-package*))
+ '(union intersection subsetp add-to-set functionp = apply)))
+
+(certify-book "set-theory" 1)
+:u :u
diff --git a/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory-original.acl2 b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory-original.acl2
new file mode 100644
index 0000000..b44f97f
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory-original.acl2
@@ -0,0 +1,24 @@
+(value :q)
+
+(LP)
+
+(defpkg "S"
+ (set-difference-equal
+ (union-eq '(PACK
+ ORDINARYP
+ <<
+ <<-IRREFLEXIVITY
+ <<-TRICHOTOMY
+ <<-MUTUAL-EXCLUSION
+ <<-TRANSITIVITY
+ FAST-<<-TRICHOTOMY
+ FAST-<<-MUTUAL-EXCLUSION
+ FAST-<<-TRANSITIVITY
+ FAST-<<-RULES
+ SLOW-<<-RULES
+ <<-RULES)
+ (union-eq *acl2-exports*
+ *common-lisp-symbols-from-main-lisp-package*))
+ '(union intersection subsetp add-to-set functionp = apply)))
+
+(certify-book "set-theory-original" ? t)
diff --git a/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory-original.lisp b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory-original.lisp
new file mode 100644
index 0000000..b710d78
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory-original.lisp
@@ -0,0 +1,3318 @@
+; Finite Set Theory for ACL2
+; Copyright (C) 2000 University of Texas at Austin
+
+; This program is free software; you can redistribute it and/or modify it under
+; the terms of Version 2 of the GNU General Public License as published by the
+; Free Software Foundation.
+
+; 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 License
+; along with this program; if not, write to the Free Software
+; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
+
+; Written by: J Strother Moore
+; email: Moore@cs.utexas.edu
+; Department of Computer Science
+; University of Texas at Austin
+; Austin, TX 78701 U.S.A.
+
+; The original kernel of this book was created with support from
+; Compaq Systems Research Center, Palo Alto, CA. A report documenting
+; the main ideas in this book is available from the ACL2 home page.
+; Visit the link "Papers about ACL2 and its Applications" and then
+; visit "Finite Set Theory".
+
+(in-package "S")
+
+(include-book "total-ordering-original")
+
+(defun standard-atom (x)
+ (or (acl2-numberp x)
+ (characterp x)
+ (stringp x)
+ (symbolp x)))
+
+(defthm standard-atom-type
+ (iff (standard-atom x)
+ (or (acl2-numberp x)
+ (characterp x)
+ (stringp x)
+ (symbolp x)))
+ :rule-classes :compound-recognizer)
+
+(in-theory (disable standard-atom))
+
+(defun ur-elementp (x)
+ (or (atom x)
+ (eq (car x) :UR-CONS)))
+
+; (defthm consp-ur-element
+; (implies (not (ur-elementp x))
+; (consp x))
+; :rule-classes :compound-recognizer)
+
+(defthm set-recursion
+ (and (implies (not (ur-elementp x))
+ (o< (acl2-count (cdr x)) (acl2-count x)))
+ (implies (not (ur-elementp x))
+ (o< (acl2-count (car x)) (acl2-count x))))
+ :rule-classes :built-in-clause)
+
+; (in-theory (disable ur-elementp))
+
+; Example objects are
+; 3 numbers
+; #\A characters
+; "Abc" strings
+; ABC symbols
+; (:UR-CONS (a b c)) lists
+; (1 2 1 3 (:UR-CONS (a b c))) sets
+
+; Some Comments on :UR-CONS
+
+; It is simplest never to write the symbol :UR-CONS in your sets
+; unless you mean to mark consp ur-elements. The symbol :UR-CONS if
+; encountered in unexpected places produces counter-intuitive results.
+
+; For example, (1 2 :UR-CONS) might be thought of as {1 2 :UR-CONS}
+; but in fact is {1 2}. The reason is that it is parsed as (1 2
+; . (:UR-CONS)). The enumeration of the elements of a set is
+; terminated by the first ur-element cdr. So just as (1 2 . 3) is {1
+; 2}, so is (1 2 . (:UR-CONS ...)). Any attempt to include :UR-CONS
+; as an element of an explicit set constant terminates the enumeration
+; of the set elements and so fails to include :UR-CONS as an element.
+
+; Is it possible to use scons to add :UR-CONS to a list? You might
+; expect (scons :UR-CONS '(1 2)) to be {:UR-CONS 1 2}. But it is in
+; fact {CONS 1 2}. If you ever succeed in using :UR-CONS as an
+; ur-element it is treated as though it were a non-canonical
+; representation of the symbol ACL2::CONS.
+
+; These considerations make it simplest to avoid using :UR-CONS except
+; in the syntax of sets.
+
+(defun set-insert (e s)
+
+; NIL is the only ur-elementp upon which set-insert is ever called, in
+; the process of canonicalizing. But I prove theorems about
+; set-insert and to make them simpler to state, I have it treat all
+; ur-elements s as the empty set. Also, both e and s are assumed to
+; be canonical.
+
+ (cond ((ur-elementp s) (cons e nil))
+ ((equal e (car s)) s)
+ ((<< e (car s))
+ (cons (car s)
+ (set-insert e (cdr s))))
+ (t (cons e s))))
+
+; Observe that if we encounter a non-standard atom we map it to a
+; character. Suppose we mapped it, instead, to a symbol, e.g.,
+; :NON-STANDARD-ATOM. Then = would not be a congruence for SYMBOLP.
+; For example, let x be a non-standard atom. Then (= x
+; :NON-STANDARD-ATOM). But (SYMBOLP x) is nil while (SYMBOLP
+; :NON-STANDARD-ATOM) is t. The moral of this story that if we
+; canonicalize non-standard atoms to objects of type type then type
+; will not admit = as a congruence. We figure that characters are the
+; least used primitive type.
+
+(defun o-fix (x)
+ (cond ((atom x)
+ (cond ((standard-atom x) x)
+ (t (code-char 255))))
+ (t (cons (o-fix (car x))
+ (o-fix (cdr x))))))
+
+(defthm ordinaryp-o-fix
+ (and (ordinaryp (o-fix x))
+ (implies (ordinaryp x) (equal (o-fix x) x))))
+
+(defun ur-fix (x)
+
+; This converts an arbitrary Lisp object into an ordinary ur-element
+; without changing the type. We do not want to change the type so
+; that set equality refines IFF and is a congruence relation for the
+; arithmetic primitives in ACL2. We discuss the conversions below.
+
+ (cond ((atom x)
+ (cond ((eq x :UR-CONS) 'ACL2::UR-CONS)
+ (t (o-fix x))))
+ ((eq (car x) :UR-CONS)
+ (cond ((or (atom (cdr x))
+ (atom (cadr x)))
+ '(:UR-CONS (NIL)))
+ (t (list :UR-CONS (o-fix (cadr x))))))
+ (t nil)))
+
+; Conversions:
+; (1) Make sure the output is ordinary, by using o-fix.
+; (2) If we encounter :UR-CONS where an ur-element is expected, we convert it
+; the symbol ACL2::UR-CONS. This prevents the accidental formation of
+; a :UR-CONS by set operations on data containing :UR-CONS. For example,
+; (scons :UR-CONS '(a b c)) will produce the set {ACL2::UR-CONS a b c}, not
+; the set {:UR-CONS a b c} and not the ``ur-element'' (:UR-CONS a b c).
+; (3) If we encounter (:UR-CONS . xxx) where an ur-element is expected, we
+; are sure to return something of the form (:UR-CONS (...)). An ur-element
+; marked :UR-CONS means a cons of some sort, no matter what is inside.
+; A rough model of the conversion rule is that if the :UR-CONS expression
+; is ill-formed it denotes (:UR-CONS (NIL)). More accurately, there are
+; three cases:
+; (a) (:UR-CONS . atom) => (:UR-CONS (NIL))
+; (b) (:UR-CONS atom . anything) => (:UR-CONS (NIL))
+; (c) (:UR-CONS (...) . anything) => (:UR-CONS (...))
+
+(defthm ordinaryp-ur-fix
+ (ordinaryp (ur-fix x)))
+
+; (in-theory (disable ur-fix))
+
+(defun canonicalize (x)
+ (cond ((ur-elementp x) (ur-fix x))
+ ((ur-elementp (cdr x))
+ (list (canonicalize (car x))))
+ (t (set-insert (canonicalize (car x))
+ (canonicalize (cdr x))))))
+
+(defthm ordinaryp-set-insert
+ (implies (and (ordinaryp e)
+ (ordinaryp x))
+ (ordinaryp (set-insert e x))))
+
+(defthm ordinaryp-canonicalize
+ (ordinaryp (canonicalize x)))
+
+(defun orderedp (x)
+ (cond ((ur-elementp x) t)
+ ((ur-elementp (cdr x)) t)
+ ((<< (cadr x) (car x))
+ (orderedp (cdr x)))
+ (t nil)))
+
+(defun canonicalp (x)
+ (cond ((atom x)
+ (and (not (eq x :UR-CONS))
+ (standard-atom x)))
+ ((eq (car x) :UR-CONS)
+ (and (consp (cdr x))
+ (consp (cadr x))
+ (ordinaryp (cadr x))
+ (equal (cddr x) nil)))
+ ((ur-elementp (cdr x))
+ (and (canonicalp (car x))
+ (equal (cdr x) nil)))
+ (t (and (canonicalp (car x))
+ (canonicalp (cdr x))
+ (orderedp x)))))
+
+(defthm canonicalp-ordinaryp
+ (implies (canonicalp x) (ordinaryp x)))
+
+(defthm orderedp-set-insert
+ (implies (and (canonicalp e)
+ (canonicalp a))
+ (orderedp (set-insert e a)))
+ :hints (("Goal" :induct (set-insert e a))))
+
+(defthm canonicalp-set-insert
+ (implies (and (canonicalp e)
+ (canonicalp a))
+ (canonicalp (set-insert e a)))
+ :hints (("Goal" :induct (set-insert e a))))
+
+(defthm o-fix-ur-cons
+ (equal (equal (o-fix x) :UR-CONS)
+ (equal x :UR-CONS)))
+
+(defthm consp-o-fix
+ (equal (consp (o-fix x))
+ (consp x)))
+
+(defthm canonicalp-ur-fix
+ (canonicalp (ur-fix X)))
+
+(defthm canonicalp-canonicalize
+ (canonicalp (canonicalize x)))
+
+(defthm canonicalize-canonicalp
+ (implies (canonicalp x) (equal (canonicalize x) x)))
+
+; So here is equality in our system.
+
+(defun = (x y)
+ (equal (canonicalize x)
+ (canonicalize y)))
+
+(defequiv =)
+
+; ----------------------------------------------------------------------------
+; The Set Constructor/Destructor Primitives
+
+; It is very convenient to pretend that sets are built as a new data
+; type. So here are the basic functions. I will keep them enabled
+; until I have proved the necessary facts about canonicalization,
+; equality (=) and subsetp. Then I'll disable them. But I introduce
+; them now so that mem and subsetp can be defined in terms of them. I
+; have also collected together certain of their elementary properties.
+; Most of these theorems are not used until after I have disabled
+; these primitives.
+
+(defun sfix (a)
+ (if (ur-elementp a)
+ nil
+ a))
+
+(defun scons (e a)
+ (if (equal e :UR-CONS)
+ (cons (canonicalize e)
+ (sfix a))
+ (cons e (sfix a))))
+
+; The macro below allows me to write (brace a b c) to mean {a, b, c}.
+
+(defmacro brace (&rest args)
+ (cond ((endp args) nil)
+ (t `(scons ,(car args)
+ (brace ,@(cdr args))))))
+
+; Here are some timings of this entire library. These timings started
+; when I began experimenting with three different flavors of scar and
+; scdr. The flavors are shown below along with some Caerlaverock
+; timings. I chose functionp1-set-insert as a representative expensive
+; proof.
+
+; When these timings were done, there were 279 events and the last one
+; was APPLY-RESTRICT. Since the book has probably changed since then,
+; these timings are only relevant insofar as they reflect the relative
+; effects of the various experiments. Even that claim is suspect:
+; since doing these timings I have discovered that there can be a
+; considerable difference (30%) between the time it takes in a fresh
+; GCL and the time it takes to ``repeat'' the computation in a soiled
+; GCL. Fresh GCL is faster. I did not record whether the times below
+; were done in fresh system or not.
+
+; During the first three experiments, I had the <<-rules -- namely <<,
+; transitivity, mutual-exclusion, and trichotomy -- disabled by
+; default and turned them on during certain proofs. They were on
+; during functionp1-set-insert, even though I eventually discovered
+; they didn't have to be for the proof to go through.
+
+; functionp1-set-insert entire file
+
+(defun scar (a)
+; (car a) ;;; 232 secs 1153 secs
+; (if (equal (car a) :UR-CONS) nil (car a)) ;;; 404 secs 1212 secs
+ (if (ur-elementp a) nil (car a)) ;;; 308 secs 1239 secs
+ )
+
+; I then learned that I did not have to have <<-rules enabled during
+; the functionp1-set-insert proof or the analogous ones. So I took out
+; those theory commands and got:
+
+; ;;; 2 secs 889 secs
+
+; Then I had the idea of coding up the ``fast << rules.'' Operating
+; in the fast-<<-rules theory by default and occasionally either
+; enabling << or switching over to the slow-<<-rules, I got the
+; following times in a fresh GCL:
+
+; ;;; 2 secs 370 secs
+
+
+(defun scdr (a)
+; (sfix (cdr a))
+; (if (equal (car a) :UR-CONS) nil (sfix (cdr a)))
+ (if (ur-elementp a) nil (sfix (cdr a)))
+ )
+
+(defcong = = (scons e a) 1
+ :hints (("Goal" :in-theory (enable =))))
+
+(defcong = = (scons e a) 2
+ :hints (("Goal" :in-theory (enable =))))
+
+(defthm scar-scons
+ (= (scar (scons e a)) e))
+
+(defthm scdr-scons
+ (= (scdr (scons e a)) (sfix a)))
+
+(defthm ur-elementp-scar
+ (implies (ur-elementp x) (equal (scar x) nil)))
+
+(defthm ur-elementp-scdr
+ (implies (ur-elementp x) (equal (scdr x) nil)))
+
+(defun setp (x)
+ (or (equal x nil)
+ (not (ur-elementp x))))
+
+(defthm setp-scdr
+ (setp (scdr a))
+ :rule-classes (:type-prescription :generalize))
+
+(defthm scons-scar-scdr
+ (implies (not (ur-elementp a))
+ (= (scons (scar a) (scdr a)) a))
+ :rule-classes :elim)
+
+(defthm acl2-count-scdr
+ (implies (not (ur-elementp a))
+ (o< (acl2-count (scdr a))
+ (acl2-count a)))
+ :rule-classes
+ ((:built-in-clause)
+ (:linear :corollary
+ (implies (not (ur-elementp a))
+ (< (acl2-count (scdr a))
+ (acl2-count a))))))
+
+(defthm consp-set-insert
+ (consp (set-insert e a))
+ :rule-classes :type-prescription)
+
+(defthm car-set-insert-not-equal-ur-cons
+ (implies (and (canonicalp e)
+ (canonicalp a))
+ (not (equal (set-insert e a) (cons :UR-CONS x)))))
+
+(defcong = equal (ur-elementp x) 1)
+
+; Note: We will generally keep sfix enabled, so this rule will not be
+; of much use.
+
+(defcong = = (sfix x) 1)
+
+(defthm not-ur-elementp-scons
+ (not (ur-elementp (scons e a))))
+
+(defthm not-consp-implies-ur-elementp
+ (implies (not (consp e))
+ (ur-elementp e)))
+
+(defthm scons-nil
+ (implies (and (syntaxp (not (equal a ''nil)))
+ (ur-elementp a))
+ (= (scons e a)
+ (scons e nil))))
+
+(defthm canonicalize-ur-cons
+ (not (equal (canonicalize x) :UR-CONS)))
+
+(defthm set-insert-set-insert
+ (implies (and (canonicalp e)
+ (canonicalp d)
+ (canonicalp a))
+ (equal (set-insert e (set-insert d a))
+ (set-insert d (set-insert e a))))
+ :hints (("Goal" :induct (set-insert e a)
+ :in-theory (slow-<<-rules))))
+
+; This rule lets us do a cross-fertilization without waiting for the
+; prior elim. The version of this rule that rewrites (set-insert e xxx)
+; to (set-insert d (set-insert e a)) has been known to cause infinite
+; loops, even with a hand-picked :loop-stopper.
+
+(defthm set-insert-short-cut
+ (implies (and (equal xxx (set-insert d a))
+ (canonicalp e)
+ (canonicalp d)
+ (canonicalp a))
+ (equal (equal (set-insert e xxx)
+ (set-insert d (set-insert e a)))
+ t)))
+
+(defthm set-insert-dup
+ (implies (and (canonicalp e)
+ (canonicalp a))
+ (equal (set-insert e (set-insert e a))
+ (set-insert e a)))
+ :hints (("Goal" :induct (set-insert e a))))
+
+(defthm scons-scons-2
+ (= (scons e (scons d a))
+ (scons d (scons e a))))
+
+(defthm scons-scons-1
+ (= (scons e (scons e a))
+ (scons e a)))
+
+(defthm equal-singleton-set-insert
+ (implies (and (canonicalp e)
+ (canonicalp d)
+ (canonicalp a))
+ (equal (equal (list e) (set-insert d a))
+ (and (equal e d)
+ (or (equal (sfix a) nil)
+ (equal (list e) a)))))
+ :hints (("Goal" :induct (set-insert d a))))
+
+(defthm car-set-insert
+ (implies (and (canonicalp e)
+ (canonicalp a))
+ (equal (car (set-insert e a))
+ (if (ur-elementp a)
+ e
+ (if (<< (car a) e)
+ e
+ (car a)))))
+ :hints (("Goal"
+ :induct (set-insert e a)
+ :in-theory (enable ur-elementp))))
+
+(defthm =-singletons
+ (equal (= (scons e nil) (scons d a))
+ (and (= e d)
+ (or (ur-elementp a)
+ (= (scons e nil) a))))
+ :hints (("Goal" :in-theory (enable = scons ur-elementp)))
+ :rule-classes
+ ((:rewrite)
+ (:rewrite :corollary
+ (equal (= (scons d a) (scons e nil))
+ (and (= e d)
+ (or (ur-elementp a)
+ (= (scons e nil) a))))
+
+; Note: This hint is required here because we do not know that
+; = is commutative (except by opening it up)!
+
+ :hints (("Goal" :in-theory (enable =))))))
+
+; Basic...
+(defun <<-cons-1-hint (x y)
+ (if (consp x)
+ (list (<<-cons-1-hint (car x) (cdr x)))
+ y))
+
+(defthm <<-cons-1
+ (implies (and (ordinaryp x)
+ (ordinaryp y))
+ (<< x (cons x y)))
+ :hints (("Goal" :induct (<<-cons-1-hint x y)
+ :in-theory (slow-<<-rules <<))))
+
+(defthm not-=-x-set-insert-x
+ (implies (and (canonicalp e)
+ (canonicalp x))
+ (not (equal e (set-insert e x))))
+ :hints (("Goal" :in-theory (cons 'ur-elementp
+ (slow-<<-rules)))))
+
+(defthm not-=-x-scons-x
+ (not (= e (scons e x)))
+ :hints (("Goal" :in-theory (enable = scons ur-elementp)))
+ :rule-classes
+ ((:rewrite)
+ (:rewrite :corollary (not (= (scons e x) e)))))
+
+; ----------------------------------------------------------------------------
+; Set Membership and the Subset Relation
+
+(defun mem (e a)
+ (cond ((ur-elementp a) nil)
+ (t (or (= e (scar a))
+ (mem e (scdr a))))))
+
+(defun subsetp (a b)
+ (cond ((ur-elementp a) t)
+ (t (and (mem (scar a) b)
+ (subsetp (scdr a) b)))))
+
+; I now prove that = is a congruence for both arguments of mem. The
+; proof for the first argument is easy because (mem e s) only uses
+; (canonicalize e). [So, if (canonicalize e) is (canonicalize e')
+; it is obvious that (mem e s) is (mem e' s).]
+
+; The proof for the second argument is harder and works this way. We
+; will establish that (mem e (canonicalize s)) is the same as (mem e
+; s). Suppose that is proved. Then suppose (= s s'). That is,
+; (canonicalize s) is (canonicalize s'). We must show that (mem e s)
+; is (mem e s'). Use the theorem to replace each by (mem e
+; (canonicalize s)) and (mem e (canonicalize s')), then substitute.
+
+; Even though I don't need it, I will prove the following for regularity.
+
+(defthm mem-canonicalize-1
+ (equal (mem (canonicalize e) a)
+ (mem e a)))
+
+; We need to little lemmas to do the second argument.
+
+; In the lemma below we must assume that the arguments to set-insert
+; are canonical. That is because it really compares using EQUAL.
+; When we use the lemma it will be on canonicalized arguments.
+
+(defthm mem-set-insert
+ (implies (and (canonicalp d)
+ (canonicalp a))
+ (equal (mem e (set-insert d a))
+ (or (= e d)
+ (mem e a))))
+ :hints (("Goal"
+ :induct (set-insert d a))))
+
+; Here is the second lemma.
+
+(defthm mem-canonicalize-2
+ (equal (mem e (canonicalize a))
+ (mem e a)))
+
+(defcong = equal (mem e a) 1)
+
+(defcong = equal (mem e a) 2
+ :hints (("Goal" :in-theory (disable mem-canonicalize-2)
+ :use ((:instance mem-canonicalize-2
+ (e e)
+ (a a))
+ (:instance mem-canonicalize-2
+ (e e)
+ (a a-equiv))))))
+
+
+; Now I repeat it for subsetp. The first argument of subsetp is the
+; harder, because we are recursing down it. The second argument is
+; easy and follows from what we already know about mem.
+
+(defthm subsetp-set-insert-1
+ (implies (and (canonicalp e)
+ (canonicalp a))
+ (equal (subsetp (set-insert e a) b)
+ (and (mem e b)
+ (subsetp a b))))
+ :hints (("Goal" :induct (set-insert e a))))
+
+(defthm subsetp-canonicalize-1
+ (equal (subsetp (canonicalize a) b)
+ (subsetp a b))
+ :hints (("Goal" :induct (subsetp a b))))
+
+(defcong = equal (subsetp a b) 1
+ :hints (("Goal"
+ :in-theory (disable subsetp-canonicalize-1)
+ :use ((:instance subsetp-canonicalize-1
+ (a a)
+ (b b))
+ (:instance subsetp-canonicalize-1
+ (a a-equiv)
+ (b b))))))
+
+(defcong = equal (subsetp a b) 2
+ :hints (("Goal" :in-theory (disable =))))
+
+; For regularity:
+
+(defthm subsetp-canonicalize-2
+ (equal (subsetp a (canonicalize b))
+ (subsetp a b)))
+
+; Next, I will prove the key facts about subsetp.
+
+(defthm subsetp-cons
+ (implies (and (not (equal e :UR-CONS))
+ (subsetp a b))
+ (subsetp a (cons e b))))
+
+(defthm subsetp-x-x
+ (subsetp x x))
+
+(in-theory (disable =))
+
+(defthm mem-subsetp
+ (implies (and (mem e a)
+ (subsetp a b))
+ (mem e b)))
+
+(defthm transitivity-of-subsetp
+ (implies (and (subsetp a b)
+ (subsetp b c))
+ (subsetp a c)))
+
+; ----------------------------------------------------------------------------
+; The Canonicality Theorem
+
+; Finally, I want to establish the key fact about equality and subset,
+; namely, that two sets are = iff they are subsets of eachother.
+
+; If (= a b), then it is obvious that (subsetp a b) and vice versa,
+; given the congruence rules above.
+
+; Suppose therefore that (subsetp a b) and (subsetp b a). We
+; prove (= a b). The proof relies on the fact that << is a total
+; ordering.
+
+; Proof. Let ca and cb be (canonicalize a) and (canonicalize b).
+; Observe that they are both ordinary. By the subsetp-canonicalize-i
+; lemmas we know that (subsetp ca cb) and (subsetp cb ca). We will
+; prove that (subsetp ca cb) implies (not (<< cb ca)). Thus,
+; ca equals cb. Q.E.D.
+
+(defthm =-is-equal
+ (implies (and (canonicalp x)
+ (canonicalp y))
+ (equal (= x y)
+ (equal x y)))
+ :hints (("Goal" :in-theory (enable =))))
+
+; I do not want to further encumber << with another rule. But this
+; is an important fact and I will :use it.
+
+(defthm mem-<<
+ (implies (and (canonicalp e)
+ (canonicalp a)
+ (mem e a))
+ (<< e a))
+ :rule-classes nil
+ :hints (("Goal" :in-theory (slow-<<-rules <<))))
+
+(defthm not-mem-e-e
+ (not (mem e e))
+ :hints (("Goal"
+ :use (:instance MEM-<<
+ (e (canonicalize e))
+ (a (canonicalize e))))))
+
+; This rule seems overly expensive so I keep it disabled most of the time.
+
+(defthm mem-container
+ (implies (mem e a)
+ (not (mem a e)))
+ :hints (("Goal"
+ :use ((:instance mem-<<
+ (e (canonicalize e))
+ (a (canonicalize a)))
+ (:instance mem-<<
+ (a (canonicalize e))
+ (e (canonicalize a)))))))
+
+(in-theory (disable mem-container))
+
+(defthm mem-implies-not-<<-car
+ (implies (and (canonicalp e)
+ (canonicalp a)
+ (mem e a))
+ (not (<< (car a) e)))
+ :hints (("Goal" :in-theory (slow-<<-rules <<))))
+
+(defthm <<-cons
+ (implies (and (canonicalp e)
+ (canonicalp a)
+ (mem e a))
+ (equal (<< a (cons e z))
+ (if (equal (car a) e)
+ (<< (cdr a) z)
+ nil)))
+ :hints (("Goal" :in-theory (enable <<) ; (fast-<<-rules <<)
+ )))
+
+(defthm subsetp-cons-reversed
+ (implies (and (subsetp a (cons e b))
+ (not (equal e :UR-CONS))
+ (not (mem e a)))
+ (subsetp a b)))
+
+(defthm yucko
+ (implies (and (canonicalp a)
+ (canonicalp b)
+ (subsetp a b)
+ (mem (car b) a))
+ (equal (car a) (car b)))
+ :rule-classes nil
+ :hints (("Goal"
+ :use ((:instance <<-trichotomy
+ (acl2::x (car a))
+ (acl2::y (car b)))))))
+
+(defthm subsetp-<<
+ (implies (and (setp a)
+ (setp b)
+ (canonicalp a)
+ (canonicalp b)
+ (subsetp a b))
+ (not (<< b a)))
+ :rule-classes nil
+ :hints (("Goal" :induct (<< b a))
+ ("Subgoal *1/24.3"
+ :use (:instance yucko
+ (a (cdr a))
+ (b b)))
+ ("Subgoal *1/22'''" :in-theory (enable <<) ; (fast-<<-rules <<)
+ )))
+
+(defthm setp-canonicalize
+ (implies (setp x)
+ (setp (canonicalize x))))
+
+; The Canonalicality Theorem:
+(defthm =-iff-subsetps
+ (implies (and (setp a)
+ (setp b))
+ (iff (= a b)
+ (and (subsetp a b)
+ (subsetp b a))))
+ :rule-classes nil
+ :hints
+ (("Goal"
+ :in-theory (union-theories '(=)
+ (disable subsetp-canonicalize-1
+ subsetp-canonicalize-2
+ canonicalize
+ setp
+ transitivity-of-subsetp))
+
+ :use ((:instance subsetp-canonicalize-1
+ (a a)
+ (b b))
+ (:instance subsetp-canonicalize-2
+ (a (canonicalize a))
+ (b b))
+ (:instance subsetp-canonicalize-1
+ (a b)
+ (b a))
+ (:instance subsetp-canonicalize-2
+ (a (canonicalize b))
+ (b a))
+ (:instance subsetp-<<
+ (a (canonicalize a))
+ (b (canonicalize b)))
+ (:instance subsetp-<<
+ (a (canonicalize b))
+ (b (canonicalize a)))))))
+
+; Now we disable those of the above rules that we don't think are
+; worth their cost.
+
+(in-theory (disable =-is-equal
+ mem-implies-not-<<-car
+ <<-cons))
+
+;----------------------------------------------------------------------------
+; = Refines iff and is a Congruence for Many ACL2 Functions
+
+(defthm standard-atom-set-insert
+ (not (standard-atom (set-insert e a))))
+
+(defthm standard-atom-canonicalize
+ (equal (standard-atom (canonicalize x))
+ (atom x)))
+
+(defcong = equal (canonicalize x) 1
+ :hints (("Goal" :in-theory (enable =))))
+
+(defthm canonicalize-=
+ (= (canonicalize x) x)
+ :hints (("Goal" :in-theory (enable =))))
+
+(defthm canonicalize-non-nil
+ (iff (canonicalize x) x)
+ :hints (("Goal" :in-theory (enable ur-elementp))))
+
+(defrefinement = iff
+ :hints (("Goal" :in-theory (enable =))))
+
+(defthm canonicalize-fix
+ (equal (canonicalize (fix x))
+ (fix (canonicalize x)))
+ :rule-classes nil
+ :hints (("Goal" :in-theory (enable ur-elementp))))
+
+(defthm <-fixes
+ (equal (< x y) (< (fix x) (fix y)))
+ :rule-classes nil)
+
+(defcong = equal (< x y) 1
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =) '(fix))
+ :use ((:instance <-fixes
+ (x x)
+ (y y))
+ (:instance <-fixes
+ (x x-equiv)
+ (y y))
+ (:instance canonicalize-fix
+ (x x))
+ (:instance canonicalize-fix
+ (x x-equiv))))))
+
+(defcong = equal (< x y) 2
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =) '(fix))
+ :use ((:instance <-fixes
+ (x x)
+ (y y))
+ (:instance <-fixes
+ (x x)
+ (y y-equiv))
+ (:instance canonicalize-fix
+ (x y))
+ (:instance canonicalize-fix
+ (x y-equiv))))))
+
+(defthm +-fixes
+ (equal (+ x y) (+ (fix x) (fix y)))
+ :rule-classes nil)
+
+(defcong = equal (+ x y) 1
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =) '(fix))
+ :use ((:instance +-fixes
+ (x x)
+ (y y))
+ (:instance +-fixes
+ (x x-equiv)
+ (y y))
+ (:instance canonicalize-fix
+ (x x))
+ (:instance canonicalize-fix
+ (x x-equiv))))))
+
+(defcong = equal (+ x y) 2
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =) '(fix))
+ :use ((:instance +-fixes
+ (x x)
+ (y y))
+ (:instance +-fixes
+ (x x)
+ (y y-equiv))
+ (:instance canonicalize-fix
+ (x y))
+ (:instance canonicalize-fix
+ (x y-equiv))))))
+
+(defthm --fixes
+ (equal (- x) (- (fix x)))
+ :rule-classes nil)
+
+(defcong = equal (- x) 1
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =) '(fix))
+ :use ((:instance --fixes
+ (x x))
+ (:instance --fixes
+ (x x-equiv))
+ (:instance canonicalize-fix
+ (x x))
+ (:instance canonicalize-fix
+ (x x-equiv))))))
+
+
+(defthm *-fixes
+ (equal (* x y) (* (fix x) (fix y)))
+ :rule-classes nil)
+
+(defcong = equal (* x y) 1
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =) '(fix))
+ :use ((:instance *-fixes
+ (x x)
+ (y y))
+ (:instance *-fixes
+ (x x-equiv)
+ (y y))
+ (:instance canonicalize-fix
+ (x x))
+ (:instance canonicalize-fix
+ (x x-equiv))))))
+
+(defcong = equal (* x y) 2
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =) '(fix))
+ :use ((:instance *-fixes
+ (x x)
+ (y y))
+ (:instance *-fixes
+ (x x)
+ (y y-equiv))
+ (:instance canonicalize-fix
+ (x y))
+ (:instance canonicalize-fix
+ (x y-equiv))))))
+
+(defthm integerp-canonicalize
+ (equal (integerp (canonicalize x))
+ (integerp x)))
+
+(defthm rationalp-canonicalize
+ (equal (rationalp (canonicalize x))
+ (rationalp x)))
+
+(defthm symbolp-canonicalize
+ (equal (symbolp (canonicalize x))
+ (symbolp x))
+ :hints (("Goal" :in-theory (enable ur-elementp))))
+
+(defthm stringp-canonicalize
+ (equal (stringp (canonicalize x))
+ (stringp x)))
+
+(defthm characterp-canonicalize
+ (equal (characterp (canonicalize x))
+ (or (characterp x)
+ (and (atom x)
+ (not (standard-atom x)))))
+ :hints (("Goal" :in-theory (enable ur-elementp))))
+
+(defthm consp-canonicalize
+ (equal (consp (canonicalize x))
+ (consp x))
+ :hints (("Goal" :in-theory (enable ur-elementp))))
+
+(defcong = equal (integerp x) 1
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =)
+ '(integerp-canonicalize))
+ :use ((:instance integerp-canonicalize
+ (x x))
+ (:instance integerp-canonicalize
+ (x x-equiv))))))
+
+(defcong = equal (rationalp x) 1
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =)
+ '(rationalp-canonicalize))
+ :use ((:instance rationalp-canonicalize
+ (x x))
+ (:instance rationalp-canonicalize
+ (x x-equiv))))))
+
+(defcong = equal (symbolp x) 1
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =)
+ '(symbolp-canonicalize))
+ :use ((:instance symbolp-canonicalize
+ (x x))
+ (:instance symbolp-canonicalize
+ (x x-equiv))))))
+
+(defcong = equal (stringp x) 1
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =)
+ '(stringp-canonicalize))
+ :use ((:instance stringp-canonicalize
+ (x x))
+ (:instance stringp-canonicalize
+ (x x-equiv))))))
+
+(defcong = equal (consp x) 1
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =)
+ '(consp-canonicalize))
+ :use ((:instance consp-canonicalize
+ (x x))
+ (:instance consp-canonicalize
+ (x x-equiv))))))
+
+
+; We do not get (defcong = equal (characterp x) 1) because we
+; canonicalize non-standard atoms to (code-char 255).
+
+; ----------------------------------------------------------------------------
+; Codified Theorem Proving Strategies
+
+; The following all turn into the corresponding defthms:
+; (defx name term)
+; (defx name term :hints ... :rule-classes ...)
+
+; But if you write
+; (defx ...a... :strategy xxx ...b...)
+; it macro expands to
+; (xxx ...a... ...b...)
+
+; Thus, if you want to codify a new theorem proving strategy xxx, you can
+; defmacro xxx and then write (defx ... :strategy xxx ...).
+
+; The main point of this is to let me write defx events and introduce
+; new strategies as I go. Also, I can name my strategies without
+; including ``def'' in front of them and still search for ``(def...''
+; when looking for things.
+
+(defun packn-in-pkg (lst pkg-witness)
+ (declare (xargs :mode :program))
+ (acl2::intern-in-package-of-symbol (coerce (acl2::packn1 lst) 'string)
+ pkg-witness))
+
+(defmacro defx (&rest args)
+ (let ((temp (member :strategy args)))
+
+; We allow the strategy to be a keyword, in which case we convert it
+; to the corresponding symbol in this package. If the strategy is not
+; a keyword, it is used as supplied.
+
+ (cond
+ (temp
+ `(,(if (keywordp (cadr temp))
+ (packn-in-pkg (list (symbol-name (cadr temp))) 'defx)
+ (cadr temp))
+ ,@(butlast args (length temp))
+ ,@(cddr temp)))
+ (t `(defthm ,@args)))))
+
+; ----------------------------------------------------------------------------
+; Proving Congruences
+
+; There are two common ways to prove congruence rules in this theory.
+
+; (1) The :canonicalize strategy: prove that (fn (canonicalize x)) is
+; (fn x). This is generally used if fn returns an ur-element (as
+; opposed to a set).
+
+; (2) The :subsetp stragegy: prove that (subsetp a1 a2) implies
+; (subsetp (fn a1) (fn a2)). This is generally used if fn returns a
+; set.
+
+(defun genname1 (name n avoid)
+ (declare (xargs :mode :program))
+ (let ((new-name (packn-in-pkg (list name n) name)))
+ (cond ((acl2::member-equal new-name avoid)
+ (genname1 name (+ 1 n) avoid))
+ (t new-name))))
+
+(defun genname (name avoid)
+ (declare (xargs :mode :program))
+ (cond ((acl2::member-equal name avoid)
+ (genname1 name 1 avoid))
+ (t name)))
+
+(defun put-nth (e n lst)
+ (cond ((zp n) (cons e (cdr lst)))
+ (t (cons (car lst) (put-nth e (- n 1) (cdr lst))))))
+
+; And here is the macro
+
+(defmacro congruence (expr n &key method)
+ (cond
+ ((eq method :canonicalize)
+ (let* ((fn (car expr))
+ (vars (cdr expr))
+ (x (nth (- n 1) vars))
+ (name1
+ (packn-in-pkg (list fn "-SET-INSERT") fn))
+ (name2
+ (packn-in-pkg (list fn "-CANONICALIZE") fn))
+ (vars1 (acl2::remove1-eq x vars)) ; Matt K. mod from delete1-eq, v2-9-4
+ (e (genname 'e vars1))
+ (a (genname x vars1))
+ (x-equiv (packn-in-pkg (list x "-EQUIV") x)))
+ `(encapsulate
+ nil
+ (local (in-theory (enable scons scar scdr ur-elementp)))
+
+ (defthm ,name1
+ (implies (and (canonicalp ,e)
+ (canonicalp ,a))
+ (equal (,fn ,@(put-nth `(set-insert ,e ,a)
+ (- n 1)
+ vars))
+ (,fn ,@(put-nth `(cons ,e ,a)
+ (- n 1)
+ vars))))
+ :hints (("Goal"
+ :induct (set-insert ,e ,a)
+
+; Note that the following in-theory is commented out! I learned that
+; if you enable = during these proofs it is generally slower. So I
+; don't.
+; :in-theory (enable =)
+
+
+ )))
+
+ (defthm ,name2
+ (equal (,fn ,@(put-nth `(canonicalize ,x)
+ (- n 1)
+ vars))
+ (,fn ,@vars)))
+
+ (defcong = equal ,expr ,n
+ :hints
+ (("Goal"
+ :in-theory (disable ,name2)
+ :use ((:instance ,name2 (,x ,x))
+ (:instance ,name2
+ (,x ,x-equiv)))))))))
+ ((eq method :subsetp)
+ (let* ((fn (car expr))
+ (vars (cdr expr))
+ (x (nth (- n 1) vars))
+ (name1
+ (packn-in-pkg (list "SUBSETP-" fn "-" fn) fn))
+ (vars1 (acl2::remove1-eq x vars)) ; Matt K. mod from delete1-eq, v2-9-4
+ (a1 (genname1 x 1 vars1))
+ (a2 (genname1 x 2 (cons a1 vars1)))
+ (x-equiv (packn-in-pkg (list x "-EQUIV") x)))
+ `(encapsulate
+ nil
+ (defthm ,name1
+ (implies (subsetp ,a1 ,a2)
+ (subsetp (,fn ,@(put-nth a1 (- n 1) vars))
+ (,fn ,@(put-nth a2 (- n 1) vars)))))
+
+ (defcong = = ,expr ,n
+ :hints (("Goal"
+ :use (:instance =-iff-subsetps
+ (a ,expr)
+ (b (,fn ,@(put-nth x-equiv
+ (- n 1)
+ vars))))))))))
+ ((eq method nil)
+ `(defcong = = ,expr ,n))
+ (t `(acl2::er acl2::soft 'congruence
+ "The :method ~x0 is unknown."
+ ',method))))
+
+; ----------------------------------------------------------------------------
+; The User Level Theory
+
+(in-theory (disable scons scar scdr ur-elementp))
+
+; ----------------------------------------------------------------------------
+; Set Union
+
+(defun union (a b)
+ (if (ur-elementp a)
+ (sfix b)
+ (scons (scar a)
+ (union (scdr a) b))))
+
+; My next goal is to prove both
+
+; (defcong = = (union a b) 1)
+; (defcong = = (union a b) 2)
+
+; The first of these is problematic but the second is easy.
+; Generally, if the congruence rule is in a slot that is held fixed in
+; the recursion (as in the second case above), the proof is an easy
+; induction, using congruence rules for the subfunctions. But if the
+; congruence rule is in a controller slot, you generally need lemmas.
+
+(defthm mem-union
+ (equal (mem e (union a b))
+ (or (mem e a)
+ (mem e b))))
+
+(defthm subsetp-scons
+ (implies (subsetp a b)
+ (subsetp a (scons e b))))
+
+(defthm subsetp-union-1
+ (subsetp a (union a b)))
+
+(defthm subsetp-union-2
+ (subsetp a (union b a)))
+
+(defthm subsetp-union
+ (implies (subsetp a1 a2)
+ (subsetp (union a1 b)
+ (union a2 b))))
+(defthm setp-union
+ (setp (union a b)))
+
+(defx :strategy :congruence (union a b) 1 :method :subsetp)
+
+(defx :strategy :congruence (union a b) 2)
+
+(defthm union-right-id
+ (implies (ur-elementp b)
+ (= (union a b) (sfix a))))
+
+(defthm union-scons
+ (= (union a (scons e b))
+ (scons e (union a b))))
+
+(defthm commutativity-of-union
+ (= (union a b) (union b a)))
+
+(defthm ur-elementp-union
+ (equal (ur-elementp (union a b))
+ (and (ur-elementp a)
+ (ur-elementp b))))
+
+(defthm associativity-of-union
+ (= (union (union a b) c)
+ (union a (union b c))))
+
+
+; ----------------------------------------------------------------------------
+; Set Intersection
+
+(defun intersection (a b)
+ (if (ur-elementp a)
+ nil
+ (if (mem (scar a) b)
+ (scons (scar a)
+ (intersection (scdr a) b))
+ (intersection (scdr a) b))))
+
+(defthm mem-intersection
+ (equal (mem e (intersection a b))
+ (and (mem e a)
+ (mem e b))))
+
+(defthm subsetp-intersection-1
+ (subsetp (intersection a b) a))
+
+(defthm subsetp-intersection-2
+ (subsetp (intersection b a) a))
+
+(defthm subsetp-intersection
+ (implies (subsetp a1 a2)
+ (subsetp (intersection a1 b)
+ (intersection a2 b))))
+
+(defthm setp-intersection
+ (setp (intersection a b)))
+
+(defx :strategy :congruence (intersection a b) 1 :method :subsetp)
+(defx :strategy :congruence (intersection a b) 2)
+
+(defthm intersection-right-id
+ (implies (ur-elementp b)
+ (= (intersection a b) nil)))
+
+(defthm scons-id
+ (implies (mem e a)
+ (= (scons e a) a)))
+
+(defthm intersection-scons
+ (= (intersection a (scons e b))
+ (if (mem e a)
+ (scons e (intersection a b))
+ (intersection a b))))
+
+(defthm commutativity-of-intersection
+ (= (intersection a b) (intersection b a)))
+
+(defthm associativity-of-intersection
+ (= (intersection (intersection a b) c)
+ (intersection a (intersection b c))))
+
+; ----------------------------------------------------------------------------
+; Arithmetic
+
+(include-book "../../../../../arithmetic/top-with-meta")
+
+(defun cardinality (a)
+ (if (ur-elementp a)
+ 0
+ (if (mem (scar a) (scdr a))
+ (cardinality (scdr a))
+ (+ 1 (cardinality (scdr a))))))
+
+(defx :strategy :congruence (cardinality a) 1 :method :canonicalize)
+
+(defthm cardinality-union-2
+ (<= (cardinality b) (cardinality (union a b)))
+ :rule-classes :linear)
+
+; Observe that we proved the easy case first, by induction on b,
+; and then we prove the other case by commutativity.
+
+(defthm cardinality-union-1
+ (<= (cardinality b) (cardinality (union b a)))
+ :rule-classes :linear)
+
+(defthm cardinality-union-3
+ (<= (cardinality (union a b))
+ (+ (cardinality a)
+ (cardinality b)))
+ :rule-classes :linear)
+
+(defthm cardinality-0
+ (equal (equal (cardinality a) 0)
+ (ur-elementp a)))
+
+(defthm cardinality-non-0
+ (implies (mem e x)
+ (< 0 (cardinality x)))
+ :rule-classes :linear)
+
+(defthm cardinality-intersection-1
+ (<= (cardinality (intersection a b)) (cardinality a))
+ :rule-classes :linear)
+
+(defthm cardinality-intersection-2
+ (<= (cardinality (intersection b a)) (cardinality a))
+ :rule-classes :linear)
+
+(defthm cardinality-scons
+ (equal (cardinality (scons e a))
+ (if (mem e a)
+ (cardinality a)
+ (+ 1 (cardinality a)))))
+
+(defthm cardinality-disjoint-union
+ (implies (not (intersection a b))
+ (= (cardinality (union a b))
+ (+ (cardinality a)
+ (cardinality b)))))
+
+
+; ----------------------------------------------------------------------------
+; Choose
+
+(defun choose (a)
+ (car (sfix (canonicalize a))))
+
+(defx :strategy :congruence (choose a) 1)
+
+(defthm ur-elementp-canonicalize
+ (equal (ur-elementp (canonicalize x))
+ (ur-elementp x))
+ :hints (("Goal" :in-theory (enable ur-elementp))))
+
+(defthm mem-choose-lemma
+ (equal (mem (car (canonicalize a)) a)
+ (not (ur-elementp a)))
+ :hints (("Goal"
+ :in-theory (enable scar scdr ur-elementp))))
+
+(defthm mem-choose
+ (equal (mem (choose a) a)
+ (not (ur-elementp a))))
+
+; One might think that the following follows from the previous
+; theorems about choose. But that is not correct. For example,
+; (choose {1 2 3}) might be 2 but (choose {2 3}) might be 3. This
+; property is due to the fact that choose is really the biggest
+; element of the set.
+
+(defthm car-canonicalize-ur-cons
+ (equal (equal (car (canonicalize a)) :UR-CONS)
+ (and (consp a)
+ (equal (car a) :UR-CONS)))
+ :hints (("Goal" :in-theory (enable ur-elementp))))
+
+(defthm choose-scons
+ (implies (not (= (choose (scons e a)) e))
+ (= (choose (scons e a)) (choose a)))
+ :hints (("Goal"
+ :in-theory
+ (enable = scons ur-elementp))))
+
+(defthm choose-singleton
+ (= (choose (scons e nil)) e)
+ :hints (("Goal" :in-theory (enable = scons ur-elementp))))
+
+(in-theory (disable choose))
+
+(defthm elim-choose-singleton
+ (implies (equal (cardinality x) 1)
+ (= (scons (choose x) nil) x)))
+
+(defthm mem-singleton
+ (implies (and (equal (cardinality x) 1)
+ (mem e x))
+ (= (scons e nil) x))
+ :rule-classes nil
+ :hints (("Goal" :in-theory (disable elim-choose-singleton)
+ :use elim-choose-singleton)))
+
+(defthm choose-ur-elementp
+ (implies (ur-elementp x)
+ (= (choose x) nil))
+ :hints (("Goal" :in-theory (enable choose ur-elementp sfix))))
+
+
+; ----------------------------------------------------------------------------
+; Set Difference
+
+(defun diff (a b)
+ (cond ((ur-elementp a)
+ nil)
+ ((mem (scar a) b)
+ (diff (scdr a) b))
+ (t (scons (scar a)
+ (diff (scdr a) b)))))
+
+(defthm mem-diff
+ (equal (mem e (diff a b))
+ (and (mem e a)
+ (not (mem e b)))))
+
+(defthm subsetp-diff-1
+ (subsetp (diff a b) a))
+
+(defthm subsetp-diff
+ (implies (subsetp a1 a2)
+ (subsetp (diff a1 b)
+ (diff a2 b))))
+
+(defthm setp-diff
+ (setp (diff a b)))
+
+(defx :strategy :congruence (diff a b) 1 :method :subsetp)
+(defx :strategy :congruence (diff a b) 2)
+
+(defthm diff-right-id
+ (implies (ur-elementp b)
+ (= (diff a b) (sfix a))))
+
+(defthm cardinality-diff-singleton
+ (equal (cardinality (diff y (scons x nil)))
+ (if (mem x y)
+ (- (cardinality y) 1)
+ (cardinality y))))
+
+(defthm cardinality-diff
+ (<= (cardinality (diff a b)) (cardinality a))
+ :rule-classes :linear)
+
+(defthm diff-nil
+ (implies (subsetp x y)
+ (= (diff x y) nil)))
+
+(defthm diff-scons
+ (implies (not (mem e s))
+ (= (diff s (scons e y)) (diff s y))))
+
+(encapsulate nil
+ (local
+ (defthm scons-x-diff-x
+ (implies (mem x s)
+ (= (scons x (diff s (scons x nil))) s))
+ :hints (("Subgoal *1/3'5'"
+ :cases ((mem sr sr0))))))
+
+ (defthm scons-diff-scons
+ (= (scons e (diff a (scons e nil)))
+ (scons e a))
+ :hints (("Goal" :cases ((mem e a))))))
+
+(defthm elim-choose-doubleton
+ (implies (equal (cardinality x) 2)
+ (= (scons (choose x)
+ (scons (choose (diff x (scons (choose x) nil)))
+ nil))
+ x)))
+
+(defthm subsetp-diff-1-corrollary
+ (implies (subsetp a b)
+ (subsetp (diff a c) b)))
+
+(defthm subsetp-not-subsetp-trick
+ (implies (and (subsetp a b)
+ (not (subsetp a (scdr b))))
+ (mem (scar b) a)))
+
+(defthm intersection-diff-2
+ (= (intersection a (diff b c))
+ (diff (intersection a b) c)))
+
+(defthm intersection-diff-1
+ (= (intersection (diff b c) a)
+ (diff (intersection a b) c)))
+
+; There are others, but I am not going to prove them now.
+
+; ----------------------------------------------------------------------------
+; Ordered Pairs as Sets
+
+; It is possible to provide ordered pairs as ur-elements. For example
+; we could define (pair x y) to be (list :UR-CONS (cons x y)). But here
+; we develop the classical treatment of ordered pairs.
+
+(defun pair (x y)
+ (brace x (brace x y)))
+
+; Observe that a pair necessarily has cardinality 2. But the larger
+; element need not have cardinality 2. For example, (pair x x) is
+; {x {x}}.
+
+; We must be able to determine whether a set of cardinality 2 is a
+; pair. Call the two elements x and y. Then either (mem x y) or (mem
+; y x). Furthermore, the larger must be of cardinality 2 or less. To
+; code this up, we have to have a way of finding ``the two elements''
+; of a set, a, of cardinality 2, when a is not necessarily in
+; canonical form. E.g., (1 (1 2)) is a pair but so is (1 1 (2 1) (1
+; 2)). At first, I wanted to avoid canonicalizing the set, for
+; efficiency reasons.
+
+; Here was my first attempt to extract ``the other'' element of a
+; set of cardinality 2.
+
+; (defun find-other (e s)
+; ; Find the first element of s that is not e.
+; (cond ((ur-elementp s) nil)
+; ((= e (scar s)) (find-other e (scdr s)))
+; (t (scar s))))
+
+; Unfortunately, this function does not admit = as a congruence in
+; the second argument. For example (find-other 1 '(1 2 3)) and
+; (find-other 1 '(1 3 2)) return different things, even though their
+; arguments are =. (It would admit it if we limited s to sets of
+; cardinality 2, but we can't.)
+
+; So I have decided simply use the classical approach in terms of
+; choose. If the first element of a pair is a number, this is not too
+; expensive.
+
+(defun pairp (a)
+ (if (equal (cardinality a) 2)
+ (let* ((x (choose a))
+ (y (choose (diff a (brace x)))))
+ (or (and (mem x y)
+ (<= (cardinality y) 2))
+ (and (mem y x)
+ (<= (cardinality x) 2))))
+ nil))
+
+(defun hd (a)
+ (cond ((pairp a)
+ (let* ((x (choose a))
+ (y (choose (diff a (brace x)))))
+ (if (mem x y)
+ x
+ y)))
+ (t nil)))
+
+(defun tl (a)
+ (cond ((pairp a)
+ (let* ((x (choose a))
+ (y (choose (diff a (brace x)))))
+ (if (mem x y)
+ (if (equal (cardinality y) 1)
+ x
+ (choose (diff y (brace x))))
+ (if (equal (cardinality x) 1)
+ y
+ (choose (diff x (brace y)))))))
+ (t nil)))
+
+(defthm setp-pair
+ (setp (pair x y)))
+
+(defcong = = (pair a b) 1)
+(defcong = = (pair a b) 2)
+(defcong = equal (pairp a) 1)
+(defcong = = (hd a) 1)
+(defcong = = (tl a) 1)
+
+(in-theory (enable mem-container))
+
+(defthm hd-pair
+ (= (hd (pair x y)) x))
+
+(defthm tl-pair
+ (= (tl (pair x y)) y))
+
+(defthm pairp-pair
+ (pairp (pair x y))
+ :rule-classes (:type-prescription :generalize))
+
+(defthm pairp-implies-setp
+ (implies (pairp x) (setp x)))
+
+(encapsulate
+ nil
+
+; Our goal here is to prove
+
+; (implies (pairp a)
+; (= (pair (hd a) (tl a)) a))
+
+; We have to give the proof pretty explicitly. It exploits the fact
+; that we know how to represent singleton and doubleton sets in terms
+; of choose. Since we have to use these lemmas explicitly, we disable
+; them.
+
+ (local (in-theory (disable elim-choose-doubleton
+ elim-choose-singleton)))
+
+; To make the proof easier to understand, we give names to certain
+; expressions. In the definitions of pair, hd and tl, we use two
+; local variables,
+
+; (let* ((x (choose a))
+; (y (choose (diff a (brace x)))))
+; ...)
+
+; Here we define functions corresponding to their values.
+
+ (local (defun x (a) (choose a)))
+ (local (defun y (a) (choose (diff a (brace (x a))))))
+
+; Given that a is known to be a pairp, there are four cases, depending
+; on which of x and y is an element of the other and whether the
+; cardinality of the bigger is 1 or 2. We will prove the main goal
+; for each of the four cases.
+
+ (local
+ (defthm case-1
+ (implies (and (mem (x a) (y a))
+ (equal (cardinality (y a)) 2)
+ (pairp A))
+ (= (pair (hd A) (tl A)) A))
+ :hints
+ (("Goal"
+ :use
+ (
+
+; Proof of Case 1:
+
+; (i) Represent A as a doubleton in terms of choose.
+
+ (:instance elim-choose-doubleton (x A))
+
+; (ii) Represent y as a doubleton.
+
+ (:instance elim-choose-doubleton (x (y a)))
+
+; (iii) When x is removed from y, the result is a singleton, which can
+; be represented with choose.
+
+ (:instance elim-choose-singleton
+ (x (diff (y a) (scons (x a) nil))))
+
+; (iv) If x is a member of a singleton set, the set is {x}.
+
+ (:instance mem-singleton
+ (e (x a))
+ (x (diff (y a) (scons (x a) nil)))))))))
+
+ (local
+ (defthm case-2
+ (implies (and (mem (x a) (y a))
+ (equal (cardinality (y a)) 1)
+ (pairp A))
+ (= (pair (hd A) (tl A)) A))
+ :hints
+ (("Goal"
+ :use
+ (
+
+; Proof of Case 2:
+
+; (i) Represent A as a doubleton in terms of choose.
+
+ (:instance elim-choose-doubleton (x A))
+
+; (ii) Represent y as a singleton.
+
+ (:instance elim-choose-singleton (x (y a)))
+
+; (iii) If x is a member of singleton set, the set is {x}.
+
+ (:instance mem-singleton
+ (e (x a))
+ (x (y a))))))))
+
+; Cases 3 and 4 are symmetric with Cases 1 and 2, interchanging the
+; roles of x and y.
+
+ (local
+ (defthm case-3
+ (implies (and (mem (y a) (x a))
+ (equal (cardinality (x a)) 2)
+ (pairp A))
+ (= (pair (hd A) (tl A)) A))
+ :hints
+ (("Goal"
+ :use
+ ((:instance elim-choose-doubleton (x A))
+ (:instance elim-choose-doubleton (x (x a)))
+ (:instance elim-choose-singleton
+ (x (diff (x a) (scons (y a) nil))))
+ (:instance mem-singleton
+ (e (y a))
+ (x (diff (x a) (scons (y a) nil)))))))))
+
+ (local
+ (defthm case-4
+ (implies (and (mem (y a) (x a))
+ (equal (cardinality (x a)) 1)
+ (pairp A))
+ (= (pair (hd A) (tl A)) A))
+ :hints
+ (("Goal"
+ :use
+ ((:instance elim-choose-doubleton (x A))
+ (:instance elim-choose-singleton (x (x a)))
+ (:instance mem-singleton
+ (e (y a))
+ (x (x a))))))))
+
+ (defthm pair-hd-tl
+ (implies (pairp A)
+ (= (pair (hd A) (tl A)) A))
+ :hints
+ (("Goal" :in-theory (disable pair hd tl)
+ :cases ((and (mem (x a) (y a)) ;;; Case 1
+ (equal (cardinality (y a)) 2))
+ (and (mem (x a) (y a)) ;;; Case 2
+ (equal (cardinality (y a)) 1))
+ (and (mem (y a) (x a)) ;;; Case 3
+ (equal (cardinality (x a)) 2))
+ (and (mem (y a) (x a)) ;;; Case 4
+ (equal (cardinality (x a)) 1)))))
+ :rule-classes (:rewrite :elim)))
+
+(in-theory (disable mem-container))
+
+(in-theory (disable pairp pair hd tl))
+
+(defthm equal-booleans
+ (implies (and (acl2::booleanp p)
+ (acl2::booleanp q))
+ (equal (equal p q)
+ (iff p q))))
+
+(defthm equal-pair
+ (equal (= (pair x1 y1)
+ (pair x2 y2))
+ (and (= x1 x2)
+ (= y1 y2)))
+ :hints
+ (("Goal" :in-theory (disable hd-pair tl-pair)
+ :use ((:instance hd-pair (x x1) (y y1))
+ (:instance hd-pair (x x2) (y y2))
+ (:instance tl-pair (x x1) (y y1))
+ (:instance tl-pair (x x2) (y y2))))))
+
+(in-theory (disable equal-booleans))
+
+(defthm equal-pair-generalized
+ (equal (= (pair x1 x2) y)
+ (and (pairp y)
+ (= x1 (hd y))
+ (= x2 (tl y)))))
+
+(in-theory (disable equal-pair-generalized))
+
+
+
+; ----------------------------------------------------------------------------
+; Functions as Sets
+
+; The following is an example of set comprehension. In particular, it
+; is
+
+; { x in s | (and (pairp x) (= e (hd x)))}
+
+(defun subset-such-that1 (s e)
+ (cond ((ur-elementp s) nil)
+ ((and (pairp (scar s))
+ (= e (hd (scar s))))
+ (scons (scar s) (subset-such-that1 (scdr s) e)))
+ (t (subset-such-that1 (scdr s) e))))
+
+; When such a function is defined we should immediately prove the
+; obvious three relationships:
+
+(defthm setp-subset-such-that1
+ (setp (subset-such-that1 a e)))
+
+(defthm mem-subset-such-that1
+ (iff (mem pair (subset-such-that1 a x))
+ (and (pairp pair)
+ (mem pair a)
+ (= (hd pair) x)))
+ :hints (("Goal" :do-not '(generalize))))
+
+(defthm subsetp-subset-such-that1
+ (subsetp (subset-such-that1 a x) a))
+
+; The congruence rules are easy.
+
+(defx :strategy :congruence (subset-such-that1 a e) 1 :method :subsetp)
+(defx :strategy :congruence (subset-such-that1 a e) 2)
+
+(defthm mem-subset-such-that1-corrollary
+ (implies (and (subsetp a (subset-such-that1 f x))
+ (mem e a))
+ (and (pairp e)
+ (= (hd e) x))))
+
+; Now we define apply:
+
+(defun apply (s e)
+ (tl (choose (subset-such-that1 s e))))
+
+(defcong = = (apply s e) 1)
+(defcong = = (apply s e) 2)
+
+(defun except (s e v)
+ (scons (pair e v)
+ (diff s (subset-such-that1 s e))))
+
+(defcong = = (except s e v) 1)
+(defcong = = (except s e v) 2)
+(defcong = = (except s e v) 3)
+
+(defthm diff-scons-1
+ (implies (acl2::syntaxp (not (equal b ''nil)))
+ (= (diff a (scons e b))
+ (diff (diff a b) (brace e)))))
+
+(defthm ur-elementp-diff
+ (iff (ur-elementp (diff a b))
+ (subsetp a b)))
+
+(defthm subset-such-that1-diff-subset-such-that-1
+ (= (subset-such-that1 (diff f (subset-such-that1 f x)) y)
+ (if (= x y)
+ nil
+ (subset-such-that1 f y))))
+
+(encapsulate
+ nil
+ (local
+ (defthm lemma2
+ (implies (and (subsetp f (subset-such-that1 g x))
+ (not (= x y)))
+ (= (subset-such-that1 f y)
+ nil))))
+
+ (defthm apply-except
+ (= (apply (except f x v) y)
+ (if (= x y)
+ v
+ (apply f y)))))
+
+(defthm mem-except
+ (equal (mem e (except f x v))
+ (if (pairp e)
+ (if (= (hd e) x)
+ (= (tl e) v)
+ (mem e f))
+ (mem e f))))
+
+(defthm subsetp-except
+ (iff (subsetp (except f x v) g)
+ (and (mem (pair x v) g)
+ (subsetp (diff f (subset-such-that1 f x))
+ g))))
+
+(defthm ur-elementp-except
+ (not (ur-elementp (except f x v))))
+
+(in-theory (disable apply except))
+
+(defmacro func* (&rest args)
+ (cond ((endp args) nil)
+ ((endp (cdr args)) (car args))
+ (t `(except (func* ,@(cdr args))
+ ,(car (car args))
+ ,(cadr (car args))))))
+
+(defmacro func (&rest args)
+ `(func* ,@args nil))
+
+
+; ----------------------------------------------------------------------------
+; Sets of ordered pairs.
+
+; This is really just a simple map over a checking a predicate. I
+; need to automate this sort of thing but I will do it by hand right
+; now.
+
+(defun pairsp (a)
+ (cond ((ur-elementp a) t)
+ (t (and (pairp (scar a))
+ (pairsp (scdr a))))))
+
+(defx :strategy :congruence (pairsp a) 1 :method :canonicalize)
+
+(defthm pairsp-union
+ (equal (pairsp (union a b))
+ (and (pairsp a)
+ (pairsp b))))
+
+(defthm pairsp-diff
+ (implies (pairsp a)
+ (pairsp (diff a b))))
+
+; This one is more useful when dealing with sets created by EXCEPT.
+
+(defthm pairsp-diff-subset-such-that1
+ (equal (pairsp (diff a (subset-such-that1 b x)))
+ (pairsp a)))
+
+(defthm pairsp-scons
+ (equal (pairsp (scons e a))
+ (and (pairp e)
+ (pairsp a))))
+
+(defthm mem-pairsp
+ (implies (and (mem e f)
+ (pairsp f))
+ (pairp e)))
+
+(defthm pairsp-subset-such-that1
+ (implies (pairsp f)
+ (pairsp (subset-such-that1 f x))))
+
+(defthm nil-not-mem-pairsp
+ (implies (pairsp f)
+ (not (mem nil f))))
+
+; ----------------------------------------------------------------------------
+; Recognizing Functions
+
+; The basic idea is to define the predicate that recognizes when a set
+; is both pairsp and has unique hds. We've got the first part. The
+; second part is called functionp1.
+
+; Here is my first functionp1. It does not insure that every element
+; of f is a pair. Thus,
+
+; (functionp1 (brace (pair 1 2)) (brace (pair 1 2) 3)) = t
+
+; Second, it is fragile in the sense that if a is not a subset of f, it
+; fails, e.g.,
+
+; (functionp1 (brace (pair 1 2)) (brace (pair 3 4))) = nil
+
+; This is not a problem at the top level, where a is f. But in stating
+; theorems about functionp1 it would be convenient to allow arbitrary a
+; with sensible results.
+
+; (defun functionp1 (a f)
+; (cond ((ur-elementp a) t)
+; (t (and (pairp (scar a))
+; (equal (cardinality (subset-such-that1 f (hd (scar a)))) 1)
+; (functionp1 (scdr a) f)))))
+
+; So here is my second:
+
+(defun functionp1 (a f)
+ (cond ((ur-elementp a) t)
+ (t (and (<= (cardinality (subset-such-that1 f (hd (scar a)))) 1)
+ (functionp1 (scdr a) f)))))
+
+(defx :strategy :congruence (functionp1 a f) 1 :method :canonicalize)
+(defcong = equal (functionp1 a f) 2)
+
+
+; Is 8 a function? I say no. The reason I say no, is that I want it
+; to be the case that two functions are equal iff apply gives the same
+; answers on both. But if I defined a function as (and (pairsp f)
+; (functionp1 f f)) then 8 is a functionp, because every element of 8
+; is a pair and their hds are unique.
+
+(defun functionp (f)
+ (if (ur-elementp f)
+ (= f nil)
+ (and (pairsp f)
+ (functionp1 f f))))
+
+(defcong = equal (functionp f) 1)
+
+; My next goal is to prove that functionp is preserved by EXCEPT.
+; I need some lemmas about functionp1
+
+(defthm cardinality-subset-such-that1
+ (<= (cardinality (subset-such-that1 f x))
+ (cardinality f))
+ :rule-classes :linear)
+
+(defun simultaneously (a b)
+ (declare (xargs :measure (cardinality a)))
+ (cond ((ur-elementp a) b)
+ (t (simultaneously (diff a (brace (scar a)))
+ (diff b (brace (scar a)))))))
+
+(defthm cardinality-subsetp
+ (implies (subsetp a b)
+ (<= (cardinality a)
+ (cardinality b)))
+ :hints (("Goal" :induct (simultaneously a b)))
+ :rule-classes :linear)
+
+
+
+; The next two theorems are not used until later, but they seem
+; natural to have around.
+
+(defthm functionp1-subsetp-2
+ (implies (and (functionp1 a g)
+ (subsetp f g))
+ (functionp1 a f))
+ :hints
+ (("Subgoal *1/4'"
+ :in-theory (disable cardinality-subsetp)
+ :use (:instance cardinality-subsetp
+ (a (SUBSET-SUCH-THAT1 F (HD (SCAR A))))
+ (b (SUBSET-SUCH-THAT1 G (HD (SCAR A))))))))
+
+(defthm functionp1-diff
+ (implies (functionp1 a f)
+ (functionp1 a (diff f b)))
+ :hints (("Goal" :in-theory (disable subsetp-diff-1)
+ :use (:instance subsetp-diff-1
+ (a f)
+ (b b)))))
+
+; Consider the goal (implies (functionp f) (functionp f')), where f'
+; is (except f x v). Ignoring the pairsp part, this opens into
+
+; (implies (functionp1 f f) (functionp1 f' f'))
+
+; We have to break both duplications. Each requires a lemma. Then
+; we put the two lemmas together to get something like:
+
+; (implies (functionp1 b f) (functionp1 a f'))
+
+; where (subsetp a b).
+
+; Here is one of the two ``breakers.''
+
+(defthm functionp1-subsetp-1
+ (implies (and (subsetp a b)
+ (functionp1 b f))
+ (functionp1 a f))
+ :hints (("Goal" :do-not '(generalize))))
+
+(encapsulate
+ nil
+
+; This is the other ``breaker''. The scons below is f', i.e., the
+; expansion of (except f x v).
+
+ (local
+ (defthm functionp1-except-lemma
+ (implies (functionp1 a f)
+ (functionp1 a (scons (pair x v)
+ (diff f (subset-such-that1 f x)))))))
+
+; Now we put the two breakers together to get the main lemma about
+; functionp1 and except.
+
+ (defthm functionp1-except
+ (implies (and (functionp1 b f)
+ (subsetp a b))
+ (functionp1 a (scons (pair x v)
+ (diff f (subset-such-that1 f x)))))))
+
+(defthm functionp-except
+ (implies (functionp f)
+ (functionp (except f x v)))
+ :hints (("Goal" :in-theory (enable except))))
+
+(defthm functionp-implies-pairsp
+ (implies (functionp f)
+ (pairsp f)))
+
+(in-theory (disable functionp))
+
+;----------------------------------------------------------------------------
+; Domain and Range
+
+(defun domain (f)
+ (cond ((ur-elementp f) nil)
+ (t (scons (hd (scar f))
+ (domain (scdr f))))))
+
+(defun range (f)
+ (cond ((ur-elementp f) nil)
+ (t (scons (tl (scar f)) (range (scdr f))))))
+
+(defthm mem-implies-mem-domain
+ (implies (mem e f)
+ (mem (hd e) (domain f))))
+
+(defthm ur-elementp-domain
+ (equal (ur-elementp (domain f))
+ (ur-elementp f)))
+
+(defx :strategy :congruence (domain f) 1 :method :subsetp)
+
+(defthm mem-implies-mem-range
+ (implies (mem e f)
+ (mem (tl e) (range f))))
+
+(defthm ur-elementp-range
+ (equal (ur-elementp (range f))
+ (ur-elementp f)))
+
+(defx :strategy :congruence (range f) 1 :method :subsetp)
+
+(defthm domain-scons
+ (= (domain (scons e f))
+ (scons (hd e) (domain f))))
+
+(defthm domain-diff-subset-such-that1
+ (implies (pairsp f)
+ (= (domain (diff f (subset-such-that1 f x)))
+ (diff (domain f) (brace x)))))
+
+(defthm domain-except
+ (implies (pairsp f)
+ (= (domain (except f x v))
+ (scons x (domain f))))
+ :hints (("Goal" :in-theory (enable except))))
+
+; The range of (except f x v) is harder to characterize. If f is
+; not a function, then (except f x v) might be. The range of f
+; might include many things that are removed by the except.
+
+(defthm range-scons
+ (= (range (scons e f))
+ (scons (tl e) (range f))))
+
+(defthm subsetp-range-except
+ (subsetp (range (except f x v))
+ (scons v (range f)))
+ :hints (("Goal" :in-theory (enable except))))
+
+; We have these two, even though the union is not necessarily a
+; function.
+
+(defthm domain-union
+ (= (domain (union f g))
+ (union (domain f) (domain g))))
+
+(defthm range-union
+ (= (range (union f g))
+ (union (range f) (range g))))
+
+(defthm cardinality-domain
+ (<= (cardinality (domain f)) (cardinality f))
+ :rule-classes :linear)
+
+(defthm cardinality-range
+ (<= (cardinality (range f)) (cardinality f))
+ :rule-classes :linear)
+
+(defthm ur-element-subset-such-that1
+ (implies (pairsp f)
+ (equal (ur-elementp (subset-such-that1 f x))
+ (not (mem x (domain f))))))
+
+(defthm cardinality-<=-0
+ (equal (< 0 (cardinality a))
+ (not (ur-elementp a))))
+
+(defthm cardinality-domain-functionp
+ (implies (functionp f)
+ (equal (cardinality (domain f))
+ (cardinality f)))
+ :hints (("Goal" :in-theory (enable functionp))))
+
+(defthm subset-such-that1-empty
+ (implies (not (mem e (domain b)))
+ (= (subset-such-that1 b e)
+ nil)))
+
+; Is the (pairsp b) hypothesis below necessary? Yes. Here is a counterexample
+; of the formula without the hypothesis.
+
+#|(let ((b (brace 123))
+ (a (brace (pair nil 33)))
+ (pair (pair nil 2)))
+ (equal (functionp1 a (scons pair b))
+ (if (and (pairp pair)
+ (mem (hd pair) (domain a)))
+ (and (functionp1 a b)
+ (or (mem pair b)
+ (not (mem (hd pair) (domain b)))))
+ (functionp1 a b))))|#
+
+(defthm functionp1-scons
+ (implies (pairsp b)
+ (equal (functionp1 a (scons pair b))
+ (if (and (pairp pair)
+ (mem (hd pair) (domain a)))
+ (and (functionp1 a b)
+ (or (mem pair b)
+ (not (mem (hd pair) (domain b)))))
+ (functionp1 a b)))))
+
+(defthm cardinality-<=-1-cases
+ (iff (< 1 (cardinality x))
+ (not (or (ur-elementp x)
+ (equal (cardinality x) 1)))))
+
+(defthm functionp-scons-lemma
+ (implies (and (functionp1 a b)
+ (subsetp a b)
+ (pairsp b)
+ (mem e a))
+ (equal (cardinality (subset-such-that1 b (hd e)))
+ 1)))
+
+; Note that the following theorem is essentially a recursive
+; alternative definition of functionp.
+
+(defthm functionp-scons
+ (equal (functionp (scons e a))
+ (if (ur-elementp a)
+ (pairp e)
+ (and (functionp a)
+ (pairp e)
+ (or (mem e a)
+ (not (mem (hd e) (domain a)))))))
+ :hints (("Goal" :in-theory (enable functionp))))
+
+(defthm functionp-union
+ (implies (and (functionp a)
+ (functionp b)
+ (not (intersection (domain a) (domain b))))
+ (functionp (union a b))))
+
+(defthm disjoint-domains-implies-disjoint
+ (implies (not (intersection (domain a) (domain b)))
+ (not (intersection a b)))
+ :rule-classes nil)
+
+(defthm cardinality-except
+ (implies (functionp f)
+ (= (cardinality (except f x v))
+ (if (mem x (domain f))
+ (cardinality f)
+ (+ 1 (cardinality f)))))
+ :hints (("Goal"
+ :use ((:instance cardinality-domain-functionp (f (except f x v)))
+ (:instance cardinality-domain-functionp (f f)))
+ :in-theory (disable cardinality-domain-functionp))))
+
+(defthm apply-outside-domain
+ (implies (not (mem e (domain f)))
+ (= (apply f e) nil))
+ :hints (("Goal" :in-theory (enable apply))))
+
+;----------------------------------------------------------------------------
+; Restrictions
+
+; I can think of three slightly different ways to define the restriction
+; of a function f to some domain s.
+
+; (1) Iterate over s and make a function of the defined values. This
+; always produces a function. However, if f is not a function, the
+; function it produces is sort of unpredictable because it uses apply,
+; so the restricted function chooses the largest pairs.
+
+(defun restrict (f s)
+ (cond ((ur-elementp s) nil)
+ ((mem (scar s) (domain f))
+ (except (restrict f (scdr s))
+ (scar s)
+ (apply f (scar s))))
+ (t (restrict f (scdr s)))))
+
+; (2) Iterate over f and make a function of the values of elements of
+; s. This always produces a function. But if f is not a function,
+; the restricted function is unpredictable because it chooses the
+; first pair presented for each domain element. I reject this
+; definition because it does not do the ``normal'' things with a
+; function. The normal things you do with a function are enquire
+; about its domain and apply it. Looking at its internal structure is
+; an invitation to low-level work.
+
+; (defun restrict2 (f s)
+; (cond ((ur-elementp f) nil)
+; ((and (pairp (scar f))
+; (mem (hd (scar f)) s))
+; (except (restrict2 (scdr f) s)
+; (hd (scar f))
+; (tl (scar f))))
+; (t (restrict2 (scdr f) s))))
+
+; (3) Iterate over f and collect everything whose hd is in s. The
+; result may not be a function, but it is if f is. This has the
+; appeal of being really simple, but, again, uses f in an abnormal
+; way.
+
+; (defun restrict3 (f s)
+; (cond ((ur-elementp f) nil)
+; ((mem (hd (scar f)) s)
+; (scons (scar f) (restrict3 (scdr f) s)))
+; (t (restrict3 (scdr f) s))))
+
+(defx :strategy :congruence (restrict f s) 1)
+
+; Next we prove that the second argument of restrict admits = as a
+; congruence relation. For some reason it took me a while to
+; realize that if you are going to prove that something is a
+; subset of (restrict f s) you must be able to answer the question
+; ``when is e a member of (restrict f s)?'' I was seeing this question
+; come up and generalized it to ``when is e a member of a function?''
+; Answering that was harder than answering it for (restrict f s),
+; which is always a function but which is built in a way that makes
+; it easier to answer the question. Here is how you do it.
+
+; The system can prove mem-restrict, below, without further help. It
+; generates three inductively proved subgoals. These are not worth
+; turning into rules because mem-restrict, once proved, is better than
+; each of them.
+
+(defthm mem-restrict
+ (equal (mem e (restrict f s))
+ (and (pairp e)
+ (mem (hd e) (domain f))
+ (= (tl e) (apply f (hd e)))
+ (mem (hd e) s)))
+ :hints (("Goal" :do-not '(generalize))))
+
+; At first I wrote (= (restrict f s) nil) instead of the inner equal.
+; But I really need the stronger equal because in the defcong= proof
+; below the question of whether (restrict f s) is a set comes up. To
+; be a set it must be either not an ur-element or nil. This means
+; that we end up testing (restrict f s) against nil in a propositional
+; setting, not a set theory setting. Since = does not refine iff
+; (because '(:UR-CONS NIL) is canonicalized to NIL), knowing that
+; (restrict f s) is not = nil does not help us.
+
+(defthm ur-elementp-restrict
+ (equal (ur-elementp (restrict f s))
+ (equal (restrict f s) nil)))
+
+(defx :strategy :congruence (restrict f s) 2 :method :subsetp)
+
+(defthm functionp-restrict
+ (functionp (restrict f s)))
+
+; My next main goal is the fundamental fact characterizing the elements
+; of a function.
+
+; Perhaps disable this when we're done?
+
+
+(defthm pigeon-hole-1
+ (implies (and (mem e a)
+ (mem d a)
+ (equal (cardinality a) 1))
+ (= e d))
+ :rule-classes nil)
+
+; The next three theorems are trivial consequences of other lemmas
+; given the fact that (choose a) is an element of a. I really ought
+; to provide macros that capture these kind of theorems. The idea in
+; all of them is that if every element of a has some property then
+; (choose a) has that property if a is non-empty.
+
+(defthm hd-choose-subset-such-that1
+ (= (hd (choose (subset-such-that1 f x)))
+ (if (ur-elementp (subset-such-that1 f x))
+ nil
+ x))
+ :hints (("Goal"
+ :in-theory (disable mem-choose)
+ :use ((:instance mem-choose
+ (a (subset-such-that1 f x)))))))
+
+(defthm pairp-choose-subset-such-that1
+ (implies (pairsp f)
+ (equal (pairp (choose (subset-such-that1 f x)))
+ (and (not (ur-elementp f))
+ (mem x (domain f)))))
+ :hints (("Goal"
+ :in-theory (cons 'equal-booleans
+ (disable mem-choose))
+ :use ((:instance mem-choose
+ (a (subset-such-that1 f x)))))))
+
+(defthm mem-choose-subset-such-that1
+ (implies (pairsp f)
+ (equal (mem (choose (subset-such-that1 f x)) f)
+ (and (not (ur-elementp f))
+ (mem x (domain f)))))
+ :hints (("Goal"
+ :in-theory (cons 'equal-booleans
+ (disable mem-choose))
+ :use ((:instance mem-choose
+ (a (subset-such-that1 f x)))))))
+
+; This is a pretty obscure fact, I think. If x is a pair in f and
+; there is only one pair in f with its hd, then choose chooses x.
+
+(defthm mem-x-implies-not-ur-elementp-subset-such-that1
+ (implies (and (mem x f)
+ (pairp x))
+ (not (ur-elementp (subset-such-that1 f (hd x))))))
+
+(defthm choose-subset-such-that1
+ (implies (and (<= (cardinality (subset-such-that1 f (hd x))) 1)
+ (mem x f)
+ (pairp x)
+ (pairsp f))
+ (= (choose (subset-such-that1 f (hd x)))
+ x))
+ :hints (("Goal"
+ :use (:instance pigeon-hole-1
+ (e x)
+ (d (choose (subset-such-that1 f (hd x))))
+ (a (subset-such-that1 f (hd x)))))))
+
+(defthm functionp-implies-mem-1
+ (implies (and (functionp1 a f)
+ (pairsp f)
+ (subsetp a f)
+ (mem hd (domain a)))
+ (mem (pair hd (tl (choose (subset-such-that1 f hd))))
+ f)))
+
+(defthm functionp-implies-mem-2
+ (implies (and (functionp1 a f)
+ (pairsp f)
+ (subsetp a f)
+ (mem (hd x) (domain a))
+ (pairp x)
+ (mem x f))
+ (= (choose (subset-such-that1 f (hd x)))
+ x)))
+
+; This is the fundamental fact about membership in a function. It
+; loops if made into a rewrite rule.
+
+(defthm mem-functionp
+ (implies (functionp f)
+ (equal (mem e f)
+ (and (pairp e)
+ (mem (hd e) (domain f))
+ (= (tl e) (apply f (hd e))))))
+ :rule-classes nil
+ :hints (("Goal"
+ :in-theory (enable functionp apply equal-booleans))))
+
+(defthm domain-restrict
+ (= (domain (restrict f s))
+ (intersection s (domain f))))
+
+(defthm apply-restrict
+ (implies (and (mem x (domain f))
+ (mem x s))
+ (= (apply (restrict f s) x)
+ (apply f x))))
+
+(defthm except-scdr-scar-elim
+ (implies (and (functionp f)
+ (not (ur-elementp f)))
+ (= (except (scdr f) (hd (scar f)) (tl (scar f)))
+ f))
+ :otf-flg t
+ :hints
+ (("Goal"
+ :in-theory (enable except functionp equal-pair-generalized)
+ :use ((:instance mem-functionp
+ (e (pair (hd (scar f)) (tl (scar f))))
+ (f f))
+ (:instance mem-singleton
+ (e (pair (hd (scar f)) (tl (scar f))))
+ (x (subset-such-that1 (scdr f) (hd (scar f)))))))))
+
+(defthm functionp-nil
+ (implies (ur-elementp f)
+ (equal (functionp f) (= f nil)))
+ :hints (("Goal" :in-theory (enable functionp))))
+
+(defthm functionp-pairp
+ (implies (not (pairp x))
+ (not (functionp (scons x y))))
+ :hints (("Goal" :in-theory (enable functionp))))
+
+(defthm except-scdr-scar-elim-special-case
+ (implies (and (functionp f)
+ (not (ur-elementp f))
+ (ur-elementp (scdr f)))
+ (= (except nil (hd (scar f)) (tl (scar f)))
+ f))
+ :hints (("Goal" :in-theory (enable except))))
+
+(defthm functionp-scdr
+ (implies (functionp f)
+ (functionp (scdr f)))
+ :hints (("Goal" :in-theory (enable functionp))))
+
+(defthm restrict-domain
+ (implies (and (functionp f)
+ (functionp g)
+ (subsetp f g))
+ (= (restrict g (domain f)) f))
+ :hints
+ (("Subgoal *1/4"
+ :use ((:instance mem-functionp (e (scar f)) (f g))))))
+
+; The lemma above will rewrite (restrict a (domain a)) to a, provided
+; (functionp a). But it is often the case that the domain expression
+; will be rewritten to something else, e.g., an intersection. So
+; we provide a bridge.
+
+(defthm restrict-domain-special-case
+ (implies (and (functionp f)
+ (= a (domain f)))
+ (= (restrict f a) f)))
+
+(defthm restrict-scons
+ (= (restrict f (scons e s))
+ (if (mem e (domain f))
+ (except (restrict f s)
+ e
+ (apply f e))
+ (restrict f s))))
+
+; ----------------------------------------------------------------------------
+; Strategies for Proving Functions and Sets Equivalent
+
+(encapsulate ((functional-equiv-fn1 () t)
+ (functional-equiv-fn2 () t))
+ (local (defun functional-equiv-fn1 nil nil))
+ (local (defun functional-equiv-fn2 nil nil))
+ (defthm functional-equivalence-constraint-1
+ (functionp (functional-equiv-fn1)))
+ (defthm functional-equivalence-constraint-2
+ (functionp (functional-equiv-fn2)))
+ (defthm functional-equivalence-constraint-3
+ (= (domain (functional-equiv-fn2))
+ (domain (functional-equiv-fn1))))
+
+; We use the unusual variable name fex (``functional equivalence x'') because
+; any variable appearing in a constraint is prohibited from occurring in
+; any theorem proved with functional-instantiation from this constraint.
+
+ (defthm functional-equivalence-constraint-4
+ (implies (mem fex (domain (functional-equiv-fn1)))
+ (= (apply (functional-equiv-fn1) fex)
+ (apply (functional-equiv-fn2) fex)))))
+
+(defun every-where-= (s f g)
+ (cond ((ur-elementp s) t)
+ (t (and (= (apply f (scar s))
+ (apply g (scar s)))
+ (every-where-= (scdr s) f g)))))
+
+(defthm every-where-=-implies-=-restrict
+ (implies (and (functionp f)
+ (functionp g)
+ (subsetp s (domain f))
+ (subsetp s (domain g))
+ (every-where-= s f g))
+ (= (restrict f s)
+ (restrict g s)))
+ :rule-classes nil)
+
+(encapsulate
+ nil
+ (local
+ (defthm every-where-=-functional-equiv-fn1-functional-equiv-fn2
+ (implies (subsetp s (domain (functional-equiv-fn1)))
+ (every-where-= s (functional-equiv-fn1) (functional-equiv-fn2)))))
+
+ (defthm functional-equivalence-theorem
+ (= (functional-equiv-fn1) (functional-equiv-fn2))
+ :rule-classes nil
+ :hints (("Goal"
+ :use (:instance every-where-=-implies-=-restrict
+ (f (functional-equiv-fn1))
+ (g (functional-equiv-fn2))
+ (s (domain (functional-equiv-fn1))))))))
+
+; The above encapsulation provides a nice way to prove two functions
+; are equal. You can just instantiate the lemma above with any two
+; functions that are known to have the same domain and that are
+; apply-equal everywhere.
+
+(defmacro functional-equivalence (name term
+ &key
+ hints
+ (rule-classes 'nil rule-classesp)
+ (otf-flg 'nil otf-flgp))
+ (let* ((xterm
+ (acl2::case-match
+ term
+ (('implies acl2::& ('= acl2::& acl2::&))
+ term)
+ (('= acl2::& acl2::&)
+ `(implies t ,term))
+ (t nil))))
+ (cond
+ ((null xterm)
+ `(acl2::er acl2::soft 'functional-equivalence
+ "The functional-equivalence strategy requires a term of ~
+ the form (= f g) or (implies h (= f g)). Your term, ~x0, ~
+ is not of this form."
+ ',term))
+ ((acl2::assoc-equal "Goal" hints)
+ `(acl2::er acl2::soft 'functional-equivalence
+ "The functional-equivalence strategy provides hints for ~
+ \"Goal\". Your hints should be provided for some Subgoal."))
+ (t
+ (let ((hyps (cadr xterm))
+ (lhs (cadr (caddr xterm)))
+ (rhs (caddr (caddr xterm))))
+ `(defthm ,name ,term
+ :hints
+ (("Goal"
+ :use ((:functional-instance
+ functional-equivalence-theorem
+ (functional-equiv-fn1
+ (lambda ()
+ ,(if (eq hyps t)
+ lhs
+ `(if ,hyps ,lhs nil))))
+ (functional-equiv-fn2
+ (lambda ()
+ ,(if (eq hyps t)
+ rhs
+ `(if ,hyps ,rhs nil)))))))
+ ,@hints)
+ ,@(if rule-classesp
+ `(:rule-classes ,rule-classes)
+ nil)
+ ,@(if otf-flgp
+ `(:otf-flg ,otf-flg)
+ nil)))))))
+
+; While I'm at it, I'll provide a way to prove that two sets are equal.
+
+; Suppose you have two arbitrary sets with the property that if x is a
+; member of one, then x is a member of the other.
+
+(encapsulate ((subsetp-strategy-set1 () t)
+ (subsetp-strategy-set2 () t))
+ (local (defun subsetp-strategy-set1 () nil))
+ (local (defun subsetp-strategy-set2 () nil))
+
+; We use the unusual variable name ssx (``subsetp strategy x'') because whatever
+; var we use in a constraint is off-limits to the user in any theorem proved
+; via functional instantiation based on these constraints.
+
+ (defthm subsetp-strategy-constraint
+ (implies (mem ssx (subsetp-strategy-set1))
+ (mem ssx (subsetp-strategy-set2)))))
+
+; Then the first set is a subset of the second.
+
+(encapsulate
+ nil
+ (local
+ (defthm subsetp-strategy-lemma
+ (implies (subsetp a (subsetp-strategy-set1))
+ (subsetp a (subsetp-strategy-set2)))))
+
+ (defthm subsetp-strategy
+ (subsetp (subsetp-strategy-set1)
+ (subsetp-strategy-set2))
+ :rule-classes nil))
+
+; And here is a handy macro to use this strategy to prove the subsetp
+; relation between two expressions under a hypothesis.
+
+; This macro allows us to write:
+; (defx foo (subsetp ... ...)
+; :strategy subset-relation
+; :rule-classes ...)
+
+(defmacro subset-relation (name term
+ &key
+ hints
+ (rule-classes 'nil rule-classesp)
+ (otf-flg 'nil otf-flgp))
+ (let* ((xterm
+ (acl2::case-match
+ term
+ (('implies acl2::& ('subsetp acl2::& acl2::&))
+ term)
+ (('subsetp acl2::& acl2::&)
+ `(implies t ,term))
+ (t nil))))
+ (cond
+ ((null xterm)
+ `(acl2::er acl2::soft 'subset-relation
+ "The subset-relation strategy requires a term of ~
+ the form (subsetp a b) or (implies h (subsetp a b)). Your term, ~x0, ~
+ is not of this form."
+ ',term))
+ ((acl2::assoc-equal "Goal" hints)
+ `(acl2::er acl2::soft 'subset-relation
+ "The subset-relation strategy provides hints for ~
+ \"Goal\". Your hints should be provided for some Subgoal."))
+ (t
+ (let ((hyps (cadr xterm))
+ (lhs (cadr (caddr xterm)))
+ (rhs (caddr (caddr xterm))))
+ `(defthm ,name ,term
+ :hints
+ (("Goal"
+ :use ((:functional-instance
+ subsetp-strategy
+ (subsetp-strategy-set1
+ (lambda ()
+ ,(if (eq hyps t)
+ lhs
+ `(if ,hyps ,lhs nil))))
+ (subsetp-strategy-set2
+ (lambda ()
+ ,(if (eq hyps t)
+ rhs
+ `(if ,hyps ,rhs nil)))))))
+ ,@hints)
+ ,@(if rule-classesp
+ `(:rule-classes ,rule-classes)
+ nil)
+ ,@(if otf-flgp
+ `(:otf-flg ,otf-flg)
+ nil)))))))
+
+; Here is a way to set equality using two subsets. It requires
+; proving (mem x a) <-> (mem x b).
+
+; We can thus write
+; (defx foo (implies ... (= ... ...))
+; :strategy equivalence-relation
+; :rule-classes ...)
+
+; Two proof obligations are generated, each a mem implying a mem. You
+; can provide hints for them with :hints-1 and :hints-2.
+
+(defmacro set-equivalence (name term
+ &key hints
+ (rule-classes 'nil rule-classesp)
+ (otf-flg 'nil otf-flgp)
+ (hints-1 'nil hints-1p)
+ (otf-flg-1 'nil otf-flg-1p)
+ (hints-2 'nil hints-2p)
+ (otf-flg-2 'nil otf-flg-2p))
+ (let* ((xterm
+ (acl2::case-match term
+ (('implies acl2::& ('= acl2::& acl2::&))
+ term)
+ (('= acl2::& acl2::&)
+ `(implies t ,term))
+ (t nil))))
+ (cond
+ ((null xterm)
+ `(acl2::er acl2::soft 'set-equivalence
+ "~x0 is not of the form (= x y) or of the form ~
+ (implies hyps (= x y))."
+ ',term))
+ ((or (acl2::assoc-equal "Goal" hints)
+ (acl2::assoc-equal "Goal" hints-1)
+ (acl2::assoc-equal "Goal" hints-2))
+ `(acl2::er acl2::soft 'set-equivalence
+ "The set-equivalence strategy provides hints for ~
+ \"Goal\". Your hints should be provided for some Subgoal."))
+ (t
+ (let ((hyps (cadr xterm))
+ (lhs (cadr (caddr xterm)))
+ (rhs (caddr (caddr xterm)))
+ (name-1 (packn-in-pkg (list name "-1") name))
+ (name-2 (packn-in-pkg (list name "-2") name)))
+ `(encapsulate
+ nil
+ (local
+ (defx ,name-1
+ ,(if (eq hyps t)
+ `(subsetp ,lhs ,rhs)
+ `(implies ,hyps (subsetp ,lhs ,rhs)))
+ :strategy subset-relation
+ ,@(if hints-1p `(:hints ,hints-1) nil)
+ ,@(if otf-flg-1p `(:otf-flg ,otf-flg-1) nil)
+ :rule-classes nil))
+ (local
+ (defx ,name-2
+ ,(if (eq hyps t)
+ `(subsetp ,rhs ,lhs)
+ `(implies ,hyps (subsetp ,rhs ,lhs)))
+ :strategy subset-relation
+ ,@(if hints-2p `(:hints ,hints-2) nil)
+ ,@(if otf-flg-2p `(:otf-flg ,otf-flg-2) nil)
+ :rule-classes nil))
+ (defthm ,name ,term
+ :hints
+ (("Goal"
+ :use ((:instance =-iff-subsetps
+ (a ,(if (eq hyps t)
+ lhs
+ `(if ,hyps ,lhs nil)))
+ (b ,(if (eq hyps t)
+ rhs
+ `(if ,hyps ,rhs nil))))
+ (:instance ,name-1)
+ (:instance ,name-2))
+ ,@hints))
+ ,@(if rule-classesp
+ `(:rule-classes ,rule-classes)
+ nil)
+ ,@(if otf-flgp
+ `(:otf-flg ,otf-flg)
+ nil))))))))
+
+; ----------------------------------------------------------------------------
+; An Example
+
+(defx union-diff-diff
+ (implies (and (subsetp a b)
+ (subsetp b c))
+ (= (union (diff b a)
+ (diff c b))
+ (diff c a)))
+ :strategy :set-equivalence)
+
+;----------------------------------------------------------------------------
+; Sequences
+
+; A sequence is a function whose domain is an initial subset of the
+; natural numbers.
+
+(defun nats (n)
+ (if (zp n)
+ '(0)
+ (scons n (nats (- n 1)))))
+
+(defthm ur-elementp-nats
+ (not (ur-elementp (nats n))))
+
+(defcong = = (nats n) 1
+ :hints (("Goal" :in-theory (enable zp))))
+
+(defthm mem-nats
+ (equal (mem e (nats n))
+ (and (integerp e)
+ (<= 0 e)
+ (<= e (nfix n))))
+ :hints (("Goal" :in-theory (enable =))))
+
+(defun sequencep (s)
+ (and (functionp s)
+ (= (domain s)
+ (diff (nats (cardinality s)) '(0)))))
+
+(defthm functionp-sequencep
+ (implies (sequencep s)
+ (functionp s)))
+
+(defthm domain-sequencep
+ (implies (sequencep s)
+ (= (domain s)
+ (diff (nats (cardinality s)) '(0)))))
+
+(in-theory (disable sequencep))
+
+(defun shift (i j f delta)
+ (declare (xargs :measure (nfix (- (+ 1 (acl2::ifix j)) (acl2::ifix i)))))
+ (cond ((and (integerp i)
+ (integerp j)
+ (<= i j))
+ (except (shift (+ 1 i) j f delta)
+ (+ i delta)
+ (apply f i)))
+ (t nil)))
+
+(defcong = = (shift i j f delta) 1)
+(defcong = = (shift i j f delta) 2)
+(defcong = = (shift i j f delta) 3)
+(defcong = = (shift i j f delta) 4)
+
+(defthm functionp-shift
+ (functionp (shift i j f delta)))
+
+; If f is a sequence, its domain is [1...n]. So (shift i j f delta)
+; takes [i...j] to [i+delta ... j+delta]. This is
+
+(defthm mem-domain-shift
+ (implies (integerp delta)
+ (= (mem x (domain (shift i j f delta)))
+ (and (integerp i)
+ (integerp j)
+ (<= i j)
+ (integerp x)
+ (<= (+ i delta) x)
+ (<= x (+ j delta))))))
+
+; We can express the domain of a shift of a sequence as a set of nats.
+
+(defx domain-shift
+ (implies (and (sequencep s)
+ (integerp delta)
+ (<= 0 delta))
+ (= (domain (shift 1 (cardinality s) s delta))
+ (diff (nats (+ delta (cardinality s)))
+ (nats delta))))
+ :strategy :set-equivalence)
+
+(defun concat (r s)
+ (union r (shift 1 (cardinality s) s (cardinality r))))
+
+(defcong = = (concat r s) 1)
+(defcong = = (concat r s) 2)
+
+(defthm functionp-concat
+ (implies (and (sequencep r)
+ (sequencep s))
+ (functionp (concat r s))))
+
+(defthm subsetp-nats-0
+ (subsetp '(0) (nats i)))
+
+(defthm =-0
+ (equal (= i 0)
+ (equal i 0))
+ :hints (("Goal" :in-theory (enable =))))
+
+(defthm subsetp-nats-nats
+ (equal (subsetp (nats i) (nats j))
+ (<= (nfix i) (nfix j))))
+
+(defthm domain-concat
+ (implies (and (sequencep r)
+ (sequencep s))
+ (= (domain (concat r s))
+ (diff (nats (+ (cardinality r) (cardinality s)))
+ '(0)))))
+
+; I need the (integerp delta) hypothesis because cardinality raises
+; the question of membership in the shifted domain and
+; mem-domain-shift has an integerp hyp.
+
+(defthm cardinality-shift
+ (implies (integerp delta)
+ (= (cardinality (shift i j f delta))
+ (if (and (integerp i)
+ (integerp j)
+ (<= i j))
+ (+ 1 (- j i))
+ 0))))
+
+(defthm cardinality-concat
+ (implies (and (sequencep r)
+ (sequencep s))
+ (= (cardinality (concat r s))
+ (+ (cardinality r) (cardinality s))))
+ :hints (("Goal"
+ :use (:instance disjoint-domains-implies-disjoint
+ (a r)
+ (b (shift 1 (cardinality s) s (cardinality r)))))))
+
+(defthm sequencep-concat
+ (implies (and (sequencep r)
+ (sequencep s))
+ (sequencep (concat r s)))
+ :hints (("Goal"
+ :in-theory
+ (set-difference-theories (enable sequencep)
+ '(concat)))))
+
+; Here is a recursive alternative definition of apply.
+
+(defthm apply-scons
+ (implies (functionp (scons pair f))
+ (= (apply (scons pair f) x)
+ (if (= (hd pair) x)
+ (tl pair)
+ (apply f x))))
+ :hints (("Goal" :in-theory (enable apply))
+ ("Subgoal 2.1'"
+ :in-theory (set-difference-theories (enable functionp)
+ '(functionp-scons-lemma))
+
+ :use ((:instance functionp-scons-lemma
+ (a f)
+ (b f)
+ (e (pair hd tl)))
+ (:instance mem-singleton
+ (x (subset-such-that1 f hd))
+ (e (pair hd tl)))))))
+
+(defthm apply-disjoint-union
+ (implies (and (functionp a)
+ (functionp b)
+ (not (intersection (domain a) (domain b))))
+ (= (apply (union a b) x)
+ (if (mem x (domain a))
+ (apply a x)
+ (apply b x)))))
+
+; Suppose you have a function, f, (not necessarily a sequence) and you
+; form another function, f', by shifting [i...j] of f up by delta.
+; What is (apply f' x)? The domain of f' is [i+delta ... j+delta].
+; If x is in that domain, then (apply f' x) is (apply f (- x delta)).
+
+; To prove this we need the important fact:
+
+(defthm apply-shift
+ (= (apply (shift i j f delta) x)
+ (if (mem x (domain (shift i j f delta)))
+ (apply f (- x delta))
+ nil)))
+
+(defthm apply-concat
+ (implies (and (sequencep r)
+ (sequencep s))
+ (= (apply (concat r s) i)
+ (cond ((and (integerp i)
+ (< 0 i))
+ (if (<= i (cardinality r))
+ (apply r i)
+ (apply s (- i (cardinality r)))))
+ (t nil))))
+ :hints (("Subgoal 11"
+ :in-theory (disable apply-outside-domain)
+ :use
+ ((:instance apply-outside-domain
+ (e (- i (cardinality r)))
+ (f s))))))
+
+(in-theory (disable concat))
+
+(defx associativity-of-concat
+ (implies (and (sequencep a)
+ (sequencep b)
+ (sequencep c))
+ (= (concat (concat a b) c)
+ (concat a (concat b c))))
+ :strategy :functional-equivalence)
+
+; Now I will define seq-hd and seq-tl to let me do recursion down
+; sequences.
+
+(defun seq-hd (s) (apply s 1))
+
+(defcong = = (seq-hd s) 1)
+
+(defun seq-tl (s)
+ (restrict (shift 1 (cardinality s) s -1)
+ (diff (nats (- (cardinality s) 1))
+ (brace 0))))
+
+(defcong = = (seq-tl s) 1)
+
+(defthm functionp-seq-tl
+ (functionp (seq-tl s)))
+
+(defthm cardinality-restrict
+ (= (cardinality (restrict f s))
+ (cardinality (intersection (domain f) s))))
+
+
+
+(defx domain-shift-generalized
+ (implies (and (integerp i)
+ (integerp j)
+ (<= i j)
+ (integerp delta)
+ (<= 0 (+ i delta)))
+ (= (domain (shift i j s delta))
+ (if (= (+ delta i) 0)
+ (nats (+ delta j))
+ (diff (nats (+ delta j))
+ (nats (+ delta i -1))))))
+ :strategy :set-equivalence)
+
+(defthm cardinality-positive
+ (implies (not (ur-elementp s))
+ (< 0 (cardinality s)))
+ :rule-classes :linear)
+
+(defthm intersection-x-x
+ (= (intersection x x) (sfix x)))
+
+(defthm cardinality-diff-nats-0
+ (implies (and (integerp i)
+ (<= 0 i))
+ (= (cardinality (diff (nats i) '(0)))
+ i)))
+
+(defthm cardinality-seq-tl
+ (implies (not (ur-elementp s))
+ (= (cardinality (seq-tl s))
+ (- (cardinality s) 1))))
+
+(defthm sequencep-seq-tl
+ (implies (not (ur-elementp s))
+ (sequencep (seq-tl s)))
+ :hints (("Goal" :in-theory (enable sequencep))))
+
+(defthm seq-tl-recursion
+ (implies (not (ur-elementp s))
+ (< (cardinality (seq-tl s))
+ (cardinality s)))
+ :rule-classes (:built-in-clause :linear))
+
+(in-theory (disable seq-hd seq-tl))
+
+; Next, I define defmap. Thus,
+
+; (defmap subset (a s b) :for x :in s :such-that (bd a x b))
+; and
+; (defmap image (a s b) :for x :in s :map (bd a x b))
+
+; will define subset and image recursively so that they return the
+; sets described below
+
+; (subset a s b) = {x in s | (bd a x b)}
+; and
+; (image a s b) = {(bd a x b) | x in s}
+
+; In addition, I get a few useful theorems about these functions, including
+; that = is a congruence for every argument.
+
+; It must be the case that congruence rules are already in place for
+; (bd a x b).
+
+(defun defmap-congruences (vars call sloc i)
+ (cond
+ ((endp vars) nil)
+ (t (cons (if (equal sloc i)
+ `(defx :strategy :congruence ,call ,i :method :subsetp)
+ `(defx :strategy :congruence ,call ,i))
+ (defmap-congruences (cdr vars) call sloc (+ 1 i))))))
+
+(defmacro defmap (name vars
+ &key
+ (for 'nil forp)
+ (in 'nil inp)
+ (such-that 'nil such-thatp)
+ (map 'nil mapp))
+
+; (defmap foo (s ...) :for x :in s :such-that px)
+; or
+; (defmap foo (s ...) :for x :in s :map px)
+
+ (cond
+ ((not (and (symbolp name)
+ (acl2::symbol-listp vars)
+ forp
+ (symbolp for)
+ (not (acl2::member-equal for vars))
+ inp
+ (symbolp in)
+ (acl2::member-equal in vars)
+ (or (and such-thatp (not mapp))
+ (and (not such-thatp) mapp))))
+ `(acl2::er acl2::soft 'defmap
+ "The proper form of a defmap command is~%~
+ (defmap name vars :for x :in v :such-that body)~%~
+ or~%~
+ (defmap name vars :for x :in v :map body),~%~
+ where name is a new function name, vars is a list of ~
+ variables, x is a variable not in vars, ~
+ v is a variable in vars, and body is a term."))
+ (such-thatp
+ (let* ((x for)
+ (s in)
+ (sloc (- (length vars) (length (member s vars))))
+ (body such-that)
+ (s1 (genname1 s 1 (cons x vars)))
+ (call `(,name ,@vars))
+ (rcall `(,name ,@(put-nth `(scdr ,s) sloc vars))))
+ `(encapsulate
+ nil
+ (defun ,name (,@vars)
+ (if (ur-elementp ,s)
+ nil
+ (let ((,x (scar ,s)))
+ (if ,body
+ (scons (scar ,s) ,rcall)
+ ,rcall))))
+
+ (defthm ,(packn-in-pkg (list "SETP-" name) 'defmap)
+ (setp ,call))
+
+ (defthm ,(packn-in-pkg (list "UR-ELEMENTP-" name) 'defmap)
+ (equal (ur-elementp ,call)
+ (equal ,call nil)))
+
+ (defthm ,(packn-in-pkg (list "MEM-" name) 'defmap)
+ (equal (mem ,x ,call)
+ (and ,body ; we write it this way in case body
+ (mem ,x ,s))) ; is not Boolean!
+ :otf-flg t)
+
+ (defthm ,(packn-in-pkg (list "SUBSETP-" name) 'defmap)
+ (subsetp ,call ,s))
+
+ ,@(defmap-congruences vars call (+ sloc 1) 1)
+
+ (defthm ,(packn-in-pkg (list "MEM-" name "-CORROLLARY") 'defmap)
+ (implies (and (subsetp ,s1 ,call)
+ (mem ,x ,s1))
+ ,body))
+
+ (defthm ,(packn-in-pkg (list "CARDINALITY-" name) 'defmap)
+ (<= (cardinality ,call)
+ (cardinality ,s))
+ :rule-classes :linear)
+
+ (defthm ,(packn-in-pkg (list "UNION-" name) 'defmap)
+ (= (,name ,@(put-nth `(union ,s1 ,s) sloc vars))
+ (union (,name ,@(put-nth s1 sloc vars))
+ ,call)))
+
+ (defthm ,(packn-in-pkg (list "INTERSECTION-" name) 'defmap)
+ (= (,name ,@(put-nth `(intersection ,s1 ,s) sloc vars))
+ (intersection (,name ,@(put-nth s1 sloc vars))
+ ,call)))
+
+ )))
+ (t ;;; :map
+
+ (let* ((x for)
+ (s in)
+ (sloc (- (length vars) (length (member s vars))))
+ (body map)
+ (fx (genname1 x 1 (cons x vars)))
+ (s1 (genname1 s 1 (cons fx (cons x vars))))
+ (call `(,name ,@vars))
+ (rcall `(,name ,@(put-nth `(scdr ,s) sloc vars))))
+ `(encapsulate
+ nil
+ (defun ,name (,@vars)
+ (if (ur-elementp ,s)
+ nil
+ (let ((,x (scar ,s)))
+ (scons ,body ,rcall))))
+
+ (defthm ,(packn-in-pkg (list "SETP-" name) 'defmap)
+ (setp ,call))
+
+ (defthm ,(packn-in-pkg (list "UR-ELEMENTP-" name) 'defmap)
+ (equal (ur-elementp ,call)
+ (ur-elementp ,s)))
+
+ (defthm ,(packn-in-pkg (list "WEAK-MEM-" name) 'defmap)
+ (implies (and (mem ,x ,s)
+ (= ,fx ,body))
+ (mem ,fx ,call)))
+
+
+ (defthm ,(packn-in-pkg (list "SUBSETP-" name) 'defmap)
+ (implies (subsetp ,s1 ,s)
+ (subsetp (,name ,@(put-nth s1 sloc vars))
+ ,call)))
+
+ ,@(defmap-congruences vars call (+ sloc 1) 1)
+
+ (defthm ,(packn-in-pkg (list "CARDINALITY-" name) 'defmap)
+ (<= (cardinality ,call)
+ (cardinality ,s))
+ :rule-classes :linear)
+
+ (defthm ,(packn-in-pkg (list "UNION-" name) 'defmap)
+ (= (,name ,@(put-nth `(union ,s1 ,s) sloc vars))
+ (union (,name ,@(put-nth s1 sloc vars))
+ ,call)))
+
+; Once I thought that
+; (image (intersection s1 s)) = (intersection (image s1) (image s))
+; But this is wrong. Consider
+; s1 = {(0 . 1) (0 . 2)}
+; s = {(1 . 1) (1 . 2)}
+; let (body e) = (cdr e) (or (tl e) if the elements are pairps)
+; Then the lhs is nil because the two sets are disjoint, but the
+; rhs is {1 2}.
+
+ (defthm ,(packn-in-pkg (list "INTERSECTION-" name) 'defmap)
+ (subsetp (,name ,@(put-nth `(intersection ,s1 ,s) sloc vars))
+ (intersection (,name ,@(put-nth s1 sloc vars))
+ ,call)))
+
+ )))))
+
+#|
+; Here are examples of both styles of defmap:
+
+(defstub bd (a x b) t)
+(acl2::skip-proofs
+ (progn (defcong = = (bd a x b) 1)
+ (defcong = = (bd a x b) 2)
+ (defcong = = (bd a x b) 3)))
+
+(defmap subset (a s b) :for x :in s :such-that (bd a x b))
+(defmap image (a s b) :for x :in s :map (bd a x b))
+
+|#
+
diff --git a/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory.acl2 b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory.acl2
new file mode 100644
index 0000000..cbe122f
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory.acl2
@@ -0,0 +1,24 @@
+(value :q)
+
+(LP)
+
+(defpkg "S"
+ (set-difference-equal
+ (union-eq '(PACK
+ ORDINARYP
+ <<
+ <<-IRREFLEXIVITY
+ <<-TRICHOTOMY
+ <<-MUTUAL-EXCLUSION
+ <<-TRANSITIVITY
+ FAST-<<-TRICHOTOMY
+ FAST-<<-MUTUAL-EXCLUSION
+ FAST-<<-TRANSITIVITY
+ FAST-<<-RULES
+ SLOW-<<-RULES
+ <<-RULES)
+ (union-eq *acl2-exports*
+ *common-lisp-symbols-from-main-lisp-package*))
+ '(union intersection subsetp add-to-set functionp = apply)))
+
+(certify-book "set-theory" ? t)
diff --git a/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory.lisp b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory.lisp
new file mode 100644
index 0000000..6108bb5
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory.lisp
@@ -0,0 +1,3232 @@
+; Finite Set Theory for ACL2
+; Copyright (C) 2001 Georgia Institute of Technology
+
+; This book is derived from the book "set-theory-original" by J Moore,
+; which is included in this directory. The only difference between
+; this version and J Moore's version is that I use the book
+; "total-ordering" also in this directory instead of the orginal
+; "total-ordering-original". This allows me to simplify some of the
+; theorems and to also remove theorems.
+
+; 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 License
+; along with this program; if not, write to the Free Software
+; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
+
+; Written by: Panagiotis Manolios
+; email: manolios@cc.gatech.edu
+; College of Computing
+; CERCS Lab
+; Georgia Institute of Technology
+; 801 Atlantic Drive
+; Atlanta, Georgia 30332-0280 U.S.A.
+
+(in-package "S")
+
+(include-book "total-ordering")
+
+(defun ur-elementp (x)
+ (or (atom x)
+ (eq (car x) :UR-CONS)))
+
+; Example objects are
+; 3 numbers
+; #\A characters
+; "Abc" strings
+; ABC symbols
+; (:UR-CONS (a b c)) lists
+; (1 2 1 3 (:UR-CONS (a b c))) sets
+
+; Some Comments on :UR-CONS
+
+; It is simplest never to write the symbol :UR-CONS in your sets
+; unless you mean to mark consp ur-elements. The symbol :UR-CONS if
+; encountered in unexpected places produces counter-intuitive results.
+
+; For example, (1 2 :UR-CONS) might be thought of as {1 2 :UR-CONS}
+; but in fact is {1 2}. The reason is that it is parsed as (1 2
+; . (:UR-CONS)). The enumeration of the elements of a set is
+; terminated by the first ur-element cdr. So just as (1 2 . 3) is {1
+; 2}, so is (1 2 . (:UR-CONS ...)). Any attempt to include :UR-CONS
+; as an element of an explicit set constant terminates the enumeration
+; of the set elements and so fails to include :UR-CONS as an element.
+
+; Is it possible to use scons to add :UR-CONS to a list? You might
+; expect (scons :UR-CONS '(1 2)) to be {:UR-CONS 1 2}. But it is in
+; fact {CONS 1 2}. If you ever succeed in using :UR-CONS as an
+; ur-element it is treated as though it were a non-canonical
+; representation of the symbol ACL2::CONS.
+
+; These considerations make it simplest to avoid using :UR-CONS except
+; in the syntax of sets.
+
+(defun set-insert (e s)
+
+; NIL is the only ur-elementp upon which set-insert is ever called, in
+; the process of canonicalizing. But I prove theorems about
+; set-insert and to make them simpler to state, I have it treat all
+; ur-elements s as the empty set. Also, both e and s are assumed to
+; be canonical.
+
+ (cond ((ur-elementp s) (cons e nil))
+ ((equal e (car s)) s)
+ ((<< e (car s))
+ (cons (car s)
+ (set-insert e (cdr s))))
+ (t (cons e s))))
+
+(defun ur-fix (x)
+
+; This converts an arbitrary Lisp object into an ordinary ur-element
+; without changing the type. We do not want to change the type so
+; that set equality refines IFF and is a congruence relation for the
+; arithmetic primitives in ACL2. We discuss the conversions below.
+
+ (cond ((atom x)
+ (cond ((eq x :UR-CONS) 'ACL2::UR-CONS)
+ (t x)))
+ ((eq (car x) :UR-CONS)
+ (cond ((or (atom (cdr x))
+ (atom (cadr x)))
+ '(:UR-CONS (NIL)))
+ (t (list :UR-CONS (cadr x)))))
+ (t nil)))
+
+; Conversions:
+; (1) If we encounter :UR-CONS where an ur-element is expected, we convert it
+; the symbol ACL2::UR-CONS. This prevents the accidental formation of
+; a :UR-CONS by set operations on data containing :UR-CONS. For example,
+; (scons :UR-CONS '(a b c)) will produce the set {ACL2::UR-CONS a b c}, not
+; the set {:UR-CONS a b c} and not the ``ur-element'' (:UR-CONS a b c).
+; (2) If we encounter (:UR-CONS . xxx) where an ur-element is expected, we
+; are sure to return something of the form (:UR-CONS (...)). An ur-element
+; marked :UR-CONS means a cons of some sort, no matter what is inside.
+; A rough model of the conversion rule is that if the :UR-CONS expression
+; is ill-formed it denotes (:UR-CONS (NIL)). More accurately, there are
+; three cases:
+; (a) (:UR-CONS . atom) => (:UR-CONS (NIL))
+; (b) (:UR-CONS atom . anything) => (:UR-CONS (NIL))
+; (c) (:UR-CONS (...) . anything) => (:UR-CONS (...))
+
+
+; (in-theory (disable ur-fix))
+
+(defun canonicalize (x)
+ (cond ((ur-elementp x) (ur-fix x))
+ ((ur-elementp (cdr x))
+ (list (canonicalize (car x))))
+ (t (set-insert (canonicalize (car x))
+ (canonicalize (cdr x))))))
+
+
+(defun orderedp (x)
+ (cond ((ur-elementp x) t)
+ ((ur-elementp (cdr x)) t)
+ ((<< (cadr x) (car x))
+ (orderedp (cdr x)))
+ (t nil)))
+
+(defun canonicalp (x)
+ (cond ((atom x)
+ (not (eq x :UR-CONS)))
+ ((eq (car x) :UR-CONS)
+ (and (consp (cdr x))
+ (consp (cadr x))
+ (equal (cddr x) nil)))
+ ((ur-elementp (cdr x))
+ (and (canonicalp (car x))
+ (equal (cdr x) nil)))
+ (t (and (canonicalp (car x))
+ (canonicalp (cdr x))
+ (orderedp x)))))
+
+(defthm orderedp-set-insert
+ (implies (and (canonicalp e)
+ (canonicalp a))
+ (orderedp (set-insert e a)))
+ :hints (("Goal" :induct (set-insert e a))))
+
+(defthm canonicalp-set-insert
+ (implies (and (canonicalp e)
+ (canonicalp a))
+ (canonicalp (set-insert e a)))
+ :hints (("Goal" :induct (set-insert e a))))
+
+(defthm canonicalp-ur-fix
+ (canonicalp (ur-fix X)))
+
+(defthm canonicalp-canonicalize
+ (canonicalp (canonicalize x)))
+
+(defthm canonicalize-canonicalp
+ (implies (canonicalp x) (equal (canonicalize x) x)))
+
+; So here is equality in our system.
+
+(defun = (x y)
+ (equal (canonicalize x)
+ (canonicalize y)))
+
+(defequiv =)
+
+; ----------------------------------------------------------------------------
+; The Set Constructor/Destructor Primitives
+
+; It is very convenient to pretend that sets are built as a new data
+; type. So here are the basic functions. I will keep them enabled
+; until I have proved the necessary facts about canonicalization,
+; equality (=) and subsetp. Then I'll disable them. But I introduce
+; them now so that mem and subsetp can be defined in terms of them. I
+; have also collected together certain of their elementary properties.
+; Most of these theorems are not used until after I have disabled
+; these primitives.
+
+(defun sfix (a)
+ (if (ur-elementp a)
+ nil
+ a))
+
+(defun scons (e a)
+ (if (equal e :UR-CONS)
+ (cons (canonicalize e)
+ (sfix a))
+ (cons e (sfix a))))
+
+; The macro below allows me to write (brace a b c) to mean {a, b, c}.
+
+(defmacro brace (&rest args)
+ (cond ((endp args) nil)
+ (t `(scons ,(car args)
+ (brace ,@(cdr args))))))
+
+; Here are some timings of this entire library. These timings started
+; when I began experimenting with three different flavors of scar and
+; scdr. The flavors are shown below along with some Caerlaverock
+; timings. I chose functionp1-set-insert as a representative expensive
+; proof.
+
+; When these timings were done, there were 279 events and the last one
+; was APPLY-RESTRICT. Since the book has probably changed since then,
+; these timings are only relevant insofar as they reflect the relative
+; effects of the various experiments. Even that claim is suspect:
+; since doing these timings I have discovered that there can be a
+; considerable difference (30%) between the time it takes in a fresh
+; GCL and the time it takes to ``repeat'' the computation in a soiled
+; GCL. Fresh GCL is faster. I did not record whether the times below
+; were done in fresh system or not.
+
+; During the first three experiments, I had the <<-rules -- namely <<,
+; transitivity, mutual-exclusion, and trichotomy -- disabled by
+; default and turned them on during certain proofs. They were on
+; during functionp1-set-insert, even though I eventually discovered
+; they didn't have to be for the proof to go through.
+
+; functionp1-set-insert entire file
+
+(defun scar (a)
+; (car a) ;;; 232 secs 1153 secs
+; (if (equal (car a) :UR-CONS) nil (car a)) ;;; 404 secs 1212 secs
+ (if (ur-elementp a) nil (car a)) ;;; 308 secs 1239 secs
+ )
+
+; I then learned that I did not have to have <<-rules enabled during
+; the functionp1-set-insert proof or the analogous ones. So I took out
+; those theory commands and got:
+
+; ;;; 2 secs 889 secs
+
+; Then I had the idea of coding up the ``fast << rules.'' Operating
+; in the fast-<<-rules theory by default and occasionally either
+; enabling << or switching over to the slow-<<-rules, I got the
+; following times in a fresh GCL:
+
+; ;;; 2 secs 370 secs
+
+
+(defun scdr (a)
+; (sfix (cdr a))
+; (if (equal (car a) :UR-CONS) nil (sfix (cdr a)))
+ (if (ur-elementp a) nil (sfix (cdr a)))
+ )
+
+(defcong = = (scons e a) 1
+ :hints (("Goal" :in-theory (enable =))))
+
+(defcong = = (scons e a) 2
+ :hints (("Goal" :in-theory (enable =))))
+
+(defthm scar-scons
+ (= (scar (scons e a)) e))
+
+(defthm scdr-scons
+ (= (scdr (scons e a)) (sfix a)))
+
+(defthm ur-elementp-scar
+ (implies (ur-elementp x) (equal (scar x) nil)))
+
+(defthm ur-elementp-scdr
+ (implies (ur-elementp x) (equal (scdr x) nil)))
+
+(defun setp (x)
+ (or (equal x nil)
+ (not (ur-elementp x))))
+
+(defthm setp-scdr
+ (setp (scdr a))
+ :rule-classes (:type-prescription :generalize))
+
+(defthm scons-scar-scdr
+ (implies (not (ur-elementp a))
+ (= (scons (scar a) (scdr a)) a))
+ :rule-classes :elim)
+
+(defthm acl2-count-scdr
+ (implies (not (ur-elementp a))
+ (o< (acl2-count (scdr a))
+ (acl2-count a)))
+ :rule-classes
+ ((:built-in-clause)
+ (:linear :corollary
+ (implies (not (ur-elementp a))
+ (< (acl2-count (scdr a))
+ (acl2-count a))))))
+
+(defthm consp-set-insert
+ (consp (set-insert e a))
+ :rule-classes :type-prescription)
+
+(defthm car-set-insert-not-equal-ur-cons
+ (implies (and (canonicalp e)
+ (canonicalp a))
+ (not (equal (set-insert e a) (cons :UR-CONS x)))))
+
+(defcong = equal (ur-elementp x) 1)
+
+; Note: We will generally keep sfix enabled, so this rule will not be
+; of much use.
+
+(defcong = = (sfix x) 1)
+
+(defthm not-ur-elementp-scons
+ (not (ur-elementp (scons e a))))
+
+(defthm not-consp-implies-ur-elementp
+ (implies (not (consp e))
+ (ur-elementp e)))
+
+(defthm scons-nil
+ (implies (and (syntaxp (not (equal a ''nil)))
+ (ur-elementp a))
+ (= (scons e a)
+ (scons e nil))))
+
+(defthm canonicalize-ur-cons
+ (not (equal (canonicalize x) :UR-CONS)))
+
+(defthm set-insert-set-insert
+ (implies (and (canonicalp e)
+ (canonicalp d)
+ (canonicalp a))
+ (equal (set-insert e (set-insert d a))
+ (set-insert d (set-insert e a))))
+ :hints (("Goal" :induct (set-insert e a)
+ :in-theory (slow-<<-rules))))
+
+; This rule lets us do a cross-fertilization without waiting for the
+; prior elim. The version of this rule that rewrites (set-insert e xxx)
+; to (set-insert d (set-insert e a)) has been known to cause infinite
+; loops, even with a hand-picked :loop-stopper.
+
+(defthm set-insert-short-cut
+ (implies (and (equal xxx (set-insert d a))
+ (canonicalp e)
+ (canonicalp d)
+ (canonicalp a))
+ (equal (equal (set-insert e xxx)
+ (set-insert d (set-insert e a)))
+ t)))
+
+(defthm set-insert-dup
+ (implies (and (canonicalp e)
+ (canonicalp a))
+ (equal (set-insert e (set-insert e a))
+ (set-insert e a)))
+ :hints (("Goal" :induct (set-insert e a))))
+
+(defthm scons-scons-2
+ (= (scons e (scons d a))
+ (scons d (scons e a))))
+
+(defthm scons-scons-1
+ (= (scons e (scons e a))
+ (scons e a)))
+
+(defthm equal-singleton-set-insert
+ (implies (and (canonicalp e)
+ (canonicalp d)
+ (canonicalp a))
+ (equal (equal (list e) (set-insert d a))
+ (and (equal e d)
+ (or (equal (sfix a) nil)
+ (equal (list e) a)))))
+ :hints (("Goal" :induct (set-insert d a))))
+
+(defthm car-set-insert
+ (implies (and (canonicalp e)
+ (canonicalp a))
+ (equal (car (set-insert e a))
+ (if (ur-elementp a)
+ e
+ (if (<< (car a) e)
+ e
+ (car a)))))
+ :hints (("Goal"
+ :induct (set-insert e a)
+ :in-theory (enable ur-elementp))))
+
+(defthm =-singletons
+ (equal (= (scons e nil) (scons d a))
+ (and (= e d)
+ (or (ur-elementp a)
+ (= (scons e nil) a))))
+ :hints (("Goal" :in-theory (enable = scons ur-elementp)))
+ :rule-classes
+ ((:rewrite)
+ (:rewrite :corollary
+ (equal (= (scons d a) (scons e nil))
+ (and (= e d)
+ (or (ur-elementp a)
+ (= (scons e nil) a))))
+
+; Note: This hint is required here because we do not know that
+; = is commutative (except by opening it up)!
+
+ :hints (("Goal" :in-theory (enable =))))))
+
+; Basic...
+(defun <<-cons-1-hint (x y)
+ (if (consp x)
+ (list (<<-cons-1-hint (car x) (cdr x)))
+ y))
+
+(defthm <<-cons-1
+ (<< x (cons x y))
+ :hints (("Goal" :induct (<<-cons-1-hint x y)
+ :in-theory (cons 'acl2::lexorder (slow-<<-rules <<)))))
+
+(defthm not-=-x-set-insert-x
+ (implies (and (canonicalp e)
+ (canonicalp x))
+ (not (equal e (set-insert e x))))
+ :hints (("Goal" :in-theory (cons 'ur-elementp
+ (slow-<<-rules)))))
+
+(defthm not-=-x-scons-x
+ (not (= e (scons e x)))
+ :hints (("Goal" :in-theory (enable = scons ur-elementp)))
+ :rule-classes
+ ((:rewrite)
+ (:rewrite :corollary (not (= (scons e x) e)))))
+
+; ----------------------------------------------------------------------------
+; Set Membership and the Subset Relation
+
+(defun mem (e a)
+ (cond ((ur-elementp a) nil)
+ (t (or (= e (scar a))
+ (mem e (scdr a))))))
+
+(defun subsetp (a b)
+ (cond ((ur-elementp a) t)
+ (t (and (mem (scar a) b)
+ (subsetp (scdr a) b)))))
+
+; I now prove that = is a congruence for both arguments of mem. The
+; proof for the first argument is easy because (mem e s) only uses
+; (canonicalize e). [So, if (canonicalize e) is (canonicalize e')
+; it is obvious that (mem e s) is (mem e' s).]
+
+; The proof for the second argument is harder and works this way. We
+; will establish that (mem e (canonicalize s)) is the same as (mem e
+; s). Suppose that is proved. Then suppose (= s s'). That is,
+; (canonicalize s) is (canonicalize s'). We must show that (mem e s)
+; is (mem e s'). Use the theorem to replace each by (mem e
+; (canonicalize s)) and (mem e (canonicalize s')), then substitute.
+
+; Even though I don't need it, I will prove the following for regularity.
+
+(defthm mem-canonicalize-1
+ (equal (mem (canonicalize e) a)
+ (mem e a)))
+
+; We need to little lemmas to do the second argument.
+
+; In the lemma below we must assume that the arguments to set-insert
+; are canonical. That is because it really compares using EQUAL.
+; When we use the lemma it will be on canonicalized arguments.
+
+(defthm mem-set-insert
+ (implies (and (canonicalp d)
+ (canonicalp a))
+ (equal (mem e (set-insert d a))
+ (or (= e d)
+ (mem e a))))
+ :hints (("Goal"
+ :induct (set-insert d a))))
+
+; Here is the second lemma.
+
+(defthm mem-canonicalize-2
+ (equal (mem e (canonicalize a))
+ (mem e a)))
+
+(defcong = equal (mem e a) 1)
+
+(defcong = equal (mem e a) 2
+ :hints (("Goal" :in-theory (disable mem-canonicalize-2)
+ :use ((:instance mem-canonicalize-2
+ (e e)
+ (a a))
+ (:instance mem-canonicalize-2
+ (e e)
+ (a a-equiv))))))
+
+
+; Now I repeat it for subsetp. The first argument of subsetp is the
+; harder, because we are recursing down it. The second argument is
+; easy and follows from what we already know about mem.
+
+(defthm subsetp-set-insert-1
+ (implies (and (canonicalp e)
+ (canonicalp a))
+ (equal (subsetp (set-insert e a) b)
+ (and (mem e b)
+ (subsetp a b))))
+ :hints (("Goal" :induct (set-insert e a))))
+
+(defthm subsetp-canonicalize-1
+ (equal (subsetp (canonicalize a) b)
+ (subsetp a b))
+ :hints (("Goal" :induct (subsetp a b))))
+
+(defcong = equal (subsetp a b) 1
+ :hints (("Goal"
+ :in-theory (disable subsetp-canonicalize-1)
+ :use ((:instance subsetp-canonicalize-1
+ (a a)
+ (b b))
+ (:instance subsetp-canonicalize-1
+ (a a-equiv)
+ (b b))))))
+
+(defcong = equal (subsetp a b) 2
+ :hints (("Goal" :in-theory (disable =))))
+
+; For regularity:
+
+(defthm subsetp-canonicalize-2
+ (equal (subsetp a (canonicalize b))
+ (subsetp a b)))
+
+; Next, I will prove the key facts about subsetp.
+
+(defthm subsetp-cons
+ (implies (and (not (equal e :UR-CONS))
+ (subsetp a b))
+ (subsetp a (cons e b))))
+
+(defthm subsetp-x-x
+ (subsetp x x))
+
+(in-theory (disable =))
+
+(defthm mem-subsetp
+ (implies (and (mem e a)
+ (subsetp a b))
+ (mem e b)))
+
+(defthm transitivity-of-subsetp
+ (implies (and (subsetp a b)
+ (subsetp b c))
+ (subsetp a c)))
+
+; ----------------------------------------------------------------------------
+; The Canonicality Theorem
+
+; Finally, I want to establish the key fact about equality and subset,
+; namely, that two sets are = iff they are subsets of eachother.
+
+; If (= a b), then it is obvious that (subsetp a b) and vice versa,
+; given the congruence rules above.
+
+; Suppose therefore that (subsetp a b) and (subsetp b a). We
+; prove (= a b). The proof relies on the fact that << is a total
+; ordering.
+
+; Proof. Let ca and cb be (canonicalize a) and (canonicalize b).
+; Observe that they are both ordinary. By the subsetp-canonicalize-i
+; lemmas we know that (subsetp ca cb) and (subsetp cb ca). We will
+; prove that (subsetp ca cb) implies (not (<< cb ca)). Thus,
+; ca equals cb. Q.E.D.
+
+(defthm =-is-equal
+ (implies (and (canonicalp x)
+ (canonicalp y))
+ (equal (= x y)
+ (equal x y)))
+ :hints (("Goal" :in-theory (enable =))))
+
+; I do not want to further encumber << with another rule. But this
+; is an important fact and I will :use it.
+
+(defthm mem-<<
+ (implies (and (canonicalp e)
+ (canonicalp a)
+ (mem e a))
+ (<< e a))
+ :rule-classes nil
+ :hints (("Goal" :in-theory (slow-<<-rules <<))))
+
+(defthm not-mem-e-e
+ (not (mem e e))
+ :hints (("Goal"
+ :use (:instance MEM-<<
+ (e (canonicalize e))
+ (a (canonicalize e))))))
+
+; This rule seems overly expensive so I keep it disabled most of the time.
+
+(defthm mem-container
+ (implies (mem e a)
+ (not (mem a e)))
+ :hints (("Goal"
+ :use ((:instance mem-<<
+ (e (canonicalize e))
+ (a (canonicalize a)))
+ (:instance mem-<<
+ (a (canonicalize e))
+ (e (canonicalize a)))))))
+
+(in-theory (disable mem-container))
+
+(defthm mem-implies-not-<<-car
+ (implies (and (canonicalp e)
+ (canonicalp a)
+ (mem e a))
+ (not (<< (car a) e)))
+ :hints (("Goal" :in-theory (slow-<<-rules <<))))
+
+(defthm <<-cons
+ (implies (and (canonicalp e)
+ (canonicalp a)
+ (mem e a))
+ (equal (<< a (cons e z))
+ (if (equal (car a) e)
+ (<< (cdr a) z)
+ nil)))
+ :hints (("Goal" :in-theory (enable <<) ; (fast-<<-rules <<)
+ )))
+
+(defthm subsetp-cons-reversed
+ (implies (and (subsetp a (cons e b))
+ (not (equal e :UR-CONS))
+ (not (mem e a)))
+ (subsetp a b)))
+
+(defthm yucko
+ (implies (and (canonicalp a)
+ (canonicalp b)
+ (subsetp a b)
+ (mem (car b) a))
+ (equal (car a) (car b)))
+ :rule-classes nil)
+
+(defthm subsetp-<<
+ (implies (and (setp a)
+ (setp b)
+ (canonicalp a)
+ (canonicalp b)
+ (subsetp a b))
+ (not (<< b a)))
+ :rule-classes nil
+ :hints (("Goal" :induct (<< b a))
+ ("Subgoal *1/5.3"
+ :use (:instance yucko
+ (a (cdr a))
+ (b b)))
+ ("Subgoal *1/4''" :in-theory (enable <<) ; (fast-<<-rules <<)
+ )))
+
+(defthm setp-canonicalize
+ (implies (setp x)
+ (setp (canonicalize x))))
+
+; The Canonalicality Theorem:
+(defthm =-iff-subsetps
+ (implies (and (setp a)
+ (setp b))
+ (iff (= a b)
+ (and (subsetp a b)
+ (subsetp b a))))
+ :rule-classes nil
+ :hints
+ (("Goal"
+ :in-theory (union-theories '(=)
+ (disable subsetp-canonicalize-1
+ subsetp-canonicalize-2
+ canonicalize
+ setp
+ transitivity-of-subsetp))
+
+ :use ((:instance subsetp-canonicalize-1
+ (a a)
+ (b b))
+ (:instance subsetp-canonicalize-2
+ (a (canonicalize a))
+ (b b))
+ (:instance subsetp-canonicalize-1
+ (a b)
+ (b a))
+ (:instance subsetp-canonicalize-2
+ (a (canonicalize b))
+ (b a))
+ (:instance subsetp-<<
+ (a (canonicalize a))
+ (b (canonicalize b)))
+ (:instance subsetp-<<
+ (a (canonicalize b))
+ (b (canonicalize a)))))))
+
+; Now we disable those of the above rules that we don't think are
+; worth their cost.
+
+(in-theory (disable =-is-equal
+ mem-implies-not-<<-car
+ <<-cons))
+
+;----------------------------------------------------------------------------
+; = Refines iff and is a Congruence for Many ACL2 Functions
+
+
+(defcong = equal (canonicalize x) 1
+ :hints (("Goal" :in-theory (enable =))))
+
+(defthm canonicalize-=
+ (= (canonicalize x) x)
+ :hints (("Goal" :in-theory (enable =))))
+
+(defthm canonicalize-non-nil
+ (iff (canonicalize x) x)
+ :hints (("Goal" :in-theory (enable ur-elementp))))
+
+(defrefinement = iff
+ :hints (("Goal" :in-theory (enable =))))
+
+(defthm canonicalize-fix
+ (equal (canonicalize (fix x))
+ (fix (canonicalize x)))
+ :rule-classes nil
+ :hints (("Goal" :in-theory (enable ur-elementp))))
+
+(defthm <-fixes
+ (equal (< x y) (< (fix x) (fix y)))
+ :rule-classes nil)
+
+(defcong = equal (< x y) 1
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =) '(fix))
+ :use ((:instance <-fixes
+ (x x)
+ (y y))
+ (:instance <-fixes
+ (x x-equiv)
+ (y y))
+ (:instance canonicalize-fix
+ (x x))
+ (:instance canonicalize-fix
+ (x x-equiv))))))
+
+(defcong = equal (< x y) 2
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =) '(fix))
+ :use ((:instance <-fixes
+ (x x)
+ (y y))
+ (:instance <-fixes
+ (x x)
+ (y y-equiv))
+ (:instance canonicalize-fix
+ (x y))
+ (:instance canonicalize-fix
+ (x y-equiv))))))
+
+(defthm +-fixes
+ (equal (+ x y) (+ (fix x) (fix y)))
+ :rule-classes nil)
+
+(defcong = equal (+ x y) 1
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =) '(fix))
+ :use ((:instance +-fixes
+ (x x)
+ (y y))
+ (:instance +-fixes
+ (x x-equiv)
+ (y y))
+ (:instance canonicalize-fix
+ (x x))
+ (:instance canonicalize-fix
+ (x x-equiv))))))
+
+(defcong = equal (+ x y) 2
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =) '(fix))
+ :use ((:instance +-fixes
+ (x x)
+ (y y))
+ (:instance +-fixes
+ (x x)
+ (y y-equiv))
+ (:instance canonicalize-fix
+ (x y))
+ (:instance canonicalize-fix
+ (x y-equiv))))))
+
+(defthm --fixes
+ (equal (- x) (- (fix x)))
+ :rule-classes nil)
+
+(defcong = equal (- x) 1
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =) '(fix))
+ :use ((:instance --fixes
+ (x x))
+ (:instance --fixes
+ (x x-equiv))
+ (:instance canonicalize-fix
+ (x x))
+ (:instance canonicalize-fix
+ (x x-equiv))))))
+
+
+(defthm *-fixes
+ (equal (* x y) (* (fix x) (fix y)))
+ :rule-classes nil)
+
+(defcong = equal (* x y) 1
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =) '(fix))
+ :use ((:instance *-fixes
+ (x x)
+ (y y))
+ (:instance *-fixes
+ (x x-equiv)
+ (y y))
+ (:instance canonicalize-fix
+ (x x))
+ (:instance canonicalize-fix
+ (x x-equiv))))))
+
+(defcong = equal (* x y) 2
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =) '(fix))
+ :use ((:instance *-fixes
+ (x x)
+ (y y))
+ (:instance *-fixes
+ (x x)
+ (y y-equiv))
+ (:instance canonicalize-fix
+ (x y))
+ (:instance canonicalize-fix
+ (x y-equiv))))))
+
+(defthm integerp-canonicalize
+ (equal (integerp (canonicalize x))
+ (integerp x)))
+
+(defthm rationalp-canonicalize
+ (equal (rationalp (canonicalize x))
+ (rationalp x)))
+
+(defthm symbolp-canonicalize
+ (equal (symbolp (canonicalize x))
+ (symbolp x)))
+
+(defthm stringp-canonicalize
+ (equal (stringp (canonicalize x))
+ (stringp x)))
+
+(defthm characterp-canonicalize
+ (equal (characterp (canonicalize x))
+ (characterp x)))
+
+(defthm consp-canonicalize
+ (equal (consp (canonicalize x))
+ (consp x))
+ :hints (("Goal" :in-theory (enable ur-elementp))))
+
+(defcong = equal (integerp x) 1
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =)
+ '(integerp-canonicalize))
+ :use ((:instance integerp-canonicalize
+ (x x))
+ (:instance integerp-canonicalize
+ (x x-equiv))))))
+
+(defcong = equal (rationalp x) 1
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =)
+ '(rationalp-canonicalize))
+ :use ((:instance rationalp-canonicalize
+ (x x))
+ (:instance rationalp-canonicalize
+ (x x-equiv))))))
+
+(defcong = equal (symbolp x) 1
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =)
+ '(symbolp-canonicalize))
+ :use ((:instance symbolp-canonicalize
+ (x x))
+ (:instance symbolp-canonicalize
+ (x x-equiv))))))
+
+(defcong = equal (stringp x) 1
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =)
+ '(stringp-canonicalize))
+ :use ((:instance stringp-canonicalize
+ (x x))
+ (:instance stringp-canonicalize
+ (x x-equiv))))))
+
+(defcong = equal (consp x) 1
+ :hints (("Goal"
+ :in-theory (set-difference-theories (enable =)
+ '(consp-canonicalize))
+ :use ((:instance consp-canonicalize
+ (x x))
+ (:instance consp-canonicalize
+ (x x-equiv))))))
+
+
+; We do not get (defcong = equal (characterp x) 1) because we
+; canonicalize non-standard atoms to (code-char 255).
+
+; ----------------------------------------------------------------------------
+; Codified Theorem Proving Strategies
+
+; The following all turn into the corresponding defthms:
+; (defx name term)
+; (defx name term :hints ... :rule-classes ...)
+
+; But if you write
+; (defx ...a... :strategy xxx ...b...)
+; it macro expands to
+; (xxx ...a... ...b...)
+
+; Thus, if you want to codify a new theorem proving strategy xxx, you can
+; defmacro xxx and then write (defx ... :strategy xxx ...).
+
+; The main point of this is to let me write defx events and introduce
+; new strategies as I go. Also, I can name my strategies without
+; including ``def'' in front of them and still search for ``(def...''
+; when looking for things.
+
+(defun packn-in-pkg (lst pkg-witness)
+ (declare (xargs :mode :program))
+ (acl2::intern-in-package-of-symbol (coerce (acl2::packn1 lst) 'string)
+ pkg-witness))
+
+(defmacro defx (&rest args)
+ (let ((temp (member :strategy args)))
+
+; We allow the strategy to be a keyword, in which case we convert it
+; to the corresponding symbol in this package. If the strategy is not
+; a keyword, it is used as supplied.
+
+ (cond
+ (temp
+ `(,(if (keywordp (cadr temp))
+ (packn-in-pkg (list (symbol-name (cadr temp))) 'defx)
+ (cadr temp))
+ ,@(butlast args (length temp))
+ ,@(cddr temp)))
+ (t `(defthm ,@args)))))
+
+; ----------------------------------------------------------------------------
+; Proving Congruences
+
+; There are two common ways to prove congruence rules in this theory.
+
+; (1) The :canonicalize strategy: prove that (fn (canonicalize x)) is
+; (fn x). This is generally used if fn returns an ur-element (as
+; opposed to a set).
+
+; (2) The :subsetp stragegy: prove that (subsetp a1 a2) implies
+; (subsetp (fn a1) (fn a2)). This is generally used if fn returns a
+; set.
+
+(defun genname1 (name n avoid)
+ (declare (xargs :mode :program))
+ (let ((new-name (packn-in-pkg (list name n) name)))
+ (cond ((acl2::member-equal new-name avoid)
+ (genname1 name (+ 1 n) avoid))
+ (t new-name))))
+
+(defun genname (name avoid)
+ (declare (xargs :mode :program))
+ (cond ((acl2::member-equal name avoid)
+ (genname1 name 1 avoid))
+ (t name)))
+
+(defun put-nth (e n lst)
+ (cond ((zp n) (cons e (cdr lst)))
+ (t (cons (car lst) (put-nth e (- n 1) (cdr lst))))))
+
+; And here is the macro
+
+(defmacro congruence (expr n &key method)
+ (cond
+ ((eq method :canonicalize)
+ (let* ((fn (car expr))
+ (vars (cdr expr))
+ (x (nth (- n 1) vars))
+ (name1
+ (packn-in-pkg (list fn "-SET-INSERT") fn))
+ (name2
+ (packn-in-pkg (list fn "-CANONICALIZE") fn))
+ (vars1 (acl2::remove1-eq x vars)) ; Matt K. mod from delete1-eq, v2-9-4
+ (e (genname 'e vars1))
+ (a (genname x vars1))
+ (x-equiv (packn-in-pkg (list x "-EQUIV") x)))
+ `(encapsulate
+ nil
+ (local (in-theory (enable scons scar scdr ur-elementp)))
+
+ (defthm ,name1
+ (implies (and (canonicalp ,e)
+ (canonicalp ,a))
+ (equal (,fn ,@(put-nth `(set-insert ,e ,a)
+ (- n 1)
+ vars))
+ (,fn ,@(put-nth `(cons ,e ,a)
+ (- n 1)
+ vars))))
+ :hints (("Goal"
+ :induct (set-insert ,e ,a)
+
+; Note that the following in-theory is commented out! I learned that
+; if you enable = during these proofs it is generally slower. So I
+; don't.
+; :in-theory (enable =)
+
+
+ )))
+
+ (defthm ,name2
+ (equal (,fn ,@(put-nth `(canonicalize ,x)
+ (- n 1)
+ vars))
+ (,fn ,@vars)))
+
+ (defcong = equal ,expr ,n
+ :hints
+ (("Goal"
+ :in-theory (disable ,name2)
+ :use ((:instance ,name2 (,x ,x))
+ (:instance ,name2
+ (,x ,x-equiv)))))))))
+ ((eq method :subsetp)
+ (let* ((fn (car expr))
+ (vars (cdr expr))
+ (x (nth (- n 1) vars))
+ (name1
+ (packn-in-pkg (list "SUBSETP-" fn "-" fn) fn))
+ (vars1 (acl2::remove1-eq x vars)) ; Matt K. mod from delete1-eq, v2-9-4
+ (a1 (genname1 x 1 vars1))
+ (a2 (genname1 x 2 (cons a1 vars1)))
+ (x-equiv (packn-in-pkg (list x "-EQUIV") x)))
+ `(encapsulate
+ nil
+ (defthm ,name1
+ (implies (subsetp ,a1 ,a2)
+ (subsetp (,fn ,@(put-nth a1 (- n 1) vars))
+ (,fn ,@(put-nth a2 (- n 1) vars)))))
+
+ (defcong = = ,expr ,n
+ :hints (("Goal"
+ :use (:instance =-iff-subsetps
+ (a ,expr)
+ (b (,fn ,@(put-nth x-equiv
+ (- n 1)
+ vars))))))))))
+ ((eq method nil)
+ `(defcong = = ,expr ,n))
+ (t `(acl2::er acl2::soft 'congruence
+ "The :method ~x0 is unknown."
+ ',method))))
+
+; ----------------------------------------------------------------------------
+; The User Level Theory
+
+(in-theory (disable scons scar scdr ur-elementp))
+
+; ----------------------------------------------------------------------------
+; Set Union
+
+(defun union (a b)
+ (if (ur-elementp a)
+ (sfix b)
+ (scons (scar a)
+ (union (scdr a) b))))
+
+; My next goal is to prove both
+
+; (defcong = = (union a b) 1)
+; (defcong = = (union a b) 2)
+
+; The first of these is problematic but the second is easy.
+; Generally, if the congruence rule is in a slot that is held fixed in
+; the recursion (as in the second case above), the proof is an easy
+; induction, using congruence rules for the subfunctions. But if the
+; congruence rule is in a controller slot, you generally need lemmas.
+
+(defthm mem-union
+ (equal (mem e (union a b))
+ (or (mem e a)
+ (mem e b))))
+
+(defthm subsetp-scons
+ (implies (subsetp a b)
+ (subsetp a (scons e b))))
+
+(defthm subsetp-union-1
+ (subsetp a (union a b)))
+
+(defthm subsetp-union-2
+ (subsetp a (union b a)))
+
+(defthm subsetp-union
+ (implies (subsetp a1 a2)
+ (subsetp (union a1 b)
+ (union a2 b))))
+(defthm setp-union
+ (setp (union a b)))
+
+(defx :strategy :congruence (union a b) 1 :method :subsetp)
+
+(defx :strategy :congruence (union a b) 2)
+
+(defthm union-right-id
+ (implies (ur-elementp b)
+ (= (union a b) (sfix a))))
+
+(defthm union-scons
+ (= (union a (scons e b))
+ (scons e (union a b))))
+
+(defthm commutativity-of-union
+ (= (union a b) (union b a)))
+
+(defthm ur-elementp-union
+ (equal (ur-elementp (union a b))
+ (and (ur-elementp a)
+ (ur-elementp b))))
+
+(defthm associativity-of-union
+ (= (union (union a b) c)
+ (union a (union b c))))
+
+
+; ----------------------------------------------------------------------------
+; Set Intersection
+
+(defun intersection (a b)
+ (if (ur-elementp a)
+ nil
+ (if (mem (scar a) b)
+ (scons (scar a)
+ (intersection (scdr a) b))
+ (intersection (scdr a) b))))
+
+(defthm mem-intersection
+ (equal (mem e (intersection a b))
+ (and (mem e a)
+ (mem e b))))
+
+(defthm subsetp-intersection-1
+ (subsetp (intersection a b) a))
+
+(defthm subsetp-intersection-2
+ (subsetp (intersection b a) a))
+
+(defthm subsetp-intersection
+ (implies (subsetp a1 a2)
+ (subsetp (intersection a1 b)
+ (intersection a2 b))))
+
+(defthm setp-intersection
+ (setp (intersection a b)))
+
+(defx :strategy :congruence (intersection a b) 1 :method :subsetp)
+(defx :strategy :congruence (intersection a b) 2)
+
+(defthm intersection-right-id
+ (implies (ur-elementp b)
+ (= (intersection a b) nil)))
+
+(defthm scons-id
+ (implies (mem e a)
+ (= (scons e a) a)))
+
+(defthm intersection-scons
+ (= (intersection a (scons e b))
+ (if (mem e a)
+ (scons e (intersection a b))
+ (intersection a b))))
+
+(defthm commutativity-of-intersection
+ (= (intersection a b) (intersection b a)))
+
+(defthm associativity-of-intersection
+ (= (intersection (intersection a b) c)
+ (intersection a (intersection b c))))
+
+; ----------------------------------------------------------------------------
+; Arithmetic
+
+(include-book "../../../../../arithmetic/top-with-meta")
+
+
+(defun cardinality (a)
+ (if (ur-elementp a)
+ 0
+ (if (mem (scar a) (scdr a))
+ (cardinality (scdr a))
+ (+ 1 (cardinality (scdr a))))))
+
+(defx :strategy :congruence (cardinality a) 1 :method :canonicalize)
+
+(defthm cardinality-union-2
+ (<= (cardinality b) (cardinality (union a b)))
+ :rule-classes :linear)
+
+; Observe that we proved the easy case first, by induction on b,
+; and then we prove the other case by commutativity.
+
+(defthm cardinality-union-1
+ (<= (cardinality b) (cardinality (union b a)))
+ :rule-classes :linear)
+
+(defthm cardinality-union-3
+ (<= (cardinality (union a b))
+ (+ (cardinality a)
+ (cardinality b)))
+ :rule-classes :linear)
+
+(defthm cardinality-0
+ (equal (equal (cardinality a) 0)
+ (ur-elementp a)))
+
+(defthm cardinality-non-0
+ (implies (mem e x)
+ (< 0 (cardinality x)))
+ :rule-classes :linear)
+
+(defthm cardinality-intersection-1
+ (<= (cardinality (intersection a b)) (cardinality a))
+ :rule-classes :linear)
+
+(defthm cardinality-intersection-2
+ (<= (cardinality (intersection b a)) (cardinality a))
+ :rule-classes :linear)
+
+(defthm cardinality-scons
+ (equal (cardinality (scons e a))
+ (if (mem e a)
+ (cardinality a)
+ (+ 1 (cardinality a)))))
+
+(defthm cardinality-disjoint-union
+ (implies (not (intersection a b))
+ (= (cardinality (union a b))
+ (+ (cardinality a)
+ (cardinality b)))))
+
+
+; ----------------------------------------------------------------------------
+; Choose
+
+(defun choose (a)
+ (car (sfix (canonicalize a))))
+
+(defx :strategy :congruence (choose a) 1)
+
+(defthm ur-elementp-canonicalize
+ (equal (ur-elementp (canonicalize x))
+ (ur-elementp x)))
+
+(defthm mem-choose-lemma
+ (equal (mem (car (canonicalize a)) a)
+ (not (ur-elementp a)))
+ :hints (("Goal"
+ :in-theory (enable scar scdr ur-elementp))))
+
+(defthm mem-choose
+ (equal (mem (choose a) a)
+ (not (ur-elementp a))))
+
+; One might think that the following follows from the previous
+; theorems about choose. But that is not correct. For example,
+; (choose {1 2 3}) might be 2 but (choose {2 3}) might be 3. This
+; property is due to the fact that choose is really the biggest
+; element of the set.
+
+(defthm car-canonicalize-ur-cons
+ (equal (equal (car (canonicalize a)) :UR-CONS)
+ (and (consp a)
+ (equal (car a) :UR-CONS)))
+ :hints (("Goal" :in-theory (enable ur-elementp))))
+
+(defthm choose-scons
+ (implies (not (= (choose (scons e a)) e))
+ (= (choose (scons e a)) (choose a)))
+ :hints (("Goal"
+ :in-theory
+ (enable = scons ur-elementp))))
+
+(defthm choose-singleton
+ (= (choose (scons e nil)) e)
+ :hints (("Goal" :in-theory (enable = scons ur-elementp))))
+
+(in-theory (disable choose))
+
+(defthm elim-choose-singleton
+ (implies (equal (cardinality x) 1)
+ (= (scons (choose x) nil) x)))
+
+(defthm mem-singleton
+ (implies (and (equal (cardinality x) 1)
+ (mem e x))
+ (= (scons e nil) x))
+ :rule-classes nil
+ :hints (("Goal" :in-theory (disable elim-choose-singleton)
+ :use elim-choose-singleton)))
+
+(defthm choose-ur-elementp
+ (implies (ur-elementp x)
+ (= (choose x) nil))
+ :hints (("Goal" :in-theory (enable choose ur-elementp sfix))))
+
+
+; ----------------------------------------------------------------------------
+; Set Difference
+
+(defun diff (a b)
+ (cond ((ur-elementp a)
+ nil)
+ ((mem (scar a) b)
+ (diff (scdr a) b))
+ (t (scons (scar a)
+ (diff (scdr a) b)))))
+
+(defthm mem-diff
+ (equal (mem e (diff a b))
+ (and (mem e a)
+ (not (mem e b)))))
+
+(defthm subsetp-diff-1
+ (subsetp (diff a b) a))
+
+(defthm subsetp-diff
+ (implies (subsetp a1 a2)
+ (subsetp (diff a1 b)
+ (diff a2 b))))
+
+(defthm setp-diff
+ (setp (diff a b)))
+
+(defx :strategy :congruence (diff a b) 1 :method :subsetp)
+(defx :strategy :congruence (diff a b) 2)
+
+(defthm diff-right-id
+ (implies (ur-elementp b)
+ (= (diff a b) (sfix a))))
+
+(defthm cardinality-diff-singleton
+ (equal (cardinality (diff y (scons x nil)))
+ (if (mem x y)
+ (- (cardinality y) 1)
+ (cardinality y))))
+
+(defthm cardinality-diff
+ (<= (cardinality (diff a b)) (cardinality a))
+ :rule-classes :linear)
+
+(defthm diff-nil
+ (implies (subsetp x y)
+ (= (diff x y) nil)))
+
+(defthm diff-scons
+ (implies (not (mem e s))
+ (= (diff s (scons e y)) (diff s y))))
+
+(encapsulate nil
+ (local
+ (defthm scons-x-diff-x
+ (implies (mem x s)
+ (= (scons x (diff s (scons x nil))) s))
+ :hints (("Subgoal *1/3'5'"
+ :cases ((mem sr sr0))))))
+
+ (defthm scons-diff-scons
+ (= (scons e (diff a (scons e nil)))
+ (scons e a))
+ :hints (("Goal" :cases ((mem e a))))))
+
+(defthm elim-choose-doubleton
+ (implies (equal (cardinality x) 2)
+ (= (scons (choose x)
+ (scons (choose (diff x (scons (choose x) nil)))
+ nil))
+ x)))
+
+(defthm subsetp-diff-1-corrollary
+ (implies (subsetp a b)
+ (subsetp (diff a c) b)))
+
+(defthm subsetp-not-subsetp-trick
+ (implies (and (subsetp a b)
+ (not (subsetp a (scdr b))))
+ (mem (scar b) a)))
+
+(defthm intersection-diff-2
+ (= (intersection a (diff b c))
+ (diff (intersection a b) c)))
+
+(defthm intersection-diff-1
+ (= (intersection (diff b c) a)
+ (diff (intersection a b) c)))
+
+; There are others, but I am not going to prove them now.
+
+; ----------------------------------------------------------------------------
+; Ordered Pairs as Sets
+
+; It is possible to provide ordered pairs as ur-elements. For example
+; we could define (pair x y) to be (list :UR-CONS (cons x y)). But here
+; we develop the classical treatment of ordered pairs.
+
+(defun pair (x y)
+ (brace x (brace x y)))
+
+; Observe that a pair necessarily has cardinality 2. But the larger
+; element need not have cardinality 2. For example, (pair x x) is
+; {x {x}}.
+
+; We must be able to determine whether a set of cardinality 2 is a
+; pair. Call the two elements x and y. Then either (mem x y) or (mem
+; y x). Furthermore, the larger must be of cardinality 2 or less. To
+; code this up, we have to have a way of finding ``the two elements''
+; of a set, a, of cardinality 2, when a is not necessarily in
+; canonical form. E.g., (1 (1 2)) is a pair but so is (1 1 (2 1) (1
+; 2)). At first, I wanted to avoid canonicalizing the set, for
+; efficiency reasons.
+
+; Here was my first attempt to extract ``the other'' element of a
+; set of cardinality 2.
+
+; (defun find-other (e s)
+; ; Find the first element of s that is not e.
+; (cond ((ur-elementp s) nil)
+; ((= e (scar s)) (find-other e (scdr s)))
+; (t (scar s))))
+
+; Unfortunately, this function does not admit = as a congruence in
+; the second argument. For example (find-other 1 '(1 2 3)) and
+; (find-other 1 '(1 3 2)) return different things, even though their
+; arguments are =. (It would admit it if we limited s to sets of
+; cardinality 2, but we can't.)
+
+; So I have decided simply use the classical approach in terms of
+; choose. If the first element of a pair is a number, this is not too
+; expensive.
+
+(defun pairp (a)
+ (if (equal (cardinality a) 2)
+ (let* ((x (choose a))
+ (y (choose (diff a (brace x)))))
+ (or (and (mem x y)
+ (<= (cardinality y) 2))
+ (and (mem y x)
+ (<= (cardinality x) 2))))
+ nil))
+
+(defun hd (a)
+ (cond ((pairp a)
+ (let* ((x (choose a))
+ (y (choose (diff a (brace x)))))
+ (if (mem x y)
+ x
+ y)))
+ (t nil)))
+
+(defun tl (a)
+ (cond ((pairp a)
+ (let* ((x (choose a))
+ (y (choose (diff a (brace x)))))
+ (if (mem x y)
+ (if (equal (cardinality y) 1)
+ x
+ (choose (diff y (brace x))))
+ (if (equal (cardinality x) 1)
+ y
+ (choose (diff x (brace y)))))))
+ (t nil)))
+
+(defthm setp-pair
+ (setp (pair x y)))
+
+(defcong = = (pair a b) 1)
+(defcong = = (pair a b) 2)
+(defcong = equal (pairp a) 1)
+(defcong = = (hd a) 1)
+(defcong = = (tl a) 1)
+
+(in-theory (enable mem-container))
+
+(defthm hd-pair
+ (= (hd (pair x y)) x))
+
+(defthm tl-pair
+ (= (tl (pair x y)) y))
+
+(defthm pairp-pair
+ (pairp (pair x y))
+ :rule-classes (:type-prescription :generalize))
+
+(defthm pairp-implies-setp
+ (implies (pairp x) (setp x)))
+
+(encapsulate
+ nil
+
+; Our goal here is to prove
+
+; (implies (pairp a)
+; (= (pair (hd a) (tl a)) a))
+
+; We have to give the proof pretty explicitly. It exploits the fact
+; that we know how to represent singleton and doubleton sets in terms
+; of choose. Since we have to use these lemmas explicitly, we disable
+; them.
+
+ (local (in-theory (disable elim-choose-doubleton
+ elim-choose-singleton)))
+
+; To make the proof easier to understand, we give names to certain
+; expressions. In the definitions of pair, hd and tl, we use two
+; local variables,
+
+; (let* ((x (choose a))
+; (y (choose (diff a (brace x)))))
+; ...)
+
+; Here we define functions corresponding to their values.
+
+ (local (defun x (a) (choose a)))
+ (local (defun y (a) (choose (diff a (brace (x a))))))
+
+; Given that a is known to be a pairp, there are four cases, depending
+; on which of x and y is an element of the other and whether the
+; cardinality of the bigger is 1 or 2. We will prove the main goal
+; for each of the four cases.
+
+ (local
+ (defthm case-1
+ (implies (and (mem (x a) (y a))
+ (equal (cardinality (y a)) 2)
+ (pairp A))
+ (= (pair (hd A) (tl A)) A))
+ :hints
+ (("Goal"
+ :use
+ (
+
+; Proof of Case 1:
+
+; (i) Represent A as a doubleton in terms of choose.
+
+ (:instance elim-choose-doubleton (x A))
+
+; (ii) Represent y as a doubleton.
+
+ (:instance elim-choose-doubleton (x (y a)))
+
+; (iii) When x is removed from y, the result is a singleton, which can
+; be represented with choose.
+
+ (:instance elim-choose-singleton
+ (x (diff (y a) (scons (x a) nil))))
+
+; (iv) If x is a member of a singleton set, the set is {x}.
+
+ (:instance mem-singleton
+ (e (x a))
+ (x (diff (y a) (scons (x a) nil)))))))))
+
+ (local
+ (defthm case-2
+ (implies (and (mem (x a) (y a))
+ (equal (cardinality (y a)) 1)
+ (pairp A))
+ (= (pair (hd A) (tl A)) A))
+ :hints
+ (("Goal"
+ :use
+ (
+
+; Proof of Case 2:
+
+; (i) Represent A as a doubleton in terms of choose.
+
+ (:instance elim-choose-doubleton (x A))
+
+; (ii) Represent y as a singleton.
+
+ (:instance elim-choose-singleton (x (y a)))
+
+; (iii) If x is a member of singleton set, the set is {x}.
+
+ (:instance mem-singleton
+ (e (x a))
+ (x (y a))))))))
+
+; Cases 3 and 4 are symmetric with Cases 1 and 2, interchanging the
+; roles of x and y.
+
+ (local
+ (defthm case-3
+ (implies (and (mem (y a) (x a))
+ (equal (cardinality (x a)) 2)
+ (pairp A))
+ (= (pair (hd A) (tl A)) A))
+ :hints
+ (("Goal"
+ :use
+ ((:instance elim-choose-doubleton (x A))
+ (:instance elim-choose-doubleton (x (x a)))
+ (:instance elim-choose-singleton
+ (x (diff (x a) (scons (y a) nil))))
+ (:instance mem-singleton
+ (e (y a))
+ (x (diff (x a) (scons (y a) nil)))))))))
+
+ (local
+ (defthm case-4
+ (implies (and (mem (y a) (x a))
+ (equal (cardinality (x a)) 1)
+ (pairp A))
+ (= (pair (hd A) (tl A)) A))
+ :hints
+ (("Goal"
+ :use
+ ((:instance elim-choose-doubleton (x A))
+ (:instance elim-choose-singleton (x (x a)))
+ (:instance mem-singleton
+ (e (y a))
+ (x (x a))))))))
+
+ (defthm pair-hd-tl
+ (implies (pairp A)
+ (= (pair (hd A) (tl A)) A))
+ :hints
+ (("Goal" :in-theory (disable pair hd tl)
+ :cases ((and (mem (x a) (y a)) ;;; Case 1
+ (equal (cardinality (y a)) 2))
+ (and (mem (x a) (y a)) ;;; Case 2
+ (equal (cardinality (y a)) 1))
+ (and (mem (y a) (x a)) ;;; Case 3
+ (equal (cardinality (x a)) 2))
+ (and (mem (y a) (x a)) ;;; Case 4
+ (equal (cardinality (x a)) 1)))))
+ :rule-classes (:rewrite :elim)))
+
+(in-theory (disable mem-container))
+
+(in-theory (disable pairp pair hd tl))
+
+(defthm equal-booleans
+ (implies (and (acl2::booleanp p)
+ (acl2::booleanp q))
+ (equal (equal p q)
+ (iff p q))))
+
+(defthm equal-pair
+ (equal (= (pair x1 y1)
+ (pair x2 y2))
+ (and (= x1 x2)
+ (= y1 y2)))
+ :hints
+ (("Goal" :in-theory (disable hd-pair tl-pair)
+ :use ((:instance hd-pair (x x1) (y y1))
+ (:instance hd-pair (x x2) (y y2))
+ (:instance tl-pair (x x1) (y y1))
+ (:instance tl-pair (x x2) (y y2))))))
+
+(in-theory (disable equal-booleans))
+
+(defthm equal-pair-generalized
+ (equal (= (pair x1 x2) y)
+ (and (pairp y)
+ (= x1 (hd y))
+ (= x2 (tl y)))))
+
+(in-theory (disable equal-pair-generalized))
+
+
+
+; ----------------------------------------------------------------------------
+; Functions as Sets
+
+; The following is an example of set comprehension. In particular, it
+; is
+
+; { x in s | (and (pairp x) (= e (hd x)))}
+
+(defun subset-such-that1 (s e)
+ (cond ((ur-elementp s) nil)
+ ((and (pairp (scar s))
+ (= e (hd (scar s))))
+ (scons (scar s) (subset-such-that1 (scdr s) e)))
+ (t (subset-such-that1 (scdr s) e))))
+
+; When such a function is defined we should immediately prove the
+; obvious three relationships:
+
+(defthm setp-subset-such-that1
+ (setp (subset-such-that1 a e)))
+
+(defthm mem-subset-such-that1
+ (iff (mem pair (subset-such-that1 a x))
+ (and (pairp pair)
+ (mem pair a)
+ (= (hd pair) x)))
+ :hints (("Goal" :do-not '(generalize))))
+
+(defthm subsetp-subset-such-that1
+ (subsetp (subset-such-that1 a x) a))
+
+; The congruence rules are easy.
+
+(defx :strategy :congruence (subset-such-that1 a e) 1 :method :subsetp)
+(defx :strategy :congruence (subset-such-that1 a e) 2)
+
+(defthm mem-subset-such-that1-corrollary
+ (implies (and (subsetp a (subset-such-that1 f x))
+ (mem e a))
+ (and (pairp e)
+ (= (hd e) x))))
+
+; Now we define apply:
+
+(defun apply (s e)
+ (tl (choose (subset-such-that1 s e))))
+
+(defcong = = (apply s e) 1)
+(defcong = = (apply s e) 2)
+
+(defun except (s e v)
+ (scons (pair e v)
+ (diff s (subset-such-that1 s e))))
+
+(defcong = = (except s e v) 1)
+(defcong = = (except s e v) 2)
+(defcong = = (except s e v) 3)
+
+(defthm diff-scons-1
+ (implies (acl2::syntaxp (not (equal b ''nil)))
+ (= (diff a (scons e b))
+ (diff (diff a b) (brace e)))))
+
+(defthm ur-elementp-diff
+ (iff (ur-elementp (diff a b))
+ (subsetp a b)))
+
+(defthm subset-such-that1-diff-subset-such-that-1
+ (= (subset-such-that1 (diff f (subset-such-that1 f x)) y)
+ (if (= x y)
+ nil
+ (subset-such-that1 f y))))
+
+(encapsulate
+ nil
+ (local
+ (defthm lemma2
+ (implies (and (subsetp f (subset-such-that1 g x))
+ (not (= x y)))
+ (= (subset-such-that1 f y)
+ nil))))
+
+ (defthm apply-except
+ (= (apply (except f x v) y)
+ (if (= x y)
+ v
+ (apply f y)))))
+
+(defthm mem-except
+ (equal (mem e (except f x v))
+ (if (pairp e)
+ (if (= (hd e) x)
+ (= (tl e) v)
+ (mem e f))
+ (mem e f))))
+
+(defthm subsetp-except
+ (iff (subsetp (except f x v) g)
+ (and (mem (pair x v) g)
+ (subsetp (diff f (subset-such-that1 f x))
+ g))))
+
+(defthm ur-elementp-except
+ (not (ur-elementp (except f x v))))
+
+(in-theory (disable apply except))
+
+(defmacro func* (&rest args)
+ (cond ((endp args) nil)
+ ((endp (cdr args)) (car args))
+ (t `(except (func* ,@(cdr args))
+ ,(car (car args))
+ ,(cadr (car args))))))
+
+(defmacro func (&rest args)
+ `(func* ,@args nil))
+
+
+; ----------------------------------------------------------------------------
+; Sets of ordered pairs.
+
+; This is really just a simple map over a checking a predicate. I
+; need to automate this sort of thing but I will do it by hand right
+; now.
+
+(defun pairsp (a)
+ (cond ((ur-elementp a) t)
+ (t (and (pairp (scar a))
+ (pairsp (scdr a))))))
+
+(defx :strategy :congruence (pairsp a) 1 :method :canonicalize)
+
+(defthm pairsp-union
+ (equal (pairsp (union a b))
+ (and (pairsp a)
+ (pairsp b))))
+
+(defthm pairsp-diff
+ (implies (pairsp a)
+ (pairsp (diff a b))))
+
+; This one is more useful when dealing with sets created by EXCEPT.
+
+(defthm pairsp-diff-subset-such-that1
+ (equal (pairsp (diff a (subset-such-that1 b x)))
+ (pairsp a)))
+
+(defthm pairsp-scons
+ (equal (pairsp (scons e a))
+ (and (pairp e)
+ (pairsp a))))
+
+(defthm mem-pairsp
+ (implies (and (mem e f)
+ (pairsp f))
+ (pairp e)))
+
+(defthm pairsp-subset-such-that1
+ (implies (pairsp f)
+ (pairsp (subset-such-that1 f x))))
+
+(defthm nil-not-mem-pairsp
+ (implies (pairsp f)
+ (not (mem nil f))))
+
+; ----------------------------------------------------------------------------
+; Recognizing Functions
+
+; The basic idea is to define the predicate that recognizes when a set
+; is both pairsp and has unique hds. We've got the first part. The
+; second part is called functionp1.
+
+; Here is my first functionp1. It does not insure that every element
+; of f is a pair. Thus,
+
+; (functionp1 (brace (pair 1 2)) (brace (pair 1 2) 3)) = t
+
+; Second, it is fragile in the sense that if a is not a subset of f, it
+; fails, e.g.,
+
+; (functionp1 (brace (pair 1 2)) (brace (pair 3 4))) = nil
+
+; This is not a problem at the top level, where a is f. But in stating
+; theorems about functionp1 it would be convenient to allow arbitrary a
+; with sensible results.
+
+; (defun functionp1 (a f)
+; (cond ((ur-elementp a) t)
+; (t (and (pairp (scar a))
+; (equal (cardinality (subset-such-that1 f (hd (scar a)))) 1)
+; (functionp1 (scdr a) f)))))
+
+; So here is my second:
+
+(defun functionp1 (a f)
+ (cond ((ur-elementp a) t)
+ (t (and (<= (cardinality (subset-such-that1 f (hd (scar a)))) 1)
+ (functionp1 (scdr a) f)))))
+
+(defx :strategy :congruence (functionp1 a f) 1 :method :canonicalize)
+(defcong = equal (functionp1 a f) 2)
+
+
+; Is 8 a function? I say no. The reason I say no, is that I want it
+; to be the case that two functions are equal iff apply gives the same
+; answers on both. But if I defined a function as (and (pairsp f)
+; (functionp1 f f)) then 8 is a functionp, because every element of 8
+; is a pair and their hds are unique.
+
+(defun functionp (f)
+ (if (ur-elementp f)
+ (= f nil)
+ (and (pairsp f)
+ (functionp1 f f))))
+
+(defcong = equal (functionp f) 1)
+
+; My next goal is to prove that functionp is preserved by EXCEPT.
+; I need some lemmas about functionp1
+
+(defthm cardinality-subset-such-that1
+ (<= (cardinality (subset-such-that1 f x))
+ (cardinality f))
+ :rule-classes :linear)
+
+(defun simultaneously (a b)
+ (declare (xargs :measure (cardinality a)))
+ (cond ((ur-elementp a) b)
+ (t (simultaneously (diff a (brace (scar a)))
+ (diff b (brace (scar a)))))))
+
+(defthm cardinality-subsetp
+ (implies (subsetp a b)
+ (<= (cardinality a)
+ (cardinality b)))
+ :hints (("Goal" :induct (simultaneously a b)))
+ :rule-classes :linear)
+
+
+
+; The next two theorems are not used until later, but they seem
+; natural to have around.
+
+(defthm functionp1-subsetp-2
+ (implies (and (functionp1 a g)
+ (subsetp f g))
+ (functionp1 a f))
+ :hints
+ (("Subgoal *1/4'"
+ :in-theory (disable cardinality-subsetp)
+ :use (:instance cardinality-subsetp
+ (a (SUBSET-SUCH-THAT1 F (HD (SCAR A))))
+ (b (SUBSET-SUCH-THAT1 G (HD (SCAR A))))))))
+
+(defthm functionp1-diff
+ (implies (functionp1 a f)
+ (functionp1 a (diff f b)))
+ :hints (("Goal" :in-theory (disable subsetp-diff-1)
+ :use (:instance subsetp-diff-1
+ (a f)
+ (b b)))))
+
+; Consider the goal (implies (functionp f) (functionp f')), where f'
+; is (except f x v). Ignoring the pairsp part, this opens into
+
+; (implies (functionp1 f f) (functionp1 f' f'))
+
+; We have to break both duplications. Each requires a lemma. Then
+; we put the two lemmas together to get something like:
+
+; (implies (functionp1 b f) (functionp1 a f'))
+
+; where (subsetp a b).
+
+; Here is one of the two ``breakers.''
+
+(defthm functionp1-subsetp-1
+ (implies (and (subsetp a b)
+ (functionp1 b f))
+ (functionp1 a f))
+ :hints (("Goal" :do-not '(generalize))))
+
+(encapsulate
+ nil
+
+; This is the other ``breaker''. The scons below is f', i.e., the
+; expansion of (except f x v).
+
+ (local
+ (defthm functionp1-except-lemma
+ (implies (functionp1 a f)
+ (functionp1 a (scons (pair x v)
+ (diff f (subset-such-that1 f x)))))))
+
+; Now we put the two breakers together to get the main lemma about
+; functionp1 and except.
+
+ (defthm functionp1-except
+ (implies (and (functionp1 b f)
+ (subsetp a b))
+ (functionp1 a (scons (pair x v)
+ (diff f (subset-such-that1 f x)))))))
+
+(defthm functionp-except
+ (implies (functionp f)
+ (functionp (except f x v)))
+ :hints (("Goal" :in-theory (enable except))))
+
+(defthm functionp-implies-pairsp
+ (implies (functionp f)
+ (pairsp f)))
+
+(in-theory (disable functionp))
+
+;----------------------------------------------------------------------------
+; Domain and Range
+
+(defun domain (f)
+ (cond ((ur-elementp f) nil)
+ (t (scons (hd (scar f))
+ (domain (scdr f))))))
+
+(defun range (f)
+ (cond ((ur-elementp f) nil)
+ (t (scons (tl (scar f)) (range (scdr f))))))
+
+(defthm mem-implies-mem-domain
+ (implies (mem e f)
+ (mem (hd e) (domain f))))
+
+(defthm ur-elementp-domain
+ (equal (ur-elementp (domain f))
+ (ur-elementp f)))
+
+(defx :strategy :congruence (domain f) 1 :method :subsetp)
+
+(defthm mem-implies-mem-range
+ (implies (mem e f)
+ (mem (tl e) (range f))))
+
+(defthm ur-elementp-range
+ (equal (ur-elementp (range f))
+ (ur-elementp f)))
+
+(defx :strategy :congruence (range f) 1 :method :subsetp)
+
+(defthm domain-scons
+ (= (domain (scons e f))
+ (scons (hd e) (domain f))))
+
+(defthm domain-diff-subset-such-that1
+ (implies (pairsp f)
+ (= (domain (diff f (subset-such-that1 f x)))
+ (diff (domain f) (brace x)))))
+
+(defthm domain-except
+ (implies (pairsp f)
+ (= (domain (except f x v))
+ (scons x (domain f))))
+ :hints (("Goal" :in-theory (enable except))))
+
+; The range of (except f x v) is harder to characterize. If f is
+; not a function, then (except f x v) might be. The range of f
+; might include many things that are removed by the except.
+
+(defthm range-scons
+ (= (range (scons e f))
+ (scons (tl e) (range f))))
+
+(defthm subsetp-range-except
+ (subsetp (range (except f x v))
+ (scons v (range f)))
+ :hints (("Goal" :in-theory (enable except))))
+
+; We have these two, even though the union is not necessarily a
+; function.
+
+(defthm domain-union
+ (= (domain (union f g))
+ (union (domain f) (domain g))))
+
+(defthm range-union
+ (= (range (union f g))
+ (union (range f) (range g))))
+
+(defthm cardinality-domain
+ (<= (cardinality (domain f)) (cardinality f))
+ :rule-classes :linear)
+
+(defthm cardinality-range
+ (<= (cardinality (range f)) (cardinality f))
+ :rule-classes :linear)
+
+(defthm ur-element-subset-such-that1
+ (implies (pairsp f)
+ (equal (ur-elementp (subset-such-that1 f x))
+ (not (mem x (domain f))))))
+
+(defthm cardinality-<=-0
+ (equal (< 0 (cardinality a))
+ (not (ur-elementp a))))
+
+(defthm cardinality-domain-functionp
+ (implies (functionp f)
+ (equal (cardinality (domain f))
+ (cardinality f)))
+ :hints (("Goal" :in-theory (enable functionp))))
+
+(defthm subset-such-that1-empty
+ (implies (not (mem e (domain b)))
+ (= (subset-such-that1 b e)
+ nil)))
+
+; Is the (pairsp b) hypothesis below necessary? Yes. Here is a counterexample
+; of the formula without the hypothesis.
+
+#|(let ((b (brace 123))
+ (a (brace (pair nil 33)))
+ (pair (pair nil 2)))
+ (equal (functionp1 a (scons pair b))
+ (if (and (pairp pair)
+ (mem (hd pair) (domain a)))
+ (and (functionp1 a b)
+ (or (mem pair b)
+ (not (mem (hd pair) (domain b)))))
+ (functionp1 a b))))|#
+
+(defthm functionp1-scons
+ (implies (pairsp b)
+ (equal (functionp1 a (scons pair b))
+ (if (and (pairp pair)
+ (mem (hd pair) (domain a)))
+ (and (functionp1 a b)
+ (or (mem pair b)
+ (not (mem (hd pair) (domain b)))))
+ (functionp1 a b)))))
+
+(defthm cardinality-<=-1-cases
+ (iff (< 1 (cardinality x))
+ (not (or (ur-elementp x)
+ (equal (cardinality x) 1)))))
+
+(defthm functionp-scons-lemma
+ (implies (and (functionp1 a b)
+ (subsetp a b)
+ (pairsp b)
+ (mem e a))
+ (equal (cardinality (subset-such-that1 b (hd e)))
+ 1)))
+
+; Note that the following theorem is essentially a recursive
+; alternative definition of functionp.
+
+(defthm functionp-scons
+ (equal (functionp (scons e a))
+ (if (ur-elementp a)
+ (pairp e)
+ (and (functionp a)
+ (pairp e)
+ (or (mem e a)
+ (not (mem (hd e) (domain a)))))))
+ :hints (("Goal" :in-theory (enable functionp))))
+
+(defthm functionp-union
+ (implies (and (functionp a)
+ (functionp b)
+ (not (intersection (domain a) (domain b))))
+ (functionp (union a b))))
+
+(defthm disjoint-domains-implies-disjoint
+ (implies (not (intersection (domain a) (domain b)))
+ (not (intersection a b)))
+ :rule-classes nil)
+
+(defthm cardinality-except
+ (implies (functionp f)
+ (= (cardinality (except f x v))
+ (if (mem x (domain f))
+ (cardinality f)
+ (+ 1 (cardinality f)))))
+ :hints (("Goal"
+ :use ((:instance cardinality-domain-functionp (f (except f x v)))
+ (:instance cardinality-domain-functionp (f f)))
+ :in-theory (disable cardinality-domain-functionp))))
+
+(defthm apply-outside-domain
+ (implies (not (mem e (domain f)))
+ (= (apply f e) nil))
+ :hints (("Goal" :in-theory (enable apply))))
+
+;----------------------------------------------------------------------------
+; Restrictions
+
+; I can think of three slightly different ways to define the restriction
+; of a function f to some domain s.
+
+; (1) Iterate over s and make a function of the defined values. This
+; always produces a function. However, if f is not a function, the
+; function it produces is sort of unpredictable because it uses apply,
+; so the restricted function chooses the largest pairs.
+
+(defun restrict (f s)
+ (cond ((ur-elementp s) nil)
+ ((mem (scar s) (domain f))
+ (except (restrict f (scdr s))
+ (scar s)
+ (apply f (scar s))))
+ (t (restrict f (scdr s)))))
+
+; (2) Iterate over f and make a function of the values of elements of
+; s. This always produces a function. But if f is not a function,
+; the restricted function is unpredictable because it chooses the
+; first pair presented for each domain element. I reject this
+; definition because it does not do the ``normal'' things with a
+; function. The normal things you do with a function are enquire
+; about its domain and apply it. Looking at its internal structure is
+; an invitation to low-level work.
+
+; (defun restrict2 (f s)
+; (cond ((ur-elementp f) nil)
+; ((and (pairp (scar f))
+; (mem (hd (scar f)) s))
+; (except (restrict2 (scdr f) s)
+; (hd (scar f))
+; (tl (scar f))))
+; (t (restrict2 (scdr f) s))))
+
+; (3) Iterate over f and collect everything whose hd is in s. The
+; result may not be a function, but it is if f is. This has the
+; appeal of being really simple, but, again, uses f in an abnormal
+; way.
+
+; (defun restrict3 (f s)
+; (cond ((ur-elementp f) nil)
+; ((mem (hd (scar f)) s)
+; (scons (scar f) (restrict3 (scdr f) s)))
+; (t (restrict3 (scdr f) s))))
+
+(defx :strategy :congruence (restrict f s) 1)
+
+; Next we prove that the second argument of restrict admits = as a
+; congruence relation. For some reason it took me a while to
+; realize that if you are going to prove that something is a
+; subset of (restrict f s) you must be able to answer the question
+; ``when is e a member of (restrict f s)?'' I was seeing this question
+; come up and generalized it to ``when is e a member of a function?''
+; Answering that was harder than answering it for (restrict f s),
+; which is always a function but which is built in a way that makes
+; it easier to answer the question. Here is how you do it.
+
+; The system can prove mem-restrict, below, without further help. It
+; generates three inductively proved subgoals. These are not worth
+; turning into rules because mem-restrict, once proved, is better than
+; each of them.
+
+(defthm mem-restrict
+ (equal (mem e (restrict f s))
+ (and (pairp e)
+ (mem (hd e) (domain f))
+ (= (tl e) (apply f (hd e)))
+ (mem (hd e) s)))
+ :hints (("Goal" :do-not '(generalize))))
+
+; At first I wrote (= (restrict f s) nil) instead of the inner equal.
+; But I really need the stronger equal because in the defcong= proof
+; below the question of whether (restrict f s) is a set comes up. To
+; be a set it must be either not an ur-element or nil. This means
+; that we end up testing (restrict f s) against nil in a propositional
+; setting, not a set theory setting. Since = does not refine iff
+; (because '(:UR-CONS NIL) is canonicalized to NIL), knowing that
+; (restrict f s) is not = nil does not help us.
+
+(defthm ur-elementp-restrict
+ (equal (ur-elementp (restrict f s))
+ (equal (restrict f s) nil)))
+
+(defx :strategy :congruence (restrict f s) 2 :method :subsetp)
+
+(defthm functionp-restrict
+ (functionp (restrict f s)))
+
+; My next main goal is the fundamental fact characterizing the elements
+; of a function.
+
+; Perhaps disable this when we're done?
+
+
+(defthm pigeon-hole-1
+ (implies (and (mem e a)
+ (mem d a)
+ (equal (cardinality a) 1))
+ (= e d))
+ :rule-classes nil)
+
+; The next three theorems are trivial consequences of other lemmas
+; given the fact that (choose a) is an element of a. I really ought
+; to provide macros that capture these kind of theorems. The idea in
+; all of them is that if every element of a has some property then
+; (choose a) has that property if a is non-empty.
+
+(defthm hd-choose-subset-such-that1
+ (= (hd (choose (subset-such-that1 f x)))
+ (if (ur-elementp (subset-such-that1 f x))
+ nil
+ x))
+ :hints (("Goal"
+ :in-theory (disable mem-choose)
+ :use ((:instance mem-choose
+ (a (subset-such-that1 f x)))))))
+
+(defthm pairp-choose-subset-such-that1
+ (implies (pairsp f)
+ (equal (pairp (choose (subset-such-that1 f x)))
+ (and (not (ur-elementp f))
+ (mem x (domain f)))))
+ :hints (("Goal"
+ :in-theory (cons 'equal-booleans
+ (disable mem-choose))
+ :use ((:instance mem-choose
+ (a (subset-such-that1 f x)))))))
+
+(defthm mem-choose-subset-such-that1
+ (implies (pairsp f)
+ (equal (mem (choose (subset-such-that1 f x)) f)
+ (and (not (ur-elementp f))
+ (mem x (domain f)))))
+ :hints (("Goal"
+ :in-theory (cons 'equal-booleans
+ (disable mem-choose))
+ :use ((:instance mem-choose
+ (a (subset-such-that1 f x)))))))
+
+; This is a pretty obscure fact, I think. If x is a pair in f and
+; there is only one pair in f with its hd, then choose chooses x.
+
+(defthm mem-x-implies-not-ur-elementp-subset-such-that1
+ (implies (and (mem x f)
+ (pairp x))
+ (not (ur-elementp (subset-such-that1 f (hd x))))))
+
+(defthm choose-subset-such-that1
+ (implies (and (<= (cardinality (subset-such-that1 f (hd x))) 1)
+ (mem x f)
+ (pairp x)
+ (pairsp f))
+ (= (choose (subset-such-that1 f (hd x)))
+ x))
+ :hints (("Goal"
+ :use (:instance pigeon-hole-1
+ (e x)
+ (d (choose (subset-such-that1 f (hd x))))
+ (a (subset-such-that1 f (hd x)))))))
+
+(defthm functionp-implies-mem-1
+ (implies (and (functionp1 a f)
+ (pairsp f)
+ (subsetp a f)
+ (mem hd (domain a)))
+ (mem (pair hd (tl (choose (subset-such-that1 f hd))))
+ f)))
+
+(defthm functionp-implies-mem-2
+ (implies (and (functionp1 a f)
+ (pairsp f)
+ (subsetp a f)
+ (mem (hd x) (domain a))
+ (pairp x)
+ (mem x f))
+ (= (choose (subset-such-that1 f (hd x)))
+ x)))
+
+; This is the fundamental fact about membership in a function. It
+; loops if made into a rewrite rule.
+
+(defthm mem-functionp
+ (implies (functionp f)
+ (equal (mem e f)
+ (and (pairp e)
+ (mem (hd e) (domain f))
+ (= (tl e) (apply f (hd e))))))
+ :rule-classes nil
+ :hints (("Goal"
+ :in-theory (enable functionp apply equal-booleans))))
+
+(defthm domain-restrict
+ (= (domain (restrict f s))
+ (intersection s (domain f))))
+
+(defthm apply-restrict
+ (implies (and (mem x (domain f))
+ (mem x s))
+ (= (apply (restrict f s) x)
+ (apply f x))))
+
+(defthm except-scdr-scar-elim
+ (implies (and (functionp f)
+ (not (ur-elementp f)))
+ (= (except (scdr f) (hd (scar f)) (tl (scar f)))
+ f))
+ :otf-flg t
+ :hints
+ (("Goal"
+ :in-theory (enable except functionp equal-pair-generalized)
+ :use ((:instance mem-functionp
+ (e (pair (hd (scar f)) (tl (scar f))))
+ (f f))
+ (:instance mem-singleton
+ (e (pair (hd (scar f)) (tl (scar f))))
+ (x (subset-such-that1 (scdr f) (hd (scar f)))))))))
+
+(defthm functionp-nil
+ (implies (ur-elementp f)
+ (equal (functionp f) (= f nil)))
+ :hints (("Goal" :in-theory (enable functionp))))
+
+(defthm functionp-pairp
+ (implies (not (pairp x))
+ (not (functionp (scons x y))))
+ :hints (("Goal" :in-theory (enable functionp))))
+
+(defthm except-scdr-scar-elim-special-case
+ (implies (and (functionp f)
+ (not (ur-elementp f))
+ (ur-elementp (scdr f)))
+ (= (except nil (hd (scar f)) (tl (scar f)))
+ f))
+ :hints (("Goal" :in-theory (enable except))))
+
+(defthm functionp-scdr
+ (implies (functionp f)
+ (functionp (scdr f)))
+ :hints (("Goal" :in-theory (enable functionp))))
+
+(defthm restrict-domain
+ (implies (and (functionp f)
+ (functionp g)
+ (subsetp f g))
+ (= (restrict g (domain f)) f))
+ :hints
+ (("Subgoal *1/4"
+ :use ((:instance mem-functionp (e (scar f)) (f g))))))
+
+; The lemma above will rewrite (restrict a (domain a)) to a, provided
+; (functionp a). But it is often the case that the domain expression
+; will be rewritten to something else, e.g., an intersection. So
+; we provide a bridge.
+
+(defthm restrict-domain-special-case
+ (implies (and (functionp f)
+ (= a (domain f)))
+ (= (restrict f a) f)))
+
+(defthm restrict-scons
+ (= (restrict f (scons e s))
+ (if (mem e (domain f))
+ (except (restrict f s)
+ e
+ (apply f e))
+ (restrict f s))))
+
+; ----------------------------------------------------------------------------
+; Strategies for Proving Functions and Sets Equivalent
+
+(encapsulate ((functional-equiv-fn1 () t)
+ (functional-equiv-fn2 () t))
+ (local (defun functional-equiv-fn1 nil nil))
+ (local (defun functional-equiv-fn2 nil nil))
+ (defthm functional-equivalence-constraint-1
+ (functionp (functional-equiv-fn1)))
+ (defthm functional-equivalence-constraint-2
+ (functionp (functional-equiv-fn2)))
+ (defthm functional-equivalence-constraint-3
+ (= (domain (functional-equiv-fn2))
+ (domain (functional-equiv-fn1))))
+
+; We use the unusual variable name fex (``functional equivalence x'') because
+; any variable appearing in a constraint is prohibited from occurring in
+; any theorem proved with functional-instantiation from this constraint.
+
+ (defthm functional-equivalence-constraint-4
+ (implies (mem fex (domain (functional-equiv-fn1)))
+ (= (apply (functional-equiv-fn1) fex)
+ (apply (functional-equiv-fn2) fex)))))
+
+(defun every-where-= (s f g)
+ (cond ((ur-elementp s) t)
+ (t (and (= (apply f (scar s))
+ (apply g (scar s)))
+ (every-where-= (scdr s) f g)))))
+
+(defthm every-where-=-implies-=-restrict
+ (implies (and (functionp f)
+ (functionp g)
+ (subsetp s (domain f))
+ (subsetp s (domain g))
+ (every-where-= s f g))
+ (= (restrict f s)
+ (restrict g s)))
+ :rule-classes nil)
+
+(encapsulate
+ nil
+ (local
+ (defthm every-where-=-functional-equiv-fn1-functional-equiv-fn2
+ (implies (subsetp s (domain (functional-equiv-fn1)))
+ (every-where-= s (functional-equiv-fn1) (functional-equiv-fn2)))))
+
+ (defthm functional-equivalence-theorem
+ (= (functional-equiv-fn1) (functional-equiv-fn2))
+ :rule-classes nil
+ :hints (("Goal"
+ :use (:instance every-where-=-implies-=-restrict
+ (f (functional-equiv-fn1))
+ (g (functional-equiv-fn2))
+ (s (domain (functional-equiv-fn1))))))))
+
+; The above encapsulation provides a nice way to prove two functions
+; are equal. You can just instantiate the lemma above with any two
+; functions that are known to have the same domain and that are
+; apply-equal everywhere.
+
+(defmacro functional-equivalence (name term
+ &key
+ hints
+ (rule-classes 'nil rule-classesp)
+ (otf-flg 'nil otf-flgp))
+ (let* ((xterm
+ (acl2::case-match
+ term
+ (('implies acl2::& ('= acl2::& acl2::&))
+ term)
+ (('= acl2::& acl2::&)
+ `(implies t ,term))
+ (t nil))))
+ (cond
+ ((null xterm)
+ `(acl2::er acl2::soft 'functional-equivalence
+ "The functional-equivalence strategy requires a term of ~
+ the form (= f g) or (implies h (= f g)). Your term, ~x0, ~
+ is not of this form."
+ ',term))
+ ((acl2::assoc-equal "Goal" hints)
+ `(acl2::er acl2::soft 'functional-equivalence
+ "The functional-equivalence strategy provides hints for ~
+ \"Goal\". Your hints should be provided for some Subgoal."))
+ (t
+ (let ((hyps (cadr xterm))
+ (lhs (cadr (caddr xterm)))
+ (rhs (caddr (caddr xterm))))
+ `(defthm ,name ,term
+ :hints
+ (("Goal"
+ :use ((:functional-instance
+ functional-equivalence-theorem
+ (functional-equiv-fn1
+ (lambda ()
+ ,(if (eq hyps t)
+ lhs
+ `(if ,hyps ,lhs nil))))
+ (functional-equiv-fn2
+ (lambda ()
+ ,(if (eq hyps t)
+ rhs
+ `(if ,hyps ,rhs nil)))))))
+ ,@hints)
+ ,@(if rule-classesp
+ `(:rule-classes ,rule-classes)
+ nil)
+ ,@(if otf-flgp
+ `(:otf-flg ,otf-flg)
+ nil)))))))
+
+; While I'm at it, I'll provide a way to prove that two sets are equal.
+
+; Suppose you have two arbitrary sets with the property that if x is a
+; member of one, then x is a member of the other.
+
+(encapsulate ((subsetp-strategy-set1 () t)
+ (subsetp-strategy-set2 () t))
+ (local (defun subsetp-strategy-set1 () nil))
+ (local (defun subsetp-strategy-set2 () nil))
+
+; We use the unusual variable name ssx (``subsetp strategy x'') because whatever
+; var we use in a constraint is off-limits to the user in any theorem proved
+; via functional instantiation based on these constraints.
+
+ (defthm subsetp-strategy-constraint
+ (implies (mem ssx (subsetp-strategy-set1))
+ (mem ssx (subsetp-strategy-set2)))))
+
+; Then the first set is a subset of the second.
+
+(encapsulate
+ nil
+ (local
+ (defthm subsetp-strategy-lemma
+ (implies (subsetp a (subsetp-strategy-set1))
+ (subsetp a (subsetp-strategy-set2)))))
+
+ (defthm subsetp-strategy
+ (subsetp (subsetp-strategy-set1)
+ (subsetp-strategy-set2))
+ :rule-classes nil))
+
+; And here is a handy macro to use this strategy to prove the subsetp
+; relation between two expressions under a hypothesis.
+
+; This macro allows us to write:
+; (defx foo (subsetp ... ...)
+; :strategy subset-relation
+; :rule-classes ...)
+
+(defmacro subset-relation (name term
+ &key
+ hints
+ (rule-classes 'nil rule-classesp)
+ (otf-flg 'nil otf-flgp))
+ (let* ((xterm
+ (acl2::case-match
+ term
+ (('implies acl2::& ('subsetp acl2::& acl2::&))
+ term)
+ (('subsetp acl2::& acl2::&)
+ `(implies t ,term))
+ (t nil))))
+ (cond
+ ((null xterm)
+ `(acl2::er acl2::soft 'subset-relation
+ "The subset-relation strategy requires a term of ~
+ the form (subsetp a b) or (implies h (subsetp a b)). Your term, ~x0, ~
+ is not of this form."
+ ',term))
+ ((acl2::assoc-equal "Goal" hints)
+ `(acl2::er acl2::soft 'subset-relation
+ "The subset-relation strategy provides hints for ~
+ \"Goal\". Your hints should be provided for some Subgoal."))
+ (t
+ (let ((hyps (cadr xterm))
+ (lhs (cadr (caddr xterm)))
+ (rhs (caddr (caddr xterm))))
+ `(defthm ,name ,term
+ :hints
+ (("Goal"
+ :use ((:functional-instance
+ subsetp-strategy
+ (subsetp-strategy-set1
+ (lambda ()
+ ,(if (eq hyps t)
+ lhs
+ `(if ,hyps ,lhs nil))))
+ (subsetp-strategy-set2
+ (lambda ()
+ ,(if (eq hyps t)
+ rhs
+ `(if ,hyps ,rhs nil)))))))
+ ,@hints)
+ ,@(if rule-classesp
+ `(:rule-classes ,rule-classes)
+ nil)
+ ,@(if otf-flgp
+ `(:otf-flg ,otf-flg)
+ nil)))))))
+
+; Here is a way to set equality using two subsets. It requires
+; proving (mem x a) <-> (mem x b).
+
+; We can thus write
+; (defx foo (implies ... (= ... ...))
+; :strategy equivalence-relation
+; :rule-classes ...)
+
+; Two proof obligations are generated, each a mem implying a mem. You
+; can provide hints for them with :hints-1 and :hints-2.
+
+(defmacro set-equivalence (name term
+ &key hints
+ (rule-classes 'nil rule-classesp)
+ (otf-flg 'nil otf-flgp)
+ (hints-1 'nil hints-1p)
+ (otf-flg-1 'nil otf-flg-1p)
+ (hints-2 'nil hints-2p)
+ (otf-flg-2 'nil otf-flg-2p))
+ (let* ((xterm
+ (acl2::case-match term
+ (('implies acl2::& ('= acl2::& acl2::&))
+ term)
+ (('= acl2::& acl2::&)
+ `(implies t ,term))
+ (t nil))))
+ (cond
+ ((null xterm)
+ `(acl2::er acl2::soft 'set-equivalence
+ "~x0 is not of the form (= x y) or of the form ~
+ (implies hyps (= x y))."
+ ',term))
+ ((or (acl2::assoc-equal "Goal" hints)
+ (acl2::assoc-equal "Goal" hints-1)
+ (acl2::assoc-equal "Goal" hints-2))
+ `(acl2::er acl2::soft 'set-equivalence
+ "The set-equivalence strategy provides hints for ~
+ \"Goal\". Your hints should be provided for some Subgoal."))
+ (t
+ (let ((hyps (cadr xterm))
+ (lhs (cadr (caddr xterm)))
+ (rhs (caddr (caddr xterm)))
+ (name-1 (packn-in-pkg (list name "-1") name))
+ (name-2 (packn-in-pkg (list name "-2") name)))
+ `(encapsulate
+ nil
+ (local
+ (defx ,name-1
+ ,(if (eq hyps t)
+ `(subsetp ,lhs ,rhs)
+ `(implies ,hyps (subsetp ,lhs ,rhs)))
+ :strategy subset-relation
+ ,@(if hints-1p `(:hints ,hints-1) nil)
+ ,@(if otf-flg-1p `(:otf-flg ,otf-flg-1) nil)
+ :rule-classes nil))
+ (local
+ (defx ,name-2
+ ,(if (eq hyps t)
+ `(subsetp ,rhs ,lhs)
+ `(implies ,hyps (subsetp ,rhs ,lhs)))
+ :strategy subset-relation
+ ,@(if hints-2p `(:hints ,hints-2) nil)
+ ,@(if otf-flg-2p `(:otf-flg ,otf-flg-2) nil)
+ :rule-classes nil))
+ (defthm ,name ,term
+ :hints
+ (("Goal"
+ :use ((:instance =-iff-subsetps
+ (a ,(if (eq hyps t)
+ lhs
+ `(if ,hyps ,lhs nil)))
+ (b ,(if (eq hyps t)
+ rhs
+ `(if ,hyps ,rhs nil))))
+ (:instance ,name-1)
+ (:instance ,name-2))
+ ,@hints))
+ ,@(if rule-classesp
+ `(:rule-classes ,rule-classes)
+ nil)
+ ,@(if otf-flgp
+ `(:otf-flg ,otf-flg)
+ nil))))))))
+
+; ----------------------------------------------------------------------------
+; An Example
+
+(defx union-diff-diff
+ (implies (and (subsetp a b)
+ (subsetp b c))
+ (= (union (diff b a)
+ (diff c b))
+ (diff c a)))
+ :strategy :set-equivalence)
+
+;----------------------------------------------------------------------------
+; Sequences
+
+; A sequence is a function whose domain is an initial subset of the
+; natural numbers.
+
+(defun nats (n)
+ (if (zp n)
+ '(0)
+ (scons n (nats (- n 1)))))
+
+(defthm ur-elementp-nats
+ (not (ur-elementp (nats n))))
+
+(defcong = = (nats n) 1
+ :hints (("Goal" :in-theory (enable zp))))
+
+(defthm mem-nats
+ (equal (mem e (nats n))
+ (and (integerp e)
+ (<= 0 e)
+ (<= e (nfix n))))
+ :hints (("Goal" :in-theory (enable =))))
+
+(defun sequencep (s)
+ (and (functionp s)
+ (= (domain s)
+ (diff (nats (cardinality s)) '(0)))))
+
+(defthm functionp-sequencep
+ (implies (sequencep s)
+ (functionp s)))
+
+(defthm domain-sequencep
+ (implies (sequencep s)
+ (= (domain s)
+ (diff (nats (cardinality s)) '(0)))))
+
+(in-theory (disable sequencep))
+
+(defun shift (i j f delta)
+ (declare (xargs :measure (nfix (- (+ 1 (acl2::ifix j)) (acl2::ifix i)))))
+ (cond ((and (integerp i)
+ (integerp j)
+ (<= i j))
+ (except (shift (+ 1 i) j f delta)
+ (+ i delta)
+ (apply f i)))
+ (t nil)))
+
+(defcong = = (shift i j f delta) 1)
+(defcong = = (shift i j f delta) 2)
+(defcong = = (shift i j f delta) 3)
+(defcong = = (shift i j f delta) 4)
+
+(defthm functionp-shift
+ (functionp (shift i j f delta)))
+
+; If f is a sequence, its domain is [1...n]. So (shift i j f delta)
+; takes [i...j] to [i+delta ... j+delta]. This is
+
+(defthm mem-domain-shift
+ (implies (integerp delta)
+ (= (mem x (domain (shift i j f delta)))
+ (and (integerp i)
+ (integerp j)
+ (<= i j)
+ (integerp x)
+ (<= (+ i delta) x)
+ (<= x (+ j delta))))))
+
+; We can express the domain of a shift of a sequence as a set of nats.
+
+(defx domain-shift
+ (implies (and (sequencep s)
+ (integerp delta)
+ (<= 0 delta))
+ (= (domain (shift 1 (cardinality s) s delta))
+ (diff (nats (+ delta (cardinality s)))
+ (nats delta))))
+ :strategy :set-equivalence)
+
+(defun concat (r s)
+ (union r (shift 1 (cardinality s) s (cardinality r))))
+
+(defcong = = (concat r s) 1)
+(defcong = = (concat r s) 2)
+
+(defthm functionp-concat
+ (implies (and (sequencep r)
+ (sequencep s))
+ (functionp (concat r s))))
+
+(defthm subsetp-nats-0
+ (subsetp '(0) (nats i)))
+
+(defthm =-0
+ (equal (= i 0)
+ (equal i 0))
+ :hints (("Goal" :in-theory (enable =))))
+
+(defthm subsetp-nats-nats
+ (equal (subsetp (nats i) (nats j))
+ (<= (nfix i) (nfix j))))
+
+(defthm domain-concat
+ (implies (and (sequencep r)
+ (sequencep s))
+ (= (domain (concat r s))
+ (diff (nats (+ (cardinality r) (cardinality s)))
+ '(0)))))
+
+; I need the (integerp delta) hypothesis because cardinality raises
+; the question of membership in the shifted domain and
+; mem-domain-shift has an integerp hyp.
+
+(defthm cardinality-shift
+ (implies (integerp delta)
+ (= (cardinality (shift i j f delta))
+ (if (and (integerp i)
+ (integerp j)
+ (<= i j))
+ (+ 1 (- j i))
+ 0))))
+
+(defthm cardinality-concat
+ (implies (and (sequencep r)
+ (sequencep s))
+ (= (cardinality (concat r s))
+ (+ (cardinality r) (cardinality s))))
+ :hints (("Goal"
+ :use (:instance disjoint-domains-implies-disjoint
+ (a r)
+ (b (shift 1 (cardinality s) s (cardinality r)))))))
+
+(defthm sequencep-concat
+ (implies (and (sequencep r)
+ (sequencep s))
+ (sequencep (concat r s)))
+ :hints (("Goal"
+ :in-theory
+ (set-difference-theories (enable sequencep)
+ '(concat)))))
+
+; Here is a recursive alternative definition of apply.
+
+(defthm apply-scons
+ (implies (functionp (scons pair f))
+ (= (apply (scons pair f) x)
+ (if (= (hd pair) x)
+ (tl pair)
+ (apply f x))))
+ :hints (("Goal" :in-theory (enable apply))
+ ("Subgoal 2.1'"
+ :in-theory (set-difference-theories (enable functionp)
+ '(functionp-scons-lemma))
+
+ :use ((:instance functionp-scons-lemma
+ (a f)
+ (b f)
+ (e (pair hd tl)))
+ (:instance mem-singleton
+ (x (subset-such-that1 f hd))
+ (e (pair hd tl)))))))
+
+(defthm apply-disjoint-union
+ (implies (and (functionp a)
+ (functionp b)
+ (not (intersection (domain a) (domain b))))
+ (= (apply (union a b) x)
+ (if (mem x (domain a))
+ (apply a x)
+ (apply b x)))))
+
+; Suppose you have a function, f, (not necessarily a sequence) and you
+; form another function, f', by shifting [i...j] of f up by delta.
+; What is (apply f' x)? The domain of f' is [i+delta ... j+delta].
+; If x is in that domain, then (apply f' x) is (apply f (- x delta)).
+
+; To prove this we need the important fact:
+
+(defthm apply-shift
+ (= (apply (shift i j f delta) x)
+ (if (mem x (domain (shift i j f delta)))
+ (apply f (- x delta))
+ nil)))
+
+(defthm apply-concat
+ (implies (and (sequencep r)
+ (sequencep s))
+ (= (apply (concat r s) i)
+ (cond ((and (integerp i)
+ (< 0 i))
+ (if (<= i (cardinality r))
+ (apply r i)
+ (apply s (- i (cardinality r)))))
+ (t nil))))
+ :hints (("Subgoal 11"
+ :in-theory (disable apply-outside-domain)
+ :use
+ ((:instance apply-outside-domain
+ (e (- i (cardinality r)))
+ (f s))))))
+
+(in-theory (disable concat))
+
+(defx associativity-of-concat
+ (implies (and (sequencep a)
+ (sequencep b)
+ (sequencep c))
+ (= (concat (concat a b) c)
+ (concat a (concat b c))))
+ :strategy :functional-equivalence)
+
+; Now I will define seq-hd and seq-tl to let me do recursion down
+; sequences.
+
+(defun seq-hd (s) (apply s 1))
+
+(defcong = = (seq-hd s) 1)
+
+(defun seq-tl (s)
+ (restrict (shift 1 (cardinality s) s -1)
+ (diff (nats (- (cardinality s) 1))
+ (brace 0))))
+
+(defcong = = (seq-tl s) 1)
+
+(defthm functionp-seq-tl
+ (functionp (seq-tl s)))
+
+(defthm cardinality-restrict
+ (= (cardinality (restrict f s))
+ (cardinality (intersection (domain f) s))))
+
+
+
+(defx domain-shift-generalized
+ (implies (and (integerp i)
+ (integerp j)
+ (<= i j)
+ (integerp delta)
+ (<= 0 (+ i delta)))
+ (= (domain (shift i j s delta))
+ (if (= (+ delta i) 0)
+ (nats (+ delta j))
+ (diff (nats (+ delta j))
+ (nats (+ delta i -1))))))
+ :strategy :set-equivalence)
+
+(defthm cardinality-positive
+ (implies (not (ur-elementp s))
+ (< 0 (cardinality s)))
+ :rule-classes :linear)
+
+(defthm intersection-x-x
+ (= (intersection x x) (sfix x)))
+
+(defthm cardinality-diff-nats-0
+ (implies (and (integerp i)
+ (<= 0 i))
+ (= (cardinality (diff (nats i) '(0)))
+ i)))
+
+(defthm cardinality-seq-tl
+ (implies (not (ur-elementp s))
+ (= (cardinality (seq-tl s))
+ (- (cardinality s) 1))))
+
+(defthm sequencep-seq-tl
+ (implies (not (ur-elementp s))
+ (sequencep (seq-tl s)))
+ :hints (("Goal" :in-theory (enable sequencep))))
+
+(defthm seq-tl-recursion
+ (implies (not (ur-elementp s))
+ (< (cardinality (seq-tl s))
+ (cardinality s)))
+ :rule-classes (:built-in-clause :linear))
+
+(in-theory (disable seq-hd seq-tl))
+
+; Next, I define defmap. Thus,
+
+; (defmap subset (a s b) :for x :in s :such-that (bd a x b))
+; and
+; (defmap image (a s b) :for x :in s :map (bd a x b))
+
+; will define subset and image recursively so that they return the
+; sets described below
+
+; (subset a s b) = {x in s | (bd a x b)}
+; and
+; (image a s b) = {(bd a x b) | x in s}
+
+; In addition, I get a few useful theorems about these functions, including
+; that = is a congruence for every argument.
+
+; It must be the case that congruence rules are already in place for
+; (bd a x b).
+
+(defun defmap-congruences (vars call sloc i)
+ (cond
+ ((endp vars) nil)
+ (t (cons (if (equal sloc i)
+ `(defx :strategy :congruence ,call ,i :method :subsetp)
+ `(defx :strategy :congruence ,call ,i))
+ (defmap-congruences (cdr vars) call sloc (+ 1 i))))))
+
+(defmacro defmap (name vars
+ &key
+ (for 'nil forp)
+ (in 'nil inp)
+ (such-that 'nil such-thatp)
+ (map 'nil mapp))
+
+; (defmap foo (s ...) :for x :in s :such-that px)
+; or
+; (defmap foo (s ...) :for x :in s :map px)
+
+ (cond
+ ((not (and (symbolp name)
+ (acl2::symbol-listp vars)
+ forp
+ (symbolp for)
+ (not (acl2::member-equal for vars))
+ inp
+ (symbolp in)
+ (acl2::member-equal in vars)
+ (or (and such-thatp (not mapp))
+ (and (not such-thatp) mapp))))
+ `(acl2::er acl2::soft 'defmap
+ "The proper form of a defmap command is~%~
+ (defmap name vars :for x :in v :such-that body)~%~
+ or~%~
+ (defmap name vars :for x :in v :map body),~%~
+ where name is a new function name, vars is a list of ~
+ variables, x is a variable not in vars, ~
+ v is a variable in vars, and body is a term."))
+ (such-thatp
+ (let* ((x for)
+ (s in)
+ (sloc (- (length vars) (length (member s vars))))
+ (body such-that)
+ (s1 (genname1 s 1 (cons x vars)))
+ (call `(,name ,@vars))
+ (rcall `(,name ,@(put-nth `(scdr ,s) sloc vars))))
+ `(encapsulate
+ nil
+ (defun ,name (,@vars)
+ (if (ur-elementp ,s)
+ nil
+ (let ((,x (scar ,s)))
+ (if ,body
+ (scons (scar ,s) ,rcall)
+ ,rcall))))
+
+ (defthm ,(packn-in-pkg (list "SETP-" name) 'defmap)
+ (setp ,call))
+
+ (defthm ,(packn-in-pkg (list "UR-ELEMENTP-" name) 'defmap)
+ (equal (ur-elementp ,call)
+ (equal ,call nil)))
+
+ (defthm ,(packn-in-pkg (list "MEM-" name) 'defmap)
+ (equal (mem ,x ,call)
+ (and ,body ; we write it this way in case body
+ (mem ,x ,s))) ; is not Boolean!
+ :otf-flg t)
+
+ (defthm ,(packn-in-pkg (list "SUBSETP-" name) 'defmap)
+ (subsetp ,call ,s))
+
+ ,@(defmap-congruences vars call (+ sloc 1) 1)
+
+ (defthm ,(packn-in-pkg (list "MEM-" name "-CORROLLARY") 'defmap)
+ (implies (and (subsetp ,s1 ,call)
+ (mem ,x ,s1))
+ ,body))
+
+ (defthm ,(packn-in-pkg (list "CARDINALITY-" name) 'defmap)
+ (<= (cardinality ,call)
+ (cardinality ,s))
+ :rule-classes :linear)
+
+ (defthm ,(packn-in-pkg (list "UNION-" name) 'defmap)
+ (= (,name ,@(put-nth `(union ,s1 ,s) sloc vars))
+ (union (,name ,@(put-nth s1 sloc vars))
+ ,call)))
+
+ (defthm ,(packn-in-pkg (list "INTERSECTION-" name) 'defmap)
+ (= (,name ,@(put-nth `(intersection ,s1 ,s) sloc vars))
+ (intersection (,name ,@(put-nth s1 sloc vars))
+ ,call)))
+
+ )))
+ (t ;;; :map
+
+ (let* ((x for)
+ (s in)
+ (sloc (- (length vars) (length (member s vars))))
+ (body map)
+ (fx (genname1 x 1 (cons x vars)))
+ (s1 (genname1 s 1 (cons fx (cons x vars))))
+ (call `(,name ,@vars))
+ (rcall `(,name ,@(put-nth `(scdr ,s) sloc vars))))
+ `(encapsulate
+ nil
+ (defun ,name (,@vars)
+ (if (ur-elementp ,s)
+ nil
+ (let ((,x (scar ,s)))
+ (scons ,body ,rcall))))
+
+ (defthm ,(packn-in-pkg (list "SETP-" name) 'defmap)
+ (setp ,call))
+
+ (defthm ,(packn-in-pkg (list "UR-ELEMENTP-" name) 'defmap)
+ (equal (ur-elementp ,call)
+ (ur-elementp ,s)))
+
+ (defthm ,(packn-in-pkg (list "WEAK-MEM-" name) 'defmap)
+ (implies (and (mem ,x ,s)
+ (= ,fx ,body))
+ (mem ,fx ,call)))
+
+
+ (defthm ,(packn-in-pkg (list "SUBSETP-" name) 'defmap)
+ (implies (subsetp ,s1 ,s)
+ (subsetp (,name ,@(put-nth s1 sloc vars))
+ ,call)))
+
+ ,@(defmap-congruences vars call (+ sloc 1) 1)
+
+ (defthm ,(packn-in-pkg (list "CARDINALITY-" name) 'defmap)
+ (<= (cardinality ,call)
+ (cardinality ,s))
+ :rule-classes :linear)
+
+ (defthm ,(packn-in-pkg (list "UNION-" name) 'defmap)
+ (= (,name ,@(put-nth `(union ,s1 ,s) sloc vars))
+ (union (,name ,@(put-nth s1 sloc vars))
+ ,call)))
+
+; Once I thought that
+; (image (intersection s1 s)) = (intersection (image s1) (image s))
+; But this is wrong. Consider
+; s1 = {(0 . 1) (0 . 2)}
+; s = {(1 . 1) (1 . 2)}
+; let (body e) = (cdr e) (or (tl e) if the elements are pairps)
+; Then the lhs is nil because the two sets are disjoint, but the
+; rhs is {1 2}.
+
+ (defthm ,(packn-in-pkg (list "INTERSECTION-" name) 'defmap)
+ (subsetp (,name ,@(put-nth `(intersection ,s1 ,s) sloc vars))
+ (intersection (,name ,@(put-nth s1 sloc vars))
+ ,call)))
+
+ )))))
+
+#|
+; Here are examples of both styles of defmap:
+
+(defstub bd (a x b) t)
+(acl2::skip-proofs
+ (progn (defcong = = (bd a x b) 1)
+ (defcong = = (bd a x b) 2)
+ (defcong = = (bd a x b) 3)))
+
+(defmap subset (a s b) :for x :in s :such-that (bd a x b))
+(defmap image (a s b) :for x :in s :map (bd a x b))
+
+|#
+
diff --git a/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/total-ordering-original.lisp b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/total-ordering-original.lisp
new file mode 100644
index 0000000..de78bee
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/total-ordering-original.lisp
@@ -0,0 +1,267 @@
+; Finite Set Theory for ACL2
+; Copyright (C) 2000 University of Texas at Austin
+
+; This program is free software; you can redistribute it and/or modify it under
+; the terms of Version 2 of the GNU General Public License as published by the
+; Free Software Foundation.
+
+; 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 License
+; along with this program; if not, write to the Free Software
+; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
+
+; Written by: J Strother Moore
+; email: Moore@cs.utexas.edu
+; Department of Computer Science
+; University of Texas at Austin
+; Austin, TX 78701 U.S.A.
+
+; The original kernel of this book was created with support from
+; Compaq Systems Research Center, Palo Alto, CA.
+
+(in-package "ACL2")
+
+; We define a total ordering on ordinary ACL2 objects composed of
+; numbers, characters, strings, symbols, and conses of these things.
+
+; We export
+; (ordinaryp x) the notion of "ordinary objects"
+; (<< x y) disabled the total ordering on such objects
+
+; <<-irreflexivity the four obvious theorems about
+; <<-trichotomy disabled total orders
+; <<-mutual-exclusion disabled
+; <<-transitivity disabled
+
+; We provide ``fast'' versions of the slow rules, named
+
+; fast-<<-trichotomy enabled
+; fast-<<-mutual-exclusion enabled
+; fast-<<-transitivity enabled
+
+; We also provide two theory macros for fiddling with the status of
+; these rules.
+
+; Options:
+; :in-theory (fast-<<-rules) ; the default setting above
+; :in-theory (fast-<<-rules <<) ; default plus << enabled
+; :in-theory (slow-<<-rules) ; slow rules enabled but << disabled
+; :in-theory (slow-<<-rules <<) ; slow rules and << enabled
+
+; These macros never enable BOTH the fast and slow rules. Sometimes
+; you need << and sometimes you don't. The optional << always has the
+; same effect whether you're using fast- or slow-<<-rules. Including
+; the << arg ENABLES <<.
+
+(defun ordinaryp (x)
+ (cond ((atom x)
+ (or (acl2-numberp x)
+ (characterp x)
+ (stringp x)
+ (symbolp x)))
+ (t (and (consp x)
+ (ordinaryp (car x))
+ (ordinaryp (cdr x))))))
+
+; This is used only for admitting the ordering relation.
+
+(defun vcount (x)
+ (cond ((atom x)
+ (cond ((acl2-numberp x) 0)
+ ((characterp x) 0)
+ ((stringp x) (+ 1 (length x)))
+ ((symbolp x)
+ (cond ((equal x nil) 0)
+ (t (+ 3
+ (length (symbol-package-name x))
+ (length (symbol-name x))))))
+ (t 0)))
+ (t (+ 1 (vcount (car x)) (vcount (cdr x))))))
+
+(local
+ (defthm vcount-character-listp
+ (implies (character-listp x)
+ (equal (vcount x) (len x)))))
+
+; The temptation below is to order all symbols by comparing their
+; symbol-package-names and their symbol-names, lexicographically. But
+; how does NIL compare to things? Since NIL occurs in its
+; symbol-package-name, such recursion would not terminate. So we put
+; NIL before all other symbols.
+
+(defun << (x y)
+ (declare (xargs :measure (vcount x)))
+ (cond
+ ((atom x)
+ (cond ((atom y)
+ (cond ((acl2-numberp x)
+ (cond ((acl2-numberp y) (< x y))
+ (t t)))
+ ((characterp x)
+ (cond ((acl2-numberp y) nil)
+ ((characterp y) (< (char-code x) (char-code y)))
+ (t t)))
+ ((stringp x)
+ (cond ((acl2-numberp y) nil)
+ ((characterp y) nil)
+ ((stringp y)
+ (<< (coerce x 'list)
+ (coerce y 'list)))
+ (t t)))
+ ((symbolp x)
+ (cond ((acl2-numberp y) nil)
+ ((characterp y) nil)
+ ((stringp y) nil)
+ ((symbolp y)
+ (cond ((equal x nil)
+ (cond ((equal y nil) nil)
+ (t t)))
+ ((equal y nil) nil)
+ (t
+ (or (<< (symbol-package-name x)
+ (symbol-package-name y))
+ (and (equal (symbol-package-name x)
+ (symbol-package-name y))
+ (<< (symbol-name x)
+ (symbol-name y)))))))
+ (t t)))
+ (t nil)))
+ (t t)))
+ ((atom y) nil)
+ (t (or (<< (car x) (car y))
+ (and (equal (car x) (car y))
+ (<< (cdr x) (cdr y)))))))
+
+; Now we prove that << is a total ordering on ACL2 objects.
+
+(defthm <<-irreflexivity
+ (not (<< x x)))
+
+(local
+ (defthm character-listp-implies-ordinaryp
+ (implies (character-listp x)
+ (ordinaryp x))))
+
+; The next three were pulled straight out of axioms.lisp, where they
+; were proved locally.
+
+(local
+ (defthm symbol-equality-rewrite
+ (implies (and (symbolp s1)
+ (symbolp s2)
+ (equal (symbol-name s1)
+ (symbol-name s2))
+ (equal (symbol-package-name s1)
+ (symbol-package-name s2)))
+ (equal (equal s1 s2) t))
+ :hints (("Goal" :use symbol-equality))))
+
+(local
+ (defthm equal-coerce
+ (implies (and (stringp x)
+ (stringp y))
+ (equal (equal (coerce x 'list)
+ (coerce y 'list))
+ (equal x y)))
+ :hints (("Goal" :use
+ ((:instance coerce-inverse-2 (x x))
+ (:instance coerce-inverse-2 (x y)))
+ :in-theory (disable coerce-inverse-2)))))
+
+(local
+ (defthm equal-char-code-rewrite
+ (implies (and (characterp x)
+ (characterp y))
+ (implies (equal (char-code x) (char-code y))
+ (equal (equal x y) t)))
+ :hints (("Goal" :use equal-char-code))))
+
+(defthm <<-trichotomy
+ (implies (and (ordinaryp x)
+ (ordinaryp y))
+ (or (<< x y)
+ (equal x y)
+ (<< y x)))
+ :rule-classes
+ ((:rewrite :corollary
+ (implies (and (ordinaryp x)
+ (ordinaryp y)
+ (not (<< x y))
+ (not (equal x y)))
+ (<< y x)))))
+
+(defthm <<-mutual-exclusion
+ (implies (<< x y)
+ (and (not (equal x y))
+ (not (<< y x))))
+ :rule-classes
+ ((:rewrite :corollary
+ (implies (<< x y)
+ (and (not (equal x y))
+ (not (<< y x)))))))
+
+(defthm <<-transitivity
+ (implies (and (<< x y) (<< y z)) (<< x z)))
+
+(defthm fast-<<-trichotomy
+ (and (implies (and (not (<< xxx y))
+ (equal xxx x)
+ (ordinaryp x)
+ (ordinaryp y)
+ (not (equal x y)))
+ (<< y x))
+ (implies (and (not (<< x yyy))
+ (equal yyy y)
+ (ordinaryp x)
+ (ordinaryp y)
+ (not (equal x y)))
+ (<< y x))))
+
+(defthm fast-<<-mutual-exclusion
+ (and (implies (and (<< xxx y)
+ (equal xxx x))
+ (and (not (equal x y))
+ (not (<< y x))))
+ (implies (and (<< x yyy)
+ (equal yyy y))
+ (and (not (equal x y))
+ (not (<< y x))))))
+
+(defthm fast-<<-transitivity
+ (implies (and (<< x y)
+ (<< yyy z)
+ (equal yyy x))
+ (<< x z)))
+
+(defmacro fast-<<-rules (&optional <<)
+
+; If << is non-nil, then enable <<, else, don't.
+
+ `(set-difference-theories (enable ,@(if << '((:DEFINITION <<)) nil)
+ fast-<<-trichotomy
+ fast-<<-mutual-exclusion
+ fast-<<-transitivity)
+ '(,@(if << nil '((:DEFINITION <<)))
+ <<-trichotomy
+ <<-mutual-exclusion
+ <<-transitivity)))
+
+(defmacro slow-<<-rules (&optional <<)
+
+; If << is non-nil, then enable <<, else, don't.
+
+ `(set-difference-theories (enable ,@(if << '((:DEFINITION <<)) nil)
+ <<-trichotomy
+ <<-mutual-exclusion
+ <<-transitivity)
+ '(,@(if << nil '((:DEFINITION <<)))
+ fast-<<-trichotomy
+ fast-<<-mutual-exclusion
+ fast-<<-transitivity)))
+
+(in-theory (fast-<<-rules))
+
diff --git a/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/total-ordering.lisp b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/total-ordering.lisp
new file mode 100644
index 0000000..0ff4c19
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/total-ordering.lisp
@@ -0,0 +1,165 @@
+; Finite Set Theory for ACL2
+
+; Copyright (C) 2001 Georgia Institute of Technology
+
+; This book is derived from the book "total-ordering-original" by J
+; Moore, which is included in this directory. The difference between
+; this version and J Moore's version is that I use the total order
+; built into ACL2 (starting with version 2.6). This allows me to
+; significantly simplify some of the theorems and to also remove
+; theorems.
+
+; 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 License
+; along with this program; if not, write to the Free Software
+; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
+
+; Written by: Panagiotis Manolios
+; email: manolios@cc.gatech.edu
+; College of Computing
+; CERCS Lab
+; Georgia Institute of Technology
+; 801 Atlantic Drive
+; Atlanta, Georgia 30332-0280 U.S.A.
+
+(in-package "ACL2")
+
+; We define an irreflexive total ordering on the ACL2 universe.
+
+; We export
+; (<< x y) disabled the total ordering
+
+; <<-irreflexivity the four obvious theorems about
+; <<-trichotomy disabled total orders
+; <<-mutual-exclusion disabled
+; <<-transitivity disabled
+
+; We provide ``fast'' versions of the slow rules, named
+
+; fast-<<-trichotomy enabled
+; fast-<<-mutual-exclusion enabled
+; fast-<<-transitivity enabled
+
+; We also provide two theory macros for fiddling with the status of
+; these rules.
+
+; Options:
+; :in-theory (fast-<<-rules) ; the default setting above
+; :in-theory (fast-<<-rules <<) ; default plus << enabled
+; :in-theory (slow-<<-rules) ; slow rules enabled but << disabled
+; :in-theory (slow-<<-rules <<) ; slow rules and << enabled
+
+; These macros never enable BOTH the fast and slow rules. Sometimes
+; you need << and sometimes you don't. The optional << always has the
+; same effect whether you're using fast- or slow-<<-rules. Including
+; the << arg ENABLES <<.
+
+(defun <<< (x y)
+ (declare (xargs :guard t))
+ (and (not (equal x y))
+ (lexorder x y)))
+
+(defun << (x y)
+ (declare (xargs :guard t))
+ (cond ((eq x nil)
+ (not (eq y nil)))
+ ((atom x)
+ (cond ((eq y nil) nil)
+ (t (<<< x y))))
+ ((atom y) nil)
+ ((equal (car x) (car y))
+ (<< (cdr x) (cdr y)))
+ (t (<< (car x) (car y)))))
+
+(defthm <<-irreflexivity
+ (not (<< x x)))
+
+(local
+(defthm lexorder-atom
+ (implies (and (atom x)
+ (consp y))
+ (lexorder x y))
+ :hints (("Goal" :in-theory (enable lexorder)))))
+
+(defthm <<-trichotomy
+ (or (<< x y)
+ (equal x y)
+ (<< y x))
+ :rule-classes
+ ((:rewrite :corollary
+ (implies (and (not (<< x y))
+ (not (equal x y)))
+ (<< y x)))))
+
+(defthm <<-mutual-exclusion
+ (implies (<< x y)
+ (and (not (equal x y))
+ (not (<< y x)))))
+
+(defthm <<-transitivity
+ (implies (and (<< x y)
+ (<< y z))
+ (<< x z)))
+
+(defthm fast-<<-trichotomy
+ (and (implies (and (not (<< xxx y))
+ (equal xxx x)
+ (not (equal x y)))
+ (<< y x))
+ (implies (and (not (<< x yyy))
+ (equal yyy y)
+ (not (equal x y)))
+ (<< y x))))
+
+(defthm fast-<<-mutual-exclusion
+ (and (implies (and (<< xxx y)
+ (equal xxx x))
+ (and (not (equal x y))
+ (not (<< y x))))
+ (implies (and (<< x yyy)
+ (equal yyy y))
+ (and (not (equal x y))
+ (not (<< y x))))))
+
+(defthm fast-<<-transitivity
+ (implies (and (<< x y)
+ (<< yyy z)
+ (equal yyy x))
+ (<< x z)))
+
+(defmacro fast-<<-rules (&optional <<)
+
+; If << is non-nil, then enable <<, else, don't.
+
+ `(set-difference-theories (enable ,@(if << '((:DEFINITION <<) (:definition acl2::alphorder)) nil)
+ fast-<<-trichotomy
+ fast-<<-mutual-exclusion
+ fast-<<-transitivity)
+ '(,@(if << nil '((:DEFINITION <<)))
+ <<-trichotomy
+ <<-mutual-exclusion
+ <<-transitivity)))
+
+(defmacro slow-<<-rules (&optional <<)
+
+; If << is non-nil, then enable <<, else, don't.
+
+ `(set-difference-theories (enable ,@(if << '((:DEFINITION <<) (:definition acl2::alphorder)) nil)
+ <<-trichotomy
+ <<-mutual-exclusion
+ <<-transitivity)
+ '(,@(if << nil '((:DEFINITION <<)))
+ fast-<<-trichotomy
+ fast-<<-mutual-exclusion
+ fast-<<-transitivity)))
+
+(in-theory (fast-<<-rules))
diff --git a/books/workshops/2002/manolios-kaufmann/support/records/certify-original.lsp b/books/workshops/2002/manolios-kaufmann/support/records/certify-original.lsp
new file mode 100644
index 0000000..755b6ca
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/records/certify-original.lsp
@@ -0,0 +1,2 @@
+(certify-book "records-original")
+:u
diff --git a/books/workshops/2002/manolios-kaufmann/support/records/certify.lsp b/books/workshops/2002/manolios-kaufmann/support/records/certify.lsp
new file mode 100644
index 0000000..c836b99
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/records/certify.lsp
@@ -0,0 +1,4 @@
+(certify-book "total-order")
+:u
+(certify-book "records")
+:u
diff --git a/books/workshops/2002/manolios-kaufmann/support/records/records-original.lisp b/books/workshops/2002/manolios-kaufmann/support/records/records-original.lisp
new file mode 100644
index 0000000..99326d3
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/records/records-original.lisp
@@ -0,0 +1,380 @@
+(in-package "ACL2")
+
+(defun fieldp (x)
+ (or (symbolp x) (integerp x)))
+
+(defthm fieldp-compound-recognizer
+ (iff (fieldp x)
+ (or (symbolp x)
+ (integerp x)))
+ :rule-classes :compound-recognizer)
+
+(defthm integerp-forward-chain-fieldp
+ (implies (integerp x) (fieldp x))
+ :rule-classes :forward-chaining)
+
+(defthm symbolp-forward-chain-fieldp
+ (implies (symbolp x) (fieldp x))
+ :rule-classes :forward-chaining)
+
+(in-theory (disable fieldp))
+
+(defun field-< (x y)
+ (if (symbolp x)
+ (and (symbolp y)
+ (symbol-< x y))
+ (or (symbolp y)
+ (< x y))))
+
+(local
+(defthm field-<-irreflexive
+ (not (field-< x x))))
+
+(local
+(defthm field-<-transitive
+ (implies (and (field-< x y)
+ (field-< y z))
+ (field-< x z))))
+
+(local
+(defthm field-<-asymmetric
+ (implies (field-< x y)
+ (not (field-< y x)))))
+
+(local
+(defthm field-<-trichotomy
+ (implies (and (fieldp x) (fieldp y)
+ (not (field-< y x)))
+ (iff (field-< x y)
+ (not (equal x y))))))
+
+(in-theory (disable field-<))
+
+
+
+
+; Ordered field-alist with no nil cdrs:
+(defun sap (x)
+ (if (atom x)
+ (null x)
+ (and (consp (car x))
+ (fieldp (caar x))
+ (cdar x)
+ (if (atom (cdr x))
+ (null (cdr x))
+ (and (sap (cdr x))
+ ;; We unforunately probably ruin tail-recursion here, but at
+ ;; least we can verify the guards.
+ (field-< (caar x) (caadr x)))))))
+
+; Lookup structure:
+(defun lsp (x)
+ (or (sap x)
+ (and (consp x)
+ (not (lsp (cdr x)))
+ (sap (car x))
+ (car x))))
+
+(defun g (a x)
+ (cond
+ ((sap x)
+ (cdr (assoc-equal a x)))
+ ((lsp x)
+ (cdr (assoc-equal a (car x))))
+ (t
+ nil)))
+
+; Ordinary setting, used for non-nil values:
+(defun s-aux (a v r)
+ (cond ((endp r)
+ (cons (cons a v) nil))
+ ((equal a (caar r))
+ (cons (cons a v) (cdr r)))
+ ((field-< a (caar r))
+ (cons (cons a v) r))
+ (t (cons (car r) (s-aux a v (cdr r))))))
+
+(defun delete-key (key 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)
+ (cond
+ ((sap 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))
+ ((null v)
+ (if (and (null (cdr (car x)))
+ (equal (caar (car x)) a))
+ (cdr x)
+ (cons (delete-key a (car x))
+ (cdr x))))
+ (t
+ (cons (s-aux a v (car x))
+ (cdr x)))))
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;; Interaction properties for s and g;
+;;; search for $$$ for main theorems.
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(local
+(defthm not-field-<-x-x
+ (not (field-< x x))
+ :hints (("Goal" :in-theory (enable field-<)))))
+
+(local
+(defthm delete-key-no-op
+ (implies (and (sap alist)
+ (not (assoc-equal key alist)))
+ (equal (delete-key key alist) alist))))
+
+(local
+(defthm values-not-nil
+ (implies (sap 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 (fieldp a)
+ (sap alist)
+ (field-< a (caar alist)))
+ (not (cdr (assoc-equal a alist))))))
+
+(local
+(defthm s-aux-to-same
+ (implies (and (fieldp a)
+ (sap alist)
+ (cdr (assoc-equal a alist)))
+ (equal (s-aux a (cdr (assoc-equal a alist))
+ alist)
+ alist))))
+
+; $$$ A main theorem
+(defthm s-same-g
+ (implies (force (fieldp a))
+ (equal (s a (g a r) r)
+ r)))
+
+(local
+(defthm value-s-aux
+ (implies (and (fieldp a)
+ (sap alist))
+ (equal (cdr (assoc-equal a (s-aux a v alist)))
+ v))))
+
+(local
+(defthm s-aux-preserves-sap
+ (implies (and (sap x)
+ (fieldp a)
+ v)
+ (sap (s-aux a v x)))))
+
+(local
+(defthm cdr-assoc-equal-delete-key
+ (implies (sap 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 sap-delete-key
+ (implies (sap alist)
+ (sap (delete-key a alist)))))
+
+(local
+(defthm sap-forward-to-fieldp-caar
+ (implies (sap alist)
+ (fieldp (caar alist)))
+ :rule-classes :forward-chaining))
+
+; $$$ A main theorem
+(defthm g-same-s
+ (implies (force (fieldp a))
+ (equal (g a (s a v r))
+ v)))
+
+(local
+(defthm s-aux-s-aux-same
+ (implies (and (fieldp a)
+ (sap alist))
+ (equal (s-aux a v (s-aux a w alist))
+ (s-aux a v alist)))))
+
+(local
+(defthm delete-key-s-aux-same
+ (implies (and (fieldp a)
+ (sap alist))
+ (equal (delete-key a (s-aux a v alist))
+ (delete-key a alist)))))
+
+(local
+(defthm field-<-s-aux
+ (implies (and (sap alist)
+ (fieldp a)
+ (fieldp b)
+ (field-< b (caar alist))
+ (not (field-< a b))
+ (not (equal a b)))
+ (field-< b (caar (s-aux a v alist))))))
+
+(local
+(defthm value-nil-sufficiency
+ (implies (and (sap alist)
+ (fieldp a)
+ (field-< a (caar alist)))
+ (equal (cdr (assoc-equal a alist))
+ nil))))
+
+(local
+(defthm caar-delete-key
+ (implies (sap alist)
+ (equal (caar (delete-key a alist))
+ (if (eq a (caar alist))
+ (caadr alist)
+ (caar alist))))))
+
+(local
+(defthm s-aux-delete-key
+ (implies (sap alist)
+ (equal (s-aux a x (delete-key a alist))
+ (s-aux a x alist)))))
+
+(local
+(defthm field-<-hack
+ (implies (and (field-< r6 r9)
+ (not (field-< r4 r9))
+ (not (equal r6 r4))
+ (fieldp r4)
+ (fieldp r6)
+ (fieldp r9))
+ (field-< r6 r4))
+ :hints (("Goal" :in-theory (disable field-<-trichotomy)
+ :use ((:instance field-<-trichotomy
+ (x r6) (y r4)))))))
+
+; $$$ A main theorem
+(defthm s-same-s
+ (implies (force (fieldp a))
+ (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))
+ (sap r)
+ x
+ y
+ (fieldp a)
+ (fieldp 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-aux))))
+ ;; The earlier forward-chaining rule hurts here.
+ :hints (("Goal" :in-theory (disable sap-forward-to-fieldp-caar)))))
+
+(local
+(defthm sap-s-aux
+ (implies (and (sap x)
+ (fieldp a)
+ v)
+ (sap (s-aux a v x)))))
+
+(local
+(defthm consp-delete-key
+ (implies (sap 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 (sap 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))
+ (sap r)
+ x
+ (fieldp a)
+ (fieldp b))
+ (equal (delete-key b (s-aux a x r))
+ (s-aux a x (delete-key b r))))
+ ;; The earlier forward-chaining rule hurts here.
+ :hints (("Goal" :in-theory (disable sap-forward-to-fieldp-caar)))))
+
+(local
+(defthm delete-key-nil
+ (implies (not (delete-key a x))
+ (not (delete-key a (delete-key b x))))))
+
+; $$$ A main theorem
+(defthm s-diff-s
+ (implies (and (force (fieldp a))
+ (force (fieldp b))
+ (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)))))
+
+(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)))))
+
+; $$$ A main theorem
+(defthm g-diff-s
+ (implies (and (force (fieldp a))
+ (force (fieldp b))
+ (not (equal a b)))
+ (equal (g a (s b v r))
+ (g a r))))
+
+
+;;;; some simple macros for defining sets and gets..
+
+(in-theory (disable s g))
+
+(defmacro <- (x a) `(g ,a ,x))
+
+(defmacro -> (x a v) `(s ,a ,v ,x))
+
+(defun update-macro (upds result)
+ (declare (xargs :guard (keyword-value-listp upds)))
+ (if (endp upds) result
+ (update-macro (cddr upds)
+ (list 's (car upds) (cadr upds) result))))
+
+(defmacro update (old &rest updates)
+ (declare (xargs :guard (keyword-value-listp updates)))
+ (update-macro updates old))
diff --git a/books/workshops/2002/manolios-kaufmann/support/records/records.lisp b/books/workshops/2002/manolios-kaufmann/support/records/records.lisp
new file mode 100644
index 0000000..e7e40a2
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/records/records.lisp
@@ -0,0 +1,287 @@
+(in-package "ACL2")
+(include-book "total-order")
+
+; Ordered field-alist with no nil cdrs:
+(defun sap (x)
+ (if (atom x)
+ (null x)
+ (and (consp (car x))
+ (cdar x)
+ (if (atom (cdr x))
+ (null (cdr x))
+ (and (sap (cdr x))
+ ;; We unforunately probably ruin tail-recursion here, but at
+ ;; least we can verify the guards.
+ (<< (caar x) (caadr x)))))))
+
+; Lookup structure:
+(defun lsp (x)
+ (or (sap x)
+ (and (consp x)
+ (not (lsp (cdr x)))
+ (sap (car x))
+ (car x))))
+
+(defun g (a x)
+ (cond
+ ((sap x)
+ (cdr (assoc-equal a x)))
+ ((lsp x)
+ (cdr (assoc-equal a (car x))))
+ (t
+ nil)))
+
+; Ordinary setting, used for non-nil values:
+(defun s-aux (a v 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)
+ (cond
+ ((endp alist)
+ alist)
+ ((equal key (caar alist))
+ (cdr alist))
+ (t
+ (cons (car alist)
+ (delete-key key (cdr alist))))))
+
+(defun s (a v x)
+ (cond
+ ((sap 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))
+ ((null v)
+ (if (and (null (cdr (car x)))
+ (equal (caar (car x)) a))
+ (cdr x)
+ (cons (delete-key a (car x))
+ (cdr x))))
+ (t
+ (cons (s-aux a v (car x))
+ (cdr x)))))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;; Interaction properties for s and g;
+;;; search for $$$ for main theorems.
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(local
+(defthm delete-key-no-op
+ (implies (and (sap alist)
+ (not (assoc-equal key alist)))
+ (equal (delete-key key alist) alist))))
+
+(local
+(defthm values-not-nil
+ (implies (sap 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 (sap alist)
+ (<< a (caar alist)))
+ (not (cdr (assoc-equal a alist))))))
+
+(local
+(defthm s-aux-to-same
+ (implies (and (sap alist)
+ (cdr (assoc-equal a alist)))
+ (equal (s-aux a (cdr (assoc-equal a alist))
+ alist)
+ alist))))
+
+; $$$ A main theorem
+(defthm s-same-g
+ (equal (s a (g a r) r)
+ r))
+
+(local
+(defthm value-s-aux
+ (implies (sap alist)
+ (equal (cdr (assoc-equal a (s-aux a v alist)))
+ v))))
+
+(local
+(defthm s-aux-preserves-sap
+ (implies (and (sap x)
+ v)
+ (sap (s-aux a v x)))))
+
+(local
+(defthm cdr-assoc-equal-delete-key
+ (implies (sap 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 sap-delete-key
+ (implies (sap alist)
+ (sap (delete-key a alist)))))
+
+; $$$ A main theorem
+(defthm g-same-s
+ (equal (g a (s a v r))
+ v))
+
+(local
+(defthm s-aux-s-aux-same
+ (implies (sap alist)
+ (equal (s-aux a v (s-aux a w alist))
+ (s-aux a v alist)))))
+
+(local
+(defthm delete-key-s-aux-same
+ (implies (sap alist)
+ (equal (delete-key a (s-aux a v alist))
+ (delete-key a alist)))))
+
+(local
+(defthm <<-s-aux
+ (implies (and (sap 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 (sap alist)
+ (<< a (caar alist)))
+ (equal (cdr (assoc-equal a alist))
+ nil))))
+
+(local
+(defthm caar-delete-key
+ (implies (sap alist)
+ (equal (caar (delete-key a alist))
+ (if (eq a (caar alist))
+ (caadr alist)
+ (caar alist))))))
+
+(local
+(defthm s-aux-delete-key
+ (implies (sap 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)))))))
+
+; $$$ A main theorem
+(defthm 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))
+ (sap 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 sap-s-aux
+ (implies (and (sap x)
+ v)
+ (sap (s-aux a v x)))))
+
+(local
+(defthm consp-delete-key
+ (implies (sap 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 (sap 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))
+ (sap 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))))))
+
+; $$$ A main theorem
+(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)))))
+
+(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)))))
+
+; $$$ A main theorem
+(defthm g-diff-s
+ (implies (not (equal a b))
+ (equal (g a (s b v r))
+ (g a r))))
+
+
+;;;; some simple macros for defining sets and gets..
+
+(in-theory (disable s g))
+
+(defmacro <- (x a) `(g ,a ,x))
+
+(defmacro -> (x a v) `(s ,a ,v ,x))
+
+(defun update-macro (upds result)
+ (declare (xargs :guard (keyword-value-listp upds)))
+ (if (endp upds) result
+ (update-macro (cddr upds)
+ (list 's (car upds) (cadr upds) result))))
+
+(defmacro update (old &rest updates)
+ (declare (xargs :guard (keyword-value-listp updates)))
+ (update-macro updates old))
diff --git a/books/workshops/2002/manolios-kaufmann/support/records/total-order.lisp b/books/workshops/2002/manolios-kaufmann/support/records/total-order.lisp
new file mode 100644
index 0000000..71ec212
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/records/total-order.lisp
@@ -0,0 +1,28 @@
+; Copyright (C) 2001 Georgia Institute of Technology
+
+; This program is free software; you can redistribute it and/or modify it under
+; the terms of Version 2 of the GNU General Public License as published by the
+; Free Software Foundation.
+
+; 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 License
+; along with this program; if not, write to the Free Software
+; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
+
+; Written by: Panagiotis Manolios who can be reached as follows.
+
+; Email: manolios@cc.gatech.edu
+
+; Postal Mail:
+; College of Computing
+; CERCS Lab
+; Georgia Institute of Technology
+; 801 Atlantic Drive
+; Atlanta, Georgia 30332-0280 U.S.A.
+
+(in-package "ACL2")
+(include-book "../../../../../misc/total-order")
diff --git a/books/workshops/2002/manolios-kaufmann/support/sorting/certify.lsp b/books/workshops/2002/manolios-kaufmann/support/sorting/certify.lsp
new file mode 100644
index 0000000..72154de
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/sorting/certify.lsp
@@ -0,0 +1,10 @@
+(certify-book "perm")
+:u
+(certify-book "total-order")
+:u
+(certify-book "perm-order")
+:u
+(certify-book "insertion-sort")
+:u
+(certify-book "quicksort")
+:u
diff --git a/books/workshops/2002/manolios-kaufmann/support/sorting/insertion-sort.lisp b/books/workshops/2002/manolios-kaufmann/support/sorting/insertion-sort.lisp
new file mode 100644
index 0000000..1ba5653
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/sorting/insertion-sort.lisp
@@ -0,0 +1,104 @@
+; Copyright (C) 2001 Georgia Institute of Technology
+
+; 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 License
+; along with this program; if not, write to the Free Software
+; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
+
+; Written by: Panagiotis Manolios who can be reached as follows.
+
+; Email: manolios@cc.gatech.edu
+
+; Postal Mail:
+; College of Computing
+; CERCS Lab
+; Georgia Institute of Technology
+; 801 Atlantic Drive
+; Atlanta, Georgia 30332-0280 U.S.A.
+
+(in-package "ACL2")
+
+(include-book "perm-order")
+
+(defun insert (a x)
+ (if (consp x)
+ (if (<<= a (car x))
+ (cons a x)
+ (cons (car x) (insert a (cdr x))))
+ (list a)))
+
+(defun isort (x)
+ (if (consp x)
+ (insert (car x) (isort (cdr x)))
+ nil))
+
+(defthm ordered-insert
+ (implies (orderedp y)
+ (orderedp (insert x y))))
+
+(defthm ordered-sort
+ (orderedp (isort x)))
+
+(defthm perm-insert
+ (perm (insert x y) (cons x y)))
+
+(defthm perm-sort
+ (perm (isort x) x))
+
+(defthm insert-insert
+ (equal (insert x (insert y z))
+ (insert y (insert x z)))
+ :rule-classes ((:rewrite :loop-stopper ((x y)))))
+
+(defthm insert-in
+ (equal (isort (insert x y))
+ (isort (cons x y))))
+
+(defthm insert-sort-remove
+ (implies (in x y)
+ (equal (insert x (isort (remove-el x y)))
+ (isort y))))
+
+(defthm sort-canonical
+ (implies (and (perm x y)
+ ;; Added for mod to ACL2 v2-8 that does better matching for calls of
+ ;; equivalence relations against the current context, to avoid a rewriter
+ ;; loop in the proof of mail:
+ (syntaxp (not (term-order x y))))
+ (equal (isort x)
+ (isort y))))
+
+(defthm main
+ (equal (perm x y)
+ (equal (isort x)
+ (isort y)))
+ :hints (("goal"
+ :use ((:instance perm-sort (x y))
+ (:instance perm-sort))
+ :in-theory (disable perm-sort)))
+ :rule-classes nil)
+
+(defthm main2
+ (implies (and (orderedp x)
+ (perm x y))
+ (equal (isort y)
+ x))
+ :rule-classes nil)
+
+(defthm main3
+ (implies (and (orderedp x)
+ (orderedp y)
+ (perm x y))
+ (equal x y))
+ :hints (("goal"
+ :use ((:instance main2) (:instance main2 (x y)))))
+ :rule-classes nil)
diff --git a/books/workshops/2002/manolios-kaufmann/support/sorting/perm-order.lisp b/books/workshops/2002/manolios-kaufmann/support/sorting/perm-order.lisp
new file mode 100644
index 0000000..3b586fc
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/sorting/perm-order.lisp
@@ -0,0 +1,39 @@
+; Copyright (C) 2001 Georgia Institute of Technology
+
+; 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 License
+; along with this program; if not, write to the Free Software
+; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
+
+; Written by: Panagiotis Manolios who can be reached as follows.
+
+; Email: manolios@cc.gatech.edu
+
+; Postal Mail:
+; College of Computing
+; CERCS Lab
+; Georgia Institute of Technology
+; 801 Atlantic Drive
+; Atlanta, Georgia 30332-0280 U.S.A.
+
+(in-package "ACL2")
+(include-book "perm")
+(include-book "total-order")
+
+(defun <<= (x y)
+ (lexorder x y))
+
+(defun orderedp (x)
+ (cond ((atom x) (null x))
+ (t (or (null (cdr x))
+ (and (<<= (car x) (cadr x))
+ (orderedp (cdr x)))))))
diff --git a/books/workshops/2002/manolios-kaufmann/support/sorting/perm.lisp b/books/workshops/2002/manolios-kaufmann/support/sorting/perm.lisp
new file mode 100644
index 0000000..718b72f
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/sorting/perm.lisp
@@ -0,0 +1,107 @@
+; Copyright (C) 2001 Georgia Institute of Technology
+
+; 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 License
+; along with this program; if not, write to the Free Software
+; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
+
+; Written by: Panagiotis Manolios who can be reached as follows.
+
+; Email: manolios@cc.gatech.edu
+
+; Postal Mail:
+; College of Computing
+; CERCS Lab
+; Georgia Institute of Technology
+; 801 Atlantic Drive
+; Atlanta, Georgia 30332-0280 U.S.A.
+
+(in-package "ACL2")
+
+(defun in (a X)
+ (declare (xargs :guard t))
+ (cond ((atom X) nil)
+ ((equal a (car X)) t)
+ (t (in a (cdr X)))))
+
+(defun remove-el (a x)
+ (declare (xargs :guard t))
+ (cond ((atom x) nil)
+ ((equal a (car x)) (cdr x))
+ (t (cons (car x) (remove-el a (cdr x))))))
+
+(defun perm (x y)
+ (declare (xargs :guard t))
+ (cond ((atom x) (atom y))
+ (t (and (in (car x) y)
+ (perm (cdr x) (remove-el (car x) y))))))
+
+(defthm perm-reflexive
+ (perm a a))
+
+(defthm remove-el-swap
+ (equal (remove-el a (remove-el b x))
+ (remove-el b (remove-el a x))))
+
+(defthm remove-el-in
+ (implies (not (equal a b))
+ (equal (in a (remove-el b y))
+ (in a y))))
+
+(local
+ (defthm perm-remove
+ (implies (perm x y)
+ (perm (remove-el a x) (remove-el a y)))))
+
+(defthm car-perm
+ (implies (and (consp x)
+ (not (in (car x) y)))
+ (not (perm y x))))
+
+(defthm perm-symmetric
+ (implies (perm x y)
+ (perm y x))
+ :hints (("Goal"
+ :induct (perm y x))
+ ("Subgoal *1/2''"
+ :use ((:instance perm-remove (a (car y)))))))
+
+(defthm perm-in
+ (implies (and (perm x y)
+ (in a x))
+ (in a y))
+ :rule-classes ((:forward-chaining :trigger-terms ((in a x) (in a y)))))
+
+(defthm perm-transitive
+ (implies (and (perm x y) (perm y z))
+ (perm x z)))
+
+(defequiv perm)
+
+(defthm perm-remove-el-app
+ (implies (in x y)
+ (equal (remove-el x (append y z))
+ (append (remove-el x y) z))))
+
+(defcong perm perm (append x y) 1)
+
+(defcong perm perm (append x y) 2)
+
+(defcong perm perm (cons x y) 2)
+
+(defcong perm perm (remove-el x y) 2)
+
+(defthm perm-app-cons
+ (perm (append x (cons y z))
+ (cons y (append x z))))
+
+(defcong perm equal (in x y) 2)
diff --git a/books/workshops/2002/manolios-kaufmann/support/sorting/quicksort.lisp b/books/workshops/2002/manolios-kaufmann/support/sorting/quicksort.lisp
new file mode 100644
index 0000000..970593e
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/sorting/quicksort.lisp
@@ -0,0 +1,107 @@
+; Copyright (C) 2001 Georgia Institute of Technology
+
+; 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 License
+; along with this program; if not, write to the Free Software
+; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
+
+; Written by: Panagiotis Manolios who can be reached as follows.
+
+; Email: manolios@cc.gatech.edu
+
+; Postal Mail:
+; College of Computing
+; CERCS Lab
+; Georgia Institute of Technology
+; 801 Atlantic Drive
+; Atlanta, Georgia 30332-0280 U.S.A.
+
+(in-package "ACL2")
+
+(include-book "insertion-sort")
+
+(defun less (x lst)
+ (cond ((atom lst) nil)
+ ((<< (car lst) x)
+ (cons (car lst) (less x (cdr lst))))
+ (t (less x (cdr lst)))))
+
+(defun notless (x lst)
+ (cond ((atom lst) nil)
+ ((not (<< (car lst) x))
+ (cons (car lst) (notless x (cdr lst))))
+ (t (notless x (cdr lst)))))
+
+(defun qsort (x)
+ (cond ((atom x) nil)
+ (t (append (qsort (less (car x) (cdr x)))
+ (list (car x))
+ (qsort (notless (car x) (cdr x)))))))
+
+(defun lessp (x lst)
+ (cond ((atom lst) t)
+ (t (and (<< (car lst) x)
+ (lessp x (cdr lst))))))
+
+(defun notlessp (x lst)
+ (cond ((atom lst) t)
+ (t (and (not (<< (car lst) x))
+ (notlessp x (cdr lst))))))
+
+(defthm perm-less-notless
+ (perm (append (less x y) (notless x y))
+ y))
+
+(defthm perm-qsort
+ (perm (qsort x) x))
+
+(defthm lessp-less
+ (lessp x (less x lst)))
+
+(defthm notlessp-notless
+ (notlessp x (notless x lst)))
+
+(defcong perm equal (lessp x lst) 2)
+
+(defcong perm equal (notlessp x lst) 2)
+
+(defthm lessp-less-qsort
+ (lessp x (qsort (less x lst))))
+
+(defthm notlessp-notless-qsort
+ (notlessp x (qsort (notless x lst))))
+
+(defthm orderedp-lemma
+ (implies (and (orderedp x)
+ (orderedp y)
+ (lessp z x)
+ (notlessp z y))
+ (orderedp (append x (cons z y))))
+ :hints (("goal" :in-theory (enable <<))))
+
+(defthm qsort-is-ordered
+ (orderedp (qsort x)))
+
+(defthm qsort-main
+ (equal (qsort x)
+ (isort x))
+ :hints (("goal" :use (:instance main2 (x (qsort x)) (y x)))))
+
+#|
+Or we can prove it as follows:
+
+(defthm qsort-main
+ (equal (qsort x)
+ (isort x))
+ :hints (("goal" :use (:instance main3 (x (qsort x)) (y (isort x))))))
+
+|# \ No newline at end of file
diff --git a/books/workshops/2002/manolios-kaufmann/support/sorting/total-order.lisp b/books/workshops/2002/manolios-kaufmann/support/sorting/total-order.lisp
new file mode 100644
index 0000000..c5984f1
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/sorting/total-order.lisp
@@ -0,0 +1,29 @@
+; Copyright (C) 2001 Georgia Institute of Technology
+
+; 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 License
+; along with this program; if not, write to the Free Software
+; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
+
+; Written by: Panagiotis Manolios who can be reached as follows.
+
+; Email: manolios@cc.gatech.edu
+
+; Postal Mail:
+; College of Computing
+; CERCS Lab
+; Georgia Institute of Technology
+; 801 Atlantic Drive
+; Atlanta, Georgia 30332-0280 U.S.A.
+
+(in-package "ACL2")
+(include-book "../../../../../misc/total-order")
diff --git a/books/workshops/2002/manolios-kaufmann/support/total-order/README b/books/workshops/2002/manolios-kaufmann/support/total-order/README
new file mode 100644
index 0000000..2901539
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/total-order/README
@@ -0,0 +1,11 @@
+The books in this directory should be certified with ACL2 v2.5. They
+are:
+
+1. total-order: this is the book described in section 2.1 of the
+ paper.
+
+2. total-order-easy-direction: this is the book refered to at the end
+ of section 2.1.
+
+3. soundness: this is the book refered to in section 2.2.
+
diff --git a/books/workshops/2002/manolios-kaufmann/support/total-order/cert_pl_exclude b/books/workshops/2002/manolios-kaufmann/support/total-order/cert_pl_exclude
new file mode 100644
index 0000000..ee02a5e
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/total-order/cert_pl_exclude
@@ -0,0 +1,10 @@
+cert_pl_exclude
+
+The presence of this file tells cert.pl not to try to build any of the books in
+this directory.
+
+Quoting from workshops/2002/manolios-kaufmann/support/Makefile:
+
+# Note: total-order is deliberately not included in DIRS because its
+# certification fails for ACL2 versions after 2.5.
+
diff --git a/books/workshops/2002/manolios-kaufmann/support/total-order/certify.lsp b/books/workshops/2002/manolios-kaufmann/support/total-order/certify.lsp
new file mode 100644
index 0000000..7c7541c
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/total-order/certify.lsp
@@ -0,0 +1,6 @@
+(certify-book "total-order")
+:u
+(certify-book "total-order-easy-direction")
+:u
+(certify-book "soundness")
+:u
diff --git a/books/workshops/2002/manolios-kaufmann/support/total-order/soundness.lisp b/books/workshops/2002/manolios-kaufmann/support/total-order/soundness.lisp
new file mode 100644
index 0000000..f6646ab
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/total-order/soundness.lisp
@@ -0,0 +1,205 @@
+; Copyright (C) 2001 Georgia Institute of Technology
+
+; 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 License
+; along with this program; if not, write to the Free Software
+; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
+
+; Written by: Panagiotis Manolios who can be reached as follows.
+
+; Email: manolios@cc.gatech.edu
+
+; Postal Mail:
+; College of Computing
+; CERCS Lab
+; Georgia Institute of Technology
+; 801 Atlantic Drive
+; Atlanta, Georgia 30332-0280 U.S.A.
+
+; Certify with ACL2 version 2.5
+
+(in-package "ACL2")
+
+(defun good-atom (x)
+ (and (atom x)
+ (or (acl2-numberp x)
+ (symbolp x)
+ (characterp x)
+ (stringp x))))
+
+(defthm good-atom-compound-recognizer
+ (iff (good-atom x)
+ (and (atom x)
+ (or (acl2-numberp x)
+ (symbolp x)
+ (characterp x)
+ (stringp x))))
+ :rule-classes :compound-recognizer)
+
+(in-theory (disable good-atom))
+
+(defun good-atom-order (x y)
+ (cond ((rationalp x)
+ (if (rationalp y)
+ (<= x y)
+ t))
+ ((rationalp y) nil)
+ ((complex-rationalp x)
+ (if (complex-rationalp y)
+ (or (< (realpart x) (realpart y))
+ (and (= (realpart x) (realpart y))
+ (<= (imagpart x) (imagpart y))))
+ t))
+ ((complex-rationalp y)
+ nil)
+ ((characterp x)
+ (if (characterp y)
+ (<= (char-code x)
+ (char-code y))
+ t))
+ ((characterp y) nil)
+ ((stringp x)
+ (if (stringp y)
+ (and (string<= x y) t)
+ t))
+ ((stringp y) nil)
+ ((symbolp x)
+ (if (symbolp y)
+ (not (symbol-< y x))
+ t))
+ ((symbolp y) nil)
+ (t t)))
+
+(defmacro boolp (x)
+ `(or (equal ,x t)
+ (equal ,x nil)))
+
+(defthm boolp-good-atom-order
+ (boolp (good-atom-order x y))
+ :rule-classes :type-prescription)
+
+(defthm good-atom-order-reflexive
+ (implies (atom x)
+ (good-atom-order x x)))
+
+(defthm equal-coerce
+ (implies (and (stringp x)
+ (stringp y))
+ (equal (equal (coerce x 'list)
+ (coerce y 'list))
+ (equal x y)))
+ :hints (("Goal" :use
+ ((:instance coerce-inverse-2 (x x))
+ (:instance coerce-inverse-2 (x y)))
+ :in-theory (disable coerce-inverse-2))))
+
+(defthm string<=-l-transitive-at-0
+ (implies (and (not (string<-l y x 0))
+ (not (string<-l z y 0))
+ (character-listp x)
+ (character-listp y)
+ (character-listp z))
+ (not (string<-l z x 0)))
+ :hints
+ (("Goal" :use (:instance string<-l-transitive
+ (i 0) (j 0) (k 0)))))
+
+(defthm good-atom-order-transitive
+ (implies (and (good-atom-order x y)
+ (good-atom-order y z)
+ (atom x)
+ (atom y)
+ (atom z))
+ (good-atom-order x z))
+ :hints (("Goal"
+ :in-theory (enable string< symbol-<))))
+
+(defthm good-atom-order-anti-symmetric
+ (implies (and (good-atom x)
+ (good-atom-order x y)
+ (good-atom-order y x))
+ (equal x y))
+ :hints (("Goal"
+ :in-theory (union-theories
+ '(string< symbol-<)
+ (disable code-char-char-code-is-identity))
+ :use ((:instance symbol-equality (s1 x) (s2 y))
+ (:instance code-char-char-code-is-identity (c y))
+ (:instance code-char-char-code-is-identity (c x)))))
+ :rule-classes
+ ((:forward-chaining :corollary
+ (implies (and (good-atom-order x y)
+ (good-atom x)
+ (not (consp x))
+ (not (consp y)))
+ (iff (good-atom-order y x)
+ (equal x y)))
+ :hints (("Goal" :in-theory
+ (disable good-atom-order))))))
+
+(defthm good-atom-order-total
+ (implies (and (atom x)
+ (atom y))
+ (or (good-atom-order x y)
+ (good-atom-order y x)))
+ :hints (("Goal"
+ :in-theory (enable string< symbol-<)))
+ :rule-classes
+ ((:forward-chaining :corollary
+ (implies (and (not (good-atom-order x y))
+ (not (consp x))
+ (not (consp y)))
+ (good-atom-order y x)))))
+
+(in-theory (disable good-atom-order))
+
+(defun good-object (x)
+ (if (consp x)
+ (and (good-object (car x))
+ (good-object (cdr x)))
+ (good-atom x)))
+
+(defun good-object-order (x y)
+ (cond ((atom x)
+ (cond ((atom y)
+ (good-atom-order x y))
+ (t t)))
+ ((atom y) nil)
+ ((equal (car x) (car y))
+ (good-object-order (cdr x) (cdr y)))
+ (t (good-object-order (car x) (car y)))))
+
+(defthm boolp-good-object-order
+ (boolp (good-object-order x y))
+ :rule-classes :type-prescription)
+
+(defthm good-object-order-reflexive
+ (good-object-order x x))
+
+(defthm good-object-order-anti-symmetric
+ (implies (and (good-object-order x y)
+ (good-object-order y x)
+ (good-object x)
+ (good-object y))
+ (equal x y))
+ :rule-classes :forward-chaining)
+
+(defthm good-object-order-transitive
+ (implies (and (good-object x)
+ (good-object-order x y)
+ (good-object-order y z))
+ (good-object-order x z)))
+
+(defthm good-object-order-total
+ (or (good-object-order x y)
+ (good-object-order y x))
+ :rule-classes nil)
diff --git a/books/workshops/2002/manolios-kaufmann/support/total-order/total-order-easy-direction.lisp b/books/workshops/2002/manolios-kaufmann/support/total-order/total-order-easy-direction.lisp
new file mode 100644
index 0000000..d46c9a1
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/total-order/total-order-easy-direction.lisp
@@ -0,0 +1,98 @@
+; Copyright (C) 2001 Georgia Institute of Technology
+
+; 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 License
+; along with this program; if not, write to the Free Software
+; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
+
+; Written by: Panagiotis Manolios who can be reached as follows.
+
+; Email: manolios@cc.gatech.edu
+
+; Postal Mail:
+; College of Computing
+; CERCS Lab
+; Georgia Institute of Technology
+; 801 Atlantic Drive
+; Atlanta, Georgia 30332-0280 U.S.A.
+
+; Certify with ACL2 version 2.5
+
+(in-package "ACL2")
+
+(defmacro boolp (x)
+ `(or (equal ,x t)
+ (equal ,x nil)))
+
+(defstub total-order (x y) t)
+
+(defun bad-atom (x)
+ (not (or (consp x)
+ (acl2-numberp x)
+ (symbolp x)
+ (characterp x)
+ (stringp x))))
+
+(defaxiom boolp-total-order
+ (boolp (total-order x y))
+ :rule-classes :type-prescription)
+
+(defaxiom total-order-anti-symmetric
+ (implies (and (total-order x y)
+ (total-order y x))
+ (equal x y))
+ :rule-classes :forward-chaining)
+
+(defaxiom total-order-transitive
+ (implies (and (total-order x y)
+ (total-order y z))
+ (total-order x z)))
+
+(defaxiom total-order-total
+ (or (total-order x y)
+ (total-order y x))
+ :rule-classes nil)
+
+(encapsulate
+ ((bad-atom<= (x y) t))
+ (local (defun bad-atom<= (x y)
+ (total-order x y)))
+
+ (defthm boolp-bad-atom<=
+ (boolp (bad-atom<= x y))
+ :rule-classes :type-prescription)
+
+ (defthm bad-atom<=-anti-symmetric
+ (implies (and (bad-atom x)
+ (bad-atom y)
+ (bad-atom<= x y)
+ (bad-atom<= y x))
+ (equal x y))
+ :hints (("goal" :use total-order-anti-symmetric))
+ :rule-classes nil)
+
+ (defthm bad-atom<=-transitive
+ (implies (and (bad-atom x)
+ (bad-atom y)
+ (bad-atom z)
+ (bad-atom<= x y)
+ (bad-atom<= y z))
+ (bad-atom<= x z)))
+
+ (defthm bad-atom<=-total
+ (implies (and (bad-atom x)
+ (bad-atom y))
+ (or (bad-atom<= x y)
+ (bad-atom<= y x)))
+ :hints (("goal" :use total-order-total))
+ :rule-classes nil))
+
diff --git a/books/workshops/2002/manolios-kaufmann/support/total-order/total-order.lisp b/books/workshops/2002/manolios-kaufmann/support/total-order/total-order.lisp
new file mode 100644
index 0000000..a6a5d23
--- /dev/null
+++ b/books/workshops/2002/manolios-kaufmann/support/total-order/total-order.lisp
@@ -0,0 +1,239 @@
+; Copyright (C) 2001 Georgia Institute of Technology
+
+; 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 License
+; along with this program; if not, write to the Free Software
+; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
+
+; Written by: Panagiotis Manolios who can be reached as follows.
+
+; Email: manolios@cc.gatech.edu
+
+; Postal Mail:
+; College of Computing
+; CERCS Lab
+; Georgia Institute of Technology
+; 801 Atlantic Drive
+; Atlanta, Georgia 30332-0280 U.S.A.
+
+; Certify with ACL2 version 2.5
+
+(in-package "ACL2")
+
+(defun bad-atom (x)
+ (not (or (consp x)
+ (acl2-numberp x)
+ (symbolp x)
+ (characterp x)
+ (stringp x))))
+
+(defstub bad-atom<= (* *) => *)
+
+(defmacro boolp (x)
+ `(or (equal ,x t)
+ (equal ,x nil)))
+
+(defaxiom boolp-bad-atom<=
+ (boolp (bad-atom<= x y))
+ :rule-classes :type-prescription)
+
+(defaxiom bad-atom<=-anti-symmetric
+ (implies (and (bad-atom x)
+ (bad-atom y)
+ (bad-atom<= x y)
+ (bad-atom<= y x))
+ (equal x y))
+ :rule-classes nil)
+
+(defaxiom bad-atom<=-transitive
+ (implies (and (bad-atom<= x y)
+ (bad-atom<= y z)
+ (bad-atom x)
+ (bad-atom y)
+ (bad-atom z))
+ (bad-atom<= x z)))
+
+(defaxiom bad-atom<=-total
+ (implies (and (bad-atom x)
+ (bad-atom y))
+ (or (bad-atom<= x y)
+ (bad-atom<= y x)))
+ :rule-classes nil)
+
+(defun atom-order (x y)
+ (cond ((rationalp x)
+ (if (rationalp y)
+ (<= x y)
+ t))
+ ((rationalp y) nil)
+ ((complex-rationalp x)
+ (if (complex-rationalp y)
+ (or (< (realpart x) (realpart y))
+ (and (= (realpart x) (realpart y))
+ (<= (imagpart x) (imagpart y))))
+ t))
+ ((complex-rationalp y)
+ nil)
+ ((characterp x)
+ (if (characterp y)
+ (<= (char-code x)
+ (char-code y))
+ t))
+ ((characterp y) nil)
+ ((stringp x)
+ (if (stringp y)
+ (and (string<= x y) t)
+ t))
+ ((stringp y) nil)
+ ((symbolp x)
+ (if (symbolp y)
+ (not (symbol-< y x))
+ t))
+ ((symbolp y) nil)
+ (t (bad-atom<= x y))))
+
+(local
+ (defthm bad-atom<=-reflexive
+ (implies (bad-atom x)
+ (bad-atom<= x x))
+ :hints (("Goal"
+ :by (:instance bad-atom<=-total (y x))))))
+
+(local
+ (defthm bad-atom<=-total-rewrite
+ (implies (and (not (bad-atom<= y x))
+ (bad-atom x)
+ (bad-atom y))
+ (bad-atom<= x y))
+ :hints (("Goal"
+ :by (:instance bad-atom<=-total)))
+ :rule-classes :forward-chaining))
+
+(local
+ (defthm equal-coerce
+ (implies (and (stringp x)
+ (stringp y))
+ (equal (equal (coerce x 'list)
+ (coerce y 'list))
+ (equal x y)))
+ :hints (("Goal" :use
+ ((:instance coerce-inverse-2 (x x))
+ (:instance coerce-inverse-2 (x y)))
+ :in-theory (disable coerce-inverse-2)))))
+
+(local
+ (defthm boolp-atom-order
+ (boolp (atom-order x y))
+ :rule-classes :type-prescription))
+
+(local
+ (defthm atom-order-reflexive
+ (implies (atom x)
+ (atom-order x x))))
+
+(local
+ (defthm string<=-l-transitive-at-0
+ (implies (and (not (string<-l y x 0))
+ (not (string<-l z y 0))
+ (character-listp x)
+ (character-listp y)
+ (character-listp z))
+ (not (string<-l z x 0)))
+ :hints
+ (("Goal" :use (:instance string<-l-transitive
+ (i 0) (j 0) (k 0))))))
+
+(local
+ (defthm atom-order-transitive
+ (implies (and (atom-order x y)
+ (atom-order y z)
+ (atom x)
+ (atom y)
+ (atom z))
+ (atom-order x z))
+ :hints (("Goal"
+ :in-theory (enable string< symbol-<)))))
+
+(local
+ (defthm atom-order-anti-symmetric
+ (implies (and (atom x)
+ (atom y)
+ (atom-order x y)
+ (atom-order y x))
+ (equal x y))
+ :hints (("Goal"
+ :in-theory (union-theories
+ '(string< symbol-<)
+ (disable code-char-char-code-is-identity))
+ :use ((:instance symbol-equality (s1 x) (s2 y))
+ (:instance bad-atom<=-anti-symmetric)
+ (:instance code-char-char-code-is-identity (c y))
+ (:instance code-char-char-code-is-identity (c x)))))
+ :rule-classes
+ ((:forward-chaining :corollary
+ (implies (and (atom-order x y)
+ (not (consp x))
+ (not (consp y)))
+ (iff (atom-order y x)
+ (equal x y)))
+ :hints (("Goal" :in-theory
+ (disable atom-order)))))))
+
+(local
+ (defthm atom-order-total
+ (implies (and (atom x)
+ (atom y))
+ (or (atom-order x y)
+ (atom-order y x)))
+ :hints (("Goal" :use (:instance bad-atom<=-total)
+ :in-theory (enable string< symbol-<)))
+ :rule-classes
+ ((:forward-chaining :corollary
+ (implies (and (not (atom-order x y))
+ (not (consp x))
+ (not (consp y)))
+ (atom-order y x))))))
+
+(in-theory (disable atom-order))
+
+(defun total-order (x y)
+ (cond ((atom x)
+ (cond ((atom y)
+ (atom-order x y))
+ (t t)))
+ ((atom y) nil)
+ ((equal (car x) (car y))
+ (total-order (cdr x) (cdr y)))
+ (t (total-order (car x) (car y)))))
+
+(defthm boolp-total-order
+ (boolp (total-order x y))
+ :rule-classes :type-prescription)
+
+(defthm total-order-reflexive
+ (total-order x x))
+
+(defthm total-order-anti-symmetric
+ (implies (and (total-order x y)
+ (total-order y x))
+ (equal x y))
+ :rule-classes :forward-chaining)
+
+(defthm total-order-transitive
+ (implies (and (total-order x y)
+ (total-order y z))
+ (total-order x z)))
+
+(defthm total-order-total
+ (or (total-order x y)
+ (total-order y x))
+ :rule-classes nil)