\renewcommand\cfile{raisa.tex}

\section{Implementation in Isabelle} \label{impl}
The syntax of \dRA\ has been implemented in Isabelle.
The source files are presently available at
\verb|http://arp.anu.edu.au:80/~jeremy/files|,
and further details may be found in \cite{thesis}.
The syntax distinguishes structure and formula variables;
externally, at the user level, a structure variable is preceded by `\verb:$:'.
% Doing this in Isabelle is quite complex, and the method used was taken 
The method used for this was taken directly 
from the Isabelle theory \texttt{LK} (\cite{OL}, Ch 6).

The \dRA\ rules have been implemented in Isabelle.
%The \dRA\ name of the rule using symbols is given on the left
%in the figures, and
%the Isabelle name is given on the right (in a few cases the 
%Isabelle rule is not quite the same).
%It was noted that some rules of \dRA\ can be derived from others, and the
%Isabelle implementation reflects this; 
%some of them %(indicated by \dag\ in Figures \ref{fig:dps} to \ref{fig:lir})
%are derived rather than being specified in the theory file.
%However, no effort was made to find a minimal set of rules.
Some particularly useful derived rules are shown in \fig{sdr}.
%Most are derived \insrc{RS.ML}.
It will be noticed that the two unary structural operators commute, and 
both distribute (in a sense) over both the binary structural operators.
These distributive rules are used, for example, in \S\ref{gord}.
Further, there is a one-directional distributive rule for `;' over `,'.
The rules \texttt{blcEa} and \texttt{blcEs}, in particular, are elegant results
which are much easier to prove for the case of a proper relation algebra.

% SELECTED DERIVED RULES
\begin{figure}[htbp]
\begin{center}
\begin{tabular}{c@{\hspace{15mm}}c}
 \multicolumn 2 c {
 \invrule { X \vdash **Y } { X \vdash Y } (\ttdef{rssS}) \quad 
 \invrule { X \vdash Y } { *Y \vdash *X } (\ttdef{dcp}) \quad
 \invrule { X \vdash \bullet \bullet Y } { X \vdash Y } (\ttdef{rbbS}) \quad
 \invrule { X \vdash Y } { \bullet X \vdash \bullet Y } (\ttdef{blbl}) 
 } \\[4.0ex]
  \invrule {*(X,Y) \vdash Z } { *Y, *X \vdash Z } (\ttdef{stcdista}) & 
 %\invrule {X \vdash *(Y,Z) } { X \vdash *Z, *Y } (\ttdef{stcdists}) \\[4.0ex]

\invrule {* (X; Y) \vdash Z} {* X; * Y \vdash Z} (\ttdef{stscdista}) \\[4.0ex]
%\invrule {Z \vdash * (X; Y)} {Z \vdash * X; * Y} (\ttdef{stscdists}) \\[4.0ex]
\invrule {\bullet  (X; Y) \vdash Z} {\bullet  Y; \bullet  X \vdash Z}
(\ttdef{blscdista}) &
%\invrule {Z \vdash \bullet  (X; Y)} {Z \vdash \bullet  Y; \bullet  X}
%(\ttdef{blscdists}) \\[4.0ex]

\invrule {(\bullet X, \bullet Y) \vdash Z} {\bullet (X, Y) \vdash Z}
(\ttdef{blcdista}) \\[4.0ex]
%\invrule {X \vdash \bullet Y, \bullet Z} {X \vdash \bullet (Y, Z)}
%(\ttdef{blcdists}) \\[4.0ex]

