Greatest lower bound of two ATJ types or
(atj-type-bottom-meet x y) → glb
As discussed in atj-type-bottom-<=,
the addition of
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.
Function:
(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:
(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:
(defthm atj-type-bottom-meet-lower-bound-left (atj-type-bottom-<= (atj-type-bottom-meet x y) x))
Theorem:
(defthm atj-type-bottom-meet-lower-bound-right (atj-type-bottom-<= (atj-type-bottom-meet x y) y))
Theorem:
(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:
(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:
(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:
(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:
(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)