Lift supremum-type to lists.
(supremum-type-list types1 types2 tops) → (mv okp supremum)
The two input lists must have the same length for the supremum to exist.
Given that
Function:
(defun supremum-type-list (types1 types2 tops) (declare (xargs :guard (and (type-listp types1) (type-listp types2) (toplevel-listp tops)))) (let ((__function__ 'supremum-type-list)) (declare (ignorable __function__)) (b* (((when (endp types1)) (mv (endp types2) nil)) ((when (endp types2)) (mv nil nil)) (type (supremum-type (car types1) (car types2) tops)) ((when (not type)) (mv nil nil)) ((mv okp types) (supremum-type-list (cdr types1) (cdr types2) tops)) ((when (not okp)) (mv nil nil))) (mv t (cons type types)))))
Theorem:
(defthm booleanp-of-supremum-type-list.okp (b* (((mv ?okp ?supremum) (supremum-type-list types1 types2 tops))) (booleanp okp)) :rule-classes :rewrite)
Theorem:
(defthm type-listp-of-supremum-type-list.supremum (b* (((mv ?okp ?supremum) (supremum-type-list types1 types2 tops))) (type-listp supremum)) :rule-classes :rewrite)
Theorem:
(defthm supremum-type-list-of-type-list-fix-types1 (equal (supremum-type-list (type-list-fix types1) types2 tops) (supremum-type-list types1 types2 tops)))
Theorem:
(defthm supremum-type-list-type-list-equiv-congruence-on-types1 (implies (type-list-equiv types1 types1-equiv) (equal (supremum-type-list types1 types2 tops) (supremum-type-list types1-equiv types2 tops))) :rule-classes :congruence)
Theorem:
(defthm supremum-type-list-of-type-list-fix-types2 (equal (supremum-type-list types1 (type-list-fix types2) tops) (supremum-type-list types1 types2 tops)))
Theorem:
(defthm supremum-type-list-type-list-equiv-congruence-on-types2 (implies (type-list-equiv types2 types2-equiv) (equal (supremum-type-list types1 types2 tops) (supremum-type-list types1 types2-equiv tops))) :rule-classes :congruence)
Theorem:
(defthm supremum-type-list-of-toplevel-list-fix-tops (equal (supremum-type-list types1 types2 (toplevel-list-fix tops)) (supremum-type-list types1 types2 tops)))
Theorem:
(defthm supremum-type-list-toplevel-list-equiv-congruence-on-tops (implies (toplevel-list-equiv tops tops-equiv) (equal (supremum-type-list types1 types2 tops) (supremum-type-list types1 types2 tops-equiv))) :rule-classes :congruence)