		Search-engine friendly clone of the ACL2 documentation.

Atj-post-translation-simplify-conds

Atj-simplify-conds-in-jstatems+jblocks

Simplify conditional expressions whose condition is a boolean literal, in statements and blocks.

Definitions and Theorems

Function: atj-simplify-conds-in-jstatem

(defun atj-simplify-conds-in-jstatem (statem)
 (declare (xargs :guard (jstatemp statem)))
 (let ((__function__ 'atj-simplify-conds-in-jstatem))
  (declare (ignorable __function__))
  (jstatem-case
   statem
   :locvar (jstatem-locvar statem.get)
   :expr (jstatem-expr (atj-simplify-conds-in-jexpr statem.get))
   :return
   (jstatem-return (and statem.expr?
                        (atj-simplify-conds-in-jexpr statem.expr?)))
   :throw (jstatem-throw (atj-simplify-conds-in-jexpr statem.expr))
   :break (jstatem-break)
   :continue (jstatem-continue)
   :if (jstatem-if (atj-simplify-conds-in-jexpr statem.test)
                   (atj-simplify-conds-in-jblock statem.then))
   :ifelse
   (jstatem-ifelse (atj-simplify-conds-in-jexpr statem.test)
                   (atj-simplify-conds-in-jblock statem.then)
                   (atj-simplify-conds-in-jblock statem.else))
   :while (jstatem-while (atj-simplify-conds-in-jexpr statem.test)
                         (atj-simplify-conds-in-jblock statem.body))
   :do (jstatem-do (atj-simplify-conds-in-jblock statem.body)
                   (atj-simplify-conds-in-jexpr statem.test))
   :for (jstatem-for (atj-simplify-conds-in-jexpr statem.init)
                     (atj-simplify-conds-in-jexpr statem.test)
                     (atj-simplify-conds-in-jexpr statem.update)
                     (atj-simplify-conds-in-jblock statem.body)))))

Function: atj-simplify-conds-in-jblock

(defun atj-simplify-conds-in-jblock (block)
  (declare (xargs :guard (jblockp block)))
  (let ((__function__ 'atj-simplify-conds-in-jblock))
    (declare (ignorable __function__))
    (cond ((endp block) nil)
          (t (cons (atj-simplify-conds-in-jstatem (car block))
                   (atj-simplify-conds-in-jblock (cdr block)))))))

Theorem: return-type-of-atj-simplify-conds-in-jstatem.new-statem

(defthm return-type-of-atj-simplify-conds-in-jstatem.new-statem
  (b* ((?new-statem (atj-simplify-conds-in-jstatem statem)))
    (jstatemp new-statem))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-simplify-conds-in-jblock.new-block

(defthm return-type-of-atj-simplify-conds-in-jblock.new-block
  (b* ((?new-block (atj-simplify-conds-in-jblock block)))
    (jblockp new-block))
  :rule-classes :rewrite)

Theorem: atj-simplify-conds-in-jstatem-of-jstatem-fix-statem

(defthm atj-simplify-conds-in-jstatem-of-jstatem-fix-statem
  (equal (atj-simplify-conds-in-jstatem (jstatem-fix statem))
         (atj-simplify-conds-in-jstatem statem)))

Theorem: atj-simplify-conds-in-jblock-of-jblock-fix-block

(defthm atj-simplify-conds-in-jblock-of-jblock-fix-block
  (equal (atj-simplify-conds-in-jblock (jblock-fix block))
         (atj-simplify-conds-in-jblock block)))

Theorem: atj-simplify-conds-in-jstatem-jstatem-equiv-congruence-on-statem

(defthm
   atj-simplify-conds-in-jstatem-jstatem-equiv-congruence-on-statem
  (implies (jstatem-equiv statem statem-equiv)
           (equal (atj-simplify-conds-in-jstatem statem)
                  (atj-simplify-conds-in-jstatem statem-equiv)))
  :rule-classes :congruence)

Theorem: atj-simplify-conds-in-jblock-jblock-equiv-congruence-on-block

(defthm
      atj-simplify-conds-in-jblock-jblock-equiv-congruence-on-block
  (implies (jblock-equiv block block-equiv)
           (equal (atj-simplify-conds-in-jblock block)
                  (atj-simplify-conds-in-jblock block-equiv)))
  :rule-classes :congruence)

Subtopics

Atj-simplify-conds-in-jstatem
Atj-simplify-conds-in-jblock