Extension of atj-type-<= to include
(atj-type-bottom-<= sub sup) → yes/no
For certain purposes, we want to calculate
the greatest lower bound of two ATJ types w.r.t. atj-type-<=;
see atj-type-bottom-meet.
However, the ATJ types with this partial order
do not quite form a meet semilattice,
because there are no lower 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-bottom-<= (sub sup) (declare (xargs :guard (and (atj-maybe-typep sub) (atj-maybe-typep sup)))) (let ((__function__ 'atj-type-bottom-<=)) (declare (ignorable __function__)) (or (null sub) (and (not (null sup)) (atj-type-<= sub sup)))))
Theorem:
(defthm booleanp-of-atj-type-bottom-<= (b* ((yes/no (atj-type-bottom-<= sub sup))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-bottom-<=-reflexive (implies (atj-maybe-type-equiv x y) (atj-type-bottom-<= x y)))
Theorem:
(defthm atj-type-bottom-<=-antisymmetric (implies (and (atj-type-bottom-<= x y) (atj-type-bottom-<= y x)) (atj-maybe-type-equiv x y)))
Theorem:
(defthm atj-type-bottom-<=-transitive (implies (and (atj-type-bottom-<= x y) (atj-type-bottom-<= y z)) (atj-type-bottom-<= x z)))
Theorem:
(defthm atj-type-bottom-<=-of-atj-maybe-type-fix-sub (equal (atj-type-bottom-<= (atj-maybe-type-fix sub) sup) (atj-type-bottom-<= sub sup)))
Theorem:
(defthm atj-type-bottom-<=-atj-maybe-type-equiv-congruence-on-sub (implies (atj-maybe-type-equiv sub sub-equiv) (equal (atj-type-bottom-<= sub sup) (atj-type-bottom-<= sub-equiv sup))) :rule-classes :congruence)
Theorem:
(defthm atj-type-bottom-<=-of-atj-maybe-type-fix-sup (equal (atj-type-bottom-<= sub (atj-maybe-type-fix sup)) (atj-type-bottom-<= sub sup)))
Theorem:
(defthm atj-type-bottom-<=-atj-maybe-type-equiv-congruence-on-sup (implies (atj-maybe-type-equiv sup sup-equiv) (equal (atj-type-bottom-<= sub sup) (atj-type-bottom-<= sub sup-equiv))) :rule-classes :congruence)