Subtype relation over primitive types [JLS14:4.10].
(primitive-type-<= sub sup) → yes/no
This is denoted (for all types)
It is the reflexive and transitive closure of the direct subtype relation primitive-type-<1, or equivalently the reflexive closure of primitive-type-<.
The subtype relation is a partial order: reflexive, antisymmetric, and transitive. Antisymmetry must be stated modulo fixing, because this function is defined to fix its arguments. Since this function fixes its arguments, reflexivity can be stated more strongly on equivalent (not necessarily equal) primitive-types.
Function:
(defun primitive-type-<= (sub sup) (declare (xargs :guard (and (primitive-typep sub) (primitive-typep sup)))) (let ((__function__ 'primitive-type-<=)) (declare (ignorable __function__)) (or (primitive-type-equiv sub sup) (primitive-type-< sub sup))))
Theorem:
(defthm booleanp-of-primitive-type-<= (b* ((yes/no (primitive-type-<= sub sup))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm primitive-type-<=-when-primitive-type-<1 (implies (primitive-type-<1 x y) (primitive-type-<= x y)))
Theorem:
(defthm primitive-type-<=-reflexive (implies (primitive-type-equiv x y) (primitive-type-<= x y)))
Theorem:
(defthm primitive-type-<=-antisymmetric (implies (and (primitive-type-<= x y) (primitive-type-<= y x)) (primitive-type-equiv x y)))
Theorem:
(defthm primitive-type-<=-transitive (implies (and (primitive-type-<= x y) (primitive-type-<= y z)) (primitive-type-<= x z)))
Theorem:
(defthm primitive-type-<=-of-primitive-type-fix-sub (equal (primitive-type-<= (primitive-type-fix sub) sup) (primitive-type-<= sub sup)))
Theorem:
(defthm primitive-type-<=-primitive-type-equiv-congruence-on-sub (implies (primitive-type-equiv sub sub-equiv) (equal (primitive-type-<= sub sup) (primitive-type-<= sub-equiv sup))) :rule-classes :congruence)
Theorem:
(defthm primitive-type-<=-of-primitive-type-fix-sup (equal (primitive-type-<= sub (primitive-type-fix sup)) (primitive-type-<= sub sup)))
Theorem:
(defthm primitive-type-<=-primitive-type-equiv-congruence-on-sup (implies (primitive-type-equiv sup sup-equiv) (equal (primitive-type-<= sub sup) (primitive-type-<= sub sup-equiv))) :rule-classes :congruence)