Direct subtype relation over primitive types [JLS14:4.10.1].
(primitive-type-<1 sub sup) → yes/no
This is denoted (for all types)
The direct subtype relation is irreflexive. Since this function fixes its arguments, we can express irreflexivity more strongly on equivalent (not necessarily equal) primitive types.
Function:
(defun primitive-type-<1 (sub sup) (declare (xargs :guard (and (primitive-typep sub) (primitive-typep sup)))) (let ((__function__ 'primitive-type-<1)) (declare (ignorable __function__)) (or (and (primitive-type-case sub :byte) (primitive-type-case sup :short)) (and (primitive-type-case sub :short) (primitive-type-case sup :int)) (and (primitive-type-case sub :int) (primitive-type-case sup :long)) (and (primitive-type-case sub :long) (primitive-type-case sup :float)) (and (primitive-type-case sub :float) (primitive-type-case sup :double)) (and (primitive-type-case sub :char) (primitive-type-case sup :int)))))
Theorem:
(defthm booleanp-of-primitive-type-<1 (b* ((yes/no (primitive-type-<1 sub sup))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm primitive-type-<1-irreflexive (implies (primitive-type-equiv x y) (not (primitive-type-<1 x y))))
Theorem:
(defthm primitive-type-<1-of-primitive-type-fix-sub (equal (primitive-type-<1 (primitive-type-fix sub) sup) (primitive-type-<1 sub sup)))
Theorem:
(defthm primitive-type-<1-primitive-type-equiv-congruence-on-sub (implies (primitive-type-equiv sub sub-equiv) (equal (primitive-type-<1 sub sup) (primitive-type-<1 sub-equiv sup))) :rule-classes :congruence)
Theorem:
(defthm primitive-type-<1-of-primitive-type-fix-sup (equal (primitive-type-<1 sub (primitive-type-fix sup)) (primitive-type-<1 sub sup)))
Theorem:
(defthm primitive-type-<1-primitive-type-equiv-congruence-on-sup (implies (primitive-type-equiv sup sup-equiv) (equal (primitive-type-<1 sub sup) (primitive-type-<1 sub sup-equiv))) :rule-classes :congruence)