Event: Start with the initial nqthm theory.

;; Sets; Matt Kaufmann, Dec. 1989, revised March 1990.  The first few events
;; are some basic events about lists.  I'll take the approach that all these
;; basic functions will be disabled once enough algebraic properties have
;; been proved.
;; Theories:
;; (deftheory set-defns
;;  (length properp fix-properp member append subsetp delete
;;          disjoint intersection set-diff setp))

Definition: length (x) = if listp (x) then 1 + length (cdr (x))

else 0 endif

Theorem: length-nlistp (x ≃ nil) → (length (x) = 0)

Theorem: length-cons length (cons (a, x)) = (1 + length (x))

Theorem: length-append length (append (x, y)) = (length (x) + length (y))

Event: Disable length.

Theorem: append-assoc append (append (x, y), z) = append (x, append (y, z))

Theorem: member-cons (a ∈ cons (x, l)) = ((a = x) ∨ (a ∈ l))

Theorem: member-nlistp (l ≃ nil) → (a ∉ l)

Event: Disable member.

Definition: subsetp (x, y) = if x ≃ nil then t

else (car (x) ∈ y) ∧ subsetp (cdr (x), y) endif Definition: subsetp-wit (x, y) = if x ≃ nil then t

elseif car (x) ∈ y then subsetp-wit (cdr (x), y)

else car (x) endif

Theorem: subsetp-wit-witnesses subsetp (x, y) = (¬ ((subsetp-wit (x, y) ∈ x) ∧ (subsetp-wit (x, y) ∉ y)))

Theorem: subsetp-wit-witnesses-general-1 ((subsetp-wit (x, y) ∉ x) ∧ (a ∈ x)) → (a ∈ y)

Theorem: subsetp-wit-witnesses-general-2 ((subsetp-wit (x, y) ∈ y) ∧ (a ∈ x)) → (a ∈ y)

Event: Disable subsetp-wit-witnesses.

Event: Disable subsetp-wit-witnesses-general-1.

Event: Disable subsetp-wit-witnesses-general-2.

Theorem: subsetp-cons-1 subsetp (cons (a, x), y) = ((a ∈ y) ∧ subsetp (x, y))

Theorem: subsetp-cons-2 subsetp (l, m) → subsetp (l, cons (a, m))

Theorem: subsetp-reflexivity subsetp (x, x)

Theorem: cdr-subsetp subsetp (cdr (x), x)

Theorem: member-subsetp ((x ∈ y) ∧ subsetp (y, z)) → (x ∈ z)

Theorem: subsetp-is-transitive (subsetp (x, y) ∧ subsetp (y, z)) → subsetp (x, z)

Theorem: member-append (a ∈ append (x, y)) = ((a ∈ x) ∨ (a ∈ y))

Theorem: subsetp-append subsetp (append (x, y), z) = (subsetp (x, z) ∧ subsetp (y, z))

Theorem: subsetp-of-append-sufficiency (subsetp (a, b) ∨ subsetp (a, c)) → subsetp (a, append (b, c))

Theorem: subsetp-nlistp (x ≃ nil) → (subsetp (x, y) ∧ (subsetp (y, x) = (y ≃ nil)))

Theorem: subsetp-cons-not-member (z ∉ x) → (subsetp (x, cons (z, v)) = subsetp (x, v))

Event: Disable subsetp.

;;;;; Other set-theoretic and list-theoretic definitions, and properp observations.

Definition: properp (x) = if listp (x) then properp (cdr (x))

else x = nil endif

Definition: fix-properp (x) = if listp (x) then cons (car (x), fix-properp (cdr (x)))

else nil endif

Theorem: properp-fix-properp properp (fix-properp (x))

Theorem: fix-properp-properp properp (x) → (fix-properp (x) = x)

Theorem: properp-cons properp (cons (x, y)) = properp (y)

Theorem: properp-nlistp (x ≃ nil) → (properp (x) = (x = nil))

Theorem: fix-properp-cons fix-properp (cons (x, y)) = cons (x, fix-properp (y))

