The syntax of \dKt\ has been implemented in Isabelle.
It uses the Isabelle type (distinct from ML types) \texttt{prop} (for sequents)
and defines types \texttt{structure} and \texttt{formula},
so as to distinguish structure and formula variables.
Since a formula can also be a structure,
there is an operator ``Structform'', which coerces a formula
argument (of Isabelle type \verb:formula:)
into the ``same'' term, but with the type \verb:structure:.
Externally, at the user level, a structure variable 
or constant is preceded by `\verb:$:',
to distinguish it from a formula variable.
%Doing this in Isabelle is quite complex, and the method used was copied 
%from the Isabelle sequent calculus theory (\cite{OL}, Ch 6).

In the Isabelle implementation, the operators are represented as follows.
\begin{center}
\begin{tabular}{c@{\quad}c@{\ \ \ }c@{\ \ \ }c@{\ \ \ }c@{\ \ \ }c@{\ \ \ }
  c@{\ \ \ }c@{\ \ \ }c@{\ \ \ }c@{\ \ \ }
  c@{\ \ \ }c@{\ \ \ }c@{\ \ \ }c@{\ \ \ }}
\dKt & $;$ & $*$ & $I$ & $\bullet$ & 
$\land$ & $\lor$ & $\neg$ & $\bot$ & $\top$ &
$\square$ & $\blacksquare$ & $\lozenge$ & $\blacklozenge$ \\
\texttt{dKt.thy} & 
\texttt{;} & \texttt{*} & \texttt{I} & \texttt{@} & 
\texttt{\&} & \texttt{v} & \texttt{-} & \texttt{F} & \texttt{T} &
\texttt{wbx} & \texttt{bbx} & \texttt{wdm} & \texttt{bdm}  
\end{tabular}
\end{center}

The rules have been implemented in Isabelle;
the \dKt\ ($\vdash \land$) rule, for example,
and its Isabelle counterpart (called \texttt{ands}) are 
$$ \frac { X \vdash A \quad Y \vdash B} {X; Y \vdash A \land B}
\qquad 
\texttt{[| \$?X |- ?A; \$?Y |- ?B |] ==> \$?X; \$?Y |- ?A \& ?B} $$
Some rules of \dKt\ can be derived from others.
For example, (Ass $\vdash$) can be derived from ($\vdash$ Ass).
The Isabelle implementation uses this, 
but no effort was made to find a minimal set of rules.
Some particularly useful derived rules are shown in \fig{sdr}.
The rules \texttt{andS} and \texttt{orA} 
are equivalent to ($\vdash \land$) and ($\lor \vdash$), since
($\vdash \land$) and ($\lor \vdash$) can be derived from 
\texttt{andS}, \texttt{orA} and the monotonicity rules.

% SELECTED DERIVED RULES
\begin{figure}[htbp] %\normalsize
\begin{center}
\begin{tabular}{c@{\hspace{15mm}}c}
 \invrule { X \vdash Y } { X \vdash **Y } (\texttt{ssS}) &
 \invrule { X \vdash Y } { *Y \vdash *X } (\texttt{dcp}) 
  \\ & \\
  \invrule {*(X;Y) \vdash Z } { *Y; *X \vdash Z } (\texttt{cbdista}) & 
 \invrule {X \vdash *(Y;Z) } { X \vdash *Z; *Y } (\texttt{cbdists}) \\ & \\

\slrule {(\bullet X; \bullet Y) \vdash Z} {\bullet (X; Y) \vdash Z}
(\texttt{bldista}) &
\slrule {X \vdash \bullet Y; \bullet Z} {X \vdash \bullet (Y; Z)}
(\texttt{bldists}) \\ & \\

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

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.

\subsection{Display Tactics}
Tactics were written to help in displaying a chosen
substructure.
Fuller details of these are given in \cite{dawson-gore-dra},
and links to relevant files are at \\
\verb?http://arp.anu.edu.au:80/~jeremy/?.
\begin{description}
\item[\texttt{disp\_tac}] % : string -> int -> tactic}]
\label{disp_tac} 
replaces a subgoal by one in which a selected
structure is displayed. 

\item[\texttt{d\_b\_tac}] 
takes a subgoal,
displays an indicated substructure,
applies a tactic 
to the transformed subgoal,
and lastly
applies the reverse of the display steps to each resulting subgoal.
Since the tactic applied should change only the displayed structure,
we had to derive the rules 
\texttt{andS} and \texttt{orA} from
\texttt{ands} and \texttt{ora}
for use in this style of proof.

For example, if we start with the subgoal
$R \vdash ((* T; \bullet * S); \bullet * Q); Y$ then, 
using the code \verb:"-l": to denote the substructure 
$(* T; \bullet * S)$,
\verb:d_b_tac "-l" (rtac mrs):
applies the monotonicity (or weakening) rule (\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 ; * Y \vdash * T; \bullet * S$" 
  "(reverse of \texttt{disp\_tac "-l"})"
\U "$R ; * 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}

\item[\texttt{fdisp, fdispfun}] 
are functions corresponding to 
\texttt{disp\_tac} and \texttt{d\_b\_tac}, but for forward proof.

\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 each displayed 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}] % :}]\mbox{} \\
This function 
displays in turn every substructure of the subgoal indicated, and
applies a given tactic (if possible)
to the sequent thus produced. 
All the display steps are eventually reversed,
in the same way as for \verb:d_b_tac:.
It can be used to replace any substructure of a particular form by 
another substructure,
giving the effect of a rewrite procedure
\cite{dawson-rewr}.
\texttt{glob\_tac} uses a top-down strategy in the sense that 
it first looks at the whole structure,
then, recursively, each sub-structure.

\item[\texttt{bup\_tac}] is like \texttt{glob\_tac}, but uses a
bottom-up strategy, displaying and testing the smallest sub-structures first.

\item[\texttt{fgl\_fun, 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.

\end{description}

The implementation of the search-and-replace tactics
is described in \cite{dawson-rewr}.
%
%\subsection{Application of the Search-and-Replace Tactics}
%\label{srapp}
%We now describe some uses of the search-and-replace tactics.
%
Examples of some of their uses are
%\begin{itemize} \item[--]
(1) to eliminate $**$,
(2) to use the various distributive laws to push $*$ down, and 
(3) to eliminate logical operators, where possible,
using those logical introduction rules satisfying the property 
that the structure on the other side is left unchanged
(in backward proof only)
%\end{itemize} 

This last replacement
is available only for backward proof because
the logical introduction rules which it uses
are uni-directional rather than bi-directional.

\subsection{Example: proof of the K rule} \label{skpf}

In \fig{Kpf} we show an example of a proof in \dKt, using the proof of the
K rule as given in \cite{wansing-sequent}.
The rule ($M \vdash $) captures the monotonicity of `;' 
and the rules
($C \vdash $) and ($\vdash P $) capture its idempotence and commutativity.
(These reflect the fact that $\land $ and $\lor$ have these properties). 
The notation (dp) denotes any display postulate.
This proof uses the (cut) rule twice.
This is the usual way of incorporating a previously proved lemma into a proof.
As we see in \S\ref{ace}, the use of the cut rule can be eliminated
\emph{automatically}.
 