\slrule {(X; Y), (X; Z) \vdash W} {X; (Y, Z) \vdash W}
(\ttdef{sccldista}) &
%\slrule {W \vdash (X; Y), (X; Z)} {W \vdash X; (Y, Z)}
%(\ttdef{sccldists}) \\[4.0ex]
\slrule {(X; Z), (Y; Z) \vdash W} {(X, Y); Z \vdash W}
(\ttdef{sccrdista}) \\[4.0ex]
%\slrule {W \vdash (X; Z), (Y; Z)} {W \vdash (X, Y); Z}
%(\ttdef{sccrdists}) \\[4.0ex]

 \multicolumn 2 c {
\invrule {X ; Y \vdash Z }{\bullet Y ; \bullet X \vdash \bullet Z }
(\ttdef{tagae}) \quad
%\invrule {Z \vdash X ; Y }{\bullet Z \vdash \bullet Y ; \bullet X }
%(\ttdef{tagse}) \\[4.0ex]
\invrule {\bullet * X \vdash Y } { * \bullet X \vdash Y} (\ttdef{bsA}) \quad
%\invrule {X \vdash \bullet * Y } {X \vdash  * \bullet Y } (\ttdef{bsS})
%\\[4.0ex]

\invrule{E \vdash X}{* E \vdash X} (\ttdef{sEa}) \quad
%\invrule{X \vdash E }{X \vdash * E } (\ttdef{sEs})\\[4.0ex]
\invrule{I \vdash X}{* I \vdash X} (\ttdef{sIa}) } \\[4.0ex]
%\invrule{X \vdash I }{X \vdash * I } (\ttdef{sIs})\\[4.0ex]

\invrule { \bullet X, E \vdash Y} {X, E \vdash Y } (\ttdef{blcEa}) &
\invrule {Y \vdash \bullet X, E} {Y \vdash X, E} (\ttdef{blcEs}) \\[4.0ex]

 \slrule {A \vdash X \quad B \vdash X }
  {A \lor B \vdash X } (\ttdef{orA}) &
 \slrule {X \vdash A \quad X \vdash B}
  {X \vdash A \land B} (\ttdef{andS}) 
\end{tabular}
\end{center}
\caption{Selected Derived Rules}
\label{fig:sdr}
\end{figure}

Of the \dRA\ logical introduction rules,
some can be applied always (in a backwards proof)
when the relevant formula is displayed.
Others, namely
($\vdash \land $), ($\lor \vdash $),
($\vdash \circ $) and ($+ \vdash $),
are subject to the ``constraint'' that the structure on the 
other side of $\vdash$ be of a particular form.
The rules \texttt{andS} and \texttt{orA} % , which are derived \insrc{dRA.ML},
are equivalent to ($\vdash \land $) and ($\lor \vdash $).
%Unlike ($\vdash \land $) and ($\lor \vdash $), 
\texttt{andS} and \texttt{orA} can be applied always %(in a backwards proof)
when the relevant formula is displayed.
Unfortunately the introduction rules for `$\circ$' and `$+$' have no such
equivalents.
Thus the introduction of `$\circ$' on the right of $\vdash$ 
is always subject to the ``constraint'' that the structure
on the left of $\vdash$ be of a particular form;
similarly for introducing `$+$' on the left.

As in classical sequent calculus, the \emph{modus operandi}
for proving a sequent is to start the proof from the bottom, ie,
from the goal, and work ``backwards''.
%in terms of the written representation of proofs, that means
%working upwards.
The first step is, where possible, to remove
all the formula (logical) operators, 
using the logical introduction rules.
In Display Logic (unlike classical sequent calculus)
this requires that the formula which is to be ``broken up''
must first be displayed.
As any formula can be displayed,
this is not a difficulty, except in that it is tedious to
select display postulates one-by-one.
The tactics described in the next two subsections were 
first written to help in this style of proof.

\comment{
Note that many of these functions
have arguments and can be considered as
having return values of type \verb:int -> tactic:.
We define a \bfi{sg-tactic}\label{sg-tactic}
as a function of type \verb:int -> tactic:
which, where the argument is a subgoal number,
returns a tactic which affects only that subgoal.
(Thus, for example, \verb:rtac: \textit{th} is an sg-tactic).
We can think of an sg-tactic as an operation which transforms subgoals
(noting that it can produce any number of subgoals from a given one).
Many of the functions we describe can be thought of as transformations
of sg-tactics.
}

