\section{Deep Nested Sequent Calculi} %\label{sec:deep}
\label{sec:eqshallowdeep}


\begin{figure}[t]
{\small
Propagation rules:
$$
\infer[pl_1]
{X[\Sc, A \seq (\Sc' \seq \Tc'), \Tc]}
{
 X[\Sc \seq (A, \Sc' \seq \Tc'), \Tc]
}
\qquad
\infer[pr_1]
{X[(\Sc \seq \Tc), \Sc' \seq A, \Tc']}
{X[(\Sc \seq \Tc, A), \Sc' \seq \Tc']}
$$
$$
\infer[pl_2]
{X[\Sc, (\Sc', A \seq \Tc') \seq \Tc]}
{X[\Sc, A, (\Sc' \seq \Tc') \seq \Tc]}
\qquad
\infer[pr_2]
{X[\Sc \seq \Tc, (\Sc' \seq \Tc', A)]}
{X[\Sc \seq \Tc, A, (\Sc' \seq \Tc')]}
$$

Identity and logical rules: In branching rules, $X[~] \in X_1[~] \merge X_2[~]$,
$\Sc \in \Sc_1 \merge \Sc_2$ and $\Tc \in \Tc_1 \merge \Tc_2$.
$$
\infer[id^d]
{X[\Uc, p \seq p, \Vc]}
{\mbox{$X[~]$, $\Uc$ and $\Vc$ are hollow.}}
\quad
\infer[\punit_l^d]
{X[\punit, \Uc \seq \Vc]}
{\mbox{$X[~]$, $\Uc$ and $\Vc$ are hollow. }}
\quad
\infer[\punit_r^d]
{X[\Sc \seq \Tc, \punit]}
{X[\Sc \seq \Tc]}
$$
$$
\infer[\tunit_l^d]
{X[\Sc, \tunit \seq \Tc]}
{X[\Sc \seq \Tc]}
\qquad
\infer[\tunit_r^d]
{X[\Uc \seq \tunit, \Vc]}
{\mbox{$X[~]$, $\Uc$ and $\Vc$ are hollow. }}
$$
$$
\infer[\ltens_l^d]
{X[\Sc, A \ltens B \seq \Tc]}
{X[\Sc, A, B \seq \Tc]}
\qquad
\infer[\ltens_r^d]
{X[\Sc \seq A \ltens B, \Tc]}
{X_1[\Sc_1 \seq A, \Tc_1] & X_2[\Sc_2 \seq B, \Tc_2]}
$$
$$
\infer[\limp_l^d]
{X[\Sc, A \limp B \seq \Tc]}
{
X_1[\Sc_1 \seq A, \Tc_1] & X_2[\Sc_2, B \seq \Tc_2]
}
\qquad
\infer[\limp_r^d]
{X[\Sc \seq \Tc, A \limp B]}
{X[\Sc \seq \Tc, (A \seq B)]}
$$
$$
\infer[\parr_l^d]
{X[\Sc, A \parr B \seq \Tc]}
{
 X_1[\Sc_1, A \seq \Tc_1]
 &
 X_2[\Sc_2, B \seq \Tc_2]
}
\qquad
\infer[\parr_r^d]
{X[\Sc \seq A \parr B, \Tc]}
{X[\Sc \seq A, B, \Tc]}
$$
$$
\infer[\excl_l^d]
{X[\Sc, A \excl B \seq \Tc]}
{X[\Sc, (A \seq B) \seq \Tc]}
\qquad
\infer[\excl_r^d]
{X[\Sc \seq A \excl B, \Tc]}
{X_1[\Sc_1 \seq A, \Tc_1] 
&
 X_2[\Sc_2, B \seq \Tc_2]
}
$$
}
\caption{The deep inference system $\biilldn$. }
% \caption{The deep inference system $\biilldn$. In branching rules, $X[~] \in X_1[~] \merge X_2[~]$,
% $\Sc \in \Sc_1 \merge \Sc_2$ and $\Tc \in \Tc_1 \merge \Tc_2$.}
\label{fig:fbilld}
\end{figure}

