Some SML code is used to do part of the work of 
finding these replacement derivation trees.
But the proof that such a replacement derivation tree is well-formed,
for example, has to be done using the theorem prover.

Here is the resulting theorem for $\lor$:

\begin{theorem}[\texttt{orC8}]
If a valid derivation tree \texttt{pt} satisfies
\begin{itemize}
\item if the bottom rule of \pt\ is (\emph{cut}), then it is
principal and its cut-formula is $A \lor B$, and
\item any cuts above the root of \pt\ have either $A$ or $B$ as
cut-formula, 
\end{itemize}
then there is another valid derivation tree 
\texttt{ptn} with the same conclusion 
as \texttt{pt}, such that
\emph{all} cuts in \texttt{ptn} have either $A$ or $B$ as cut-formula.
\end{theorem}

\begin{verbatim}
orC8 = 
  "[| cutIsLRP (?A v ?B) ?pt; allPT wfb ?pt; allPT (frb rls) ?pt;
      allNextPTs (cutOnFmls {?B, ?A}) ?pt |]
   ==> EX ptn.
          conclPT ptn = conclPT ?pt & allPT wfb ptn &
          allPT (frb rls) ptn & allPT (cutOnFmls {?B, ?A}) ptn"
\end{verbatim}


\subsection{Putting it all together}
\cc{s-pat}
\label{s-pat}

A monolithic proof of the cut-elimination theorem would be very complex,
involving several nested inductions.
For the transformations above replace one cut by many left-principal cuts,
one left-principal cut by many principal cuts and one principal cut 
by one or two cuts on subformulae, whereas we need, ultimately,
to replace many cuts in a given derivation tree.
We manage this complexity by defining two predicates,
\texttt{canElim} and \texttt{canElimAll},
whose meanings (assuming valid trees) are given below.

% from HOL_Elim.thy
\begin{verbatim}
  canElim      :: "(pftree => bool) => bool"
  canElimAll   :: "(pftree => bool) => bool"
\end{verbatim}

\texttt{canElim f} means that if a valid derivation tree \texttt{pt}
has no cuts other than (possible) one
at the bottom, and satisfies \texttt{f}, then there is an equivalent 
valid cut-free derivation tree.