\subsection{Display Tactics}
%A Display Logic proof typically proceeds by displaying a particular subterm,
%simplifying it or manipulating it in some way, then displaying another
%subterm, and so on.
The functions described below
were written to help in the process of displaying a chosen substructure.
%These tactics are found in the file \verb:RS.tac:.
\begin{description}
\item[\texttt{disp\_tac : string -> int -> tactic}]\tti{disp\_tac}
\label{disp_tac} 
replaces a subgoal by one in which a selected
structure is displayed. 
The structure selected is indicated by a string argument, of which
the first character is 
`\verb:|:' or `\verb:-:',
to indicate the left or right side of the turnstile.
Remaining characters are 
\begin{itemize}
\item[] `\verb:l:' or `\verb:r:',
to indicate the left or right operand of the `,' operator
\item[] `\verb:L:' or `\verb:R:',
to indicate the left or right operand of the `;' operator
\item[] `\verb:*:' or `\verb:@:',
to indicate the operand of the `$*$' or the `$\bullet$' operator
\end{itemize}
For example, in the (sub)goal 
$R \vdash ((* T; \bullet * S), \bullet * Q); Y$ 
the string \verb:"-L": denotes the sub-structure 
$((* T; \bullet * S), \bullet * Q)$.
Thus \verb:disp_tac "-L": performs the first (bottom) step
of the proof example shown below.

\item[\texttt{fdisp : string -> thm -> thm}]\tti{fdisp}
is the corresponding function for forward proof, displaying the selected part
of the conclusion of the given theorem.

\item[\texttt{d\_b\_tac : string -> (int -> tactic) -> int -> tactic}]
\tti{d\_b\_tac} \mbox{}\\
\verb:d_b_tac: \textit{str tacfn sg}
takes subgoal \textit{sg}, 
displays the part selected by \textit{str} (as for \verb:disp_tac:)
and applies \textit{tacfn} to the transformed subgoal.
It then applies the reverse of the display steps to each resulting subgoal.
This requires that the subgoals produced by \textit{tacfn}
are in a suitable form to permit the display steps used to be reversed.
This will be the case if \textit{tacfn}
only affects the displayed sub-structure,
and leaves the rest of the sequent alone.
This was the purpose of deriving the rules 
\texttt{andS} and \texttt{orA} (which satisfy this requirement) from
\texttt{ands} and \texttt{ora} (which do not).

For example, if we start with the subgoal
$R \vdash ((* T; \bullet * S), \bullet * Q); Y$ then 
\verb:d_b_tac "-L" (rtac mrs):
applies the monotonicity rule ($\vdash M$) (\texttt{mrs}) to 
the sub-structure $(* T; \bullet * S), \bullet * Q$
by the following steps (read upwards)
\vpf
\begin{center}
\bpf
\A "$R \vdash (* T; \bullet * S); Y$"
\U "$R ; * \bullet Y \vdash * T; \bullet * S$" 
  "(reverse of \texttt{disp\_tac "-L"})"
\U "$R ; * \bullet Y \vdash (* T; \bullet * S), \bullet * Q$" "(\texttt{mrs})"
\U "$R \vdash ((* T; \bullet * S), \bullet * Q); Y$" 
  "(\texttt{disp\_tac "-L"})"
\epf
\end{center}
%displays the sub-structure $(* T; \bullet * S), \bullet * Q$
%to give 
%$R ; * \bullet Y \vdash (* T; \bullet * S), \bullet * Q$,
%applies the monotonicity rule ($\vdash M$) to give
%$R ; * \bullet Y \vdash * T; \bullet * S$,
%and reverses the display operation to
%give the new subgoal
%$R \vdash (* T; \bullet * S); Y$.

\comment{
The implementation of \verb:d_b_tac:
used a tactical \verb:THENEXP: 
corresponding to 
the HOL tactical \texttt{THEN} (\cite{HOLdesc}, \S14.4.4),
and to the tactical
\ttdef{THEN\_ALL\_NEW\_SUBGOALS}
as described by Easthaughffe et al in \cite{dove}, p.~378.
It applies one tactic to a given subgoal, then
a second tactic to each resulting subgoal.
}

