Partial order over the ATJ types that denote built-in ACL2 types.
(atj-atype-<= sub sup) → yes/no
See atj-type-<=.
Function:
(defun atj-atype-<= (sub sup) (declare (xargs :guard (and (atj-atypep sub) (atj-atypep sup)))) (let ((__function__ 'atj-atype-<=)) (declare (ignorable __function__)) (and (atj-atype-case sub :integer (member-eq (atj-atype-kind sup) '(:integer :rational :number :value)) :rational (member-eq (atj-atype-kind sup) '(:rational :number :value)) :number (member-eq (atj-atype-kind sup) '(:number :value)) :character (member-eq (atj-atype-kind sup) '(:character :value)) :string (member-eq (atj-atype-kind sup) '(:string :value)) :symbol (member-eq (atj-atype-kind sup) '(:symbol :value)) :boolean (member-eq (atj-atype-kind sup) '(:boolean :symbol :value)) :cons (member-eq (atj-atype-kind sup) '(:cons :value)) :value (atj-atype-case sup :value)) t)))
Theorem:
(defthm booleanp-of-atj-atype-<= (b* ((yes/no (atj-atype-<= sub sup))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm atj-atype-<=-reflexive (implies (atj-atype-equiv x y) (atj-atype-<= x y)))
Theorem:
(defthm atj-atype-<=-antisymmetric (implies (and (atj-atype-<= x y) (atj-atype-<= y x)) (atj-atype-equiv x y)))
Theorem:
(defthm atj-atype-<=-transitive (implies (and (atj-atype-<= x y) (atj-atype-<= y z)) (atj-atype-<= x z)))
Theorem:
(defthm atj-atype-<=-of-value-left (implies (atj-atype-case x :value) (equal (atj-atype-<= x y) (atj-atype-case y :value))))
Theorem:
(defthm atj-atype-<=-of-cons-left (implies (atj-atype-case x :cons) (equal (atj-atype-<= x y) (or (atj-atype-case y :cons) (atj-atype-case y :value)))))
Theorem:
(defthm atj-atype-<=-of-atj-atype-fix-sub (equal (atj-atype-<= (atj-atype-fix sub) sup) (atj-atype-<= sub sup)))
Theorem:
(defthm atj-atype-<=-atj-atype-equiv-congruence-on-sub (implies (atj-atype-equiv sub sub-equiv) (equal (atj-atype-<= sub sup) (atj-atype-<= sub-equiv sup))) :rule-classes :congruence)
Theorem:
(defthm atj-atype-<=-of-atj-atype-fix-sup (equal (atj-atype-<= sub (atj-atype-fix sup)) (atj-atype-<= sub sup)))
Theorem:
(defthm atj-atype-<=-atj-atype-equiv-congruence-on-sup (implies (atj-atype-equiv sup sup-equiv) (equal (atj-atype-<= sub sup) (atj-atype-<= sub sup-equiv))) :rule-classes :congruence)