Total order on expression priorities.
(expr-priority-<= prio1 prio2) → yes/no
We assign a unique numeric index to each priority, and we compare the numbers. The higher the priority, the higher the number. The exact numbers do not matter; only their relative magnitude does.
This total order on expression priorities is
the reflexive and transitive closure of the binary relation
that consists of the pairs
Function:
(defun expr-priority-number (prio) (declare (xargs :guard (expr-priorityp prio))) (let ((__function__ 'expr-priority-number)) (declare (ignorable __function__)) (expr-priority-case prio :primary 16 :postfix 15 :unary 14 :cast 13 :mul 12 :add 11 :sh 10 :rel 9 :eq 8 :and 7 :xor 6 :ior 5 :logand 4 :logor 3 :cond 2 :asg 1 :expr 0)))
Theorem:
(defthm natp-of-expr-priority-number (b* ((number (expr-priority-number prio))) (natp number)) :rule-classes :rewrite)
Theorem:
(defthm expr-priority-number-of-expr-priority-fix-prio (equal (expr-priority-number (expr-priority-fix prio)) (expr-priority-number prio)))
Theorem:
(defthm expr-priority-number-expr-priority-equiv-congruence-on-prio (implies (expr-priority-equiv prio prio-equiv) (equal (expr-priority-number prio) (expr-priority-number prio-equiv))) :rule-classes :congruence)
Function:
(defun expr-priority-<= (prio1 prio2) (declare (xargs :guard (and (expr-priorityp prio1) (expr-priorityp prio2)))) (let ((__function__ 'expr-priority-<=)) (declare (ignorable __function__)) (<= (expr-priority-number prio1) (expr-priority-number prio2))))
Theorem:
(defthm booleanp-of-expr-priority-<= (b* ((yes/no (expr-priority-<= prio1 prio2))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm expr-priority-<=-of-expr-priority-fix-prio1 (equal (expr-priority-<= (expr-priority-fix prio1) prio2) (expr-priority-<= prio1 prio2)))
Theorem:
(defthm expr-priority-<=-expr-priority-equiv-congruence-on-prio1 (implies (expr-priority-equiv prio1 prio1-equiv) (equal (expr-priority-<= prio1 prio2) (expr-priority-<= prio1-equiv prio2))) :rule-classes :congruence)
Theorem:
(defthm expr-priority-<=-of-expr-priority-fix-prio2 (equal (expr-priority-<= prio1 (expr-priority-fix prio2)) (expr-priority-<= prio1 prio2)))
Theorem:
(defthm expr-priority-<=-expr-priority-equiv-congruence-on-prio2 (implies (expr-priority-equiv prio2 prio2-equiv) (equal (expr-priority-<= prio1 prio2) (expr-priority-<= prio1 prio2-equiv))) :rule-classes :congruence)