\item[\texttt{fdispfun : string -> (thm -> thm) -> thm -> thm}]\tti{fdispfun}
\mbox{} \\
is a corresponding operation for forward proof.
\verb:fdispfun: \textit{str thfn th} displays the part of 
theorem \textit{th} indicated by string \textit{str}, applies
transformation \textit{thfn} to the result, then reverses the display
steps used.

\end{description}

\subsection{Search-and-Replace Tactics} \label{srtac}
Tactics were written to display all structures in a sequent in turn, 
and apply any appropriate transformations (selected from a given set)
to the structure.
These can be used to rewrite all substructures of
a particular form, for example, to rewrite all occurrences of 
``$X,(Y,Z)$'' to ``$(X,Y),Z$''.

\begin{description}
\item[\texttt{glob\_tac :}]\tti{glob\_tac}\mbox{} \\
\mbox{\textbf{\texttt{(term -> int -> (int -> tactic) list) -> int -> tactic}}}
\\
The first argument of \texttt{glob\_tac} is a function
\textit{actfn}\label{actfnbwd},
which is called as \textit{actfn tm asp}, where
\textit{tm} is a subterm, and \textit{asp} has the value 0 or 1
to indicate that \textit{tm} is displayed as
the antecedent or succedent part of a sequent.
\textit{actfn tm asp}
should return either \verb:[]: or \verb:[:\textit{tacf}\verb:]:,
where,
%\textit{tacf} is an sg-tactic, ie
when \textit{sg} is a subgoal number,
\textit{tacf sg} is a tactic.
When \textit{tm} is displayed as the
antecedent (if $\textit{asp} = 0$) or succedent (if $\textit{asp} = 1$),
\textit{tacf} should be a tactic which changes only \textit{tm}.

Then \texttt{glob\_tac} \textit{actfn sg}
displays in turn every subterm of subgoal \textit{sg}, and
applies the tactic, if any, given by \textit{actfn tm asp},
(where \textit{tm} is the subterm displayed
%, as antecedent if $\textit{asp} = 0$ or succedent if $\textit{asp} = 1$)
on the side indicated by \textit{asp})
to the sequent thus produced. 
All the display steps are eventually reversed,
in the same way as for \verb:d_b_tac:.

\texttt{glob\_tac} uses a top-down strategy in that 
it first tests the whole structure with the function \textit{actfn},
then, recursively, each sub-structure.
\comment{
(Note that although elsewhere we refer to the ``top'' or ``bottom''
of a proof tree,
in this context we are using ``top-down'' and ``bottom-up'' 
to describe the order in which we examine all sub-terms of a term;
``top-down'' means that we look at a term before its sub-terms,
whereas ``bottom-up'' means that we look at the sub-terms of a term
before the term).
}
If \textit{actfn} returns a tactic function
(ie, not the empty list)
then the changed structure is tested again.
%(thus \texttt{glob\_tac} will loop infinitely if 
%\textit{actfn} returns \verb:[:\textit{tacf}\verb:]:
%such that \textit{tacf} leaves the subgoal unchanged).

\item[\ttdef{bup\_tac}] is like \texttt{glob\_tac}, but uses a
bottom-up strategy, displaying and testing the smallest sub-structures first.
% Like \texttt{glob\_tac}, it will retest a (possibly) changed sub-structure
% after \verb:[:\textit{tacf}\verb:]: is applied.

\item[\texttt{fgl\_fun, fbl\_fun :}]\tti{fgl\_fun}\tti{fbl\_fun}\mbox{} \\
\mbox{\textbf{\texttt{(term -> int -> (thm -> thm) list) -> thm -> thm}}} \\
These functions are like \texttt{glob\_tac} and \texttt{bup\_tac},
but for doing forward proof.

