		Search-engine friendly clone of the ACL2 documentation.

Semantics

Beval

Semantics of Imp boolean expressions.

Signature
(beval exp env) → bool
Arguments: exp — Guard (bexpp exp).; env — Guard (envp env).
Returns: bool — Type (booleanp bool).

This is formalized via an evaluation function that maps a boolean expression and an environment to a boolean. The boolean is the value of the expression given the environment.

Since boolean expressions may contain arithmetic expressions, the evaluation of boolean expressions involves the evaluation of arithmetic expressions.

The (recursive) evaluation of Imp's boolean expressions always terminates.

This evaluation function is executable.

Definitions and Theorems

Function: beval

(defun beval (exp env)
  (declare (xargs :guard (and (bexpp exp) (envp env))))
  (bexp-case exp
             :const exp.value
             :equal (equal (aeval exp.left env)
                           (aeval exp.right env))
             :less (< (aeval exp.left env)
                      (aeval exp.right env))
             :not (not (beval exp.arg env))
             :and (and (beval exp.left env)
                       (beval exp.right env))))

Theorem: booleanp-of-beval

(defthm booleanp-of-beval
  (b* ((bool (beval exp env)))
    (booleanp bool))
  :rule-classes :rewrite)

Theorem: beval-of-bexp-fix-exp

(defthm beval-of-bexp-fix-exp
  (equal (beval (bexp-fix exp) env)
         (beval exp env)))

Theorem: beval-bexp-equiv-congruence-on-exp

(defthm beval-bexp-equiv-congruence-on-exp
  (implies (bexp-equiv exp exp-equiv)
           (equal (beval exp env)
                  (beval exp-equiv env)))
  :rule-classes :congruence)

Theorem: beval-of-env-fix-env

(defthm beval-of-env-fix-env
  (equal (beval exp (env-fix env))
         (beval exp env)))

Theorem: beval-env-equiv-congruence-on-env

(defthm beval-env-equiv-congruence-on-env
  (implies (env-equiv env env-equiv)
           (equal (beval exp env)
                  (beval exp env-equiv)))
  :rule-classes :congruence)