Theorem: fix-properp-nlistp (x ≃ nil) → (fix-properp (x) = nil)

Theorem: properp-append properp (append (x, y)) = properp (y)

Theorem: fix-properp-append fix-properp (append (x, y)) = append (x, fix-properp (y))

Theorem: append-nil append (x, nil) = fix-properp (x)

Definition: delete (x, l) = if listp (l)

then if x = car (l) then cdr (l)

else cons (car (l), delete (x, cdr (l))) endif else l endif

Theorem: properp-delete properp (delete (x, l)) = properp (l)

Definition: disjoint (x, y) = if listp (x) then (car (x) ∉ y) ∧ disjoint (cdr (x), y)

else t endif

Definition: disjoint-wit (x, y) = if listp (x)

then if car (x) ∈ y then car (x)

else disjoint-wit (cdr (x), y) endif else t endif

Theorem: disjoint-wit-witnesses disjoint (x, y) = (¬ ((disjoint-wit (x, y) ∈ x) ∧ (disjoint-wit (x, y) ∈ y)))

Event: Disable disjoint-wit.

Event: Disable disjoint-wit-witnesses.

Definition: intersection (x, y) = if listp (x)

then if car (x) ∈ y then cons (car (x), intersection (cdr (x), y))

else intersection (cdr (x), y) endif else nil endif

Theorem: properp-intersection properp (intersection (x, y))

Definition: set-diff (x, y) = if listp (x)

then if car (x) ∈ y then set-diff (cdr (x), y)

else cons (car (x), set-diff (cdr (x), y)) endif else nil endif

Theorem: properp-set-diff properp (set-diff (x, y))

Definition: setp (x) = if ¬ listp (x) then x = nil

else (car (x) ∉ cdr (x)) ∧ setp (cdr (x)) endif

Theorem: setp-implies-properp setp (x) → properp (x)

Event: Disable properp.

Event: Let us define the theory set-defns to consist of the following events: length, properp, fix-properp, member, append, subsetp, delete, disjoint, intersection, set-diff, setp, properp.

;; Set theory lemmas

Theorem: delete-cons delete (a, cons (b, x)) = if a = b then x

else cons (b, delete (a, x)) endif

Theorem: delete-nlistp (x ≃ nil) → (delete (a, x) = x)

Theorem: listp-delete listp (delete (x, l)) = if listp (l) then (x ≠ car (l)) ∨ listp (cdr (l))

else f endif

Theorem: delete-non-member (x ∉ y) → (delete (x, y) = y)

Theorem: delete-delete delete (y, delete (x, z)) = delete (x, delete (y, z))

Theorem: member-delete setp (x) → ((a ∈ delete (b, x)) = ((a ≠ b) ∧ (a ∈ x)))

Theorem: setp-delete setp (x) → setp (delete (a, x))

Event: Disable delete.

Theorem: disjoint-cons-1 disjoint (cons (a, x), y) = ((a ∉ y) ∧ disjoint (x, y))

Theorem: disjoint-cons-2 disjoint (x, cons (a, y)) = ((a ∉ x) ∧ disjoint (x, y))

Theorem: disjoint-nlistp ((x ≃ nil) ∨ (y ≃ nil)) → disjoint (x, y)

Theorem: disjoint-symmetry disjoint (x, y) = disjoint (y, x)

Theorem: disjoint-append-right disjoint (u, append (y, z)) = (disjoint (u, y) ∧ disjoint (u, z))

Theorem: disjoint-append-left disjoint (append (y, z), u) = (disjoint (y, u) ∧ disjoint (z, u))

Theorem: disjoint-non-member ((a ∈ x) ∧ (a ∈ y)) → (¬ disjoint (x, y))

Theorem: disjoint-subsetp-monotone-second (subsetp (y, z) ∧ disjoint (x, z)) → disjoint (x, y)

Theorem: subsetp-disjoint-2 (subsetp (x, y) ∧ disjoint (y, z)) → disjoint (z, x)

Theorem: subsetp-disjoint-1 (subsetp (x, y) ∧ disjoint (y, z)) → disjoint (x, z)

