Total order over expression grades.
(expr-grade-<= grade1 grade2) → yes/no
See pprint-expressions for background.
We assign a numeric index to every grade and then we compare the indices. The indices indicate precedence: the smaller the index, the higher the precedence.
Function:
(defun expr-grade-index (grade) (declare (xargs :guard (expr-gradep grade))) (let ((__function__ 'expr-grade-index)) (declare (ignorable __function__)) (expr-grade-case grade :top 16 :assignment 15 :conditional 14 :logical-or 13 :logical-and 12 :ior 11 :xor 10 :and 9 :equality 8 :relational 7 :shift 6 :additive 5 :multiplicative 4 :cast 3 :unary 2 :postfix 1 :primary 0)))
Theorem:
(defthm natp-of-expr-grade-index (b* ((index (expr-grade-index grade))) (natp index)) :rule-classes :rewrite)
Theorem:
(defthm expr-grade-index-of-expr-grade-fix-grade (equal (expr-grade-index (expr-grade-fix grade)) (expr-grade-index grade)))
Theorem:
(defthm expr-grade-index-expr-grade-equiv-congruence-on-grade (implies (expr-grade-equiv grade grade-equiv) (equal (expr-grade-index grade) (expr-grade-index grade-equiv))) :rule-classes :congruence)
Function:
(defun expr-grade-<= (grade1 grade2) (declare (xargs :guard (and (expr-gradep grade1) (expr-gradep grade2)))) (let ((__function__ 'expr-grade-<=)) (declare (ignorable __function__)) (<= (expr-grade-index grade1) (expr-grade-index grade2))))
Theorem:
(defthm booleanp-of-expr-grade-<= (b* ((yes/no (expr-grade-<= grade1 grade2))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm expr-grade-<=-of-expr-grade-fix-grade1 (equal (expr-grade-<= (expr-grade-fix grade1) grade2) (expr-grade-<= grade1 grade2)))
Theorem:
(defthm expr-grade-<=-expr-grade-equiv-congruence-on-grade1 (implies (expr-grade-equiv grade1 grade1-equiv) (equal (expr-grade-<= grade1 grade2) (expr-grade-<= grade1-equiv grade2))) :rule-classes :congruence)
Theorem:
(defthm expr-grade-<=-of-expr-grade-fix-grade2 (equal (expr-grade-<= grade1 (expr-grade-fix grade2)) (expr-grade-<= grade1 grade2)))
Theorem:
(defthm expr-grade-<=-expr-grade-equiv-congruence-on-grade2 (implies (expr-grade-equiv grade2 grade2-equiv) (equal (expr-grade-<= grade1 grade2) (expr-grade-<= grade1 grade2-equiv))) :rule-classes :congruence)