\renewcommand\cfile{thms.tex}

\subsection{Theorems proved using Isabelle} \label{thpr}
We give some examples of theorems and derived rules
that have been proved in \dRA, using Isabelle.
They show how some relation algebraic results can be turned into structural
derived rules, ie, rules in which all the operators are structural, and
all the variables denote arbitrary structures.
This (together with the display postulates) enables them to be reused
in doing proofs in structural form.

Chin \& Tarski \cite{CT} give a number of results whose proof is
far from simple.
%For many theorems, it is also possible to state a purely structural version,
%as a structural rule.
For example, their Theorem 2.7 and the corresponding structural rule are
\begin{center}
$ (a \circ b) \land c \vdash a \circ ((\smile a \circ c) \land b) $
\qquad
\slrule
{X; ((\bullet X; Z), Y) \vdash W}
{(X; Y), Z \vdash W}
\end{center}
Chin \& Tarski \cite{CT} Theorem 2.11 and its corresponding structural rule
are
\begin{center}
$(r \circ s) \land (t \circ u)
\vdash (r \circ ((\smile r \circ t) \land (s \circ \smile u))) \circ u
$ \hfill
%which is proved as \ttdef{CT211}.
\slrule
{(U; ((\bullet U; W), (V; \bullet X))); X \vdash Z}
{(U; V), (W; X) \vdash Z}
\end{center}
%which is derived as \ttdef{CT211sr}.
The Dedekind rule (\cite{RALL}, \S5.3; \cite{RALF}, \S2.1) 
and its corresponding structural rule are
\begin{center}
$
(q \circ r) \land s
\vdash (q \land (s \circ \smile r)) \circ (r \land (\smile q \circ s))
$ \quad
%It is proved as \ttdef{ded} \insrc{ded.ML}.
%The structural rule version
\slrule
{(X, (Z; \bullet Y)); (Y, (\bullet X; Z)) \vdash W}
{(X; Y), Z \vdash W}
\end{center}
%is derived as \ttdef{dedsr}.
All these results were proved in \dRA, using Isabelle.

Some interesting theorems were 
useful in various areas of \cite{thesis}.
Again, they can be proved in the form of structural rules.
These show an interesting similarity between the 
Boolean and relational ``times'' operators, `,' and `;',
and their identities, $I$ and $E$.
Firstly, we have
\begin{center} \hfill
\invrule {((X; Y), E); Z \vdash W } { ((X, \bullet Y); I), Z \vdash W}
(\ttdl{thab}) \hfill \mbox{}
\end{center}

Next we have two results which can be proved from it.

\begin{center} \hfill
\invrule { (X, E); (Y, Z) \vdash W } { ((X, E); Y), Z \vdash W }
(\ttdl{th78sr}) \hfill
\invrule { (X; I), (Y; Z) \vdash W } { ((X; I), Y); Z \vdash W }
(\ttdl{th56sr}) \hfill \mbox{}
\end{center}

These results have the following corollaries,
giving examples of cases where the
Boolean and relational products of two quantities are equal.
\begin{center}
  \hfill
\invrule { (X, E); (E, Z) \vdash W } { (X, E), (E, Z) \vdash W }
(\ttdl{cor78i}) \hfill
\invrule { (X; I), (I; Z) \vdash W } { (X; I); (I; Z) \vdash W }
(\ttdl{cor56i}) \hfill \mbox{}
\end{center}
%These corollaries are obtained by
%setting $Y = E$ in \texttt{th78sr},
%and $Y = I$ in \texttt{th56sr}.

\subsection{Proving the RA axioms} \label{provRA}

Using Isabelle we can mechanize the formal proofs of completeness of \dRA\ with
respect to \RA.
Here, we sketch how this is done.
We show, informally,
how any result provable in \RA\ can be proved in \dRA.
%This is a result about the completeness of \dRA\ with respect to \RA.
This completeness result 
is weaker than Theorem 6 of \cite{dRA}
in that we only show how to derive, in \dRA, any \RA-equation
(expressed in terms of \emph{formulae});
by contrast,
\cite{dRA} also deals with \dRA-sequents involving \emph{structures}
whose translation into a formula inequality is valid in \RA.

