Merge branch 'add/bind_let' into 'master'

Add bind_let rule

See merge request !14

spec/changelog.tex

@@ -15,6 +15,9 @@ Proof rules:
         clause.
   \item Addition of the \proofRule{reordering} rule to represent reordering of
         the literals in a clause.
+  \item Addition of the \proofRule{bind_let} rule.  This rule can be used to
+        preprocess \inlineAlethe{let} expressions similar to the \proofRule{bind}
+        rule used with ordinary quantifiers.
 \end{itemize}
 
 \noindent

spec/rule_list.tex

@@ -1551,9 +1551,55 @@ $k$. & $\Gamma$ & \ctxsep &
   The premise $i_1, \dots, i_n$ must be in the same subproof as
   the \currule{} step.  If for $t_i≈ s_i$ the $t_i$ and $s_i$
   are syntactically equal, the premise
-  is skipped.
+  is omitted.
 \end{RuleDescription}
 
+\begin{RuleDescription}{bind_let}
+  This rule corresponds to the \proofRule{bind} rule for \inlineAlethe{let}.
+  It allows the renaming of the variables bound by the \inlineAlethe{let} step,
+  the rewriting of the substituted terms, and the rewriting of the body of the 
+  \inlineAlethe{let}, resulting in a new \inlineAlethe{let} term.  
+  It has the form
+
+\begin{AletheXS}
+$i_1$. & $\Gamma$ & \ctxsep & $t_{1} ≈ s_{1}$ & ($\dots$) \\
+\aletheLineS
+$i_n$. & $\Gamma$ & \ctxsep & $t_{n} ≈ s_{n}$ & ($\dots$) \\
+\aletheLineS
+$j$. & \spctx{$\Gamma, y_1,\dots, y_n,  x_1 \mapsto y_1, \dots ,  x_n \mapsto y_n$}
+   & \ctxsep &  $u ≈ u'$ & ($\dots$) \\
+\spsep
+$k$. & $\Gamma$ & \kern-5.5em\ctxsep & % The kern hacking here is to make the rule readable
+     $ \kern-3em (\lsymb{let}\,x_1~=~t_1,\, \dots,\, x_n~=~t_n \lsymb{in}\, u) ≈
+                 (\lsymb{let}\,y_1~=~s_1,\, \dots,\, y_n~=~s_n\,\lsymb{in}\, u')$
+     & (\currule{}\;$i_1$, \dots, $i_n$) \\
+\end{AletheXS}
+
+  The variables $y_1, \dots, y_n$ are neither free in
+  $(\lsymb{let}\,x_1 = t_1,\, \dots,\, x_n = t_n\,\lsymb{in}\, u)$ nor, for each
+  $y_i$ different from $x_i$, occur in $\Gamma$.
+
+  The premise $i_1, \dots, i_n$ must be in the same subproof as
+  the \currule{} step.  If for $t_i≈ s_i$ the $t_i$ and $s_i$
+  are syntactically equal, the premise
+  is omitted.
+\end{RuleDescription}
+
+\begin{RuleExample}
+The following example shows how this rule is used in a proof generated
+by Carcara's elaborator.  It elaborates an implicit application of
+symmetry of equality.
+\begin{AletheVerb}
+(step t1 (cl (= (= 0 1) (= 1 0))) :rule eq_symmetric)
+(anchor :step t2 :args ((p Bool) (:= (p Bool) p)))
+(step t2.t1 (cl (= (= p false) (= false p))) :rule eq_symmetric)
+(step t2 (cl (= (let ((p (= 0 1))) (= p false))
+                (let ((p (= 1 0))) (= false p))))
+         :rule bind_let :premises (t1))
+\end{AletheVerb}
+ 
+\end{RuleExample}
+
 \begin{RuleDescription}{distinct_elim}
 This rule eliminates the $\lsymb{distinct}$ predicate. If called with one
 argument this predicate always holds: