Proper subtype relation over primitive types [JLS14:4.10].
(primitive-type-< sub sup) → yes/no
This is denoted (for all types)
It is the transitive closure of the direct subtype relation primitive-type-<1.
Function:
(defun primitive-type-< (sub sup) (declare (xargs :guard (and (primitive-typep sub) (primitive-typep sup)))) (let ((__function__ 'primitive-type-<)) (declare (ignorable __function__)) (primitive-type-case sub :boolean nil :char (or (primitive-type-case sup :int) (primitive-type-case sup :long) (primitive-type-case sup :float) (primitive-type-case sup :double)) :byte (or (primitive-type-case sup :short) (primitive-type-case sup :int) (primitive-type-case sup :long) (primitive-type-case sup :float) (primitive-type-case sup :double)) :short (or (primitive-type-case sup :int) (primitive-type-case sup :long) (primitive-type-case sup :float) (primitive-type-case sup :double)) :int (or (primitive-type-case sup :long) (primitive-type-case sup :float) (primitive-type-case sup :double)) :long (or (primitive-type-case sup :float) (primitive-type-case sup :double)) :float (primitive-type-case sup :double) :double nil)))
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-<-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)