		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Check-expr-mul

Check if an expression is a multiplication.

Signature
(check-expr-mul expr) → (mv yes/no arg1 arg2)
Arguments: expr — Guard (exprp expr).
Returns: yes/no — Type (booleanp yes/no).; arg1 — Type (exprp arg1).; arg2 — Type (exprp arg2).

If it is, return its two sub-expressions.

Definitions and Theorems

Function: check-expr-mul

(defun check-expr-mul (expr)
  (declare (xargs :guard (exprp expr)))
  (if (and (expr-case expr :binary)
           (binop-case (expr-binary->op expr)
                       :mul))
      (mv t (expr-binary->arg1 expr)
          (expr-binary->arg2 expr))
    (mv nil (irr-expr) (irr-expr))))

Theorem: booleanp-of-check-expr-mul.yes/no

(defthm booleanp-of-check-expr-mul.yes/no
  (b* (((mv ?yes/no ?arg1 ?arg2)
        (check-expr-mul expr)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: exprp-of-check-expr-mul.arg1

(defthm exprp-of-check-expr-mul.arg1
  (b* (((mv ?yes/no ?arg1 ?arg2)
        (check-expr-mul expr)))
    (exprp arg1))
  :rule-classes :rewrite)

Theorem: exprp-of-check-expr-mul.arg2

(defthm exprp-of-check-expr-mul.arg2
  (b* (((mv ?yes/no ?arg1 ?arg2)
        (check-expr-mul expr)))
    (exprp arg2))
  :rule-classes :rewrite)

Theorem: expr-count-of-check-expr-mul-arg1

(defthm expr-count-of-check-expr-mul-arg1
  (b* (((mv ?yes/no ?arg1 ?arg2)
        (check-expr-mul expr)))
    (implies yes/no
             (< (expr-count arg1)
                (expr-count expr))))
  :rule-classes :linear)

Theorem: expr-count-of-check-expr-mul-arg2

(defthm expr-count-of-check-expr-mul-arg2
  (b* (((mv ?yes/no ?arg1 ?arg2)
        (check-expr-mul expr)))
    (implies yes/no
             (< (expr-count arg2)
                (expr-count expr))))
  :rule-classes :linear)

Theorem: check-expr-mul-of-expr-fix-expr

(defthm check-expr-mul-of-expr-fix-expr
  (equal (check-expr-mul (expr-fix expr))
         (check-expr-mul expr)))

Theorem: check-expr-mul-expr-equiv-congruence-on-expr

(defthm check-expr-mul-expr-equiv-congruence-on-expr
  (implies (expr-equiv expr expr-equiv)
           (equal (check-expr-mul expr)
                  (check-expr-mul expr-equiv)))
  :rule-classes :congruence)