Add some bitvector rules

This moves #31 forward!

spec/rule_list.tex

@@ -229,6 +229,16 @@ simplifications.}
 \ruleref{qnt_simplify} & Simplification of constant quantified formulas. \\
 \end{xltabular}
 
+\begin{xltabular}{\linewidth}{l X}
+\caption{Bitvector rules.}
+\label{rule-tab:simplification}\\
+  Rule & Description \\
+  \hline
+\ruleref{bitblast_extract} & Bitblasting of $\lsymb{extract}$. \\
+\ruleref{bitblast_ult} & Bitblasting of $\lsymb{ult}$. \\
+\ruleref{bitblast_add} & Bitblasting of $\lsymb{add}$. \\
+\end{xltabular}
+
 \subsection{Rule List}
 \label{sec:alethe:rules-list}
 
@@ -1530,6 +1540,112 @@ constants are unfolded during proof printing. Hence, the slightly strange
 form and the reordering of equalities.
 \end{RuleDescription}
 
+\begin{RuleDescription}{bitblast_extract}
+\begin{AletheX}
+$i$. & \ctxsep & $((\lsymb{extract}\ j\ i)\ x) ≈ (\lsymb{bbT}\ \varphi_i\ \ldots\ \varphi_j)$ & (\currule) \\
+\end{AletheX}
+
+\noindent
+where the formulas $\varphi_k$ are $(\lsymb{bitOf}_k\ x)$ for $i \leq k \leq j$.
+
+Alternatively, the rule may also be phrased as a ``short-circuiting'' of the
+above when $x$ is a $\lsymb{bbT}$ application:
+
+\medskip
+\begin{AletheX}
+$i$. & \ctxsep & $((\lsymb{extract}\ j\ i)\ (\lsymb{bbT}\ x_0\ \ldots\
+x_i\ \ldots \ x_j\ \ldots\ x_n)) ≈ (\lsymb{bbT}\ x_i\ \ldots\ x_j)$ & (\currule) \\
+\end{AletheX}
+
+\noindent
+This alternative is based on the validity of the equality
+\[
+\lsymb{bitOf}_k\ (\lsymb{bbT}\ x_0\ \ldots\ x_i\ \ldots \ x_j\ \ldots\ x_n) ≈ x_k
+\]
+for any bit-vector $x$ of size $n+1$, where $0\leq k\leq n$.
+
+\end{RuleDescription}
+
+\begin{RuleDescription}{bitblast_ult}
+\begin{AletheX}
+$i$. & \ctxsep & $(\lsymb{bvult}\ x\ y) ≈ \mathrm{res}_{n-1}$ & (\currule) \\
+\end{AletheX}
+in which both $x$ and $y$ must have the same type $(\lsymb{BitVec}\ n)$ and, for
+$i\geq 0$
+\[
+  \begin{array}{lcl}
+    \mathrm{res}_0&=&\neg (\lsymb{bitOf}_0\ x) \wedge (\lsymb{bitOf}_0\ y)\\
+    \mathrm{res}_{i+1}&=&(((\lsymb{bitOf}_{i+1}\ x) ≈ (\lsymb{bitOf}_{i+1}\ y))\wedge \mathrm{res}_i)\vee
+                       (\neg (\lsymb{bitOf}_{i+1}\ x) \wedge (\lsymb{bitOf}_{i+1}\ y))
+  \end{array}
+\]
+
+\noindent
+Alternatively, the rule may also be phrased as a ``short-circuiting'' of the
+above when $x$ and $y$ are ``$\lsymb{bbT}$'' applications. So given that
+\[
+  \begin{array}{lcl}
+    x&=&(\lsymb{bbT}\ x_0\ \ldots\ x_i\ \ldots \ x_j\ \ldots\ x_n)\\
+    y&=&(\lsymb{bbT}\ y_0\ \ldots\ y_i\ \ldots \ y_j\ \ldots\ y_n)\\
+  \end{array}
+\]
+then ``$\mathrm{res}$'' can be defined, for $i \geq 0$, as 
+\[
+  \begin{array}{lcl}
+    \mathrm{res}_0&=&\neg x_0 \wedge y_0\\
+    \mathrm{res}_{i+1}&=&((x_{i+1} ≈ y_{i+1})\wedge
+                          \mathrm{res}_i)\vee (\neg x_{i+1}\wedge y_{i+1})
+  \end{array}
+\]
+
+\end{RuleDescription}
+
+\begin{RuleDescription}{bitblast_add}
+\begin{AletheX}
+$i$. & \ctxsep & $(\lsymb{bvadd}\ x\ y) ≈ A_1$ & (\currule) \\
+\end{AletheX}
+in which both $x$ and $y$ must have the same type $(\lsymb{BitVec}\ n)$.
+The term ``$A_1$'' is
+\begin{align*}
+(\lsymb{bbT}\;& (((\lsymb{bitOf}_{0}\ x) \,\lsymb{xor}\,(\lsymb{bitOf}_{0}\ y))\,\lsymb{xor}\,\mathrm{carry}_0) \\
+              & (((\lsymb{bitOf}_{1}\ x) \,\lsymb{xor}\,(\lsymb{bitOf}_{1}\ y))\,\lsymb{xor}\,\mathrm{carry}_1) \\
+              & \ldots \\
+              & (((\lsymb{bitOf}_{n-1}\ x) \,\lsymb{xor}\, (\lsymb{bitOf}_{n-1}\ y))\,\lsymb{xor}\,\mathrm{carry}_{n-1}))
+\end{align*}
+and for $i\geq 0$
+\[
+  \begin{array}{lcl}
+    \mathrm{carry}_0&=&\bot\\
+    \mathrm{carry}_{i+1}&=&((\lsymb{bitOf}_{i}\ x) \wedge (\lsymb{bitOf}_{i}\ y))\vee(((\lsymb{bitOf}_{i}\ x)\,\lsymb{xor}\, (\lsymb{bitOf}_{i}\ y))\wedge \mathrm{carry}_i)
+  \end{array}
+\]
+
+\noindent
+Alternatively, the rule may also be phrased as a ``short-circuiting'' of the
+above when $x$ and $y$ are ``$\lsymb{bbT}$'' applications. So given that
+\[
+  \begin{array}{lcl}
+    x&=&(\lsymb{bbT}\ x_0\ \ldots\ x_i\ \ldots \ x_j\ \ldots\ x_n)\\
+    y&=&(\lsymb{bbT}\ y_0\ \ldots\ y_i\ \ldots \ y_j\ \ldots\ y_n)\\
+  \end{array}
+\]
+then the rule can be alternatively phrased as
+
+\begin{AletheX}
+$i$. & \ctxsep & $(\mathrm{bvadd}\ x\ y) ≈ A_2$ & (\currule) \\
+\end{AletheX}
+with $A_2 := (\lsymb{bbT}\ (x_0 \,\lsymb{xor}\, y_0)\,\lsymb{xor}\,\mathrm{carry}_0\ \ldots\ (x_{n-1}
+        \,\lsymb{xor}\, y_{n-1})\,\lsymb{xor}\,\mathrm{carry}_{n-1})$ and
+``$\mathrm{carry}$'' being defined, for $i \geq 0$, as 
+\[
+  \begin{array}{lcl}
+    \mathrm{carry}_0&=&\bot\\
+    \mathrm{carry}_{i+1}&=&(x_i\wedge y_i)\vee((x_i\,\lsymb{xor}\, y_i)\wedge \mathrm{carry}_i)
+  \end{array}
+\]
+
+\end{RuleDescription}
+
 \clearpage
 \subsection{Index of Rules}
 \label{sec:alethe:rules-index}