In \cite{dRA}
a (Lindenbaum) relation algebra is constructed from \dRA.
Here we consider the proof system which corresponds to \RA.
By the completeness theorem of Birkhoff \cite{birk}, discussed in \cite{ho},
the proof rules for \RA\
consist only of substituting terms for variables 
in the relevant equations
(defining a Boolean algebra and (RA2) to (RA8)),
and replacing equals by equals.

Firstly, following \cite{dRA}, Theorem 6,
we let $A=B$ mean $A \vdash B$ and $B \vdash A$;
more formally, we introduce the following rules
\begin{center}
\slrule {A \vdash B \quad B \vdash A } { A = B}(\ttdef{eqI})
\qquad
\slrule {A = B } { A \vdash B}(\ttdef{eqD1})
\qquad
\slrule {A = B } { B \vdash A}(\ttdef{eqD2})
\end{center}
%\seesrc{RA.thy}.
%It was easy to prove that this equality is reflexive, symmetric and transitive.
This equality was easily proved to be reflexive, symmetric and transitive.
%proved as \ttdef{eqrefl}, \ttdef{eqsym} and \ttdef{eqtrans}. %\insrc{RA.ML}.
We define $A \leq B$ as $(A \land B) = A$, as in \RA.
It is then proved %, as the theorem \ttdef{lett}, 
that \mbox{$A \leq B \iff A \vdash B$}.

Then the \RA\ axioms can be proved; (RA2) to (RA8) are proved using Isabelle.
%\src{RA.ML}\@.
Axiom (RA1), which says that the logical operators form a Boolean algebra,
follows from the fact that \dRA\
%Gentzen sequent calculus
contains classical propositional logic.% (see \S\ref{decproc}).

In using the \RA\ axioms we would implicitly rely on the 
equality operator $=$ being symmetric and transitive,
which we proved, as indicated above.
The proof system for \RA\ also uses the fact,
as noted above, that equality permits substitution of equals.
That is, suppose $C[A]$ and $C[B]$ are formulae
such that $C[B]$ is obtained from $C[A]$ by replacing some occurrences of $A$
by $B$. 
If we now prove in \RA\ that
$A = B$ and $C[A] = D$ then 
we could deduce $C[B] = D$ by substituting $B$ for $A$.
%from \RA\ equations $A = B$ and $C[A] = D$, 
%one deduces $C[B] = D$.

To show that this can be done in \dRA\
we have to use induction on the structure of $C[\cdot]$. 
Each induction step 
uses one of six derived results, of which two are shown below.
%, proved as \ttdef{eqcs} in \src{RA.ML}.
\begin{center} 
\begin{tabular}{c@{\quad}c@{\quad}c}
\slrule {A_1 = A \quad B_1 = B} {A_1 \land B_1 = A \land B}
(\ttdef{eqc\_and}) &
\label{eqcs}
\slrule {A_1 = A } {\smile A_1 = \smile A } (\ttdef{eqc\_conv}) 
\end{tabular}
\end{center}

Alternatively, any given instance of this result could be proved 
with the help of the tactic \ttdef{idf\_tac}, described in \S\ref{otm}.
Details are given in \cite{thesis}.
\comment{
A proof would have the form shown below,
where `\ddag' denotes a number of sequents 
of the form $A \vdash A$, and where `=' denotes either
(\texttt{eqD1}) or (\texttt{eqD2}).
\vpf
\begin{center} \small
\bpf
\A "$A = B $"
\U "$B \vdash A $" "="%"(\texttt{eqD2})" 
\A "\ddag"
\B "$C[B] \vdash C[A]$" "(\texttt{idf\_tac})"
\A "$C[A] = D$"
\U "$C[A] \vdash D$" "="%"(\texttt{eqD1})"
\B "$C[B] \vdash D$" "(cut)"

\A "$C[A] = D$"
\U "$D \vdash C[A] $" "="%"(\texttt{eqD2})" 
\A "$A = B $"
\U "$A \vdash B $" "="%"(\texttt{eqD1})" 
\A "\ddag"
\B "$C[A] \vdash C[B] $" "(\texttt{idf\_tac})"
\B "$D \vdash C[B]$" "(cut)"

\B "$C[B]=D$" "(\texttt{eqI})"
\epf
\end{center}

Note that, by the cut-elimination theorem, this could be converted to a proof
which does not use the cut rule.
In fact, in \cite{thesis}, the procedure for transforming a proof to one not
using the cut rule was automated.
}

\renewcommand\cfile{}