Extension of atj-type-<= to include
(atj-type-top-<= sub sup) → yes/no
For certain purposes, we want to calculate
the least upper bound of two ATJ types w.r.t. atj-type-<=;
see atj-type-top-join.
However, the ATJ types with this partial order
do not quite form a join semilattice,
because there are no upper bounds, for instance,
for two different
Thus, we extend the partial order
to the set of ATJ types plus
We show that this extended relation is a partial order, i.e. reflexive, anti-symmetric, and transitive.
Function:
(defun atj-type-top-<= (sub sup) (declare (xargs :guard (and (atj-maybe-typep sub) (atj-maybe-typep sup)))) (let ((__function__ 'atj-type-top-<=)) (declare (ignorable __function__)) (or (null sup) (and (not (null sub)) (atj-type-<= sub sup)))))
Theorem:
(defthm booleanp-of-atj-type-top-<= (b* ((yes/no (atj-type-top-<= sub sup))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-top-<=-reflexive (implies (atj-maybe-type-equiv x y) (atj-type-top-<= x y)))
Theorem:
(defthm atj-type-top-<=-antisymmetric (implies (and (atj-type-top-<= x y) (atj-type-top-<= y x)) (atj-maybe-type-equiv x y)))
Theorem:
(defthm atj-type-top-<=-transitive (implies (and (atj-type-top-<= x y) (atj-type-top-<= y z)) (atj-type-top-<= x z)))
Theorem:
(defthm atj-type-top-<=-of-atj-maybe-type-fix-sub (equal (atj-type-top-<= (atj-maybe-type-fix sub) sup) (atj-type-top-<= sub sup)))
Theorem:
(defthm atj-type-top-<=-atj-maybe-type-equiv-congruence-on-sub (implies (atj-maybe-type-equiv sub sub-equiv) (equal (atj-type-top-<= sub sup) (atj-type-top-<= sub-equiv sup))) :rule-classes :congruence)
Theorem:
(defthm atj-type-top-<=-of-atj-maybe-type-fix-sup (equal (atj-type-top-<= sub (atj-maybe-type-fix sup)) (atj-type-top-<= sub sup)))
Theorem:
(defthm atj-type-top-<=-atj-maybe-type-equiv-congruence-on-sup (implies (atj-maybe-type-equiv sup sup-equiv) (equal (atj-type-top-<= sub sup) (atj-type-top-<= sub sup-equiv))) :rule-classes :congruence)