\section{Formalising  Display Calculi}\label{sec:dl}

\begin{figure}[t]
  \begin{tabular}[c]{l@{\extracolsep{3cm}}l}
\multicolumn{2}{l}{Cut and identity:}
  \\[0px]
  \qquad
  \AxiomC{(id)\quad$p\turn p$}
  \DisplayProof
  &
  \AxiomC{$X\turn A$}
  \AxiomC{$A\turn Y$}
  \LeftLabel{(cut)\,}
  \BinaryInfC{$X\turn Y$}
  \DisplayProof
\\%[5px]
\multicolumn{2}{l}{Logical rules:}
\\[0px]
  \quad
  \AxiomC{$\Phi\turn X$}
  \LeftLabel{($I\turn$)\,}
  \UnaryInfC{$I\turn X$}
  \DisplayProof
  \quad
  \AxiomC{($\bot\turn$)\quad$\bot\turn\Phi$}
  \DisplayProof
  &
  \AxiomC{($\turn I$)\quad$\Phi\turn I$}
  \DisplayProof
  \quad
  \AxiomC{$X\turn\Phi$}
  \LeftLabel{($\turn\bot$)\,}
  \UnaryInfC{$X\turn\bot$}
  \DisplayProof
\\[10px]
  \quad
  \AxiomC{$A,B\turn X$}
  \LeftLabel{($\otimes\turn$)\,}
  \UnaryInfC{$A\otimes B\turn X$}
  \DisplayProof
  &
  \AxiomC{$X\turn A$}
  \AxiomC{$Y\turn B$}
  \LeftLabel{($\turn\otimes$)\,}
  \BinaryInfC{$X,Y\turn A\otimes B$}
  \DisplayProof
\\[10px]
  \quad
  \AxiomC{$A\turn X$}
  \AxiomC{$B\turn Y$}
  \LeftLabel{($\parr\turn$)\,}
  \BinaryInfC{$A\parr B\turn X,Y$}
  \DisplayProof
  &
  \AxiomC{$X\turn A,B$}
  \LeftLabel{($\turn\parr$)\,}
  \UnaryInfC{$X\turn A\parr B$}
  \DisplayProof
\\[10px]
  \quad
  \AxiomC{$X\turn A$}
  \AxiomC{$B\turn Y$}
  \LeftLabel{($\limp\turn$)\,}
  \BinaryInfC{$A\limp B\turn X>Y$}
  \DisplayProof
  &
  \AxiomC{$X\turn A>B$}
  \LeftLabel{($\turn\limp$)\,}
  \UnaryInfC{$X\turn A\limp B$}
  \DisplayProof
\\[10px]
  \quad
  \AxiomC{$A<B\turn X$}
    \LeftLabel{($\excl\turn$)\,}
  \UnaryInfC{$A\excl B\turn X$}
  \DisplayProof
  &
  \AxiomC{$X\turn A$}
  \AxiomC{$B\turn Y$}
  \LeftLabel{($\turn\excl$)\,}
  \BinaryInfC{$X<Y\turn A\excl B$}
  \DisplayProof
\\
\multicolumn{2}{l}{Structural rules:}
\\[5px]
\multicolumn{2}{c}{
  \AxiomC{$X\turn Y>Z$}
  \doubleLine
  \LeftLabel{(rp)\,}
  \UnaryInfC{$X,Y\turn Z$}
  \DisplayProof
  \quad
  \AxiomC{$X, Y \turn Z$}
  \doubleLine
  \LeftLabel{(rp)\,}
  \UnaryInfC{$Y\turn X>Z$}
  \DisplayProof
  \quad
  \AxiomC{$X<Y\turn Z$}
  \doubleLine
  \LeftLabel{(drp)\,}
  \UnaryInfC{$X\turn Y,Z$}
  \DisplayProof
  \quad
  \AxiomC{$X \turn Y,Z$}
  \doubleLine
  \LeftLabel{(drp)\,}
  \UnaryInfC{$X<Z\turn Y$}
  \DisplayProof
}
\\[10px]
\multicolumn{2}{c}{
  \AxiomC{$X,\Phi\turn Y$}
  \doubleLine
  \LeftLabel{($\Phi\turn$)\,}
  \UnaryInfC{$X\turn Y$}
  \DisplayProof
 \quad
  \AxiomC{$X\turn \Phi,Y$}
  \doubleLine
  \LeftLabel{($\turn\Phi$)\,}
  \UnaryInfC{$X\turn Y$}
  \DisplayProof 
 \quad
  \AxiomC{$X,Y\turn Z$}
  \LeftLabel{(Com $\turn$)\,}
  \UnaryInfC{$Y,X\turn Z$}
  \DisplayProof
  \quad
  \AxiomC{$X\turn Y,Z$}
  \LeftLabel{($\turn$ Com)\,}
  \UnaryInfC{$X\turn Z,Y$}
  \DisplayProof
}
\\[10px]
  \quad
  \AxiomC{$W,(X,Y)\turn Z$}
  \doubleLine
  \LeftLabel{(Ass $\turn$)\,}
  \UnaryInfC{$(W,X),Y\turn Z$}
  \DisplayProof
  &
  \AxiomC{$W\turn (X,Y),Z$}
  \doubleLine
  \LeftLabel{($\turn$ Ass)\,}
  \UnaryInfC{$W\turn X,(Y,Z)$}
  \DisplayProof