Theorem: subsetp-disjoint-3 (subsetp (x, y) ∧ disjoint (z, y)) → disjoint (x, z)

Event: Disable disjoint.

Theorem: intersection-disjoint (intersection (x, y) = nil) = disjoint (x, y)

Theorem: intersection-nlistp ((x ≃ nil) ∨ (y ≃ nil)) → (intersection (x, y) = nil)

Theorem: member-intersection (a ∈ intersection (x, y)) = ((a ∈ x) ∧ (a ∈ y))

Theorem: subsetp-intersection subsetp (x, intersection (y, z)) = (subsetp (x, y) ∧ subsetp (x, z))

Theorem: intersection-symmetry subsetp (intersection (x, y), intersection (y, x))

Theorem: intersection-cons-1 intersection (cons (a, x), y) = if a ∈ y then cons (a, intersection (x, y))

else intersection (x, y) endif

Theorem: intersection-cons-2 (a ∉ y) → (intersection (y, cons (a, x)) = intersection (y, x))

;; The following is needed because DISJOINT-INTERSECTION-COMMUTER,
;; added during polishing, caused the proof of
;; DISJOINT-DOMAIN-CO-RESTRICT (in "alists.events") to fail.

Theorem: intersection-cons-3 (w ∈ x) → (subsetp (intersection (y, cons (w, z)), x)

= subsetp (intersection (y, z), x))

Theorem: intersection-cons-subsetp subsetp (intersection (x, y), intersection (x, cons (a, y)))

Theorem: subsetp-intersection-left-1 subsetp (intersection (x, y), x)

Theorem: subsetp-intersection-left-2 subsetp (intersection (x, y), y)

Theorem: subsetp-intersection-sufficiency-1 subsetp (y, z) → subsetp (intersection (x, y), z)

Theorem: subsetp-intersection-sufficiency-2 subsetp (y, z) → subsetp (intersection (y, x), z)

Theorem: intersection-associative intersection (intersection (x, y), z) = intersection (x, intersection (y, z))

Theorem: intersection-elimination subsetp (x, y) → (intersection (x, y) = fix-properp (x))

Theorem: length-intersection length (x) ≮ length (intersection (x, y))

Theorem: subsetp-intersection-member (subsetp (intersection (x, y), z) ∧ (a ∉ z)) → (((a ∈ x) → (a ∉ y)) ∧ ((a ∈ y) → (a ∉ x)))

;; The following wasn't needed in the proof about generalization, but it's a nice rule.

Theorem: intersection-append intersection (append (x, y), z) = append (intersection (x, z), intersection (y, z))

;; I'd rather just prove that intersection distributes over append on
;; the right but that isn't true.  Congruence relations would probably
;; help a lot with that problem.  In the meantime, I content myself
;; with the following.

Theorem: disjoint-intersection-append disjoint (x, intersection (y, append (z1 , z2 ))) = (disjoint (x, intersection (y, z1 )) ∧ disjoint (x, intersection (y, z2 )))

;; See comment just above DISJOINT-INTERSECTION-APPEND

Theorem: subsetp-intersection-append subsetp (intersection (u, append (x, y)), z) = (subsetp (intersection (u, x), z) ∧ subsetp (intersection (u, y), z))

Theorem: subsetp-intersection-elimination-lemma (subsetp (y, x) ∧ (¬ subsetp (y, z))) → (¬ subsetp (intersection (x, y), z))

Theorem: subsetp-intersection-elimination subsetp (y, x) → (subsetp (intersection (x, y), z) ↔ subsetp (y, z))

Theorem: disjoint-intersection disjoint (intersection (x, y), z) = disjoint (x, intersection (y, z))

Theorem: subsetp-intersection-monotone-1 (subsetp (intersection (x, y), z) ∧ subsetp (x1 , x)) → subsetp (intersection (x1 , y), z)

;; The lemma SUBSETP-INTERSECTION-MONOTONE-2 below was added during
;; polishing of the final proof in "generalize.events", since the
;; lemma immediately above wasn't enough at that point.  Actually
;; I realized at this point that intersection commutes from the point
;; of view of subsetp:

