		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Expr-grade-<=

Total order over expression grades.

Signature
(expr-grade-<= grade1 grade2) → yes/no
Arguments: grade1 — Guard (expr-gradep grade1).; grade2 — Guard (expr-gradep grade2).
Returns: yes/no — Type (booleanp yes/no).

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.

Definitions and Theorems

Function: expr-grade-index

(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: natp-of-expr-grade-index

(defthm natp-of-expr-grade-index
  (b* ((index (expr-grade-index grade)))
    (natp index))
  :rule-classes :rewrite)

Theorem: expr-grade-index-of-expr-grade-fix-grade

(defthm expr-grade-index-of-expr-grade-fix-grade
  (equal (expr-grade-index (expr-grade-fix grade))
         (expr-grade-index grade)))

Theorem: expr-grade-index-expr-grade-equiv-congruence-on-grade

(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: expr-grade-<=

(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: booleanp-of-expr-grade-<=

(defthm booleanp-of-expr-grade-<=
  (b* ((yes/no (expr-grade-<= grade1 grade2)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: expr-grade-<=-of-expr-grade-fix-grade1

(defthm expr-grade-<=-of-expr-grade-fix-grade1
  (equal (expr-grade-<= (expr-grade-fix grade1)
                        grade2)
         (expr-grade-<= grade1 grade2)))

Theorem: expr-grade-<=-expr-grade-equiv-congruence-on-grade1

(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: expr-grade-<=-of-expr-grade-fix-grade2

(defthm expr-grade-<=-of-expr-grade-fix-grade2
  (equal (expr-grade-<= grade1 (expr-grade-fix grade2))
         (expr-grade-<= grade1 grade2)))

Theorem: expr-grade-<=-expr-grade-equiv-congruence-on-grade2

(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)