Check if an expression is a binary expression.
If it is, return its operator and sub-expressions.
Function:
(defun check-expr-binary (expr) (declare (xargs :guard (exprp expr))) (let ((__function__ 'check-expr-binary)) (declare (ignorable __function__)) (if (expr-case expr :binary) (mv t (expr-binary->op expr) (expr-binary->arg1 expr) (expr-binary->arg2 expr)) (mv nil (irr-binop) (irr-expr) (irr-expr)))))
Theorem:
(defthm booleanp-of-check-expr-binary.yes/no (b* (((mv ?yes/no ?op ?arg1 ?arg2) (check-expr-binary expr))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm binopp-of-check-expr-binary.op (b* (((mv ?yes/no ?op ?arg1 ?arg2) (check-expr-binary expr))) (binopp op)) :rule-classes :rewrite)
Theorem:
(defthm exprp-of-check-expr-binary.arg1 (b* (((mv ?yes/no ?op ?arg1 ?arg2) (check-expr-binary expr))) (exprp arg1)) :rule-classes :rewrite)
Theorem:
(defthm exprp-of-check-expr-binary.arg2 (b* (((mv ?yes/no ?op ?arg1 ?arg2) (check-expr-binary expr))) (exprp arg2)) :rule-classes :rewrite)
Theorem:
(defthm expr-count-of-check-expr-binary-arg1 (b* (((mv ?yes/no ?op ?arg1 ?arg2) (check-expr-binary expr))) (implies yes/no (< (expr-count arg1) (expr-count expr)))) :rule-classes :linear)
Theorem:
(defthm expr-count-of-check-expr-binary-arg2 (b* (((mv ?yes/no ?op ?arg1 ?arg2) (check-expr-binary expr))) (implies yes/no (< (expr-count arg2) (expr-count expr)))) :rule-classes :linear)
Theorem:
(defthm check-expr-binary-of-expr-fix-expr (equal (check-expr-binary (expr-fix expr)) (check-expr-binary expr)))
Theorem:
(defthm check-expr-binary-expr-equiv-congruence-on-expr (implies (expr-equiv expr expr-equiv) (equal (check-expr-binary expr) (check-expr-binary expr-equiv))) :rule-classes :congruence)