Rewrite rules about certain functions distributing over if.
We found it necessary to include rules to distribute certain functions over ifs. It seems that, in the course of these symbolic execution proofs, we will always want to distribute functions over ifs. This distribution happens at the goal level, but not in the rewriter by default.
Theorem:
(defthm mv-nth-of-if (equal (mv-nth n (if a b c)) (if a (mv-nth n b) (mv-nth n c))))
Theorem:
(defthm scharp-of-if (equal (scharp (if a b c)) (if a (scharp b) (scharp c))))
Theorem:
(defthm ucharp-of-if (equal (ucharp (if a b c)) (if a (ucharp b) (ucharp c))))
Theorem:
(defthm sshortp-of-if (equal (sshortp (if a b c)) (if a (sshortp b) (sshortp c))))
Theorem:
(defthm ushortp-of-if (equal (ushortp (if a b c)) (if a (ushortp b) (ushortp c))))
Theorem:
(defthm sintp-of-if (equal (sintp (if a b c)) (if a (sintp b) (sintp c))))
Theorem:
(defthm uintp-of-if (equal (uintp (if a b c)) (if a (uintp b) (uintp c))))
Theorem:
(defthm slongp-of-if (equal (slongp (if a b c)) (if a (slongp b) (slongp c))))
Theorem:
(defthm ulongp-of-if (equal (ulongp (if a b c)) (if a (ulongp b) (ulongp c))))
Theorem:
(defthm sllongp-of-if (equal (sllongp (if a b c)) (if a (sllongp b) (sllongp c))))
Theorem:
(defthm ullongp-of-if (equal (ullongp (if a b c)) (if a (ullongp b) (ullongp c))))
Theorem:
(defthm booleanp-of-if (equal (booleanp (if a b c)) (if a (booleanp b) (booleanp c))))