
\documentclass{article}

\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{url}
% \usepackage{exptrees}

\newcommand\comment[1]{} 
\newcommand\biilldc{$\mbox{BiILL}_{dc}$}
\newcommand\filldc{$\mbox{FILL}_{dc}$}
\newcommand\biillsn{$\mbox{BiILL}_{sn}$}
\newcommand\fillsn{$\mbox{FILL}_{sn}$}
\newcommand\biilldn{$\mbox{BiILL}_{dn}$}
\newcommand\filldn{$\mbox{FILL}_{dn}$}

\begin{document}

\title{Isabelle work on Full Intuitionistic Linear Logic}

\author{Jeremy E.\ Dawson}

\maketitle

\section{Introduction and Acknowledgements}
This document describes my work in Isabelle from July 2013 relating to the
paper
"Annotation-Free Sequent Calculi for
Full Intuitionistic Linear Logic", subsequently published in CSL 2013
\cite{fill-csl}.

During the early part of 2013 I worked on proving, in Isabelle, the
lemmas and theorems of the then version of that paper,
but discovered a problem
with the exclusion-deletion procedure described in it.  

A revised version of the paper which did not use this procedure was prepared
(with my name added as a co-author).

Since then I have been trying to verify the lemmas and theorems of the 
revised version of the paper.

\section{The nested sequent datatype cannot involve multisets}
\label{s-msde}
A nested sequent could be defined (and is defined in Isabelle) using a tree
structure with two binary operators, ``$\Rightarrow$" and ``,'',
and this could be expressed as a datatype in Isabelle.
However, in the paper a nested sequent is constructed using the operator 
``$\Rightarrow$", with a multiset of nested sequents on either side of the
``$\Rightarrow$".

Thus the formulation in the paper does not require explicit rules for
commutativity or associativity, or for $M,\Phi$ (where $\Phi$ is the empty
multiset).

Now Isabelle permits nested datatypes.  For example, a derivation tree is made
up of an end-sequent and a list of derivation trees (whose end-sequents are the
premises of the final rule of the whole tree).  Thus the datatype is nested, ie
the derivation tree contains a list of derivation trees.
But this is possible only because ``list'' is also a datatype.  We couldn't do
this if ``list'' were replaced by ``multiset'' in the description above.

CITE Traytel et al.

So we defined a relation, \emph{multiset-equivalence},
\texttt{ms\_deep\_equiv}, under which any two 
Isabelle nested sequents are equivalent if they would be the same if each
collection of sequents, separated by commas, were considered the same.
This includes where the difference between two Isabelle nested sequents occurs
at any depth.

INCLUDE definitions for this.

While we used the relation \texttt{ms\_deep\_equiv} to describe the situation
where two nested sequents are equivalent, we defined the shallow and deep
nested sequent calculi \biillsn\ and \biilldn\ to contain rules expressing the 
monoid (commutativity, associativity and $\Phi$) rules
(\texttt{sn\_ac0} and \texttt{dn\_ac0}), in addition to the rules shown in the
paper.

\subsection{Lemmas about \texttt{ms\_deep\_equiv}}

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}

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

As discussed above, for nested sequents we used a datatype
with connectives comma and $\Rightarrow$,
and a constant for the empty multiset (as in the display calculus).

For the display calculus we have rules named (for example)
\texttt{rp}, 
\texttt{drp}, 
\texttt{pA} (permutation of the antecedent), 
\texttt{aS} (associativity of the succedent), 
\texttt{anda} and \texttt{ands} 
($\land$-rule, antecedent and succedent), etc.

The entire set of rules is called
\texttt{rlscf} (for \biilldc, including \texttt{drp}), or
\texttt{frlscf} (for \filldc, excluding \texttt{drp}).
See file \texttt{F\_Rls.thy}.