\begin{figure}[t]
{\small
  \begin{tabular}[c]{lcl}
  \multicolumn{3}{l}{  
     If $X_1[~] = [~]$ and $X_2[~] = [~]$ 
     then $X_1[~] \merge X_2[~] = \{ [~] \}$
   }
\\
    If $X_1[~]$ & $=$ &
          $(\Gamma_1, Y_1[~], P_1,\dots,P_m \seq \Delta_1, Q_1,\dots,Q_n)$
    and
\\
    \hphantom{If} $X_2[~]$ & $=$ &
          $(\Gamma_2, Y_2[~], S_1,\dots,S_m \seq \Delta_2, T_1,\dots,T_n)$
   then
\\
   $X_1[~] \merge X_2[~]$ & $=$ &
      $\{~ (\Gamma_1, \Gamma_2, Y[~], U_1,\dots,U_m \seq \Delta_1,\Delta_2,
          V_1,\dots,V_n)~~ \mid$
\\
   & &
        $
        \begin{array}{l} 
         Y[~] \in Y_1[~]\merge Y_2[~] 
        \mbox{ and }
        U_i \in P_i \merge S_i 
        \mbox{ for } 
        1 \leq i \leq m
        \mbox{ and } \\
        V_j \in Q_j \merge T_j
        \mbox{ for } 
        1 \leq j \leq n 
       ~\}
        \end{array}$
%  \end{tabular}
\\
%  \begin{tabular}[c]{lcl}
    If $X_1[~]$ & $=$ & $(\Gamma_1, P_1,\dots,P_m \seq \Delta_1, Y_1[~], Q_1,\dots,Q_n)$
    and
    \\
    \hphantom{If} $X_2[~]$ & $=$ & $(\Gamma_2, S_1,\dots,S_m \seq \Delta_2, Y_2[~], T_1,\dots,T_n)$
    then
    \\
    $X_1[~] \merge X_2[~]$ & $=$ & 
    $\{~
      (\Gamma_1, \Gamma_2, U_1,\dots,U_m \seq \Delta_1,\Delta_2, Y[~],
       V_1,\dots,V_n)$ $\mid$
    \\
     & &
    $\begin{array}{l}
     Y[~] \in Y_1[~]\merge Y_2[~] \mbox{ and }
     U_i \in P_i \merge S_i \mbox{ for } 1 \leq i \leq m \mbox{ and }\\
     V_j \in Q_j \merge T_j$ for $1 \leq j \leq n ~\}
     \end{array}
    $
  \end{tabular}
}
\caption{Merging of contexts}
\label{fig:merge}
\end{figure}

%% A nested sequent $X$ (resp. a context $X[~]$) is said to be {\em
%%   hollow} iff it contains no occurrences of formulae.  For example,
%% $(\sunit \seq \sunit) \seq (\sunit \seq [~]), (\sunit \seq \sunit)$ is
%% a hollow context.

%% The deep inference system $\biilldn$ for $\biill$
%% is given in Fig.~\ref{fig:fbilld}. 
%% Merging of sequents and contexts (denoted by $\merge$) is explained below.

%\subsection{Applying a context to a rule}

\emph{Deep} inference rules for nested sequents 
are applied in a {\em context}, i.e., a
nested sequent with a hole $[~]$.
% We need to define several notions of contexts in our formalisation. 
We use several notions of contexts in our formalisation. 
The first two accept a set of nested
sequent rules and return a set of nested sequent rules while the
third accepts and returns a set of Isabelle nested sequents 
%and returns a set of Isabelle nested sequents
{\small
\begin{verbatim}
  ctxt :: "nested psc set => nested psc set"
  dctxt :: "nested psc set => nested psc set"
  hctxt :: "nested set => nested set"
\end{verbatim}
}
\noindent For example, if $([P], C) \in R$, where $[P]$ 
is a singleton list (rather than a context)
containing one premise, then
$([X[P]], X[C]) \in \texttt{ctxt}\ R$ is also a single premise rule.
Likewise, if $C \in R$ and $X[~]$ is a hollow context then 
$X[C] \in \texttt{hctxt}\ R$.

