		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-minus-expression

Check if an integer negation expression is well-formed.

Signature
(check-minus-expression arg arg-type arg-obligs expr ctxt) → result
Arguments: arg — Guard (expressionp arg).; arg-type — Guard (typep arg-type).; arg-obligs — Guard (proof-obligation-listp arg-obligs).; expr — Guard (expressionp expr).; ctxt — Guard (contextp ctxt).
Returns: result — Type (type-resultp result).

The operand must be an integer, and the result is an integer.

Definitions and Theorems

Function: check-minus-expression

(defun check-minus-expression (arg arg-type arg-obligs expr ctxt)
 (declare (xargs :guard (and (expressionp arg)
                             (typep arg-type)
                             (proof-obligation-listp arg-obligs)
                             (expressionp expr)
                             (contextp ctxt))))
 (declare (ignorable expr))
 (let ((__function__ 'check-minus-expression))
   (declare (ignorable __function__))
   (b*
    (((mv okp obligs)
      (match-type arg arg-type (type-integer)
                  ctxt))
     ((unless okp)
      (type-result-err (list :type-mismatch-minus
                             (expression-fix arg)
                             (type-fix arg-type)
                             (type-boolean))))
     ((acl2::run-when (consp obligs))
      (raise "Internal error: obligations ~x0 for the integer type."
             obligs)))
    (make-type-result-ok :types (list (type-integer))
                         :obligations (append arg-obligs obligs)))))

Theorem: type-resultp-of-check-minus-expression

(defthm type-resultp-of-check-minus-expression
 (b*
  ((result
        (check-minus-expression arg arg-type arg-obligs expr ctxt)))
  (type-resultp result))
 :rule-classes :rewrite)

Theorem: check-minus-expression-of-expression-fix-arg

(defthm check-minus-expression-of-expression-fix-arg
 (equal (check-minus-expression (expression-fix arg)
                                arg-type arg-obligs expr ctxt)
        (check-minus-expression arg arg-type arg-obligs expr ctxt)))

Theorem: check-minus-expression-expression-equiv-congruence-on-arg

(defthm check-minus-expression-expression-equiv-congruence-on-arg
 (implies
   (expression-equiv arg arg-equiv)
   (equal (check-minus-expression arg arg-type arg-obligs expr ctxt)
          (check-minus-expression arg-equiv
                                  arg-type arg-obligs expr ctxt)))
 :rule-classes :congruence)

Theorem: check-minus-expression-of-type-fix-arg-type

(defthm check-minus-expression-of-type-fix-arg-type
 (equal (check-minus-expression arg (type-fix arg-type)
                                arg-obligs expr ctxt)
        (check-minus-expression arg arg-type arg-obligs expr ctxt)))

Theorem: check-minus-expression-type-equiv-congruence-on-arg-type

(defthm check-minus-expression-type-equiv-congruence-on-arg-type
 (implies
  (type-equiv arg-type arg-type-equiv)
  (equal
      (check-minus-expression arg arg-type arg-obligs expr ctxt)
      (check-minus-expression arg
                              arg-type-equiv arg-obligs expr ctxt)))
 :rule-classes :congruence)

Theorem: check-minus-expression-of-proof-obligation-list-fix-arg-obligs

(defthm
     check-minus-expression-of-proof-obligation-list-fix-arg-obligs
 (equal
      (check-minus-expression arg arg-type
                              (proof-obligation-list-fix arg-obligs)
                              expr ctxt)
      (check-minus-expression arg arg-type arg-obligs expr ctxt)))

Theorem: check-minus-expression-proof-obligation-list-equiv-congruence-on-arg-obligs

(defthm
 check-minus-expression-proof-obligation-list-equiv-congruence-on-arg-obligs
 (implies
  (proof-obligation-list-equiv arg-obligs arg-obligs-equiv)
  (equal
      (check-minus-expression arg arg-type arg-obligs expr ctxt)
      (check-minus-expression arg
                              arg-type arg-obligs-equiv expr ctxt)))
 :rule-classes :congruence)

Theorem: check-minus-expression-of-expression-fix-expr

(defthm check-minus-expression-of-expression-fix-expr
 (equal (check-minus-expression arg arg-type
                                arg-obligs (expression-fix expr)
                                ctxt)
        (check-minus-expression arg arg-type arg-obligs expr ctxt)))

Theorem: check-minus-expression-expression-equiv-congruence-on-expr

(defthm check-minus-expression-expression-equiv-congruence-on-expr
 (implies
  (expression-equiv expr expr-equiv)
  (equal
      (check-minus-expression arg arg-type arg-obligs expr ctxt)
      (check-minus-expression arg
                              arg-type arg-obligs expr-equiv ctxt)))
 :rule-classes :congruence)

Theorem: check-minus-expression-of-context-fix-ctxt

(defthm check-minus-expression-of-context-fix-ctxt
 (equal (check-minus-expression arg arg-type
                                arg-obligs expr (context-fix ctxt))
        (check-minus-expression arg arg-type arg-obligs expr ctxt)))

Theorem: check-minus-expression-context-equiv-congruence-on-ctxt

(defthm check-minus-expression-context-equiv-congruence-on-ctxt
 (implies
  (context-equiv ctxt ctxt-equiv)
  (equal
      (check-minus-expression arg arg-type arg-obligs expr ctxt)
      (check-minus-expression arg
                              arg-type arg-obligs expr ctxt-equiv)))
 :rule-classes :congruence)