\section{Implementation of Display Logic rewriting in Isabelle}
  \label{app:DL-impl}

The implementation of Display Logic in Isabelle is described
generally in \cite{thesis}.
Here we describe the implementation of the rewriting procedure.
In part, this is conceptually similar to the implementation 
described for LPF, in that
it uses simple functions to build more complex strategies for traversing
a term and finding subterms to rewrite, just as described in 
Appendix \ref{app:LPF-impl}.
However, the function that is used to perform a single rewrite 
is distinctly different from a HOL conversion.

We first introduce the concept of an \emph{action},
defined by
\begin{center} \texttt{
datatype $\alpha$ action = Unc | Act of (int -> thm -> $\alpha$) ;
} \end{center}
An action is used to operate on a sequent;
\texttt{Unc} means the sequent will be unchanged,
whereas \texttt{Act}~\textit{fn} means that 
\textit{fn} is used to transform the sequent.
For backward proof, 
\textit{fn} replaces a subgoal with a number of replacement subgoals;
thus when \textit{sg} is a subgoal number, 
\textit{fn}~\textit{sg} is a tactic
(which has type \texttt{thm~->~thm~Seq.seq}).
For forward proof, we would want \textit{fn} to be a function which 
maps one theorem to another.  However, to enable the code to be shared,
we let \textit{fn} have an extra integer argument which is ignored.
Thus for forward or backward proof, the type
\texttt{$\alpha$} is \texttt{thm} or \texttt{thm Seq.seq} respectively.