Some of the proofs involving \texttt{ctxt} were easier using a related
definition \texttt{dctxt} where $X[S \seq T]$ means adding nested sequents to
$S$ or to $T$, rather than to $S \seq T$.
For example, if
 $([P_1 \seq P_2], (C_1 \seq C_2)) \in \texttt{dctxt}\ R$, then 
 $([P_1, X \seq P_2], (C_1, X \seq C_2)) \in \texttt{dctxt}\ R$.
Similarly,
if $([P_1 \seq P_2], (C_1 \seq C_2)) \in \texttt{dctxt}\ R$
then
$([(P_1 \seq P_2) \seq X], ((C_1 \seq C_2) \seq X)) \in \texttt{dctxt}\ R$
% turns into $(X \seq Y) \seq Z$ and ditto for
% conclusion.

%% Some proofs were easier using this formulation.
%% We needed lemmas like the following, and also \texttt{dc\_anda} 
%% (see \S\ref{s-one-prem-log}). 
%% \begin{verbatim}
%% nseqs_ctxt_dctxt : "([$?pa => $?ps], $?ca => $?cs) : ctxt ?R ==>
%%    ([$?pa => $?ps], $?ca => $?cs) : dctxt ?R"
%% \end{verbatim}

% \subsection{Alternative formulations of \texttt{ctxt} or \texttt{dctxt}}
%   \label{s-alt-dc}
%   PROBABLY OMIT
% Initially we used the following introduction clauses as the base cases for the
% inductive definitions of \texttt{ctxt} and \texttt{dctxt}.
% \begin{verbatim}
% same "r : rs ==> r : ctxt rs"
% same "r : rs ==> r : dctxt rs"
% \end{verbatim}
% We contemplated changing these to
% \begin{verbatim}
% same "([Xp], Xc) : rs ==> ([Xp], Xc) : ctxt rs"
% same "([$Yp => $Zp], $Yc => $Zc) : rs ==>  
%       ([$Yp => $Zp], $Yc => $Zc) : dctxt rs"
% \end{verbatim}
% because we find that only in the base cases can we get 
% $r \in \texttt{ctxt}\ rs$ or 
% $r \in \texttt{dctxt}\ rs$ for any $r$ not in the form shown (ie, where
% $r$ has a single premise and, for \texttt{dctxt}, $r$ contains nested
% sequents).
% We experimented with making this change, which would give us that always if
% $r \in \texttt{ctxt}\ rs$ or $r \in \texttt{dctxt}\ rs$ then $r$ has this form
% (without assuming that rules in $rs$ have this form).
% But we would then lose certain useful properties, such as 
% \begin{verbatim}
% in_ctxt_derl : "(?ps, ?c) : derl ?pscrel ==>
%   (?ps, ?c) : derl (ctxt ?pscrel)"
% \end{verbatim}
% And, more importantly, \texttt{nseqs\_ctxt\_dctxt} (see above)
% would no longer hold.

%\subsection{Merging nested sequents}

The nested sequent system $\biilldn$ is given in Fig.~\ref{fig:fbilld}.
% Notice that structural rules are missing from $\biilldn$.
Notice that it lacks the structural rules.
The zero-premise rules 
require that certain sequents or contexts are {\em hollow}, i.e., contain
no occurrences of formulae.
The branching rules require operations to merge contexts
and nested sequents, which are explained below.

The {\em merge set} $X_1 \merge X_2$ of two sequents $X_1$ and $X_2$
is defined as:
\begin{center}
\begin{tabular}[c]{l@{\extracolsep{1cm}}cl}
% $X_1 \merge X_2 = $
 \multicolumn{3}{l}{
  $X_1 \merge X_2 = \{~ 
   (\Gamma_1, \Gamma_2, Y_1, \dots, Y_m \seq \Delta_1, \Delta_2, Z_1,
    \dots, Z_n) ~\mid$
 }
\\
  & & $X_1 = (\Gamma_1, P_1, \dots, P_m \seq \Delta_1, Q_1,\dots,Q_n)$
  \mbox{ and }
\\
  & & 
  $X_2 = (\Gamma_2, S_1, \dots, S_m \seq \Delta_2, T_1, \dots, T_n)$
 \mbox{ and }
\\
 & &
  $Y_i \in P_i \merge S_i$ for $1 \leq i \leq m$ 
  and $Z_j \in Q_j \merge T_j$ for $1 \leq j \leq n$
  $~\}$