For the nested sequent calculus we have rules named (for example)
\texttt{sn\_rp}, 
\texttt{sn\_drp}, 
\texttt{sn\_pA} (permutation of the antecedent), 
\texttt{sn\_aS} (associativity of the succedent), 
\texttt{sn\_anda} and \texttt{sn\_ands}.
Because of the apparent difficulty of formalising nested sequents using
multisets, we needed additional rules to handle commutativity and
associativity, and the identity for the comma operator.
These rules correspond to equivalent rules for the display calculus.

The entire set of rules is called \texttt{sn\_rlscf}.
See file \texttt{N\_Rls.thy}.

We have proved equivalence between these two systems.
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 equivalence between a nested sequent and a display calculus sequent
is expressed 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}

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).

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{Shallow Nested Sequent Calculus to Display Calculus}
With a lot of lemmas deriving a display calculus rule from a set of nested
sequent rules, like
\begin{verbatim}
sd_dands : "[| {invert sn_ira} <= ?rules';  ... |] ==>
   ([?A => $?Za, ?B => $?Z], ?A +++ ?B => $?Za,,, $?Z) : derl (nrulefs ?rules')"
\end{verbatim}
where the premises list the rules of \biillsn\ which are actually used,
which shows that an individual display calculus rule can be proved in the
shallow nested system (see \texttt{N\_Rls.ML}), 
we are able to prove
\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}
that is, each \biilldc\ rule is derivable in \biillsn, and
then that each sequent derivable in \biilldc\ is derivable in \biillsn.
See the file \texttt{Dc\_Sn.ML}.

\subsection{Display Calculus to Shallow Nested Sequent Calculus}
In this case we get a set of results like
\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}
where the premises list the rules of \biilldc\ which are actually used,
which shows that an individual shallow nested calculus rule
can be proved in the display calclus (see \texttt{F\_Rls.ML}),
we are able to prove
\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 is derivable in \biilldc, and
then that each sequent derivable in \biillsn\ is derivable in \biilldc.  
See the file \texttt{Dc\_Sn.ML}.

\section{The Deep Nested Sequent Calculus}
\subsection{Applying a context to a rule}
We needed to define several notions of ``context'', denoted $X[~]$ in the
paper.
\begin{verbatim}
  ctxt :: "nested psc set => nested psc set"
  dctxt :: "nested psc set => nested psc set"
  hctxt :: "nested set => nested set"
\end{verbatim}
Thus, where $([P], C) \in R$, 
$([X[P]], X[C]) \in \texttt{ctxt}\ R$.
Likewise, if $C \in R$ and $X[~]$ is a hollow context then 
$X[C] \in \texttt{hctxt}\ R$.

