\section{Display Logic} \label{dl}

\subsection{Introduction}

A number of different logical systems can be formulated using the
method, or style, of Display Logic \cite{Bel}.
These include several normal modal logics \cite{Wansing},
and intuitionistic logic \cite{ILR}.
Display Logic resembles the Gentzen sequent calculus \textbf{LK},
but with significant differences.
For example, the rule for introducing the connective `$\lor$' 
(on the left) in \textbf{LK} and its counterpart in Display Logic are
\begin{equation} \label{v|-1}
 \frac {\Gamma, A \vdash \Delta \quad \Gamma, B \vdash \Delta }
  {\Gamma, A \lor B \vdash \Delta } (\mbox{\textbf{LK}-}\lor \vdash )
\qquad %\textrm{ and }
\qquad 
 \frac {A \vdash Z \quad B \vdash Z }
  {A \lor B \vdash Z } (\mbox{DL-}\lor \vdash )
\end{equation}
Whereas, in \textbf{LK},
$\Gamma$ and $\Delta$ denote comma-separated lists of formulae,
in Display Logic, $Z$ denotes a Display Logic \emph{structure}.
A {structure} is defined as a formula, %or a structure variable,
or a combination of structures formed using the \emph{structural operators}
(one of which is `,').
%Conventionally we use $X,Y,Z,W,\ldots$ as variables denoting structures.
%which can involve several \emph{structural} operators (one of which is `,').
Informally, \emph{formulae} and \emph{formula} (or \emph{logical})
\emph{operators} are the 
formulae and operators of the logic being displayed, 
whereas the structural operators are additional operators used in
presenting that logic as a display logic. 
(See \cite{dRA} or \cite{thesis}
for a full explanation of \emph{structures} and \emph{formulae}).
In Display Logic, unlike in \textbf{LK},
the introduced formula (here, $A \lor B$) stands by itself
on one side of the turnstile;
this is generally the case with 
Display Logic rules.
%the ``logical introduction rules''
%(ie, the rules which introduce the logical operators,
%eg DL-$\vdash \lor$ above).
However there are also rules (the ``display postulates'')% described below)
which effectively allow moving substructures from one side to the other.
All display postulates are bi-directional (invertible) rules.

In Display Logic,
in terms of backwards proof, the ``logical introduction rules''
eliminate the logical (formula) operators and replace them with corresponding
structural operators.
For example, rules for introducing the $\lor$ operator are shown.
Note that the ($\lor \vdash $) rule shown below is different from the one
above; in some Display Logics they both hold.
\begin{equation} \label{v|-2}
\mbox{\slrule {A \vdash X \quad B \vdash Y }
{A \lor B \vdash X,Y } ($\lor \vdash $)} \qquad\qquad
\mbox{\slrule {Z \vdash A,B } {Z \vdash A \lor B } ($\vdash \lor $)}
\end{equation}

A display logic will also have some ``basic structural rules'',
which are expressed in terms of structural connectives only, and
which capture properties of the logic and its logical operators.
For example, the following rules express the associativity of 
$\land$ and $\lor$
(the double line means the rule is bi-directional).
$$
\mbox{\invrule {X,(Y,Z) \vdash W} {(X,Y),Z \vdash W} ($A \vdash$)} \qquad\qquad
\mbox{\invrule {W \vdash X,(Y,Z) } {W \vdash (X,Y),Z } ($\vdash A$)}
$$

As an alternative to writing a rule with one premise $\mathcal P$ and a
conclusion $\mathcal C$ separated by a horizontal line, we often write 
$\mathcal P \Longrightarrow \mathcal C$, and 
for a bi-directional rule we often write 
$\mathcal P \Longleftrightarrow \mathcal C$.
For a full explanation of Display Logic see, for example, \cite{dRA}.

By way of example,
the Display Logic formulation of classical propositional logic has
structural operators `,' `$*$' `$I$' .
As in \textbf{LK}, `,' is used to stand for either `$\land$' or `$\lor$';
which one it is
depends not only on which side of the `$\vdash$' the `,' appears, 
but also on the number of `*' operators in whose scope the `,' lies. 
This reflects the duality between `$\land$' and `$\lor$',
as expressed by DeMorgan's laws.
Each structural operator stands for one, or two (depending on the position),
formula operators.
Thus `$I$' stands for truth or falsity, 
`$*$' for Boolean negation and `$,$' for `$\land$' or `$\lor$'.
The logical identity
$A \land B \Rightarrow C \iff A \Rightarrow C \lor \lnot B$
(which is an example of ``residuation'', explained below)
becomes an instance of the display postulate 
$ \displaystyle X,Y \vdash Z \iff X \vdash Z, *Y$
and 
$ \lnot A \Rightarrow B \iff \lnot B \Rightarrow A$
becomes an instance of 
$ \displaystyle  * X \vdash Y \iff * Y \vdash X$.

\comment{
The logical identities
$$A \land B \Rightarrow C \iff A \Rightarrow C \lor \lnot B
\qquad \qquad 
 \lnot A \Rightarrow B \iff \lnot B \Rightarrow A$$
become the display postulates
$$ \displaystyle A,B \vdash C \iff A \vdash C, *B
\qquad \qquad 
 \displaystyle  * A \vdash B \iff * B \vdash A$$
These are examples of ``residuation''.
}

\subsection{Residuation} \label{DL-resid}

As noted in \S\ref{intl}, 
Display Logic does not have equalities or inverses;
the fact that any chosen substructure can be displayed
depends on the notion of \emph{residuation}.

Consider a partially ordered set, with binary functions $s$, $f$ and $g$.
To say that $f$ and $g$ are \emph{residuals} of $s$ means
that the following hold (for all $a$, $b$ and $c$)
$$s(a,b) \leq c \iff a \leq f(c,b)$$
$$s(a,b) \leq c \iff b \leq g(a,c)$$
(see \cite{Dunn}, \S6, or \cite{sdpr})
These equivalences have the effect of ``displaying'' $a$ and $b$ respectively.
When all the connectives used in a proposition have residuals, 
any subterm can be displayed.
If we then have a rule which partly instantiates to 
$a \leq X \Longrightarrow a' \leq X$,
we can form a proof as follows.
\begin{center}
\vpf
\bpf
\A "$s(a,b) \leq c$"
\U "$a \leq f(c,b)$"
\U "$a' \leq f(c,b)$"
\U "$s(a',b) \leq c$"
\epf
\end{center}
We have in effect rewritten the subterm $a$ (located in an arbitrary position)
to $a'$.
This is the manner in which we rewrite arbitrarily chosen substructures
in Display Logic.

Note that for the proof above, we required  
only $a \leq X \Longrightarrow a' \leq X$,
not $a \leq X \Longleftrightarrow a' \leq X$.
That is, $a'$ may be a strictly stronger proposition than $a$.
Effectively, doing subterm rewrites this way also allows a subterm to be
replaced by one that is logically either
stronger or weaker, according to the subterm's position.

\subsection{Rewriting} \label{DL-rewr}

It will be noted that among the examples above, 
both the basic structural rules ($A \vdash$)
and ($\vdash A$), and the logical introduction rule ($\vdash \lor$)
have on one side a single structural variable 
(which can stand for any structure,
including any formula) which remains unchanged;
the expression being ``rewritten'' appears on the other side.
This is typical of many rules.
In some other cases, rules of this form can be derived.
For example, if the rule for ($\lor \vdash $) given in the logic
is that shown at (\ref{v|-2}),
it may be possible to derive the version given at (\ref{v|-1}).

The following example shows this rule being used.
The first (bottom) step is to display the disjunction $A \lor C$
(``dp'' denotes ``display postulate(s)'');
then the ($\lor \vdash $) rule is applied (which splits the branch of the
proof tree).
Finally, the display postulate(s) which were used to display $A \lor C$
are reversed (in both branches).
This last step relies on the fact that the ($\lor \vdash $) rule 
leaves the term on the right of the `$\vdash$' unchanged.
Notice that the required display postulates move $A \lor C$
to the left, so the introduction rule needed is that for 
introducing $\lor$ on the \emph{left}.

\vpf
\begin{center}
\bpf
\A "$D \vdash * A, B$"
\U "$A \vdash * (D, * B)$" "(dp)"
\A "$D \vdash * C, B$"
\U "$C \vdash * (D, * B)$" "(dp)"
\B [2em] "$A \lor C \vdash * (D, * B)$" "($\lor \vdash $)"
\U "$D \vdash * (A \lor C), B$" "(dp)"
\epf
\end{center}

An example of several steps of this form follows.
The rules used are %(from bottom up)
the logical introduction rules 
($\vdash \to $), ($\to \vdash $), ($\land \vdash $) and ($\lnot \vdash $),
distribution of `$*$' over `,' (ie, DeMorgan's law),
and double negation elimination.
\vpf
\begin{center}
\bpf
\A "$* C \vdash * C, A, B$"
\U "$* C \vdash * C, * * A, B$" "($\vdash **$)"
\U "$* C \vdash * C, * \lnot A, B$" "($\lnot \vdash $)"
\U "$* C \vdash * (\lnot A, C), B$" "($\vdash$*-,-dist)"
\U "$* C \vdash * (\lnot A \land C), B$" "($\land \vdash $)"

\A "$A \vdash * C, A, B$"
\U "$A \vdash * C, * * A, B$" "($\vdash **$)"
\U "$A \vdash * C, * \lnot A, B$" "($\lnot \vdash $)"
\U "$A \vdash * (\lnot A, C), B$" "($\vdash$*-,-dist)"
\U "$A \vdash * (\lnot A \land C), B$" "($\land \vdash $)"
\B [2em] "$C \to A \vdash * (\lnot A \land C), B$" "($\to \vdash $)"
\U "$C \to A \vdash \lnot A \land C \to B$" "($\vdash \to $)"

\epf
\end{center}

The tactics can be programmed to perform the above steps one at a time,
or all in one step; observe that if a proof rule splits a branch of the proof
tree, the search-and-rewrite process continues on each branch independently. 
We now describe how this is implemented in Isabelle.

\subsection{Implementation in Isabelle} \label{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 \S\ref{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 A.
\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 
\S\ref{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 \S\ref{LPF-impl} it is easy to create more. %in fact \texttt{ELSEaf} and
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}.