		Search-engine friendly clone of the ACL2 documentation.

Atj-types

Atj-type-top-join

Least upper bound of two ATJ types or nils, with respect to the partial order atj-type-top-<=.

Signature
(atj-type-top-join x y) → lub
Arguments: x — Guard (atj-maybe-typep x).; y — Guard (atj-maybe-typep y).
Returns: lub — Type (atj-maybe-typep lub).

As discussed in atj-type-top-<=, the addition of nil as top element of the partial order results in a join semilattice.

We define this operation by five cases: the first two are obvious, while the remaining three are motivated by the fact that :acons, :avalue, and nil are the only elements that have more than one element that is strictly smaller.

To validate this definition of least upper bound, we prove that the this operation indeed returns an upper bound that is less than or equal to any other upper bound, i.e. that it returns the least upper bound.

The commutativity, idempotence, and associativity of the join operation follows from these and the partial order properties, according to lattice theory. So we do not prove these properties explicitly here.

Definitions and Theorems

Function: atj-type-top-join

(defun atj-type-top-join (x y)
 (declare (xargs :guard (and (atj-maybe-typep x)
                             (atj-maybe-typep y))))
 (let ((__function__ 'atj-type-top-join))
  (declare (ignorable __function__))
  (cond ((atj-type-top-<= x y)
         (atj-maybe-type-fix y))
        ((atj-type-top-<= y x)
         (atj-maybe-type-fix x))
        ((and (atj-type-top-<= x (atj-type-acl2 (atj-atype-cons)))
              (atj-type-top-<= y (atj-type-acl2 (atj-atype-cons))))
         (atj-type-acl2 (atj-atype-cons)))
        ((and (atj-type-top-<= x (atj-type-acl2 (atj-atype-value)))
              (atj-type-top-<= y (atj-type-acl2 (atj-atype-value))))
         (atj-type-acl2 (atj-atype-value)))
        (t nil))))

Theorem: atj-maybe-typep-of-atj-type-top-join

(defthm atj-maybe-typep-of-atj-type-top-join
  (b* ((lub (atj-type-top-join x y)))
    (atj-maybe-typep lub))
  :rule-classes :rewrite)

Theorem: atj-type-top-join-upper-bound-left

(defthm atj-type-top-join-upper-bound-left
  (atj-type-top-<= x (atj-type-top-join x y)))

Theorem: atj-type-top-join-upper-bound-right

(defthm atj-type-top-join-upper-bound-right
  (atj-type-top-<= y (atj-type-top-join x y)))

Theorem: atj-type-top-join-least

(defthm atj-type-top-join-least
  (implies (and (atj-type-top-<= x z)
                (atj-type-top-<= y z))
           (atj-type-top-<= (atj-type-top-join x y)
                            z)))

Theorem: atj-type-top-join-of-atj-maybe-type-fix-x

(defthm atj-type-top-join-of-atj-maybe-type-fix-x
  (equal (atj-type-top-join (atj-maybe-type-fix x)
                            y)
         (atj-type-top-join x y)))

Theorem: atj-type-top-join-atj-maybe-type-equiv-congruence-on-x

(defthm atj-type-top-join-atj-maybe-type-equiv-congruence-on-x
  (implies (atj-maybe-type-equiv x x-equiv)
           (equal (atj-type-top-join x y)
                  (atj-type-top-join x-equiv y)))
  :rule-classes :congruence)

Theorem: atj-type-top-join-of-atj-maybe-type-fix-y

(defthm atj-type-top-join-of-atj-maybe-type-fix-y
  (equal (atj-type-top-join x (atj-maybe-type-fix y))
         (atj-type-top-join x y)))

Theorem: atj-type-top-join-atj-maybe-type-equiv-congruence-on-y

(defthm atj-type-top-join-atj-maybe-type-equiv-congruence-on-y
  (implies (atj-maybe-type-equiv y y-equiv)
           (equal (atj-type-top-join x y)
                  (atj-type-top-join x y-equiv)))
  :rule-classes :congruence)