		Search-engine friendly clone of the ACL2 documentation.

Object-designators

Object-disjointp

Check if two designated objects are disjoint.

Signature
(object-disjointp objdes1 objdes2) → yes/no
Arguments: objdes1 — Guard (objdesignp objdes1).; objdes2 — Guard (objdesignp objdes2).
Returns: yes/no — Type (booleanp yes/no).

This has to be a sufficient condition for disjointness, but not necessarily a necessary condition; that is, it can be a conservative definition, because it is only used to express when object updates are independent. For now, we require the two object designators to be top-level designators in allocated storage and to be distinct. We may relax this notion in the future, but for now this suffices for our needs.

Definitions and Theorems

Function: object-disjointp

(defun object-disjointp (objdes1 objdes2)
  (declare (xargs :guard (and (objdesignp objdes1)
                              (objdesignp objdes2))))
  (let ((__function__ 'object-disjointp))
    (declare (ignorable __function__))
    (and (objdesign-case objdes1 :alloc)
         (objdesign-case objdes2 :alloc)
         (not (equal (objdesign-alloc->get objdes1)
                     (objdesign-alloc->get objdes2))))))

Theorem: booleanp-of-object-disjointp

(defthm booleanp-of-object-disjointp
  (b* ((yes/no (object-disjointp objdes1 objdes2)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: object-disjointp-commutative

(defthm object-disjointp-commutative
  (equal (object-disjointp x y)
         (object-disjointp y x)))

Theorem: object-disjointp-of-objdesign-fix-objdes1

(defthm object-disjointp-of-objdesign-fix-objdes1
  (equal (object-disjointp (objdesign-fix objdes1)
                           objdes2)
         (object-disjointp objdes1 objdes2)))

Theorem: object-disjointp-objdesign-equiv-congruence-on-objdes1

(defthm object-disjointp-objdesign-equiv-congruence-on-objdes1
  (implies (objdesign-equiv objdes1 objdes1-equiv)
           (equal (object-disjointp objdes1 objdes2)
                  (object-disjointp objdes1-equiv objdes2)))
  :rule-classes :congruence)

Theorem: object-disjointp-of-objdesign-fix-objdes2

(defthm object-disjointp-of-objdesign-fix-objdes2
  (equal (object-disjointp objdes1 (objdesign-fix objdes2))
         (object-disjointp objdes1 objdes2)))

Theorem: object-disjointp-objdesign-equiv-congruence-on-objdes2

(defthm object-disjointp-objdesign-equiv-congruence-on-objdes2
  (implies (objdesign-equiv objdes2 objdes2-equiv)
           (equal (object-disjointp objdes1 objdes2)
                  (object-disjointp objdes1 objdes2-equiv)))
  :rule-classes :congruence)