%% \\[10px]
%%   \quad
%%   \AxiomC{$X,Y\turn Z$}
%%   \LeftLabel{(Com $\turn$)\,}
%%   \UnaryInfC{$Y,X\turn Z$}
%%   \DisplayProof
%%   &
%%   \AxiomC{$X\turn Y,Z$}
%%   \LeftLabel{($\turn$ Com)\,}
%%   \UnaryInfC{$X\turn Z,Y$}
%%   \DisplayProof
\\[10px]
% \multicolumn{2}{c}{
%   \AxiomC{$W\vdash (X> Y), Z$}
%     \LeftLabel{(Grnb)}
%   \UnaryInfC{$W\vdash X>(Y,Z)$}
% \DisplayProof
% }
  \quad
  \AxiomC{$W,(X<Y)\turn Z$}
    \LeftLabel{(Grnb $\turn$)}
  \UnaryInfC{$(W,X)<Y\turn Z$}
  \DisplayProof
  &
  \AxiomC{$W\vdash (X> Y), Z$}
    \LeftLabel{($\turn$ Grnb)}
  \UnaryInfC{$W\vdash X>(Y,Z)$}
\DisplayProof
  \end{tabular}
\caption{$\filldc$ and $\biilldc$: display calculi for FILL and BiILL}
\label{Fig:dc}
\end{figure}

Our formalisation of the display calculus $\biilldc$ is very similar to that 
in~\cite{DBLP:conf/tphol/DawsonG02},  
so we shall not go into details of the formalisation
and refer the reader instead to \cite{DBLP:conf/tphol/DawsonG02}. 
The display system $\biilldc$ is given in Figure~\ref{Fig:dc}, where 
double-lined inference rules are invertible.
The display calculus $\filldc$ is obtained from $\biilldc$ by removing
the introduction rules for $\excl.$

As in our previous formalisation~\cite{DBLP:conf/tphol/DawsonG02}, 
structure variables like $X$ are
encoded as \verb!$"X"! and formula variables like $A$ are encoded as
\verb!"A"!. The quotes are necessary since we handle substitutions
explicitly rather than via Isabelle variables~\cite{DBLP:conf/tphol/DawsonG02}.
For example, the cut rule is encoded as:
\begin{verbatim}
 cutr == ([($"X" |- "A"), ("A" |- $"Y")], ($"X" |- $"Y"))
\end{verbatim}


%% NOTE - Following theorem is true, but we don't prove it formally 
%% \begin{theorem}[Display Property]\label{thm:display}
%%  For every structure $Z$ which is an antecedent (resp. succedent)
%%  part of the sequent $X \turn Y$, there is a sequent $Z \turn Y'$
%%  (resp. $X' \turn Z$) obtainable from $X \turn Y$ using only (rp) and
%%  (drp), thereby displaying the $Z$ as the whole of one side.
%% \end{theorem}

%% \begin{theorem}[Cut-Admissibility Effective]\label{thm:cutad}
%%   From cut-free $\biilldc$-derivations of $X \turn A$ and 
%%   $A \turn Y$ there is an effective procedure to obtain
%%   a cut-free $\biilldc$-derivation of $X
%%   \turn Y$.
%% \end{theorem}

To prove the cut-admissibility result we largely reuse the code we
used to prove cut-admissibility for the display calculus for relation
algebras~\cite{DBLP:conf/tphol/DawsonG02}. 
The proof that a connective satisfies Belnap's C8 condition had to be coded in part
individually for each connective, but, even so, we were able to reuse
most of our previous code. Each display logic rule of $\biilldc$ is
encoded as shown above for cut, giving \verb!rlsb!, and its
strict subset \verb!rlscfb! which excludes the cut rule.

Given a set \texttt{S} of encoded rules, the set \texttt{rulefs S} is
the (infinite) set of substitutional instances of members of
\texttt{S}.  From our previous work~\cite{DBLP:conf/lpar/DawsonG10},
the rule \texttt{(ps, c)} with list of premise (sequents) \texttt{ps}
and conclusion (sequent) \texttt{c} is an admissible rule of
\texttt{S} if the following holds, where colon is
set-membership $\in$:
\begin{verbatim}
(?ps : dersrec ?rls {} --> ?c : derrec ?rls {})
 ==> (?ps, ?c) : adm ?rls
\end{verbatim}

We then proved cut-admissibility as below where colon now simply states
the name of the theorem:
\begin{theorem}[Cut-Admissibility]\label{thm:cutad-verif}
  From cut-free $\biilldc$-derivations of $X \turn A$ and 
  $A \turn Y$ we can obtain
  a cut-free $\biilldc$-derivation of $X
  \turn Y$.
\begin{verbatim}
dc_cut_adm : "rulefs {cutr} <= adm (rulefs rlscfb)"
\end{verbatim}
\end{theorem}

%% Note the subtle difference between the theoretical
%% Theorem~\ref{thm:cutad} and our verified Theorem~\ref{thm:cutad-verif}
%% which only surfaces when formalising mathematical theorems: 

%% Note that we have not actually verified that there is an effective procedure 
%% for cut-elimination, since we have not formalised the notion of effective procedure. That is, the effective procedure is implicit since it is precisely the method of
%% the Isabelle proof.

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "root"
%%% End: 
