%\section{Equivalence of Display and Shallow Nested Calculi}\label{sec:eqdlshallow}

%\section{The display calculus and the shallow nested sequent calculus}


We now prove the equivalence between the 
display calculus and the shallow nested sequent calculus.
First we defined translation functions 
\begin{verbatim}
consts
  nested_to_str :: "bool => nested => structr"
  nested_to_seq :: "nested => structr sequent"
  seq_to_nested :: "structr sequent => nested"
  str_to_nested :: "structr => nested"
\end{verbatim}
where the translation from a nested sequent to a display calculus structure
depends on whether it is in an antecedent or succedent position.

The first two of these functions convert a nested sequent to a display calculus
sequent or structure by converting `$\seq$' 
to `$\vdash$' (for \texttt{nested\_to\_seq}),
to `$>$' (for \texttt{nested\_to\_str True}), or
to `$<$' (for \texttt{nested\_to\_str False}),
and converting comma to comma.
The latter two convert `$\vdash$', `$>$', and `$<$' to `$\seq$'.

For example %\marginpar{Are the U and V themselves translated recursively?}
\texttt{nested\_to\_seq} takes $(A \seq B) \seq (C \seq D)$ to
  $A < B \vdash C > D$, and \texttt{seq\_to\_nested} does the reverse.

If we consider only the set of display calculus sequents with $<$ and $>$ in 
antecedent and succedent positions respectively (expressed by
\texttt{seq\_LtGtOK}), and
the set of nested sequents of the form $S \seq T$, then 
\texttt{nested\_to\_seq} and \texttt{seq\_to\_nested} are mutually inverse
bijections between these sets. We can express this by:

\begin{verbatim}
nest_seq_equiv : "(seq_LtGtOK ?seq & seq_to_nested ?seq = ?nes) =
      ((EX a s. ?nes = ($a => $s)) & nested_to_seq ?nes = ?seq)"
\end{verbatim}

%% THIS BIT NOW EXPLAINED ABOVE
%% where the display calculus sequent must satisfy the condition
%% \texttt{seq\_LtGtOK} which means that $<$ and $>$ symbols must be only
%% found in antecedent and succedent positions respectively, and
%% the nested sequent must be a single sequent (not a comma-separated list of
%% sequents).

%% OMIT THIS PARA - DON'T THINK WE USE IT
%% Since, in both systems, we have rules in which we explicitly substitute for
%% structure and formula variables, we also need functions which convert between a
%% substitution of display calculus structures and substitution of nested
%% sequents.  

%% \subsection{Proving the Display Calculus in the
%%   Shallow Nested Calculus}
%% \label{s-sn-dc}
%% With a lot of lemmas deriving a display calculus rule from a set of nested
%% sequent rules, like

%% \begin{lemma}
%% Consider the $\biilldc$ rule $\mldn\vdash$ for introducing $\mldn$ into the
%% antecedent shown below left and its 
%% translation under \verb!seq_to_nested! into a nested sequent rule
%% $\rho$ below middle where $\biilldc$ structures like $Z'_a$ are recursively
%% translated into $\biillsn$ Isabelle nested sequents like $Z_a$:
%% \\[15px]
%% \AxiomC{$ A \vdash Z'_a$}
%% \AxiomC{$ B \vdash Z'_b$}
%% \RightLabel{$\mldn\vdash$}
%% \BinaryInfC{$ A \mldn B \vdash Z'_a, Z'_b$}
%% \DisplayProof  
%% \qquad
%% \AxiomC{$ A \seq Z_a$}
%% \AxiomC{$ B \seq Z_b$}
%% \RightLabel{$\rho$}
%% \BinaryInfC{$ A \mldn B \seq Z_a, Z_b$}
%% \DisplayProof  
%% \qquad
%% \AxiomC{$S, \Phi \seq T$}
%% \RightLabel{$sn\_ira$}
%% \UnaryInfC{$S \seq T$}
%% \DisplayProof  
%% \\[15px]
%% If each of the Isabelle nested sequent calculus rules
%% \verb!invert sn_ira!; \ldots ; \verb!sn_pA!
%% is in the set \verb!rules'! of 
%% Isabelle nested sequent calculus rules 
%% then the Isabelle nested sequent calculus rule $\rho$
%% is derivable using the substitutional instances of  rules in 
%% \verb!rules'!.
%% \begin{verbatim}
%% sd_dands : 
%%   "[| {invert sn_ira} <= ?rules'; {invert sn_rp} <= ?rules';
%%       {sn_ora} <= ?rules'; {sn_ira} <= ?rules'; 
%%       {sn_rp} <= ?rules'; {sn_pA} <= ?rules' |]
%%      ==> ([?A => $?Za, ?B => $?Z], ?A +++ ?B => $?Za ,,, $?Z)
%%           : derl (nrulefs ?rules')"
%% \end{verbatim}
%% % sd_dands : "[| {invert sn_ira} <= ?rules';  ... |] ==>
%% %    ([?A => $?Za, ?B => $?Z], ?A +++ ?B => $?Za,,, $?Z) : derl (nrulefs ?rules')"
  
%% \end{lemma}

%% The lemma lists the rules of $\biillsn$ which are actually used in the
%% particular derivation found
%% and shows how one individual display calculus rule can
%% be derived in the shallow nested system (see \texttt{N\_Rls.ML}). 

%% Collecting the cases for all $\biilldc$ gives

%% \begin{theorem}\label{thm:prov-displ-calc-1}
%% If \verb!?r = (ps, c)! with premise list 
%% \verb!ps! and conclusion instance
%% \verb!c!
%% is an instance of a rule from the cut-free fragment
%% \verb!rlscfb!
%% of
%% $\biilldc$, then its rule instance
%% \verb!pscmap seq_to_nested ?r!
%% is derivable in the cut-free fragment
%% \verb!snb_rlscf! of~
%% $\biillsn$.
%% Moreover, for 
%% each rule \verb!(?ps, ?c)! if \verb!(?ps, ?c)! 
%% is derivable using substituitional
%% instances of cut-free
%% $\biilldc$, then its image under the mapping to 
%% nested sequents
%% is derivable using substitutional instances of cut-free $\biillsn$.

%% \begin{verbatim}
%% tr_rules_dc_snb : "?r : rulefs rlscfb 
%%    ==> pscmap seq_to_nested ?r : derl (nrulefs snb_rlscf)"
%% tr_derl_dc_snb : "(?ps, ?c) : derl (rulefs rlscfb) ==>
%%    pscmap seq_to_nested (?ps, ?c) : derl (nrulefs snb_rlscf)"
%% \end{verbatim}
%% See the file \texttt{Dc\_Sn.ML}.
%% \end{theorem}
%% % that is, each $\biilldc$ rule, when mapped to a $\biillsn$ rule,
%% % is derivable in $\biillsn$, and
%% % then that each derived rule of $\biilldc$, when mapped to a $\biillsn$ rule,
%% % is derivable in $\biillsn$.

%% \subsection{Proving the Shallow Nested Sequent Calculus 
%%   in the Display Calculus}
%% \label{s-dc-sn}

%% In this case we get a set of results which show that an individual
%% shallow nested calculus rule can be proved in the display calclus (see
%% \texttt{F\_Rls.ML}).

%% \begin{lemma}
%% If each of the $\biilldc$ rules
%% \verb!invert drp, invert rp ...!
%% is in the set \verb!rules'! of 
%% display calculus rules 
%% and $\rho$ is the image under
%% \verb!nested_to_seq!
%% of the nested sequent calculus rule 
%% $\mlcn_r$
%% then the display calculus rule $\rho$
%% is derivable using the substitutional instances of  rules in 
%% \verb!rules'!.

%% \begin{verbatim}
%% ds_dands : 
%%  "[| {invert drp} <= ?rules'; {invert rp} <= ?rules'; ... |] 
%%      ==> 
%%      ([$?Za |- ?A,, $?Ya, $?Z |- ?B,, $?Y],
%%        $?Za,, $?Z |- ?A && ?B,, ($?Ya,, $?Y)) : derl (rulefs ?rules')"
%% \end{verbatim}
%% \end{lemma}

%% Collecting them together we are able to prove
%% \begin{theorem}
%% If \verb!?r = (ps, c)! with premise list 
%% \verb!ps! and conclusion instance
%% \verb!c!
%% is an instance of a rule from the cut-free fragment
%% \verb!snb_rlscf!
%% of
%% $\biillsn$, then its rule instance
%% \verb!pscmap nested_to_seq ?r!
%% is derivable in the cut-free fragment
%% \verb!rlscfb! of~$\biilldc$.
%% Moreover, for 
%% each rule \verb!(?ps, ?c)!, if \verb!(?ps, ?c)! 
%% is derivable using substituitional
%% instances of cut-free
%% $\biillsn$, then its image under the mapping to 
%% display sequents
%% is derivable using substitutional instances of cut-free $\biilldc$.
%% \begin{verbatim}
%%  tr_rules_snb_dc : "?r : nrulefs snb_rlscf 
%%       ==> pscmap nested_to_seq ?r : derl (rulefs rlscfb)"
%%  tr_derl_snb_dc : "(?ps, ?c) : derl (nrulefs snb_rlscf) 
%%       ==> pscmap nested_to_seq (?ps, ?c) : derl (rulefs rlscfb)" 
%% \end{verbatim}
%% % that is, each $\biillsn$\ rule, when mapped to a $\biilldc$ rule,
%% % is derivable in $\biilldc$, and
%% % then that each derived rule of $\biillsn$,
%% % when mapped to a $\biilldc$ rule, is derivable in $\biilldc$.  
%% See the file \texttt{Dc\_Sn.ML}.
%% \end{theorem}

%% \begin{theorem}
%% \label{thm:biill-sn-eq-dc}
%% A formula is cut-free $\biillsn$-provable iff it is cut-free
%% $\biilldc$-provable.
%% \end{theorem}

%% The proof of Theorem~\ref{thm:biill-sn-eq-dc} used the near-equivalence
%% of provability of sequents in the two systems, given by the theorems
%% \texttt{tr\_der\_dc\_snb} and \texttt{tr\_der\_snb\_dc},
%% as described in \S\ref{s-sn-dc} and \S\ref{s-dc-sn} above.
%% The version \texttt{dc\_sn\_equiv\_alt} below was straightforward to prove;
%% the version \texttt{dc\_sn\_equiv} requires the invertibility in the
%% display calculus of the left-introduction rule for \texttt{T}, ie
%% $\tunit$. Note that there no translation applied 
%% because formulae are the same in both calculi


The proof systems $\biilldc$ and $\biillsn$ are very similar. 
In fact, their structural rules are the same (modulo some notational variance).
The only difference is that $\biilldc$ requires that introduction rules
be applied only to a `displayed' formula, i.e., the principal formula
must appear in isolation either on the left or on the right of the turnstile.
Their equivalence is not really surprising, so we state their equivalence here
and refer the reader to Isabelle proof scripts for details.
\begin{theorem}
The display sequent $A \vdash B$ is cut-free $\biilldc$-derivable iff
the nested sequent $A \seq B$ is cut-free $\biillsn$-derivable.
The display sequent $\mltp \vdash A$ is cut-free $\biilldc$-derivable iff
the nested sequent $ \seq B$ is cut-free $\biillsn$-derivable.
\begin{verbatim}
dc_sn_equiv_alt = "((?A |- ?B) : derrec (rulefs rlscfb) {}) =
         ((?A => ?B) : derrec (nrulefs snb_rlscf) {})"
dc_sn_equiv : "((T |- ?A) : derrec (rulefs rlscfb) {}) =
         (($NI => ?A) : derrec (nrulefs snb_rlscf) {})"
\end{verbatim}
\end{theorem}

%% \begin{theorem}
%% \label{thm:cut-elim-biillsn}
%% All substitutional instances of the cut rule are admissible in $\biillsn.$
%% \begin{verbatim}
%% sn_cut_adm : "nrulefs {sn_cutr} <= adm (nrulefs snb_rlscf)"
%% \end{verbatim}
%% \end{theorem}

%% The last is an actual cut admissibility proof based on that for
%% display calculi. It is not just a consequence of various previous
%% theorems.

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