		Search-engine friendly clone of the ACL2 documentation.

Library-extensions

Oset-theorems

Some theorems about osets.

Among other theorems, we introduce an alternative pick-a-point reasoning support for subset. Unlike pick-a-point-subset-strategy, this uses a defun-sk and a ruleset.

Definitions and Theorems

Theorem: not-emptyp-when-in-of-subset

(defthm set::not-emptyp-when-in-of-subset
  (implies (and (in a x) (subset x y))
           (not (emptyp y))))

Theorem: subset-of-union-when-both-subset

(defthm set::subset-of-union-when-both-subset
  (implies (and (subset a s) (subset b s))
           (subset (union a b) s)))

Theorem: cardinality-of-union-upper-bound-when-both-subset

(defthm set::cardinality-of-union-upper-bound-when-both-subset
  (implies (and (subset a s) (subset b s))
           (<= (cardinality (union a b))
               (cardinality s)))
  :rule-classes (:rewrite :linear))

Theorem: intersect-of-insert-left

(defthm set::intersect-of-insert-left
  (equal (intersect (insert a x) y)
         (if (in a y)
             (insert a (intersect x y))
           (intersect x y))))

Theorem: intersect-of-insert-right

(defthm set::intersect-of-insert-right
  (equal (intersect x (insert a y))
         (if (in a x)
             (insert a (intersect x y))
           (intersect x y))))

Theorem: same-element-when-cardinality-leq-1

(defthm set::same-element-when-cardinality-leq-1
  (implies (and (<= (cardinality set) 1)
                (in elem1 set)
                (in elem2 set))
           (equal elem1 elem2))
  :rule-classes nil)

Theorem: cardinality-of-tail-leq

(defthm set::cardinality-of-tail-leq
  (<= (cardinality (tail set))
      (cardinality set))
  :rule-classes :linear)

Theorem: head-of-intersect-member-when-not-emptyp

(defthm set::head-of-intersect-member-when-not-emptyp
  (implies (not (emptyp (intersect x y)))
           (and (in (head (intersect x y)) x)
                (in (head (intersect x y)) y))))

Theorem: emptyp-when-proper-subset-of-singleton

(defthm set::emptyp-when-proper-subset-of-singleton
  (implies (and (subset x (insert a nil))
                (not (equal x (insert a nil))))
           (emptyp x)))

Theorem: intersect-mono-subset

(defthm set::intersect-mono-subset
  (implies (subset a b)
           (subset (intersect a c)
                   (intersect b c))))

Theorem: emptyp-to-subset-of-nil

(defthm set::emptyp-to-subset-of-nil
  (equal (emptyp a) (subset a nil)))

Theorem: not-member-when-member-of-disjoint

(defthm set::not-member-when-member-of-disjoint
  (implies (and (not (intersect a b)) (in x a))
           (not (in x b))))

Theorem: emptyp-of-intersect-of-subset-left

(defthm set::emptyp-of-intersect-of-subset-left
  (implies (and (subset a b)
                (emptyp (intersect b c)))
           (emptyp (intersect a c))))

Theorem: subset-of-intersect-if-subset-of-both

(defthm set::subset-of-intersect-if-subset-of-both
  (implies (and (subset a b) (subset a c))
           (subset a (intersect b c))))

Theorem: subset-of-tail-and-delete-when-subset

(defthm set::subset-of-tail-and-delete-when-subset
  (implies (and (not (emptyp x)) (subset x y))
           (subset (tail x) (delete (head x) y))))

Theorem: subset-of-difference-when-disjoint

(defthm set::subset-of-difference-when-disjoint
  (implies (and (subset x y)
                (emptyp (intersect x z)))
           (subset x (difference y z))))

Theorem: not-emptyp-of-intersect-when-in-both

(defthm set::not-emptyp-of-intersect-when-in-both
  (implies (and (in a x) (in a y))
           (not (emptyp (intersect x y)))))

Theorem: subset-sk-necc

(defthm set::subset-sk-necc
  (implies (set::subset-sk set1 set2)
           (implies (in elem set1)
                    (in elem set2))))

Theorem: booleanp-of-subset-sk

(defthm set::booleanp-of-subset-sk
  (b* ((bool (set::subset-sk set1 set2)))
    (booleanp bool))
  :rule-classes :type-prescription)

Theorem: subset-sk-of-tail-when-subset-sk

(defthm set::subset-sk-of-tail-when-subset-sk
  (implies (set::subset-sk set1 set2)
           (set::subset-sk (tail set1) set2)))

Theorem: subset-sk-when-subset

(defthm set::subset-sk-when-subset
  (implies (subset set1 set2)
           (set::subset-sk set1 set2)))

Theorem: subset-when-subset-sk

(defthm set::subset-when-subset-sk
  (implies (set::subset-sk set1 set2)
           (subset set1 set2)))

Theorem: subset-to-subset-sk

(defthm set::subset-to-subset-sk
  (equal (subset set1 set2)
         (set::subset-sk set1 set2)))