Theorem: subsetp-intersection-commuter subsetp (intersection (x, y), z) = subsetp (intersection (y, x), z)

Theorem: subsetp-intersection-monotone-2 (subsetp (intersection (y, x), z) ∧ subsetp (x1 , x)) → subsetp (intersection (x1 , y), z)

Theorem: disjoint-intersection-commuter disjoint (x, intersection (y, z)) = disjoint (x, intersection (z, y))

Theorem: disjoint-intersection3 disjoint (free, intersection (vars, x)) → (intersection (x, intersection (vars, free)) = nil)

Event: Disable intersection.

Theorem: member-set-diff (a ∈ set-diff (y, z)) = ((a ∈ y) ∧ (a ∉ z))

Theorem: subsetp-set-diff-1 subsetp (set-diff (x, y), x)

Theorem: disjointp-set-diff disjoint (set-diff (x, y), y)

Theorem: subsetp-set-diff-2 subsetp (x, set-diff (y, z)) = (subsetp (x, y) ∧ disjoint (x, z))

Theorem: set-diff-cons set-diff (cons (a, x), y) = if a ∈ y then set-diff (x, y)

else cons (a, set-diff (x, y)) endif

Theorem: set-diff-nlistp (x ≃ nil) → (set-diff (x, y) = nil)

;; The following was discovered during final polishing, for the
;; proof of MAIN-HYPS-RELIEVED-6-FIRST.

Theorem: disjoint-set-diff-general disjoint (x, set-diff (y, z)) = subsetp (intersection (x, y), z)

;; No longer relevant:
;(prove-lemma disjoint-set-diff-subsetp (rewrite)
;  (implies (and (disjoint x (set-diff y z))
; (subsetp z z1))
;    (disjoint x (set-diff y z1)))
;  ((use (disjoint-wit-witnesses (y (set-diff y z1))))
;   (disable member-set-diff set-diff)))
;; Instead of the following I'll prove the corresponding (in light of
;; DISJOINT-SET-DIFF-GENERAL) fact INTERSECTION-X-X about intersection.
;(prove-lemma disjoint-set-diff (rewrite)
;  (disjoint x (set-diff y x)))

Theorem: intersection-subsetp-identity (properp (x) ∧ subsetp (x, y)) → (intersection (x, y) = x)

Theorem: intersection-x-x properp (x) → (intersection (x, x) = x)

Theorem: subsetp-set-diff-mononone-2 subsetp (set-diff (x, append (y, z)), set-diff (x, z))

Theorem: subsetp-set-diff-monotone-second subsetp (set-diff (x, y), set-diff (x, z)) = subsetp (intersection (x, z), y)

Theorem: set-diff-nil set-diff (x, nil) = fix-properp (x)

Theorem: set-diff-cons-non-member-1 (a ∉ x) → (set-diff (x, cons (a, y)) = set-diff (x, y))

Theorem: length-intersection-set-diff length (x) = (length (set-diff (x, y)) + length (intersection (x, y)))

Theorem: length-set-diff-opener length (set-diff (x, y)) = (length (x) − length (intersection (x, y)))

Theorem: listp-set-diff listp (set-diff (x, y)) = (¬ subsetp (x, y))

;; Here is a messy lemma about disjoint and such

Theorem: disjoint-intersection-set-diff-intersection disjoint (x, intersection (y, set-diff (z, intersection (y, x))))

Event: Disable set-diff.

Theorem: member-fix-properp (a ∈ fix-properp (x)) = (a ∈ x)

Theorem: setp-append setp (append (x, y)) = (disjoint (x, y) ∧ setp (fix-properp (x)) ∧ setp (y))

Theorem: setp-cons setp (cons (a, x)) = ((a ∉ x) ∧ setp (x))

Theorem: setp-nlistp (x ≃ nil) → (setp (x) = (x = nil))

Definition: make-set (l) = if ¬ listp (l) then nil