\subsection{An alternative definition for \texttt{ctxt}} \label{s-dctxt}
Some of the proofs involving \texttt{ctxt} were easier using a related
definition where $X[S \Rightarrow T]$ means adding nested sequents to
$S$ or to $T$, rather than to $S \Rightarrow T$.
For example, if
 $([P' \Rightarrow P''], C' \Rightarrow C'') \in \texttt{dctxt} R$, then 
 $([P', X \Rightarrow P''], C', X \Rightarrow C'') \in \texttt{dctxt} R$.

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}
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}
We also defined merged sequents, using triples, so in effect
$(X_1, X_2, X) \in \texttt{rmerge}$,
where $X$ is a sequent in $X_1 \bullet 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, X_2$.

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 sn_rlscf)" 
\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{((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}

\subsection{From Deep to Shallow Nested Sequent Calculi}
\label{s-dn-sn}
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 
\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 sn_rlscf)"
ctxt_splrs_sn :
   "[| ([?p], $?ca => $?cs) = ?psc; ?psc : ctxt (nrulefs dn_splrs) |]
         ==> ?psc : derl (nrulefs sn_rlscf)"
ctxt_dn_ac0 :
    "[| ([$?pa => $?ps], $?ca => $?cs) = ?psc; ?psc : ctxt (nrulefs dn_ac0) |]
          ==> ?psc : derl (nrulefs sn_rlscf)" 
\end{verbatim}

For the axioms, we proved that the axioms 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.
A sequent $S$ satisfies \texttt{rule\_base0 rules} if, for hollow $X$,
$X \Rightarrow S$ and $S \Rightarrow 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 sn_rlscf)"
dn_axioms_rb0 : "?S : dn_axioms ==> rule_base0 sn_rlscf ?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 sn_rlscf)"
rb2_ands : "[| (?Sa, ?Sb, ?Sc) : rmerge; (?Ta, ?Tb, ?Tc) : rmerge |] ==>
  rule_base2 sn_rlscf 
    ($?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{verbatim}
dn_sn_der : "?r : biilldn ==> ?r : derl (nrulefs sn_rlscf)" 
\end{verbatim}

\subsection{From Shallow to Deep Nested Sequent Calculi}

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{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}

The key lemma here is that the rules (the display rules,
$rp_i$ and $drp_i$, and the Grishin rules $gl$ and $gr$)
which are in the shallow calculus \biillsn\ but not in the deep calculus
\biilldn\ are admissible in \biilldn.

For this we first prove a permutation lemma (Lemma 18), 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_rp_anda :
   "?c = ($?ca => $?cs) --> ([?p], ?c) : ctxt (nrulefs {sn_anda}) -->
      (?c, ?c') : ms_deep_equiv --> ([?c'], ?d') : nrulefs {sn_rp} -->
    (EX p' q q' d.  (?p, p') : ms_deep_equiv &
       ([p'], q) : nrulefs {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{snb\_ieg\_rlscf}
which has $eg$ and $ig$ in place of $rp_2$, $drp_2$, $gl$ and $gr$ in
\texttt{snb\_rlscf}, and proved their equivalence in the theorem
\texttt{snb\_rlscf\_eq\_ieg}.

\begin{verbatim}
snb_rlscf_eq_ieg : "derl (nrulefs snb_rlscf) = derl (nrulefs snb_ieg_rlscf)"
\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}, which expresses Theorems 17 and 19.
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{verbatim}
sn_dn_der : "derl (nrulefs snb_rlscf) <= adm biilldn"
sn_dn_equiv : "(?r : derrec (nrulefs snb_rlscf) {}) =
  (?r : derrec biilldn {})" 
\end{verbatim}

To get Corollary~20, which looks like a straightforward consequence of 
Theorem~19, we in fact have to define a formula $A$ being provable.
Conventionally, in \biilldc\ we take this to mean that $I \vdash A$ is
derivable, but in BiILL it seems more natural to use
$\cdot \Rightarrow A$, or, in our implementation, $NI \Rightarrow A$.

With these interpretations we need to prove the invertibility of either the 
$(I\vdash)$ rule in \biilldc\ or the $I_l$ rule of \biilldn.
We did the former, using a lemma \texttt{pscrel\_adm} designed to facilitate
proofs of the invertibility of logical rules.

\begin{verbatim}
pscrel_adm : "[| ALL ps c x.  (ps, c) : ?rls --> (c, x) : ?rel -->
	(EX ps'. (ps', x) : derl ?rls & (ps, ps') : allrel ?rel);
      (?s, ?s') : ?rel |] ==> ([?s], ?s') : adm ?rls"
dc_dn_equiv : "((T |- ?A) : derrec (rulefs rlscfb) {}) =
         (($NI => ?A) : derrec biilldn {})"
\end{verbatim}

\begin{verbatim}
\end{verbatim}

\begin{thebibliography}{10}
\bibitem{fill-csl}
\newblock 
Ranald Clouston, Jeremy Dawson, Rajeev Gor\'e \& Alwen Tiu.
\newblock Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic.
\newblock In Proc.\ CSL, 2013. DETAILS
\end{thebibliography}

\end{document}

