\newpage
\appendix
\section{Equivalence of Display and Shallow Nested Calculi}
\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]
%% Many single-premise rules of display calculi are invertible,
%% and
In the following, the function \texttt{invert} inverts a rule
(meaningful only for a rule with one premise).
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!biilldc_cf!
of
$\biilldc$, then its rule instance
\verb!pscmap seq_to_nested ?r!
is derivable in the cut-free fragment
\verb!biillsn_cf! 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 biilldc_cf
==> pscmap seq_to_nested ?r : derl (nrulefs biillsn_cf)"
tr_derl_dc_snb : "(?ps, ?c) : derl (rulefs biilldc_cf) ==>
pscmap seq_to_nested (?ps, ?c) : derl (nrulefs biillsn_cf)"
\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!biillsn_cf!
of
$\biillsn$, then its rule instance
\verb!pscmap nested_to_seq ?r!
is derivable in the cut-free fragment
\verb!biilldc_cf! 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 biillsn_cf
==> pscmap nested_to_seq ?r : derl (rulefs biilldc_cf)"
tr_derl_snb_dc : "(?ps, ?c) : derl (nrulefs biillsn_cf)
==> pscmap nested_to_seq (?ps, ?c) : derl (rulefs biilldc_cf)"
\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
\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 biilldc_cf) {}) =
((?A => ?B) : derrec (nrulefs biillsn_cf) {})"
dc_sn_equiv : "((T |- ?A) : derrec (rulefs biilldc_cf) {}) =
(($NPhi => ?A) : derrec (nrulefs biillsn_cf) {})"
\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 biillsn_cf)"
\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.
\section{Equivalence of Shallow and Deep Nested Calculi}
\subsection{Proving the Deep from the Shallow Nested Sequent Calculus}
\begin{lemma}
\label{lm:dist}
The following rules are derivable in $\biillsn$ without cut:
$$
\infer[dist_l]
{(\Xc_1, \Xc_2 \seq \Yc_1,\Yc_2), \Uc \seq \Vc}
{
(\Xc_1 \seq \Yc_1), (\Xc_2 \seq \Yc_2), \Uc \seq \Vc
}
\qquad
\infer[dist_r]
{\Uc \seq \Vc, (\Xc_1, \Xc_2 \seq \Yc_1,\Yc_2)}
{
\Uc \seq \Vc, (\Xc_1 \seq \Yc_1), (\Xc_2 \seq \Yc_2)
}
$$
\end{lemma}
Intuitively, these rules embody
the weak distributivity formalised by the Grishin (b) rule.
% It is not surprising that these rules are derivable, as they essentially embody
% the weak distributivity principle formalised by the Grishin(b) rule.
In the formalisation we proved the slightly less general result
\texttt{snb\_lem14a} and its symmetric counterpart below from which we
can obtain Lemma~\ref{lm:dist} with one application of
???\marginpar{How to do this Jeremy?}
\begin{lemma}
The following rules are derivable in $\biillsn$ without cut:
$$
\infer[dist_l]
{(\Xc_1, \Xc_2 \seq \Yc_1,\Yc_2) \seq \Vc}
{
(\Xc_1 \seq \Yc_1), (\Xc_2 \seq \Yc_2) \seq \Vc
}
\qquad
\infer[dist_r]
{\Uc \seq (\Xc_1, \Xc_2 \seq \Yc_1,\Yc_2)}
{
\Uc \seq (\Xc_1 \seq \Yc_1), (\Xc_2 \seq \Yc_2)
}
$$
\begin{verbatim}
snb_lem14a = "([($?Xa => $?Ya),,, ($?Xb => $?Yb) => $?V],
($?Xa,,, $?Xb => $?Ya,,, $?Yb) => $?V) : derl (nrulefs biillsn_cf)"
\end{verbatim}
\end{lemma}
\begin{lemma}
\label{lm:merge}
If $\Xc \in \Xc_1 \merge \Xc_2$ then the rules below are cut-free derivable in $\biillsn$:
$$
\infer[m_l]
{\Xc, \Vc \seq \Uc}
{
\Xc_1, \Xc_2, \Vc \seq \Uc
}
\qquad
\infer[m_r]
{\Uc \seq \Vc, \Xc}
{
\Uc \seq \Vc, \Xc_1, \Xc_2
}
$$\marginpar{JED, how to close the difference here ? Missing $\Vc$.}
\begin{verbatim}
rmerge_der : "(?Xa, ?Xb, ?X) : rmerge
==> {([$?Xa,,, $?Xb => $?U], $?X => $?U),
([$?U => $?Xa,,, $?Xb], $?U => $?X)} <= derl (nrulefs fillsn_cf)"
\end{verbatim}
\end{lemma}
\begin{proof}
This follows straightforwardly from Lem.~\ref{lm:dist}.
\end{proof}
% \begin{verbatim}
% rmerge_der : "(?X, ?Y, ?Z) : rmerge
% ==> {([$?X,,, $?Y => $?U], $?Z => $?U),
% ([$?U => $?X,,, $?Y], $?U => $?Z)} <= derl (nrulefs fillsn_cf)"
% \end{verbatim}
\begin{lemma}
\label{lm:context-merge}
Suppose $X[~] \in X_1[~] \merge X_2[~]$ and suppose there exists $Y[~]$
such that for any $\Uc$ \marginpar{Not formalised by JED?}
and any $\rho \in \{drp_1, drp_2, rp_1, rp_2\}$,
the figure below left is a valid inference
rule in $\biillsn$:
\[
\qquad
\qquad\qquad
\infer[\rho]
{X[\Uc]}
{Y[\Uc]}
\qquad\qquad
\infer[\rho]
{X_1[\Uc]}
{Y_1[\Uc]}
\qquad
\qquad
\infer[\rho]
{X_2[\Uc]}
{Y_2[\Uc]}
\]
Then there exists $Y_1[~]$ and $Y_2[~]$ such that
$Y[~] \in Y_1[~] \merge Y_2[~]$ and the second and the third figures above
are also valid instances of $\rho$ in $\biillsn$.
\end{lemma}
\begin{proof}
This follows from the fact that $X[~]$, $X_1[~]$ and $X_2[~]$ have exactly the same
nested structure, so whatever display rule applies to one also applies to the others.
\end{proof}
% We prove in turn that the deep propagation rules (\texttt{dn\_bprs}),
% single-premise logical rules (\texttt{dn\_splrs})
% and monoid (commutativity, associativity and $\Phi$) rules (\texttt{dn\_ac0})
% are derivable in the shallow system.
% These proofs are simpler but have some features similar to the proofs using
\begin{lemma}
For any context,
the deep propagation rules
\texttt{dn\_bprs}, single-premise logical rules
\texttt{dn\_splrs} and added monoid (commutativity, associativity and
$\Phi$) rules \texttt{dn\_ac0} of $\biilldn$ are cut-free derivable in
the shallow system $\biillsn$.
% These proofs are simpler but have some features similar to
% the proofs using \texttt{rule\_base0} and \texttt{rule\_base2}
% described below.
\begin{verbatim}
ctxt_bprs_sn :
"[| ([?p], $?ca => $?cs) = ?psc; ?psc : ctxt (nrulefs dn_bprs) |]
==> ?psc : derl (nrulefs fillsn_cf)"
ctxt_splrs_sn :
"[| ([?p], $?ca => $?cs) = ?psc; ?psc : ctxt (nrulefs dn_splrs) |]
==> ?psc : derl (nrulefs fillsn_cf)"
ctxt_dn_ac0 :
"[| ([$?pa => $?ps], $?ca => $?cs) = ?psc; ?psc : ctxt (nrulefs dn_ac0) |]
==> ?psc : derl (nrulefs fillsn_cf)"
\end{verbatim}
\end{lemma}
A nested sequent $S$ satisfies \texttt{rule\_base0 rules} if, for all
hollow $X$, both $X \Rightarrow S$ and $S \Rightarrow X$ are derivable
using \texttt{rules}.
For the axioms, we proved that the axioms\marginpar{All this to be
cleaned up.} themselves (without the context
$X[~]$) are derivable (\texttt{dn\_axioms\_der}),
and using lemmas (\texttt{dn\_axioms\_rb0} and \texttt{hctxt\_rb0}) we
proved that the axioms with the hollow contexts $X[~]$ are derivable.
Thus \texttt{dn\_axioms\_rb0} says that the axioms (without context) can be
extended by hollow $X$ in this way once, and \texttt{hctxt\_rb0} extends this
inductively to apply to any hollow extension of an axiom.
\begin{verbatim}
dn_axioms_der : "?S : dn_axioms ==> ([], ?S) : derl (nrulefs fillsn_cf)"
dn_axioms_rb0 : "?S : dn_axioms ==> rule_base0 fillsn_cf ?S"
hctxt_rb0 : "[| rule_base0 ?rules ?S; sn_idps <= ?rules;
{sn_pA, sn_pS} <= ?rules; ?H : hctxt {?S} |] ==> rule_base0 ?rules ?H"
rule_base0_def : "rule_base0 ?rules ?S ==
(ALL X:hollows. ([], $X => $?S) : derl (nrulefs ?rules)) &
(ALL X:hollows. ([], $?S => $X) : derl (nrulefs ?rules))"
\end{verbatim}
For the two-premise logical rules, we prove theorems like
\begin{verbatim}
dn_ands_sn : "[| (?Sa, ?Sb, ?Sc) : rmerge; (?Ta, ?Tb, ?Tc) : rmerge |] ==>
([$?Sa => ?A,,, $?Ta, $?Sb => ?B,,, $?Tb],
$?Sc => ?A && ?B,,, $?Tc) : derl (nrulefs fillsn_cf)"
rb2_ands : "[| (?Sa, ?Sb, ?Sc) : rmerge; (?Ta, ?Tb, ?Tc) : rmerge |] ==>
rule_base2 fillsn_cf
($?Sa => ?A,,, $?Ta, $?Sb => ?B,,, $?Tb, $?Sc => ?A && ?B,,, $?Tc)"
deep2_ctxt : "[| sn_idps <= ?rules; {sn_pA, sn_pS} <= ?rules;
rule_base2 ?rules (?Ya, ?Yb, ?Yc);
(?Wa, ?Wb, ?Wc) : rmerge1 (?Ya, ?Yb, ?Yc) |] ==>
rule_base2 ?rules (?Wa, ?Wb, ?Wc)"
\end{verbatim}
Then by the lemmas \texttt{rb2\_ands}, etc, and \texttt{deep2\_ctxt},
we are able to show from \texttt{dn\_ands\_sn} (etc)
that the deep two-premise logical rules are derivable in the shallow calculus.
Similar to \texttt{rule\_base0}, \texttt{rule\_base2} expresses that a triple
of sequents $(P_1, P_2, C)$ satisfies that
$X \Rightarrow C$ is derivable from
$X_1 \Rightarrow P_1$ and $X_2 \Rightarrow P_2$,
for all $(X_1, X_2, X) \in \texttt{rmerge}$, and similarly for
$C \Rightarrow X$, $P_1 \Rightarrow X_1$ and $P_2 \Rightarrow X_2$.
So, similarly to the use of \texttt{rule\_base0} for the axioms,
these results are used to show that the two-premise
logical rules in their contexts are derivable.
These results are combined to show that nested sequents derivable in the deep
calculus are derivable in the shallow calculus.
\begin{theorem}
\label{thm:soundness}
Every rule of the deep nested sequent calculus $\biilldn$ is
cut-free derivable in the shallow nested sequent calculus $\biillsn.$
\begin{verbatim}
dn_sn_der : "?r : biilldn ==> ?r : derl (nrulefs fillsn_cf)"
\end{verbatim}
\end{theorem}
\begin{corollary}
\label{thm:soundness}
If a sequent $X$ is provable in $\biilldn$ then it is cut-free provable in $\biillsn.$
\end{corollary}
\subsection{Proving the Shallow from the Deep Nested Sequent Calculus}
\label{s-dn-sn}
We first note that since our formulation of $\biilldn$\ involves the comma
as a structural connective, and explicit inclusion of the
monoid rules \texttt{dn\_ac0} (see \S\ref{s-msde}),
it is necessary to prove that
our system makes multiset-equivalent nested sequents interderivable
using the monoid rules, and conversely.
\begin{lemma}
If two deep nested sequents $X_a$ and $X_b$ are multiset-equivalent
then the single-premise rule from $X_a$ to $X_b$ is derivable in all
contexts using only the monoid rules of associativity, commutativity
and identity. Conversely, if the deep nested sequent $X_N$ is
derivable from the deep nested sequent $X_M$ in all contexts using the
monoid rules then $X_N$ and $X_M$ are multiset-equivalent.
\begin{verbatim}
msde_derl : "(?a, ?b) : ms_deep_equiv
==> ([?a], ?b) : derl (ctxt (nrulefs dn_ac0))"
dn_ac0_msde : "([?M], ?N) : ctxt (nrulefs dn_ac0)
==> (?M, ?N) : ms_deep_equiv"
\end{verbatim}
\end{lemma}
The key lemma here is that the rules $rp_i$, $drp_i$,
$gl$ and $gr$ which are in the shallow calculus
$\biillsn$\ but not in the deep calculus $\biilldn$\ are admissible in
$\biilldn$.
\begin{lemma}
\label{lm:permute}
The rules $drp_1$, $rp_1$, $drp_2$, $rp_2$, $gl$, and $gr$ permute up over all logical rules of $\biilldn.$
\end{lemma}
This is the permutation lemma, that (in general)
where one of the shallow rules in question follows a rule of $\biilldn$\
in a derivation, then the derivation can be re-ordered so that the
shallow rule precedes the deep rule.
In some cases we need to use a different or additional deep rule, and
where the deep rule is an axiom then the result is that we can dispense with
the shallow rule.
\subsubsection{Where the deep rule is an axiom} \label{s-perm-ax}
We define the set of hollow structures (see \texttt{hollows.intrs}),
and the idea of a \emph{hollow context} $X[~]$
(see \texttt{hctxt.intrs}).
Theorems \texttt{dn\_gen\_id}, \texttt{dn\_gen\_tS} and \texttt{dn\_gen\_fA}
express that any nested sequent which is multiset-equivalent to the
axioms as written in the paper is derivable using our rules.
Then theorems \texttt{id\_then}, \texttt{tS\_then} and \texttt{fA\_then}
express that each of these axioms followed by an instance of the rules
$rp_1$, $drp_1$, $rp_2$, $drp_2$, $gl$ and $gr$, and also $ig$ and $eg$ (see
the proof of Lemma~18, in page~19 in the Appendix),
is derivable in $\biilldn$.
\begin{verbatim}
dn_gen_id : "[| set_of ?U <= hollows; set_of ?V <= hollows;
ms_of_ns ?X = mins (NStructform ?A) ?U;
ms_of_ns ?Y = mins (NStructform ?A) ?V;
($?Z => $?W) : hctxt {$?X => $?Y} |] ==>
([], $?Z => $?W) : derl biilldn"
id_then : premises as for dn_gen_id, plus
([$?Z => $?W], ?S) : nrulefs {sn_rp, sn_drp, invert sn_rp,
invert sn_drp, sn_gl, sn_gr, sn_ig, sn_eg} |] ==>
([], ?S) : derl biilldn"
\end{verbatim}
See the file \texttt{Rotate.ML}.
\subsubsection{Where the deep rule is a single-premise logical rule}
\label{s-one-prem-log}
We proved theorems of the following form
\begin{verbatim}
p_irp_anda : "?c = ($?ca => $?cs) -->
([?p], ?c) : ctxt (nrulefs {sn_anda}) -->
(?c, ?c') : ms_deep_equiv --> ([?c'], ?d') : nrulefs {invert sn_rp} -->
(EX p' q q' d. (?p, p') : ms_deep_equiv &
([p'], q) : nrulefs {invert sn_rp} & (q, q') : ms_deep_equiv &
([q'], d) : dctxt (nrulefs {sn_anda}) & (d, ?d') : ms_deep_equiv)"
\end{verbatim}
That is, where a rule among
$rp_1$, $drp_1$, $rp_2$, $drp_2$, $gl$, $gr$, $eg$ and $eg$
appears below a logical rule in a derivation,
the derivation steps may be permuted so that the logical rule follows
the other rule.
Before realising we needed to use $rp_1$, $drp_1$, $eg$ and $eg$
instead of
$rp_1$, $drp_1$, $rp_2$, $drp_2$, $gl$ and $gr$
we proved the twelve theorems for the six logical rules and
for $rp_2$ and $drp_2$ using the tactics \texttt{mpttacs}.
We proved the twelve theorems
for $rp_1$ and $drp_1$ using the tactics \texttt{mpttacs\_i}.
Having proved the twelve theorems
for $gl$ and $gr$ using the tactics \texttt{mpttacs\_g}
we found that the same tactics worked to prove the twelve theorems
for $eg$ and $ig$.
It may be noted that this result uses \texttt{dctxt}, not \texttt{ctxt},
in the conclusion. This made semi-automatic proof easier;
the lemmas for all the logical rules concerned (6 of them) for all the
structural rules involved (6 of them) were done using just three separate sets
of tactics.
To use \texttt{dctxt} in this way we needed the results
\texttt{dc\_anda} and \texttt{dcok\_anda} (etc).
\begin{verbatim}
dc_anda : "([?p], ?c) : dctxt (nrulefs {sn_anda}) ==>
EX p' c'. (?p, p') : ms_deep_equiv & (c', ?c) : ms_deep_equiv &
([p'], c') : ctxt (nrulefs {sn_anda})"
dcok_anda : "EX p' q q' d. (?p1, p') : ms_deep_equiv &
([p'], q) : nrulefs {?sn_rule1} & (q, q') : ms_deep_equiv &
([q'], d) : dctxt (nrulefs {sn_anda}) & (d, ?d'1) : ms_deep_equiv ==>
EX p' q q' d. (?p1, p') : ms_deep_equiv &
([p'], q) : nrulefs {?sn_rule1} & (q, q') : ms_deep_equiv &
([q'], d) : ctxt (nrulefs {sn_anda}) & (d, ?d'1) : ms_deep_equiv"
\end{verbatim}
These results, and similar ones for the other rules of $\biilldn$,
and the results of \S\ref{s-perm-ax}, will give that the rules
$rp_1$, $drp_1$, $rp_2$, $drp_2$, $gl$ and $gr$ are admissible in $\biilldn$.
See \S\ref{s-TBA}.
See the file \texttt{CRotate.ML}.
\subsubsection{Where the deep rule is a two-premise logical rule}
\label{s-two-prem-log}
These are similar to the one-premise rules, except that the statement of the
theorem is more complicated, as are accordingly the proof tactics.
The following lemmas needed to be used for some of these results.
Of these, \texttt{rmerge\_msde} in particular was extraordinarily difficult to
prove.
\begin{verbatim}
rmerge_msde : "[| (?c, ?c') : ms_deep_equiv; (?a, ?b, ?c) : rmerge |] ==>
EX a' b'. (?a, a') : ms_deep_equiv &
(?b, b') : ms_deep_equiv & (a', b', ?c') : rmerge"
rmerge1_msde_comma :
"[| (?a, ?b, ?c) : rmerge1 (?A, ?B, ?C); ms_of_ns ?C = {#?C#};
(?c, $?dY,,, $?dZ) : ms_deep_equiv |] ==>
EX aY aZ bY bZ cY cZ.
(?a, $aY,,, $aZ) : ms_deep_equiv & (?b, $bY,,, $bZ) : ms_deep_equiv &
(cY, ?dY) : ms_deep_equiv & (cZ, ?dZ) : ms_deep_equiv &
((aY, bY, cY) : rmerge1 (?A, ?B, ?C) & (aZ, bZ, cZ) : rmerge |
(aZ, bZ, cZ) : rmerge1 (?A, ?B, ?C) & (aY, bY, cY) : rmerge)"
msde_commasD : "($?Aa,,, $?Ab, $?Ba,,, $?Bb) : ms_deep_equiv ==>
EX Caa Cab Cba Cbb. (?Aa, $Caa,,, $Cab) : ms_deep_equiv &
(?Ab, $Cba,,, $Cbb) : ms_deep_equiv &
($Caa,,, $Cba, ?Ba) : ms_deep_equiv &
($Cab,,, $Cbb, ?Bb) : ms_deep_equiv"
\end{verbatim}
See the file \texttt{P2Rotate.ML}.
\subsubsection{Where the deep rule is a propagation rule}
\label{s-prop-rules}
The statement of the theorems, and some of the proofs, are similar to those
described in \S\ref{s-one-prem-log}.
The eight theorems for the cases $rp_1, drp_1$ with
$pl_1, pr_1, pl_2, pr_2$ were proved using the same set of tactics
\texttt{mpttacs\_ine},
but the theorems for $pl_1$ required replacing $pl_1$ with either
\texttt{dn\_pl1t} (which uses $pl_1$ twice) or
\texttt{dn\_plc} (which uses $pl_1$ then $pl_2$),
as shown in the first two cases of the proof of Lemma~36.
Similarly for the theorems for $pr_1$.
Unfortunately we had to subsequently generalise these new rules
\texttt{dn\_pl1t} and \texttt{dn\_plc}
to \texttt{dn\_pl1tg} and \texttt{dn\_plcg}
to enable proving the required theorems analogous to \texttt{dc\_anda},
see \S\ref{s-one-prem-log}.
For the eight theorems for the cases $ig, eg$ with
$pl_1, pr_1, pl_2, pr_2$ four were proved using the same set of tactics
\texttt{mpttacs\_ieg},
but the other four needed to be proved individually.
These were \texttt{p\_ig\_pr1, p\_eg\_pl1, p\_ig\_pr2, p\_eg\_pl2}.
Of these eight theorems,
\texttt{p\_ig\_pl1, p\_ig\_pr2, p\_eg\_pl2, p\_eg\_pr1}
include cases where the propagation rule simply disappears rather than just
being permuted to below the $ig$ or $eg$ rule, as shown in the third and
fourth cases of the proof of Lemma~36.
To express these it was simplest to define a rule
\texttt{sn\_rpt\_nes} which just repeats a nested sequent unchanged.
See the file \texttt{Prop\_Rotate.ML}.
\subsubsection{Complication: using $eg$ and $ig$ versus $gl$ and $gr$}
\label{s-glr-ieg}
The paper introduces rules $eg$ and $ig$, which, given the rules
$rp_1$, $drp_1$, $rp_2$ and $drp_2$, are equivalent to $gl$ and $gr$.
Further, $rp_2$ and $drp_2$ are special cases of $ig$ and $eg$.
Therefore, given the admissibility of $rp_1$, $drp_1$, $rp_2$ and $drp_2$,
the admissibility of $eg$ and $ig$ is equivalent to the
the admissibility of $gl$ and $gr$.
However in proving some of the permutation lemmas described above,
when permuting $rp_2$ or $drp_2$ above rules of $\biilldn$, we had to change the
instance of $rp_2$ and $drp_2$ to an instance of $ig$ and $eg$.
We first planned to just consider $ig$ as $gr$ followed by $rp_2$,
but realised this
may cause a problem in proving termination of this permutation procedure.
This affects rules \texttt{p2\_rp\_lollia} and \texttt{p2\_drp\_excls},
and also \texttt{p\_rp\_pr2} and \texttt{p\_drp\_pl2}.
This is because other instances of the permutation rule
replace one of the rules of $\biilldn$\ by two rules of $\biilldn$,
namely \texttt{p2\_irp\_lollia} and \texttt{p2\_idrp\_excls}.
Then the proof of termination is not obvious.
For example, let $B_1$ and $B_2$ be rules of $\biilldn$, and
let $A_1$ and $A_2$ be rules we are hoping to prove admissible.
Suppose we have permutation lemmas which replace
\begin{itemize}
\item the subderivation
$B_1 A_2$ (ie rule $B_1$, then rule $A_2$) by $A_1 A_2$ (whether or not
followed by another $B$-rule),
and
\item $B_2 A_1$ by $A_1 B_2 B_1$
\end{itemize}
Then we get
$$B_2 B_1 A_2 \Rightarrow B_2 A_1 A_2 \Rightarrow A_1 B_2 B_1 A_2 $$
which loops indefinitely.
That is, when permutation lemmas produce a result using two logical rules,
and when other permutation lemmas produce a result using two of the hopefully
admissible rules, we may get a problem.
So we now look at proving the permutation lemmas for
$rp_1$, $drp_1$, $eg$ and $ig$
instead of
$rp_1$, $drp_1$, $rp_2$, $drp_2$, $gl$ and $gr$
(as in Lemma~36 in the paper).
But it seems we should also do this for Lemmas 34 and 35 of the paper
(see \S\ref{s-perm-ax}).
So we defined the rule set \texttt{biillsn_ieg_cf}
which has $eg$ and $ig$ in place of $rp_2$, $drp_2$, $gl$ and $gr$ in
\texttt{biillsn\_cf}, and proved their equivalence in the theorem
\texttt{biillsn\_cf\_eq\_ieg}.
\begin{verbatim}
biillsn_cf_eq_ieg : "derl (nrulefs biillsn_cf) = derl (nrulefs biillsn_ieg_cf)"
\end{verbatim}
\subsubsection{Complication: admissibility of hollow context weakening}
\label{s-hollow-weak}
In \S\ \ref{s-perm-ax}, \ref{s-one-prem-log}, \ref{s-two-prem-log},
\ref{s-prop-rules} and \ref{s-glr-ieg}
we proved the lemmas needed to show the $\biilldn$-admissibility of the
rules $rp_1$, $drp_1$, $eg$ and $ig$.
It seemed at first that the remaining rules of $\biilldn$\ would be derivable in
$\biillsn$.
However we found that the two-premise logical rules in
the shallow calculus $\biillsn$\ differ from those in the deep calculus
$\biilldn$\ (even when we ignore the contexts $X[~]$ and $X_i[~]$).
The difference is that where the shallow and deep rules are respectively
$$
\frac {\mathcal U \Rightarrow A, \mathcal V \quad
\mathcal U' \Rightarrow B, \mathcal V'}
{\mathcal{U, U'} \Rightarrow A \otimes B, \mathcal{V, V'}}
\qquad
\frac {\mathcal S_1 \Rightarrow A, \mathcal T_1 \quad
\mathcal S_2 \Rightarrow B, \mathcal T_2}
{\mathcal S \Rightarrow A \otimes B, \mathcal T}
$$
where $ \mathcal S = \mathcal S_1 \bullet \mathcal S_2$
and $ \mathcal T = \mathcal T_1 \bullet \mathcal T_2$.
So to use the deep rule to derive the shallow rule we need to identify
$\mathcal S$ with $\mathcal{U, U'}$ and then find some
$\mathcal S_1$ and $\mathcal S_2$ such that
$\mathcal S = \mathcal S_1 \bullet \mathcal S_2$ and
$\mathcal U$ and $\mathcal U'$ can be weakened to
$\mathcal S_1$ and $\mathcal S_2$ respectively
(similarly for $\mathcal T$, $\mathcal T_i$, $\mathcal V$, $\mathcal V'$).
This requires showing that "hollow-weakening" is admissible.
We suspect that a more general result is true, where we replace
$(U,X \Rightarrow Y,V)$ below by any hollow context of
$(X \Rightarrow Y)$, but we didn't need that.
As with any admissibility result, the proof of this involved extending all the
rules of $\biilldn$\ by hollow structures $U$ and $V$.
By lemma \texttt{hollows\_rmerge}, we extend \emph{both} the premises as well
as the conclusion of a two-premise logical rule by $U$ and $V$.
\begin{verbatim}
hollow_weak' : "[| ($?X => $?Y) : derrec biilldn {};
?U : hollows; ?V : hollows |] ==>
($?U,,, $?X => $?Y,,, $?V) : derrec biilldn {}"
hollows_rmerge : "?H : hollows ==> (?H, ?H, ?H) : rmerge"
\end{verbatim}
Hence we get that the two-premise rules of $\biillsn$\ are admissible (not
derivable) in $\biilldn$.
All the other rules are easier, and so we get that all the rules of
\begin{verbatim}
sn_ands_dn : "nrulefs {sn_ands} <= adm biilldn"
\end{verbatim}
\subsubsection{Wrapping it up}
From \S\ \ref{s-perm-ax}, \ref{s-one-prem-log}, \ref{s-two-prem-log},
\ref{s-prop-rules} and \ref{s-glr-ieg}
we have the $\biilldn$-admissibility of $rp_1$, $drp_1$, $eg$ and $ig$,
and from \S\ref{s-hollow-weak}
we have $\biilldn$-admissibility of the two-premise logical rules.
The other rules of $\biillsn$\ are $\biilldn$-derivable,
so we get \texttt{sn\_dn\_der}.
Combining this with \texttt{dn\_sn\_der} (see \S\ref{s-dn-sn})
we get \texttt{sn\_dn\_equiv}.
These proofs made good use of the lemmas relating
\texttt{derrec}, \texttt{derl}, \texttt{adm}
described in our LPAR 2010 (or Raj's talk in India) paper \cite{xx}
\begin{theorem}
If a sequent $X$ is cut-free $\biillsn$-derivable then it is also $\biilldn$-derivable.
\end{theorem}
\begin{corollary}\label{cor:dc=dn}
A formula is cut-free $\biilldc$-derivable iff it is $\biilldn$-derivable.
\end{corollary}
\begin{theorem}
Every rule that is cut-free derivable in $\biillsn$ is (cut-free) admissible in
$\biilldn$.
\begin{verbatim}
sn_dn_der : "derl (nrulefs biillsn_cf) <= adm biilldn"
\end{verbatim}
A sequent is cut-free provable (derivable from the empty set of assumption
sequents) in $\biillsn$ iff it is provable $\biilldn$.
\begin{verbatim}
sn_dn_equiv : "(?r : derrec (nrulefs biillsn_cf) {}) =
(?r : derrec biilldn {})"
\end{verbatim}
The formula $A$ is cut-free provable in the display calculus iff it
is (cut-free) provable in $\biilldn$.
\begin{verbatim}
dc_dn_equiv : "((T |- ?A) : derrec (rulefs biilldc_cf) {}) =
(($NPhi => ?A) : derrec biilldn {})"
\end{verbatim}
\end{theorem}
\subsection{Automating these proofs in Isabelle}
Note the form of the theorem \texttt{p\_rp\_anda} in \S\ref{??},
which requires finding values for unknowns $p', q, q', d$ such that
(among other requirements) $(p,p'), (q,q')$ and $(d, d')$ are all in
\texttt{ms\_deep\_equiv}.
We mostly used a recursive compund tactic for this, initially defined thus
\begin{verbatim}
fun perm_msde_tac' sg = FIRST' [ atac,
(resolve_tac [msde.seqs, msde_commas, msde_commas_rev]
THEN_ALL_NEW perm_msde_tac'),
rtac refl_msde', etac refl_ms_of_ns_eq,
eresolve_tac msde_commas_empty, resolve_tac msde_assocs,
resolve_tac msde_comm_assocs] sg ;
\end{verbatim}
For the above, \texttt{msde.seqs} and \texttt{msde\_commas} are shown;
the last three lines represent various ways to solve the goal, and samples of
the theorems used are shown.
\begin{verbatim}
msde.seqs : "[| (?aa, ?ba) : ms_deep_equiv; (?as, ?bs) : ms_deep_equiv |]
==> ($?aa => $?as, $?ba => $?bs) : ms_deep_equiv"
msde_commas : "[| (?aa, ?ba) : ms_deep_equiv; (?as, ?bs) : ms_deep_equiv |]
==> ($?aa,,, $?as, $?ba,,, $?bs) : ms_deep_equiv"
msde_commas_empty (one of them) :
["ms_of_ns ?Y = {#} ==> ($?X,,, $?Y, ?X) : ms_deep_equiv"
msde_comm_assocs (one of them) ;
["(($?aa1,,, $?C2),,, $?B2, ($?C2,,, $?B2),,, $?aa1) : ms_deep_equiv"
\end{verbatim}
The tactic works generally when there are some, but not too many, unknowns in
the goal to be instantiated. Generally, of the three occurrences of
$(\_, \_) \in \texttt{ms\_deep\_equiv}$, it was best to attempt the first and
last before the middle one.
However, this led to a problem.
If a premise of each subgoal was $(A, B) \in \texttt{ms\_deep\_equiv}$,
then the first and last subgoals of the form
$(\_, \_) \in \texttt{ms\_deep\_equiv}$
could both get solved by instantiating in a way
which used that premise, and then the final (second of the three)
subgoal would look like
$(\ldots B \ldots, \ldots A \ldots) \in \texttt{ms\_deep\_equiv}$,
which wouldn't get solved.
Thus we devised a general technique to ensure that a premise which appeared in
multiple subgoals could only get used in one of them.
\begin{verbatim}
keep :: bool => 'a => 'a"
keep_def : "keep ?b ?f == ?f"
keep_msdeI : "?nsp : ms_deep_equiv ==> keep ?b (?nsp : ms_deep_equiv)"
keepF_thin : "[| keep False ?P; PROP ?W |] ==> PROP ?W"
keepFD : "keep False ?P ==> ?P"
\end{verbatim}
First (\emph{before} the premise which is to be used once only is propagated to
multiple subgoals), change each such premise $P$ to
\texttt{keep ?b } $P$ ---
in this case, by the tactic \texttt{REPEAT o dtac keep\_msdeI}.
Then, in \texttt{perm\_msde\_tac'} above, we changed
\texttt{atac} to \texttt{etac keepFD}.
This ensures that when such a premise is used, the variable \texttt{?b} is
changed to \texttt{False}.
Finally, we use the tactic \texttt{REPEAT o ematch\_tac [keepF\_thin]}
to remove occurrences of \texttt{keep False} \ldots where and when required.
In our case the problem was to avoid reuse of a premise in \emph{separate}
uses of \texttt{perm\_msde\_tac'}, so we defined \texttt{perm\_msde\_tac} as shown.
(This would not have prevented the same premise being used twice within the
same invocation of \texttt{perm\_msde\_tac}).
\begin{verbatim}
val perm_msde_tac =
(REPEAT o ematch_tac [keepF_thin]) THEN' perm_msde_tac' ;
\end{verbatim}
The proofs of the permutation lemma involved a large number of cases,
because a sequent expression such as $X [\mathcal S \seq \mathcal T]$
can match a given sequent $Z$ in numerous ways, for two reasons:
\begin{itemize}
\item when $\mathcal S$ and $\mathcal T$ are multisets (that is, in our
formulation, there are many ways that
$(\mathcal S, \ldots) \in \texttt{msde\_deep\_equiv}$ can be achieved)
\item the context $X [~]$ may be of any size (which means that
$\mathcal S \seq \mathcal T$ can match any part of $Z$
\end{itemize}
The attempted proof encounters plenty of obviously impossible cases
such as a formula matching $\mathcal S \seq \mathcal T$.
After these are detected and eliminated, we counted the cases where
a goal (such as the conclusion of \texttt{p\_rp\_anda}) is actually solved.
These cases numbered 616, which shows the value of automating the process as
much as possible.
% \subsection{Lemmas about \texttt{ms\_deep\_equiv}}
% OMIT THIS SECTION
% There were a number of seemingly basic lemmas about the
% \texttt{ms\_deep\_equiv} relation which were not easy to prove.
% For example,
% \begin{verbatim}
% mins_msde_lem ;
% msde_ex_plus ;
% msde_mins_inv ;
% msde_plus_inv ;
% msde_commasD ;
% ctxt_nseq_lem ;
% \end{verbatim}