Their first argument is again a function \textit{actfn}\label{actfnfwd},
called as \textit{actfn tm asp}.
% where \textit{tm} is a subterm, and \textit{asp} has the value 0 or 1
% to indicate that \textit{tm} is displayed as
% the antecedent or succedent part of a sequent.
Here \textit{actfn tm asp}
should return either \verb:[]: or \verb:[:\textit{thtr}\verb:]:,
where
\textit{thtr} is a theorem transformation, ie a function of type
\verb:thm -> thm:,
which changes only the term \textit{tm} displayed on the side indicated by
\textit{asp}.
\comment{
When \textit{tm} is displayed as the
antecedent (if $\textit{asp} = 0$) or succedent (if $\textit{asp} = 1$)
of the conclusion of a theorem \textit{th},
\textit{thtr th} should be a theorem which differs from \textit{th}
only in that \textit{tm} has been changed.

Then \texttt{fgl\_fun} \textit{actfn th}
displays every sub-structure of the conclusion of \textit{th}
and tests it with \textit{actfn};
if \textit{actfn} returns a theorem transformation
then it is applied.
The strategy is top-down, as for \texttt{glob\_tac}, with 
every transformed sub-structure retested.
    
\texttt{fbl\_fun} does the same, but using a bottom-up strategy.
Again, a (possibly) changed sub-structure will be retested
after \verb:[:\textit{thtr}\verb:]: is applied.
}

\end{description}

%\subsection{Implementation of the Search-and-Replace Tactics}
\label{srimp}
%We now discuss the implementation of the search-and-replace tactics.

The first implementation of these tactics and functions was described in
\cite{thesis}, \S2.5.3.
A later implementation gives the user great flexibility in 
programming the search strategy,
enabling him/her to specify (for example)
whether to traverse the
structure top-down or bottom-up, 
whether or not to attempt further changes to a rewritten substructure,
whether or not to repeat the whole procedure when any substructure is
rewritten,
etc.
This implementation is described in \cite[\S4.4]{rewr}.

\comment{ following was sent to CADE 
A function \texttt{travdown},
used for both forwards and backwards proof,
takes a ``search strategy'' \textit{strat}
and returns the strategy which applies \textit{strat}
to the immediate subterms of a given term.
For each immediate subterm in turn,
this (result) strategy
displays it, applies \textit{strat} to it, and then reverses the display step.
\texttt{travdown} is then
used to program the recursive top-down or bottom-up strategies,
which display and apply \textit{actfn} to every subterm in the sequent.
For full details of \texttt{travdown}, and ``strategies'', and their 
types, see \cite{thesis}, \S2.5.3.

These functions are then used for both backward and forward proof,
by supplying appropriate arguments which give
the methods for applying a display postulate, combining two transformations
of a term, and so on.
Firstly, for backward proof, the term is a subgoal, and the
transformation consists of applying a tactic to the term, to
produce a number of new subgoals.
Secondly, for forward proof, the term is the conclusion of the 
theorem generated so far, and its transformation results in a new theorem.
%
%The method is to display every subterm in the appropriate order
%(for the top-down or bottom-up strategy) and apply any transformation
%given by \textit{actfn}.
%Arguments to \texttt{travdown} and \texttt{globfns} give the
%methods for applying a display postulate, combining two transformations
%of a term, and so on.
Full details are given in \cite{thesis}.

There is an alternative implementation for the top-down search strategy only.
The term is traversed, but the appropriate
display postulates are applied only when 
it is useful to do so, that is, until a subterm is found of a form
which, when displayed, would in fact get transformed by \textit{actfn}.
This contrasts with the first implementation where
often a sequence of 
display postulates would be applied, and then its inverse applied, without
anything else happening in between.
In this second implementation, a list of display postulates
is kept, to be applied when needed.
These display postulates will then be applied to display a sub-structure
when it is seen that that sub-structure, if displayed, could be transformed.
}