\begin{figure}[!htb] %\normalsize
\begin{center}

\up 4
\bpf

\A "$A \to B \vdash A \to B$"
\U "$\square (A \to B) \vdash \bullet ( A \to B)$" "($\square \vdash $)"
\U "$\square (A \to B); \square A \vdash \bullet ( A \to B)$" "($M \vdash $)"
\U "$\square (A \to B) \land \square A \vdash \bullet ( A \to B)$"
   "($\land \vdash $)"
\U "$\bullet (\square (A \to B) \land \square A) \vdash A \to B$" "(dp)"
\A "$A \vdash A$"
\U "$\square A \vdash \bullet A$" "($\square \vdash $)"
\U "$\square (A \to B); \square A \vdash \bullet A$" "($M \vdash $)"
\U "$\square (A \to B) \land \square A \vdash \bullet A$" "($\land \vdash $)"
\U "$\bullet (\square (A \to B) \land \square A) \vdash A$" "(dp)"
\B [2em] "$\bullet (\square (A \to B) \land \square A); 
  \bullet (\square (A \to B) \land \square A) \vdash (A \to B) \land A$"
 "($\vdash \land $)"
\U "$\bullet (\square (A \to B) \land \square A) \vdash (A \to B) \land A$"
   "($C \vdash $)"
\U "$\square (A \to B) \land \square A \vdash \square ((A \to B) \land A)$"
   "(dp, $\vdash \square $)"
\U "(1)"

\epf

\up 2

\bpf

\A "$A \vdash A$"
\A "$B \vdash B$"
\B [2em] "$A \to B \vdash * A; B$" "($\to \vdash $)"
\U "$A \to B \vdash B; * A$" "($\vdash P $)"
\U "$A \to B; A \vdash B$" "(dp)"
\U "$(A \to B) \land A \vdash B$" "($\land \vdash $)"
\U "$\square ((A \to B) \land A) \vdash \bullet B$" "($\square \vdash $)"
\U "(2)"

\epf

\up 2

\bpf

\A "$\square (A \to B) \vdash \square (A \to B)$"
\A "$\square A \vdash \square A$"
\B [2em] "$\square (A \to B); \square A \vdash 
  \square (A \to B) \land \square A $" "($\vdash \land $)" 
%\A "$\square (A \to B) \land \square A \vdash \square ((A \to B) \land A)$"
%\A "$\square (A \to B) \land \square A \vdash \square ((A \to B) \land A)$"
\A "\qquad (1)"
\A "(2) \qquad"
\B [2em] "$\square (A \to B) \land \square A \vdash \bullet B$" "(cut)"
\B [2em] "$\square (A \to B); \square A \vdash \bullet B$" "(cut)"
\U "$\square (A \to B); \square A \vdash \square B$" "($\vdash \square $)"
\U "$\square (A \to B) \vdash \square A \to \square B$" "($\vdash \to $)"

\epf
\end{center}

\caption{Proof of the K rule from \cite{wansing-sequent}}.
\label{fig:Kpf}
\end{figure}