		Search-engine friendly clone of the ACL2 documentation.

Expression

Expression-count

Measure for recurring over expression structures.

Signature
(expression-count x) → count
Arguments: x — Guard (expressionp x).
Returns: count — Type (natp count).

Definitions and Theorems

Function: expression-count

(defun expression-count (x)
  (declare (xargs :guard (expressionp x)))
  (let ((__function__ 'expression-count))
    (declare (ignorable __function__))
    (case (expression-kind x)
      (:const 1)
      (:var 1)
      (:add (+ 3
               (expression-count (expression-add->arg1 x))
               (expression-count (expression-add->arg2 x))))
      (:mul (+ 3
               (expression-count (expression-mul->arg1 x))
               (expression-count (expression-mul->arg2 x)))))))

Theorem: natp-of-expression-count

(defthm natp-of-expression-count
  (b* ((count (expression-count x)))
    (natp count))
  :rule-classes :type-prescription)

Theorem: expression-count-of-expression-fix-x

(defthm expression-count-of-expression-fix-x
  (equal (expression-count (expression-fix x))
         (expression-count x)))

Theorem: expression-count-expression-equiv-congruence-on-x

(defthm expression-count-expression-equiv-congruence-on-x
  (implies (expression-equiv x x-equiv)
           (equal (expression-count x)
                  (expression-count x-equiv)))
  :rule-classes :congruence)

Theorem: expression-count-of-expression-add

(defthm expression-count-of-expression-add
  (implies t
           (< (+ (expression-count arg1)
                 (expression-count arg2))
              (expression-count (expression-add arg1 arg2))))
  :rule-classes :linear)

Theorem: expression-count-of-expression-add->arg1

(defthm expression-count-of-expression-add->arg1
  (implies (equal (expression-kind x) :add)
           (< (expression-count (expression-add->arg1 x))
              (expression-count x)))
  :rule-classes :linear)

Theorem: expression-count-of-expression-add->arg2

(defthm expression-count-of-expression-add->arg2
  (implies (equal (expression-kind x) :add)
           (< (expression-count (expression-add->arg2 x))
              (expression-count x)))
  :rule-classes :linear)

Theorem: expression-count-of-expression-mul

(defthm expression-count-of-expression-mul
  (implies t
           (< (+ (expression-count arg1)
                 (expression-count arg2))
              (expression-count (expression-mul arg1 arg2))))
  :rule-classes :linear)

Theorem: expression-count-of-expression-mul->arg1

(defthm expression-count-of-expression-mul->arg1
  (implies (equal (expression-kind x) :mul)
           (< (expression-count (expression-mul->arg1 x))
              (expression-count x)))
  :rule-classes :linear)

Theorem: expression-count-of-expression-mul->arg2

(defthm expression-count-of-expression-mul->arg2
  (implies (equal (expression-kind x) :mul)
           (< (expression-count (expression-mul->arg2 x))
              (expression-count x)))
  :rule-classes :linear)