\subsection{Application of the Search-and-Replace Tactics}
\label{srapp}
We now describe some uses of the search-and-replace tactics.
Provided the function \textit{actfn}, as described in
\S\ref{srtac}, returns an action which changes only the displayed subterm
\textit{tm},
these tactics perform local ``rewrites'' on subexpressions.
%These require programming a function \textit{actfn}, as described in
%\S\ref{srtac}.
%Recall that \textit{actfn tm asp} tests whether to perform
%an action on a sequent which has \textit{tm} displayed on the side indicated by
%\textit{asp};
%it returns either \verb:[]: or \verb:[:\textit{action}\verb:]:.
%In practice, the action performed on the sequent will change only
%\textit{tm}, leaving the other side of the sequent unchanged;
%thus these tactics are used to perform local ``rewrites'' on subexpressions.

Examples of the use of these tactics are
(1)
to eliminate 
$**$ and $\bullet \bullet$,
(2)
to use the various derived distributive laws to
push $*$ and $\bullet$ down, and
(3)
to eliminate logical operators, where possible,
using a set of logical introduction rules 
including \texttt{andS} and \texttt{orA} (see \fig{sdr}) --
this is only for backward proof. 

\comment{
Examples of the use of these tactics are
%{(see source files \texttt{pat.tac} and \texttt{dRA.tac})}
\begin{itemize} \shrinklist{0.5}
\item[--] to eliminate 
$**$ and $\bullet \bullet$ 
%(\verb:pr_dbl:, \verb:fpr_dbl:)
\item[--] to use the various derived distributive laws to
push $*$ and $\bullet$ down
%(\verb:pr_dist:, \verb:fpr_dist:)
\item[--] to eliminate logical operators, where possible,
using a set of logical introduction rules 
%satisfying the property mentioned in \S\ref{decproc} below
including \texttt{andS} and \texttt{orA} (see \fig{sdr}) --
this is only for backward proof. 
%(Many moves in a typical Display Logic proof
%involve replacing connectives by corresponding structural operators.)
\end{itemize} 
}
As these examples illustrate, we can achieve the power of a procedure
which rewrites using equalities or equivalences, such as
\texttt{rewrite\_tac} and \texttt{rewrite\_rule} in Isabelle and
\texttt{REWRITE\_TAC} and \texttt{REWRITE\_RULE} in HOL,
even though the \dRA\
formalization does not contain any general rewriting facility.
However \dRA\ requires more than simple rewriting due to the 
logical introduction rules with ``constraints''.

The fact that \texttt{pr\_intr} is available only for backward proof illustrates
that these tactics can be used with
uni-directional rules,
such as the logical introduction rules,
as well as with bi-directional rules.
This useful aspect of the tactics
contrasts with the more typical rewriting tactics, such as 
in Isabelle and HOL,
%\texttt{rewrite\_tac} and \texttt{rewrite\_rule} in Isabelle, and
%\texttt{REWRITE\_TAC} and \texttt{REWRITE\_RULE} in HOL,
where the rules used to rewrite an expression \emph{must} be equalities.

In \cite{dRA}, \S4,
a function $\tau$ which translates structures to formulae --
for example, to convert
$B ; \bullet A \vdash \bullet D , * C$ to
$B \circ \smile A \vdash \smile D \lor \neg C$ --
is crucial in the proof of soundness of \dRA. 
%Another example is to
%convert a theorem in structural form to one in logical form,
%for example, from
Its implementation in a forward proof
is another example of the use of a search-and-replace function.
For this we can use some of the logical introduction rules,
in their original form (as given in \cite{dRA}),
using \texttt{fbl\_fun}.
%The transformation \ttdef{s2l}, defined as
%\tti{fpr\_tau}\texttt{fbl\_fun (ffpr fpr\_tau)}
%does this conversion.
Note that this must be done bottom up,
%(using \texttt{fbl\_fun}),
ie, on the smallest sub-structures first,
because only at the bottom are the sub-structures also formulae.
%also all the variables must be formula
%variables, not structure variables.
%This transformation implements the function $\tau$\index{tau@$\tau$|textbf},
%as defined in \cite{dRA}, \S4.

