		Search-engine friendly clone of the ACL2 documentation.

Atj-types

Atj-type-bottom-meet

Greatest lower bound of two ATJ types or nils, with respect to the partial order atj-type-bottom-<=.

Signature
(atj-type-bottom-meet x y) → glb
Arguments: x — Guard (atj-maybe-typep x).; y — Guard (atj-maybe-typep y).
Returns: glb — Type (atj-maybe-typep glb).

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

We define this operation by three cases: the first two are obvious, and the third one suffices because no element of the semilattice has more than one elements that are strictly larger.

To validate this definition of greatest lower bound, we prove that the this operation indeed returns a lower bound that is greater than or equal to any other lower bound, i.e. that it returns the greatest lower 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-bottom-meet

(defun atj-type-bottom-meet (x y)
  (declare (xargs :guard (and (atj-maybe-typep x)
                              (atj-maybe-typep y))))
  (let ((__function__ 'atj-type-bottom-meet))
    (declare (ignorable __function__))
    (cond ((atj-type-bottom-<= x y)
           (atj-maybe-type-fix x))
          ((atj-type-bottom-<= y x)
           (atj-maybe-type-fix y))
          (t nil))))

Theorem: atj-maybe-typep-of-atj-type-bottom-meet

(defthm atj-maybe-typep-of-atj-type-bottom-meet
  (b* ((glb (atj-type-bottom-meet x y)))
    (atj-maybe-typep glb))
  :rule-classes :rewrite)

Theorem: atj-type-bottom-meet-lower-bound-left

(defthm atj-type-bottom-meet-lower-bound-left
  (atj-type-bottom-<= (atj-type-bottom-meet x y)
                      x))

Theorem: atj-type-bottom-meet-lower-bound-right

(defthm atj-type-bottom-meet-lower-bound-right
  (atj-type-bottom-<= (atj-type-bottom-meet x y)
                      y))

Theorem: atj-type-bottom-meet-greatest

(defthm atj-type-bottom-meet-greatest
  (implies (and (atj-type-bottom-<= z x)
                (atj-type-bottom-<= z y))
           (atj-type-bottom-<= z (atj-type-bottom-meet x y))))

Theorem: atj-type-bottom-meet-of-atj-maybe-type-fix-x

(defthm atj-type-bottom-meet-of-atj-maybe-type-fix-x
  (equal (atj-type-bottom-meet (atj-maybe-type-fix x)
                               y)
         (atj-type-bottom-meet x y)))

Theorem: atj-type-bottom-meet-atj-maybe-type-equiv-congruence-on-x

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

Theorem: atj-type-bottom-meet-of-atj-maybe-type-fix-y

(defthm atj-type-bottom-meet-of-atj-maybe-type-fix-y
  (equal (atj-type-bottom-meet x (atj-maybe-type-fix y))
         (atj-type-bottom-meet x y)))

Theorem: atj-type-bottom-meet-atj-maybe-type-equiv-congruence-on-y

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