		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-not-expression

Check if a boolean negation expression is well-formed.

Signature
(check-not-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 a boolean, and the result is a boolean.

Definitions and Theorems

Function: check-not-expression

(defun check-not-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-not-expression))
   (declare (ignorable __function__))
   (b*
    (((mv okp obligs)
      (match-type arg arg-type (type-boolean)
                  ctxt))
     ((unless okp)
      (type-result-err (list :type-mismatch-not (expression-fix arg)
                             (type-fix arg-type)
                             (type-boolean))))
     ((acl2::run-when (consp obligs))
      (raise "Internal error: obligations ~x0 for the boolean type."
             obligs)))
    (make-type-result-ok :types (list (type-boolean))
                         :obligations (append arg-obligs obligs)))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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