Simplify conditional expressions whose condition is a boolean literal, in statements and blocks.
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)