%\newpage
\subsection{Other Tactics and Methods} \label{otm}
\paragraph{idf\_tac} \label{idf_tac}
In the identity rule
(id) $p \vdash p$,
$p$ stands for a primitive proposition,
not an arbitrary formula.
It is, however, true that $A \vdash A$ for any formula $A$;
this is proved by induction (see \cite{dRA}, Lemma 2).
The restriction to primitive propositions
is not reflected in the Isabelle implementation,
which contains the rule $A \vdash A$, %called \ttdef{idf},
where $A$ is a variable standing for any formula.
However the tactic \ttdef{idf\_tac}
will convert an identity subgoal such as
$q \circ (\smile p \lor \neg r) \vdash
q \circ (\smile p \lor \neg r)$
into three separate subgoals
$ \quad q \vdash q \quad p \vdash p \quad r \vdash r $ .
The tactic can therefore provide a proof, from the rule
$p \vdash p$,
of any given instance
of the general theorem (which is provable only by induction)
that $A \vdash A$ for any formula $A$.

This tactic uses a set of six derived results
(one for each logical operator, of which two examples are shown).
\begin{center} 
\begin{tabular}{c@{\qquad}c}
\slrule {A_1 \vdash A \quad B_1 \vdash B} {A_1 \circ B_1 \vdash A \circ B} 
(\ttdef{cong\_comp}) &
\slrule {A \vdash A_1 } {\lnot A_1 \vdash \lnot A }
(\ttdef{cong\_not}) 
\label{congs}
\end{tabular}
\end{center}

\paragraph{Structural operators from logical ones}

It is also possible to implement the function $\tau$\index{tau@$\tau$}
in a backwards proof.
We can ``create'' logical connectives  
(as we read a proof upwards);
this can on occasions help in managing a complex proof.
%(though it is never \emph{necessary} in proving a sequent which is a tautology
%since it must use the (cut) rule, and we know (cut) is eliminable
%-- see Chapter~\ref{ch:cut}).
The tactic \ttdef{tau\_tac} does this. 
It uses variants of the logical introduction rules  
where all the premises are 
``structure-free'' and ``connective-free'', ie
of the form $A \vdash X$ or $X \vdash A$.
Structural or logical operators appear only in their conclusions.
%These rules are listed in \ttdef{tau\_thms}.

The inverse of $\tau$\index{tau@$\tau$} is implemented for forward proof. 
%\ttdef{l2s}, defined as 
%\tti{fpr\_inv\_tau}\texttt{fgl\_fun (ffpr fpr\_inv\_tau)} \seesrc{dRA.tac}.
This use of the search-and-replace method can only be done top down
(using \texttt{fgl\_fun}), and it uses the cut rule.
Not all formula operators will necessarily be changed to structural ones: for
example, 
`$\circ$' or `$\land$' in a succedent position and
`$+$' or `$\lor$' in an antecedent position cannot be converted to structural
operators.

\paragraph{Flipping theorems}\label{flip}

It may be observed in Fig.~1 of \cite{dRA} that many of the rules
in the two columns are symmetric about the turnstile, for example
\begin{center}
($A; \vdash$)\invrule
{X;(Y;Z) \vdash W} {(X;Y);Z \vdash W} (\ttdef{arA}) \qquad
($\vdash A;$)\invrule
{W \vdash X;(Y;Z) } {W \vdash (X;Y);Z } (\ttdef{arS})
\end{center}
In fact most rules in the right-hand column of that figure
could be derived from the corresponding rules in the
left-hand column by ``flipping'' them about the turnstile,
ie, interchanging the parts before and after $\vdash$ .
Likewise, ``flipped'' versions were derived for
those rules in \fig{sdr} which use only structural operators.
The procedure for doing this has been formalized in 
the theorem transformation functions
\texttt{flip\_st\_p} and \texttt{flip\_st\_c}, of type \texttt{thm -> thm}.
These use the theorem \verb:dcp: (see \fig{sdr})
to swap the sides of each sequent (by putting a $*$ in front of each side),
use the distributive laws to push the $*$ down as far as possible,
and rename variables to absorb the $*$.
The transformations require the rules to be in structural form 
(see \S\ref{thpr} below).
This applies generally in display logics -- having proved one theorem or rule
in structural form, you then get one ``free'', with each part moved to the
other side of the turnstile.
%Unfortunately they are not very ``robust'', and
%Some forms of theorem causes these transformations to fail, 
%or to produce a result different from that intended;
%in particular, they don't work when the identities $I$ and $E$ are present.
%sometimes
%\texttt{flip\_st\_p} (which works on the premises first) and
%\texttt{flip\_st\_c} (which works on the conclusion first) 
%behave differently.
%Useful further work would include investigating these problems
%and finding a simple fix.
The theorem transformations
\texttt{flip\_bl\_p} and \texttt{flip\_bl\_c}
do the same thing, but with $\bullet$ instead of $*$.
These transform a theorem to a corresponding one in terms of the
converse relations.
%These functions are found \insrc{flip.tac}.

