Lift atj-type-top-join to lists.
(atj-type-top-list-join x y) → lub
This is done element-wise. When the shorter list is exhausted, we return (what remains of) the longer list.
We show that this indeed returns the least upper bound of the order relation lifted to lists.
Function:
(defun atj-type-top-list-join (x y) (declare (xargs :guard (and (atj-maybe-type-listp x) (atj-maybe-type-listp y)))) (let ((__function__ 'atj-type-top-list-join)) (declare (ignorable __function__)) (cond ((endp x) (atj-maybe-type-list-fix y)) ((endp y) (atj-maybe-type-list-fix x)) (t (cons (atj-type-top-join (car x) (car y)) (atj-type-top-list-join (cdr x) (cdr y)))))))
Theorem:
(defthm atj-maybe-type-listp-of-atj-type-top-list-join (b* ((lub (atj-type-top-list-join x y))) (atj-maybe-type-listp lub)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-top-list-join-upper-bound-left (atj-type-top-list-<= x (atj-type-top-list-join x y)))
Theorem:
(defthm atj-type-top-list-join-upper-bound-right (atj-type-top-list-<= y (atj-type-top-list-join x y)))
Theorem:
(defthm atj-type-top-list-join-least (implies (and (atj-type-top-list-<= x z) (atj-type-top-list-<= y z)) (atj-type-top-list-<= (atj-type-top-list-join x y) z)))
Theorem:
(defthm consp-of-atj-type-top-list-join (b* ((?lub (atj-type-top-list-join x y))) (equal (consp lub) (or (consp x) (consp y)))))
Theorem:
(defthm atj-type-top-list-join-of-atj-maybe-type-list-fix-x (equal (atj-type-top-list-join (atj-maybe-type-list-fix x) y) (atj-type-top-list-join x y)))
Theorem:
(defthm atj-type-top-list-join-atj-maybe-type-list-equiv-congruence-on-x (implies (atj-maybe-type-list-equiv x x-equiv) (equal (atj-type-top-list-join x y) (atj-type-top-list-join x-equiv y))) :rule-classes :congruence)
Theorem:
(defthm atj-type-top-list-join-of-atj-maybe-type-list-fix-y (equal (atj-type-top-list-join x (atj-maybe-type-list-fix y)) (atj-type-top-list-join x y)))
Theorem:
(defthm atj-type-top-list-join-atj-maybe-type-list-equiv-congruence-on-y (implies (atj-maybe-type-list-equiv y y-equiv) (equal (atj-type-top-list-join x y) (atj-type-top-list-join x y-equiv))) :rule-classes :congruence)