elseif car (l) ∈ cdr (l) then make-set (cdr (l)) else cons (car (l), make-set (cdr (l))) endif

Theorem: make-set-preserves-member (x ∈ make-set (l)) = (x ∈ l)

Theorem: make-set-preserves-subsetp-1 subsetp (make-set (x), make-set (y)) = subsetp (x, y)

Theorem: make-set-preserves-subsetp-2 subsetp (x, make-set (y)) = subsetp (x, y)

Theorem: make-set-preserves-subsetp-3 subsetp (make-set (x), y) = subsetp (x, y)

Theorem: make-set-gives-setp setp (make-set (x))

Theorem: make-set-set-diff make-set (set-diff (x, y)) = set-diff (make-set (x), make-set (y))

Theorem: set-diff-make-set set-diff (x, make-set (y)) = set-diff (x, y)

Theorem: listp-make-set listp (make-set (x)) = listp (x)

Event: Disable setp.

;;;;;; The following were proved in the course of the final run
;;;;;; through the generalization proof.  There are a couple or
;;;;;; so noted above here, too.

Theorem: set-diff-append set-diff (x, append (y, z)) = set-diff (set-diff (x, z), y)

Theorem: length-set-diff-leq length (x) ≮ length (set-diff (x, y))

Theorem: lessp-length listp (x) → (0 < length (x))

Theorem: listp-intersection listp (intersection (x, y)) = (¬ disjoint (x, y))

Theorem: length-set-diff-lessp (¬ disjoint (x, new)) → (length (set-diff (x, new)) < length (x))

Theorem: disjoint-implies-empty-intersection disjoint (x, y) → (intersection (x, y) = nil)

