Least upper bound of two ATJ types or
(atj-type-top-join x y) → lub
As discussed in atj-type-top-<=,
the addition of
We define this operation by five cases:
the first two are obvious,
while the remaining three are motivated by the fact that
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.
Function:
(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:
(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:
(defthm atj-type-top-join-upper-bound-left (atj-type-top-<= x (atj-type-top-join x y)))
Theorem:
(defthm atj-type-top-join-upper-bound-right (atj-type-top-<= y (atj-type-top-join x y)))
Theorem:
(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:
(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:
(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:
(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:
(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)