		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svex-svstmt-ite

Signature
(svex-svstmt-ite test then else) → ite
Arguments: test — Guard (svex-p test).; then — Guard (svex-p then).; else — Guard (svex-p else).
Returns: ite — Type (svex-p ite).

Definitions and Theorems

Function: svex-svstmt-ite

(defun svex-svstmt-ite (test then else)
  (declare (xargs :guard (and (svex-p test)
                              (svex-p then)
                              (svex-p else))))
  (let ((__function__ 'svex-svstmt-ite))
    (declare (ignorable __function__))
    (b* ((test (svex-fix test))
         (then (svex-fix then))
         (else (svex-fix else)))
      (or (svex-case test :quote
                     (if (eql (4vec-reduction-or test.val) -1)
                         then
                       (if (eql (4vec-reduction-or test.val) 0)
                           else
                         nil))
                     :otherwise nil)
          (and (hons-equal then else) then)
          (svex-call '?*
                     (list test then else))))))

Theorem: svex-p-of-svex-svstmt-ite

(defthm svex-p-of-svex-svstmt-ite
  (b* ((ite (svex-svstmt-ite test then else)))
    (svex-p ite))
  :rule-classes :rewrite)

Theorem: svex-svstmt-ite-correct

(defthm svex-svstmt-ite-correct
  (b* ((?ite (svex-svstmt-ite test then else)))
    (equal (svex-eval ite env)
           (4vec-?* (svex-eval test env)
                    (svex-eval then env)
                    (svex-eval else env)))))

Theorem: vars-of-svex-svstmt-ite

(defthm vars-of-svex-svstmt-ite
  (b* ((?ite (svex-svstmt-ite test then else)))
    (implies (and (not (member v (svex-vars test)))
                  (not (member v (svex-vars then)))
                  (not (member v (svex-vars else))))
             (not (member v (svex-vars ite))))))

Theorem: svex-svstmt-ite-under-iff

(defthm svex-svstmt-ite-under-iff
  (b* ((?ite (svex-svstmt-ite test then else)))
    (iff ite t)))

Theorem: svex-svstmt-ite-when-cond-true

(defthm svex-svstmt-ite-when-cond-true
  (b* ((?ite (svex-svstmt-ite test then else)))
    (implies (equal (4vec-reduction-or (svex-eval test env))
                    -1)
             (equal (svex-eval ite env)
                    (svex-eval then env)))))

Theorem: svex-svstmt-ite-when-cond-false

(defthm svex-svstmt-ite-when-cond-false
  (b* ((?ite (svex-svstmt-ite test then else)))
    (implies (equal (4vec-reduction-or (svex-eval test env))
                    0)
             (equal (svex-eval ite env)
                    (svex-eval else env)))))

Theorem: svex-svstmt-ite-of-svex-fix-test

(defthm svex-svstmt-ite-of-svex-fix-test
  (equal (svex-svstmt-ite (svex-fix test)
                          then else)
         (svex-svstmt-ite test then else)))

Theorem: svex-svstmt-ite-svex-equiv-congruence-on-test

(defthm svex-svstmt-ite-svex-equiv-congruence-on-test
  (implies (svex-equiv test test-equiv)
           (equal (svex-svstmt-ite test then else)
                  (svex-svstmt-ite test-equiv then else)))
  :rule-classes :congruence)

Theorem: svex-svstmt-ite-of-svex-fix-then

(defthm svex-svstmt-ite-of-svex-fix-then
  (equal (svex-svstmt-ite test (svex-fix then)
                          else)
         (svex-svstmt-ite test then else)))

Theorem: svex-svstmt-ite-svex-equiv-congruence-on-then

(defthm svex-svstmt-ite-svex-equiv-congruence-on-then
  (implies (svex-equiv then then-equiv)
           (equal (svex-svstmt-ite test then else)
                  (svex-svstmt-ite test then-equiv else)))
  :rule-classes :congruence)

Theorem: svex-svstmt-ite-of-svex-fix-else

(defthm svex-svstmt-ite-of-svex-fix-else
  (equal (svex-svstmt-ite test then (svex-fix else))
         (svex-svstmt-ite test then else)))

Theorem: svex-svstmt-ite-svex-equiv-congruence-on-else

(defthm svex-svstmt-ite-svex-equiv-congruence-on-else
  (implies (svex-equiv else else-equiv)
           (equal (svex-svstmt-ite test then else)
                  (svex-svstmt-ite test then else-equiv)))
  :rule-classes :congruence)