;; The following lemma DISJOINT-INTERSECTION3-MIDDLE is needed for the
;; proof of ALL-VARS-DISJOINT-OR-SUBSETP-GEN-CLOSURE in
;; generalize.events.  I think I could avoid lemmas like this one
;; INTERSECTION were actually commutative-associative (in which case
;; I'd get rid of disjoint and rely on normalization).

Theorem: disjoint-intersection3-middle disjoint (y, intersection (x, z)) → (intersection (x, intersection (y, z)) = nil)

;; Maybe I should redo the notion of disjoint sometime, perhaps using
;; the fact that intersection is commutative and associative when it's
;; equated with nil.

Theorem: disjoint-subsetp-hack (disjoint (x, intersection (u, v)) ∧ subsetp (w, x)) → disjoint (u, intersection (w, v))

Theorem: subsetp-set-diff-sufficiency subsetp (x, y) → subsetp (set-diff (x, z), y)

;; The following lemma SETP-INTERSECTION-SUFFICIENCY is needed for
;; MAPPING-RESTRICT from "alists.events", because (I believe)
;; DOMAIN-RESTRICT, which was added during polishing, changed the
;; course of the previous proof.  Similarly for
;; SETP-SET-DIFF-SUFFICIENCY and the lemma MAPPING-CO-RESTRICT.

Theorem: setp-intersection-sufficiency setp (x) → setp (intersection (x, y))

Theorem: setp-set-diff-sufficiency setp (x) → setp (set-diff (x, y))

;; The definition of FIX-PROPERP was also added in polishing because
;; of a problem with the proof of GEN-CLOSURE-ACCEPT in
;; "generalize.events".  Here are a couple of lemmas about it that
;; might or might not be useful; all other lemmas about it above, and
;; the definition, were added during polishing.

Event: Disable fix-properp.

Theorem: subsetp-fix-properp-1 subsetp (fix-properp (x), y) = subsetp (x, y)

Theorem: subsetp-fix-properp-2 subsetp (x, fix-properp (y)) = subsetp (x, y)

Event: Make the library "sets".

Index

append-assoc, 1 append-nil, 4

cdr-subsetp, 2

delete, 4–6 delete-cons, 5 delete-delete, 5 delete-nlistp, 5 delete-non-member, 5 disjoint, 4, 6, 8–12 disjoint-append-left, 6 disjoint-append-right, 6 disjoint-cons-1, 6 disjoint-cons-2, 6 disjoint-implies-empty-intersecti

on, 12 disjoint-intersection, 8 disjoint-intersection-append, 8 disjoint-intersection-commuter, 9 disjoint-intersection-set-diff-i

ntersection, 11 disjoint-intersection3, 9 disjoint-intersection3-middle, 12 disjoint-nlistp, 6 disjoint-non-member, 6 disjoint-set-diff-general, 10 disjoint-subsetp-hack, 12 disjoint-subsetp-monotone-secon

d, 6 disjoint-symmetry, 6 disjoint-wit, 4 disjoint-wit-witnesses, 4 disjointp-set-diff, 9

fix-properp, 3, 4, 8, 10, 11, 13 fix-properp-append, 3 fix-properp-cons, 3 fix-properp-nlistp, 3 fix-properp-properp, 3

intersection, 4, 6–13 intersection-append, 8 intersection-associative, 7 intersection-cons-1, 7 intersection-cons-2, 7 intersection-cons-3, 7 intersection-cons-subsetp, 7 intersection-disjoint, 6 intersection-elimination, 8 intersection-nlistp, 7 intersection-subsetp-identity, 10 intersection-symmetry, 7 intersection-x-x, 10

length, 1, 8, 10, 12 length-append, 1 length-cons, 1 length-intersection, 8 length-intersection-set-diff, 10 length-nlistp, 1 length-set-diff-leq, 12 length-set-diff-lessp, 12 length-set-diff-opener, 10 lessp-length, 12 listp-delete, 5 listp-intersection, 12 listp-make-set, 11 listp-set-diff, 10

make-set, 11 make-set-gives-setp, 11 make-set-preserves-member, 11 make-set-preserves-subsetp-1, 11 make-set-preserves-subsetp-2, 11 make-set-preserves-subsetp-3, 11 make-set-set-diff, 11 member-append, 2 member-cons, 1 member-delete, 6 member-fix-properp, 11 member-intersection, 7 member-nlistp, 1 member-set-diff, 9 member-subsetp, 2

properp, 3–5, 10 properp-append, 3 properp-cons, 3 properp-delete, 4 properp-fix-properp, 3 properp-intersection, 4 properp-nlistp, 3 properp-set-diff, 5

set-defns, 5 set-diff, 5, 9–13 set-diff-append, 12 set-diff-cons, 9 set-diff-cons-non-member-1, 10 set-diff-make-set, 11 set-diff-nil, 10 set-diff-nlistp, 9 setp, 5, 6, 11, 13 setp-append, 11 setp-cons, 11 setp-delete, 6 setp-implies-properp, 5 setp-intersection-sufficiency, 13 setp-nlistp, 11 setp-set-diff-sufficiency, 13 subsetp, 1–3, 6–13 subsetp-append, 2 subsetp-cons-1, 2 subsetp-cons-2, 2 subsetp-cons-not-member, 3 subsetp-disjoint-1, 6 subsetp-disjoint-2, 6 subsetp-disjoint-3, 6 subsetp-fix-properp-1, 13 subsetp-fix-properp-2, 13 subsetp-intersection, 7 subsetp-intersection-append, 8 subsetp-intersection-commuter, 9 subsetp-intersection-eliminatio

n, 8

n-lemma, 8 subsetp-intersection-left-1, 7 subsetp-intersection-left-2, 7 subsetp-intersection-member, 8 subsetp-intersection-monotone-1, 8 subsetp-intersection-monotone-2, 9 subsetp-intersection-sufficienc

y-1, 7 y-2, 7

subsetp-is-transitive, 2

subsetp-nlistp, 3

subsetp-of-append-sufficiency, 3 subsetp-reflexivity, 2 subsetp-set-diff-1, 9 subsetp-set-diff-2, 9 subsetp-set-diff-mononone-2, 10 subsetp-set-diff-monotone-secon

d, 10 subsetp-set-diff-sufficiency, 13 subsetp-wit, 2 subsetp-wit-witnesses, 2 subsetp-wit-witnesses-general-1, 2 subsetp-wit-witnesses-general-2, 2