\subsection{Definition of the transformation}
\label{s-mlp}
\cc{mlp.tex}
\cc{s-mlp}

In \S\ref{s-mcp} we described the proofs about
transforming a derivation tree to make a cut principal.
These proofs were couched in terms of existence --
the relevant results
\texttt{makeCutLP} and \texttt{makeCutRP}, 
state the existence of a new derivation tree whose cuts are 
left-principal, or principal.
Likewise, the result \texttt{extSub''} merely states the existence of 
the substitution needed to construct one node of the new derivation tree.

As part of an attempt to implement some of the proofs of 
Wansing \cite{wansing-displaying-modal-logic} 
(discussed later, \S \ref{s-wsn}), 
we gave (partially) a functional definition of the transformation
used to obtain the new derivation tree.

We define the following transformations:
\begin{verbatim}
  mLP, mLP'	:: "pftree => sequent => pftree => pftree"
  mLPs	:: "pftree => sequent list => pftree list => pftree list"
  mRP, mRP'	:: "pftree => sequent => pftree => pftree"
  mRPs	:: "pftree => sequent list => pftree list => pftree list"
\end{verbatim}
The function \texttt{mLP} produces the derivation tree whose existence is
asserted in the theorem \texttt{makeCutLP}. Thus
the arguments to \texttt{mLP} are
\begin{enumerate}
\item a derivation tree with root $A \vdash Y$,
such as the right subtree of the first tree given in
Fig. \ref{fig-cut-p}
\item the sequent $X_Y$,
\item a tree with root $X_A$, 
such as the left subtree of the first tree given in 
Fig. \ref{fig-cut-p},
\end{enumerate}
where $X_A$ will usually contain occurrences of $A$ in 
one or more succedent position(s),
and $X_Y$ is $X_A$ with zero, one or more of these occurrences of $A$
changed to $Y$.
The result is a new derivation tree,
with root sequent $X_Y$
whose new cuts (on $A$) are left-principal,
such as the second subtree given in Fig. \ref{fig-cut-p}.
\texttt{mLPs} takes for its third argument
a list of derivation trees instead of one, and returns
a corresponding list.

Likewise \texttt{mRP}, given derivation trees whose root sequents are
$X_A$ ($A$ in antecedent positions) and $Y \vdash A$, and given $X_Y$,
which is $X_A$ with some occurrences of $A$ 
in antecedent positions changed to $Y$,
returns a derivation trees whose root sequent is $X_Y$,
whose new cuts are right-principal.

The definition of \texttt{mLP} is presented using a function \texttt{mLP'},
which is just \texttt{mLP} when applied to a derivation tree in which,
if the root sequent is $X \vdash A$, the displayed occurrence of $A$ is 
not principal.
In turn, these functions are defined in terms of a function \texttt{newSub},
defined by 

% from newSub.thy
\begin{verbatim}
  newSub_Pr "newSub (Pr seqA rule ptlA) seqY =
      stepSub (ruleSubOf (Pr seqA rule ptlA)) (conclRule rule) seqY"
\end{verbatim}

Here, \texttt{ruleSubOf} gives a substitution which takes \texttt{rule}
to the instance actually used at the bottom of \texttt{Pr seqA rule ptlA}.
To explain \texttt{stepSub (fs, suba) seq seqY},
let \texttt{(fs, suby)} be a substitution which takes \texttt{seq} to 
\texttt{seqY}, and let \texttt{sub} be a structure variable substitution
which acts as \texttt{suby} on the structure variables in \texttt{seq},
and as \texttt{suba} on other structure variables.

% from RP.thy
\begin{verbatim}
mLP'_Pr = "mLP' ptAY seqY (Pr seqA rule ptlA) =
   (let sub = newSub (Pr seqA rule ptlA) seqY;
        premsinst = premsRule (ruleSubst sub rule)
    in Pr seqY rule (mLPs ptAY premsinst ptlA))" : thm

mLP_Pr' = "mLP ptAY seqY (Pr seqA rule ptlA) =
   (if strIsFml (succ (conclRule rule)) & succ seqA ~= succ seqY
    then let seqYA = $(antec seqY) |- $(succ seqA)
         in Pr seqY cut [mLP' ptAY seqYA (Pr seqA rule ptlA), ptAY]
    else mLP' ptAY seqY (Pr seqA rule ptlA))" : thm
\end{verbatim}

The definition of \texttt{mRP} is similar.
Proving the necessary results is complicated by the fact that it is 
necessary to show that the substitution \texttt{suby} in the definition
of \texttt{stepSub} exists, and that although such a substitution
is not unique, the choice does not matter.  

The result \texttt{makeCutmLP}, and a similar result \texttt{makeCutmRP},
correspond to \texttt{makeCutLP} and \texttt{makeCutRP}.
\begin{verbatim}
makeCutmLP =
  "[| allPT (cutOnFmls {}) ptAY; allPT (frb rls) ptAY;
      allPT wfb ptAY; conclPT ptAY = (A |- $Y); allPT (frb rls) ptA;
      allPT wfb ptA; allPT (cutOnFmls {}) ptA;
      seqRep True (Structform A) Y (conclPT ptA) seqY;
      ptY = mLP ptAY seqY ptA |]
   ==> conclPT ptY = seqY & allPT (cutIsLP A) ptY & 
       allPT (frb rls) ptY & allPT wfb ptY" : thm
\end{verbatim}

Surprisingly, proving \texttt{makeCutmLP} and \texttt{makeCutmRP},
turned out to be very much
more difficult than proving the corresponding existence results
\texttt{makeCutLP} and \texttt{makeCutRP}.