\texttt{canElimAll f} means that if every subtree of a given 
valid tree \texttt{pt} satisfies \texttt{f}, 
then there is a valid
cut-free derivation tree \texttt{pt'} equivalent to \texttt{pt}
(we also include as part of this definition the requirement
that if the bottom rule of \texttt{pt} is not (\textit{cut}),
then the bottom rule of \texttt{pt'} is the same).

\footnote{
RAJ - you suggest making the following lemmata.
I see your point, but wonder how it would look.
Firstly, there would be thirteen of them,
\texttt{allLP'} to \texttt{canElimAll}.
I assume one lemma with 13 parts would be best.
(or did you mean just \texttt{allLP'} and \texttt{allLRP'} ?)
Secondly, the present statements in English (at present for some only)
are rather informal, ``you can eliminate \ldots''.

If neither of these are a problem, then we could state the rest in
English similarly, and make the change, and
list all the Isabelle theorems below.

Alternatively, part of what I've written is of the flavour of a proof,
so some or all of it could be made part of the proof of the ultimate result,
except for the fact that it has Isabelle theorems interspersed in it.
}

We can now restate the theorems 
\texttt{allLP} and \texttt{allLRP},
in terms of \texttt{canElim} and \texttt{canElimAll}.

\begin{theorem}[\texttt{allLP'}, \texttt{allLRP'}]
\begin{enumerate}
\item If you can eliminate any number of left-principal cuts on $A$ from 
a valid tree \pt,
then you can eliminate a single cut on $A$ from the bottom of \pt.
\item If you can eliminate any number of principal cuts on $A$ from 
a valid tree \pt,
then you can eliminate a single left-principal
cut on $A$ from the bottom of \pt.
\end{enumerate}
\end{theorem}

\begin{proof}
\begin{enumerate}
\item The theorem \texttt{allLP} says 
``you can turn a tree \pt\ which has one cut, which is at the bottom
and is on $A$,
into a tree with several cuts, which are all left-principal and are on $A$'',
which is equivalent to the theorem statement.
\item This has a corresponding proof. \qed
\end{enumerate}
\end{proof}

\comment{
We can now turn the theorems 
\texttt{allLP} 
(``you can turn a tree with one cut, at the bottom, on $A$,
into a tree with several cuts, all left-principal on $A$'')
into \texttt{allLP'}:
\begin{verbatim}
allLP' = "canElimAll (cutIsLP ?A) ==> canElim (cutOnFmls {?A})"
\end{verbatim}
(``if you can eliminate several cuts, all left-principal on $A$,
then you can eliminate a single cut, at the bottom, on $A$'').

Likewise \texttt{allLRP} is turned into \texttt{allLRP'}:
\begin{verbatim}
allLRP' = "canElimAll (cutIsLRP ?A) ==> canElim (cutIsLP ?A)" 
\end{verbatim}
}

Now if we can eliminate one cut (or left-principal cut, or principal cut)
then we can eliminate any number, by eliminating them one at a time
starting from the top-most cut.  This is easy because eliminating a cut
affects only the proof tree above the cut. 
(There is just a slight complication:
we need to show that eliminating a cut must not 
change a lower cut from being principal to not principal).

This gives the following three theorems:

\begin{verbatim}
elimLRP = "canElim (cutIsLRP ?A) ==> canElimAll (cutIsLRP ?A)"
elimLP = "canElim (cutIsLP ?A) ==> canElimAll (cutIsLP ?A)"
elimFmls = "canElim (cutOnFmls ?s) ==> canElimAll (cutOnFmls ?s)" 
\end{verbatim}

We also have two results which will be combined with \texttt{elimFmls}

\begin{verbatim}
twoElim = "[| canElim (cutOnFmls {?A}); canElim (cutOnFmls {?B}) |]
    ==> canElim (cutOnFmls {?B, ?A})"
\end{verbatim}
(``if you can eliminate a cut (at the bottom) on $A$
and if you can eliminate one on $B$
then you can eliminate one which may be either on $B$ or $A$'').
\begin{verbatim}
trivElim = "canElim (cutOnFmls {})" 
\end{verbatim}
(``you can eliminate cuts (if any) from a tree which has no cuts'').

We also have the theorems such as \texttt{orC8} (see \S\ref{s-deal})
showing that a tree with a single (left- and right-) principal 
cut on a particular formula can be replaced by a tree with cuts on 
the subformulae of that formula;
these theorems are converted to a list of theorems \texttt{thC8Es'}, 
of which one is
\begin{verbatim}
"canElimAll (cutOnFmls {?B, ?A}) ==> canElim (cutIsLRP (?A v ?B))"
\end{verbatim}

Combining this with the previous results 
\texttt{elimLRP}, \texttt{allLRP'}, \texttt{elimLP} and \texttt{allLP'}
we get the list of theorems \texttt{thC8Es}, including
\begin{verbatim}
"canElimAll (cutOnFmls {?B, ?A}) ==> canElim (cutOnFmls {?A v ?B})"
\end{verbatim}

We then combine these with the result \texttt{elimFmls} and
(in the case of a binary logical connective) \texttt{twoElim} to get
the list of theorems \texttt{elimFmlRecs}, including
\begin{verbatim}
"[| canElim (cutOnFmls {?A}); canElim (cutOnFmls {?B}) |]
    ==> canElim (cutOnFmls {?A v ?B})"
\end{verbatim}

The theorems \texttt{elimFmlRecs} are then used in a proof by
structural induction on the structure of a formula to prove
\begin{verbatim}
canElimFml = "canElim (cutOnFmls {?fml})"
\end{verbatim}
(``you can eliminate one cut on any given formula \texttt{fml}''), 
\begin{verbatim}
canElimAny = "canElim (cutOnFmls UNIV)", 
\end{verbatim}
(``you can eliminate one cut whatever the cut-formula''), 
and, using \texttt{elimFmls},
\begin{verbatim}
canElimAll = "canElimAll (cutOnFmls UNIV)"
\end{verbatim}

Finally we convert \texttt{canElimAll} into
\begin{verbatim}
cutElim = 
  "IsDerivableR rls {} ?concl ==> IsDerivableR (rls - {cut}) {} ?concl"
\end{verbatim}