
\newpage
\appendix

\section{Isabelle text of selected definitions and theorems}

\subsection{Isabelle text of definitions and basic lemmas}
\begin{verbatim}
ldi_derl :
  "[| ALL psc:?pscs. ldi ?lrules ?drules psc; (?ps, ?c) : derl ?pscs |] ==>
          ldi ?lrules ?drules (?ps, ?c)"
cldi_ex_interp :
  "[| (ALL psc : ?pscs. cldi ?lrules ?drules psc); 
         ?c : derivableR ?drules {} |] ==> edi ?lrules ?drules ?c"
\end{verbatim}

\subsection{Isabelle text of lemmas for \S\ref{s-unary}, unary logical rules}
Belnap's C4 property is used in the proof of cut-elimination, it being one of
the properties that structural rules must satisfy for Belnap's cut-elimination
theorem to apply to a Display Calculus.

Here, \texttt{seqSVs'} $b ~ seq$ is a list of the structural variables 
in succedent (if $b = True$) or antecedent (if $b = False$) position 
in a sequent $seq$ 

\begin{verbatim}
C4_def : "C4 ?rule == ALL prem:set (premsRule ?rule). 
  ALL b. ALL s:set (seqSVs' b (conclRule ?rule)).
    s ~: set (seqSVs' (~ b) prem)"
\end{verbatim}

\begin{verbatim}
SF_some_sub :
   "[| ALL (ps, c):PC ` ?rules. ~ seqCtnsFml c & distinct (seqSVs c);
         ALL r:?rules. C4 r; (?prems, ?concl) : derl (PC ` rulefs ?rules);
         (?concl, ?sconcl) : seqrep ?sa (Structform ?fml) ?Z |]
      ==> EX sprems.
         (?prems, sprems) : seqreps ?sa (Structform ?fml) ?Z &
         (sprems, ?sconcl) : derl (PC ` rulefs ?rules)" 
\end{verbatim}

Lemma~\ref{l-dp-ldi} is actually proved more generally.
We define an \emph{invertible set} of rules to be a set of unary rules such
that the inverse of any of them is derivable from the substitution instances of
them.
The set \texttt{aidps} of rules satisfies this property
(theorem \texttt{inv\_rules\_aidps}) 

\begin{verbatim}
inv_rules_def : "inv_rules ?rules == ALL r:?rules. EX p.
  premsRule r = [p] & ([conclRule r], p) : derl (PC ` rulefs ?rules)" 

inv_rules_aidps : "inv_rules aidps" 
\end{verbatim}

Then Lemma~\ref{l-dp-ldi} actually holds for any invertible set of rules.

\begin{verbatim}
bi_lrule_ldi_lem : "[| ?r : rulefs ?lrules; inv_rules ?lrules |] ==>
  ldi ?lrules ?drules (PC ?r)" 
\end{verbatim}

\begin{verbatim}
non_bin_lem_gen "[| aidps <= ?drules; {nota, nots} <= ?drules;
        (?ps, ?concl) : PC ` rulefs aidps;
        ALL p:set ?ps. ~ seqHasComma p;
        ALL p:set ?ps. Ex (interp ?drules p) |] ==>
     Ex (interp ?drules ?concl)"
\end{verbatim}

\begin{verbatim}
tS_ldi : "ldi aidps rlscf ([], $I |- T)"
fA_ldi : "ldi aidps rlscf ([], F |- $I)"
idf_ldi : "ldi aidps rlscf ([], ?A |- ?A)"
\end{verbatim}

\begin{verbatim}
sdA1 : "[| ALL U. ([$?Y' |- $U], $?Y |- $U) : ?logI; strIsLog ?W;
         (True, ?W, ?W') : strrep ?Y ?Y' |] ==>
      ([$?W' |- $?Z], $?W |- $?Z) : derl (?logI Un PC ` rulefs aidps)" 
\end{verbatim}

\begin{verbatim}
seqrep_interpA : "[| ALL U. ([$?Y' |- $U], $?Y |- $U) : ?logI;
     seqIsLog ($?W |- $?Z); strFVPPs ?Y' <= strFVPPs ?Y;
     ($?W |- $?Z, $?W' |- $?Z') : seqrep False ?Y ?Y';
     ?logI <= PC ` rulefs ?rules; aidps <= ?rules;
     interp ?rules ($?W' |- $?Z') ?intp |] ==>
  interp ?rules ($?W |- $?Z) ?intp" 
\end{verbatim}

\begin{verbatim}
logA_ldi : "[| ALL (ps, c):PC ` aidps. ~ seqCtnsFml c & distinct (seqSVs c);
         Ball aidps C4; strFVPPs ?Y <= fmlFVPPs ?fml; seqIsLog (?fml |- $?U);
         ALL U. ([$?Y |- $U], ?fml |- $U) : ?logI;
         ?logI <= PC ` rulefs ?rules; aidps <= ?rules |] ==>
     ldi aidps ?rules ([$?Y |- $?U], ?fml |- $?U)" 
\end{verbatim}

We have results analogous top the above for a logical introduction rule 
for a formula on the right,
are \texttt{seqrep\_interpS} and \texttt{logS\_ldi}.

\subsection{Isabelle text of lemmas for \S\ref{s-lair2},
additive binary logical rules}
\begin{verbatim}
SF_some1sub : "[| ALL (ps, c):PC ` ?rules.
    ~ seqCtnsFml c & distinct (seqSVs c) & seqIsLog c &
    Ball (set ps) seqIsLog &
    (ALL p:set ps.  distinct (seqSVs p) &
      (ALL b. set (seqSVs' b p) = set (seqSVs' b c)));
    Ball ?rules C4; (?prems, ?concl) : derl (PC ` rulefs ?rules);
    (?concl, ?sconcls) : lseqrep ?sa (Structform ?fml) ?Zs |] ==>
  EX spremss. (?prems, spremss) : lseqreps ?sa (Structform ?fml) ?Zs &
    (ALL n<length ?Zs. (map (%l. l ! n) spremss, ?sconcls ! n) :
      derl (PC ` rulefs ?rules))" 
\end{verbatim}

\begin{verbatim}
lseqrep_interpA : "[| rlscf <= ?rules;
   ALL U. (map (%Y'. $Y' |- $U) ?Ys, $?Y |- $U) : ?logI;
   seqIsLog ($?W |- $?Z); ALL Y':set ?Ys. strFVPPs Y' <= strFVPPs ?Y;
   ($?W |- $?Z, ?Ss') : lseqrep False ?Y ?Ys;
   ?logI <= PC ` rulefs ?rules; aidps <= ?rules;
   ALL S:set ?Ss'. Ex (interp ?rules S) |] ==>
 Ex (interp ?rules ($?W |- $?Z))"
\end{verbatim}

\begin{verbatim}
mlogA_ldi : "[| ALL (ps, c):PC ` aidps.  ~ seqCtnsFml c &
    distinct (seqSVs c) & seqIsLog c & Ball (set ps) seqIsLog &
    (ALL p:set ps.  distinct (seqSVs p) &
      (ALL b. set (seqSVs' b p) = set (seqSVs' b c)));
    Ball aidps C4; seqIsLog (?fml |- $?U);
    ALL U. (map (%Y'. $Y' |- $U) ?Ys, ?fml |- $U) : ?logI;
    ALL Y:set ?Ys. strFVPPs Y <= fmlFVPPs ?fml;
    ?logI <= PC ` rulefs ?rules; aidps <= ?rules; rlscf <= ?rules |] ==>
   ldi aidps ?rules (map (%Y'. $Y' |- $?U) ?Ys, ?fml |- $?U)" 
\end{verbatim}

\subsection{Isabelle text of lemmas for \S\ref{s-ldi-uc-ctr},
Unit-Contraction and Contraction}

The set \texttt{stars} $S$ is the set of all structures which consist of the
structure $S$ preceded by any number of occurrences of \texttt{Star}
(ie, of \# symbols).

The relation \texttt{seqdel (stars I)} will be the relation used for
unit-contraction, where
$(p, c) \in \texttt{seqdel}\ Fs$ if $p$ is obtained from $c$ by deleting 
(in any number of places) a structure in $Fs$.

\begin{verbatim}
ex_box_uc : "[| ?atom = I; (?C, ?Cd) : seqdel (stars ?atom);
    ?Cd : derivableR aidps {?Cd'} |] ==>
   EX C'.  (C', ?Cd') : seqdel (stars ?atom) &
     C : derivableR aidps {?C'}"
\end{verbatim}

The rules for replacing $(\emptyset, X)$ by $X$ on the left and the right
of the $\vdash$ are \texttt{ila} and \texttt{ils},
and the left contraction rule is \texttt{cA}.

\begin{verbatim}
delI_der : "[| (?Y, ?Y') : strdel (stars I); aidps <= ?rules;
    {ila, ils} <= ?rules |] ==>
   {([$?X |- $?Y], $?X |- $?Y'), ([$?Y |- $?X], $?Y' |- $?X)} <=
     derl (PC ` rulefs ?rules)" 

ldi_ila : "[| aidps <= ?rules; {ila, ils} <= ?rules |] ==>
   ldi aidps ?rules (PC ila)" 
\end{verbatim}

\begin{verbatim}
ctr_der : "[| (?Y, ?Y') : mstrctr; aidps <= ?rules; {cA} <= ?rules |] ==>
  {([$?X |- $?Y], $?X |- $?Y'), ([$?Y |- $?X], $?Y' |- $?X)} <=
    derl (PC ` rulefs ?rules)" :

ldi_cA : "[| aidps <= ?rules; {cA} <= ?rules |] ==> ldi aidps ?rules (PC cA)" 
\end{verbatim}

Note that the theorem \texttt{ctr\_der} needs to be applied twice 
(once for each side of the $\vdash$) to give the result in the main text.

\subsection{Isabelle text of lemmas for \S\ref{s-del}, the Deletion Lemma}
The proof threw up a number of (logically) 
trivial cases which nonetheless needed particular results to be included
as lemmas to be used automatically in simplification, such as:

\begin{verbatim}
stars_Sf_not_Comma : "Comma ?X ?Y ~: stars (Structform ?fml)" 
Stars_Sf_ne_Comma : "Comma ?X ?Y ~= funpow Star ?n (Structform ?fml)" 
Stars_eq_Comma_iff : "(Comma ?X ?Y = funpow Star ?n (Comma ?U ?V)) =
    (?n = 0 & ?X = ?U & ?Y = ?V)" 
\end{verbatim}

\begin{verbatim}
deletion :
   "[| ?atom = Structform ?fml; (?C, ?Cd) : seqdel ?pn (stars ?atom);
         ?C' : derivableR aidps {?C} |]
      ==> (EX Cd'.
          (?C', Cd') : seqdel ?pn (stars ?atom) &
          Cd' : derivableR aidps {?Cd}) |
      (EX n m Z1 Z2.
          ?C' = ($(funpow Star n ?atom) |- $(funpow Star m (Comma Z1 Z2))) &
          (if odd m then $Z1 |- * $Z2 else * $Z1 |- $Z2)
          : derivableR aidps {?Cd} |
          ?C' = ($(funpow Star m (Comma Z1 Z2)) |- $(funpow Star n ?atom)) &
          (if even m then $Z1 |- * $Z2 else * $Z1 |- $Z2)
          : derivableR aidps {?Cd})" : Thm.thm
\end{verbatim}

\subsection{Isabelle text of lemmas for \S\ref{s-ldi-wk},
Unit-Weakening and Weakening}
\begin{verbatim}
ex_box_repI_atoms :
    "[| (?C, ?Cd) : seqrepI str_atoms; ?C : derivableR aidps {?C'} |] ==>
    EX Cd'. (?C', Cd') : seqrepI str_atoms & ?Cd : derivableR aidps {Cd'}"
\end{verbatim}

\begin{verbatim}
seqrepI_der : "[| (?S', ?S) : seqrepI ?Fs; aidps <= ?rules;
    {ila, ils, mra} <= ?rules |] ==>
  ([?S], ?S') : derl (PC ` rulefs ?rules)"

ldi_repI_atoms : "[| aidps <= ?rules; {ila, ils, mra} <= ?rules;
             (?c, ?p) : seqrepI str_atoms |] ==>
	    ldi aidps ?rules ([?p], ?c)"
\end{verbatim}

\begin{verbatim}
seqwk_der : "[| (?S', ?S) : seqdel ?Fs;
      aidps <= ?rules; {mra} <= ?rules |] ==>
    ([?S], ?S') : derl (PC ` rulefs ?rules)" 
\end{verbatim}

\begin{verbatim}
ldi_wkI : "[| aidps <= ?rules; {mra, ila, ils, tS, fA} <= ?rules;
            (?c, ?p) : seqdel (stars I) |] ==>
          cldi aidps ?rules ([?p], ?c)" 
\end{verbatim}

\subsection{Isabelle text of lemmas for \S\ref{s-mult},
  Binary Multiplicative Logical Introduction rules}

\begin{verbatim}
wkI_der : "[| (?Y', ?Y) : strdel (stars I); aidps <= ?rules;
         {iila, iils} <= ?rules |] ==>
   {([$?X |- $?Y], $?X |- $?Y'), ([$?Y |- $?X], $?Y' |- $?X)}
      <= derl (PC ` rulefs ?rules)" 
\end{verbatim}

\begin{verbatim}
ldi_wkI_alt : "[| aidps <= ?drules;
     {iila, iils, tS, fA, ila, ils, tA, fS} <= ?drules;
     (?c, ?p) : seqdel (stars I) |] ==>
   cldi aidps ?drules ([?p], ?c)"
\end{verbatim}

The following result applies to display postulates satisfying 
a set of standard set of display postulates properties.
\begin{verbatim}
dp_props_def : "dp_props (?ps, ?c) =
  (length ?ps = 1 & ~ seqCtnsFml ?c & distinct (seqSVs ?c) & seqIsLog ?c &
  (ALL p:set ?ps. seqIsLog p & distinct (seqSVs p) & ~ seqCtnsFml p &
           (ALL b. set (seqSVs' b p) = set (seqSVs' b ?c))))"

repm_some1sub :
   "[| ALL rule:?rules. dp_props (PC rule); ?As ~= [];
       ([?prem], ?concl) : derl (PC ` rulefs ?rules);
       (?concl, ?sconcls) : lseqrepm ?rsa ?sa (Structform ?fml) ?As |]
    ==> EX sprems. 
       (?prem, sprems) : lseqrepm ?rsa ?sa (Structform ?fml) ?As &
       (ALL k<length ?As.
	   ([sprems ! k], ?sconcls ! k) : derl (PC ` rulefs ?rules))"
\end{verbatim}

We mention that the proof of \texttt{repm\_some1sub} involved very considerable
effort; it used the following lemma (see the proofs of it in \texttt{GRepm.ML})

\begin{verbatim}
repm_seq_sub :
   "[| ~ seqCtnsFml ?pat; distinct (seqSVs ?pat);
     (seqSubst ?suba ?pat, ?Ys) : lseqrepm ?rsa ?pn (Structform ?A) ?Xs |]
   ==> EX subys. map (%suby. seqSubst suby ?pat) subys = ?Ys"
\end{verbatim}

\begin{verbatim}
ands_mix_gen :
   "[| PC ` rulefs aidps <= ?rules; ands_rep <= ?rules;
      PC ` rulefs ilrules <= ?rules;
    (?Z, [?X, ?Y]) : lseqrepm repnI_atoms True (Structform (?A && ?B))
      [Structform ?A, Structform ?B] |] ==> ?Z : derrec ?rules {?X, ?Y}"
\end{verbatim}

\begin{verbatim}
lseqrepm_interp_andT :
   "[| ands_rep <= ?rules; ora_rep <= ?rules;
         PC ` rulefs {anda} <= ?rules; PC ` rulefs {ors} <= ?rules;
         PC ` rulefs aidps <= ?rules; PC ` rulefs ilrules <= ?rules;
	 (?WZ, [?pa, ?pb]) : lseqrepm repnI_atoms True 
	    (Structform (?A && ?B)) [Structform ?A, Structform ?B];
         ALL S:set [?pa, ?pb]. Ex (interpn ?rules S) |]
      ==> Ex (interpn ?rules ?WZ)" 
\end{verbatim}

\begin{verbatim}
ldin_ands_rep : "[| (?ps, ?WZ) : ands_rep; PC ` rulefs ilrules <= ?drules;
            PC ` rulefs aidps <= ?drules; PC ` rulefs {ors} <= ?drules;
	   PC ` rulefs {anda} <= ?drules; ora_rep <= ?drules;
	  ands_rep <= ?drules; ?lrules <= aidps |] ==>
	ldin ?lrules ?drules (?ps, ?WZ)" 
\end{verbatim}

\begin{verbatim}
ldi_add_equiv : "(?c : derrec ldi_add {}) = (?c : derivableR rlscf_nw {})" 
ldi_add_cldin : "?rule : ldi_add ==> cldin aidps ldi_add ?rule"
ldi_add_interp : "Ball (derrec ldi_add {}) (edin aidps ldi_add)" 
rlscf_nw_interp : "Ball (derivableR rlscf_nw {}) (edi aidps rlscf_nw)" 
\end{verbatim}