We also have a type \texttt{side}, whose values are 
\texttt{Ant} and \texttt{Suc}, denoting the 
\emph{antecedent} and \emph{succedent} (left and right)
sides of the `$\vdash$'\ .

Instead of a conversion, we have an \emph{action function},
of type \texttt{$\alpha$ actfn = term~->~side~->~$\alpha$~action}.
If, for example it is called 
with arguments term $t$ and side \texttt{Ant}, 
and returns action 
\texttt{Act}~\textit{act},  
\textit{act} should transform a sequent 
$t \vdash X$ to another sequent $t' \vdash X$
(for backward proof, the result may be any number of new subgoal sequents).

Again, we have functions that combine or transform these action functions;
these functions differ for forward or backward proof, 
but to let the
forward and backward functions share a lot of the code we define a record type 
\texttt{$\alpha$~meth},
which is described in Appendix \ref{app:DL-code}.
\comment{
with the following fields 
(note that here the arguments referred to as ``actions'' do \emph{not}
have the \texttt{Act} prefix):
\begin{description} %\shrinklist{0.5}
\item[\mdseries\texttt{idact : int -> thm -> $\alpha$}]
is the identity action,
the action which doesn't change the sequent
\item[\mdseries\texttt{actcomb
: (int -> thm -> $\alpha$) * (int -> thm -> $\alpha$) -> 
  (int -> thm -> $\alpha$)}]
is the sequential composition of two actions
\item[\mdseries\texttt{dpact : thm -> int -> thm -> $\alpha$}]
gives the action to be taken to transform a term
using a given display postulate 
\item[\mdseries\texttt{find\_tm : int -> thm -> term}]
is the function which finds the term being
examined, ie, in backwards proof, the subgoal,
or, in forward proof, the conclusion of the theorem.
\end{description}

The source code defining the values used for these arguments is
\begin{center}
\begin{tabular}{l}
\textbf{\qquad \qquad for backward proof} \\ \\
\texttt{fun idact sg = all\_tac ;} \\
\texttt{val actcomb = op THENEXP ;} \\
\texttt{val dpact = rtac o md2 ;} \\
\texttt{fun find\_tm sg state = nth (prems\_of state, sg-1) ;}
%\end{tabular} \end{center} \begin{center} \begin{tabular}{l}
\\ \\
\textbf{\qquad \qquad for forward proof} \\ \\
\texttt{fun idact \_ th = th ;} \\
\texttt{fun actcomb (f, g) \_ = (g 0) o (f 0) ;} \\
\texttt{fun dpact theq \_ th = th RS md1 theq ;} \\
\texttt{fun find\_tm \_ = concl\_of ;}
\end{tabular}
\end{center}

In the above, \texttt{md1} and 
\texttt{md2} turn a meta-equivalence to
forwards and backwards meta-implications;
\verb:(:\textit{tacf1} \verb:THENEXP: \textit{tacf2}\verb:): \textit{sg}
applies \textit{tacf1}
to subgoal number \textit{sg}, then
applies \textit{tacf2} to each resulting subgoal.
This tactical may be generally useful; it corresponds 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.
}
With this framework, it is easy to construct functions
analogous to conversionals.
We have several operators of which 
\texttt{THENaf}, \texttt{REPaf}, \texttt{SUBaf} 
%\texttt{TDaf} and \texttt{BUaf}
are similar to those described in 
Appendix \ref{app:LPF-impl}, so they are not all described here.
\begin{description}
\item[\texttt{THENaf, ELSEaf : 'a meth -> 'a actfn * 'a actfn -> 'a actfn}]
\mbox{} \\
These combine the effects of two action functions in sequence.
\texttt{THENaf}
applies the second
whether or not the first succeeds,
but \texttt{ELSEaf} applies the second only if the first fails.
%\item[\texttt{TDFaf : 'a meth -> 'a actfn -> 'a actfn}]
%goes through whole term, in top-down order,
%looking for subterms to change, 
%but only making the first possible change in any branch of the term's 
%``structure tree''.
%It is defined by 
%\begin{center} \noindent
%\texttt{
%fun TDFaf meth af tm = \hfill \mbox{} \\
%\hfill ELSEaf meth (af, SUBaf meth (TDFaf meth af)) tm ; }
%\end{center}
\end{description}

As in Appendix \ref{app:LPF-impl} it is easy to create more. 
For example, \texttt{TDFaf}, given by 
\begin{center} \noindent
\texttt{
fun TDFaf meth af tm = \hfill \mbox{} \\
\hfill ELSEaf meth (af, SUBaf meth (TDFaf meth af)) tm ; }
\end{center}
goes through whole term, in top-down order,
looking for subterms to change, 
but only making the first possible change in any branch of the term's 
``structure tree''.
\texttt{TDFaf} was written solely for the purpose of producing the 
%\LaTeX\ source of
intermediate steps of the second example in \S\ref{DL-rewr}.

As explained above, rewriting a subterm involves displaying that subterm,
performing the rewrite action, and then reversing the display step.
(The process of displaying any chosen subterm has been automated,
and is described in \cite{thesis}).
However, in attempting to rewrite a subterm (eg, where \texttt{TDaf},
which is analogous to \texttt{TDtt},
is used to find and perform all possible rewrites)
it is important for efficiency that a subterm be displayed only if the 
subsequent attempt to rewrite it will succeed.
The coding of \texttt{SUBaf} ensures this;
a subterm is displayed only if it will be changed.
This is why the arguments of an action function are a term $t$ and a side;
the action function tests these to see whether a sequent 
$t \vdash X$ or $X \vdash t$ would be changed, rather than testing 
the theorem containing the sequent.
Once a subterm is identified to be changed, though, 
we may need to test the new subterm for further possible changes;
in this case we have to wait until the original
subterm is displayed and changed before 
we can ascertain the new subterm.

We have to programme the action functions.
This is achieved for forward proof as follows.
%A rule \textit{rule} of the form $A \vdash X \Longrightarrow B \vdash X$
%gives rise to a function \textit{patfn},
%where, for a term $t$,
%\textit{patfn t} tells whether $A$ can be instantiated to match $t$.
%If so, \textit{rule} is selected,
%and \texttt{Act}~\textit{fn}, where
%\textit{fn~i~th} = \textit{th}~\texttt{RS}~\textit{rule},
%is returned as the action.
%Normally an action function will use several rules;
%these are in two lists,
%one each for terms $t$ on the antecedent and succedent sides.
%The first rule (in the appropriate list) which matches $t$ is selected.
Given a term $t$, on (say) the antecedent side, a rule \textit{rule}
of the form 
$A \vdash X \Longrightarrow A' \vdash X$,
which instantiates to 
$t \vdash X \Longrightarrow t' \vdash X$,
is used;
then \texttt{Act} $f$, where $f$ takes 
$t \vdash X $ to $ t' \vdash X$, is returned.
Typically \textit{rule} is selected from a specified set of candidate rules.

For backward proof, the procedure is similar, 
except that the rule \textit{rule} may have several premises, 
of the form
$$ [| B_1 \vdash X ; \ldots ; B_n \vdash X |] \Longrightarrow A \vdash X $$
and the action returned takes the goal $A\vdash X $ (instantiated)
to the several subgoals 
$ B_1 \vdash X , \ldots , B_n \vdash X $ (instantiated).
%The relevant functions are found in the source file \texttt{pat.tac}.