\end{tabular}
\end{center}

The merge set $X_1[~] \merge X_2[~]$ of 
two contexts $X_1[~]$ and $X_2[~]$ is defined in Figure~\ref{fig:merge}.
If $X[~] = X_1[~] \merge X_2[~]$ we say $X_1[~]$ and $X_2[~]$
are a {\em partition} of $X[~]$.
We extend the notion of a merge set between multisets of formulae and sequents
as follows. Given 
$
\Xc = \Gamma \cup \{X_1,\dots,X_n\}
$
and
$
\Yc = \Delta \cup \{Y_1,\dots,Y_n\} 
$
their merge set contains all multisets of the form:
$
\Gamma \cup \Delta \cup \{Z_1,\dots,Z_n\}
$
where $Z_i \in X_i \merge Y_i.$



In Isabelle we defined merged sequents using triples, so in effect
$(X_1, X_2, X) \in \texttt{rmerge}$ means $X$ is a sequent in $X_1 \merge X_2$.
This is easier to define than in the paper where multisets are used, because
we require simply that each structural atom (formula or structure variable)
in $X$ is replaced by $\Phi$ in exactly one of $X_1$ or $X_2$. That
is, each atom has to go in one partition or the other.
Likewise, to express the idea of $X_1[~] \bullet X_2[~]$ we define 
$(X_1, X_2, X) \in \texttt{rmerge1} (Y_1, Y_2, Y)$ to be similar except that at
one spot $X$ contains $Y$, where $X_i$ contains $Y_i$.

%% \begin{verbatim}
%% rmerge :: "(nested * nested * nested) set"
%% rmerge1 :: "(nested * nested * nested) => (nested * nested * nested) set"
%% \end{verbatim}

% We then prove the general result that if $(X, Y, Z) : \texttt{rmerge}$ 
% then $Z => U$ can be derived from $X, Y => U$ in the shallow calculus,
% and likewise $U => Z$ from $U => X, Y$.
% \begin{verbatim}
% rmerge_derL : "(?X, ?Y, ?Z) : rmerge ==>
  % ([$?X,,, $?Y => $?U], $?Z => $?U) : derl (nrulefs fillsn_cf)" 
% \end{verbatim}
%

% \subsection{An alternative definition for \texttt{rmerge1}} \label{s-dmerge1}
%% As in the case of defining \texttt{dctxt} as an alternative to \texttt{ctxt},
%% we defined \texttt{dmerge1} as an alternative to \texttt{rmerge1}.
%% For example
%% $$
%% \frac{(Z_1, Z_2, Z) \in \texttt{rmerge} \quad ((X_1 \Rightarrow Y_1), (X_2 \Rightarrow Y_2), (X \Rightarrow Y)) \in
%% \texttt{dmerge1} (S_1, S_2, S)}
%% {((X_1 \Rightarrow Z_1, Y_1), (X_2 \Rightarrow Z_2, Y_2), (X \Rightarrow Z, Y))
%%   \in \texttt{dmerge1} (S_1, S_2, S)}
%%   $$
%% We then proved the lemmas linking \texttt{dmerge1} with \texttt{rmerge1}

%% \begin{verbatim}
%% rmerge1_dmerge1 : "($?aa => $?as, $?ba => $?bs, $?ca => $?cs) :
%%     rmerge1 ($?Aa => $?As, $?Ba => $?Bs, $?Ca => $?Cs) ==>
%%   ($?aa => $?as, $?ba => $?bs, $?ca => $?cs) :
%%      dmerge1 ($?Aa => $?As, $?Ba => $?Bs, $?Ca => $?Cs)"

%% drmerge1_ands :
%%          "[| (?qa', ?qb', ?d) : dmerge1 ?t'; ?t' : dn_ands |]
%%             ==> EX qa qb da ds t.
%%                (qa, ?qa') : ms_deep_equiv &
%%                (qb, ?qb') : ms_deep_equiv &
%%                (qa, qb, $da => $ds) : rmerge1 t &
%%                t : dn_ands & (?d, $da => $ds) : ms_deep_equiv" 
%% \end{verbatim}


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