\paragraph{Automated cut-elimination} \label{cutelim}

\comment{
  During proof construction, the rules used are stored in
  the nodes of a tree using an appropriate ML datatype. Given the
  original sequent, we can thus reproduce the original proof.
  (A derivation of a sequent could also be attempted by applying
  the same rules until/unless some rule application fails).
  
}
% Functions were written to represent a proof tree as an ML structure, 
% and then to apply the procedure of Belnap's cut-elimination theorem
% for Display Logic \cite{Bel} to eliminate uses of the cut rule from the proof.
% This enables a proof composed from previously proved lemmata
% (using the cut rule) 
% to be converted to a cut-free proof.
% A sketch of how the cut-elimination
% procedure works can be found in \cite[Appendix]{dRA}.
Belnap's original proof of cut-elimination is operational; see the
proof sketch in \cite[Appendix]{dRA}.
%Its implementation involved the following steps
It was implemented as follows.
\begin{itemize}
\item
The rules used in a proof are stored in
the nodes of a tree using an appropriate ML datatype,
where each node represents a single proof step.
Thus, given the original sequent, we can reproduce the original proof.
% (A derivation of a similar sequent could also be attempted by applying
% the same rules until/unless some rule application fails).
%An ML datatype was declared to represent a proof
%as a tree,
%whose nodes are the proof steps, and the value stored at a node 
%is the rule used in the corresponding proof step.
\item Functions were written in ML to turn an Isabelle proof, using the various
compound tactics described in \S\ref{srtac},
into a proof consisting of single steps, and then to represent that proof
as a tree, as above.
\item
%Functions were written to rearrange the steps of the proof tree
%so as to push a cut upwards as far as possible, 
%ie until both premises of that cut are sequents
%in which the cut-formula is first introduced (either by an introduction rule
%or by the axiom $p \vdash p$).
Functions were written to allow us to rearrange the nodes of such
proof trees to push a cut upwards until the cut-formula becomes
principal in both premises of that cut (either due to an introduction
rule or an axiom $p \vdash p$).
\item
% Such a cut is converted to cuts on smaller formulae.
Such a cut is either eliminated completely or is
converted to cuts on smaller formulae using a look-up table that
gives a recipe of how to do so for each logical connective. Display
logic gurantees that such a recipe always exists.
%This uses a table giving, for each logical operator
%(eg $\land$), the section of proof tree needed 
%to convert a cut with cut-formula $A \land B$ to a proof containing cuts
%on $A$ and $B$.
\item This procedure 
is applied recursively to remove all cuts from the proof tree.
\end{itemize}
Full details are given in \cite[Ch. 5]{thesis}.

One novel use of this procedure would be to convert each proof of
Chin and Tarski \cite{CT} into a \dRA\ proof as follows. Simply begin to
convert the proof by following the text. Sooner or later, the text
``stores'' the current reasoning as a lemma. At this point, we let
the converted text constitute a premise of cut. We then continue
to convert the text, until the lemma is used. At this point we
insert a cut in the converted proof. 
Now applying the automated cut-elimination procedure
will give a new, purely cut-free proof. Often, this proof is
shorter, although, in general, it will be exponentially longer.

\renewcommand\cfile{}