\newcommand \pair[2] {\texttt{(}\textit{#1}\texttt{,}\textit{#2}\texttt{)}}

As noted previously,
the cut-elimination theorem of sequent calculi (which 
says that if a sequent is provable, it is provable without using the cut rule)
applies in all
Display Logics, provided that the rules satisfy certain conditions, which are
relatively easily checked (\cite{Bel}).
In a backwards proof search, use of the cut rule involves guessing
the arbitrary formula $A$; this is a disadvantage in doing automated proof,
as there will be infinitely many possibilities that may be chosen as $A$.
The cut rule is the only rule with this property;
in all the other rules, every variable appearing in a premise also 
appears in the conclusion.
Therefore, knowing that the cut rule can be avoided 
means that, in searching for a backward proof,
at each stage there is only a finite number of possible next steps.

However, proofs using (cut) can often be easier to construct, and 
(cut) is necessary to make use of previously proved lemmata.

The construction described in this chapter 
eliminates the uses of (cut) from a \dRA\ proof,
converting a proof using (cut) to one not using (cut).
This provides a demonstration of the procedure 
used in the proof of the cut-elimination theorem.
It also allows a user to construct proofs using (cut),
knowing that a cut-free proof can be obtained automatically if desired.

We give a small example of proofs with and without (cut).
A larger example, which illustrates more aspects of the procedure, is in
Appendix~\ref{app:cut}.
\vpf
\begin{center}
\bpf
\A "$ A \vdash A $" 
\U "$ A, B \vdash A $" "($M \vdash $)"
\U "$ (A \land B) \vdash A $" "($\land \vdash $)"

\A "$ A \vdash A $" 
\U "$ A \vdash A, C $" "($\vdash M $)"
\U "$ A \vdash (A \lor C) $" "($\vdash \lor $)"

\B [2.0em] "$ A \land B \vdash A \lor C $" "(cut)"
\epf
\hfill
\bpf
\A "$ A \vdash A $" 
\U "$ A \vdash A, C $" "($\vdash M $)"
\U "$ A \vdash A \lor C $" "($\vdash \lor $)"
\U "$ A, B \vdash A \lor C $" "($M \vdash $)"
\U "$ A \land B \vdash A \lor C $" "($\land \vdash $)"
\epf
\end{center}

\subsubsection{Description of the cut-elimination procedure}

First we outline the cut-elimination procedure in Display Logics.
This procedure applies in all Display Logics satisfying Belnap's conditions
(C1) to (C8) (see \cite{Bel}).
The rules of \dRA\ are known to satisfy (C1) to (C8), see \cite{dRA}.
For each cut such as
\vpf
\begin{center}
\bpf
\A "$ \Pi_l $" 
\U "$ X \vdash A $" 
\A "$ \Pi_r $" 
\U "$ A \vdash Y $" 
\B [1.5em] "$ X \vdash Y $" "(cut)"
\epf
\end{center}
there are various possibilities, according to the points
where the cut-formula $A$ first appears in the proofs $\Pi_l$ and $\Pi_r$
(recall that we think of a proof as proceeding downwards).
If $A$ is introduced
in both $X \vdash A$ and $A \vdash Y$, then condition (C8) of \cite{Bel}
ensures that the cut can be replaced by cut(s) on smaller formulae
(which are sub-formulae of $A$).
Alternatively, if either $X$ or $Y$ is $A$ then the cut can simply be deleted.

An example of this is given in \fig{C8}. 
In this example, $A$ is $B \land C$.
%There is an example like this for each of the logical operators.

\begin{figure}[htbp]
\begin{center}
\vpf
\bpf
\A "$U \vdash B$"
\A "$V \vdash C$"
\B "$U,V \vdash B \land C$" "($\vdash \land $)"
\A "$B,C \vdash W$"
\U "$B \land C \vdash W$" "($\land \vdash $)"
\B "$U,V \vdash W$" "(cut)"
\epf

\bpf
\A "$V \vdash C$"
\A "$U \vdash B$"
\A "$B,C \vdash W$"
\U "$B \vdash W,*C$" "(dp)"
\B "$U \vdash W,*C$" "(cut)"
\U "$C \vdash *U,W$" "(dp)"
\B "$V \vdash *U,W$" "(cut)"
\U "$U,V \vdash W$" "(dp)"
\epf
\end{center}
\caption{Example of converting cut to cuts on smaller formulae}
\label{fig:C8}
\end{figure}

In the general case, $A$ is introduced further up in
$\Pi_l$ and $\Pi_r$.
Belnap's conditions ensure that at the point where $A$ is introduced in the
branch above $X \vdash A$, it occupies the whole of the succedent part of the
sequent.
Likewise 
at the point where $A$ is introduced in the
branch above $A \vdash Y$, it occupies the whole of the antecedent part of that
sequent.
Note that we are only interested in the occurrences of $A$ 
which correspond to the occurrences of $A$ as the cut-formula, 
as seen in the diagram.
That is, we will
ignore any occurrences of $A$ in
$X$ or $Y$ and higher occurrences traceable to those.
We thus have the situation shown in \fig{cut123}(a),
where $A$ is introduced at $ Z \vdash A $ and at $A \vdash W $.

\begin{figure}[htbp]
\vpf
\begin{center}
\bpf
\A "$\vdots$"
\U "$ Z \vdash A $" 
\U "$\vdots$"
\U "$ X \vdash A $" 
\A "$\vdots$"
\U "$ A \vdash W $" 
\U "$\vdots$"
\U "$ A \vdash Y $" 
\B [1.5em] "$ X \vdash Y $" "(cut)"
\U ['] ""
\U ['] "(a)"
\epf
\hfill
\bpf
\A "$\vdots$"
\U "$ Z \vdash A $" 
\A "$\vdots$"
\U "$ A \vdash W $" 
\U "$\vdots$"
\U "$ A \vdash Y $" 
\B [1.5em] "$ Z \vdash Y $" "(cut)"
\U "$\vdots$"
\U "$ X \vdash Y $" 
\U ['] ""
\U ['] "(b)"
\epf
\hfill
\bpf
\A "$\vdots$"
\U "$ Z \vdash A $" 
\A "$\vdots$"
\U "$ A \vdash W $" 
\B [1.5em] "$ Z \vdash W $" "(cut)"
\U "$\vdots$"
\U "$ Z \vdash Y $" 
\U "$\vdots$"
\U "$ X \vdash Y $" 
\U ['] ""
\U ['] "(c)"
\epf
\end{center}
\vspace{-1.0ex}
\caption{ Stages in the cut-elimination procedure\qquad}
\vspace{-0.0ex}
\qquad \qquad \qquad 
\begin{tabular}{l}
(a) Original proof tree, before moving cut on $A$  \\
(b) Intermediate stage  \\
(c) Proof tree with cut on $A$ moved up
\end{tabular}
\label{fig:cut123}
\end{figure}
The procedure then is to replace all the occurrences of $A$,
from $X \vdash A$ up to $Z \vdash A$, by $Y$, and move the cut accordingly,
to give the tree shown in \fig{cut123}(b).
We then replace all the occurrences of $A$,
from $A \vdash Y$ up to $A \vdash W$, by $Z$, and move the cut accordingly,
to give the tree shown in \fig{cut123}(c).
This is now the first case, where $A$ is introduced at the premises of the cut,
which is dealt with by (C8), as described above.

Note that the situation may be considerably more complicated than shown in
\fig{cut123}(a), as there may be several places where $A$ is introduced 
rather than just one on each side ($ Z \vdash A $ and $A \vdash W $)
as shown.
Specifically, as you go up the proof tree from $X \vdash A$,
the tree may branch, as shown in \fig{cutcomp}(b). 

Alternatively, $A$ may occur more than once in a sequent
in a single branch; it is introduced at two places, one above the other.
An example of this scenario is given in \fig{cutcomp}(c). 
Note that $A'$ and $A''$ are both $A$,
the primes just used to distinguish the two occurrences.
There may be irrelevant intermediate steps, which are not indicated.
So the two places where $A$ is introduced are the top and third
(from the top) sequents of \fig{cutcomp}(c). 
\begin{figure}[htbp]
\vpf
\begin{center}
\bpf
\A "$\vdots$"
\U "$ Z \vdash A $" 
\U "$\vdots$"
\U "$ X \vdash A $" 
\U ['] ""
\U ['] "(a)"
\epf
\hfill
\bpf
\A "$\vdots$"
\U "$ Z_1 \vdash A $" 
\U "$\vdots$"
\A "$\vdots$"
\U "$ Z_2 \vdash A $" 
\U "$\vdots$"
\B "$\vdots$"
\U [2.0em] "$ X \vdash A $" 
\U ['] ""
\U ['] "(b)"
\epf
\hfill
\bpf
%\A "$ *V', X \vdash V'' $" 
\A "$\vdots$"
\U "$ *V', X \vdash A'' $" "(intro $A''$)"
\U "$ X, *A'' \vdash V' $" "(dp)"
\U "$ X, *A'' \vdash A' $" "(intro $A'$)"
\U "$ X \vdash A',A'' $" "(dp)"
\U "$ X \vdash A $" "($\vdash C $)" 
\U ['] ""
\U ['] "(c)"
\epf
\end{center}
\vspace{-1.0ex}
\caption{Possible configurations in tracing $A$ upwards}
\label{fig:cutcomp}
\end{figure}

\subsubsection{Structure of proof trees}

To rearrange these proof trees, we need to represent their tree structure in ML.
In our representation of a proof tree, by the datatype \ttdef{rtpt},
the nodes correspond to the 
proof steps (the horizontal
lines in the diagrammatic representation);
the node 
\texttt{Pr(}\textit{th}\texttt{,}\textit{node-list}\texttt{)}
identifies the theorem \textit{th} which justifies that proof step, and
contains a list \textit{node-list}
of the nodes at the next level up.
Where a proof tree is incomplete (ie, there are premises, or leaves,
which are not axioms) there is a node \texttt{Unf} for each unproved premise
of the top-most theorem.
We use as an example the following proof tree,
which gives the proof of
$ A \vdash B \Longrightarrow A \land C \vdash B \land \top $.
Note that of the leaf sequents, 
$ A \vdash B $ is a premise (of the whole proof tree) 
whereas $ I \vdash \top $ is the axiom \texttt{tS}.
\up 4
\begin{center}
\bpf
\A "$ A \vdash B $" 
\A "$ I \vdash \top $" 
\U "$ C \vdash \top $" "(\texttt{exs})"
\B [2em] "$ A, C \vdash B \land \top $" "(\texttt{ands})"
\U "$ A \land C \vdash B \land \top $" "(\texttt{anda})"
\epf
\end{center}
\up 2
Therefore we represent it as
$$
\texttt{Pr (anda, [Pr (ands, [Unf, Pr (exs, [Pr (tS, [])])])])}
$$
Note how, of the leaf sequents of the proof tree as displayed above,
the premise $A \vdash B$ is represented by \texttt{Unf}, while
the axiom $ I \vdash \top $ is represented by \texttt{Pr~(tS,~[])}.

\subsubsection{Recording proof step information}

The construction applies to backwards proofs, where each step uses
the Isabelle ``resolution tactic'', \texttt{rtac}.
To manipulate proof trees in the way needed for the cut-elimination procedure,
we have to record details of each step, namely the theorem and subgoal number
used by \texttt{rtac}.

As we wanted to use as much of the structure of the Isabelle 
subgoal package as possible without alteration,
we defined a new type for a tactic
and related functions.  A ``tactic'' of this new type records the 
theorem and subgoal number for each elementary proof step.
Since an Isabelle tactic can represent several elementary
proof steps or just one,
this would suggest that the type used should involve a list
of (theorem, subgoal-number) pairs.
So as to avoid the need to concatenate lists (which can be inefficient),
we use, rather than a list type,
a function which prepends these pairs to a given list.

Since the list of elementary steps applied by a tactic will in some cases
depend on the form of the subgoal to which the tactic is applied,
the new-style tactic must take the subgoal as an argument
and return a list 
of (theorem, subgoal-number) pairs
together with each new proof state that the 
corresponding regular tactic would return.

In an expression like
\texttt{rtac} \textit{th sg state},
the variables \textit{sg} and \textit{state} (subgoal number and proof state)
give the subgoal;
\texttt{rtac} \textit{th}
is of type \texttt{int -> thm -> thm Sequence.seq},
that is, \texttt{int -> tactic},
since \texttt{tactic} abbreviates 
\texttt{thm -> thm Sequence.seq}.
As a consequence of all this,
and the fact that the list is in the form of a prepend function,
the new versions of tactics and related functions
will have types in which \texttt{tactic} is replaced by
\pagebreak
\par\noindent
\texttt{thm -> 
(((thm * int) list -> \\ (thm * int) list) * thm) Sequence.seq}
\par\noindent

We will call these new-style tactics
\textbf{tsl-tactics}\index{tsl-tactic}\label{tsl-tactic},
`tsl' standing for (theorem, subgoal) list.
The tsl-tactics and related functions of cognate types
are found \insrc{tsl.ML}, in the structure \texttt{tsl},
with the same names as the corresponding standard Isabelle functions.
The corresponding standard Isabelle versions of these functions
are in structure \texttt{no\_tsl}.
The code for many tactics, such as \texttt{d\_b\_tac} and \texttt{glob\_tac},
and tacticals, such as \texttt{THEN} and \texttt{THENEXP},
is included.
For most of these functions, this code is identical to that for the 
Isabelle versions; it appears again in the structure \texttt{tsl}
because it uses the ``tsl version'' of another function, such as
\texttt{rtac}, \texttt{THEN} and \texttt{all\_tac}.

From a list of tactics in this form, we need to derive the equivalent list
of single step tactics (ie, steps of the form 
\texttt{rtac} \textit{th sg});
the following functions, in \src{tsl.ML}, perform this and related functions.
\begin{description}

\item[\texttt{tsltac : 
'a -> ('a -> (('b list -> 'b list) * 'a)}]\tti{tsltac}
\mbox{}\hspace{4em} \textbf{\texttt{Sequence.seq) list -> 'b list}} \\
is used with \texttt{'a} = \texttt{thm} and
\texttt{'b} = \texttt{thm * int}.
Where \textit{initst} is the initial proof state, and
\textit{tsltlist} is a list of tsl-tactics,
\texttt{tsltac} \textit{initst tsltlist}
returns the list of simple proof steps which 
\textit{tsltlist} would perform in the initial proof state \textit{initst};
the proof steps are returned in the form of (theorem, subgoal) pairs,
where a pair \pair{th}{sg} corresponds to the simple proof step
\texttt{rtac} \textit{th sg}.
The text of \texttt{tsltac} is simply
%\begin{center}
\\[1.0ex]
\texttt{fun tsltac st rtl = (\#1 (Sequence.hd (tsl.EVERY rtl st))) [];}
%\end{center}

\item[\texttt{tsl2rt : (thm * int) list -> tactic list}]\tti{tsl2rt}
takes a list of (theorem, subgoal) pairs,
and returns the corresponding list of tactics
(turning a pair \pair{th}{sg} into \texttt{rtac} \textit{th sg}).

\item[\texttt{tsl2txt : (thm * int) list -> string}]\tti{tsl2txt}\label{tsl2txt}
is like \texttt{tsl2rt}, except that it returns a tactic list
as a string of the form \texttt{"byev [$\ldots$] ;"},
enabling subsequent use of the Isabelle function \texttt{use\_string}
(which submits a list of strings to ML as though they were typed in at the
terminal),
or of cut-and-paste and/or editing operations.
\end{description}

Note that much of what we do assumes that each 
\texttt{rtac} \textit{th sg} step produces at most only a single next state;
this is certainly the case so long as there is no higher-order unification
(which involves function variables).
We have not yet observed any use for function variables in doing Display
Logic.

\subsubsection{Functions for manipulating proof trees}

The following functions, found \insrc{pftr.ML},
are used to form and manipulate proof trees.
\begin{description}
\item[\texttt{ptpthm : rtpt -> thm}]\tti{ptpthm}
returns the theorem associated with a proof tree.
Its text is simple: 
\vspace{-2ex}
\begin{verbatim}
fun ptpthm Unf = asm_rl
  | ptpthm (Pr (th, pts)) = map ptpthm pts MRS th ;
\end{verbatim}

\item[\texttt{tsl2pt : (thm * int) list -> rtpt}]\tti{tsl2pt} 
\mbox{} \\
This function turns a (theorem, subgoal) list into a proof tree,
%working from the top of the proof tree down;
building the proof tree from the leaves down to the end-sequent;
thus it processes the proof steps in reverse order.
It uses a working list of incomplete proof trees,
which are branches that have not yet been built down to the points where they
are joined.
This list is initially empty, but is
extended with null proof trees (ie, \texttt{Unf}) as necessary.
The following is done repeatedly (by the function \ttdef{add2ptl}):
for a pair \pair{th}{sg}
(representing a proof step \texttt{rtac} \textit{th sg}),
where \textit{th} has $n$ premises
\begin{itemize} \shrinklist{0.5}
\item[--] take $n$ proof trees, starting from the
\textit{sg}'th one, from the working list, calling them \textit{ptl}
\item[--] form a new proof tree 
\texttt{Pr(}\textit{th}\texttt{,}\textit{ptl}\texttt{)}
and put it in the working list in place of the proof trees \textit{ptl}
\end{itemize}

\item[\texttt{pt2tsl : rtpt -> (thm * int) list}]\tti{pt2tsl} 
\mbox{} \\
This function does the reverse of \texttt{tsl2pt}: it turns a 
proof tree into a list of 
proof steps in the form of (theorem, subgoal) pairs,
where a pair \pair{th}{sg} corresponds to the simple proof step
\texttt{rtac} \textit{th sg}.

\item[\texttt{addb2pt : rtpt list * rtpt -> rtpt list * rtpt}]\tti{addb2pt} 
\mbox{} \\
This function joins proof trees in a list \textit{btl} to the \texttt{Unf} nodes
at the top of a proof tree \textit{pt}.
That is, where a proof tree \textit{pt} represents an incomplete proof,
with unproved subgoals, and the 
proof trees in the list \textit{btl} provide proofs of those subgoals,
\texttt{addb2pt} \pair{btl}{pt}
forms the single proof tree in which the unproved subgoals of \textit{pt}
are matched to the proofs in the list \textit{btl}.
To suit the recursive definition of the function, 
\texttt{addb2pt} \pair{btl}{pt}
returns \pair{btlr}{npt},
where \textit{npt} is 
\textit{pt} with \texttt{Unf} nodes
replaced by trees taken from the list \textit{btl},
and \textit{btlr} is the unused part of the list \textit{btl}.

\item[\texttt{replace\_th : (string * rtpt) list -> rtpt -> rtpt}]
\tti{replace\_th} 
\mbox{} \\
This function replaces any occurrence in a proof tree of one or more theorems 
by a corresponding proof tree (which would be a proof of the theorem).
It is called as \texttt{replace\_th} \textit{nal pt}, where
\textit{nal} is an ``association list'' of theorem names and replacement proof
trees; every theorem in \textit{pt} whose name \textit{name} is found in 
a pair \pair{name}{rpt}
in \textit{nal} is replaced, in \textit{pt}, by the corresponding replacement
proof tree \textit{rpt}.
This is useful when a proof uses derived rules; 
the occurrences of those derived rules in the proof tree
can then be replaced by their proofs.
In this way it is easy to produce a proof tree
such that primitive rules used in the proof
actually appear as steps in the proof tree.

\end{description}

It might be thought more natural to implement the function
\texttt{tsl2pt} by taking
the (theorem, subgoal) pairs in forward order, and building the
proof tree from the root upwards.
However, this would lead to an inefficiency, namely at each step,
in processing the pair \pair{th}{sg},
it would
be necessary find the spot in the tree corresponding to
subgoal number \textit{sg};
that requires traversing the tree to find the
\textit{sg}'th occurrence of \texttt{Unf}.

Alternatively, each node could also contain a field showing
how many \texttt{Unf} nodes are in the part of the tree rooted at
the given node, ie how many currently unproved
subgoals there are in that part of the tree.
This alternative is implemented by the datatype \texttt{rtnt} and the
functions \texttt{add2nt}, \texttt{addl2nt} and \texttt{add2ntl}. 

\subsubsection{Naming Isabelle theorems}

Recall from \S\ref{isathm} that an Isabelle theorem,
of type \texttt{thm}, can have the
form of (\emph{inter alia}) a \dRA\ sequent or a rule.
In Isabelle, the theorem type \texttt{thm} contains a field
which can contain a name for the theorem.
The Isabelle function 
\texttt{name\_thm : string * thm -> thm}\tti{name\_thm}
gives a name to a theorem.
The function 
\texttt{name\_of\_thm : thm -> string}\tti{name\_of\_thm},
defined \insrc{name.ML},
returns the name of a theorem.
The \src{name.ML} also redefines a number of Isabelle functions so as to
give theorems names; for example, if theorems 
\textit{th1} and \textit{th2} have names
\textit{name1} and \textit{name2}, the theorem
\textit{th1} \texttt{RS} \textit{th2} will be given the name
\texttt{(}\textit{name1}\texttt{ RS }\textit{name2}\texttt{)}.
(This is useful for producing the text of a tactic as a string,
as in \texttt{tsl2txt}, see \page{tsl2txt} above).

\subsubsection{Functions implementing the cut-elimination procedure}

The following functions, found \insrc{cut.ML}, are used to 
implement the cut-elimination procedure.
\begin{description}
\item[\texttt{findpt : string list -> term -> term * string list}]
\tti{findpt} 
\mbox{} \\
The first argument is
an exploded string which will represent the location of $A$ in
a term, using the characters as in the first argument of \texttt{disp\_tac}
(see \page{disp_tac}).
Then \texttt{findpt} \textit{estr tm} finds the part of the term \textit{tm}
indicated by \textit{estr}.
If there is a formula \textit{fm} in the location indicated
then \texttt{(}\textit{fm}\texttt{,[])} is returned.
On the other hand, \texttt{findpt} may find a structure variable 
representing a structure of which $A$ would be a sub-structure,
for example if \textit{tm} is $*U \vdash *V$ and \textit{estr} is
\texttt{["-","*","L"]}.
Then \texttt{findpt} returns \texttt{(}\textit{V}\texttt{,["L"])},
indicating that $A$ is at the \texttt{"L"} position in the structure
represented by $V$.

\item[\texttt{findlocs : term -> term -> string list -> string list}]%
\tti{findlocs} 
\mbox{}\\ \mbox{}\hspace{4em}
\textbf{\texttt{-> string list list -> string list list}} \\
\texttt{findlocs} \textit{pt tm} \texttt{[]} \textit{within} \texttt{[]}
finds the locations of term \textit{pt} (which is typically a structure variable)
in term \textit{tm} (which is typically the premise of a structural rule).
Each such location (using the same character codes as \texttt{findpt})
has \textit{within} (which is typically the second component of the pair
returned by \texttt{findpt}) appended to it.

Thus \texttt{findpt} and \texttt{findlocs} together 
are used to trace the occurrence of the cut-formula $A$ up a proof tree.
Continuing the example given in the description
of \texttt{findpt}, consider the derived rule
\mbox{$V,V \vdash U \Longrightarrow *U \vdash *V$.}
If calling \texttt{findpt}, as above, gives that 
$A$ is at the \texttt{"L"} position of the structure
represented by $V$, then calling 
\mbox{
\texttt{findlocs} $V$ $(V,V \vdash U)$ \texttt{[]} \texttt{["L"]} \texttt{[]}
}
returns \texttt{[["|","l","L"],["|","r","L"]]} 
to indicate the two locations where $A$ is to be found in the sequent
$V,V \vdash U$.

\item[\texttt{repcut : rtpt -> string list -> rtpt -> rtpt}]\tti{repcut} 
\mbox{}\\ 
This is a recursive procedure which removes a single cut.
The cut is moved upwards one proof step at a time, and \texttt{repcut} is
called again (recursively) once for each such move.
%It is called once for each step that the cut is moved upwards.
In terms of \fig{cut123}, it is called first as 
\texttt{repcut} \textit{right} \textit{loc} \textit{left},
where 
\textit{right} is the proof tree whose conclusion is $A \vdash Y$,
\textit{left} is the proof tree whose conclusion is $X \vdash A$,
and \textit{loc} is \texttt{["-"]}, 
denoting that the cut-formula $A$ is found at the 
\texttt{"-"} position in $X \vdash A$.
For subsequent calls, going up the tree from $X \vdash A$ to $Z \vdash A$,
\textit{left} changes, and \textit{loc} changes as it continues to indicate
the position of $A$ in the conclusion of \textit{left}.
When this process reaches $Z \vdash A$ (as in \fig{cut123}(b))
the same thing is repeated on the other side, calling
\texttt{repcut} \textit{left} \textit{loc} \textit{right},
where 
\textit{left} is the proof tree whose conclusion is $Z \vdash A$,
\textit{right} is the proof tree whose conclusion is $A \vdash Y$,
and \textit{loc} is \texttt{["|"]}.

Note that we recognize that we have reached the intermediate stage
(\fig{cut123}(b)) and then the
final stage (\fig{cut123}(c)) by the fact that 
the premise of the last rule under consideration contains a formula
in the position representing $A$.
(It doesn't check that the rule actually introduces $A$).
Thus if the sequence between $Z \vdash A$ and $X \vdash A$ 
contains a use of a rule like
$*A \vdash *U \Longrightarrow U \vdash A$
(where the formula $A$ in the rule matches the cut-formula $A$), 
the procedure will fail.
(Use of such a rule is perfectly legal, but unlikely in practice,
since one would tend to use the corresponding, 
but more general, structural rule
$*V \vdash *U \Longrightarrow U \vdash V$.
In fact, the rule
$*A \vdash *U \Longrightarrow U \vdash A$
breaks one of the set of conditions shown by Belnap \cite{Bel}
to be sufficient to ensure that a Display Logic satisfies
the cut-elimination theorem.)

\item[\texttt{C8 : rtpt -> rtpt -> rtpt}]\ttl{C8} 
\mbox{}\\ 
When we finish moving the cut on $A$ upwards, ie we reach the stage in
\fig{cut123}(c),
we have sequents $Z \vdash A$ and $A \vdash W$ which are the points
where $A$ is introduced.
We then need to convert the cut on $A$ to cuts on the components of $A$.
The function \texttt{C8}, \insrc{C8.ML}, does this;
with proof trees whose conclusions are $Z \vdash A$ and $A \vdash W$ 
it returns a proof tree whose conclusion is $Z \vdash W$,
containing cuts on the components of $A$.
(Alternatively, if one of the arguments is $A \vdash A$, \texttt{C8}
returns the other argument).
The function \texttt{C8} is coded as a list of particular cases,
depending on the names of the Isabelle theorems (\dRA\ rules)
%whose conclusions are 
which introduce the occurrences of $A$ in
$Z \vdash A$ and $A \vdash W$.
Possible future work would be to find a procedure that works 
where arbitrary introduction rules are used at these points.

\item[\texttt{repcuts : rtpt -> rtpt}]\tti{repcuts} removes all the cuts in a
proof tree.

%This is used to find the locations of $A$ in the various terms in 
%the proof between $Z \vdash A$ and $X \vdash A$, and between
%$A \vdash W$ and $A \vdash Y$.

\end{description}

Note that \texttt{C8} and \texttt{repcuts} recognize rules
by their Isabelle theorem names.
If derived rules are used which contain or use (cut), for example,
then the instances of (cut) contained in the use of those rules will
not be removed.
Likewise, if derived logical introduction rules are used, then \texttt{C8}
will not work.
The function \texttt{replace\_th} was written to provide an easy way to ensure
that when a proof relies on a rule such as (cut), that rule is visible as
a step in the proof tree.