%
% \documentclass{paper}
\documentclass[a4paper,11pt]{article}
%\documentclass[twocolumn,a4paper,11pt]{article}

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

\renewcommand{\today}{\number\day\ 
  \ifcase\month\or
  January\or February\or March\or April\or May\or June\or
  July\or August\or September\or October\or November\or December\fi
  \ \number\year}

\setcounter{secnumdepth}2
\setcounter{tocdepth}2

% \newtheorem{theorem}{Theorem}[section]

\newcommand{\qed}{\hfill$\dashv$}

\newenvironment{proof}{
 \noindent{\bf Proof:}}{\mbox{\bf Q.E.D.}\vspace{1ex}}

\newtheorem{definition}{Definition}[section]
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}{Lemma}[section]
\newtheorem{corollary}{Corollary}[section]
    
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Preamble

\newcommand\derl{\texttt{derl}}
\newcommand\dercl{\texttt{dercl}}
\newcommand\derrec{\texttt{derrec}}
\newcommand\rls{\texttt{rls}}
\newcommand\adm{\texttt{adm}}
\newcommand{\pscrel}{\mathtt{rls}}
\newcommand{\dersrec}{\mathtt{dersrec}}
\newcommand{\prems}{\mathtt{plvs}}

\newcommand{\hash}{\texttt{\#}}
\newcommand{\bra}{\texttt{\{}}
\newcommand{\ket}{\texttt{\}}}

\newcommand\cfile{}

\newcommand\comment[1]{} 
\newcommand\cc[1]{#1} % for label names 

\newcommand\invrule[2]{ 
% for use in non-math mode, args interpreted in math mode
  \begin{tabular}{@{}c@{}}
  $ #1 $ \\ \hline \hline $ #2 $
  \end{tabular}}
\newcommand\slrule[2]{ % similar to \frac, except
% for use in non-math mode, args interpreted in math mode
  \begin{tabular}{@{}c@{}}
  $ #1 $ \\ \hline $ #2 $
  \end{tabular}}

\renewcommand\theenumi{(\alph{enumi})}
\renewcommand\labelenumi{\theenumi}
\renewcommand\theenumii{(\roman{enumii})}
\renewcommand\labelenumii{\theenumii}

\newcommand\src[1]{source file \texttt{#1}}
\newcommand\apsrc[1]{Appendix \ref{app:code}}
\newcommand\seesrc[1]{(see source file \texttt{#1})}
\newcommand\insrc[1]{in source file \texttt{#1}}
\newcommand\page[1]{page~\pageref{#1}}
\newcommand\fig[1]{Fig.~\ref{fig:#1}}
\newcommand\ch[1]{Chapter~\ref{ch:#1}}
\newcommand\tbl[1]{Table~\ref{tbl:#1}}
\newcommand\thrm[1]{Theorem~\ref{thrm:#1}}
\newcommand\lem[1]{Lemma~\ref{lem:#1}}
\newcommand\ttl[1]{\tti{#1}\label{#1}}
\newcommand\ttdl[1]{\texttt{#1}\tti{#1}\label{#1}}
\newcommand\ttdef[1]{\texttt{#1}\tti{#1}}
\newcommand\tti[1]{\index{#1@\texttt{#1}}}
\newcommand\bfi[1]{\textbf{#1}\index{#1|textbf}}
\newcommand\dRA{{\boldmath $\delta$}\textbf{RA}}
\newcommand\dKt{{\boldmath $\delta$}\textbf{Kt}}
\newcommand\NRA{\textbf{NRA}}
\newcommand\RA{\textbf{RA}}
%\newcommand\M{$\mathcal M$}
\newcommand\MC{\ensuremath{\mathcal C}}
\newcommand\MD{\ensuremath{\mathcal D}} 
\newcommand\MP{\ensuremath{\mathcal P}}
\newcommand\MQ{\ensuremath{\mathcal Q}}
\newcommand\MR{\ensuremath{\mathcal R}}
\newcommand\MS{\ensuremath{\mathcal S}}
\newcommand\M{\ensuremath{\mathcal M}}
\newcommand\Mp{$\mathcal M'$}
\newcommand\psl{\ensuremath\MQ_{l1} \ldots \MQ_{ln}}
\newcommand\psr{\ensuremath\MQ_{r1} \ldots \MQ_{rm}}

\newcommand\up[1]{\vspace{-#1ex}} 
\newcommand\vpf{\vspace{-3ex}} % to reduce space before proof tree
\newcommand\1{\textbf 1}
\newcommand\0{\textbf 0}
\newcommand\cut{(\emph{cut})}
\newcommand\dt{\texttt{dt}}
\newcommand\dtn{\texttt{dtn}}

\newcommand{\pordered}[3]{#1 <_{\texttt{\scriptsize #2}} #3}
\newcommand{\Revpordered}[3]{#1 >_{\texttt{\scriptsize #2}} #3}
\newcommand{\LRPord}[2]{\pordered{#1}{LRP}{#2}}
\newcommand{\cutord}[2]{\pordered{#1}{cut}{#2}}
\newcommand{\snoneord}[2]{\pordered{#1}{sn1}{#2}}
\newcommand{\dtord}[2]{\pordered{#1}{dt}{#2}}
\newcommand{\Revdtord}[2]{\Revpordered{#1}{dt}{#2}}

\newcommand\GL{\textbf{GL}}
\newcommand\GLS{\textrm{GLS}}
\newcommand\GLR{\textit{GLR}}
\newcommand\GLRp{\ensuremath{\Box X, X, \Box B \vdash B}} % premise of GLR
\newcommand\GLRc{\ensuremath{\Box X \vdash \Box B}} % conclusion of GLR
\newcommand\lxxc{\ensuremath{\Box X, X \vdash B}} % conclusion of lem20
\newcommand\gbna{\ensuremath{\Box G, \Box B^k \vdash \Box A}} 
\newcommand\GLRB{\textit{GLR}($B$)}
\newcommand\GLRXB{\textit{GLR}($X,B$)}

\newcommand\pmz{\texttt{pm0}}
\newcommand\pmgez{\texttt{pm\_ge0}}

\newcommand\delz{\texttt{del0}}
\newcommand\delzs{\ensuremath{\partial^0}}

\newcommand\muxbn{\texttt{muxbn}}

\newcommand\lgp{\mathrm{S4C}}
\newcommand\wbx{\Box}
\newcommand\wdi{\lozenge}
%\newcommand\nxt{\bigcirc}
\newcommand\nxt{\circ}
\newcommand\limp{\rightarrow}
\newcommand\leqv{\leftrightarrow}

\newcommand{\Boxes}{\ensuremath{\vec{\Phi}}}
\newcommand{\Boxesi}[1]{\ensuremath{\vec{\Phi}_{-#1}}}

\newcommand{\cute}{cut-elimination}
\newcommand{\cuta}{cut-admissibility}
\newcommand{\ctra}{contraction-admissibility}
\newcommand{\weaka}{weakening-admissibility}

\newcommand{\ds}{\displaystyle\strut}

\newcommand{\idrule}[2]{
 \mbox{#1 \ $\ds$ #2}
}

\newcommand{\urule}[4]{
   \AxiomC{#2}
   \LeftLabel{#1}
   \RightLabel{#4}
   \UnaryInfC{#3}
   \DisplayProof
}

\newcommand{\brule}[4]{
  \AxiomC{#2}
  \AxiomC{#3}
  \LeftLabel{#1}        
  \BinaryInfC{#4} 
  \DisplayProof
}



\hyphenation{
 non-classical
 conn-ection
 typi-cally
 tradi-tional
 frame-works
 con-clusion
 der-ivation
}

\pagestyle{plain}

\begin{document}

\title{Machine-checked Proof-Theory for Propositional Modal Logics}

\author{
 Jeremy E.\ Dawson\thanks{Supported by Australian Research Council
   Grant DP120101244.},
 Rajeev Gor\'e and
 Jesse Wu
\\
Logic and Computation Group,
School of Computer Science
\\ The Australian National University,
Canberra ACT 2601
%, Australia
}

\date{}
%% Title 
\maketitle

\begin{abstract}
  We describe how we machine-checked the admissibility of the standard
  structural rules of weakening, contraction and cut for
  multiset-based sequent calculi for the unimodal logics S4, S4.3 and K4De,
  as well as for the bimodal logic $\lgp$ recently investigated by Mints.
  Our proofs for both S4 and S4.3 appear to be new while our
  proof for $\lgp$ is different from that originally presented by Mints,
  and appears to avoid the complications he encountered. 
  The paper is intended to be an overview of how to machine-check proof theory
  for readers with a good understanding of proof theory.
\end{abstract}

%% Here begins the main text

\tableofcontents
\newpage

\section{Introduction} \label{s-intro}

Sequent calculi provide a rigorous basis for meta-theoretic studies of
various logics. The central theorem is cut-elimination/admissibility,
which states that detours through lemmata can be avoided, since it can
help to show many important logical properties like consistency,
interpolation, and Beth definability. Cut-free sequent calculi are
also used for automated deduction, for nonclassical extensions of
logic programming, and for studying the connection between normalising
lambda calculi and functional programming.  Sequent calculi, and their
extensions, therefore play an important role in logic and computation.

Meta-theoretic reasoning about sequent calculi is error-prone because
it involves checking many combinatorial cases,
with some being very difficult, but many being very
similar. Invariably, authors resort to expressions like ``the other
cases are similar'', or ``we omit details''. The literature contains
many examples of meta-theoretic proofs with serious and subtle
errors in the original pencil-and-paper proofs. For example, the
cut-elimination theorem for the modal ``provability logic'' GL,
where $\Box \varphi$ can be read as ``$\varphi$ is provable in Peano
Arithmetic'', has a long and chequered history which has only recently
been resolved~\cite{Gore08}. 

Here, we describe how we formalised cut-elimination for traditional,
propositional, multiset-based sequent calculi without explicit
structural rules for the propositional modal logics S4, S4.3, K4De
and $\lgp$ using the interactive proof-assistant Isabelle/HOL.
As far as we know, the proofs for S4 and S4.3 are new,
and avoid the complexities of previous proofs for these logics.
Our results also confirm the recent claim of
cut-elimination for $\lgp$ due to Mints, although our proof is different,
and avoids the complications he encountered in his proofs.

In Section~\ref{sec:preliminaries}, we briefly describe traditional
sequent calculi, discuss the need for multisets,
and describe the general form of our main theorems.
%
In Section~\ref{s-modal} we describe the modal logics we study.
%
In Section~\ref{s-ipa} we give a brief overview of how interactive proof
assistants work.
%
In Section~\ref{s-eol} we show how we encode
% describe techniques and functions we have
% defined for reasoning about derivations, and
formulae, sequents and rules, showing a sequent rule as an example.
%
In Section~\ref{s-dp} we describe how we encoded the notion of derivability,
giving rise to what we call ``implicit derivations''.
%
In Section~\ref{s-dtobj} we show how we encoded ``explicit derivations''
as concrete tree data structures, and the functions used to reason about them.
%
In Section~\ref{s-gls} we describe how we generalised the forms of our 
sequent rules to easily capture rule skeletons extended with arbitrary
contexts which are essential to make weakening admissible.
%
In Section~\ref{s-wic} we describe how we encoded the properties of weakening,
invertible of some rules, and contraction in Isabelle.
%
In Section~\ref{s-cagen} we describe how we generalised our previous work on
explicit derivations to facilitate inductive proof of properties 
(such as the admissibility of contraction or cut), and
in Section~\ref{s-main-lemmas} we describe this further specifically for
cut-admissibility.
%
In Sections~\ref{s-s4} to \ref{s-s4cns} we describe the 
cut-admissibility proofs for the specific logics S4, S4.3, K4De and S4C.
%
The remaining sections discuss related work and conclude.

We assume the reader is familiar with basic proof-theory
and higher-order logic, but assume that the reader is a novice
in interactive proof assistants.
%
Our Isabelle code can be found at
\url{http://users.rsise.anu.edu.au/~jeremy/isabelle/2005/seqms/}.  
Some of this work was reported informally in \cite{Gore09}
and also, more formally, in \cite{dawson-gore-generalised}.

%TO DO - include explanation of Isabelle notation

\section{Preliminaries}
\subsection{Sequents Built From Multisets Versus Sets}
\label{sec:preliminaries}

Proof-theorists typically work with sequents  $\Gamma
\vdash \Delta$ where $\Gamma$ and $\Delta$ are ``collections'' of
formulae. The ``collections'' found in the literature increase in
complexity from simple sets for classical logic \cite{gentzen-lk},
to multisets for linear logic \cite{girard-linear-logic},
to ordered lists for substructural logics \cite{schroeder-heister},
to complex tree structures for display logics \cite{belnap1982}.
%
A sequent rule typically has a rule name, a (finite) number of premises,
a side-condition and a conclusion.
% \begin{prooftree}
%   \AxiomC{$\Gamma_1 \vdash \Delta_1 
%            \qquad\cdots\qquad 
%            \Gamma_n \vdash \Delta_n$}
%   \LeftLabel{RuleName}
%   \RightLabel{Condition}
%   \UnaryInfC{$\Gamma_0 \vdash \Delta_0$}
% \end{prooftree}
Rules are read top-down as ``if all the premises hold then the
conclusion holds''.  A derivation of the judgement $\Gamma \vdash
\Delta$ is typically a finite tree of judgements with root $\Gamma
\vdash \Delta$ where parents are obtained from children by ``applying
a rule''. We use ``derivation''  to refer to a
proof \emph{within} a calculus, reserving ``proof'' for a
meta-theoretic proof of a theorem \emph{about} the calculus.  

Sequent calculi typically contain three structural rules called
weakening, contraction and cut. These rules are bad for automated
reasoning using backward proof-search since they can be applied at any
time. Thus for backward proof-search, we are interested in sequent
calculi which do not contain explicit rules for weakening, contraction
and cut. The traditional way to design such calculi is to assume that
sequents are built out of multisets, omit these rules from the
calculus itself, and prove that each of these rules is
admissible. That is, for each rule, we have to prove that the
conclusion sequent is derivable if each of its premises are derivable.
For example, our work does not
regard the cut rules shown below as being part of the
system:
\[
  \AxiomC{$\Gamma \vdash A, \Delta$}
  \AxiomC{$\Gamma, A \vdash \Delta$}
  \LeftLabel{(cut)}
  \BinaryInfC{$\Gamma \vdash \Delta$}
  \DisplayProof
\qquad
  \AxiomC{$\Gamma_1 \vdash A, \Delta_1$}
  \AxiomC{$\Gamma_2, A \vdash \Delta_2$}
  \LeftLabel{(cut)}
  \BinaryInfC{$\Gamma_1, \Gamma_2 \vdash \Delta_1, \Delta_2$}
  \DisplayProof
\]
Thus our results will be lemmata of the form:
if $\Gamma \vdash A, \Delta$ is (cut-free) derivable
and $\Gamma, A \vdash \Delta$ is (cut-free) derivable
then $\Gamma \vdash \Delta$ is (cut-free) derivable.

\subsection{Our Modal Logics}
\label{s-modal}

The sequent calculi we study are designed to reason about the
meta-theory of the basic modal logics S4, S4.3, K4De (called GTD by
Mints) and $\lgp$. Semantically, the first three are mono-modal logics
characterised, respectively, by Kripke frames having: 
reflexive and transitive frames;
reflexive, transitive and linear frames; and transitive and dense
frames. The logic $\lgp$, called dynamic topological
logic, is a bimodal logic where $\wbx$ is captured by a reflexive and
transitive binary relation $R_\wbx$ and where $\nxt$ is captured by a
serial and discrete linear relation $R_\nxt$ with an interaction
between them of ``confluency'':
\begin{eqnarray}
  \label{eq:1}
\forall x \forall y \forall z \exists u. 
 R_\wbx(x,y) \;\&\; R_\nxt(x, z) \Rightarrow R_\nxt(y,u) \;\&\;
 R_\wbx(z, u)
\end{eqnarray}

The Hilbert-calculi for these logics are obtained by extending a
traditional Hilbert-calculus for classical propositional logic with
the axioms and inference rules as shown below using the naming
conventions given in
Figure~\ref{fig:axioms-and-inference-rules}:

\begin{figure}[t]
  \centering
\begin{tabular}[c]{llll}
  Axiom Name & Schema & Rule Name & Schema
\\
   K
  & $\wbx (\varphi\limp\psi) \limp (\wbx\varphi \limp \wbx\psi)$ 
  & RN$\wbx$
  & $\varphi$/$\wbx\varphi$
\\
   $\Box\bot$
  & $\Box\bot \leqv \bot$
  & RN$\circ$
  & $\varphi$/$\circ\varphi$
\\
   De
  & $\wbx\wbx\varphi \limp \wbx\varphi $ 
  & & \\
   T 
  & $\wbx\varphi \limp \varphi $ 
& \\
   4 
  & $\wbx\varphi \limp \wbx\wbx\varphi $ 
& \\
   .3 
  & $\wbx (\wbx\varphi\limp\psi) \lor \wbx (\wbx\psi \limp \varphi)$ 
& \\
   C
  & $\nxt\wbx\varphi \limp \wbx\nxt\varphi$  
& \\
   K$_\nxt$
  & $\nxt (\varphi\limp\psi) \leqv (\nxt\varphi \limp \nxt\psi)$ 
& \\
   $\nxt\bot$
  & $\nxt \bot \leqv \bot$
\end{tabular}
  \caption{Various Axioms and Inference Rules}
  \label{fig:axioms-and-inference-rules}
\end{figure}

\begin{center}
\begin{tabular}[c]{lll}
  Logic & Axioms & Rules
\\
  S4 & K,$\Box\bot$,4,T & RN$\wbx$
\\
  S4.3 & K,$\Box\bot$,4,T,.3 & RN$\wbx$
\\
 K4De (GTD) & K,$\Box\bot$,4,De & RN$\wbx$
\\
 $\lgp$ & K,$\Box\bot$,K$_{\nxt}$,T,4,C,$\nxt\bot$  & RN$\wbx$, RN$\nxt$
\end{tabular}
\end{center}

% The logic $\lgp$ is obtained from S4 by adding the following axioms
% and rule:

% \begin{tabular}[c]{ll}
%   Axiom/Rule Name & Schema
% \\
%    K$_\nxt$
%   & $\nxt (\varphi\limp\psi) \leqv (\nxt\varphi \limp \nxt\psi)$ 
% \\
%    $\nxt\bot$
%   & $\nxt \bot \leqv \bot$
% \\
%    C
%   & $\nxt\wbx\varphi \limp \wbx\nxt\varphi$  
% \end{tabular}

The modal logic $\lgp$ is designed to capture the basic logic for
hybrid systems \cite{davoren-gore-aiml-2001}
where equation~(\ref{eq:1}) captures the lower semi-continuity of
the linear discrete relation with respect to the topological
interpretation of the $\wbx$-connective.

\subsection{Interactive Proof Assistants}\label{s-ipa}

Interactive proof-assistants are now a mature technology for
``formalising mathematics'' \cite{ams-formal-proof}.
They come in many different flavours as
indicated by the names of some of the most popular ones
{\tt Mizar, HOL, Coq, LEGO, NuPrl, NqThm, Isabelle,
    $\lambda$-Prolog, HOL-Lite, LF, ELF, Twelf},
with apologies to those whose favourite proof-assistant we have
omitted. 

Most of the modern proof-assistants are implemented using a modern
functional programming language such as ML, which was specifically
designed for the implementation of, and interaction with,
such proof-assistants.

The lowest levels typically implement a typed $\lambda$-calculus with
hooks provided to allow the encoding of further logical notions such as
equality of terms on top of this base implementation. The base
implementation is usually very small, comprising of a few hundred
lines of code, so that this code can be scrutinised by experts to
ensure its correctness.

Almost all aspects of proof-checking eventually compile down to a
type-checking problem using this small core, so that trust rests on
strong typing and a well-scrutinised small core of (ML) code.

Most proof-assistants also allow the user to create a proof-transcript
which can be cross-checked using other proof-assistants to guarantee
correctness. 

    \begin{figure}[t]
      \centering
    \begin{tabular}[c]{lr}
        $[ \beta_1 \ ; \  \beta_2 \ ; \ \cdots \ ; \  \beta_n ] \Longrightarrow \alpha$ 
        & $\beta$
    \\[2em]
        $\theta = match(\beta, \alpha)$ 
        & $\beta_1\theta \ ; \ \beta_2\theta \ ; \ \cdots
           \ ; \ \beta_n\theta$
    \end{tabular}
      \caption{Backward Chaining in Logical Frameworks}
    \label{fig:backward-chaining}
    \end{figure}

Figure~\ref{fig:backward-chaining} shows how these logical
frameworks typically work. Thus given some goal $\beta$ and an
expression which claims that $\alpha$ is implied by the conjunction of
$\beta_1$ up to $\beta_n$, the Isabelle engine
pattern-matches $\alpha$ and $\beta$ to find
a substitution $\theta$ such that $\alpha \theta = \beta$, 
and then reduces the original goal $\beta$ to the $n$ subgoals
$\beta_1\theta, \ldots, \beta_n\theta$ (note that $n$ may be 0).
We can then repeat this procedure on each $\beta_i \theta$ until all subgoals
are proved (which requires that each final step produces no new subgoals,
ie, has $n = 0$).
The pattern matching required is usually higher order unification. 
The important point is that the logical framework keeps track of
sub-goals and the current proof state.

The syntax of the ``basic propositions'' such as $\alpha$, $\beta$ is
defined via an ``object logic'', which is a parameter. Different
``object logics'' can be invoked using the same logical-framework for
the task at hand.

The logical properties of ``$;$'' such as associativity or commutativity,
and properties of the ``$\Longrightarrow$'' such as classicality or
linearity are determined by the ``meta-logic'', which is usually fixed
for the logical framework in question.

For example, the meta-logic of Isabelle \cite{paulson-nipkow}
is higher-order typed intuitionistic logic with connectives
$\Longrightarrow$ (implication), $!!$ ($\forall$), $==$ (equality),
and no negation,
while the object-logic is classical higher-order logic 
(HOL) using $\longrightarrow$, \texttt{ALL} ($\forall$), $=$,
\texttt{EX} ($\exists$), and $\sim$ (not) \cite{gordon-hol}.
Unlike in classical first-order logic, which has terms and formulae,
functions and predicates, in Isabelle's meta-logic and in HOL
we just have terms (where a formula is a term of type boolean), and 
functions (where a predicate is a function whose return type is boolean).
Further, functions are themselves terms, of a function type, and
% (eg, $\alpha \to \beta$), and 
``higher order'' simply means that functions can accept other
functions as arguments and can produce functions as results.
This allows a uniform treatment of all these entities.

As noted, the meta-logic allows propositions such as
$[\beta_1 ; \beta_2] \Longrightarrow \alpha$, which in fact is the
pretty-printer's rendering of 
$\beta_1 \Longrightarrow (\beta_2 \Longrightarrow \alpha)$.
Think of this as meaning 
``from $\beta_1$ and $\beta_2$ one may infer $\alpha$''.
Since the object-logic (HOL) contains the connectives $\&$
and $\longrightarrow$ with their usual classical semantics, we find that 
$\beta_1 \& \beta_2 \longrightarrow \alpha$ means the same 
(but in a classical rather than intuitionistic setting)
as $\beta_1 \Longrightarrow (\beta_2 \Longrightarrow \alpha)$.
But to direct Isabelle to actually use an inference
to reduce $\alpha$ to $\beta_1 \theta, \ldots, \beta_n \theta$
as explained above, we need the first (meta-logical) form.
Thus we shall see two logical syntaxes:
$\Longrightarrow$, $!!$ (and ; as explained above)
for the Isabelle intuitionistic meta-level, and 
$\longrightarrow$, \texttt{ALL}, \&, \texttt{EX} and $\sim$
for the classical HOL object-level.
Together they are referred to as Isabelle/HOL \cite{Isabelle-hol}.

\section{A Deep Embedding of Formulae, Sequents and Rules}\label{s-eol}

Recall that the meta-logic provides us with a method for backward
chaining via expressions of the form (see Fig.~\ref{fig:backward-chaining}):
$$[ \beta_1 \ ; \cdots \ ; \ \beta_n ] \Longrightarrow \alpha$$

The usual method for obtaining the power for reasoning about sequent
derivations is to use the full power of higher-order classical logic
(HOL) to build the basic object-level propositions $\beta_i$.

Isabelle's incarnation of HOL provides the usual connectives of logic
such as conjunction, disjunction, implication, negation and the higher
order quantifiers. But it also provides many powerful facilities
allowing us to define new types, define functions which accept and
return other functions as arguments, and even define infinite sets
using inductive definitions \cite{Isabelle-hol}.

For example, the following HOL expressions would capture the usual inductive
definition of the set \texttt{even\_nat} of even natural numbers
by encoding the facts that ``zero is even,
and if $n$ is even then so is $n + 2$'',
where \texttt{:} stands for set membership $\in$:

\begin{verbatim}
                0 : even_nat
                n : even_nat ==> n + 2 : even_nat
\end{verbatim}

Most proof-assistants will automatically generate an induction
principle from a given inductive definition. For example, Isabelle
will automatically generate the usual induction principle which states
that we can prove a property $P$ holds of all even naturals if we
can show that $P(0)$ holds and we can show that $P(n)$ implies
$P(n+2)$. An implicit assumption which facilitates such induction
principles is that the inductive definitions are the \emph{only} way to
construct its members. Thus, if $m$ is an even natural, then it is
either $0$, or is of the form $n + 2$ for some (``smaller'') even natural $n$.
Together, they form the base case and the inductive step of an inductive
definition that defines the set \texttt{even\_nat} 
as the smallest set of terms $0, 0 + 2,
0 + 2 + 2, \ldots$.
It is implicit in these definitions that an inference step such as
   $\mathtt{n : even\_nat} \Longrightarrow \mathtt{n + 2 : even\_nat}$
may be applied only finitely many times.

We previously said that we shall see two syntaxes:
a meta-level intuitionistic logic and an object-level classical HOL syntax.
Since we wish to reason about sequent calculi for modal logics, 
we now need to encode a third logical syntax: 
namely the syntax of modal sequents.


\begin{samepage}
To encode sequent calculus into HOL we first encode terms for capturing
the grammar for recognising formulae as below where comments are enclosed in
\verb!(*! and \verb!*)!:
\begin{verbatim}
datatype formula
      = FC string (formula list)    (* formula connective *)
      | FV string                   (* formula variable   *)
      | PP string                   (* prim prop          *)
\end{verbatim}
\end{samepage}

We use three type constructors \verb!FC!, \verb!FV! and \verb!PP!
which encode, respectively, formula connectives, formula variables, and atomic
formulae (primitive propositions) as HOL terms. Each of them takes one string
argument which is simply the string we want to use for that construction.
The formula connective constructor \texttt{FC} also accepts a list
of formulae, which constitute its subformulae. 
%
For example, the term \verb!FC "&&" [FV "A", PP "q"]! encodes $A\; \land \; q$
where we use ``\verb!&&!'' as the string for conjunction of classical logic.
Since we want to encode modal logics, we require only
the classical connectives, plus three unary modalities
\verb!FC "Box" [.]! for $\wbx .$ and \verb!FC "Dia" [.]! for
$\wdi .$ and \verb!FC "Circ" [.]! for $\nxt$.

Isabelle's HOL allows us to form sets and multisets of objects of an
arbitrary type, so the HOL expressions \verb!formula set! and
\verb!formula multiset! capture the types of modal formula sets
and modal formula multisets.

Using these types we can build a sequent type using a constructor
\texttt{Sequent}:
\begin{verbatim}
datatype 'a sequent = Sequent "'a multiset" "'a multiset"
\end{verbatim}
Here \texttt{'a} is a type variable and the datatype \texttt{'a sequent}
demands that the constructor \texttt{Sequent} is followed by two multisets of
items of type \texttt{'a}.
For example, the datatype \texttt{formula sequent} 
would require our sequents to
be constructed out of multisets of formulae (of type \texttt{formula}).
An alternative infix notation for the constructor \texttt{Sequent} is
$\vdash$ or \texttt{|-}.

We define the type for our sequent rules by the type definition:
\begin{verbatim}
types 'a psc = "'a list * 'a"      (* single rule *)
\end{verbatim}
Such a sequent rule is a pair $(ps, c)$ of a list of items $ps$ (the premises)
and a single item $c$ (the conclusion):
the items are of some type \texttt{'a} which is a parameter.
We shall instantiate the type variable \texttt{'a}
with the type \texttt{formula sequent} to obtain sequents
built from two multisets of modal formulae.

Note that in common parlance we may say that $(ps, c)$ is a rule
% $A \Rightarrow B \Rightarrow A \land B$ is a ``rule'', 
meaning that $ps$ and $c$ may be instantiated in any way.
% In the usage of our Isabelle implementation we would call this a schema 
% which can be instantiated to give infinitely many rules.
Such a ``rule'' is a schema which can be instantiated to give
infinitely many rule instances.
When describing the Isabelle implementation we may refer to a specific pair
$(ps, c)$ as a ``rule'', 
although in the context of logical rules, this could be better described
as a specific instance of a rule schema; 
where we describe our Isabelle theorems involving
``sets of rules'', these will usually be the infinite sets of instances of a
finite set of rule schemata.

% Isabelle's HOL allows us to form lists of objects of an arbitrary
% but fixed type, so we define the type of a rule as a pair with the
% first component being a list of sequent premises and the second
% component being the conclusion sequent:
% $$\mathtt{datatype ~inf ~=~ (seq ~list ~,~ seq)}$$

Thus, we can use the HOL type-declaration below to
declare that $rls$ is a set of sequent rules,
where each element of $rls$ is a pair $(ps, c)$ whose first
component $ps$ is a list of its premise sequents,
and whose second component $c$ is its conclusion sequent:
$$\mathtt{rls ~::~formula~sequent~psc~set}$$
Each sequent consists of two multisets of
items of type \texttt{formula}, and inductively define the set
$rls$ by giving a finite collection of rule schemata, each denoting
an infinite set of instances, which belong to this set.
For example, the traditional rule $(\vdash\land)$ for
introducing a conjunction into the right hand side of a
sequent, as shown below, can be given by the encoding below it where we
use the string \verb|&&| to encode $\land$,
``\texttt{+}'' for multiset union, and
\verb!{#!$A$\verb!#}! to denote a singleton multiset:
$$
     \brule{$(\vdash\land)$}
           {$\Gamma \vdash A, \Delta$}
           {$\Gamma \vdash B, \Delta$}
           {$\Gamma \vdash A \land B, \Delta$}
$$

$$
     \mathtt{(\;[\; G \vdash \bra\hash A \hash\ket + D 
                   \ , \
                 G \vdash \bra\hash B \hash\ket + D \;], 
          \ \ G \vdash \bra\hash A \;\&\& \; B\hash\ket + D \;\; ) \in rls}
$$
When this clause appears in the definition of \texttt{rls}, it means
that this sequent rule is in \texttt{rls} for each possible value of A,B,G,D
of the appropriate type.
% The encoding uses HOL's notation ``\texttt{+}'' for multiset union, and
% uses \verb!{#! and \verb!#}! to encode the braces for multisets.

Having encoded the notions of formulae and sequents into HOL, we are
now in a position to encode the notion of derivability and
derivations. As we shall explain shortly, the notion of derivability
and derivations are subtly different in the following senses:
\begin{description}
\item[Derivability:] we write inductively defined predicates in HOL to
  capture the set of sequents derivable from a given, possibly empty,
  set of potential leaf sequents, using a given set of rules defined using
  the encoding of formulae and sequents described above. The base
  case will capture that every given leaf is vacuously derivable,
  and the inductive case will capture that a sequent $c$ is derivable
  if the rule set contains a rule $(ps, c)$ where each of the
  premises in $ps$ is itself derivable. We do not construct an actual
  derivation, as such, but just ensure that there exists a sequence of
  sequent rule applications which can take us from the given leaf sequents
  to the given end-sequent. We therefore use the word ``implicit'' to
  describe such derivations.
\item[Derivation (trees):] we create a new object type called
  \texttt{dertree} which will allow us to encode an explicit tree
  as a HOL term to represent an actual derivation of the given sequent
  from the given leaves using the given set of rules. We
  therefore use the word ``explicit'' to describe such derivations.
\end{description}

% \begin{figure}[t]
%   \centering
%   \begin{tabular}[c]{ll}
%    $c \in \prems \Longrightarrow c \in \derrec~\pscrel~\prems$
%    &
%    $[\ \ ] \in \dersrec~\pscrel~\prems$
%     \\[1em]
%      \AxiomC{$p_1 \cdots p_k$}
%      \LeftLabel{$\pscrel$}
%      \UnaryInfC{$c$}
%      \DisplayProof
%      &
%      \AxiomC{$\{ pms_1 , \cdots , pms_n \}$}
%      \dashedLine
%      \LeftLabel{$\dersrec~\pscrel$}
%      \UnaryInfC{$[\ p_1, \cdots , p_k \ ]$}
%      \DisplayProof
%     \\[1em]
%      \multicolumn{2}{l}{
%        $(ps, c) \in \pscrel \ ; \ ps  \in \dersrec~\pscrel~\prems
%         \Longrightarrow c \in \derrec~\pscrel~\prems$}
%     \\[1em]
%      \multicolumn{2}{c}{
%      \AxiomC{$\{ pms_1, \cdots , pms_n \}$}
%      \LeftLabel{$\derrec~\pscrel$}
%      \dashedLine
%      \UnaryInfC{$c$}
%      \DisplayProof}
%     \\[2em]
%      \AxiomC{$\{ pms_1 , \cdots , pms_n \}$}
%      \LeftLabel{$\derrec~\pscrel$}
%      \dashedLine
%      \UnaryInfC{$c$}
%      \DisplayProof
%     &
%      \AxiomC{$\{ pms_1 , \cdots , pms_n \}$}
%      \dashedLine
%      \LeftLabel{$\dersrec~\pscrel$}
%      \UnaryInfC{$[\ c_1, \cdots , c_m \ ]$}
%      \DisplayProof
%      \\[1em]
%      \multicolumn{2}{l}{
%         $c \in \derrec~\pscrel~\prems \ ; \ cs \in \dersrec~\pscrel~\prems$}
%     \\
%      \multicolumn{2}{c}{
%         $\Longrightarrow c\# cs \in \dersrec~\pscrel~\prems$}
%      \\[1em]
%      \multicolumn{2}{c}{
%      \AxiomC{$\{ pms_1 , \cdots , pms_n \}$}
%      \dashedLine
%      \LeftLabel{$\dersrec~\pscrel$}
%      \UnaryInfC{$[\ c, c_1, \cdots , c_m \ ]$}
%      \DisplayProof}
%        \end{tabular}
%   \caption{Inductively Definining Derivable Sequents}
%   \label{fig:derrec}
% \end{figure}

%\section{Our General Derivability Predicates} \label{s-dp} 

\section{Implicit and Explicit Derivations} \label{s-dp} 

In Section~\ref{s-dp-def}, we give an inductively
defined predicate \texttt{derrec} for capturing the set of all
recursively derivable sequents. 
%
In Section~\ref{s-dp-ind}, we describe the principle of induction that
is automatically generated by Isabelle/HOL from \texttt{derrec} and
describe how it can be used to prove an arbitrary property $P$ of such
sequents. 
%
In Section~\ref{s-dp-more}, we describe our other implicit derivability
predicates in less detail.
%
In Section~\ref{s-dtobj} we describe how we encoded explicit derivation
trees.
%
In Section~\ref{s-dt-imp-exp} we describe how we can move to and fro between
these two notions.  

\subsection{Defining Derivability (Implicitly) in Isabelle} \label{s-dp-def} 
We are now in a position to encode the set $\derrec$ of ``recursively
derivable sequents'' given a set \texttt{plvs} of (potential) leaf sequents
and a given set \texttt{rls} of sequent rules. 
The set \texttt{derrec rls plvs} is defined inductively as shown below
(the Isabelle code is precisely as it appears in the Isabelle theory file).
It defines simultaneously the predicates
\texttt{derrec} (that a single sequent is derivable) and  
\texttt{dersrec} (that all sequents in a list are derivable).

\begin{definition}[\texttt{derrec, dersrec}]\label{def-derrec}
\texttt{derrec rls plvs} is the set of end-sequents which are derivable from
the set \texttt{plvs} of potential leaves
using the set \texttt{rls} of sequent rules. \\
\texttt{dersrec rls plvs} is the set of lists of endsequents
which are all derivable from
potential leaves \texttt{plvs} using sequent rules \texttt{rls}:
\end{definition}
\begin{samepage}
\begin{verbatim}
consts   (* these are type declarations *)
  derrec  :: "'a psc set => 'a set => 'a set"
  dersrec :: "'a psc set => 'a set => 'a list set"

inductive "derrec rls plvs" "dersrec rls plvs"
  intrs (* the clauses defining members of these two
            mutually defined inductive sets          *)
    dpI   "eseq : plvs ==> eseq : derrec rls plvs"
   derI   "[| (ps, eseq) : rls ; ps : dersrec rls plvs |]
             ==> eseq : derrec rls plvs"
   dlNil  "[] : dersrec rls plvs"
  dlCons  "[| seq : derrec rls plvs ; 
             seqs : dersrec rls plvs |]
             ==> seq # seqs : dersrec rls plvs"
\end{verbatim}
\end{samepage}

\comment{ version using all object logic connectives
  \begin{tabular}[c]{l@{\extracolsep{1cm}}l}
  \\
    1 & $\mathtt{\derrec ~::~ (seq ~list~ * ~seq) ~set 
       ~\Rightarrow ~seq ~set
       ~\Rightarrow ~seq ~set }$
   \\
    2 & $\mathtt{?c : \;?\prems \longrightarrow \;?c :
      \;?\derrec~?\pscrel~?\prems} ~;$
   \\
    3 & $ \;\; \mathtt{(?ps, ?c) : \;?\pscrel \ \longrightarrow }$
   \\
    4 & $\mathtt{\;\;\;\; (ALL ~p . ~p : (set ~?ps)
           \longrightarrow ~p ~: ~\derrec~?\pscrel~?\prems) \;\; }$
   \\
    5 & ~~~$\mathtt{\longrightarrow ~?c ~ ~\derrec~?\pscrel~?\prems}$
  \end{tabular}

}

\comment{ version using \texttt{ALL} and \texttt{:} 
  \begin{tabular}[c]{l@{\extracolsep{1cm}}l}
  \\
    1 & $\mathtt{\derrec ~::~ (seq ~list~ * ~seq) ~set 
       ~\Rightarrow ~seq ~set
       ~\Rightarrow ~seq ~set }$
   \\
    2 & $\mathtt{?c : \;?\prems \Longrightarrow \;?c :
      \;?\derrec~?\pscrel~?\prems} ~;$
   \\
    3 & $[ \;\; \mathtt{(?ps, ?c) : \;?\pscrel \ ; }$
   \\
    4 & $\mathtt{\;\;\;\; ALL ~p . ~p : (set ~?ps)
                 \Longrightarrow ~p ~: ~\derrec~?\pscrel~?\prems \;\; ]}$
   \\
    5 & ~~~$\mathtt{\Longrightarrow ~?c ~ ~\derrec~?\pscrel~?\prems}$
  \end{tabular}
}

\comment{  version using symbols $\forall$ and $\in$
  \begin{tabular}[c]{l@{\extracolsep{1cm}}l}
  \\
  1 & $\mathtt{\derrec ~::~ (seq ~list~ * ~seq) ~set 
  ~\Rightarrow ~seq ~set
  ~\Rightarrow ~seq ~set }$
  \\
  2 & $\mathtt{?c \in \;?\prems \Longrightarrow \;?c \in
  \;?\derrec~?\pscrel~?\prems} ~;$
  \\
  3 & $[ \;\; \mathtt{(?ps, ?c) \in \;?\pscrel \ ; }$
  \\
  4 & $\mathtt{\;\;\;\; \forall ~p . ~p \in (set ~?ps)
  \Longrightarrow ~p ~\in ~\derrec~?\pscrel~?\prems \;\; ]}$
  \\
  5 & ~~~$\mathtt{\Longrightarrow ~?c ~\in ~\derrec~?\pscrel~?\prems}$
  \end{tabular}
}

\bigskip

We now explain the Isabelle code and why it achieves the meanings for
\texttt{derrec} and \texttt{dersrec} given in the definition.
These are two mutually inductively defined sets 
each of which depends on the other.
The type declarations mean that where 
\texttt{plvs} is a set of (potential) leaf sequents 
and \texttt{rls} is a set of ``rules'',
instances of (\emph{premise list, conclusion}) pairs,
then \texttt{derrec rls plvs} is a set of sequents.
A sequent is in \texttt{derrec rls plvs} 
if and only if finite repeated application
of the clauses of the definition require it to be,
and likewise \texttt{dersrec rls plvs}.
We now describe the four clauses, each of which is preceded by its name:

% The explanation is as below where a leading ``\texttt{?}''  indicates
% to Isabelle/HOL that the item is an implicitly universally quantified 
% free variable which is instantiated by pattern matching:
% outermost universal quantifier which is not shown explicitly, but
% which binds free variables such as $\mathtt{?c, ?ps}, ?\pscrel,
% ?\prems$:
\begin{description}
% \item[\rm 1] A type declaration which tells the proof-assistant that
  % $\derrec$ accepts a set of inference rules, each consisting of a
  % pair whose first component is a list of (premise) sequents and whose
  % second component is a (conclusion) sequent, and a set
  % of (initial) sequents, and produces a set of sequents;
\item[\texttt{dpI}] The base case of the inductive definition of $\derrec$
  captures that each initial sequent \texttt{eseq} from
  $\mathtt{\prems}$ is itself (vacuously) derivable from the initial
  leaf set $\mathtt{\prems}$ using the rules $\mathtt{}\rls$. The
  \verb!:! stands for set membership $\in$.
\item[\texttt{derI}] If \verb!(ps, eseq)! is the list of premises
  and the conclusion of a rule, and the premise list \texttt{ps} satisfies
  \texttt{dersrec rls plvs},
  meaning that the premises \texttt{ps} are all derivable (see below),
  then the conclusion \texttt{eseq} is derivable.
  % use \verb!;! to separate the two conjuncts and use \verb![! and
  % \verb!]! to enclose the two conjuncts into the antecedent of the
  % inductive clause (implication);
%  The second conjunct of the ``if'' part of the inductive
  % clause which captures that each premise \texttt{p} in the set
  % obtained from sequent list \texttt{?ps} is derivable from the
  % initial premises $\mathtt{?}\prems$ using the rules
  % $\mathtt{?}\rls$. Here we use a function \verb!set! to convert
  % the list \verb!?ps! into the set of its members, use $\mathtt{\in}$
  % for set membership and use an explicit $\mathtt{\forall}$ quantifier \verb!ALL!
  % to bind the variable \verb!p! (which is why it is not prefixed with
  % a \verb!?!);
  % \item[\texttt{dpI}] The ``then'' part of the inductive clause which
    % concludes that sequent \verb!?c! is derivable from
    % $\mathtt{?}\prems$ using $\mathtt{?}\rls$.
\item[\texttt{dlNil}] An empty list of sequents satisfies 
\texttt{dersrec rls plvs}
\item[\texttt{dlCons}] If \texttt{seq} satisfies \texttt{derrec rls plvs}
  and the list \texttt{seqs} satisfies \texttt{dersrec rls plvs}
  then the list \texttt{seq \# seqs} satisfies \texttt{dersrec rls plvs}.
  The symbol \texttt{\#} denotes appending an item \texttt{seq}
  to the front of a list \texttt{seqs} to form a longer list.
\end{description}

Note that the clauses \texttt{dlNil} and \texttt{dlCons} give us that
a list is in \texttt{dersrec rls plvs} if all its members are
in \texttt{derrec rls plvs}; 
and since these clauses give \emph{all} members of 
\texttt{dersrec rls plvs}, this ``if'' is in fact ``if and only if''.

In fact the actual Isabelle/HOL code is more general, in that the
things being derived are of a parametric type \texttt{'a} and
need not be sequents, but could be formulae or other constructs,
and a ``rule'' merely consists of a list of ``premises'' and a ``conclusion''.
We describe it in terms of sequents, here, merely to place
it in the context of our cut-admissibility proofs.

\subsection{Inductive Proofs via Automated Inductive Principles}
\label{s-dp-ind}

We use inductive definitions because correct induction principles are
generated automatically by Isabelle from the inductive definition of
$\derrec$. A heavily simplified version of the induction principle 
automatically generated for proving an arbitrary property $\mathtt{P}$
by the definition of the inductive set \derrec\ is shown below
using meta-level intuitionistic connectives (\verb!==>!, \verb|!!|,
\verb!;!) and
object-level classical HOL connectives (\verb!ALL!, \verb!-->!, \verb!:!)

\bigskip

\comment{ version with object logic connectives}
\noindent
\begin{tabular}[l]{@{}l@{\extracolsep{0.3cm}}l}
1 &  $!!\ x. !!\ P.$
 \\
2 &  \verb![|! $\mathtt{x~ : ~\derrec ~\pscrel ~\prems ~ ;}$ 
 \\
3 & $\mathtt{\;\;\; (ALL\ c.\ c : ~\prems \longrightarrow ~P(c)) ~ ;}$ 
\\
4 & $\mathtt{\;\;\; (ALL\ c.\ ALL\ ps.\ (ps, c) : \pscrel \longrightarrow
               ~(ALL\ y : (set ~ps). ~P(y))~ \longrightarrow ~P(c))}$ 
\\
5 & \verb!|]! \verb!==>! $ \mathtt{~P(x)}$
\end{tabular}

\comment{ version with $\forall$, $\in$, $\Longrightarrow$
\begin{tabular}[c]{l@{\extracolsep{1cm}}l}
1 &  $\mathtt{\forall x. \forall P.}$
 \\
2 & $[ \mathtt{\;\;\; x~ \in ~\derrec ~\pscrel ~\prems ~;}$
 \\
3 & $\mathtt{\;\;\; \forall c . c \in ~\prems \Longrightarrow ~P(c) ~;}$ 
\\
4 & $\mathtt{\;\;\; \forall c . \forall ps.
  [\;\; (ps, c) \in ~\pscrel \;\; ; 
               ~\forall y \in (set ~ps). ~P(y)~]
          \Longrightarrow ~P(c)}$
\\
5 & $] \;\;\; \mathtt{ \Longrightarrow ~P(x)}$
\end{tabular}
}
\bigskip
An explanation is:
\begin{description}
\item[\rm 1] for all sequents $x$ and all properties $P$
\item[\rm 2 ] if $x$ is derivable from (potential) leaves $\prems$ using rules
  $\pscrel$, and
\item[\rm 3 ] $P$ holds for every sequent $c$ in $\prems$, and
\item[\rm 4 ] for each rule $(ps, c)$, $P$ of each premise in $ps$
  implies $P$ of its conclusion $c$,
\item[\rm 5 ] then $P$ holds of $x$
\end{description}

We can visualise this induction principle as below where we replace
the meta-level \verb!==>! by a horizontal line and replace the
meta-level \verb!;! with juxtaposition of premises and replace
\verb!:! by set membership $\in$:
$$
\frac {x \in derrec\ rls\ plvs \quad
   \forall c \in plvs. P\ c \quad 
   \forall (ps, c) \in rls. (\forall p\ in\ ps. P\ p) \Rightarrow P\ c}
   {P\ x}
$$

This is an induction principle
which we use often in proof-theory: prove that some property holds of
the leaves of a derivation, and prove that the property is preserved
from the premises to the conclusion of each rule. For example,
consider the standard translation from sequents of LK to formulae
given by $\tau(A_1, \cdots , A_n \vdash B_1, \cdots , B_m) = A_1 \land
\cdots \land A_n \limp B_1 \lor \cdots \lor B_m$. We typically use
this translation to argue that all derivable sequents are valid in the
semantics of first-order logic. The proof proceeds by showing that the
translation of the leaves of a derivation are all valid, and showing
that if the translations of the premises are valid then the
translations of the conclusion are valid, for every rule.
Note that no explicit derivation is created by this induction
principle since it uses derivability (implicit derivations).

Thus this induction principle is really a lemma, but our formal
encoding of it requires one more definition.

\begin{definition}
  For all sets \verb!A! and all unary predicates \verb!P!, the
  property {\rm\texttt{Ball A P}} holds iff every member \verb!x! of \verb!A!
  satisfies \verb!P!:
\begin{verbatim}
Ball_def: "Ball A P == ALL x. x : A --> P x"
\end{verbatim}
\end{definition}
The following is the formal inductive principle described informally
above which is generated by Isabelle/HOL, automatically, using
``\texttt{?}'' to show arguments that are implicitly universally quantified.

\begin{lemma}[derrec-induction]\label{l-der-ind}
  For every sequent \verb!x!, 
  every rule set \verb!rls!,
  every list of leaves \verb!plvs!,
  and every property \verb!P!, if
    \begin{enumerate}
  \item \verb!x! is derivable from potential leaves
  \verb!plvs! using the rules in \verb!rls!, and
  \item every sequent \verb!c! in \verb!plvs! obeys \verb!P!,  and
  \item for every sequent \verb!c! and premise list \verb!ps! 
        if \verb!(ps, c)! is a rule in \verb!rls!,
   and each premise in \verb!ps! is derivable from potential leaves
  \verb!plvs! using rules in \verb!rls! and 
  every premise from \verb!ps! obeys \verb!P! then \verb!c! obeys
  \verb!P!
    \end{enumerate}
  then \verb!x! obeys \verb!P!:
\end{lemma}

\begin{verbatim}
standard drs.inductr: 
 "[| ?x : derrec ?rls ?plvs ; 
     !!c. c : ?plvs ==> ?P c ;
     !!c ps. [| (ps, c) : ?rls ; 
                ps : dersrec ?rls ?plvs ;
                Ball (set ps) ?P |] ==> ?P c
  |] ==> ?P ?x"
\end{verbatim}

\begin{proof}
Isabelle automatically generates an induction principle (not shown)
from the definition of \texttt{derrec}.  
Since the definition also involves defining \texttt{dersrec} (which expresses
that a list of items are all derivable), the automatically generated principle
involves a property $P_1$ of derivable sequents and a property $P_2$ of lists
of derivable sequents. 
Naturally we choose property $P_2$ of a list to be that all members of the
list satisfy $P_1$.  That instantiation gives us the lemma.
\end{proof}

\comment{
The induction theorem generated by Isabelle is shown below.
\begin{verbatim}
drs.induct ;
   "[| !!concl. concl : ?plvs ==> ?P1.0 concl;
         !!concl ps.
            [| (ps, concl) : ?rls; ps : dersrec ?rls ?plvs; ?P2.0 ps |]
            ==> ?P1.0 concl;
         ?P2.0 [];
         !!seq seqs.
            [| seq : derrec ?rls ?plvs; ?P1.0 seq;
               seqs : dersrec ?rls ?plvs; ?P2.0 seqs |]
            ==> ?P2.0 (seq # seqs) |]
      ==> 
      (?xb : derrec ?rls ?plvs --> ?P1.0 ?xb) &
      (?xa : dersrec ?rls ?plvs --> ?P2.0 ?xa)" : Thm.thm
\end{verbatim}
}

Intuitively, Isabelle converts object-level classical implications
$(\longrightarrow)$ into meta-level intuitionistic implications
(\verb!==>!), allowing us to use the lemma itself for sub-goaling.
% $$
% \frac {?x \in derrec\ ?rls\ ?plvs \quad
%    \forall c \in~ ?plvs.\; ?P\ c \quad 
%    \frac{\forall (ps, c) \in ?rls. (\forall p\ in\ ps. ?P\ p)}{?P\ c}}
%    {?P\ ?x}
% $$

Using these inductive principles we proved the following lemma about
derivability using Isabelle, where the question marks indicate
free-variables which are implicitly universally quantified:
\begin{lemma}\label{l-derrec-trans}
  If each premise in \texttt{ps} is derivable from leaves $\prems$ using
  rules $\pscrel$,
  and \texttt{eseq} is derivable from \texttt{ps} using $\pscrel$,
  then \texttt{eseq} is derivable from $\prems$ using $\pscrel$:
 \begin{multline} \notag
   [| \mathtt{?ps \subseteq derrec~?\pscrel~?\prems
       \ ; \
       ?eseq \in derrec~?\pscrel~?ps} |]
   \\
      \Longrightarrow  \mathtt{
       ?eseq \in derrec~?\pscrel~?\prems
   }
 \end{multline}
% Isabelle derrec_trans;

\noindent
\end{lemma}

\subsection{Further Implicit Derivability Predicates}
% \marginpar{Do we ever use these in the code that we show in this paper ? NO}
\label{s-dp-more} 
% SOME OF THIS IS COVERED IN \S5
We briefly describe the remaining functions we used to describe
derivability.  % A fuller account is given in \cite{gore-india}.
% MENTIONED AT END OF \S\ref{s-dp-def}
% This framework is general in that a rule merely consists of ``premises''
% and a ``conclusion'', and is independent of whether the things derived
% are formulae, sequents, or other constructs, but we will refer to them
% as sequents.

\begin{definition}[derivable rule]\label{d-der-rule}
For a list of sequents \texttt{lvs} and a sequent \texttt{eseq},
\texttt{(lvs, eseq)} is a \emph{derivable} rule with respect to the rule set
\texttt{rls} if we can construct an implicit derivation using rules in 
\texttt{rls} whose leaves are \emph{exactly} the sequents \texttt{lvs} 
(in the same order), and whose endsequent is \texttt{eseq}.
\end{definition}

We formalise this notion using functions \texttt{derl} (for the derivable
rules) and \texttt{dersl} (an auxiliary function).

\begin{definition}[\texttt{derl, dersl}]\label{d-derl}
For a list of sequents \texttt{lvs} and a sequent \texttt{eseq},
the pair \texttt{(lvs, eseq)} is in \texttt{derl rls}
if it is a derivable rule with respect to \texttt{rls}.
% if rules of \texttt{rls} can be combined to form 
% a derivation of \texttt{eseq} from (exactly) the list of sequents
% \texttt{lvs} (in that order).

For lists of sequents \texttt{lvs} and \texttt{eseqs}, 
the pair \texttt{(lvs, eseqs)} is in \texttt{dersl rls}
if there is a sequence of rule instances from \texttt{rls}
which take us from (exactly) the list of leaf sequents \texttt{lvs}
to the list of endsequents \texttt{eseqs}.
% if rules of \texttt{rls} can be combined to form 
% a number of derivation, placed side-by-side,
% deriving \texttt{cs} from (exactly) the list of sequents \texttt{lvs}.
We envisage a number of implicit derivations drawn side-by-side,
whose endsequents are the members of the list \texttt{eseqs}. 
% although, in contrast to \S\ref{s-dtobj}, we are not explicitly representing
% the trees in Isabelle. 
\end{definition}

\begin{verbatim}
types 'a psc = "'a list * 'a"      (* single step inference *)
consts (* these are type definitions *)
  derl      :: "'a psc set => 'a psc set"
  dersl     :: "'a psc set => ('a list * 'a list) set"

inductive "derl rls" "dersl rls"
intrs
asmI "([eseq], eseq) : derl rls"
dtderI "[| (lvs, eseq) : rls ; (lvss, lvs) : dersl rls |] 
                    ==> (lvss, eseq) : derl rls"
dtNil "([], []) : dersl rls"
dtCons "[| (lvs, eseq) : derl rls ; (lvss, eseqs) : dersl rls|]
                    ==> (lvs @ lvss, eseq # eseqs) : dersl rls"
\end{verbatim}

This formalises the notion of a derivable rule:
\texttt{derl rls} is the set of derivable rules with respect to \texttt{rls}.

  % derl, dercl, adm :: "'a psc set => 'a psc set"
  % dercsl    :: "'a psc set => ('a list list * 'a list) set"
  % derrec    :: "'a psc set => 'a set => 'a set"
  % dersrec   :: "'a psc set => 'a set => 'a list set"
\comment{
These are defined as inductively defined sets,
using the clauses below, explained as follows:
\begin{description}
\item[\texttt{asmI}] 
A single sequent \texttt{eseq} forms a derivation tree, 
deriving endsequent \texttt{eseq} from leaf list \texttt{[eseq]}. 

\item[\texttt{dtderI}] 
If we have derivation trees deriving \texttt{lvs} from \texttt{lvss},
and \texttt{(lvs, eseq)} is a rule in \texttt{rls}, then
we can join them to form a derivation tree deriving \texttt{eseq} from
\texttt{lvss}.

\item[\texttt{dtNil}] 
An empty list of derivation trees derives an empty list of endsequents from
an empty list of leaves.

\item[\texttt{dtCons}] 
If a derivation tree derives \texttt{eseq} from \texttt{lvs}
and a list of trees derives \texttt{eseqs} from \texttt{lvss},
then there is a list of trees deriving 
\texttt{eseq \# eseqs} from \texttt{lvs @ lvss}.
(Recall that \texttt{\#} ``conses'' an item to the front of a list,
and \texttt{@} denotes concatenation of lists).
\end{description}
}

Where an inference rule \texttt{'a psc} is a list of premises \texttt{ps}
and a conclusion \texttt{c}, a ``derived rule'' is of the same type.
We define \texttt{derl rls} to be the set of
rules derivable from the rule set \texttt{rls}.
% and \texttt{derrec rls plvs} is the set of sequents 
% derivable using rules \texttt{rls} from the set \texttt{plvs} of premises.
This, like \texttt{derrec}, was defined as an inductive set.
So $\mathtt{(lvs, eseq) \in \derl\ \rls}$ %, 
% equivalently, $\mathtt{(lvs, eseq) \in \dercl\ \rls}$,
reflects the shape of an implicit derivation tree:
\texttt{lvs} is a list of exactly the leaves used, in the correct order,
whereas $\mathtt{eseq \in \derrec\ \rls\ plvs}$ holds
even if the set of (potential) leaves \texttt{plvs} contains extra sequents.

We note that the definition means that $([c], c) \in$ \texttt{derl rls}:
that is, the ``trivial" derived rules are included.
To define \texttt{derl rls} to exclude the ``trivial" derived rules
would complicate results such as Theorem~\ref{t-der-derl}.  

The formal Isabelle definitions of \texttt{derl}
used also the function \texttt{dersl}, 
which represents several implicit derivation trees side-by-side: \\
$\mathtt{(lvss, eseqs) \in dersl~rls}$ when the list \texttt{lvss} is the
concatenation of their lists of leaves, and \texttt{eseqs} is the list
of their endsequents.

% , \texttt{dercl} and \texttt{derrec} used also the functions
% \texttt{dersl}, \texttt{dercsl} and \texttt{dersrec} respectively.
% The auxiliary function \texttt{dersrec} represents several sequents,
% all derivable from the premises. 
%  The function \texttt{dercsl} is similar, but it
% shows which premises are part of which tree.
% That is, $\mathtt{(pss, cs) \in \texttt{dercsl}\ rls}$ 
% implies $\mathtt{(concat\ pss, cs) \in \texttt{dersl}\ rls}$.  
% We showed that \texttt{derl} and \texttt{dercl}
% (defined using auxiliary functions 
% \texttt{dersl} and \texttt{dercsl} respectively) are equivalent.

\comment{
Here are the inductions principles for \texttt{derrec} and \texttt{derl} 
in Isabelle: these are obtained from the automatically generated principles
by replacing the auxiliary functions \texttt{dersrec} (etc) by their meanings.

\begin{verbatim}
drs.inductr': "[| ?xb : derrec ?rls ?plvs;
   !!concl. concl : ?plvs ==> ?P1.2 concl;
   !!concl ps. [| (ps, concl) : ?rls;
         ALL t:set ps. t : derrec ?rls ?plvs;
         Ball (set ps) ?P1.2 |] ==> ?P1.2 concl |] ==> ?P1.2 ?xb"

drc.inductr': "[| (?xd, ?xc) : derl ?rls; !!c. ?P1.2 [c] c;
   !!concl ps pss.  [| (ps, concl) : ?rls;
         (pss, ps) : allrel (derl ?rls);
         (pss, ps) : allrel {(x', y'). ?P1.2 x' y'} |] ==>
     ?P1.2 (concat pss) concl |] ==> ?P1.2 ?xd ?xc" 
\end{verbatim}
end comment }

\comment{
POSSIBLY MOVE 
We may .contrast use of the ``structural'' induction principle
for \texttt{derrec} with induction on the height of a derivation tree.  
Using induction on the height, it is possible, and in some proofs necessary, 
to transform a sub-tree in some height-preserving (or height-reducing) way, and
use the assumption that the transformed tree has property $P$. 
That approach is not available when using the induction principle 
from Lemma~\ref{l-der-ind}, and was not needed for our earlier proofs.

POSSIBLY MOVE EARLIER 
Where we have a property of two derivations, such as cut-admissibility,
as shown in the diagram,
we need a more complex induction principle, which we derived
(limited to the case where the set \textit{plvs} of ultimate leaves is
empty) :
\begin{center}
\begin{prooftree}
\AxiomC{$\MQ_{l1} \ldots \MQ_{ln}$}
\RightLabel{$\rho_l$}
\UnaryInfC{$\MR_{l}$} 
\AxiomC{$\MQ_{r1} \ldots \MQ_{rm}$}
\RightLabel{$\rho_r$}
\UnaryInfC{$\MR_{r}$}
% \RightLabel{(\textit{cut ?})}
\dashedLine
\BinaryInfC{$\MS$}
\end{prooftree}
\end{center}

In proving $P\ \MR_l\ \MR_r$, we make the inductive assumptions that 
$P\ \MQ_{li}\ \MR_r$ and $P\ \MR_l\ \MQ_{rj}$ 
for each $i \leq n$ and $j \leq m$.

$$
 \begin{array}{c} 
  cl \in derrec\ rlsl\ \{\} \quad cr \in derrec\ rlsr\ \{\}  \\
      \forall (lps, lc) \in rlsl, (rps, rc) \in rlsr.\
       (\forall lp\ in\ lps. P\ lp\ rc) \land (\forall rp\ in\ rps. P\ lc\ rp) 
           \Rightarrow P\ lc\ rc \\
\hline { P\ cl\ cr} 
\end{array}
$$

We omit details because we shall give details of a generalisation of this
induction principle in Section~\ref{s-cagen}.
}

\begin{theorem} \label{t-der-derl}
With respect to some given set of rules \verb!rls:!
  \begin{enumerate}
  \item the items derivable from a set \texttt{plvs} of leaves are the
  items derivable from the set of sequents derivable from \texttt{plvs}:
\begin{verbatim}
derrec_trans_eq :
  "derrec ?rls ?plvs = derrec ?rls (derrec ?rls ?plvs)"
\end{verbatim}
  \item derivability (whether defined using \texttt{derrec} or \texttt{derl})
  using the set of derived rules is equivalent to
  derivability using the original set of rules:
\begin{verbatim}
derrec_derl_deriv_eq :
  "derrec (derl ?rls) ?plvs = derrec ?rls ?plvs"
derl_deriv_eq : "derl (derl ?rls) = derl ?rls" 
\end{verbatim}
  \end{enumerate}
\end{theorem}


Finally, we can define the notion of an admissible rule.
\begin{definition}[admissible, \texttt{adm}]\label{d-adm}
A rule \texttt{(ps, c)} is \emph{admissible} with respect to a rule set 
\texttt{rls} if, assuming its premises (leaves) \texttt{ps} are derivable 
from the empty set $\{\}$ of leaves using rules from \texttt{rls},
then so is its conclusion (endsequent) \texttt{c}:
\end{definition}
\begin{verbatim}
consts  (* this is a type declaration *)
  adm :: "'a psc set => 'a psc set"

inductive "adm rls"
  intrs   (* inductive defn of the set of admissible rules *)
    I  "(ps : dersrec rls {} --> c : derrec rls {}) 
        ==> (ps, c) : adm rls"
\end{verbatim}

Using Definition~\ref{d-adm} we obtained the following four results,
which were surprisingly tricky since \adm\ is not monotonic
in its argument \texttt{rls}, where \verb!<=! encodes $\subseteq$.

\begin{theorem}
With respect to some given set of rules \verb!rls:!
  \begin{enumerate}
  \item every derivable rule is admissible;
  \item the admissible rules are closed under admissibility;
  \item the admissible rules are closed under admissibility after derivability;
  \item the admissible rules are closed under derivability. 
  \end{enumerate}
\begin{verbatim}
 "derl ?rls <= adm ?rls"          "adm (adm ?rls) = adm ?rls"
 "adm (derl ?rls) = adm ?rls"     "derl (adm ?rls) = adm ?rls"
\end{verbatim}
\end{theorem}

\subsection{Explicit Derivation Trees: a deep embedding of derivations}
\label{s-dtobj}

The main advantage of the method outlined in the previous section was
that there was no concrete representation of a derivation. That is, we
relied on the proof-assistant to perform pattern-matching and rule
instantiations in an appropriate way, so that all we needed was to
capture the idea that derivations began with leaves and
ended with a single end-sequent.

When we reason about cut-elimination, often we are required to
perform transformations on explicit derivations. We therefore need a
representation of such trees inside our encoding.
%
In previous work~\cite{dawson-gore-generalised},
we described such an encoding using the following datatype:

\begin{verbatim}
   datatype seq dertree = Der seq (seq dertree list)
                        | Unf seq
\end{verbatim}

The declaration states that a derivation tree can either be an
\verb!Unf!inished (unproved)
leaf sequent built using the constructor \verb!Unf!,
or it can be a pair \verb!(seq, dts)! consisting of a conclusion
sequent \verb!seq!
and a list \verb!dts! of
(sub-)derivation trees bound together using the constructor \verb!Der!.

\begin{definition}
Given an object \texttt{dt} of type \texttt{dertree},
\texttt{conclDT dt} returns the first argument of the constructors
\verb!Der! and \verb!Unf! as the conclusion (endsequent) of \verb!dt!.

For a tree \texttt{dt} which is not an \verb!Unf!inished leaf,
\texttt{nextUp dt} returns the list of trees whose conclusions are the premises
of the last rule of \texttt{dt}, and
\texttt{botRule dt} returns the bottom rule (premise
list and conclusion) of \texttt{dt}.
\end{definition}
\begin{verbatim}
primrec
  conclDT_Der: "conclDT (Der seq dts) = seq"
  conclDT_Unf: "conclDT (Unf seq) = seq" 

  nextUp_Der: "nextUp (Der seq dts) = dts"
  botRule_Der: "botRule (Der seq dts) = (map conclDT dts, seq)"
\end{verbatim}

Here, \texttt{map conclDT dts} applies \texttt{conclDT}
to each member of the list \texttt{dts} of derivation trees and hence
returns the premises of the bottom rule.

% In that work, we also described how we maintained substitutions as lists of
% \marginpar{this para could be confusing, and doesn't have any bearing on the
% rest}
% pairs of the form $(x, t)$ representing the substitution $x := t$. We
% also described how we manipulated substitutions and instantiation
% directly to obtain rule instances.
% We required such low-level aspects to be made explicit so that we
% could reason about display logic which required us to check conditions
% on rules such as ``a rule is closed under substitution of arbitrary
% structures for variables''.

Our use of \verb!dertee! can be seen as an even deeper embedding of
proof-theory into Isabelle/HOL since it utilises the proof-assistant
to describe an explicit derivation rather than the implicit existence
of such a derivation as encoded by our derivability predicates from the
previous section.

\subsection{To and fro between explicit and implicit derivations}
\label{s-dt-imp-exp}

Omitting details now, suppose we define \verb!valid rls dt! to hold
when derivation tree \verb!dt! correctly uses rules from \verb!rls! only and
has no \verb!Unf!inished leaves: that is,
the leaves of \texttt{dt} are all instances of the conclusions of rules which
have no premises (ie, such as $\Gamma, A \vdash A, \Delta$).
We linked our two approaches for specifying the derivable sequents by proving:

\begin{lemma}
If derivation tree \verb!dt! is valid w.r.t. the rules $\pscrel$ then its
endsequent is (implicitly) derivable from the empty set of leaves
using $\pscrel$:
\end{lemma}

\begin{verbatim}
valid_derrec: 
      "valid ?rls ?dt ==> conclDT ?dt : derrec ?rls {}" 
\end{verbatim}

\begin{lemma}
If the end-sequent \verb!eseq! is (implicitly) derivable
from the empty set $\{\}$ of leaves using rules $\pscrel$
then there exists an explicit derivation tree \verb!dt! which is
valid w.r.t. $\pscrel$, whose end-sequent is \verb!eseq!:
\end{lemma}
\begin{verbatim}
derrec_valid: 
       "?eseq : derrec ?rls {} 
        ==>  EX dt. valid ?rls dt & conclDT dt = ?eseq"
\end{verbatim}

Thus we now know that the implicit derivations captured by our
derivability predicate $\derrec$ can be faithfully captured using the
deeper embedding using explicit \verb!dertree! derivation trees. Indeed, the
lemmas allow us to move freely between the two embeddings at will to
omit or include details as required \cite{dawson-gore-generalised}.

\section{Subformula Relation, Rule Skeletons and Extensions with Contexts}
\label{s-gls}

Our generalised definition of formulae allows a single definition of
the immediate (proper) subformula relation, \texttt{ipsubfml}, which
will not need to be changed when new connectives are added.

\begin{definition}
  If a formula \verb!P! is in the set obtained from the list of
  formulae \verb!Ps! then \verb!P! is a proper subformula of
  any larger formula \verb!FC conn Ps! created using a
  formula-connective \verb!conn! and \verb!Ps!:
\begin{verbatim}
consts  (* this is a type-declaration for function ipsubfml  *)
    ipsubfml :: "(formula * formula) set"
inductive "ipsubfml" (* proper immediate subformula relation *)
    intrs  
    ipsI "P : set Ps ==> (P, FC conn Ps) : ipsubfml"
\end{verbatim}
\end{definition}

For example, \texttt{(f, Box f) : ipsubfml} because \texttt{Box f} is the
abbreviation \texttt{Box f == FC ``Box`` [f]} where \verb!conn! is
the string \verb!``Box``! and \verb!Ps! is the formula-list \verb![f]!.

In \S\ref{s-eol} we showed that the traditional $\land R$ rule from LK
could be encoded as below using a sequent consisting of a pair
$(\Gamma,\Delta)$ of multisets of formulae, written $\Gamma \vdash
\Delta$, where multiset braces are written as \verb!{#! and \verb!#}!
and multiset union is written as \texttt{+}:
$$
     \mathtt{(\;[\; G \vdash \bra\hash A \hash\ket + D 
                   \ , \
                   G \vdash \bra\hash B \hash\ket + D \;], 
            \ \ G \vdash \bra\hash A \;\&\& \; B\hash\ket + D \;\; ) \in \pscrel}
$$
The essence of the rule is more succinctly described by the rule
skeleton $\MR_s$ shown below left. We now describe how we can 
uniformly extend $\MR_s$ with the context $X \vdash Y$ to obtain the
extended rule $\MR_e$ shown below at right:
% \begin{verbatim}
% datatype 'a sequent = 
 % Sequent "'a multiset" "'a multiset"    ("((_)/ |- (_))" [6,6] 5)
% \end{verbatim}
%Given a rule such as $(\vdash \land)$ in the form on the left,
$$
\MR_s = \frac{\vdash A \quad \vdash B} {\vdash A \land B}
\qquad\qquad\qquad
\MR_e = \frac{X \vdash Y, A \quad X \vdash Y, B} {X \vdash Y, A \land B}
$$

\begin{definition}
If the sequent \verb!seqXY!  is the pair \verb!(X, Y)!,
representing the sequent $X \vdash Y$, and
the sequent \verb!seqUV! is the pair \verb!(U, V)!,
representing the sequent $U \vdash V$,  then
\verb!extend seqUV seqXY! is the sequent 
\verb!(X+U, Y+V)!, representing the sequent
$X, U \vdash Y, V$ since
\verb!seqXY + seqUV! is
\verb!(X+U, Y+V)!
by the pointwise extension of \verb!+!  to 
pairs of multisets and the function \texttt{pscmap} allows us to modify
a rule \texttt{(ps, c)} by applying an arbitrary function \texttt{f} to each of
its components:
\end{definition}

\begin{verbatim}
consts   (* this is a type declaration *)
  extend :: "'a sequent => 'a sequent => 'a sequent"
  extrs  :: "'a sequent psc set => 'a sequent psc set"

defs
  extend_def : "extend seqXY seqUV ==  seqXY + seqUV"
  pscmap_def : "pscmap f (ps, c) = (map f ps, f c)" 
\end{verbatim}

We can now take a set \texttt{rules} of rule skeletons and produce their
uniform extension with arbitrary context \texttt{flr} 
(for ``formulae left and right'') representing $X \vdash Y$.

\begin{definition}[\texttt{extrs}]
Given a rule set \texttt{rules}, the inductively defined set
\texttt{extrs rules} is the set of rules
consisting of all uniform extensions of all rules in \texttt{rules}:
\end{definition}

\begin{verbatim}
inductive "extrs rules"
  intrs
    I "psc : rules ==> pscmap (extend flr) psc = epsc 
       ==> epsc : extrs rules"
\end{verbatim}

For example, we can now use  functions \texttt{extend} and
\texttt{pscmap}
so that 
\begin{gather*}
\texttt{extend}\ (X \vdash Y)\ (U \vdash V) = (X + U) \vdash (Y + V) \\
\MR_e = \texttt{pscmap}\ (\texttt{extend}\ (X \vdash Y))\ \MR_s
\end{gather*}
Thus \texttt{pscmap} uniformly extends the skeleton provided by
$\MR_s$ with arbitrary contexts $X$ and $Y$ on respective sides to
encode $\MR_e$ using multiset addition $+$.
So \texttt{extrs} $S$ means the set of all such extensions 
of all rules in the set $S$.

Then we define \texttt{lksss}, the set of rules for Gentzen's LK;
we show just a selection. 
The rules below are the (skeletons of some of the) traditional invertible
logical introduction rules from LK (without any context):
$$
~
\frac{\vdash A \quad \vdash B}{\vdash A \land B }
\quad ~
\frac{\vdash A, B}{\vdash A \lor B }
\quad ~
\frac{B \vdash \quad \vdash A}{A \to B \vdash}
\quad ~
\frac{A, B \vdash}{A \land B \vdash}
\quad ~
\frac{A \vdash \quad B \vdash}{A \lor B \vdash}
\quad ~
\frac{A \vdash B}{\vdash A \to B }
~
$$
Using \verb!&&! for $\land$, \verb!v! for $\lor$ and \verb!--! for $\lnot$,
we can encode the logical introduction rules 
as shown below, to obtain the set \verb!lksir! of LK
right introduction rule skeletons, where
\verb!{#}!
rather than \verb!{##}! is the empty-multiset:

\begin{definition}[\texttt{lksir}]
\texttt{lksir} is the set of right logical introduction rules, 
in the form without any context and using the form which is invertible, as
shown above.
\end{definition}

\begin{verbatim}
inductive "lksir" (* LK right introduction rule skeletons *)
 intrs
  andr 
   "([{#} |- {#A#}, {#} |- {#B#}], {#} |- {#A && B#}) : lksir"
  orr   "([{#} |- {#A#} + {#B#}], {#} |- {#A v B#})   : lksir"
  negr  "([{#A#} |- {#}], {#} |- {#--A#})             : lksir"
  impr  "([{#A#} |- {#B#}], {#} |- {#A -> B#})        : lksir"
\end{verbatim}

Similar rules \texttt{lksil} (not shown) give the skeletons of the
traditional invertible rules for left-introduction. By adding the
initial sequent ``axiom'' $A \vdash A$ with an empty list \verb![]! of premises
below we obtain the set of ``unextended'' rules \texttt{lksne} for LK:

\begin{definition}[\texttt{lksne}]
\texttt{lksne} is the set of rules, not extended by any arbitrary context,
without structural rules, for LK.
\end{definition}

\begin{verbatim}
inductive "lksne" (* LK rule skeletons before being extended *)
  intrs
    axiom  "([], {#A#} |- {#A#})        : lksne"
    ilI    "(ps, c) : lksil ==> (ps, c) : lksne"
    irI    "(ps, c) : lksir ==> (ps, c) : lksne"
\end{verbatim}

We can now form the full extended set \texttt{lksss} of rules for LK,
by extending each rule skeleton \verb!psc! from \verb!lksne! by an
arbitrary pair $(X, Y)$ of contexts \texttt{flr} (for \verb!f!ormulae
\verb!l!eft and \verb!r!ight) regarded as a sequent $X \vdash Y$:
\begin{definition}[\texttt{lksss}]
\texttt{lksss} is the set of rules, extended by arbitrary contexts,
without structural rules, for LK.
\end{definition}

\begin{verbatim}
inductive "lksss"
  intrs
    extI "psc : lksne ==> pscmap (extend flr) psc : lksss"
\end{verbatim}

Now, we can encode the skeleton shown below right of the traditional
K-rule shown below left:
\[
\AxiomC{$\Gamma \vdash A$}
\RightLabel{$(K)$}
\UnaryInfC{$\Sigma, \wbx\Gamma \vdash \wbx A, \Delta$}
\DisplayProof
\qquad\qquad\qquad
\AxiomC{$ \Gamma \vdash A$}
\RightLabel{$(SK)$}
\UnaryInfC{$\wbx\Gamma \vdash \wbx A$}
\DisplayProof
\]

\begin{definition}[\texttt{SK}]
\texttt{SK} is the set of instances of the skeleton of the
K rule of modal logic 
\end{definition}

\begin{verbatim}
inductive "SK"
  intrs 
      I "([X |- {#A#}], mset_map Box X |- {#Box A#}) : SK"
\end{verbatim}

Note that $X$ is a multiset, and $\Box X$ is informal notation for applying 
$\Box$ to each member of $X$; this is implemented using \texttt{mset\_map},
used in the encoded \texttt{SK} rule.
Using a similar notation we write $\Box B^k$ for $(\Box B)^k$,
the multiset containing $n$ copies of $\Box B$.
Development of \texttt{mset\_map} and relevant lemmas is in the source files
\texttt{Multiset\_no\_le.\{thy,ML\}}.

By extending the skeletons of the LK rules and 
extending only the conclusion of the skeleton $(SK)$ of the 
$K$ rule above, we could obtain an encoding of the
traditional sequent calculus for the modal logic K:
% \marginpar{We don't actually do this - the closest is Jesse's
% definition of \texttt{gs4\_rls}}

\begin{verbatim}
inductive "lksK"
  intrs
    extI "psc : lksne ==> pscmap (extend flr) psc : lksK"
       K "(ps, c) : SK ==> (ps, extend flr c)     : lksK"
\end{verbatim}

Since we actually handle more complex logics, but not K as such,
we have not made this a formal definition.

Note that most of these definitions use the Isabelle feature for
inductively defined sets, even though many of them are not actually
inductive (ie, recursive).
We do this because Isabelle automatically generates useful theorems for them,
including
rules which help us prove or use an expression such as \texttt{rl : lksne}.

\section{The Weakening, Inversion and Contraction Properties} \label{s-wic}

We now encode the weakening, inversion and contraction as 
properties.
% describe how we encoded the statements of the main lemmas
% regarding the admissibility of weakening, contraction and cut, along
% with the encoding of the invertibility lemmas required for contraction
% admissibility. 

% \subsection{Weakening}\label{s-wk}

\begin{definition} \label{d-wk-adm}
A set  \texttt{rls} of rules satisfies the weakening admissibility property if,
whenever a sequent $X \vdash Y$ is derivable, any larger sequent
$(X \vdash Y) + (U \vdash V) = (X, U \vdash Y, V)$ is derivable:

\begin{verbatim}
consts (* type for function wk_adm using type variable 'a *)
   wk_adm    :: "'a sequent psc set => bool"

wk_adm_def : "wk_adm rls ==
     ALL XY. XY : derrec rls {} -->
                  (ALL UV. XY + UV : derrec rls {})"
\end{verbatim}
\end{definition}

Here, the variable \texttt{rls} is forced to be a set of sequent rules
by the type of \texttt{wk\_adm}, and thence
the variables \texttt{XY} and \texttt{UV} will be forced to be
of type \texttt{sequent} by the typing restrictions on the inputs to
\texttt{derrec}.

\begin{definition}[\texttt{inv\_rl}]\label{def-inv-rl}
  A rule \verb|(ps, c)| is \emph{invertible} with respect to a set
  \verb|rls| of rules if, whenever \verb|c| is derivable using
  \verb!rls!, so is every member of \verb|ps|:
\begin{verbatim}
inv_rl.simps: 
  "inv_rl rls (ps, c) =
          (c : derrec rls {} --> ps : dersrec rls {})"
\end{verbatim}
\end{definition}

  Here, the definition of \verb|dersrec| hides a universal
  quantifier over the members of the list \verb|ps|: see 
  Definition~\ref{def-derrec}.

% \subsection{Contraction}\label{s-ctr}
To encode contraction, we utilise an axiomatic type class for
sequents, described in more detail elsewhere~\cite{dawson-gore-generalised}.
Thus we can write 
$(A \vdash 0) + (A \vdash 0) \leq (X \vdash Y)$ to mean that
the multiset $X$ contains at least two copies of $A$
and write $(X \vdash Y) - (A \vdash 0)$ 
for the sequent obtained by deleting one of these copies from $X$.
Similarly we can write 
$(0 \vdash A) + (0 \vdash A) \leq (X \vdash Y)$ to mean that
the multiset $Y$ contains at least two copies of $A$
and write $(X \vdash Y) - (0 \vdash A)$ 
for the sequent obtained by deleting one of these copies from $Y$.
More generally, we can write $UV + UV \leq XY$ to assert that the sequent 
$XY - UV$ can be obtained from $XY$ by contracting the contents of the sequent
$UV$.
Thus, if the multiset of all formulae in $UV$ (on both sides) is the singleton
multiset \texttt{\{\#A\#\}}
we know that the skeleton of the relevant contraction
rule is one of:
$$\frac{A,A \vdash}{A \vdash} \qquad \qquad \frac{\vdash A,A}{\vdash A}$$

\begin{definition}
A set \texttt{rls} of rules satisfies the contraction admissibility property
for the formula \verb$A$ if,
whenever a derivable sequent $X \vdash Y$ satisfies
$(A \vdash 0) + (A \vdash 0) \leq (X \vdash Y)$, 
the sequent $(X \vdash Y) - (A \vdash 0)$ is derivable,
and likewise for $0 \vdash A$.
\begin{verbatim}
ctr_adm_def : "ctr_adm rls A == 
    ALL UV. ms_of_seq UV = {#A#} -->
       (ALL XY. XY : derrec rls {} --> UV + UV <= XY -->
         XY - UV : derrec rls {})"
\end{verbatim}
\end{definition}

The first condition \verb|ms_of_seq As = {#?A#}|,
asserts that the formulae on both sides of the sequent \verb!As!
form the singleton multiset \verb|{#?A#}|, thus capturing that the
contraction can happen on either side of the turnstile.

\section{Generalising Cut-Admissibility Proofs} \label{s-cagen}

We now show how our previous work~\cite{dawson-gore-generalised}
on multicut admissibility for LK
can be formulated to make it as general as possible. We first give
details of induction principles and lemmata for ``structural''
induction over implicit derivations obtained via our derivability
predicates and then describe their analogues for explicit derivation
trees.

\subsection{A General Framework for Reasoning About
Implicit Derivations}\label{s-gen-ip} 

The initial sequents of our sequent calculi will be
allowed to apply to arbitrary formulae, not only atoms, and this
excludes the possibility of proving height-preserving invertibility.
This, and also the form of our contraction rule, which allows just one
contraction per derivation step, prevents us from proving a height-preserving
\ctra{} result.
For proofs of \ctra{}, without height-preservation, an
induction principle which also involves the size or structure of the
relevant formula is required.
Furthermore, proving cut-admissibility requires induction on both size of
formula and derivation height (or a proxy for it).
We therefore require a double induction on height (or proxy) 
and formula size (as measured by any well-founded subformula relation).

\comment{
The initial rule (id) is usually couched in terms of an atomic formula
$p$ as $\Gamma , p \vdash p, \Delta$. For backward proof-search, it is
better to use the ``lifted'' version using an arbitrary formula $A$
via $\Gamma , A \vdash A, \Delta$ since this allows us to stop
backward proof-search much sooner.  But doing so excludes the
possibility of proving height-preserving invertibility and \ctra{}
results. For example, in proving the invertibility of the $(\land
\vdash)$ rule (say), the base case of the given derivation when
$\Gamma, A \land B \vdash \Delta$ is derivable using the ``lifted''
(id) rule requires us to show that $\Gamma, A, B \vdash \Delta$ is
derivable from the knowledge that $A \land B$ appears in $\Delta$.
Hence $\Delta = \Delta' \cup \{A \land B\}$ for some $\Delta'$. The
obvious solution is to argue that both $\Gamma, A, B \vdash B,
\Delta'$ and $\Gamma, A, B \vdash A, \Delta'$ are also instances of
(id) and then to apply the $(\vdash\land)$ rule (forwards) to obtain a
derivation of $\Gamma, A, B \vdash A \land B, \Delta'$.  But the
height of the derivation of $\Gamma, A, B \vdash A \land B, \Delta'$
is 2 while the height of the original derivation $\Gamma, A \land
B \vdash \Delta$ is 1, so height is not preserved.

We cannot use an induction on height alone.  That is, for
the general case when $\Gamma, A \land B \vdash \Delta$ is derived
from premises $\Gamma_1, A \land B \vdash \Delta_1$ and $\Gamma_2, A
\land B \vdash \Delta_2$ via some binary rule (say), we cannot just
claim that $\Gamma_1, A, B \vdash \Delta_1$ and $\Gamma_2, A, B \vdash
\Delta_2$ are derivable because the derivations of $\Gamma_1, A \land
B \vdash \Delta_1$ and $\Gamma_2, A \land B \vdash \Delta_2$ are
``smaller'', but we must use a lexicographic ordering
$(n, m)$ which allows us to argue that the derivations of
$\Gamma_1, A \land B \vdash \Delta_1$ and $\Gamma_2, A \land B \vdash
\Delta_2$ are ``smaller'' since their $n$-value formula-size $A \land
B$ is the same but their $m$-value is less than that of $\Gamma, A \land B
\vdash \Delta$.  We explain how we formalised such generalised
inductive principles in the next section.
}

Our first induction principle could be seen as using a lexicographic ordering
$(n,m)$ where $n$ is the sub-formula relation and $m$ is the (inverse of the)
distance from the end-sequent in the original derivation.

We use a relation \texttt{sub} on formulae: 
it could be any relation on formulae, but 
we use the (immediate) sub-formula relation. 
To put our general results in context, we may refer to \texttt{sub} as a
``sub-formula relation''.
In general we want \texttt{sub} to be well-founded; more generally
our theorems will apply to the ``well-founded part'' of \texttt{sub}.

In regard to the height measure, or distance from the original end-sequent,
our first induction principle,
instead of assuming that a property holds for all derivations of lesser
height, merely assumes that it holds for sub-derivations.
% The implementation of this first encodes an inductive step condition.

\comment{not defined as this, but proved equivalent, if we show code need
some further explanation}

\begin{definition}[\texttt{wfp}]
For a binary relation \texttt{sub}, a formula $A$ is in \texttt{wfp\ sub}, 
the ``well-founded part'' of \texttt{sub},
iff there is not any infinite descending chain $\ldots, A_2, A_1, A$
such that $(A_1, A), (A_2, A_1), \ldots$ are all in \texttt{sub}.
\end{definition}

% gen_step :: "('fml => 'seq => bool) =>
      % 'fml => ('fml * 'fml) set => 'seq set => 'seq psc => bool" 

\begin{definition}[\texttt{gen\_step}]\label{d-gen-step}
For a formula \verb$A$, a property \verb$P$,
a subformula relation \texttt{sub},
a set of sequents \texttt{derivs},
% a set of rules \texttt{rls},
% a set of \texttt{rls}-derivable sequents \texttt{derivs} 
% (e.g. \texttt{derrec rls plvs}),
and a particular rule \texttt{r = (ps, c)}, where 
\verb$ps$ is a list of premises and \verb$c$ is the conclusion of \texttt{r}:

\begin{description}
\item[\texttt{gen\_step P\ A sub derivs r}] means
\item[If] 
   \begin{enumerate}
   \item\label{d-gen-step-item:1} forall \verb$A'$ such that
     \texttt{(A', A) $\in$ sub} and all sequents \verb$s$ $\in$
     \texttt{derivs} the property \verb$P A' s$ holds, and
   \item\label{d-gen-step-item:2} for every premise \verb!p! $\in$
     \verb!ps! both \texttt{p $\in$ derivs} and \verb!P A p! holds, and
   \item \verb!c! $\in$ \texttt{derivs}
   \end{enumerate}
 \item[then] \verb!P A c! holds.
\end{description}
\end{definition}

\begin{verbatim}
gen_step_def : 
 "gen_step P A sub derivs (ps, c) =
  ( (ALL A'. (A', A) : sub --> Ball derivs (P A'))
     --> (ALL p : set ps. p : derivs & P A p) --> c : derivs 
   --> P A c)"
\end{verbatim}
In this text, \texttt{ALL p : set ps} means $\forall p \in ps$.
Typically \texttt{derivs} will be the set of sequents derivable using 
a given set \texttt{rls} of rules, and a given set of leaves \texttt{plvs},
so \texttt{derivs} = \texttt{derrec rls plvs}.

Intuitively, given a fixed rule \texttt{r = (ps, c)},
a fixed formula \texttt{A}, a fixed property \texttt{P} 
and a fixed relation \texttt{sub}, 
Definition~\ref{d-gen-step}\ref{d-gen-step-item:1} formalises
for any derivable sequent \verb$s$ that
\verb$(A, c)$ is ``less than'' 
\verb$(A', s)$
if \verb$(A', A)$ $\in$ \texttt{sub}. 
Definition~\ref{d-gen-step}\ref{d-gen-step-item:2} formalises
for any premise \verb!p! from \verb!ps!
that \verb$(A, p)$ is ``less than'' 
\verb$(A, c)$ if \verb$p$ is a premise of \verb$c$ in the rule \verb$r$.
Thus, it can be seen as a particular instance of a
 lexicographic ordering on formula-sequent 
pairs where 
$(A_1, s_1)$ is ``less than'' $(A_2, s_2)$ if
$(A_1, A_2) \in \mathtt{sub}$ or, if 
$A_1 = A_2$ and $s_2$ is a premise of $c$ via the particular rule
(instance) $r = (ps, c)$.

Alternatively, by Definition~\ref{d-gen-step},
\texttt{gen\_step} describes the situation where 
if a property $P$ is true
generally for sub-formulae $A'$, and for the
premises of a particular rule then the property holds for the
conclusion of that rule.

The main theorem, named \texttt{gen\_step\_lem} and given
as Theorem~\ref{genstep:lem} below, states that if this step case can
be proved for all possible rule instances then \verb$P$ holds for all cases.

\begin{theorem}[\texttt{gen\_step\_lem}]\label{genstep:lem}~
For a formula 
\verb!A!, a property \verb$P$,
a subformula relation \texttt{sub},
a sequent \texttt{S} and
a set of rules \texttt{rls}:
If
  \begin{enumerate}
\item \verb$A$ is in the well-founded part of the subformula relation
  \texttt{sub}, and
\item for all formulae \verb$A'$ and all rules \texttt{r} in \texttt{rls},
% and all \texttt{rls}-derivable sequents \texttt{derrec rls \{\}},
the induction step condition
\texttt{gen\_step P A' sub (derrec rls \{\}) r}
holds, and
\item sequent \texttt{S} is \texttt{rls}-derivable
  \end{enumerate}
then \texttt{P\ A\ S} holds.
\end{theorem}

\begin{verbatim}
gen_step_lem: 
  "[| ?A : wfp ?sub ;
      ALL A'. ALL r : ?rules. 
                   gen_step ?P A' ?sub (derrec ?rules {}) r ;
      ?S : derrec ?rules {} |] 
    ==> ?P ?A ?S"
\end{verbatim}

\begin{proof}
We combine the principle of well-founded induction, applied to the
formula $A$ and the well-founded subfomula relation \texttt{sub},
with the induction principle \textsf{derrec-induction} for \texttt{derrec}
shown as Lemma~\ref{l-der-ind}, which is provided by Isabelle
as a consequence of the inductive definition of \texttt{derrec}.
\end{proof}

% As we shall see in \S\ref{xxx} we can obtain \ldots\ by instantiating
% Theorem~\ref{genstep:lem} in a particular way.

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


% \section{Old Generalising Cut-Admissibility Proofs} \label{s-cagen}

% We now show how our previous work on multicut admissibility for LK
% can be formulated to make it as general as possible.
% %

% For proofs of \ctra{}, without height-preservation, a stronger
% induction principle is required. The axioms of our systems will be
% allowed to apply to arbitrary formula, not only atoms, and this
% excludes the possibility of proving height-preserving invertibility
% and \ctra{} results. To compensate for the lack of an explicit height,
% a double induction on premises (instead of explicit derivation height)
% and formula size (as measured by any well-founded subformula relation)
% is used. The implementation of this first encodes an inductive step
% condition:

% \subsection{Old A General Framework for Inductive Proofs} \label{s-gen-ip}

% \begin{definition}[\texttt{gen\_step}] \label{d-gen-step} ~\\
% %isabelle gen_step.simps
% For a formula $A$, a property $P$,
% a subformula relation \texttt{sub},
% a set of sequents \texttt{derivs},
% % a set of rules \texttt{rls},
% % a set of \texttt{rls}-derivable sequents \texttt{derivs} 
% % (e.g. \texttt{derrec rls plvs}),
% and a particular rule \texttt{r = $(ps, c)$},

% \texttt{gen\_step $P\ A$ sub derivs r} means:

%  \noindent If
%  \begin{itemize}
%    \item forall $A'$ such that \texttt{$(A', A) \in$ sub}
%    and all sequents $D \in$ \texttt{derivs} the property
%    $P\ A'\ D$ holds, 
%    \item for every premise $p \in ps$ both \texttt{$p \in$ derivs}
%      and $P\ A\ p$ holds, and
%    \item $c \in$ \texttt{derivs}
%  \end{itemize}
%  then $P\ A\ c$ holds.
% \end{definition}

% Typically \texttt{derivs} will be the set of sequents derivable using 
% a given set \texttt{rls} of rules, \texttt{derivs} = \texttt{derrec rls plvs}.

% In English, this step condition states that if a property $P$ is true
% generally for formulae of lower rank $A'$, and for the (derivable)
% premises of a particular rule then the property holds for the conclusion
% of that rule. The main theorem, named \texttt{gen\_step\_lem} and given
% as Theorem~\ref{genstep:lem} below, states that if this step case can
% be proved for all possible rule instances then $P$ holds for all cases.

% \begin{theorem}[\texttt{gen\_step\_lem}]\label{genstep:lem}~
% %isabelle gen_step_lem
% If 
% \begin{itemize}
% \item $A$ is in the well-founded part of the subformula relation \texttt{sub},
% \item sequent \texttt{S} is \texttt{rls}-derivable and
% \item for all formulae $A'$ and all possible rules \texttt{r} in \texttt{rls},
% % and all \texttt{rls}-derivable sequents \texttt{derrec rls \{\}},
% the induction step condition
% \texttt{gen\_step $P\ A'$ sub (derrec rls \{\}) r}
% holds
% \end{itemize}
% then \texttt{P\ A\ S} holds.
% \end{theorem}

\subsection{Induction for Two-premise Subtrees}

% In \S\ref{s-dp-more} we briefly mentioned
We now turn to the induction principle used for
deriving cut-admissibility, or indeed any property $P$ of two-premise
implicit derivations.  In the diagram below, to prove $P (c{l}, c{r})$,
for example, to prove that a cut between $c{l}$ and $c{r}$ 
is admissible, the induction assumption is that
 $P (psl_i, c{r})$ and $P (c{l}, psr_j)$ hold for all $i$ and $j$:
% \begin{center}
% \bpf
% \A "$\MQ_{l1} \ldots \MQ_{ln}$"
% \U "$\MR_{l}$" "$\rho_l$"
% \A "$\MQ_{r1} \ldots \MQ_{rm}$"
% \U "$\MR_{r}$" "$\rho_r$"
% \B "?" "(\textit{cut ?})"
% \epf
% \end{center}

\begin{center}
\begin{prooftree}
\AxiomC{$psl_{1} \ldots psl_{n}$}
\RightLabel{$\rho_l$}
\UnaryInfC{$cl$} 
\AxiomC{$psr_{1} \ldots psr_{m}$}
\RightLabel{$\rho_r$}
\UnaryInfC{$cr$}
\RightLabel{(\textit{cut ?})}
\dashedLine
\BinaryInfC{$\MC$}
\end{prooftree}
\end{center}
A proof of $P (cl, cr)$ using this induction assumption
inevitably proceeds according to what the rules $\rho_l$ and $\rho_r$
are, and further, for a cut-formula $A$, whether it is principal in
either or both of $\rho_l$ and $\rho_r$.  But our proofs also use
induction on the size of the cut-formula, or, more generally, on some
well-founded relation on formulae.
% Since the $psl_{i}$, etc, above are sequents, 
So we actually consider a property $P\ A\ (cl, cr)$ where
$A$ is the cut-formula,
$psl$ are the premises $psl_{1} \ldots psl_{n}$ of rule $\rho_l$,
and $cl$ is its conclusion, and analogously for $\rho_r$ and $cr$.
In proving $P\ A\ (cl, cr)$,
in addition to the inductive assumption above, we assume
that $P\ A' \ (da, db)$ holds generally for $(A', A) \in \mathtt{sub}$ and
all sequents $da$ and $db$ which are ``\texttt{rls}-derivable'',
ie, derivable from the empty set of leaves using rules from $rls$.
These intuitions give the following definition \texttt{gen\_step2sr} of 
a condition which permits one step of the inductive proof:
% where we shorten ``derivable from the empty set of premises using rule
% from \texttt{rls}'' to ``\texttt{rls}-derivable'':
\comment{this is not the same as near the end of \S6 because that one does
not also involve assuming P holds for smaller formulae}
\begin{definition}[\texttt{gen\_step2sr}]
 For a formula \texttt{A}, 
 a property \texttt{P},
 a subformula relation \texttt{sub},
 a set of rules \texttt{rls},
 sequent rules \texttt{(psl, cl)}, and
 \texttt{(psr, cr)}:\\
 \texttt{gen\_step2sr P A sub rls ((psl, cl), (psr, cr))} means:

 \noindent If 
\begin{enumerate}
 \item 
 \texttt{P~A'~(da,~db)} holds
 for all subformulae \texttt{A'} of \texttt{A}
 and all \texttt{rls}-derivable sequents 
 \texttt{da} and \texttt{db}, and
 \item for each premise \texttt{pa} in \texttt{psl}, \texttt{pa} is
 \texttt{rls}-derivable and \texttt{P A (pa, cr)} holds, and
 \item for each premise \texttt{pb} in \texttt{psr},
 \texttt{pb} is \texttt{rls}-derivable and
 \texttt{P A (cl, pb)} holds, and
 \item \texttt{cl} and \texttt{cr} are \texttt{rls}-derivable, 
 \end{enumerate} 
 then \texttt{P A (cl, cr)} holds.
\begin{verbatim}
gen_step2sr_simp :
"gen_step2sr P A sub rls ((psl, cl), (psr, cr)) =
( (ALL A'. (A', A) : sub -->
   (ALL da:derrec rls {}. 
    ALL db:derrec rls {}. P A' (da, db)))
  -->
  (ALL pa:set psl. pa : derrec rls {} & P A (pa, cr)) -->
  (ALL pb:set psr. pb : derrec rls {} & P A (cl, pb)) -->
    cl : derrec rls {} --> cr : derrec rls {} 
     --> P A (cl, cr) )"
\end{verbatim}
\end{definition}

The main theorem \texttt{gen\_step2sr\_lem} below for proving an
arbitrary property $P$ states that if the step of the inductive proof
goes through in all cases, ie, for all possible final rule instances
$\rho_l = (psl, cl)$ on the left and
$\rho_r = (psr, cr)$ on the right, then $P$ holds for all formulae $A$
and sequents $cl$ and $cr$ on the left and right respectively.

\begin{theorem}[\texttt{gen\_step2sr\_lem}]\label{thm-gen-step2sr-lem}
 If \texttt{A} is in the well-founded part of the subformula relation;
 sequents \texttt{seql} and \texttt{seqr} are \texttt{rls}-derivable ;
 and for all formulae \texttt{A'}, and all rules \texttt{(psl, cl)} and
 \texttt{(psr, cr)}, our induction step condition
 \texttt{gen\_step2sr P A' sub rls ((psl, cl), (psr, cr))}
holds, then
\texttt{P A (seql, seqr)} also holds.
\end{theorem}

\begin{verbatim}
gen_step2sr_lem : 
 "[| ?A : wfp ?sub ; 
     ?seql : derrec ?rls {} ; ?seqr : derrec ?rls {} ;
     ALL A'. ALL (psl, cl):?rls. ALL (psr, cr):?rls.
             gen_step2sr ?P A' ?sub rls ((psl, cl), (psr, cr)) |] 
     ==> ?P ?A (?seql, ?seqr)" 
\end{verbatim}

\begin{proof}
As with Lemma~\ref{genstep:lem}, the proof of this involves combining 
induction principles available to us.  It is more complex than 
Lemma~\ref{genstep:lem} because we had to deal with the well-founded induction
on the sub-formula relation and \texttt{derrec}-induction
(Lemma~\ref{l-der-ind}) on the \emph{two} implicit derivations which provide
the two premises of the cut.
\end{proof}

This enables us to split up an inductive proof, by showing,
separately, that \texttt{gen\_step2sr} holds for particular cases of
the final rules \texttt{(psl, cl)} and \texttt{(psr, cr)} on each side.
In some cases these results apply generally to different calculi. 

For example, the inductive step for the case where the cut-formula $A$ is
parametric, not principal, on the left is encapsulated in the
following theorem where \texttt{prop2 car ?erls ?A (?cl, ?cr)},
which is equivalent to \texttt{(?cl, ?cr) : car ?erls ?A},
means that the conclusion of a cut on \texttt{A} with premises
\texttt{cl} and \texttt{cr} is derivable using rules \texttt{erls}.
Below, \texttt{:\#} stands for membership of a multiset, and \texttt{\~}
stands for classical negation, and \texttt{wk\_adm} refers to weakening
admissibility for a system of rules, 
defined formally in Definition~\ref{d-wk-adm}.

\begin{theorem}
  If weakening is admissible for the rule set \texttt{erls}, all
  extensions of some rule \texttt{(ps, U |- V)} are in the rule set
  \texttt{erls}, and the final rule instance \texttt{pscl}
  of the left hand (implicit) subtree
  is an extension of \texttt{(ps, c)} where the cut-formula \texttt{A}
  is not in \texttt{V} (meaning that \texttt{A} is
  parametric on the left), then
  \texttt{gen\_step2sr (prop2 car ?erls) ?A ?sub ?rls (?pscl, ?pscr)}
  holds.

\begin{verbatim}
lcg_gen_step:
"[| wk_adm ?erls ; 
    extrs {(?ps, ?U |- ?V)} <= ?erls ; 
    ~ ?A :# ?V ;
    ?pscl = pscmap (extend (?W |- ?Z)) (?ps, ?U |- ?V) |]
==> gen_step2sr (prop2 car ?erls) ?A ?any ?erls (?pscl, ?pscr)"
\end{verbatim}
\end{theorem}

% Of course, for a system containing explicit weakening rules, 
% weakening is {\it a fortiori} admissible. 

% NEED TO ADJUST THIS - NOT INCLUDING GLS IN THIS PAPER
% This result codifies parametric proof steps, and is quite general
% enough to apply in the proof for \GLS.  As we note later, the proof
% for \GLS\ involves one really difficult case and a lot of fairly
% routine cases.  In dealing with the routine cases, automated theorem
% proving has the benefit of ensuring that no detail is overlooked; in
% addition we have the fact that, as in this example, we often have more
% general theorems that apply directly to a set of rules such as \GLS.

Notice that so far we have dealt with a shallow embedding of
derivations; it does not apply to proofs which require
derivation trees to be represented explicitly.
As noted in \S\ref{s-dtobj}, the derivability of a sequent is equivalent to
the existence of a valid derivation tree for it, and so now
we describe the similar approach for explicit derivation trees.

\subsection{Induction principles for explicit derivation trees}
\label{s-ipedt}

Sometimes we need to proceed by induction on (for example) the length of a
derivation by which a sequent can be obtained, rather than by the fact of a
sequent having been obtained earlier in the same derivation. At other
times, we not only need to do induction on height, but we may also
have to transform the immediate premises in some way, for example, by
utilising the admissibility of weakening or contraction. 

We could change our (notion of implicit derivations) derivability
predicate \verb!derrec rls plvs! with a third argument
\verb!ht!, say, so that \texttt{derrec rls plvs ht} captured the set of
sequents derivable from the leaves in \verb!plvs! using
rules from \verb!rls! with height \verb!ht!. But then it becomes much
harder to incorporate the transformations of the immediate premises of
an end-sequent using the weakening and contraction lemmata since we
have no explicit access to the derivation itself.
So to compare (say) the heights of derivations, we must be able to define them
and for this we need to look at explicit derivation trees.

We can use explicit derivation trees to perform a proof equivalent to one
using Theorem~\ref{genstep:lem},
by using the following definitions and lemmata.

\begin{definition}[\texttt{gen\_step\_tr}]
For all properties \verb!P!, all formulae \verb!B!,
all ``sub-formula'' relations \verb!sub! and 
all (explicit) derivation trees \verb!dta!:\\
\texttt{gen\_step\_tr P B sub dta} means:\\ 
if 
\begin{enumerate}
\item \verb!P C dtb! holds for all subformulae \verb!C! of \verb!B!
and all derivation trees \verb!dtb!, and 
\item 
\verb!P B dtsub! holds for all the immediate subtrees \verb!dtsub! of 
\verb!dta!
\end{enumerate}
then \verb!P B dta! holds.
\end{definition}
\begin{verbatim}
gen_step_tr_def: 
  "gen_step_tr P B sub dta ==
    (ALL C. (C, B) : sub --> (ALL dtb. P C dtb)) -->
    (ALL dtsub:set (nextUp dta). P B dtsub) --> P B dta"
\end{verbatim}

\begin{lemma}[\texttt{gen\_step\_tr\_lem}]
For all properties \verb!P!,
for all formulae \verb!A!,
for all relations \verb!sub!,
for all derivations \verb!dt!,
if \verb!A! is in the well-founded part of \verb!sub!,
and \verb!gen_step_tr P B sub dtb! holds for all formulae \verb!B! and
all derivations \verb!dtb!, then
\verb!P A dt! holds.
\end{lemma}
\begin{verbatim}
gen_step_tr_lem: 
  "[| ?A : wfp ?sub ; 
      ALL B dtb. (gen_step_tr ?P B ?sub dtb) |] 
      ==> ?P ?A ?dt"
\end{verbatim}
  
\begin{definition}[\texttt{gen\_step2\_tr}]
For all properties \verb!P!,
for all formulae \verb!B!,
for all ``sub-formula'' relations \verb!sub!,
for all pairs \verb!(dta, dtb)! of derivation trees:\\
\texttt{gen\_step2\_tr P B sub (dta, dtb)} means:\\
if
\begin{enumerate}
\item \verb!P C (dtaa, dtbb)! holds for every sub-formula \verb!C! of \verb!B!
and all derivation trees \verb!dtaa! and \verb!dtbb!,
and
\item \verb!P B (dtp, dtb)! holds for all immediate subtrees \verb!dtp! of 
\verb!dta!,
and
\item \verb!P B (dta, dtq)! holds for all immediate subtrees \verb!dtq! 
of \verb!dtb!
\end{enumerate}
then \verb!P B (dta, dtb)! holds:
\end{definition}
\begin{verbatim}
gen_step2_tr.simps: 
 "gen_step2_tr P B sub (dta, dtb) =
  ((ALL C. (C, B):sub --> (ALL dtaa dtbb. P C (dtaa, dtbb)))
  --> (ALL dtp:set (nextUp dta). P B (dtp, dtb)) 
  --> (ALL dtq:set (nextUp dtb). P B (dta, dtq)) 
  --> P B (dta, dtb))" 
\end{verbatim}

\begin{lemma}[\texttt{gen\_step2\_tr\_lem}]
For all properties \verb!P!,
for all formulae \verb!A!,
for all relations \verb!sub!,
for all derivation trees \verb!dta! and \verb!dtb!,
if \verb!A! is in the well-founded part of \verb!sub!,
and \verb!gen_step2_tr P B sub (dtaa, dtbb)! holds for all formulae \verb!B! and
all derivations \verb!dtaa! and \verb!dtbb!, then
\verb!P A (dta, dtb)! holds:  
\end{lemma}
\begin{verbatim}
gen_step2_tr_lem: 
 "[| ?A : wfp ?sub ; 
     ALL B dtaa dtbb. gen_step2_tr ?P B ?sub (dtaa, dtbb) |]
     ==> ?P ?A (?dta, ?dtb)"
\end{verbatim}

These properties are exact analogues, for explicit derivation trees,
of the properties 
\texttt{gen\_step} and  \texttt{gen\_step2sr} 
and Theorems \ref{genstep:lem} and \ref{thm-gen-step2sr-lem},
with (for example) Lemma~\ref{l-gs2-tr-casdt-sr} linking them.

However, the purpose of using explicit derivation trees is to define different
induction patterns.
For example, we defined an induction pattern which depends on the inductive
assumption that the property $P$ holds for the given tree on one side, and any
smaller tree on the other side. 

\begin{definition}[\texttt{measure}]
For all \verb!a!,
all \verb!b!,
and all functions \\
\verb!f :: 'a => nat!,
the pair \verb!(a, b)! is in \verb!measure f!
iff \verb!f a < f b!:
\end{definition}
\begin{verbatim}
measure_eq: "((?a, ?b) : measure ?f) = (?f ?a < ?f ?b)"
\end{verbatim}

\begin{definition}[\texttt{height\_step2\_tr}]
For all properties \verb!P!,
for all formulae \verb!A!,
for all subformula relations \verb!sub!,
for all pairs \verb!(dta, dtb)! of derivations, \\
\texttt{height\_step2\_tr P A sub (dta, dtb)} means: \\
if
\begin{enumerate}
\item \verb!P B (a, b)! holds for all subformulae \verb!B! of \verb!A! and
for all derivation trees \verb!a! and \verb!b!, and
\item \verb!P A (tp, dtb)! holds
for all derivation trees \verb!tp! of smaller height than \verb!dta!, and
\item \verb!P A (dta, tq)! holds 
for all derivation trees \verb!tq! of smaller height than \verb!dtb!  
\end{enumerate}
then \verb!P A (dta, dtb)! holds.
\end{definition}
\begin{verbatim}
height_step2_tr_def:
"height_step2_tr P A sub (dta, dtb) =
 ((ALL B. (B, A) : sub --> (ALL a b. P B (a, b))) -->
 (ALL dtp. heightDT dtp < heightDT dta --> P A (dtp, dtb)) -->
 (ALL dtq. heightDT dtq < heightDT dtb --> P A (dta, dtq)) -->
 P A (dta, dtb))"
\end{verbatim}

In some cases we found that this wasn't enough, and defined a more
general pattern, in which the inductive assumption applies where the sum
of the heights of the two trees is smaller.

\begin{definition}[\texttt{sumh\_step2\_tr}]
For a property \verb!P!,
a formula \verb!A!,
a subformula relation \verb!sub!,
and a pair of derivations \verb!(dta, dtb)!, \\
\texttt{sumh\_step2\_tr P A sub (dta, dtb)} means: \\
if
\begin{enumerate}
\item \verb!P B (a, b)!
holds for all subformulae \verb!B! of \verb!A!
and all derivation trees \verb!a! and \verb!b!, and
\item for all derivation trees \verb!dtaa!  and \verb!dtbb!, we have \\
$\texttt{heightDT dtaa} + \texttt{heightDT dtbb} < 
  \texttt{heightDT dta} + \texttt{heightDT dtb}$ \\ implies
\verb!P A (dtaa, dtbb)! 
\end{enumerate}
then \verb!P A (dta, dtb)! holds
\end{definition}

\begin{verbatim}
sumh_step2_tr_eq: 
 "sumh_step2_tr P A sub (dta, dtb) =
   ((ALL B. (B, A) : sub --> (ALL a b. P B (a, b))) -->
   (ALL dtaa dtbb. heightDT dtaa + heightDT dtbb <
      heightDT dta + heightDT dtb --> P A (dtaa, dtbb)) -->
   P A (dta, dtb))" 
\end{verbatim}

We could of course generalise this by replacing \texttt{heightDT} by any
natural number function, which may be different for trees on the 
left and right sides.
Indeed it could be further generalised to any well-founded relation on pairs
of derivation trees.

Each of these properties is successively weaker since the
corresponding inductive assumption is stronger, hence $P$ applies to
correspondingly wider classes of derivations: as formalised next.

\begin{lemma} \label{l-gs2-hs2-sumh}
For a property \verb!P!,
a formula \verb!A!,
a relation \verb!sub!,
and for a pair \verb!(dta, dtb)! of derivations:
\begin{enumerate}
\item \label{gs2-tr-height}
  \verb!gen_step2_tr! implies \verb!height_step2_tr!
\item \label{hs2-sumh}
  \verb!height_step2_tr! implies \verb!sumh_step2_tr!
\end{enumerate}
\end{lemma}
\begin{verbatim}
gs2_tr_height: 
  "gen_step2_tr ?P ?A ?sub (?dta, ?dtb) ==>
             height_step2_tr ?P ?A ?sub (?dta, ?dtb)" 

hs2_sumh: 
   "height_step2_tr ?P ?A ?sub (?dta, ?dtb) ==>
             sumh_step2_tr ?P ?A ?sub (?dta, ?dtb)" 
\end{verbatim}

Accordingly we need the lemma that proving these step results is sufficient
for only the weakest of them.

\begin{lemma}[\texttt{sumh\_step2\_tr\_lem}] \label{l-sumh-step2-tr-lem}
For a property \verb!P! and
a formula \verb!A! in the well-founded part of a relation
\verb!sub!,
if 
\verb!sumh_step2_tr P A sub (dta, dtb)!
holds for all derivations \verb!dta! and \verb!dtb!
then
\verb!P A (dtaa, dtbb)! holds for all derivations \verb!dtaa! and \verb!dtbb!:
\end{lemma}
\begin{verbatim}
sumh_step2_tr_lem: 
 "[|  ?A : wfp ?sub ;
      ALL A dta dtb. sumh_step2_tr ?P A ?sub (dta, dtb) |] 
  ==> ?P ?A (?dtaa, ?dtbb)"
\end{verbatim}

We are now in a position to define the statement of
cut-admissibility in Isabelle,
and to apply all of these results.

\section{Statement of Cut-Admissibility in Isabelle}
\label{s-main-lemmas}

% and the step of an inductive proof of cut-admissibility,
% for implicit and explicit derivation trees.

\begin{definition}[\texttt{cas,car}]\label{def-cas-car}
For all formulae $A$, and all pair  of sequents:
\begin{description}
\item[ \texttt{car rls} $A$] holds if the sequent obtained by applying the
  cut rule on formula $A$ to them is derivable: that is, $(X_l \vdash
  Y_l, X_r \vdash Y_r) \in \texttt{car}\ \texttt{rls}\ A$ iff $(X_l,
  (X_r - A) \vdash (Y_l - A), Y_r)$ is \texttt{rls}-derivable;

\item[\texttt{cas rls} $A$] holds if cut-admissibility on $A$ is
  available for that pair of sequents: that is, $(X_l \vdash Y_l, X_r %
  \vdash Y_r) \in \texttt{cas}\ \texttt{rls}\ A$ means that \emph{if}
  $X_l \vdash Y_l$ and $X_r \vdash Y_r$ are \texttt{rls}-derivable,
  \emph{then} $(X_l \vdash Y_l, X_r \vdash Y_r) \in \texttt{car}\
  \texttt{rls}\ A$.
\end{description}
\end{definition}

\begin{verbatim}
car_eq: 
  "((Xl |- Yl, Xr |- Yr) : car rls A) =
   ((Xl + (Xr - {#A#}) |- Yl - {#A#} + Yr) : derrec rls {})"

cas_eq: 
 "((seql, seqr) : cas rls A) =
    (seql : derrec rls {} & seqr : derrec rls {} 
      --> (seql, seqr) : car rls A)"
\end{verbatim}

% "([| ?seql : derrec ?rls {}; ?seqr : derrec ?rls {} |]
%     ==> (?seql, ?seqr) : car ?rls ?A) ==> (?seql, ?seqr) : cas ?rls ?A"

When we are talking about proving \texttt{cas} or \texttt{car}
by induction on the (implicit) derivation of the two sequents,
that is, we are talking about two sequents which are derivable,
then these two concepts become equivalent.
This is because the definition of \texttt{gen\_step2sr} only involves the 
property of the pair of sequents in the cases where those two sequents are
derivable.
Recall that \texttt{prop2} simply gives an equivalent concept with a different
type.

\begin{lemma} \label{l-gs2-cas-eq-car}
The induction steps for proving \texttt{cas} and \texttt{car} 
are equivalent:
\end{lemma}

\begin{verbatim}
prop2_def     : "prop2 f rls A seqs == seqs : f rls A"

gs2_cas_eq_car: "gen_step2sr (prop2 cas ?rls) ?A ?sub ?rls =
                 gen_step2sr (prop2 car ?rls) ?A ?sub ?rls"
\end{verbatim}

\begin{definition}[\texttt{casdt}]\label{def-casdt}
% Firstly we define \texttt{casdt}:
For any set \verb!rls! of rules  and any formula 
\verb!A!, 
two \emph{valid} (ie. no unproved leaves,
and all steps are rules of \texttt{rls})
derivation trees \texttt{dtl} and \texttt{dtr} 
satisfy \texttt{casdt rls A} 
iff their conclusions satisfy \texttt{car}:
% \marginpar{JED which is better?}
% For any set of rules \verb!rls!, and any formula 
% \verb!A!, two terms \texttt{dtl} and \texttt{dtr} 
% satisfy \texttt{casdt rls A} iff
% both \texttt{dtl} and \texttt{dtr} 
% being \emph{valid} (ie. no unproved leaves,
% and all steps are rules of \texttt{rls})
% derivation trees implies that
% their conclusions satisfy \texttt{car}:
\end{definition}
% casdt.I: "valid rls dtl & valid rls dtr -->
    % (conclDT dtl, conclDT dtr) : car rls A ==> (dtl, dtr) : casdt rls A"
\begin{verbatim}
casdt_eq: 
   "((?dtl, ?dtr) : casdt ?rls ?A) =
         (valid ?rls ?dtl & valid ?rls ?dtr 
            --> (conclDT ?dtl, conclDT ?dtr) : car ?rls ?A)"
\end{verbatim}

Here is the lemma linking the induction step for cut-admissibility in terms of
implicit derivability with the corresponding 
induction step for explicit derivation trees.

\begin{lemma}[\texttt{gs2\_tr\_casdt\_sr}]\label{l-gs2-tr-casdt-sr}
Given two derivation trees \texttt{dta} and \texttt{dtb},
a cut-formula \texttt{A}, 
a sub-formula relation \texttt{sub}, and a rule set \texttt{rls}, 
if the bottom rules of those trees satisfy the step condition 
\texttt{gen\_step2sr} for cut-admissibility, then the two trees 
satisfy the step condition \texttt{gen\_step2\_tr} for cut-admissibility:
\end{lemma}
\begin{verbatim}
gs2_tr_casdt_sr:
   "gen_step2sr (prop2 cas ?rls) ?A ?ipsubfml ?rls 
        (botRule ?dta, botRule ?dtb) ==> 
    gen_step2_tr (prop2 casdt ?rls) ?A ?ipsubfml (?dta, ?dtb)"
\end{verbatim}

In fact the two concepts are essentially equivalent:
\begin{theorem}[\texttt{gs2\_casdt\_equiv}]\label{t-gs2-casdt-equiv}
Given a set of derivation rules \texttt{rls}, a formula \texttt{A}, 
a sub-formula relation \texttt{ipsubfml} and two bottom rules \texttt{pscl}
and \texttt{pscr}, then the following are equivalent:
\begin{enumerate}
\item if \texttt{pscl} and \texttt{pscr} are in \texttt{rls},
then they satisfy the step condition
\texttt{gen\_step2sr} for cut-admissibility (for implicit derivations)
\item all trees \texttt{dta} and \texttt{dtb} whose bottom rules 
are \texttt{pscl} and \texttt{pscr} respectively, 
satisfy the step condition \texttt{gen\_step2\_tr} for cut-admissibility
(for explicit derivations)
\end{enumerate}
\end{theorem}

\begin{verbatim}
gs2_casdt_equiv:
"(?pscl : ?rls --> ?pscr : ?rls --> gen_step2sr (prop2 cas ?rls)
    ?A ?ipsubfml ?rls (?pscl, ?pscr)) =
(ALL dta dtb.  botRule dta = ?pscl --> botRule dtb = ?pscr -->
  gen_step2_tr (prop2 casdt ?rls) ?A ?ipsubfml (dta, dtb))"
\end{verbatim}

% \subsection{Weakening, Invertibility and Contraction} %
% Weakening admissibility, invertibility, and \ctra{} are stated
% using \texttt{wk\_adm}, \texttt{inv\_rl} and \texttt{ctr\_adm}
% respectively: 
% % MOST DUPLICATED EARLIER in \S11 
% \begin{description} 
% \item[\texttt{wk\_adm rls}]~\\ 
% This states that Weakening is admissible
% for \texttt{rls}. In particular, for any \texttt{rls}-derivable
% sequent $S$, the addition of any other sequent $As$ to this is also
% \texttt{rls}-derivable. Formally, given \texttt{$S \in$ derrec rls \{\}}
% then \texttt{$S + As \in$ derrec rls \{\}}. This is part of the base
% formalisation.  
% \item[\texttt{inv\_rl rls (ps, c)}]~\\ 
% Given a rule
% instance \texttt{(ps, c)}, within a particular calculus \texttt{rls},
% \texttt{inv\_rl} holds if whenever \texttt{c} is \texttt{rls}-derivable,
% then all the premises \texttt{ps} are also \texttt{rls}-derivable.
% % \item[\texttt{ctr\_adm rls A}]~\\ 
% Contraction-admissibility is
% given as a property for a set of rules \texttt{rls}, and a single
% contraction-formula \texttt{A}: for all sequents \texttt{As}, if
% the only formula in \texttt{As} is equal to \texttt{A} then for
% all \texttt{rls}-derivable sequents $S$ where \texttt{As + As}
% is a sub-sequent of $S$, it holds that $S -$\texttt{As} is also
% \texttt{rls}-derivable.  
% \end{description}

%The rather strange definition for \texttt{ctr\_adm} is used so that
% proving \ctra{} is possible using \texttt{gen\_step\_lem}, while also
% allowing the contraction-formula to be present as part of either the
% antecedent or the succedent.

%It should also be noted that the base formalisation only states
% admissibility for a single contraction-formula. However, a simple
% induction on multisets is sufficient to transform this result into an
% admissibility result for multiple formulae.

%Like \texttt{wk\_adm\_ext\_concl}, the proof of inversion lemmas
% only uses the simpler induction principle \texttt{drs.inductr} from
% Lemma~\ref{inductr:lem}. Proving \texttt{ctr\_adm} uses the induction
% principle \texttt{gen\_step\_lem} as in Lemma~\ref{genstep:lem}, which
% allows a double induction over both height and rank. Like the pen and
% paper proofs, the Isabelle proofs of \texttt{ctr\_adm} within this text
% make heavy use of inversion results.

%It is also interesting to note that when using \ctra{} within a \cuta{}
% proof, instead of picking a number of formula to contract on, it is
% simpler in Isabelle to show that the original sequent is a sub-sequent
% of the result after duplicating all formulae within the desired
% endsequent. As an example, consider a derivation of a sequent $\Gamma_C,
% \Gamma_C, \Gamma \vdash \Delta$ where we wish to use \ctra{} to derive
% $\Gamma_C, \Gamma \vdash \Delta$. In Isabelle, this is done by showing
% that the given sequent $\Gamma_C, \Gamma_C, \Gamma \vdash \Delta$ is a
% sub-sequent of $\Gamma_C, \Gamma_C, \Gamma, \Gamma \vdash \Delta, \Delta$.

% In addition to the \texttt{height\_step2\_tr\_lem} lemma,
% we also use the following induction principle, named \texttt{sum\_step2\_tr}.
% The assumption now is that the inductive property holds for two new
% derivations, where some well-founded measure on the new derivations is
% strictly less than the same measure on the derivations leading to $\MC_l$
% and $\MC_r$. For Cut, this measure will be derivation height. Essentially,
% \cuta{} of new derivations can be assumed, as long as their combined
% height is less than the level of the original cut-sequents $\MC_l$
% and $\MC_r$.

% \begin{definition}[\texttt{sum\_step2\_tr}]~\\
% For a formula $A$, a property $P$,
% a subformula relation \texttt{sub},
% measures on derivation trees \texttt{gsl} and \texttt{gsr},
% %a corresponding set of \texttt{rls}-derivable sequents \texttt{derivs}
% (e.g. \texttt{derrec rls plvs}),
% and explicit derivation trees \texttt{dta} and \texttt{dtb},
% 
% \smallskip
% 
% \texttt{sum\_step2\_tr $P\ A$ sub gsl gsr (dta, dtb)} means: \\
 % if
 % \begin{itemize} 
   % \item forall $B$ such that \texttt{$(B, A) \in$ sub}\\
   % the property $P\ B\ (a, b)$ holds for all derivation trees
     % \texttt{a} and \texttt{b}, and
   % \item for all derivation trees \texttt{dtaa} and \texttt{dtbb} where\\
   % \texttt{gsl dtaa + gsr dtbb < gsl dta + gsr dtb}\\
   % the property $P\ A (dtaa, dtbb)$ holds
 % \end{itemize} 
 % then $P\ A\ (dta, dtb)$ holds.
% \end{definition}

% Instantiating the measures in \texttt{sum\_step2\_tr} with measures 
% of derivation height results in the final principle used to prove \cuta{}:
% 
% ALREADY HAVE THIS AS LEMMA 11.5
% \begin{theorem}[\texttt{sumh\_step2\_tr\_lem}]~\\
% Where \texttt{heightDT dt} gives the height of
% an explicit derivation tree \texttt{dt}.
% \begin{description}
% \item[if]
% \texttt{A} is in the well-founded part
% of the subformula relation \texttt{sub}\\
% and for all formulae \texttt{B},
% and derivation trees \texttt{dta} and \texttt{dtb}\\
% the induction step condition 
% \texttt{sum\_step2\_tr P B sub heightDT heightDT (dta, dtb)} holds
% \item[then]
% \texttt{P A (dta, dtb)} holds
% \end{description}
% \end{theorem}

We are now ready to apply our formalisation work to particular calculi.

\section{Weakening, Contraction and Cut Admissibility for S4} \label{s-s4}

% \subsection{Motivation andRelated Work}
% \label{background:S4}

There exist both pen and paper
\cite{ohnishi1957,troelstra-schwichtenberg-basic} and a
formalised proof~\cite{dawson14} of mix-elimination for sequent
calculi for S4 containing explicit weakening and contraction rules.
As stated previously, explicit structural rules are
detrimental for automated reasoning, giving  a practical
motivation for proving that such rules are admissible. This is our goal.

Troelstra and Schwichtenberg also state \cute{} for a sequent calculus
G3s~\cite{troelstra-schwichtenberg-basic} for S4 that contains no
explicit structural rules.  Unfortunately, their ``proof''
 only discusses one actual transformation, and in particular
overlooks one non-trivial case -- when Cut is applied on a formula
$\Box A$, with both premises being an instance of the G3s R$\Box$ rule
(shown below). In this case, the deduction cannot be transformed by
simply permuting the Cut, or introducing a new Cut of smaller rank, on
the sequents in the original deduction. Greater detail is given later
in this section.
\begin{center}
% following line fixed after initial submission
\AxiomC{$\Box \Gamma \vdash A, \Diamond \Delta$}
\LeftLabel{R$\Box$}
\UnaryInfC{$\Gamma', \Box \Gamma \vdash \Box A, \Diamond \Delta, \Delta'$}
\DisplayProof
\end{center}

Goubault~\cite{Goubault96} acknowledges the problem posed by absorbing
Weakening into the R$\Box$ rule. However, his solutions are
given in the context of typed $\lambda$-calculi for a minimal version
of S4, interpreted as a sequent calculus through a version of the
Curry-Howard correspondence. Based on a proposal from
\cite{bierman96}, Goubault-Larrecq replaces the R$\Box$ rule by a
different rule with multiple premises (for subformulae within the
principal formula), along with both re-write and garbage collection
rules for the $\lambda$ terms involved. While this solution could
possibly be extended to sequent calculi, the creation of new premises
and hence branching is detrimental to backward proof search. Our
solution presented in this section also has the advantage of being
significantly simpler.

Negri~\cite{Negri05} proves various admissibility theorems for S4, but
the calculus involved is labelled. These labels include elements of
the Kripke semantics within the calculus, and so the resulting
theorems are thus not entirely syntactical proofs. Furthermore, there
are rules in the calculus which deal only with reachability between
worlds. While perhaps not as inefficient as the standard structural
rules, these rules nevertheless do not operate on logical
connectives. In particular to S4, from the perspective of automated
reasoning, applying all possible instances of the transitivity rule
(shown below) or checking whether the transitivity rule has been
saturated can be a very time-consuming process.
\begin{center}
\AxiomC{$xRz, xRy, yRz, \Gamma \vdash \Delta$}
\LeftLabel{Transitivity}
\UnaryInfC{$xRy, yRz, \Gamma \vdash \Delta$}
\DisplayProof{}

\medskip

$R$ is the accessibility relation. $x, y, z$ are worlds.
\end{center}

\subsection{Calculus for S4}

\begin{figure}[!htbp]
\centering
\begin{tabular}{ll}
\textit{Initial Sequents}\\[11px]
 \multicolumn{2}{c}{
    \AxiomC{}
    \LeftLabel{id}
    \UnaryInfC{$\Gamma, \varphi \vdash \varphi, \Delta$}
    \DisplayProof
  }
\\[15px]
\textit{Classical rules}\\[11px]
\qquad    \AxiomC{$\Gamma, \varphi , \psi \vdash \Delta$}
    \LeftLabel{L$\land$}
    \UnaryInfC{$\Gamma, \varphi \land \psi \vdash \Delta$}
    \DisplayProof 
&
    \AxiomC{$\Gamma \vdash \varphi, \Delta$}
    \AxiomC{$\Gamma \vdash \psi, \Delta$}
    \LeftLabel{R$\land$}
    \BinaryInfC{$\Gamma \vdash \varphi \land \psi ,  \Delta$}
    \DisplayProof 
\\[12px]
\qquad
    \AxiomC{$\Gamma , \varphi  \vdash \Delta$}
    \AxiomC{$\Gamma  , \psi \vdash \Delta$}
    \LeftLabel{L$\lor$}
    \BinaryInfC{$\Gamma, \varphi \lor \psi  \vdash  \Delta$}
    \DisplayProof 
&
    \AxiomC{$\Gamma \vdash \varphi , \psi, \Delta$}
    \LeftLabel{R$\lor$}
    \UnaryInfC{$\Gamma \vdash \varphi \lor \psi,  \Delta$}
    \DisplayProof 
\\[12px]
\qquad
    \AxiomC{$\Gamma \vdash \varphi, \Delta$}
    \AxiomC{$\Gamma, \psi \vdash \Delta$}
    \LeftLabel{L$\to$}
    \BinaryInfC{$\Gamma , \varphi \to \psi \vdash \Delta$}
    \DisplayProof
&
    \AxiomC{$\Gamma , \varphi \vdash \psi, \Delta$}
    \LeftLabel{R$\to$}
    \UnaryInfC{$\Gamma \vdash \varphi \to \psi, \Delta$}
    \DisplayProof
\\[12px]
\qquad
    \AxiomC{$\Gamma \vdash \varphi, \Delta$}
    \LeftLabel{L$\lnot$}
    \UnaryInfC{$\Gamma , \lnot \varphi \vdash \Delta$}
    \DisplayProof
&
    \AxiomC{$\Gamma , \varphi \vdash \Delta $}
    \LeftLabel{R$\lnot$}
    \UnaryInfC{$\Gamma \vdash \lnot \varphi, \Delta$}
    \DisplayProof
\\[15px]
\textit{Modal rules}\\[11px]
\qquad
    \AxiomC{$\Gamma , \varphi, \wbx \varphi \vdash \Delta$}
    \LeftLabel{Refl}
    \UnaryInfC{$\Gamma , \wbx \varphi \vdash \Delta$}
    \DisplayProof
&
    \AxiomC{$\Gamma , \wbx \Gamma \vdash \varphi$}
    \LeftLabel{S4$\wbx$}
    \UnaryInfC{$\Sigma, \wbx \Gamma \vdash \wbx \varphi, \Delta$}
    \DisplayProof
\end{tabular}
\caption{\label{S4:rules}Sequent calculus GS4 for S4.}
\end{figure}

% spacing in figure above needed to be adjusted to allow that figure and this
% to appear on one page, otherwise this one appears on a page by itself - why?
\begin{figure}[!htbp]
\begin{verbatim}
inductive "lksne" intrs (* skeletons of LK rules *)
  axiom   "([], {#A#} |- {#A#}) : lksne"
    ilI   "psc : lksil ==> psc  : lksne"
    irI   "psc : lksir ==> psc  : lksne"

inductive "lksss" intrs (* extended skeletons for LK *)
   extI   "psc : lksne ==> pscmap (extend flr) psc     : lksss"

inductive "lkrefl" intrs (* refl rule skeleton *)
      I   "([{#A#} + {#Box A#} |- {#}], {#Box A#} |- {#}) : lkrefl"

inductive "lkbox" intrs (* S4 Box rule skeleton *)
      I   "([gamma + mset_map Box gamma |- {#A#}],
                     mset_map Box gamma |- {#Box A#})  : lkbox"

inductive "gs4_rls" intrs
    lksI  "psc : lksss ==> psc : gs4_rls"
   reflI  "psc : lkrefl ==> pscmap (extend flr) psc  : gs4_rls"
          (* Box rule allows extra formulae in conclusion only *)
    boxI  "(prem, conc) : lkbox ==>
                              (prem, extend flr conc) : gs4_rls"
\end{verbatim}
\caption{\label{S4:rules:text}Isabelle rules for GS4.}
\end{figure}

The sequent calculus we use for S4 is based on the calculus
G3cp~\cite{troelstra-schwichtenberg-basic}, with the addition of two
modal rules.  Note that the initial sequents
$\Gamma, \varphi \vdash \varphi, \Delta$ do not require that $\varphi$
be atomic, and that there are only rules for $\wbx$ formulae since
$\wdi\varphi$ is interpreted as $\lnot\wbx\lnot\varphi$. The rules of the
calculus are shown in Figures \ref{S4:rules} and \ref{S4:rules:text}.
Note that the clause \verb!boxI! in the inductive definition for
\verb!gs4_rls!  applies \verb!extend! only to the conclusion,
corresponding to the appearance of the two sets $\Sigma$ and $\Delta$
in the conclusion of the rule $S4\wbx$.

The Isabelle encoding of the calculus is modular, with the
overall calculus, \texttt{gs4\_rls}, built up from separate
declarations of the id rule, the classical rules acting on antecedents
and succedents, and the two modal rules.


\subsection{Weakening for S4} 

Intuitively, weakening is admissible for a system of rules if,
whenever the conclusion $c$ of a rule $(ps, c)$ is weakened to $c'$, 
there is a rule with conclusion $c'$ and premises $ps'$ which are 
(optionally) weakened counterparts of $ps$.

The following definition seeks to formalise this condition.  

\begin{definition}
A set of rules \verb!rls! satisfies \verb!ext_concl! iff: for every
list of premises \verb!ps! and conclusion \verb!c! that form a
rule ($\rho_1$ say) in \verb!rls!, and for all possible
sequents \verb!UV!, there exists a list of premises \verb!ps'! such
that the premises \verb!ps'! and the extended conclusion  \verb!c + UV!
also form an instance of some rule ($\rho_1'$ say) in \verb!rls! and 
for every premise \verb!p! from \verb!ps! there is a corresponding
premise \verb!p'! in \verb!ps'! such that \verb!p'! is either \verb!p!
itself or is an extension of \verb!p!:
\end{definition}

\begin{center}
\AxiomC{$\texttt{p}_1 \ldots \texttt{p}_k$}
\RightLabel{$(\rho_1)$}
\UnaryInfC{$\texttt{c}$}
\DisplayProof
\qquad
\qquad\qquad\qquad
\AxiomC{$\texttt{p'}_1 \ldots \texttt{p'}_k$}
\RightLabel{$(\rho_1')$}
\UnaryInfC{$\texttt{c + UV}$}
\DisplayProof
\qquad\qquad\qquad
$\texttt{p}_i \leq \texttt{p'}_i$
\end{center}

% $$
% \frac{\texttt{p}_1 \ldots \texttt{p}_k}{\texttt{c}} 
% \qquad\qquad\qquad
% \frac{\texttt{p'}_1 \ldots \texttt{p'}_k}{\texttt{c + UV}}
% $$
In the Isabelle text
% \texttt{allrel} as described in \S\ref{s-dp-more}.
\texttt{(ps, ps') : allrel r} means that 
\texttt{ps} and \texttt{ps'} are lists of the same length 
where each corresponding pair of their members is in \texttt{r}.
The relation $\leq$ for sequents is defined in terms of 
$\leq$ for multisets, that is, $X \vdash Y \leq X' \vdash Y'$ means 
$X \leq X'$ and $Y \leq Y'$.

\begin{verbatim}
ext_concl_def: 
 "ext_concl rls ==
   ALL (ps, c) : rls. ALL UV. EX ps'.
   (ps', c + UV) : rls & (ps, ps') : allrel {(p, p'). p <= p'}"

inductive "allrel r" intrs
    allrel_Nil  "([], []) : allrel r"
    allrel_Cons "[| (ha, hb) : r ; (ta, tb) : allrel r |] 
                  ==>  (ha # ta, hb # tb) : allrel r"
\end{verbatim}

\begin{lemma} \label{l-ext-concl-wk}
  If rule set \verb!rls! obeys \verb!ext_concl! then \verb!rls!
  admits weakening:
\begin{verbatim}
       wk_adm_ext_concl: "ext_concl ?rls ==> wk_adm ?rls"
\end{verbatim}
\end{lemma}

  The lemma \verb!wk_adm_ext_concl! is so simple it can be proved directly 
  by the induction principle for \verb!derrec! Lemma~\ref{l-der-ind}
 % shown in \S\ref{s-dp-ind},
  (without using \verb!gen_step_lem!).
  Use of lemmas like \verb!gen_step_lem! is really only for the purpose of
  breaking up the proofs, so that various different cases of
  \verb!gen_step! (ie various final rules of the derivation) can be
  put into separate lemmata, some of which may be able to be reused for
  different calculi.

\begin{lemma} \label{l-gs4-ext-concl}
The set of rule \verb!gs4_rls! satisfies  \verb!ext_concl!.
\end{lemma}
\verb!             gs4_ext_concl: "ext_concl gs4_rls"!

\begin{corollary} \label{c-gs4-wk-adm}
 The rules of S4 satisfy weakening admissibility.
\end{corollary}
\verb!              gs4_wk_adm: "wk_adm gs4_rls"!

\subsection{Invertibility and Contraction for S4}\label{s-s4-inv-ctr}

We now describe how we captured the traditional proof of
invertibility.

Suppose that we are given a calculus consisting of the rule set
\verb!drls! and suppose that we want to reason about the derivability
predicate \verb!derrec! defined earlier. Let \verb!derivs! be the set
\verb!derrec drls {}! of all sequents that are derivable from the
empty set of leaves using the rules of \verb!drls!.  Suppose that we
wish to prove that every rule in \verb!irls! is invertible w.r.t.
\verb!drls! (where \verb!irls! is usually a subset of \verb!drls!).

Omitting details, the function
\verb!invs_of irls c! returns the set of sequents obtainable by
applying each rule of \verb!irls! to the sequent \verb!c!
\textit{backwards} once. That is, a sequent \verb!seq! is in
\verb!invs_of irls c! if applying some rule $\rho$ of \verb!irls!
to \verb!c! backwards, once, will give \verb!seq!  as one of
the premises of $\rho$.  

To prove that a rule \verb!(ps, concl)! is invertible w.r.t. \verb!drls!
requires us to prove that each sequent \verb!seq! from the list
\verb!ps! of premises is in \verb!derivs! if \verb!concl! is in
\verb!derivs!. To prove that each rule in a set of rules \verb!irls!
is invertible w.r.t. \verb!drls! requires us to prove that the above
property holds for each rule \verb!(ps, concl)! from \verb!irls!: that
is, \verb!invs_of irls concl <= derivs!  where \verb!<=! encodes the
subset relation.

Traditional proofs of invertibility proceed by an induction on
the structure of a given derivation of a sequent
\verb!concl! $\in$ \verb!derivs!. Assuming that the final rule in this
derivation is \verb!(ps, concl)!, the induction hypothesis is to
assume that the invertibility lemma holds for each premise in
\verb!ps!. That is, we assume that every sequent \verb!seq! obtained
by applying any rule from \verb!irls! \textit{backwards}, once, to any
premise \verb!p! in \verb!ps!  is itself in \verb!derivs!:
\begin{verbatim}
           ALL p:set ps. invs_of irls p <= derivs
\end{verbatim}

Use of the induction hypothesis stated above can then be encoded in 
\texttt{inv\_step} as follows.
 Let an ``\texttt{irls}-inverse'' of a sequent $s$ be a sequent $s'$
 obtained from $s$ by applying any rule from \verb!irls!  backwards once.

\begin{definition}[\texttt{inv\_step}]\label{d-inv-step}
 For a given set \verb!derivs! of derivable sequents,
 for a rule set \verb!irls!,
 and for every rule instance \verb!(ps, concl)!,
 the property: \\
 \verb!inv_step derivs irls (ps, concl)! means:
 \begin{description}
 \item[If]
  % assuming that every premise in \verb!ps! is in \verb!derivs!,
  every premise in \verb!ps! being in \verb!derivs! implies that
 every ``\texttt{irls}-invert'' of premises in \verb!ps! is in \verb!derivs!,
 \item[then] every ``\texttt{irls}-invert'' of the conclusion \texttt{concl} 
 is in \verb!derivs!.
 \end{description}
\end{definition}
\begin{verbatim}
inv_step.simps:
   "inv_step derivs irls (ps, concl) =
        (set ps <= derivs 
              --> (ALL p:set ps. invs_of irls p <= derivs) 
         --> invs_of irls concl <= derivs)"
\end{verbatim}

\comment{
note the above does use Ball, but the word Ball gets printed only where
eta-contraction is possible (and then only sometimes)
eg ALL p:set ?ps. f p is also Ball (set ps) f
and ALL p: set ps. f p q is Ball (set ps) (%p. f p q)
}

This is the key result for doing invertibility by stating various cases
of the induction step as separate lemmata.

The expression \verb!UNION (set ?ps) (invs_of ?irls)!  represents the
set $X$ of all sequents obtained by applying some rule from
\verb!irls! backwards once to every sequent \verb!p!  from a list of
sequents \verb!ps! viewed as a set:
\[
 X := \bigcup_{\verb!p!~\in~\verb!set ps!} \verb!(invs_of ?irls p)!
\]
Then, 
\verb!(set ?ps Un UNION (set ?ps) (invs_of ?irls))!
represents the union of $X$ and the list of sequents \verb!ps! treated
as a set, ie $\verb!(set ps)! \cup X$.

The property \verb!inv_stepm! is weaker than \verb!inv_step! but is
monotonic in its first argument, which makes reusing lemmata such as
\verb!lks_inv_stepm! possible as follows.

\begin{definition}[\texttt{inv\_stepm}]\label{d-inv-stepm}
For all rule sets \verb!drls!,
for all rule sets \verb!irls!,
for all rules \verb!(ps, concl)!,
the expression
\verb!inv_stepm drls irls (ps, concl)!  means: 
the \texttt{irls}-inverses of \verb!concl! 
are derivable using \verb!derrec drls! from 
\verb!(set ps)! and the \texttt{irls}-inverses 
of every \verb!p! $\in$ \verb!set ps!:
\end{definition}
\begin{verbatim}
inv_stepm.simps:
"inv_stepm drls irls (ps, concl) =
  (invs_of irls concl <= 
     derrec drls (set ps Un UNION (set ps) (invs_of irls)))"
\end{verbatim}

\begin{lemma}[\texttt{inv\_step\_mono}]\label{lemma:inv-stepm-monotonic}
 \verb!inv_stepm! is monotonic in its first argument:
\end{lemma}
\begin{verbatim}
inv_step_mono:
   "[| inv_stepm ?drlsa ?irls ?psc ; ?drlsa <= ?drlsb |] 
     ==> inv_stepm ?drlsb ?irls ?psc"
\end{verbatim}

\begin{lemma}[\texttt{inv\_step\_m}]\label{lemma:inv-step-from-inv-stepm}
  For every set \verb!drls! of rules and every 
  set \verb!plvs! of sequents, the function
  \verb!derrec drls plvs! returns the set of sequents derivable
  from \verb!plvs! using the rules of \verb!drls!. Let us call this
  set of sequents \verb!derivs!.
  For every set \verb!drls! of rules used for derivations,
  for every rule set \verb!irls!,
  for every rule \verb!psc!,
  if 
  \verb!inv_stepm drls irls psc! 
  holds then so does
  \verb!inv_step derivs irls psc!
  for any set of leaf sequents \verb!plvs!:
\end{lemma}
\begin{verbatim}
inv_step_m:
   "inv_stepm ?drls ?irls ?psc 
            ==> inv_step (derrec ?drls ?plvs) ?irls ?psc"
\end{verbatim}

\begin{lemma}[\texttt{gen\_inv\_by\_step}]\label{lemma:inv-from-inv-step}
  For every rule set \verb!rls! which is used to construct a set
  \verb!derrec rls {}! of derivations from the empty set of leaves,
%  using \verb!derrec!, 
for every rule set \verb!irls!, every rule
  \verb!psc! from \verb!irls! is invertible w.r.t. \verb!rls! if every
  rule instance \verb!(ps, concl)! from \verb!rls! obeys \\
  \verb!inv_step (derrec rls {}) irls (ps, concl)!:
\end{lemma}
\begin{verbatim}
gen_inv_by_step: 
   "[| Ball ?rls (inv_step (derrec ?rls {}) ?irls) ; 
       ?psc : ?irls |]
     ==> inv_rl ?rls ?psc"
\end{verbatim}

\begin{lemma}\label{l-gs4-refl-inv}
Every instance of the rule Refl, extended with
arbitrary contexts, is invertible in the rule set \verb!gs4_rls!:  
\end{lemma}
\begin{verbatim}
          Ball (extrs lkrefl) (inv_rl gs4_rls)
\end{verbatim}
\begin{proof}
  Suppose that $\Gamma , \wbx \varphi \vdash \Delta$ is derivable.
  We can show that the premise
  $\Gamma , \varphi, \wbx \varphi \vdash \Delta$ is derivable by 
  applying weakening, which has already been shown to be admissible in
  \verb!gs4_rls!.
\hfill
\end{proof}

\begin{lemma}\label{l-gs4-lksss-inv}
  Every instance of the rule set \verb!lksss! (of classical
  propositional logic) is invertible in the rule set
  \verb!gs4_rls!:
\end{lemma}
\begin{verbatim}
      Ball lksss (inv_rl gs4_rls)
\end{verbatim}

% \noindent{\bf Proof:} % was 
\begin{proof}
  By Lemma~\ref{lemma:inv-from-inv-step}, it suffices to prove
  \texttt{(inv\_step (derrec gs4\_rls \{\}) lksss) psc} 
  for every rule \verb!psc! from \verb!gs4_rls!.
  By Lemma~\ref{lemma:inv-step-from-inv-stepm}, it suffices to prove
  \texttt{inv\_stepm gs4\_rls lksss psc} 
  for every rule \verb!psc! from \verb!gs4_rls!.
%  
  Here, \verb!lksss == extrs lksne!, the rule set \verb!lksne!
  extended with arbitrary contexts.
  We proceed by cases on each rule 
  \verb!psc! $in$ \verb!gs4_rls!:

%{
%\addtolength\leftmargini{-2em}
\begin{description}
\item[\rm \texttt{psc} = Refl.]
  % Where the rule \verb!psc! is Refl:
  Immediate, the inverse of rule Refl is an instance of
  weakening.
\begin{verbatim}
"?psc : extrs lkrefl 
  ==> inv_stepm gs4_rls (extrs lksne) ?psc"
\end{verbatim}

\item[\rm \texttt{psc} is from LK.]
  Where the rule \verb!psc! is a classical rule, we first prove that
  the set of classical rules is invertible w.r.t. itself:
\begin{verbatim}
"?psc : extrs lksne ==> 
    inv_stepm (extrs lksne) (extrs lksne) ?psc"
\end{verbatim}
  Since the rules \verb!lksss! are a subset of the rules
  \verb!gs4_rls!, 
  we can use (the monotonicity) Lemma~\ref{lemma:inv-stepm-monotonic} 
  to obtain:
\begin{verbatim}
"?psc : extrs lksne 
  ==> inv_stepm gs4_rls (extrs lksne) ?psc"
\end{verbatim}
  
\item[\rm \texttt{psc} = $S4\wbx$.]
  When the last rule is $S4\wbx$ (with arbitrary contexts in conclusion
  only to make weakening admissible) we prove a general result.

  If the rule set \verb!rls! contains exactly one rule
  \verb!extcs {(ps, c)}! which is the rule (skeleton) \verb!(ps, c)!
  with only the conclusion extended by an arbitrary context, 
  and \texttt{rl} is any member (instance) of \texttt{rls},
  then \verb!inv_stepm rls (extrs {(ips, ic)}) rl! holds for any
  rule \verb!(ips, ic)! extended with arbitrary contexts if
  the (skeleton of the) conclusion \verb!ic! and the 
  the (skeleton of the) conclusion \verb!c! are disjoint:
\begin{verbatim}
inv_stepm_disj_cs: 
    "[| seq_meet ?c ?ic = 0 ; 
        extcs {(?ps, ?c)} = ?rls ; 
        ?rl : ?rls |] 
      ==> inv_stepm ?rls (extrs {(?ips, ?ic)}) ?rl"
\end{verbatim}

  In particular, we can put \verb!extcs {(?ps, ?c)}! to be the rule
  $S4\wbx$ and put \verb!(extrs {(?ips, ?ic)})! to be any rule from
  \verb!lksss! since the skeletons of the conclusions of the
  \verb!lksss! rules contain only the principal formula of the
  respective rule and none of these is a $\wbx$-formula.
\end{description}
% {\mbox{\bf Q.E.D.}} % was 
\hfill
\end{proof}
%}

\begin{theorem}[\texttt{inv\_rl\_gs4\_refl} and \texttt{inv\_rl\_gs4\_lks}]
The Refl (\texttt{lkrefl}) rule and all Classical (\texttt{lksss}) rules are invertible within \texttt{gs4\_rls}.
\end{theorem}
\begin{proof}
%TODO: remove this? Takes up too much space.
The theorem is simply the conjunction of Lemmas 
\ref{l-gs4-refl-inv} and \ref{l-gs4-lksss-inv}.
We explain some of the cases in English to
highlight the new aspects.

Consider invertibility for the R$\lor$ rule. We  
proceed by an induction on height, and use the induction principle 
\texttt{gen\_inv\_by\_step} from
Lemma~\ref{lemma:inv-from-inv-step}.

\begin{description}
\item[\rm Case 1 Axiom.]
If $\Gamma \vdash \varphi \lor \psi, \Delta$ is an axiom, and $\varphi
\lor \psi$ is principal, then $\Gamma = \Gamma', \varphi \lor \psi$.
The derivation for $\Gamma \vdash \varphi, \psi, \Delta$ is then:
\begin{center}
\AxiomC{}
\LeftLabel{id}
\UnaryInfC{$\Gamma', \varphi \vdash \varphi, \psi, \Delta$}
\AxiomC{}
\LeftLabel{id}
\UnaryInfC{$\Gamma', \psi \vdash \varphi, \psi, \Delta$}
\LeftLabel{L$\lor$}
\BinaryInfC{$\Gamma', \varphi \lor \psi \vdash \varphi, \psi, \Delta$}
\DisplayProof{}
\end{center}
If $\varphi \lor \psi$ is parametric in (id), then $\Gamma \vdash
\Delta$ is (id), and so is $\Gamma \vdash \varphi, \psi, \Delta$.

\item[\rm Case 2 Principal.]
If $\Gamma \vdash \varphi \lor \psi, \Delta$ is not an axiom, but
$\varphi \lor \psi$ is principal, then R$\lor$ must have been the last
rule applied. Invertibility follows immediately from the premises of
the R$\lor$ rule.

\item[\rm Case 3 Parametric.]
If $\Gamma \vdash \varphi \lor \psi, \Delta$ is not an axiom, and
$\varphi \lor \psi$ is parametric, then an application of a new instance
of that last rule (perhaps using the induction hypothesis) obtains the
necessary endsequent. This is because all rules allow arbitrary contexts
in their conclusion (and premises when the premises contain context). To
illustrate, consider the two cases when the last rule used to originally
derive $\Gamma \vdash \varphi \lor \psi, \Delta$ is either the Refl or
the S4$\wbx$ rule:
\begin{itemize}
\item
If the last rule was Refl then $\Gamma = \Gamma', \wbx A$
and the original derivation is:
\begin{center}
\AxiomC{$\Pi$}
\noLine
\UnaryInfC{$\Gamma', A, \wbx A \vdash \Delta, \varphi \lor \psi$}
\LeftLabel{Refl}
\UnaryInfC{$\Gamma', \wbx A \vdash \Delta, \varphi \lor \psi$}
\DisplayProof{}
\end{center}
Applying the inductive hypothesis on the premises gives a derivation of
$\Gamma', A, \wbx A \vdash \Delta, \varphi, \psi$. Applying Refl to this
gives the required $\Gamma', \wbx A \vdash \varphi, \psi, \Delta$.

\item If the last rule was S4$\wbx$ then $\Gamma = \Sigma, \wbx \Gamma'$ 
and $\Delta = \wbx A, \Delta'$ and the original derivation looks like:
\begin{center}
\AxiomC{$\Pi$}
\noLine
\UnaryInfC{$\Gamma', \wbx \Gamma' \vdash A$}
\LeftLabel{S4$\wbx$}
\UnaryInfC{$\Sigma, \wbx \Gamma' \vdash \wbx A, \Delta', \varphi \lor \psi$}
\DisplayProof{}
\end{center}
To derive $\Gamma \vdash \varphi, \psi, \Delta$, simply apply a new
instance of S4$\wbx$ to the original premise, this time with $\varphi,
\psi$ as the context instead of $\varphi \lor \psi$:

\begin{center}
\AxiomC{$\Pi$}
\noLine
\UnaryInfC{$\Gamma', \wbx \Gamma' \vdash A$}
\LeftLabel{S4$\wbx$}
\UnaryInfC{$\Sigma, \wbx \Gamma' \vdash \wbx A, \Delta', \varphi, \psi$}
\DisplayProof{}
\end{center}

\end{itemize}
\end{description}
\hfill
\end{proof}

\begin{theorem}[\texttt{gs4\_ctr\_adm}] \label{t-gs4-ctr-adm}
Contraction is admissible for \texttt{gs4\_rls}.
\begin{verbatim}
         gs4_ctr_adm: "ctr_adm gs4_rls ?A"
\end{verbatim}

\end{theorem}
% main results used in Isabelle are
% gen_ctr_adm_step, ctr_adm_step_lksne, sc_ctr_adm_step, 
% inv_rl_gs4_refl, ctr_adm_step_lkbox (which uses ctr_adm_step_s4g)
\begin{proof}
The cases for the G3cp % \marginpar{what is G3cp?}
and Refl rules are handled in the standard manner as in
the literature (see \cite{troelstra-schwichtenberg-basic} and \cite{Negri01}) 
using the invertibility results above. 
The formalisation performs the necessary transformations
using a simple instantiation \texttt{gen\_ctr\_adm\_step} (not shown)
of the induction principle \texttt{gen\_step\_lem} of
Theorem~\ref{genstep:lem}.

When the rule above the contraction is an instance of the S4$\wbx$
rule, there are two possible cases. Either one or both copies of the
contraction-formula exist within the context of the S4$\wbx$ rule,
or both copies are principal.

In the first case, deleting one copy still leaves an instance of the
rule. That is, if the contraction-formula is $A$, with $A$ in the
succedent, then the original rule instance is as shown below where
either $\wbx \varphi = A$ or $A \in \Delta$:
\begin{center}
\AxiomC{$\Gamma, \wbx \Gamma \vdash \varphi$}
\LeftLabel{S4$\wbx$}
\UnaryInfC{$\Sigma, \wbx \Gamma \vdash \wbx \varphi, A, \Delta$}
\DisplayProof{}
\end{center}

Applying the S4$\wbx$ rule without introducing the shown second copy
of $A$ in the conclusion above gives a proof of $\Sigma, \wbx \Gamma
\vdash \wbx \varphi, \Delta$ as required since an occurrence of $A$ is
still in the succedent as $\wbx \varphi = A$ or $A \in
\Delta$. Similarly, if $A$ is in the context $\Sigma$ the new
S4$\wbx$ rule instance is then:
%\marginpar{Was just $\varphi$ in succedent of conclusion. (for Jesse to check)}
\begin{center}
\AxiomC{$\Gamma, \wbx \Gamma \vdash \varphi$}
\LeftLabel{S4$\wbx$}
\UnaryInfC{$\Sigma - A, \wbx \Gamma \vdash \wbx\varphi, A, \Delta$}
\DisplayProof{}
\end{center}

The harder case occurs when both instances of the contraction-formula
$A$ are principal. Due to the nature of the S4$\wbx$ rule this
requires $A$ to occur in the antecedent only, as there cannot be two
principal formulae in the succedent. As only boxed formulae are
principal, $A$ has form $\wbx B$. The original rule instance is thus
represented by:
% \marginpar{Was just $\varphi$ in succedent of conclusion.}
\begin{center}
\AxiomC{$B, B, \wbx B, \wbx B,\Gamma, \wbx \Gamma \vdash \varphi$}
\LeftLabel{S4$\wbx$}
\UnaryInfC{$\Sigma, \wbx B, \wbx B, \wbx \Gamma \vdash \wbx\varphi, \Delta$}
\DisplayProof{}
\end{center}

The copies of $\wbx B$ and $B$ can be contracted upon,
 first using the induction hypothesis that the result applies to preceding
sequents in the derivation, and then on the rank of the contraction-formula.
The S4$\wbx$ rule can then be applied to give the required conclusion.
% \marginpar{Was just $\varphi$ in succedent of conclusion.}
\begin{center}
\AxiomC{$B, \wbx B,\Gamma, \wbx \Gamma \vdash \varphi$}
\LeftLabel{S4$\wbx$}
\UnaryInfC{$\Sigma, \wbx B, \wbx \Gamma \vdash \wbx\varphi, \Delta$}
\DisplayProof{}
\end{center}

In the Isabelle proof, this step is unfortunately rather more tedious. A
significant number of proof steps in the formalisation are dedicated to
manipulating the ordering of formulae to convince the proof assistant
that the S4$\wbx$ rule can be applied after applying the induction hypotheses,
and that the resulting sequent is indeed what is required.
\hfill
\end{proof}

\subsection{Cut-admissibility for S4}\label{s-s4-cut}

We first state a lemma used several times in the proof of cut-admissibility.

\begin{lemma} \label{l-gs2-car-sumhs-tr}
Given two (explicit) derivation trees \texttt{dta} and \texttt{dtb},
a cut-formula \texttt{A}, 
a sub-formula relation \texttt{sub}, and a rule set \texttt{rls}, 
if the bottom rules of those trees satisfy the step condition 
\texttt{gen\_step2sr} for cut-admissibility, then the two trees 
satisfy the step condition \texttt{sumh\_step2\_tr} for cut-admissibility:
\begin{verbatim}
gs2_car_sumhs_tr:
  "gen_step2sr (prop2 car ?rls) ?A ?sub ?rls 
               (botRule ?dta, botRule ?dtb) 
   ==> sumh_step2_tr (prop2 casdt ?rls) ?A ?sub (?dta, ?dtb)"
\end{verbatim}
\end{lemma}

\begin{proof}
By combining Lemmas
\ref{l-gs2-hs2-sumh}, \ref{l-gs2-tr-casdt-sr} and \ref{l-gs2-cas-eq-car}.
\hfill
\end{proof}

\comment{is just
gs2_car_cas RS gs2_tr_casdt_sr RS gs2_tr_height RS hs2_sumh}

\begin{theorem}[\texttt{gs4\_cas}]\label{t-gs4-cas}
Cut is admissible in the calculus \texttt{gs4\_rls}.
\end{theorem}

\begin{verbatim}
gs4_cas: 
  "(?Xl |- mins ?A ?Yl, mins ?A ?Xr |- ?Yr) : cas gs4_rls ?A"
\end{verbatim}

\begin{proof}
Our proof essentially uses a double induction on level and rank, where 
level measures the sum of the heights of the derivation trees for the left and
right premises of the cut, and rank measures the complexity of the cut-formula.
It uses Lemma~\ref{l-sumh-step2-tr-lem}, in which \texttt{?sub}
is instantiated to the immediate subformula relation.
\comment{ which means, strictly speaking, 
that so far as rank is concerned, the induction assumes only 
cut admissibility for cut-formula which are immediate subformulae}

The two most difficult cases to consider correspond to when the cut-formula is principal below an application of the S4$\wbx$ rule on the left, and also principal in either the Refl or the S4$\wbx$ rule on the right. As these are all modal rules, the Cut in question must be on a boxed formula, $\wbx A$.


%%%%%%%%%% S4 left, refl right %%%%%%%%%%
In the former case, the original Cut has form:
\begin{center}
\AxiomC{$\Pi_l$}
\noLine
\UnaryInfC{$\Gamma_L, \wbx \Gamma_L \vdash A$}
\LeftLabel{S4$\wbx$}
\UnaryInfC{$\Sigma, \wbx \Gamma_L \vdash \Delta_L, \wbx A$}
    \AxiomC{$\Pi_r$}
    \noLine
    \UnaryInfC{$ A, \wbx A, \Gamma_R \vdash \Delta_R$}
    \LeftLabel{Refl}
    \UnaryInfC{$\wbx A, \Gamma_R \vdash \Delta_R$}
\LeftLabel{Cut on $\wbx A$}
\BinaryInfC{$\Sigma, \wbx \Gamma_L, \Gamma_R \vdash \Delta_L, \Delta_R$}
\DisplayProof
\end{center}
This is transformed as follows:
\begin{center}
\AxiomC{$\Pi_l$}
\noLine
\UnaryInfC{$\Gamma_L, \wbx \Gamma_L \vdash A$}
        \AxiomC{$\Pi_l$}
        \noLine
        \UnaryInfC{$\Gamma_L, \wbx \Gamma_L \vdash A$}
        \LeftLabel{S4$\wbx$}
        \UnaryInfC{$\Sigma, \wbx \Gamma_L \vdash \Delta_L, \wbx A$}
                \AxiomC{$\Pi_r$}
                \noLine
                \UnaryInfC{$A, \wbx A, \Gamma_R \vdash \Delta_R$}
            \RightLabel{Cut on $\wbx A$}
            \BinaryInfC{$A, \Sigma, \wbx \Gamma_L, \Gamma_R \vdash \Delta_L, \Delta_R$}
    \RightLabel{Cut on $A$}
    \BinaryInfC{$\Sigma, \Gamma_L, \wbx \Gamma_L, \wbx \Gamma_L, \Gamma_R \vdash \Delta_L, \Delta_R$}
    \dashedLine
    \RightLabel{Contraction-admissibility}
    \UnaryInfC{$\Sigma, \Gamma_L, \wbx \Gamma_L, \Gamma_R \vdash \Delta_L, \Delta_R$}
    \LeftLabel{Refl$^*$}
    \UnaryInfC{$\Sigma, \wbx \Gamma_L, \Gamma_R \vdash \Delta_L, \Delta_R$}
\DisplayProof
\end{center}
Here Refl$^*$ means multiple uses of Refl, once
for each member of $\Gamma_L$.
Importantly, the new Cut on $\wbx A$ has lower level,
and the Cut on $A$ is of smaller rank.
Thus both can be eliminated by the induction hypotheses.

%%%%%%%%%% S4 both sides %%%%%%%%%%

For the latter case, when S4$\wbx$ is principal on both sides,
the original Cut has form:
\begin{center}
\AxiomC{$\Pi_l$}
\noLine
\UnaryInfC{$\Gamma_L, \wbx \Gamma_L \vdash A$}
\LeftLabel{S4$\wbx$}
\UnaryInfC{$\Sigma_L, \wbx \Gamma_L \vdash \Delta_L, \wbx A$}
    \AxiomC{$\Pi_r$}
    \noLine
    \UnaryInfC{$A, \wbx A, \Gamma_R, \wbx \Gamma_R \vdash B$}
    \LeftLabel{S4$\wbx$}
    \UnaryInfC{$\wbx A, \Sigma_R, \wbx \Gamma_R \vdash \wbx B, \Delta_R$}
\LeftLabel{Cut on $\wbx A$}
\BinaryInfC{$\Sigma_L, \Sigma_R, \wbx \Gamma_L, \wbx \Gamma_R \vdash \wbx B, \Delta_L, \Delta_R$}
\DisplayProof
\end{center}

The normal process of reducing Cut level would apply Cut
on the left cut-sequent and the premise of the right cut-sequent, as follows:
\begin{center}
\AxiomC{$\Pi_l$}
\noLine
\UnaryInfC{$\Gamma_L, \wbx \Gamma_L \vdash A$}
\LeftLabel{S4$\wbx$}
\UnaryInfC{$\Sigma_L, \wbx \Gamma_L \vdash \Delta_L, \wbx A$}
        \AxiomC{$\Pi_r$}
        \noLine
        \UnaryInfC{$A, \wbx A, \Gamma_R, \wbx \Gamma_R \vdash B$}
    \LeftLabel{Cut on $\wbx A$}
    \BinaryInfC{$A, \Sigma_L, \wbx \Gamma_L, \Gamma_R, \wbx \Gamma_R \vdash B, \Delta_L$}
\DisplayProof
\end{center}
Unfortunately, this results in a deduction where we can no longer recover
the $\wbx B$ present in the conclusion of the original Cut. The nature
of the calculus and the S4$\wbx$ rule means that new box formulae cannot
be introduced in any succedent which contains some context $\Delta$
(or where there are additional formula $\Sigma$ in the antecedent). As
stated earlier, this case is omitted in the \cute{} theorem of Troesltra
and Schwichtenberg~\cite{troelstra-schwichtenberg-basic}.

To overcome this issue without introducing the complications and new
branching rule in the solution of Goubault~\cite{Goubault96}, we
modify the original derivation of the left premise to produce one of
equal height upon which we can still apply the induction hypothesis on
level. The new application of the S4$\wbx$ rule differs from the
original by simply not adding any context in the conclusion. Formally,
the $\Sigma$ and $\Delta$ of the generic S4$\wbx$ rule in Figure
\ref{S4:rules} are $\emptyset$ in the new S4$\wbx$ instance below:
\begin{center}
\AxiomC{$\Pi_l$}
\noLine
\UnaryInfC{$\Gamma_L, \wbx \Gamma_L \vdash A$}
        \AxiomC{$\Pi_l$}
        \noLine
        \UnaryInfC{$\Gamma_L, \wbx \Gamma_L \vdash A$}
        \LeftLabel{S4$\wbx$ (new)}
        \UnaryInfC{$\wbx \Gamma_L \vdash \wbx A$}
                \AxiomC{$\Pi_r$}
                \noLine
                \UnaryInfC{$A, \wbx A, \Gamma_R, \wbx \Gamma_R \vdash B$}
            \LeftLabel{Cut on $\wbx A$}
            \BinaryInfC{$A, \wbx \Gamma_L, \Gamma_R, \wbx \Gamma_R \vdash B$}
    \RightLabel{Cut on $A$}
    \BinaryInfC{$\Gamma_L, \wbx \Gamma_L, \wbx \Gamma_L, \Gamma_R, \wbx \Gamma_R \vdash B$}
    \dashedLine
    \RightLabel{Contraction-admissibility}
    \UnaryInfC{$\Gamma_L, \wbx \Gamma_L, \Gamma_R, \wbx \Gamma_R \vdash B$}
    \LeftLabel{S4$\wbx$}
    \UnaryInfC{$\Sigma_L, \Sigma_R, \wbx \Gamma_L, \wbx \Gamma_R \vdash \wbx B, \Delta_L, \Delta_R$}
\DisplayProof
\end{center}
In the formalised proof, this instance is the only case where the
inductive principle of Lemma~\ref{l-sumh-step2-tr-lem}
% ie  \texttt{sumh\_step2\_tr\_lem}
is actually required.
As the combined height of the derivations leading to $\wbx
\Gamma_L \vdash \wbx A$ and $A, \wbx A, \Gamma_R, \wbx \Gamma_R \vdash
B$ is lower than the level of the original Cut, the induction
hypothesis on level can be applied.
In all the other cases Theorem~\ref{thm-gen-step2sr-lem}
% ie \texttt{gen\_step2sr\_lem}
would have sufficed.
So in fact in all the other cases the property we prove is
\texttt{gen\_step2sr \ldots} and we use Lemma~\ref{l-gs2-car-sumhs-tr}
to link it to the required property \texttt{sumh\_step2\_tr \ldots}
where the ellipses indicate arguments to each function as appropriate.
\hfill
\end{proof}

\section{Weakening, Contraction and Cut Admissibility for S4.3} \label{s-s43}

There exists a syntactic pen and paper proof of cut-admissibility
for S4.3 in the literature~\cite{Shimura91},
however the calculus involved contains
Weakening and Contraction as explicit rules, and mix-elimination is
proved rather than cut.  There also exist published semantic proofs of
closure under Cut for both sequent and hypersequent calculi for
S4.3~\cite{gore94,indrzejczak12}. 
% But, there are no syntactic pen and
% paper proofs of \cuta{} in the literature, nor any machine checked
% proofs for a sequent calculus for S4.3 devoid of explicit structural
% rules (as far as we know).
To our knowledge, there are no published papers for S4.3
providing a sequent calculus devoid of structural rules and proving
cut-elimination per se.

Labelled calculi~\cite{Negri05,castellini06}
are perhaps the closest representatives
in the literature. As noted previously, while these calculi do not use
Weakening or Contraction, they explicitly include the semantics of the
logic in the calculi, along with corresponding operations on world
accessibility rather than logical operators, thus they are not purely
syntactic. 

\subsection{Calculus for S4.3}

The rules of the sequent calculus for S4.3 are listed in
Figure~\ref{S43:rules}. The calculus is based on the 
version of Gor\'e~\cite{gore94}, but with Weakening absorbed into the
modal rules.  Note, in the S4.3$\Box$ rule of Figure~\ref{S43:rules},
that $\Boxes = \{\varphi_1, \dots, \varphi_n \}$ and $\Boxesi{i} =
\{\varphi_1, \dots, \varphi_{i-1}, \varphi_{i+1}, \dots, \varphi_n \}$
for $1 \leq i \leq n$.

\begin{figure}[ht]
\centering
\begin{tabular}{l@{\extracolsep{2cm}}l}
\multicolumn{2}{l}{\textit{Zero Premise Rule (Axiom)}}
\\[12px]
\multicolumn{2}{c}{
    \AxiomC{}
    \LeftLabel{id}
    \UnaryInfC{$\Gamma, \varphi \vdash \varphi, \Delta$}
    \DisplayProof
}
\\[16px]
\multicolumn{2}{l}{\textit{Classical rules}}
\\[12px]
 \qquad
 \AxiomC{$\Gamma, \varphi , \psi \vdash \Delta$}
    \LeftLabel{L$\land$}
    \UnaryInfC{$\Gamma, \varphi \land \psi \vdash \Delta$}
    \DisplayProof 
 &
    \AxiomC{$\Gamma \vdash \varphi, \Delta$}
    \AxiomC{$\Gamma \vdash \psi, \Delta$}
    \LeftLabel{R$\land$}
    \BinaryInfC{$\Gamma \vdash \varphi \land \psi ,  \Delta$}
    \DisplayProof 
\\[12px]
 \qquad
    \AxiomC{$\Gamma , \varphi  \vdash \Delta$}
    \AxiomC{$\Gamma  , \psi \vdash \Delta$}
    \LeftLabel{L$\lor$}
    \BinaryInfC{$\Gamma, \varphi \lor \psi  \vdash  \Delta$}
    \DisplayProof 
 &
    \AxiomC{$\Gamma \vdash \varphi , \psi, \Delta$}
    \LeftLabel{R$\lor$}
    \UnaryInfC{$\Gamma \vdash \varphi \lor \psi,  \Delta$}
    \DisplayProof 
\\[12px]
 \qquad
  \AxiomC{$\Gamma \vdash \varphi, \Delta$}
    \AxiomC{$\Gamma, \psi \vdash \Delta$}
    \LeftLabel{L$\to$}
    \BinaryInfC{$\Gamma , \varphi \to \psi \vdash \Delta$}
    \DisplayProof
 &
    \AxiomC{$\Gamma , \varphi \vdash \psi, \Delta$}
    \LeftLabel{R$\to$}
    \UnaryInfC{$\Gamma \vdash \varphi \to \psi, \Delta$}
    \DisplayProof
\\[12px]
 \qquad
  \AxiomC{$\Gamma \vdash \varphi, \Delta$}
    \LeftLabel{L$\lnot$}
    \UnaryInfC{$\Gamma , \lnot \varphi \vdash \Delta$}
    \DisplayProof
 &
    \AxiomC{$\Gamma , \varphi \vdash \Delta $}
    \LeftLabel{R$\lnot$}
    \UnaryInfC{$\Gamma \vdash \lnot \varphi, \Delta$}
    \DisplayProof
\\[16px]
\multicolumn{2}{l}{\textit{Modal rules}}
\\[12px]
\multicolumn{2}{c}{
    \AxiomC{$\Gamma , \varphi, \Box \varphi \vdash \Delta$}
    \LeftLabel{Refl}
    \UnaryInfC{$\Gamma , \Box \varphi \vdash \Delta$}
    \DisplayProof
}
\\[16px]
\multicolumn{2}{c}{
 \AxiomC{$\Gamma , \Box \Gamma \vdash \varphi_1, \Box \Boxesi{1} \; \cdots \; 
       \Gamma , \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i} \; \cdots \;
       \Gamma , \Box \Gamma \vdash \varphi_n, \Box \Boxesi{n}$}
    \LeftLabel{S4.3$\Box$}
    \RightLabel{$\dagger$}
    \UnaryInfC{$\Sigma, \Box \Gamma \vdash \Box \Boxes, \Delta$}
    \DisplayProof
}
\end{tabular}
\caption{\label{S43:rules}Sequent calculus for S4.3
where $\dagger$ is $\forall \psi. \Box \psi \not \in \Sigma \cup \Delta$}
\end{figure}

For backward proof search, the S4.3$\Box$ rule can
be thought of as producing a new premise for all boxed formula in its
conclusion, each of these formula being un-boxed separately in its own
premise.  Thus the general statement of the rule contains an
indeterminate number of premises, one is necessary for each $\varphi_i
\in \Boxes$. For the sake of simplicity and clarity, at times only one
of these premises will be shown as a representative for all $n$
premises. That is, the rule will be represented in the following form
shown below at left:
\[
    \AxiomC{$\Gamma , \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i}$}
    \LeftLabel{S4.3$\Box$}
    \UnaryInfC{$\Sigma, \Box \Gamma \vdash \Box \Boxes, \Delta$}
    \DisplayProof
\qquad
    \AxiomC{$\Gamma , \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i}$}
    \LeftLabel{S4.3$\Box$}
    \RightLabel{$\forall \psi. \wbx\psi \not\in \Sigma \cup \Delta$}
    \UnaryInfC{$\Sigma, \Box \Gamma \vdash \Box \Boxes, \Delta$}
    \DisplayProof
\]

There are two different versions of the S4.3$\Box$ rule: either the
context ($\Sigma\cup\Delta$) can contain any formulae, as shown
above left, or they cannot include top-level boxed-formulae, as shown
above right. In the latter case, the $\Box \Gamma$ and $\Box \Boxes$
in the conclusion of the S4.3$\Box$ rule must correspond to exactly
all the top-level boxed formulae within that sequent. The two versions
of the calculus are in fact equivalent, following a proof of the
admissibility of Weakening for the latter, however, for efficient
backward proof search, the version above right is preferred as it is
invertible and hence does not require backtracking during proof search.

Henceforth, $\Sigma$ and $\Delta$ within the S4.3$\Box$ rule will be
restricted from containing the $\Box$ operator at the top-level. In
Isabelle, this is implemented by creating a new type of formula, based
on the default formula type. HOL's \texttt{typedef} allows a concise
method of declaring new types as a subset of an existing type,
where \verb!~=! stands for inequality:
\begin{verbatim}
    typedef nboxfml =
        "{f::formula. ALL (a::formula). f ~= FC ''Box'' [a]}"
\end{verbatim}

The Isabelle formalisation of the overall calculus is based on the
calculus for S4 given in Figure~\ref{S4:rules}.  The only change is in
the S4.3$\Box$ rule, which requires the mapping function
\texttt{nboxseq} to create a new premise for each individual boxed
formula in the succedent.  The code for this is given in
Figure~\ref{S43:isabellerules}.

%\lstset{basicstyle=\ttfamily\footnotesize}
\lstset{basicstyle=\ttfamily}
\begin{figure}[hb!]
% \begin{lstlisting} % this spaces out characters for some reason
\begin{verbatim}
(* Functions to unbox one formula for each premise *)
consts
  ithprem :: "formula multiset => formula list => formula 
               => formula sequent"
  nprems  :: "formula multiset => formula list 
               => formula sequent list"

(* The boxes in the succedent are treated as a list As.
   "ms_of_list (remove1 Ai As)" is the multiset consisting of 
   all elements in "As", with one copy of "Ai" removed. *)
defs
  ithprem_def : 
    "ithprem Gamma As Ai ==
        mset_map Box Gamma + Gamma |-
        {#Ai#} + mset_map Box (ms_of_list (remove1 Ai As))"
  nprems_def : 
    "nprems Gamma As == map (ithprem Gamma As) As"

consts (* type definitions for functions *)
  gs43_rls :: "formula sequent psc set"
    s43box :: "formula sequent psc set"

(* The S4.3 box rule *)
inductive "s43box" 
 intrs
    I "(nprems gamma As, mset_map Box gamma |-
         mset_map Box (ms_of_list As))            : s43box"

(* The S4.3 calculus as an extension of the LK calculus *)
inductive "gs43_rls" 
 intrs
      lksI "psc : lksss ==> psc : gs43_rls"
     reflI "psc : lkrefl ==> 
                          pscmap (extend flr) psc : gs43_rls"
    (* boxI allows extra formulae in conclusion only,
       and enforces the `dagger' condition of Figure 5 *)
    boxI  : "(p, c) : lkbox ==> 
                       (p, extend (nboxseq flr) c) : gs43_rls"
\end{verbatim}
% \end{lstlisting}
\caption{\label{S43:isabellerules}S4.3 calculus as encoded in Isabelle}
\end{figure}
\lstset{basicstyle=\ttfamily\small}

\subsection{Weakening for S4.3} \label{s-s43-wk}
As the S4.3$\Box$ rule does not allow arbitrary contexts, \weaka{} must
be proved by induction, in this case on both height and rank
(of the implicit derivation tree, ie, using Lemma~\ref{genstep:lem}).
To simplify the case for the S4.3$\Box$ rule and its multiple premises,
we prove \weaka{} for the antecedent and succedent separately, and only
considering a single formula at a time. The Isabelle encodings for these
properties are given below. The induction itself proceeds on the height
of the derivation, with a sub-induction on the rank of the formula
$A$ being inserted into the conclusion.

\begin{definition} ~
\begin{description}
\item[\texttt{wk\_adm\_single\_antec rls}] means:\\ For any
\texttt{rls}-derivable sequent $S$, and any single formulae $A$,\\
if \texttt{$S \in$ derrec rls \{\}} then \texttt{$S + $(\{\#A\#\} |-
\{\#\}) $\in$ derrec rls \{\}}.

\item[\texttt{wk\_adm\_single\_succ rls}] means:\\ For any
\texttt{rls}-derivable sequent $S$, and any single formulae $A$,\\ if
\texttt{$S \in$ derrec rls \{\}} then \texttt{$S + $(\{\#\} |- \{\#A\#\})
$\in$ derrec rls \{\}}.

\end{description}
\end{definition}

\begin{lemma}[\texttt{wk\_adm\_sides}]
For a set of rules \texttt{rls}, 
if \texttt{wk\_adm\_single\_antec} and \texttt{wk\_adm\_single\_succ}
both hold then so does \texttt{wk\_adm}.
\end{lemma}
\begin{proof}
By multiset induction, repeatedly applying the results for single formulae.
\hfill
 \end{proof}

\begin{theorem}[\texttt{gs43\_wk\_adm}]
  Weakening is admissible for the calculus consisting of the set of
  rule \texttt{gs43\_rls}.
\end{theorem}
\begin{proof}
  In the case of the S4.3$\Box$ rule, if $A$ is not boxed, then it is
  allowed to be contained in the context of the rule's conclusion. The
  derivability of the original premises, followed by an application of
  a new S4.3$\Box$ rule including $A$ as part of its context, then
  gives the required sequent. The difficulty arises when $A$ is a
  boxed formula, say $A = \Box B$. For the sake of clarity, the
  representation of the original sequent can be split into its boxed
  and non-boxed components, so the original derivation
  is:
%\marginpar{Was $\Boxesi{i}$ in succedent of premiss.}
\begin{center}
\AxiomC{$\Pi$}
\noLine
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \varphi_i, \wbx\Boxesi{i}$}
\LeftLabel{S4.3$\Box$}
\UnaryInfC{$\Sigma, \Box \Gamma \vdash \Box \Boxes, \Delta$}
\DisplayProof{}
\end{center}

When $A$ is to be added to the antecedent, the induction on height can
be used to add $A = \Box B$ to each of the original
premises. Following this by an application of the sub-induction on
formula rank, allows the addition of $B$, giving the derivability of
$B, \Box B, \Gamma, \Box \Gamma \vdash \varphi_i, \wbx\Boxesi{i}$. An
application of the S4.3$\Box$ rule then completes the case:
\begin{center}
\AxiomC{$B, \Box B, \Gamma, \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i}$}
\LeftLabel{S4.3$\Box$}
\UnaryInfC{$\Box B, \Sigma, \Box \Gamma \vdash \Box \Boxes, \Delta$}
\DisplayProof{}
\end{center}

The final case to consider is that of adding $A = \Box B$ to the
succedent. The goal once again is to use the S4.3$\Box$ rule to give
the desired conclusion. From the original premises
{$\Gamma, \Box \Gamma \vdash \varphi_i, \wbx\Boxesi{i}$}, the induction
hypothesis on height (inserting $\Box B$) gives the derivability of
$\Gamma, \Box \Gamma \vdash \varphi_i, \wbx\Boxesi{i}, \Box B$. A
different application of the S4.3$\Box$ rule, bringing in empty
contexts, on the original premises also gives the derivability of
$\Box \Gamma \vdash \Box \Boxes$. Applying the induction on formula
rank then shows that $\Box \Gamma \vdash B, \Box \Boxes$ is
derivable.

At this point, the derivability of all necessary premises for a new
S4.3$\Box$ rule instance has been proven.
These are sequents of the form 
$\Gamma, \Box \Gamma \vdash \varphi'_i, \Box \Boxesi{i}'$ 
where $\Boxes' = \Boxes, B$ and $\varphi'$ is from the multiset 
$\Boxes \cup \{B\}$ as appropriate.
The final rule application is then:

\begin{center}
\AxiomC{$\Gamma, \Box \Gamma \vdash \varphi'_i, \Box \Boxesi{i}'$}
\LeftLabel{S4.3$\Box$}
\UnaryInfC{$\Sigma, \Box \Gamma \vdash \Box \Boxes, \Box B, \Delta$}
\DisplayProof{}
\end{center}
\hfill
\end{proof}

% In the base formalisation, a general lemma about \weaka{} suffices for a
% fairly broad range of calculi. If the conclusion of rules can be extended
% with an arbitrary context, then proving \weaka{} is very straightforward
% using an induction on height (premises in the formalisation). Weakening
% in formulae is as simple as instantiating the context of the rule as it
% was originally, but with the new formula also included. Note that this
% may require introducing new formulae in the premises as well, using the
% inductive hypothesis.

%\begin{lemma}[\texttt{wk\_adm\_ext\_concl}]\label{wk_adm:lem}
%If all rules in a calculus can be extended by arbitrary contexts
% in the conclusion, then Weakening is admissible in that calculus.
%\end{lemma}
%\begin{proof}
%By an induction on height, using drs.inductr (Lemma~\ref{inductr:lem}).
%\end{proof}

%This lemma is essentially a sufficient condition for \weaka{}, in the same
%style as the conditions for \cuta{} given by \cite{Rasga05}.
%For calculi where some rule(s) restrict contexts in their conclusion,
% the lemma \texttt{wk\_adm\_ext\_concl} no longer applies, and so a proof
% of \weaka{} requires the standard inductive style proof involving a case
% analysis of the last rule applied.

\subsection{Invertibility and Contraction for S4.3} \label{s-s43-inv-ctr}
As for S4, we prove inversion lemmata for the G3cp and Refl rules within
the overall calculus.

\begin{theorem}[\texttt{inv\_rl\_gs43\_refl} and
   \texttt{inv\_rl\_gs43\_lks}] 
Refl (\texttt{lkrefl}) and all Classical rules (\texttt{lksss})
 are invertible within the calculus \texttt{gs43\_rls}.
\end{theorem}

\begin{proof}
  Since the inverse of the Refl rule is an instance of weakening,
  which we have shown is admissible, the only notable case occurs for
  the G3cp rules, where the last rule applied in the original
  derivation is S4.3$\Box$.  The proof uses the induction principle of
  Lemma~\ref{lemma:inv-from-inv-step}.  

  If the original derivation is as shown below left then proving
  invertibility for G3cp requires showing the derivability of all
  premises after applying a G3cp rule backwards from the endsequent of
  the S4.3$\Box$ rule. The classical rules do not operate on boxed
  formulae, so this rule can only modify $\Sigma$ or $\Delta$ upwards
  into $\Sigma'$ and $\Delta'$ respectively as shown below right:
\begin{center}
\AxiomC{$\Pi$}
\noLine
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i}$}
\LeftLabel{S4.3$\Box$}
\UnaryInfC{$\Sigma, \Box \Gamma \vdash \Box \Boxes, \Delta$}
\DisplayProof{}
\qquad
\AxiomC{$\Sigma', \Box \Gamma \vdash \Box \Boxes, \Delta'$}
\LeftLabel{G3cp rule}
\UnaryInfC{$\Sigma, \Box \Gamma \vdash \Box \Boxes, \Delta$}
\DisplayProof{}
\end{center}

Clarifying again, invertibility of the G3cp rule requires deriving
 $\Sigma', \Box \Gamma \vdash \Box \Boxes, \Delta'$.
The usual tactic would apply another instance of the S4.3$\Box$ rule
to the original premises, but bringing in a different context.
However, this does not admit a proof if there are boxed formula in $\Sigma'$ or
$\Delta'$. For example, if the G3cp rule is L$\land$ and the principal
formula is $A \land \Box B$ then $\Sigma'$ contains a boxed formula,
$\Box B$, which cannot be introduced within the (box-free) context of
a new S4.3$\Box$ rule application.

To accommodate this case, the premises of the modal rule are used to
derive the conclusion without any context. Then \weaka{} is used to
bring the remaining formulae in the premise of the G3cp rule:
\begin{center}
\AxiomC{$\Pi$}
\noLine
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i}$}
\LeftLabel{S4.3$\Box$}
\UnaryInfC{$\Box \Gamma \vdash \Box \Boxes$}
\dashedLine
\LeftLabel{Weakening-admissibility}
\UnaryInfC{$\Sigma', \Box \Gamma \vdash \Box \Boxes, \Delta'$}
\DisplayProof{}
\end{center}
\hfill
\end{proof}

For S4, proving invertibility is sufficient to lead to a 
contraction admissibility proof.
However, using invertibility alone does not allow an obvious
transformation when dealing with the S4.3$\Box$ rule.
In order to prove \ctra{}, we first require the following lemma:

%TODO: possibly change the statement of this lemma?

% this lemma, called gs43_refl, is used in proof of gs43_ctr_adm, in the case 
% (* two cases, contraction formula both boxed/one unboxed in premise *)

\begin{lemma}[\texttt{gs43\_refl}]\label{lemma:R-refl-admin}
The rule R-refl is admissible in \texttt{gs43\_rls}.
\begin{center}
\AxiomC{$\Gamma \vdash \Delta, \Box A$}
\LeftLabel{R-refl}
\UnaryInfC{$\Gamma \vdash \Delta, A$}
\DisplayProof{}
\end{center}

The corresponding statement of the lemma in Isabelle (not shown) states that
%\begin{lstlisting}
%    seq : derrec gs43_rls {} -->
%      (ALL X Y. seq = extend (X |- Y) (0 |- {#Box A#}) -->
%      extend (X |- Y) (0 |- {#A#}) : derrec gs43_rls {})
%\end{lstlisting}
if a sequent \texttt{seq} is derivable in \texttt{gs43\_rls} and the
sequent is equivalent to $X \vdash Y, \Box A$ for any $X$ and $Y$,
then $X \vdash Y, A$ is also derivable.

\end{lemma}
\begin{proof}
By an induction on the structure of the (implicit) derivation tree, 
using the \texttt{derrec}-induction principle, Lemma~\ref{l-der-ind}.
% for all $\Gamma$ and $\Delta$.
The analysis is on the last rule applied in deriving
$\Gamma \vdash \Delta, \Box A$.
\begin{description}
\item[\rm Case 1 The last rule applied was id.]
If $\Box A$ is parametric then $\Gamma \vdash \Delta$ is an axiom,
and the conclusion will be also.
If $\Box A$ is principal, then $\Gamma = \{\Box A\} \cup \Gamma'$
and the following transformation is applied:
\begin{center}
\AxiomC{}
\LeftLabel{id}
\UnaryInfC{$A, \Box A, \Gamma' \vdash \Delta, A$}
\LeftLabel{Refl}
\UnaryInfC{$\Box A, \Gamma' \vdash \Delta, A$}
\DisplayProof{}
\end{center}

\item[\rm Case 2 The last rule applied was from G3cp.]
No rules in G3cp operate on a boxed formula, so $\Box A$ must be
parametric. The induction hypothesis on height is thus applicable to
the premise of the G3cp rule. Applying the original G3cp on the resulting
sequent gives the desired conclusion.

\item[\rm Case 3. The last rule applied was Refl.]
As in Case 2, $\Box A$ must be parametric,
 as Refl only operates on boxed formula in the antecedent.

\item[\rm Case 4. The last rule applied was S4.3$\Box$.]
Then one premise of the original deduction un-boxes $\Box A$.
Using Refl % as many times as required 
for each member of $\Gamma'$ (denoted by Refl$^*$)
followed by weakening admissibility
on this premise is enough to produce the conclusion.
For clarity, here we express $\Gamma = \Sigma \cup \Box \Gamma'$ and
$\Delta = \Box \Boxes \cup \Delta'$. The original derivation is:
\begin{center}
\AxiomC{$\Pi_1$}
\noLine
\UnaryInfC{$\Gamma', \Box \Gamma' \vdash \Box \Boxes, A$}
        \AxiomC{$\Pi_2$}
        \noLine
        \UnaryInfC{$\Gamma', \Box \Gamma' \vdash
          \varphi_i, \Box \Boxesi{i}, \Box A$}
    \BinaryInfC{$\Sigma, \Box \Gamma' \vdash \Box \Boxes, \Delta', \Box A$}
    \DisplayProof{}
\end{center}
This is transformed into:
\begin{center}
\AxiomC{$\Pi_1$}
\noLine
\UnaryInfC{$\Gamma', \Box \Gamma' \vdash \Box \Boxes, A$}
\LeftLabel{Refl$^*$}
\UnaryInfC{$\Box \Gamma' \vdash \Box \Boxes, A$}
\LeftLabel{Weakening-admissibility}
\dashedLine
\UnaryInfC{$\Sigma, \Box \Gamma' \vdash \Box \Boxes, \Delta', A$}
\DisplayProof{}
\end{center}
\end{description}
\hfill
\end{proof}

%The above lemma is crucial in the case when the S4.3$\Box$
% rule was the last used in a derivation.

\begin{theorem}[\texttt{gs43\_ctr\_adm}]
Contraction is admissible in \texttt{gs43\_rls}.
\end{theorem}
% this thm uses gen_ctr_adm_step which is gen_step_lem instantiated for ctr_adm
\begin{proof}
We use the induction principle Lemma~\ref{genstep:lem},
for implicit derivation trees. 
If the last rule used in the derivation was the S4.3$\Box$ rule,
there are two cases to consider. The case where the
contraction-formula is parametric is handled by simply re-applying
another instance of the S4.3$\Box$ rule as in the S4 case.
Similarly, when the contraction-formula is principal in the
antecedent, then the proof proceeds as for S4.
Specifically, one copy of $\Box A$
from $\Sigma, \Box A, \Box A, \Box \Gamma \vdash
\Box \Boxes, \Delta$ must be removed. 
The original derivation is:
\begin{center}
\AxiomC{$\Pi$}
\noLine
\UnaryInfC{$A, A, \Box A, \Box A, \Gamma, \Box \Gamma \vdash
  \varphi_i, \Box \Boxesi{i}$}
\LeftLabel{S4.3$\Box$}
\UnaryInfC{$\Sigma, \Box A, \Box A, \Box \Gamma \vdash \Box \Boxes, \Delta$}
\DisplayProof{}
\end{center}

By contracting twice using first the induction hypothesis on height,
then the induction hypothesis on rank,
on all premises followed by an application of the S4.3$\Box$ rule,
the desired endsequent is obtained:
\begin{center}
\AxiomC{$\Pi$}
\noLine
\UnaryInfC{$A, A, \Box A, \Box A, \Gamma, \Box \Gamma \vdash
  \varphi_i, \Box \Boxesi{i}$}
\dashedLine
\LeftLabel{IH on height}
\UnaryInfC{$A, A, \Box A, \Gamma, \Box \Gamma \vdash
  \varphi_i, \Box \Boxesi{i}$}
\dashedLine
\LeftLabel{IH on rank}
\UnaryInfC{$A, \Box A, \Gamma, \Box \Gamma \vdash
  \varphi_i, \Box \Boxesi{i}$}
\LeftLabel{S4.3$\Box$}
\UnaryInfC{$\Sigma, \Box A, \Box \Gamma \vdash \Box \Boxes, \Delta$}
\DisplayProof{}
\end{center}

When the contraction-formula is principal in the succedent,
there are two possible  premises to consider.
Either a premise ``un-boxes'' one of the contraction-formulae%
\footnote{Technically, there are two
syntactically identical premises which individually un-box one of the
two copies of $\Box A$.}, or it leaves both boxed.
The original deduction is:
\begin{center}
\AxiomC{$\Pi_1$}
\noLine
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \Box \Boxes, A, \Box A$}
        \AxiomC{$\Pi_2$}
        \noLine
        \UnaryInfC{$\Gamma, \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i}, \Box A, \Box A$}
    \BinaryInfC{$\Sigma, \Box \Gamma \vdash \Box \Boxes, \Box A, \Box A, \Delta$}
    \DisplayProof{}
\end{center}

In the latter case, the induction hypothesis can be directly applied,
removing one copy of the boxed formulae:
\begin{center}
\AxiomC{$\Pi_2$}
\noLine
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i},
  \Box A, \Box A$}
\dashedLine
\LeftLabel{IH on height}
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i}, \Box A$}
\DisplayProof{}
\end{center}

In the former case,
% the original derivation is:
% \begin{center}
% \AxiomC{$\Pi_1$}
% \noLine
% \UnaryInfC{$\Gamma, \Box \Gamma \vdash \Box \Boxes, A, \Box A$}
        % \AxiomC{$\Pi_2$}
        % \noLine
        % \UnaryInfC{$\Gamma, \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i}, \Box A, \Box A$}
    % \BinaryInfC{$\Sigma, \Box \Gamma \vdash \Box \Boxes, \Box A, \Box A, \Delta$}
    % \DisplayProof{}
% \end{center}
% 
% For this sub-case,
we use Lemma~\ref{lemma:R-refl-admin} to
produce the following:
\begin{center}
\AxiomC{$\Pi_1$}
\noLine
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \Box \Boxes, A, \Box A$}
\dashedLine
\LeftLabel{R-refl}
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \Box \Boxes, A, A$}
\dashedLine
\LeftLabel{IH on rank}
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \Box \Boxes, A$}
        \AxiomC{$\Pi_2$}
        \noLine
        \UnaryInfC{$\Gamma, \Box \Gamma \vdash \varphi_i, \Box
          \Boxesi{i}, \Box A, \Box A$}
        \dashedLine
        \LeftLabel{IH on height}
        \UnaryInfC{$\Gamma, \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i}, \Box A$}
    \LeftLabel{S4.3$\Box$}
    \BinaryInfC{$\Sigma, \Box \Gamma \vdash \Box \Boxes, \Box A, \Delta$}
    \DisplayProof{}
\end{center}
\hfill
\end{proof}

\subsection{Cut-admissibility for S4.3} \label{s-s43-ca}

\begin{theorem}[\texttt{gs43\_cas}]\label{t-gs43-cas}
Cut is admissible in the calculus \texttt{gs43\_rls}.
\end{theorem}
\begin{proof}
As with Theorem~\ref{t-gs4-cas}, we use the induction principle of
Lemma~\ref{l-sumh-step2-tr-lem}, involving induction on the sums of heights of
two explicit trees, although for the majority of cases the simpler principle
Theorem~\ref{thm-gen-step2sr-lem} would suffice. 
So again, in those cases, we prove 
\texttt{gen\_step2sr \ldots} and we use Lemma~\ref{l-gs2-car-sumhs-tr}
to link it to the required property \texttt{sumh\_step2\_tr \ldots},
where the ellipses indicate arguments to each function as appropriate.

When S4.3$\Box$ leads to the left cut-sequent, and the Refl rule is
used on the right, the transformation mimics the corresponding case
for S4. However, for the case where S4.3$\Box$ is principal
on both sides we require a new transformation. For clarity, the premises
above the S4.3$\Box$ rule on the left are given as two cases, depending
on whether the cut-formula is un-boxed or not. The boxed formula in the
succedents of the premises are also distinguished by the superscripts
$L$ and $R$ for left and right cut premises respectively.
Explicitly, these are 
$\Boxes^L = \{\varphi_1^L, \ldots, \varphi_i^L, \ldots, \varphi_n^L\}$
and $\Boxes^R = \{\psi_1^R, \ldots, \psi_k^R, \ldots, \psi_m^R\}$.
The original cut thus has the form:
\begin{center}
{ % \footnotesize
\AxiomC{$\Pi_L^a$}
\noLine
\UnaryInfC{$\Gamma_L, \Box \Gamma_L \vdash
  \varphi_i^L, \Box \Boxesi{i}^L, \Box A$}
        \AxiomC{$\Pi_L^b$}
        \noLine
        \UnaryInfC{$\Gamma_L, \Box \Gamma_L \vdash A, \Box \Boxes^L$}
    \LeftLabel{S4.3$\Box$}
\BinaryInfC{$\Sigma_L, \Box \Gamma_L \vdash \Box \Boxes^L, \Delta_L, \Box A$}
\UnaryInfC{$\vdots$}
\noLine
\UnaryInfC{$\vdots$}
\AxiomC{$\Pi_R$}
\noLine
\UnaryInfC{$A, \Box A, \Gamma_R, \Box \Gamma_R \vdash \psi_k^R, \Box \Boxesi{k}^R$}
\LeftLabel{S4.3$\Box$}
\UnaryInfC{$\Box A, \Sigma_R, \Box \Gamma_R \vdash \Box \Boxes^R, \Delta_R$}
\LeftLabel{Cut on $\Box A$}
\insertBetweenHyps{\hskip -3cm}
\BinaryInfC{$\Sigma_L, \Sigma_R, \Box \Gamma_L, \Box \Gamma_R \vdash \Box \Boxes^L, \Box \Boxes^R, \Delta_L, \Delta_R$}
\DisplayProof{}
}
\end{center}

To remove this cut, the derivation is transformed into one where the
principal rule (S4.3$\Box$) is applied last to produce the desired
endsequent. The problem is then proving that the premises of the following
S4.3$\Box$ rule application are derivable. This in itself requires
two different transformations of the original derivation, depending on
the two forms that the premises can take; either the un-boxed formula
in the succedent originated from the left cut premise,
that is from $\Box \Boxes^L$, or from the right, within $\Box \Boxes^R$.
These cases are named $\mathcal{P}_L$ and $\mathcal{P}_R$ respectively.
The final S4.3$\Box$ rule used in our new transformation is then:

\begin{center}
\AxiomC{$\MP_L$}
\noLine
\UnaryInfC{$\Gamma_L, \Box \Gamma_L, \Gamma_R, \Box \Gamma_R \vdash
  \varphi_i^L, \Box \Boxesi{i}^L, \Box \Boxes^R$}
\UnaryInfC{$\vdots$}
    \AxiomC{$\MP_R$}
    \noLine
    \UnaryInfC{$\Gamma_L, \Box \Gamma_L, \Gamma_R, \Box \Gamma_R \vdash \Box \Boxes^L, \psi_k^R, \Box \Boxesi{k}^R$}
\LeftLabel{S4.3$\Box$}
\insertBetweenHyps{\hskip -0.2cm}
\BinaryInfC{$\Sigma_L, \Sigma_R, \Box \Gamma_L, \Box \Gamma_R \vdash
  \Box \Boxes^L, \Box \Boxes^R, \Delta_L, \Delta_R$}
\DisplayProof{}
\end{center}

For both transformations, the same idea behind the principal S4$\Box$
rule case is used. We first derive the original cut-sequents but without
their original contexts. These new sequents will be called $\mathcal{D}_L$
and $\mathcal{D}_R$ respectively, that is, 
{$\mathcal{D}_L = \Box \Gamma_L \vdash \Box \Boxes^L, \Box A$} and
{$\mathcal{D}_R = \Box A, \Box \Gamma_R \vdash \Box \Boxes^R$}.
These are derived using the derivations in the original cut,
but applying new instances of the S4.3$\Box$ rule.
Importantly, the derivations of the new sequents $\mathcal{D}_L$ and
$\mathcal{D}_R$ have the same height as the original cut-sequents.
This is the case where the induction principle of 
Lemma~\ref{l-sumh-step2-tr-lem} is required.

\begin{center}
\AxiomC{$\Pi_L^a$}
\noLine
\UnaryInfC{$\Gamma_L, \Box \Gamma_L \vdash \varphi_i^L, \Box \Boxesi{i}^L, \Box A$}
        \AxiomC{$\Pi_L^b$}
        \noLine
        \UnaryInfC{$\Gamma_L, \Box \Gamma_L \vdash A, \Box \Boxes^L$}
    \LeftLabel{S4.3$\Box$}
    \BinaryInfC{$\mathcal{D}_L = \Box \Gamma_L \vdash \Box \Boxes^L, \Box A$}
    \DisplayProof{}
\end{center}

\begin{center}
\AxiomC{$\Pi_R$}
\noLine
\UnaryInfC{$A, \Box A, \Gamma_R, \Box \Gamma_R \vdash \psi_k^R, \Box \Boxesi{k}^R$}
\LeftLabel{S4.3$\Box$}
\UnaryInfC{$\mathcal{D}_R = \Box A, \Box \Gamma_R \vdash \Box \Boxes^R$}
\DisplayProof{}
\end{center}

Having introduced all the necessary notation and pre-requisites,
the first actual case to consider is deriving $\mathcal{P}_L$.
The induction on level allows $\mathcal{D}_R$ to be cut, on cut-formula
$\Box A$, with all of the sequents given by the derivation $\Pi_L^a$
above the original left S4.3$\Box$ rule. The transformation performs $n$
cuts, for all premises corresponding to the formulae in $\Boxes^L$.
The results of this cut then match exactly with $\mathcal{P}_L$ after using
the admissibility of Weakening to introduce the formulae of $\Gamma_R$
in the antecedent.

\begin{center}
\AxiomC{$\Pi_L^a$}
\noLine
\UnaryInfC{$\Gamma_L, \Box \Gamma_L \vdash \varphi_i^L, \Box \Boxesi{i}^L, \Box A$}
        \AxiomC{$\MD_R$}
        \noLine
        \UnaryInfC{$\Box A, \Box \Gamma_R \vdash \Box \Boxes^R$}
    \RightLabel{Cut on $\Box A$}
    \BinaryInfC{$\Gamma_L, \Box \Gamma_L, \Box \Gamma_R \vdash \varphi_i^L, \Box \Boxesi{i}^L, \Box \Boxes^R$}
    \dashedLine
    \RightLabel{Weakening-admissibility}
    \UnaryInfC{$\mathcal{P}_L = \Gamma_L, \Box \Gamma_L, \Gamma_R, \Box \Gamma_R \vdash \varphi_i^L, \Box \Boxesi{i}^L, \Box \Boxes^R$}
    \DisplayProof{}
\end{center}

To derive the sequents in $\mathcal{P}_R$, the induction hypothesis
on level is used to cut $\mathcal{D}_L$ with all of the premises above
the right S4.3$\Box$ in the original cut, with cut-formula $\Box A$.
The induction on formula rank on $A$ is then used to cut the sequent resulting
from $\Pi_L^b$ with all these new sequents. Finally, \ctra{} allows
the removal of the extra copies of $\Box \Gamma$ and $\Box \Boxes^L$,
and concludes the case.

\begin{center}
\AxiomC{$\Pi_L^b$}
\noLine
\UnaryInfC{$\Gamma_L, \Box \Gamma_L \vdash A, \Box \Boxes^L$}
\UnaryInfC{$\vdots$}
\noLine
\UnaryInfC{$\vdots$}
\noLine
\UnaryInfC{$\vdots$}
        \AxiomC{$\MD_L$}
        \noLine
        \UnaryInfC{$\Box \Gamma_L \vdash \Box \Boxes^L, \Box A$}
                \AxiomC{$\Pi_R$}
                \noLine
                \UnaryInfC{$A, \Box A, \Gamma_R, \Box \Gamma_R \vdash \psi_k^R, \Box \Boxesi{k}^R$}
            \RightLabel{Cut on $\Box A$}
            \BinaryInfC{$\Box \Gamma_L, A, \Gamma_R, \Box \Gamma_R \vdash \Box \Boxes^L, \psi_k^R, \Box \Boxesi{k}^R$}
    \RightLabel{Cut on $A$}
\insertBetweenHyps{\hskip -1.2cm}
    \BinaryInfC{$\Gamma_L, \Box \Gamma_L, \Box \Gamma_L, \Gamma_R, \Box \Gamma_R \vdash \Box \Boxes^L, \Box \Boxes^L, \psi_k^R, \Box \Boxesi{k}^R$}
    \dashedLine
    \RightLabel{\scriptsize{\hskip -1em}
      \begin{tabular}{c}Contraction-\\[-0.3ex] admissibility\end{tabular}}
    \UnaryInfC{$\mathcal{P}_R = \Gamma_L, \Box \Gamma_L, \Gamma_R, \Box \Gamma_R \vdash \Box \Boxes^L, \psi_k^R, \Box \Boxesi{k}^R$}
    \DisplayProof{}
\end{center}

To conclude, the transformations above derive $\mathcal{P}_L$ and
$\mathcal{P}_R$ while reducing cut-level or cut-rank. These are the
premises of an instance of the S4.3$\Box$ rule which results in the
conclusion of the original cut. This completes the \cuta{} proof.
\hfill
\end{proof}

\section{Weakening, Contraction and Cut Admissibility for GTD} \label{s-gtd}

We now describe Isabelle proofs of 
cut admissibility for a sequent calculus for 
the logic GTD described in \cite{mints-jaegerfest}.
%
Axiomatically, GTD is $K$ with the additional axiom
$\Box A \Leftrightarrow \Box \Box A$.
The sequent inference rules involving $\Box$,
allowing arbitrary context in
the conclusion so as to make weakening admissible,
are shown below:
$$
\frac{\wbx\Gamma,  \Gamma \vdash A}
  {\Sigma, \Box \Gamma \vdash \Box A, \Delta} (\vdash\Box)
\qquad\qquad\qquad
\frac{\wbx\Gamma,  \Gamma \vdash \Box A}
  {\Sigma, \Box \Gamma \vdash \Box A, \Delta} (\Box\vdash)
$$

% We first formalised $GTD$ as 
% \texttt{glssc GTD}
% using a framework which had previously been applied to other logics.
% \texttt{GTD} means the rules involving $\Box$, and \texttt{glssc} refers to 
% a set of classical logic rules, including explicit weakening and contraction
% rules. 

% Our formalisation involves sequents consisting of multisets of formulae on
% either side of a turnstile. 

% \begin{verbatim}
% datatype 'a sequent = Sequent "'a multiset" "'a multiset"
% \end{verbatim}

The skeletons of the above two rules are encoded as \texttt{GTD} shown below by
factoring out the form of $A$ as either $B$ or as $\wbx B$:
\begin{verbatim}
inductive "GTD"  
 intrs
    I  "A = B | A = Box B ==>
              ([mset_map Box X + X |- {#A#}], 
                mset_map Box X     |- {#Box B#}) : GTD"
\end{verbatim}

% glssc_gs2sr_ng: 
%   "[| c8ger_prop ?psubfml (glssc ?R) ?A (glne - wkrls - UNION UNIV ctrrls);
%          (?psa, ?ca) : extrs glne; (?psb, ?cb) : extrs glne |] ==>
%    gen_step2sr (prop2 mar (glssc ?R)) ?A ?psubfml (glssc ?R)
%      ((?psa, ?ca), ?psb, ?cb)"
% \end{verbatim}

% The property \texttt{c8ger\_prop} says essentially that if \emph{single} cuts 
% on subformulae of $A$ are admissible then a single cut on $A$
% is admissible where the last rules on either side are logical introduction
% rules introducing the cut-formula $A$.

% \begin{verbatim}
% "c8ger_prop ?isubfml ?drls ?A ?c8rls ==
%       ALL ps qs pse qse X Y.
%          (ps, 0 |- {#?A#}) : ?c8rls -->
%          (qs, {#?A#} |- 0) : ?c8rls -->
%          pse = map (extend (X |- Y)) ps -->
%          qse = map (extend (X |- Y)) qs -->
%          set pse Un set qse <= derrec ?drls {} -->
%          (ALL sfa.
%              (sfa, ?A) : ?isubfml --> (ALL seqs. seqs : cas ?drls sfa)) -->
%          (X |- Y) : derrec ?drls {}"
% \end{verbatim}

% In the cases of the logical introduction rules proving multicut admissibility
% is more difficult than proving single cut admissibility.  
% Where introduction of (just one instance of) the cut-formula $A$
% is the last step on each side before the cut,
%  it is nesessary to perform multicut elimination on $A$ between 
% $\MQ_{l1} \ldots \MQ_{ln}$ and $\MC_{r}$, and between
% $\MC_{l}$ and $\MQ_{r1} \ldots \MQ_{rm}$;
% then one performs single-cut elimination on the sub-formulae of $A$.
% These steps are part of the proof of \texttt{c8\_gs2\_mas}.
% An example follows.
% Note that here (unlike some of the other diagrams) the contexts
% $U$ and $Y$ may contain copies of the cut-formula.
% Let $Y'$ be $Y$ with copies of $A \land B$ deleted, and 
% $U'$ be $U$ with copies of $A \land B$ deleted.

% \begin{center}
% \begin{prooftree}
% \AxiomC{$X \vdash A, Y$}
% \AxiomC{$X \vdash B, Y$}
% \RightLabel{($\vdash \land$)}
% \BinaryInfC{$X \vdash A \land B, Y$}
% \AxiomC{$U, A, B \vdash V$}
% \RightLabel{($\land \vdash$)}
% \UnaryInfC{$U, A \land B \vdash V$}
% \RightLabel{(\textit{mix ?})}
% \dashedLine
% \BinaryInfC{$X, U' \vdash Y', V$}
% \end{prooftree}
% \end{center}

% This is replaced by

% \begin{center}
% \begin{prooftree}
% \AxiomC{$X \vdash A, Y$}
% \AxiomC{$U, A \land B \vdash V$}
% \RightLabel{(\textit{inductive mix})}
% \dashedLine
% \BinaryInfC{$X, U' \vdash A, Y', V$}
% \dashedLine
% \UnaryInfC{\large (A)}
% \end{prooftree}
% \end{center}

% \begin{center}
% \begin{prooftree}
% \AxiomC{$X \vdash B, Y$}
% \AxiomC{$U, A \land B \vdash V$}
% \RightLabel{(\textit{inductive mix})}
% \dashedLine
% \BinaryInfC{$X, U' \vdash B, Y', V$}
% \dashedLine
% \UnaryInfC{\large (B)}
% \end{prooftree}
% \end{center}

% \begin{center}
% \begin{prooftree}
% \AxiomC{$X \vdash A \land B, Y$}
% \AxiomC{$U, A, B \vdash V$}
% \RightLabel{(\textit{inductive mix})}
% \dashedLine
% \BinaryInfC{$X, U', A, B \vdash Y', V$}
% \dashedLine
% \UnaryInfC{\large (C)}
% \end{prooftree}
% \end{center}

% Then (A), (B) and (C) are combined using inductive cuts on the smaller
% cut-formulae $A$ and $B$, and the necessary contractions,
%  to derive the required sequent {$X, U' \vdash Y', V$}.

% \begin{verbatim}
% c8_gs2_mas:
%    "[| wk_adm ?drls; ?prl = (?ps, 0 |- {#?A#}); ?qrl = (?qs, {#?A#} |- 0);
%          ?prl : ?c8rls; ?qrl : ?c8rls;
%          ?eprl = pscmap (extend (?Xl |- ?Yl)) ?prl;
%          ?eqrl = pscmap (extend (?Xr |- ?Yr)) ?qrl;
%          c8ger_prop ?sub ?drls ?A ?c8rls |] ==>
%        gen_step2sr (prop2 mas ?drls) ?A ?sub ?drls (?eprl, ?eqrl)"
% \end{verbatim}

% We proved that \texttt{c8ger\_prop} holds in the following theorem.
% \begin{verbatim}
% rls_c8: "c8ger_prop ipsubfml (glssc ?rls) ?A
%    (glne - wkrls - UNION UNIV ctrrls)"
% \end{verbatim}

% It remains to look at the case where the final rule on both sides of the
% desired cut are instances of the $GTD$ rules.
% Here there are two quite distinct cases, depending on which $GTD$ rule is used
% as the final step for the left premise of the cut.  

% For the first case, the rule on the left is
%  the $(\Box \vdash)$ rule as shown,
% and for the rule on the right,
% only its conclusion matters, and is as shown.

% \begin{center}
% \begin{prooftree}
% \AxiomC{$\Gamma, \Box \Gamma \vdash \Box A$}
% \RightLabel{$(\Box\vdash)$}
% \UnaryInfC{$\Box \Gamma \vdash \Box A$}
% % \AxiomC{$A^n, \Box A^n, \Delta, \Box \Delta \vdash B'$}
% % \RightLabel{$\textit{ctr}^*\vdash$}
% % \UnaryInfC{$A, \Box A, \Delta, \Box \Delta \vdash B'$}
% \AxiomC{$\cdots$}
% \UnaryInfC{$\Box A^n, \Box \Delta \vdash \Box B$}
% \RightLabel{(\textit{mix ?})}
% \dashedLine
% \BinaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
% \end{prooftree}
% \end{center}

% we use the inductive hypothesis permitting multicutting $\Box A$ between
% $\Gamma, \Box \Gamma \vdash \Box A$ with $\Box A^n, \Box \Delta \vdash \Box B$
% then we use weakening and the $(\Box \vdash)$ rule, to get

% \begin{center}
% \begin{prooftree}
% \AxiomC{$\Gamma, \Box \Gamma \vdash \Box A$}
% \AxiomC{$\cdots$}
% \UnaryInfC{$\Box A^n, \Box \Delta \vdash \Box B$}
% \RightLabel{(\textit{inductive mix})}
% \dashedLine
% \BinaryInfC{$\Gamma, \Box \Gamma, \Box \Delta \vdash \Box B$}
% \RightLabel{(\textit{weak})}
% \UnaryInfC{$\Gamma, \Delta, \Box \Gamma, \Box \Delta \vdash \Box B$}
% \RightLabel{($\Box\vdash$)}
% \UnaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
% \end{prooftree}
% \end{center}

% The second case, with the $(\vdash \Box)$ rule on the left as shown,
% is more complicated. 
% Note that, for the rule on the right, $B'$ can be either $\Box B$ or $B$.

% \begin{center}
% \begin{prooftree}
% \AxiomC{$\Gamma, \Box \Gamma \vdash A$}
% \RightLabel{$(\Box\vdash)$}
% \UnaryInfC{$\Box \Gamma \vdash \Box A$}
% \AxiomC{$A^n, \Box A^n, \Delta, \Box \Delta \vdash B'$}
% \UnaryInfC{$\Box A^n, \Box \Delta \vdash \Box B$}
% \RightLabel{(\textit{mix ?})}
% \dashedLine
% \BinaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
% \end{prooftree}
% \end{center}

% In this case, from the premise on the right, we perform 
% inductive mix on $\Box A$ with the conclusion on the left,
% then mix on $A$ with the premise on the left,
% contraction(s) on $\Box \Gamma$, and finally an instance of the 
% $(\vdash \Box)$ or $(\Box \vdash)$ rule (whichever was on the right before).
% The result is shown below.

% \begin{center}
% \begin{prooftree}
% \AxiomC{$\Gamma, \Box \Gamma \vdash A$}
% \AxiomC{$\Box \Gamma \vdash \Box A$}
% \AxiomC{$A^n, \Box A^n, \Delta, \Box \Delta \vdash B'$}
% \RightLabel{(\textit{inductive mix})}
% \dashedLine
% \BinaryInfC{$A^n, \Box \Gamma, \Delta, \Box \Delta \vdash B'$}
% \RightLabel{(\textit{inductive mix})}
% \dashedLine
% \BinaryInfC{$\Gamma, \Box \Gamma, \Box \Gamma, \Delta, \Box \Delta \vdash B'$}
% \RightLabel{$(\textit{ctr}^*\vdash)$}
% \UnaryInfC{$\Gamma, \Box \Gamma, \Delta, \Box \Delta \vdash B'$}
% \UnaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
% \end{prooftree}
% \end{center}

% \begin{verbatim}
% glssc_gs2sr_GTD_GTD:
%    "[| (?psa, ?ca) : GTD; (?psb, ?cb) : GTD |] ==>
%    gen_step2sr (prop2 mar (glssc GTD)) ?A ipsubfml (glssc GTD)
%        ((?psa, ?ca), ?psb, ?cb)"
% \end{verbatim}

% Finally we combine these results to get the mix admissibility result.

% \begin{verbatim}
% mas_GTD: "(?seql, ?seqr) : mas (glssc GTD) ?A"
% \end{verbatim}

% \section{Inductive proof of cut (\emph{not} mix) admissibility for GTD}
% \label{s-cut-gtd}
% The previous section dealt with a proof of cut admissibility where the
% inductive hypothesis was essentially that mix-admissibility is available for
% the end-sequents of ``smaller'' pairs of derivations.

% We now want to explore what it takes to produce an inductive proof where the
% inductive hypothesis is that (specifically) single-cut admissibility is
% available for ``smaller'' pairs of derivations.

% We define the ordinary logical rules of the differently from the above, 
% so that the rules ($\vdash\lor$) and ($\land\vdash$) are 
% of the forms shown (without the context)
% $$
% \frac{A, B \vdash}{A \land B \vdash}
% \qquad
% \frac{\vdash A, B}{\vdash A \lor B }
% $$
% In these forms, these rules are invertible.

% We define the rules of the system as follows.
% The rules used for classical logic (before extending them with a context) 
% form the set \texttt{lkxcne}: the rule sets \texttt{idrls},
%  \texttt{wkrls}, \texttt{ctrrls} $A$, \texttt{lksil} and \texttt{lksir} 
% are the axioms, weakening rules, contraction (on $A$) rules, 
% and the left and right logical introduction rules.

% \begin{verbatim}
% inductive "lkxcss xrls"
%   intros
%     extI : "psc : lkxcne ==> pscmap (extend flr) psc : lkxcss xrls"
%     x : "psc : xrls ==> psc : lkxcss xrls"

% inductive "lkxcne"
%   intros
%     id : "psc : idrls ==> psc : lkxcne" 
%     wk : "psc : wkrls ==> psc : lkxcne"
%     ctr : "psc : ctrrls A ==> psc : lkxcne" 
%     ilI : "psc : lksil ==> psc : lkxcne"
%     irI : "psc : lksir ==> psc : lkxcne"
% \end{verbatim}

% When proving single-cut admissibility, the contraction rule causes a
% difficulty, since going up one step in the proof gives us an extra copy of the
% cut-formula to deal with, and the inductive hypothesis enables us to use an
% inductively available cut only to get rid of one copy of the cut-formula.

% The solution is to use the invertibility of the logical introduction rules,
% which reduces the problem of cut on a cut-formula $A$ containing a logical
% connective to cut on sub-formulae of $A$.

% Unfortunately the contraction rule causes the same sort of difficulty here as
% it does with the cut rule.
% So we have to prove, inductively, a sort of ``multi-invertibilty'' property,
% that multiple copies of a formula are invertible according to the introduction
% rule for that formula.
% Again, we define a predicate indicating that one step of an inductive proof
% of this result is available.

% Firstly, we define the set of inverses of a sequent according to a rule set:
% if $(ps, seq) \in irls$ and $p \in ps$, 
% then $p \in \texttt{invs\_of}\ irls\ seq$.

% Then the property of interest is that when a sequent is derivable, its
% inverses are also derivable.  
% The predicate \texttt{inv\_step} describes that this property holds for the 
% end-sequent of a derivation, assuming that it holds for the preceding
% sequent(s).
% Note that there are two rule sets involved, the rules used for derivations and
% the rules being shown to be invertible.

% In the definition of \texttt{inv\_step}, \texttt{derivs} will be the set of
% derivable sequents.
% Then \texttt{inv\_step} \ldots means that 
% for the last rule $(ps, concl)$ of a derivation:
% if the inverses of the premises $ps$ of that rule are derivable,
% then the inverses of the conclusion $concl$ are derivable.

% Finally, \texttt{gtd\_inv\_step} shows that the logical introduction rules,
% with each formula repeated $n$ times, and with contexts, are invertible,
% and \texttt{gtd\_inv\_rl} is the invertibility result.

% \begin{verbatim}
% invs_of_def: "invs_of ?irls ?seq ==
%          {x. EX p ps. x = p & p : set ps & (ps, ?seq) : ?irls}"

% inv_step.simps: "inv_step ?derivs ?irls (?ps, ?concl) =
%    (set ?ps <= ?derivs --> (ALL p:set ?ps. invs_of ?irls p <= ?derivs) -->
%            invs_of ?irls ?concl <= ?derivs)"

% gtd_inv_step: "[| ?r : lksil Un lksir; ?x : lkxcss GTD |] ==>
%   inv_step (derrec (lkxcss GTD) {}) (extrs (multiples {?r})) ?x"

% gtd_inv_rl: "Ball (extrs (multiples lksne)) (inv_rl (lkxcss GTD))"
% \end{verbatim}

% NOTE: From here the proof of cut admissibility is a single theorem with
% one long monolithic proof.  Perhaps I should rearrange it so as to better
% enable a description of the intermediate results.

% First we need a change in the pattern of proof by induction.
% Referring to the diagram in \S\ref{s-induction}, 
% the induction hypothesis that $P (\MQ_{li}, \MC_{r})$ and $P (\MC_{l},
% \MQ_{rj})$ hold for all $i$ and $j$ will not be sufficient.
% Rather we will need an assumption that 
% $P (\MQ'_{li}, \MC_{r})$ and $P (\MC_{l}, \MQ'_{rj})$ hold whenever 
% $\MQ'_{li}$ is derived by a derivation no larger than the derivation
% of $\MQ_{li}$ (likewise for $\MQ'_{rj}$).

% This means that we need to define the height of a derivation tree, and
% therefore that we need to define a derivation tree value whose height can be
% defined and calculated. 

% Since we have proved invertibility for the logical introduction rules, 
% when the cut-formula is a compound formula, then, regardless of what the 
% final rules in the actual derivation trees are, we can use the invertibility
% and reduce the problem to that of cuts on smaller formula.

% We then use the fact that for all the logical connnectives,
%  with their left and right logical introduction rules, 
% we can use cuts on the subformulae on the premises of the introduction rules
% to achieve the effect of a cut on the whole formula 
% on the conclusions of those introduction rules.
% This is expressed in the following theorem:

% \begin{verbatim}
% gprstep_q: "[| All (ctr_adm ?drls); wk_adm ?drls;
%    (?ps, {#} |- {#?A#}) : lksir; (?qs, {#?A#} |- {#}) : lksil;
%    ?pse = map (extend (?Xl |- ?Yl)) ?ps;
%    ?qse = map (extend (?Xr |- ?Yr)) ?qs;
%    set ?pse Un set ?qse <= derrec ?drls {};
%    ALL sfa.  (sfa, ?A) : ipsubfml --> (ALL Xl Yl Xr Yr.
%         (Xl |- mins sfa Yl, mins sfa Xr |- Yr) : cas ?drls sfa);
%    extrs lksne <= ?drls |] ==> (?Xl + ?Xr |- ?Yl + ?Yr) : derrec ?drls {}"
% \end{verbatim}

% There then remains the cases where the cut-formula $A$ is not a compound formula
% introduced by the logical introduction rules in the sets 
% \texttt{lksil} and \texttt{lksir}.

% This means that $A$ is either a boxed formula or a primitive proposition
% (or, in our formulation, a formula variable). 
% Because the bottom rule on either side may be a contraction on $A$, 
% in which case cutting with the premise of that rule is of no help, 
% we look upwards on either side to the lowest rule
% which is not a contraction on $A$.

% We have a lemma \texttt{top\_ctr\_r} which says that you can go up a derivation
% tree to a rule which is not contraction on $A$ on the right.
% A similar lemma \texttt{top\_ctr\_l} applies to contraction on the left.

% \begin{verbatim}
% top_ctr_r: "[| ?ctrrl = ([{#} |- {#?A#} + {#?A#}], {#} |- {#?A#});
%    valid ?rls ?dt; conclDT ?dt = extend ?flr ({#} |- {#?A#}) |] ==>
%    EX dtn n.  botRule dtn ~: extrs {?ctrrl} & valid ?rls dtn &
%          heightDT ?dt = heightDT dtn + n &
%          conclDT dtn = extend ?flr (times (Suc n) ({#} |- {#?A#}))"
% \end{verbatim}

% We then look at the final rule of that derivation tree (which is necessarily
% not a contraction).
% There are cases where the rule is either one of the box rules or is an
% extension $\rho'$ of a rule $\rho$ in \texttt{lkxcne},
% and in this case the rule may or may not have $A$ as its principal formula.

% Where the rule has $A$ (in succedent position) as its principal formula,
% it can only be weakening (or the axiom, which is a trivial case).
% In this case either there are no contractions following the weakening, in which
% case weakening (of $A$) makes the cut-elimination trivial, or
% we construct a tree without the weakening step and with one fewer contractions,
% and this tree has the same conclusion;
% as this tree is smaller, we can apply the inductive hypothesis that 
% cut-elimination is available.

% % end of rwr_tacs
% Next there is the case where the principal formula of the rule $\rho$
% is not $A$.  
% This case is like the parametric rule case of the simpler cut-elimiation
% proofs.

% \begin{center}
% \begin{prooftree}
% \AxiomC{$X' \vdash Y', A^n$}
% \RightLabel{($\rho'$)}
% \UnaryInfC{$X \vdash Y, A^n$}
% \RightLabel{($\textit{ctr}^* \vdash$)}
% \UnaryInfC{$X \vdash Y, A$}
% \AxiomC{$A, U \vdash V$}
% \RightLabel{(\textit{cut ?})}
% \dashedLine
% \BinaryInfC{$X, U \vdash Y, V$}
% \end{prooftree}
% \end{center}

% Here we must apply the requisite number of contractions on $A$ to the premises
% of $\rho'$, then apply (using the inductive hypothesis) cut on $A$ to each of
% them, and finally apply $\rho''$ which is the appropriate (but different from
% $\rho'$) extension of $\rho$.

% \begin{center}
% \begin{prooftree}
% \AxiomC{$X' \vdash Y', A^n$}
% \RightLabel{($\textit{ctr}^* \vdash$)}
% \UnaryInfC{$X' \vdash Y', A$}
% \AxiomC{$A, U \vdash V$}
% \RightLabel{(\textit{inductive cut})}
% \dashedLine
% \BinaryInfC{$X', U \vdash Y', V$}
% \RightLabel{($\rho''$)}
% \UnaryInfC{$X, U \vdash Y, V$}
% \end{prooftree}
% \end{center}

% The remaining case is where the last rule on the left above the contractions on
% $A$ is one of the $GTD$ rules. 
% But as their conclusion is of the form $\Box \Gamma \vdash \Box A$,
% this tells us that there are in fact no contractions following this rule.

% We now look at the right side, and again, look for the last rule above a
% continuous sequence of contractions on the cut-formula.

% Among the cases of the last rule on the right above the contractions,
% the cases of axiom or weakening involving $A$, or an extension of
% a rule in \texttt{lkxcne} whose principal formula is not $A$, are similar to
% those above.

% This leaves us the case where the last rules on both sides above any
% contractions are the GTD rules.

% For the first case, the rule on the left is
%  the $(\Box \vdash)$ rule as shown,
% and for the rule on the right,
% only its conclusion matters, and is as shown.

% \begin{center}
% \begin{prooftree}
% \AxiomC{$\Gamma, \Box \Gamma \vdash \Box A$}
% \RightLabel{$(\Box\vdash)$}
% \UnaryInfC{$\Box \Gamma \vdash \Box A$}
% % \AxiomC{$A^n, \Box A^n, \Delta, \Box \Delta \vdash B'$}
% % \RightLabel{$\textit{ctr}^*\vdash$}
% % \UnaryInfC{$A, \Box A, \Delta, \Box \Delta \vdash B'$}
% \AxiomC{$\cdots$}
% \UnaryInfC{$\Box A^n, \Box \Delta \vdash \Box B$}
% \RightLabel{$(\textit{ctr}^*\vdash)$}
% \UnaryInfC{$\Box A, \Box \Delta \vdash \Box B$}
% \RightLabel{(\textit{cut ?})}
% \dashedLine
% \BinaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
% \end{prooftree}
% \end{center}

% We use the inductive hypothesis permitting cutting $\Box A$ between
% $\Gamma, \Box \Gamma \vdash \Box A$ and $\Box A, \Box \Delta \vdash \Box B$
% then we use weakening and the $(\Box \vdash)$ rule, to get

% \begin{center}
% \begin{prooftree}
% \AxiomC{$\Gamma, \Box \Gamma \vdash \Box A$}
% \AxiomC{$\cdots$}
% \UnaryInfC{$\Box A, \Box \Delta \vdash \Box B$}
% \RightLabel{(\textit{inductive cut})}
% \dashedLine
% \BinaryInfC{$\Gamma, \Box \Gamma, \Box \Delta \vdash \Box B$}
% \RightLabel{(\textit{weak})}
% \UnaryInfC{$\Gamma, \Delta, \Box \Gamma, \Box \Delta \vdash \Box B$}
% \RightLabel{($\Box\vdash$)}
% \UnaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
% \end{prooftree}
% \end{center}

% The second case, with the $(\vdash \Box)$ rule on the left as shown,
% is more complicated. 
% Note that, for the rule on the right, $B'$ can be either $\Box B$ or $B$.

% \begin{center}
% \begin{prooftree}
% \AxiomC{$\Gamma, \Box \Gamma \vdash A$}
% \RightLabel{$(\Box\vdash)$}
% \UnaryInfC{$\Box \Gamma \vdash \Box A$}
% \AxiomC{$A^n, \Box A^n, \Delta, \Box \Delta \vdash B'$}
% \UnaryInfC{$\Box A^n, \Box \Delta \vdash \Box B$}
% \RightLabel{$(\textit{ctr}^*\vdash)$}
% \UnaryInfC{$\Box A, \Box \Delta \vdash \Box B$}
% \RightLabel{(\textit{cut ?})}
% \dashedLine
% \BinaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
% \end{prooftree}
% \end{center}

% In this case, from the premise on the right, we perform contractions on 
% $\Box A$, then inductive cut on $\Box A$ with the conclusion on the left,
% then contractions on $A$, then cut on $A$ with the premise on the left,
% contraction(s) on $\Box \Gamma$, and finally an instance of the 
% $(\vdash \Box)$ or $(\Box \vdash)$ rule (whichever was on the right before).
% The result is shown below.

% \begin{center}
% \begin{prooftree}
% \AxiomC{$\Gamma, \Box \Gamma \vdash A$}
% \AxiomC{$\Box \Gamma \vdash \Box A$}
% \AxiomC{$A^n, \Box A^n, \Delta, \Box \Delta \vdash B'$}
% \RightLabel{$(\textit{ctr}^*\vdash)$}
% \UnaryInfC{$A^n, \Box A, \Delta, \Box \Delta \vdash B'$}
% \RightLabel{(\textit{inductive cut})}
% \dashedLine
% \BinaryInfC{$A^n, \Box \Gamma, \Delta, \Box \Delta \vdash B'$}
% \RightLabel{$(\textit{ctr}^*\vdash)$}
% \UnaryInfC{$A, \Box \Gamma, \Delta, \Box \Delta \vdash B'$}
% \RightLabel{(\textit{inductive cut})}
% \dashedLine
% \BinaryInfC{$\Gamma, \Box \Gamma, \Box \Gamma, \Delta, \Box \Delta \vdash B'$}
% \RightLabel{$(\textit{ctr}^*\vdash)$}
% \UnaryInfC{$\Gamma, \Box \Gamma, \Delta, \Box \Delta \vdash B'$}
% \RightLabel{$(\vdash \Box)$ or $(\Box \vdash)$}
% \UnaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
% \end{prooftree}
% \end{center}

% Finally we combine these results to get the cut admissibility result,
% in terms of explicit derivation trees, and then in terms of derivability.
% \begin{verbatim}
% gtd_casdt: "(?dta, ?dtb) : casdt (lkxcss GTD) ?A" : Thm.thm
% gtd_cas: "(?cl, ?cr) : cas (lkxcss GTD) ?A" : Thm.thm 
% \end{verbatim}

\subsection{Calculus for GTD} \label{s-cut-gtdns}

We now look at proving cut admissibility for a version of GTD without structural
rules, where the box rules have their conclusions (only) 
extended with an arbitrary context, which permits weakening to be admissible.

We define the rules of the sequent calculus as follows.  The rules used for
classical logic (before extending them with a context) form the set
\texttt{lksne} where the rule sets \texttt{idrls}, \texttt{lksil} and
\texttt{lksir} are the axioms and the left and right logical
introduction rules: see Figure~\ref{S4:rules}.

\begin{definition}[\texttt{lkssx}]\label{def-lkssx}
  Given, a rule set \verb!xrls!, every rule of \verb!xrls! is in the
  rule set \verb!lkssx xrls!, and 
  every rule \verb!psc! in rule set \verb!lknse! gives a
  rule in \verb!lkssx xrls! obtained by uniformly extending 
  both the premise and conclusion of \verb!psc! with an arbitrary
  context (sequent) \verb!flr!:
\end{definition}
\begin{verbatim}
inductive "lkssx xrls" 
  intrs
      x  "psc : xrls ==> psc : lkssx xrls"
   extI  "psc : lksne ==> pscmap (extend flr) psc : lkssx xrls"
\end{verbatim}

\begin{definition}[\texttt{extcs}]\label{def-extcs}
Given a rule set \verb!rules!,
the rule set \verb!extcs rules! is obtained by extending only the
conclusion \verb!c! of each rule \verb!(ps, c)! in 
\verb!rules! by an arbitrary context (sequent) \verb!flr! (while
leaving the premises unchanged):
\end{definition}
\begin{verbatim}
inductive "extcs rules" 
  intrs
      I   "(ps, c) : rules ==> (ps, extend flr c) : extcs rules" 
\end{verbatim}

The rule set \texttt{lkssx (extcs GTD)} for GTD is obtained by
extending only the conclusion of the rule \verb!GTD! and by
extending every rule of \verb!lknse!.

\subsection{Weakening-admissibility for GTD}

First we prove weakening admissibility, using
a lemma which allows us to apply Lemma~\ref{l-ext-concl-wk}.

\begin{lemma} \label{l-extrs-cs}
For any rule sets \texttt{rls} and \texttt{rlsa} 
\begin{enumerate}
\item \texttt{extrs rlsa} $\cup$ \texttt{extcs rls} 
satisfies \texttt{ext\_concl}
\item \texttt{extrs rlsa} $\cup$ \texttt{extcs rls} 
satisfies weakening admissibility
\end{enumerate}
\begin{verbatim}
extrs_cs_ext_concl: "ext_concl (extrs ?rlsa Un extcs ?rls)"
wk_adm_extrs_cs: "wk_adm (extrs ?rlsa Un extcs ?rls)"
\end{verbatim}
\end{lemma}
\begin{proof}
The first is easy. The second follows using
Lemma~\ref{l-ext-concl-wk}.
\hfill
\end{proof}

\begin{corollary} \label{c-wk-adm-lkssx-extcs}
GTD satisfies weakening admissibility.
\begin{verbatim}
      wk_adm_lkssx_cs: "wk_adm (lkssx (extcs ?xrls))"
\end{verbatim}
\end{corollary}
\begin{proof}
Since the rule set \texttt{lkssx (extcs GTD)} for GTD is also equal to
\texttt{extrs lksne} $\cup$ \texttt{extcs GTD},
the result follows from Lemma~\ref{l-extrs-cs}.
\hfill
\end{proof}

\subsection{Inversion and Contraction-admissibility for GTD}

For contraction admissibility, first we need to prove invertibility of
the classical logical rules.  The general method for doing so was
described in \S\ref{s-s4-inv-ctr}.

Recall the predicate \texttt{inv\_stepm}, which is used in an
inductive proof of invertibility. Its three arguments are:
\begin{description}
\item[\texttt{drls}]
first, the set of \emph{derivation rules} with respect to which 
the invertibility (a case of admissibility) is defined,
\item[\texttt{irls}]
second, the set of rules whose invertibility is being considered 
  (the \emph{inversion rules})
\item[\texttt{(ps, c)}]
third, the \emph{final rule} of a derivation --- 
since we are talking about
proving the invertibility result by induction on the derivation, the
inductive hypothesis is that the invertibility result applies to the premises
\texttt{ps} of this final rule.
\end{description}

By Lemma~\ref{lemma:inv-stepm-monotonic}, \texttt{inv\_stepm}
(although not \texttt{inv\_step}) is monotonic in the derivation rules
argument. For its second argument the following holds.
\begin{lemma} \label{l-inv-stepm-union}
For a given set \texttt{drls} of derivation rules and a given final rule
\texttt{psc}, if \texttt{inv\_stepm} applies for inversion rule sets
\texttt{irlsa} and \texttt{irlsb}, then it applies for 
\texttt{irlsa} $\cup$ \texttt{irlsb}.
\end{lemma}

\begin{verbatim}
inv_stepm_Un:
"[| inv_stepm ?drls ?irlsa ?psc ; 
    inv_stepm ?drls ?irlsb ?psc |]
   ==> inv_stepm ?drls (?irlsa Un ?irlsb) ?psc"
\end{verbatim}

So far as the third argument is concerned, 
the requirement to prove a rule is invertible is simply that 
\texttt{inv\_stepm \ldots} applies for all cases of the third argument
(see Lemmas \ref{lemma:inv-from-inv-step} and
\ref{lemma:inv-step-from-inv-stepm}): 
thus the lemmata we use are expressed to apply to single cases of the third
argument.

We now describe the lemmata used as building-blocks for the required
invertibility result.

\begin{lemma} \label{inv_stepm-lemmas}~\\
\begin{enumerate}
\item \texttt{inv\_stepm \ldots} applies where the
derivation rules and the set of rules to be inverted are 
the classical logical rules \texttt{extrs lksne}, 
and the final rule is any one of those rules
\begin{verbatim}
lks_inv_stepm: 
   "?psc : extrs lksne ==>
     inv_stepm (extrs lksne) (extrs lksne) ?psc"
\end{verbatim}
\item \label{inv-stepm-disj}
  where the set of inversion rules is the set of extensions of
a single skeleton whose conclusion is \texttt{ic}, and
the set of derivation rules is the set of extensions of
a single skeleton rule whose conclusion is \texttt{c}, 
and these skeleton conclusions 
\texttt{ic} and \texttt{c} are disjoint
(ie, have no formula in common on the same side of the turnstile),
and the final rule is one of those derivation rules, then 
\texttt{inv\_stepm \ldots} applies
\begin{verbatim}
inv_stepm_disj:
  "[| seq_meet ?c ?ic = 0 ; 
      extrs {(?ps, ?c)} = ?rls ; ?rl : ?rls |] 
     ==> inv_stepm ?rls (extrs {(?ips, ?ic)}) ?rl"
\end{verbatim}
\item \label{inv-stepm-disj-cs}
as for \ref{inv-stepm-disj}, except that the set of derivation rules
is the set of extensions in the conclusion only (using \texttt{extcs}) 
of the single skeleton
\begin{verbatim}
inv_stepm_disj_cs: 
"[| seq_meet ?c ?ic = 0 ; 
    extcs {(?ps, ?c)} = ?rls ; ?rl : ?rls |]
   ==> inv_stepm ?rls (extrs {(?ips, ?ic)}) ?rl" 
\end{verbatim}
\item \label{inv-stepm-scrls}
  where the set of inversion rules 
and the set of derivation rules are each the set of extensions of
a single skeleton rule whose conclusion has a single formula,
and if those two skeletons' conclusions are equal
then the two skeletons are equal,
then \texttt{inv\_stepm \ldots} applies
\begin{verbatim}
inv_stepm_scrls:
"[| extrs {?srl} = ?rls ; ?rl : ?rls ;
    ?srl : scrls ; ?irl : scrls ;
    snd ?srl = snd ?irl --> ?srl = ?irl |] 
  ==> inv_stepm ?rls (extrs {?irl}) ?rl"
\end{verbatim}
\end{enumerate}
\end{lemma} 

Parts \ref{inv-stepm-disj} and \ref{inv-stepm-disj-cs}
  (\texttt{inv\_stepm\_disj} and \texttt{inv\_stepm\_disj\_cs})
are for the case where the principal formula 
of the rule to be inverted is in the context of 
the conclusion of the last rule of the derivation:
the first premise gives us that the formula to be inverted is
not the principal formula of the rule, though it is expressed in a way 
which is relevant to a case where the rules in question have more than just one
principal formula.

Part \ref{inv-stepm-scrls} (\texttt{inv\_stepm\_scrls}),
whose proof uses part \ref{inv-stepm-disj},
uses the fact that for each formula involved there
are unique introduction rules for the left and right sides of $\vdash$,
so an inversion step is either
parametric or gives us the premise(s) of the last rule applied.

%gtdns_inv_rl: "Ball (extrs lksne) (inv_rl (lkssx (extcs GTD)))" 
\begin{lemma}
  Every rule of \verb!lksss! is invertible in the calculus for GTD.
\end{lemma}
\begin{verbatim}
gtdns_inv_rl: "Ball (extrs lksne) (inv_rl (lkssx (extcs GTD)))" 
\end{verbatim}

\begin{proof}
This uses Lemmas \ref{lemma:inv-from-inv-step},
\ref{lemma:inv-step-from-inv-stepm} and \ref{inv_stepm-lemmas}.  
\end{proof}

Then, to prove contraction admissibility, we follow an approach very similar
to \S\ref{s-s4-inv-ctr}. 
For the rules ($\Box\vdash$) and ($\vdash\Box$), the proof for the cases
where either of these is the final rule is just the same as for the 
S4$\Box$ rule in \S\ref{s-s4-inv-ctr}.
%Thus we get the result
\begin{lemma} \label{l-gtd-ctr}
Contraction is admissible in GTD.
\end{lemma}
\begin{verbatim}
          gtdns_ctr_adm: "ctr_adm (lkssx (extcs GTD)) ?A"
\end{verbatim}

\comment{ requires too much explanation
MOVE THIS TO \S\ref{s-s4-inv-ctr} ??

We used a useful and quite general lemma 
to handle the case where at least one of the copies of the formula to be
contracted arises from the extension of the conclusion of the box rule.

\begin{verbatim}
ctxt_ctr_adm_step1_cs: "[| pg_meet ?concl (?As + ?As) <= ?As;
  ?rl = (?ps, ?concl); (?ps, extend ?flr ?concl) = ?erl;
  extcs {?rl} <= ?rules |] ==> ctr_adm_step1 (derrec ?rules {}) ?erl ?As"
\end{verbatim}

\texttt{ctr\_adm\_step1} is a simplified version of \texttt{ctr\_adm\_step},
without the inductive hypothesis relating to smaller formulae.
}

\subsection{Cut-admissibility for GTD}

Now, for cut admissibility, the difficult cases are where the last rule on both
sides is one of the two box rules ($\vdash\Box$) and ($\Box\vdash$):
$$
\frac{\wbx\Gamma,  \Gamma \vdash B}
  {\Sigma, \Box \Gamma \vdash \Box B, \Delta} (\vdash\Box)
\qquad\qquad\qquad
\frac{\wbx\Gamma,  \Gamma \vdash \Box B}
  {\Sigma, \Box \Gamma \vdash \Box B, \Delta} (\Box\vdash)
$$

Since the proof is effectively the same whichever of these two rules is on the
right, we define a unary function \texttt{s4g .} such that 
\begin{itemize}
\item 
\texttt{s4g} $(\lambda B.\ \{B, \Box B\})$
  is all instances of either $(\vdash\Box)$ or $(\Box\vdash)$,
\item 
\texttt{s4g} $(\lambda B.\ \{B\})$ is all instances of $(\vdash\Box)$, and 
\item 
\texttt{s4g} $(\lambda B.\ \{\Box B\})$ is all instances of $(\Box\vdash)$
\end{itemize}
where the function \texttt{prs B} encapsulates the choices of $B$
and/or $\Box B$, as required and where 
\verb!s4g prs! below encodes only the skeletons of the rules above: 
see the definition of GTD at the start of \ref{s-gtd}.  Formally,

\begin{definition}[\texttt{s4g}] \label{d-s4g}
\texttt{s4g prs} is the set of instances of the following rule 
where $A \in \texttt{prs} B$:
$$
\frac{\wbx\Gamma,  \Gamma \vdash A}
  {\Box \Gamma \vdash \Box B} 
$$
\end{definition}
\begin{verbatim}
inductive "s4g prs"
  intrs I "A : prs B ==>
                     ([mset_map Box X + X |- {#A#}],
                       mset_map Box X |- {#Box B#}) : s4g prs"
\end{verbatim}

The case of the ($\vdash\Box$) rule on the left is dealt with in
\S\ref{s-s4-cut}: depending on whether we have the
rule ($\vdash\Box$) or ($\Box\vdash$) on the right, we may need to change
$B$ to $\Box B$ in the diagrams there.

For the case where we have the ($\Box\vdash$) rule on the left,
the original derivation is as in the following diagram,
where $B'$ is $B$ or $\Box B$.
\begin{center}
\AxiomC{$\Pi_l$}
\noLine
\UnaryInfC{$\Gamma_L, \wbx \Gamma_L \vdash \Box A$}
\LeftLabel{$\Box\vdash$}
\UnaryInfC{$\Sigma_L, \wbx \Gamma_L \vdash \Delta_L, \wbx A$}
    \AxiomC{$\Pi_r$}
    \noLine
    \UnaryInfC{$A, \wbx A, \Gamma_R, \wbx \Gamma_R \vdash B'$}
    \LeftLabel{$\Box\vdash$ or $\vdash\Box$}
    \UnaryInfC{$\wbx A, \Sigma_R, \wbx \Gamma_R \vdash \wbx B, \Delta_R$}
\LeftLabel{Cut on $\wbx A$}
\BinaryInfC{$\Sigma_L, \Sigma_R, \wbx \Gamma_L, \wbx \Gamma_R \vdash
  \wbx B, \Delta_L, \Delta_R$}
\DisplayProof
\end{center}

As in \S\ref{s-s4-cut}, we modify the original derivation of a premise,
in this case the right premise, by simply not adding any context in the
conclusion.  This produces a derivation of equal height
upon which we can still apply the induction hypothesis on level.
Formally,
the $\Sigma$ and $\Delta$ of the generic 
box rule ($\vdash\Box$) or ($\Box\vdash$)
are $\emptyset$ in the new instance below:
\begin{center}
\AxiomC{$\Pi_l$}
\noLine
\UnaryInfC{$\Gamma_L, \wbx \Gamma_L \vdash \Box A$}
\AxiomC{$\Pi_r$}
\noLine
\UnaryInfC{$A, \wbx A, \Gamma_R, \wbx \Gamma_R \vdash B'$}
    \RightLabel{$\Box\vdash$ or $\vdash\Box$ (new)}
\UnaryInfC{$\wbx A, \wbx \Gamma_R \vdash \Box B$}
            \RightLabel{Cut on $\wbx A$}
\BinaryInfC{$\Gamma_L, \wbx \Gamma_L, \wbx \Gamma_R \vdash \Box B$}
    \RightLabel{Weakening-admissibility}
    \dashedLine
\UnaryInfC{$\Gamma_L, \wbx \Gamma_L, \Gamma_R, \wbx \Gamma_R \vdash \Box B$}
    \RightLabel{$\Box\vdash$}
\UnaryInfC{$\Sigma_L, \Sigma_R, \wbx \Gamma_L, \wbx \Gamma_R \vdash
  \wbx B, \Delta_L, \Delta_R$}
\DisplayProof
\end{center}

\comment{
OMIT? This gives the result \texttt{gtd\_box\_box\_lem} below.

OMIT THESE?
\begin{verbatim}
s4_box_box_lem:
   "[| ?prsl = (%B. {B}); wk_adm ?drls; All (ctr_adm ?drls);
         extcs (s4g ?prsl) <= ?drls; extcs (s4g ?prsr) <= ?drls;
         (map conclDT ?dtll, ?cl) : extcs (s4g ?prsl);
         (map conclDT ?dtlr, ?cr) : extcs (s4g ?prsr) |]
      ==> sumh_step2_tr (prop2 casdt ?drls) ?A ipsubfml
       (Der ?cl ?dtll, Der ?cr ?dtlr)" 

gtd_box_box_lem:
   "[| ?prsl = (%B. {Box B}); wk_adm ?drls; All (ctr_adm ?drls);
         extcs (s4g ?prsl) <= ?drls; extcs (s4g ?prsr) <= ?drls;
         (map conclDT ?dtll, ?cl) : extcs (s4g ?prsl);
         (map conclDT ?dtlr, ?cr) : extcs (s4g ?prsr) |]
      ==> sumh_step2_tr (prop2 casdt ?drls) ?A ipsubfml
       (Der ?cl ?dtll, Der ?cr ?dtlr)" 
\end{verbatim}
}

For the cut-elimination proof we also use results for the 
parametric cases, that is, where the cut-formula appears in the context of the
last rule on either side above the cut.
This includes cases where that rule is in \texttt{extrs} \ldots 
(where the rule has a context which appears in premises and conclusion)
and where that rule is in \texttt{extcs} \ldots 
(where the rule has a context which appears only in the conclusion).

The following lemma is used for the common situation of a cut which is
parametric with respect to the last rule of the left-hand derivation.

\begin{lemma}[\texttt{lcg\_gen\_step}] \label{l-param-step}
Consider a set \texttt{erls} of derivation rules,
for which weakening is admissible, and which contains all extensions 
of a skeleton rule $\rho$ with premises \texttt{ps} and conclusion 
$U \vdash V$.
Consider two derivations of which the final rule of the left side 
is an extension of $\rho$.
Then for a cut-formula $A$ which is not contained in $V$, 
and any subformula relation \texttt{sub},
the inductive step condition \texttt{gen\_step2\_sr \ldots} holds for the
admissibility of a cut on $A$.
\end{lemma}
\begin{verbatim}
lcg_gen_step:
  "[| wk_adm ?erls ; 
      extrs {(?ps, ?U |- ?V)} <= ?erls ; 
      ~ ?A :# ?V ;
      ?pscl = pscmap (extend (?W |- ?Z)) (?ps, ?U |- ?V) |] 
    ==> 
    gen_step2sr (prop2 car ?erls) ?A ?sub ?erls (?pscl, ?pscr)"
\end{verbatim}

A similar lemma \texttt{lcg\_gen\_steps\_extcs}
holds for the case where only extensions in the conclusion of
$\rho$ are contained in \texttt{erls}.

\begin{verbatim}
lcg_gen_steps_extcs:
   "[| wk_adm ?rls ; 
       extcs {(?ps, ?c)} <= ?rls ; ~ ?A :# succ ?c |] 
     ==> gen_step2sr (prop2 car ?rls) ?A ?sub ?rls
                     ((?ps, extend ?flr ?c), ?psr, ?cr)"
\end{verbatim}

Finally we need to deal with the cases of matching instances of the usual
logical introduction rules.
Here we use a general result giving requirements for certain cases of the
final rules on either side of a putative cut to satisfy the step condition 
for cut-admissibility.

It uses a property \texttt{c8\_ercas\_prop}, which encodes the property that a
cut which is principal (ie, the cut formula is introduced by a
logical introduction rule in the final step) on both sides
is reducible to cuts on sub-formulae.
It is loosely defined as follows:

\begin{definition}[\texttt{c8\_ercas\_prop}] \label{d-c8-ercas-prop}
Given a set of derivation rules \texttt{prls},
a cut-formula $A$, a subformula relation \texttt{psubfml}, 
and a set of skeleton rules (typically logical introduction rules)
\texttt{rls}, \\
\texttt{c8\_ercas\_prop psubfml prls A rls}
means: \\
assuming that we have cut-admissibility for cut-formulae 
which are smaller than $A$ according to \texttt{psubfml},
where two derivations have as their final sequents
$X_l \vdash A, Y_l$ and $X_r, A \vdash Y_r$, and on both sides 
the final rule introduces $A$ using logical introduction rules in \texttt{rls},
then $X_l, X_r \vdash Y_l, Y_r$ is derivable,
that is, the cut on $A$ is admissible. 
\end{definition}

Of course, whether \texttt{c8\_ercas\_prop} holds depends on the
specific set of logical rules. Beyond that, however, the
following lemma is quite general.

\begin{lemma} \label{l-gs2sr-alle}
Given a set of derivation rules \texttt{drls},
a cut-formula $A$, and a subformula relation \texttt{psubfml}, if
\begin{itemize}
\item \texttt{drls} satisfy weakening admissibility
\item there is a set \texttt{rls} of skeleton rules all of whose extensions are
contained in \texttt{drls}
\item all rules in \texttt{rls}, other than axiom rules $B \vdash B$,
  have a single formula in their conclusion
\item the axiom rules are also in \texttt{drls}
\item \texttt{drls} and \texttt{rls} satisfy \texttt{c8\_ercas\_prop}
\item the final rules of two derivations are extensions of rules in
\texttt{rls}
\end{itemize}
then the step condition \texttt{gen\_step2sr} for cut-admissibility for the two
derivations is satisfied.
\end{lemma}
\begin{verbatim}
gs2sr_alle:
  "[| wk_adm ?drls ; 
      c8_ercas_prop ?psubfml ?drls ?A ?rls ;
      ?rls <= iscrls ; 
      idrls <= ?drls ; 
      extrs ?rls <= ?drls ;
      (?psa, ?ca) : extrs ?rls ; 
      (?psb, ?cb) : extrs ?rls |] 
    ==> gen_step2sr (prop2 car ?drls) ?A ?psubfml ?drls 
                    ((?psa, ?ca), ?psb, ?cb)"
\end{verbatim}

\comment{
This theorem (which incorporates the parametric cases) uses 
\texttt{c8\_ercas\_prop} which says essentially
that if both sides of the cut are logical introduction rules,
and cut is admissible on smaller cut-formulae,
then the cut in question is admissible.

(LATER - on looking back at the previous section I find the result
\texttt{gprstep\_q} shown -
basically that result plus the case of the axiom rules gives us
\texttt{gen\_lksne\_c8sg} below)

Omitting the definition of \texttt{c8\_ercas\_prop},
here is the theorem which uses it:

\begin{verbatim}
c8_ercas_gs2: "[| c8_ercas_prop ?psubfml ?drls ?A ?c8rls;
  ?prl = (?ps, 0 |- {#?A#}); ?prl : ?c8rls;
  ?qrl = (?qs, {#?A#} |- 0); ?qrl : ?c8rls;
  ?eprl = pscmap (extend ?pe) ?prl; ?eqrl = pscmap (extend ?qe) ?qrl |] ==>
  gen_step2sr (prop2 car ?drls) ?A ?psubfml ?drls (?eprl, ?eqrl)"
\end{verbatim}
end comment }

We apply this result to the logic GTD using first another general result

\begin{lemma}[\texttt{gen\_lksne\_c8}] \label{l-gen-lksne-c8}
If a set of derivation rules \texttt{drls} satisfies weakening admissibility 
and contraction admissibility, and contains the extensions of the logical
introduction rule skeletons \texttt{lksne} then the condition
\texttt{c8\_ercas\_prop} is satisfied 
(for the usual immediate proper subformula relation and for any cut-formula).
\end{lemma}

\begin{verbatim}
gen_lksne_c8: 
   "[| ALL A'. ctr_adm ?drls A' ; 
       wk_adm ?drls ; extrs lksne <= ?drls |] 
     ==> c8_ercas_prop ipsubfml ?drls ?A lksne" 
\end{verbatim}

\begin{corollary}[\texttt{gtdns\_lksne\_c8}] \label{c-gtdns-lksne-c8}
GTD satisfies \texttt{c8\_ercas\_prop} in relation to the 
logical introduction rule skeletons \texttt{lksne}.
\end{corollary}

\begin{verbatim}
gtdns_lksne_c8:
     "c8_ercas_prop ipsubfml (lkssx (extcs GTD)) ?A lksne" 
\end{verbatim}

Finally we get the cut admissibility result.
Here, \texttt{mins} $A\ M$ means multiset $M$ with one additional copy
of $A$ inserted.

\begin{theorem}[\texttt{gtdns\_casdt, gtdns\_cas}] \label{t-GTD-ca}
GTD satisfies cut-admissibility.
\end{theorem}

\begin{verbatim}
gtdns_casdt: "(?dt, ?dta) : casdt (lkssx (extcs GTD)) ?A" 

  gtdns_cas: "(?Xl |- mins ?A ?Yl, mins ?A ?Xr |- ?Yr) :
                              cas (lkssx (extcs GTD)) ?A"
\end{verbatim}

\section{Weakening, Contraction and Cut Admissibility 
  for Dynamic Topological Logic S4C}\label{s-s4cns}

We  now describe Isabelle proofs of the
cut admissibility of the logic S4C described by Mints~\cite{mints-jaegerfest}.
%
This system has two ``modal'' operators, $\Box$ and $\circ$.
The $S4$-axioms hold for $\Box$, $\circ$ commutes with the boolean operators,
and the following are given:
\begin{align*}
\circ (A \to B) & \leftrightarrow (\circ A \to \circ B) \\
\circ \bot & \leftrightarrow \bot \\
\circ \Box A & \to \Box \circ A
\end{align*}

The following sequent rules are given for S4C by Mints \cite{mints-jaegerfest}
$$
\frac{\circ^k A, \Gamma \vdash \Delta, \circ^k B}
  {\Gamma \vdash \Delta, \circ^k (A \to B)}(\vdash\to)
\qquad
\frac{\Gamma \vdash \Delta, \circ^k A \quad \circ^k B, \Gamma \vdash \Delta}
  {\circ^k (A \to B), \Gamma \vdash \Delta}(\to\vdash)
$$
$$
\frac{\circ^k A, \Gamma \vdash \Delta}
  {\circ^k \Box A, \Gamma \vdash \Delta}(\Box\vdash)
\qquad
\frac{\Gamma \vdash \Delta}
  {\circ \Gamma \vdash \circ \Delta}(\circ)
\qquad
\frac{\mathcal B \vdash A}{\mathcal B \vdash \Box A}(\vdash\Box)
$$

In the $(\vdash\Box)$ rule, $\mathcal B$ must consist of 
``$\Box$-formulae'', that is, formulae of the form $\circ^k \Box A$.

As Mints omits the other logical operators, 
we include, for them, the usual logical introduction rules
with the principal and side formulae preceded by $\circ^k$ just 
as with the $(\vdash\to)$ and $(\to\vdash)$ rules shown above.

% The property we will prove inductively is mix (rather than cut) admissibility.
Our version of the calculus 
contains no explicit structural rules, so
we prove invertibility of the logical rules and contraction
admissibility. The presence of the $(\circ)$ rule makes the proof
more complicated and is handled similarly 
to our handling of contraction in proving cut admissibility for GTD.

As we have no structural rules,
we use a presentation of the system which 
\begin{itemize}
\item allows an arbitrary context to be added to the conclusion (only) of the
$(\vdash \Box)$ and $(\circ)$ rules
\item uses a version of the $(\Box \vdash)$
rule which includes the principal formula in the premise
\end{itemize}

$$
\frac{\Gamma \vdash \Delta}
  {\Sigma, \circ \Gamma \vdash \circ \Delta, \Pi}(\circ)
\qquad
\frac{\mathcal B \vdash A}{\Gamma, \mathcal B \vdash \Box A, \Delta}
  (\vdash\Box)
\qquad
\frac{\circ^k \Box A, \circ^k A, \Gamma \vdash \Delta}
  {\circ^k \Box A, \Gamma \vdash \Delta}(\Box\vdash)
$$

\subsection{Calculus for S4C}

We now describe how we encoded the sequent calculus.
First we define the rules which can be extended by an arbitrary context
in their premises and conclusion.
Without the context, these rules form the set \texttt{s4cnsne}.

Applying \texttt{nkmap} $k$ to a rule applies $\circ^k$ to each formula
appearing in that rule, and \texttt{funpow} $f\ x$ means applying 
$f$ to $x$, $n$ times, i.e., $f^n(x)$.

\begin{verbatim}
inductive "s4cnsne"
  intrs
       id  "psc : idrls ==> psc        : s4cnsne"
  circ_il  "rl : lksil ==> nkmap k rl  : s4cnsne"
  circ_ir  "rl : lksir ==> nkmap k rl  : s4cnsne"
   circ_T  "rl : lkrefl ==> nkmap k rl : s4cnsne"

inductive "lkrefl" 
  intrs
  I  "([{#A#} + {#Box A#} |- {#}], {#Box A#} |- {#}) : lkrefl"

defs
  nkmap_def : "nkmap k == pscmap (seqmap (funpow Circ k))"

inductive "s4cns"
 intrs
   extI "rl : s4cnsne ==> pscmap (extend (U |- V)) rl : s4cns"
 extcsI "(ps, c) : circ Un s4cbox ==>
                              (ps, extend (U |- V) c) : s4cns"

inductive "circ"
  intrs
       I "([seq], seqmap Circ seq) : circ"

inductive "s4cbox"
  intrs
      boxI "M : msboxfmls ==> ([M |- {#A#}], 
                                M |- {#Box A#}) : s4cbox"

inductive "msboxfmls"
  intrs
      I "ALL f. f :# M --> f : boxfmls ==> M : msboxfmls"

inductive "boxfmls"
  intrs
      I "funpow Circ k (Box B) : boxfmls"
\end{verbatim}

We first prove the admissibility of weakening and
contraction.
% QUESTION - we did prove contraction admissibility, but is it essential?

\subsection{Weakening for S4C}

Weakening admissibility was straightforward using Lemma~\ref{l-ext-concl-wk}.

\subsection{Inversion and Contraction-admissibility for S4C}

Invertibility of the logical introduction rules was dealt with using multiple
lemmata showing various cases of \texttt{inv\_stepm}, as described in
\S\ref{s-s4-inv-ctr}: as noted there,
a proof of invertibility can be split up into 
\begin{itemize}
\item the invertibility of various different rules 
\item cases of what the last rule in the derivation, 
from whose conclusion we wish to apply one of the inverted rules
\end{itemize}
As in \S\ref{s-s4-inv-ctr}, we make significant use of 
Lemma~\ref{lemma:inv-stepm-monotonic}.

We then prove contraction admissibility.
This uses predicates and results which are essentially
Definition~\ref{d-gen-step} and Lemma~\ref{genstep:lem},
but instantiated to apply to the property of contraction admissibility,
giving the property \texttt{ctr\_adm\_step} and a lemma
\texttt{gen\_ctr\_adm\_step}.

\comment{
The formalisation performs the necessary transformations
using a simple instantiation \texttt{gen\_ctr\_adm\_step} (not shown)
of the induction principle \texttt{gen\_step\_lem} of
Theorem~\ref{genstep:lem}.
MENTIONED AT \ref{t-gs4-ctr-adm} --- SHOULD THIS GO THERE?
PROPOSE TO DELETE THESE DETAILS

\begin{verbatim}
gen_ctr_adm_step: 
   "[| ?A : wfp ?sub;
       ALL dt. ALL (ps, concl) : ?rules.
               ctr_adm_step ?sub (derrec ?rules {}) (ps, concl) dt |]
      ==> ctr_adm ?rules ?A" 

ctr_adm_step_eq: 
   "ctr_adm_step ?sub ?derivs (?ps, ?concl) ?A =
    (ALL As.  ms_of_seq As = {#?A#} -->
    (ALL A'.  (A', ?A) : ?sub --> (ALL As.  ms_of_seq As = {#A'#} -->
      (ALL XY.  XY : ?derivs --> As + As <= XY --> XY - As : ?derivs))) -->
    (ALL p:set ?ps. p : ?derivs & (As + As <= p --> p - As : ?derivs)) -->
    As + As <= ?concl --> ?concl - As : ?derivs)"
\end{verbatim}
}

We now look at proving \texttt{ctr\_adm\_step} for each possible case for
the last rule of a derivation.

\begin{lemma} \label{l-gen-ctr-adm-step-inv}
If 
\begin{itemize}
\item rule set $lrls$ consists of rules
   which are the identity (axiom) rules $A \vdash A$,
   or are rules with a single formula in their conclusion,
\item all rules in $lrls$ have the ``subformula'' property 
  (which here means that for every premise \emph{other than a premise which
contains the conclusion}, every formula in that premise is a subformula of a
formula in the conclusion
\item the rule set $drls$ (derivation rules) contains the extensions of $lrls$
\item in regard to the derivation rules $drls$, the inverses of extensions of
$lrls$ are admissible
\item rule $(ps, c)$ is an extension of a rule of $lrls$
\end{itemize}
then the contraction admissibility step \texttt{ctr\_adm\_step}
 holds for the final rule $(ps, c)$ and the derivation rule set $drls$.
\end{lemma}
So the conclusion of this lemma means: assuming that
\begin{itemize}
\item contraction on formulae $A'$ smaller than $A$ is admissible, and 
\item contraction on $A$ is admissible in the sequents $ps$
\end{itemize}
 then contraction on $A$ in sequent $c$ is admissible.  

\begin{verbatim}
gen_ctr_adm_step_inv:
   "[| ?epsc : extrs ?lrls ; 
       ?lrls <= iscrls ; 
       extrs ?lrls <= ?drls ;
       Ball ?lrls (subfml_cp_prop ?sub) ;
       Ball (extrs ?lrls) (inv_rl ?drls) |] 
     ==> ctr_adm_step ?sub (derrec ?drls {}) ?epsc ?A"

subfml_cp_prop.simps:
   "subfml_cp_prop sub (ps, c) =
      (ALL p:set ps. c <= p 
       | (ALL fp. ms_mem fp p -->
          (EX fc. ms_mem fc c & (fp, fc) : ub)))" 
\end{verbatim}

Then the other cases of \texttt{ctr\_adm\_step} were proved separately:

\begin{lemma} \label{l-s4c-ctr-box-circ}
In S4C, for derivations with final rules $(\vdash \Box)$ and $(\circ)$
(extended in their conclusions), the 
inductive contraction admissibility step \texttt{ctr\_adm\_step} holds.
\end{lemma}

\begin{verbatim}
ctr_adm_step_s4cbox_r:
  "[| (?ps, ?c) : extcs s4cbox ; extcs s4cbox <= ?drls |]
     ==> ctr_adm_step ?sub (derrec ?drls {}) (?ps, ?c) ?A"

ctr_adm_step_circ_r:
  "[| (?ps, ?c) : extcs circ ; extcs circ <= ?drls |]
     ==> ctr_adm_step ipsubfml (derrec ?drls {}) (?ps, ?c) ?A"
\end{verbatim}

Consequently, we get contraction admissibilty.  
The only case not covered above is for the reflexivity rule $(\Box\vdash)$,
in its form where the principal formula is copied to the premise.
This is required for contraction admissibility, which becomes simple 
with the rule in this form.

\begin{lemma}[\texttt{s4cns\_ctr\_adm}] \label{l-s4c-ctr}
Contraction is admissible in GTD.
\end{lemma}
\begin{verbatim}
     s4cns_ctr_adm: "ctr_adm s4cns ?A"
\end{verbatim}

\subsection{Cut-admissibility for S4C} \label{s-s4c-cut}

To prove cut admissibility for a sequent calculus containing an explicit
contraction rule, two methods are
\begin{itemize}
\item to prove mix-elimination directly, where the property proved by
induction on the derivation is that any instance of the mix rule is admissible;
in effect this was done in \cite{dawson-gore-generalised} for the more 
complex logic GLS,
\item in respect of the derivations on either side of the cut, to 
look up the derivation skipping over consecutive instances of contraction on
the cut-formula, and consider the various cases of the next rule on either
side above those contractions.
\end{itemize}

We do something similar to the second approach here, but we look up the
derivations on either side to find the last rule before a consecutive
sequence of $(\circ)$ rules.
For this we use the theorem \texttt{top\_circ\_ns}.
In some cases we also need the fact that if the bottom rule is not $(\circ)$,
then the tree asserted to exist is actually the original one.
The function \texttt{forget} exists simply to prevent automatic case splitting
of its argument: logically it does nothing.

\begin{lemma}[\texttt{top\_circ\_ns}] \label{l-top-circ-ns}
Given a valid (explicit) derivation tree \texttt{dt}, then 
there is a valid (explicit) tree \texttt{dtn} and an integer $k$ such that
\begin{itemize}
\item the bottom rule of \texttt{dtn} is not $(\circ)$, 
\item the conclusions $c$ and $c'$ of \texttt{dt} and \texttt{dtn}
  are related by $c = \circ^k c'$
\item height of \texttt{dt} = height of \texttt{dtn} $ + k$
\item \texttt{dt} and \texttt{dtn} iff $k = 0$ iff the bottom rule of 
   \texttt{dt} is not $(\circ)$
\end{itemize}
\end{lemma}

\begin{verbatim}
top_circ_ns: 
   "valid ?rls ?dt 
    ==> EX dtn k.
          botRule dtn ~: extcs circ & valid ?rls dtn 
        & seqmap (funpow Circ k) (conclDT dtn) <= conclDT ?dt 
        & heightDT ?dt = heightDT dtn + k 
        & forget ((k = 0) = (botRule ?dt ~: extcs circ) 
        & (k = 0) = (dtn = ?dt))"

forget_def: "forget f == f"
\end{verbatim}

But one easy case is where the last rule on \emph{both} sides is the $(\circ)$
rule: then we can apply cut (on a smaller formula) to the premises of the
$(\circ)$ rules, and then apply the $(\circ)$ rule.
So when we look at the $(\circ)$ rules on both sides immediately preceding the
cut, we need only bother about the case where the number of those 
$(\circ)$ rules is zero on one side.

First, the case where both rules are the $(\vdash\Box)$ rule.
The fact that the conclusions of both the $(\circ)$ rule and the $(\vdash\Box)$ 
rule may be extended by an arbitrary context complicates matters.
Consider the following diagram of a number of $(\circ)$ rules followed by the
$(\vdash\Box)$ rule.
\begin{center}
\begin{prooftree}
\AxiomC{$\M \vdash A$}
\RightLabel{$(\vdash\Box)$}
\UnaryInfC{$\Gamma, \M \vdash \Box A, \Delta$}
\RightLabel{$(\circ^*)$}
\UnaryInfC{$\Gamma', \circ^k \Gamma, \circ^k \M \vdash 
  \circ^k \Box A, \circ^k \Delta, \Delta'$}
\end{prooftree}
\end{center}

In this case we can instead construct the following derivation tree,
which is of the same height.
\begin{center}
\begin{prooftree}
\AxiomC{$\M \vdash A$}
\RightLabel{$(\vdash\Box)$}
\UnaryInfC{$\M \vdash \Box A$}
\RightLabel{$(\circ^*)$}
\UnaryInfC{$\circ^k \M \vdash \circ^k \Box A$}
\end{prooftree}
\end{center}
Thus we can use, in proving an inductive step, the fact that
$\circ^k \M \vdash \circ^k \Box A$ is derivable, and with a derivation
of the same height as that of $\Gamma', \circ^k \Gamma, \circ^k \M \vdash 
  \circ^k \Box A, \circ^k \Delta, \Delta'$.
This will be used in our proofs without further comment.

Now, where the cut-formula is within $\circ^k \Delta, \Delta'$
(where this is the derivation tree on the left of a desired cut),
or within $\Gamma', \circ^k \Gamma$ (where this tree is on the right),
the cut is admissible because we can
start from the derivable sequent $\M \vdash A$ and apply $(\vdash\Box)$ and 
$\circ$ rule without any extra formulae in the conclusions, as discussed above.
In this case we just use weakening admissibility
to obtain the result of the cut.

These situations are covered by Lemma~\ref{l-s4cns-cs-param-l} 
(\texttt{s4cns\_cs\_param\_l''}) below and the symmetric
result \texttt{s4cns\_cs\_param\_r''}.

\begin{lemma} \label{l-s4cns-cs-param-l}
Let the left premise subtree of a desired cut be \texttt{dt},
with \texttt{dtn} and $k$ as in Lemma~\ref{l-top-circ-ns},
let the bottom rule of \texttt{dtn} be an extension (of the conclusion) of  
a rule in \texttt{s4cns} whose conclusion is $cl \vdash cr$,
and let $C$ not be in $\circ^k cr$.
Then the inductive step \texttt{sumh\_step2\_tr} for proving cut-admissibility
with cut-formula $C$ holds
(where \verb!list! and \verb!lista! are names automatically generated
by Isabelle for the lists of premises of final rules).
\end{lemma}
\begin{verbatim}
s4cns_cs_param_l'':
   "[| (?ps, ?cl |- ?cr) : s4cns ; valid s4cns ?dtn ;
       botRule ?dtn : extcs {(?ps, ?cl |- ?cr)} ;
       count (mset_map (funpow Circ ?k) ?cr) ?C = 0 |]
      ==> sumh_step2_tr (prop2 casdt s4cns) ?C ?sub 
                        (Der (seqmap (funpow Circ ?k) 
                             (conclDT ?dtn) + ?flr) ?list,
                         Der ?dtr ?lista)" 
\end{verbatim}

A similar pair of results, discussed later (see Lemma~\ref{l-s4cns-param-l}),
covers the case where the rule above the $(\circ)$
rules is a skeleton rule which is extended by an arbitrary context in its
conclusion \emph{and} its premises.  

Now we can assume that the cut-formula is within the principal part of the 
rule before the $(\circ)$ rules (noting that for the $(\vdash\Box)$ rule
the ``principal part'' means the entire $\M \vdash \Box A$).
Then there must be zero $(\circ)$ rules on the right side:
because if there are zero $\circ$ rules on the left,
then the cut-formula must be $\Box A$, whence
there would also be zero $(\circ)$ rules on the right.

In the diagrams, \textit{(cut ?)} represents the instance of the cut rule which
we are aiming to show is admissible.
\begin{center}
\begin{prooftree}
\AxiomC{$\M \vdash A$}
\RightLabel{$(\vdash\Box)$}
\UnaryInfC{$\Gamma, \M \vdash \Box A, \Delta$}
\RightLabel{$(\circ^*)$}
\UnaryInfC{$\Gamma', \circ^k \Gamma, \circ^k \M \vdash 
  \circ^k \Box A, \circ^k \Delta, \Delta'$}
\AxiomC{$\circ^k \Box A, \M' \vdash B$}
\RightLabel{$(\vdash\Box)$}
\UnaryInfC{$\Gamma'', \circ^k \Box A, \M' \vdash \Box B, \Delta''$}
\RightLabel{(\textit{cut ?})}
\dashedLine
\BinaryInfC{$\Gamma', \circ^k \Gamma, \Gamma'', \circ^k \M, \M' \vdash
  \Box B, \circ^k \Delta, \Delta', \Delta''$}
\end{prooftree}
\end{center}

Here we do the cut, by induction, before the $(\vdash\Box)$ rule on the right, 
using a derivation similar to that on the left, but without any context,
then we apply the $(\vdash\Box)$ rule, introducing the required context.
\begin{center}
\begin{prooftree}
\AxiomC{$\M \vdash A$}
\RightLabel{$(\vdash\Box)$}
\UnaryInfC{$\M \vdash \Box A$}
\RightLabel{$(\circ^*)$}
\UnaryInfC{$\circ^k \M \vdash \circ^k \Box A$}
\AxiomC{$\circ^k \Box A, \M' \vdash B$}
\RightLabel{(\textit{inductive cut})}
\dashedLine
\BinaryInfC{$\circ^k \M, \M' \vdash B$}
\RightLabel{$(\vdash\Box)$}
\UnaryInfC{$\Gamma', \circ^k \Gamma, \Gamma'', \circ^k \M, \M' \vdash
  \Box B, \circ^k \Delta, \Delta', \Delta''$}
\end{prooftree}
\end{center}

For the other cases, we first consider the ``parametric'' cases,
where the last rule above the $(\circ)$ rules is an extension $\rho'$
of a rule $\rho$ in \texttt{s4cnsne},
and the principal formula of $\rho$ is not the ``de-circled'' cut-formula $A$.
Recall that \texttt{s4cnsne} consists of the axiom, logical introduction rules
and the $(\Box\vdash)$ rule, as skeletons (ie, not extended with context),
but with $\circ^k$ applied to their formulae.
\begin{center}
\begin{prooftree}
\AxiomC{$X' \vdash Y', A$}
\RightLabel{($\rho'$)}
\UnaryInfC{$X \vdash Y, A$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$W, \circ^k X \vdash \circ^k Y, \circ^k A, Z$}
\AxiomC{$\circ^k A^m, U \vdash V$}
\RightLabel{(\textit{cut ?})}
\dashedLine
\BinaryInfC{W, $\circ^k X, U \vdash \circ^k Y, Z, V$}
\end{prooftree}
\end{center}

Here we must apply the $\circ$ rule the requisite number of times 
to the premise(s) of $\rho'$,
then apply (using the inductive hypothesis) cut on $\circ^k A$ to each of
them, and finally apply $\rho''$ which we get by applying
$\circ^k$ to $\rho$, and then extending it appropriately.

This uses the result that if a rule is in \texttt{s4cnsne} then so is
the result of applying $\circ^k$ to all formulae in its premises and
conclusion.
\begin{verbatim}
     s4cnsne_nkmap: "?r : s4cnsne ==> nkmap ?k ?r : s4cnsne"
\end{verbatim}
\begin{center}
\begin{prooftree}
\AxiomC{$X' \vdash Y', A$}
\RightLabel{($\circ^*$)}
\UnaryInfC{W, $\circ^k X' \vdash \circ^k Y', \circ^k A, Z$}
\AxiomC{$\circ^k A^m, U \vdash V$}
\RightLabel{(\textit{inductive cut})}
\dashedLine
\BinaryInfC{W, $\circ^k X', U \vdash \circ^k Y', Z, V$}
\RightLabel{($\rho''$)}
\UnaryInfC{W, $\circ^k X, U \vdash \circ^k Y, Z, V$}
\end{prooftree}
\end{center}

Lemma~\ref{l-s4cns-param-l} (\texttt{s4cns\_param\_l'}) and
the symmetric result \texttt{s4cns\_param\_r'} cover this case.

\begin{lemma} \label{l-s4cns-param-l}
Let the left premise subtree of a desired cut be \texttt{dt},
with \texttt{dtn} and $k$ as in Lemma~\ref{l-top-circ-ns},
let the bottom rule of \texttt{dtn} be an extension of  
a rule in \texttt{s4cnsne} whose conclusion is $cl \vdash cr$,
and let $C$ not be in $\circ^k cr$.
Then the inductive step \texttt{sumh\_step2\_tr} for proving cut-admissibility
with cut-formula $C$ holds.
\end{lemma}
\begin{verbatim}
s4cns_param_l': 
   "[| (?ps, ?cl |- ?cr) : s4cnsne ;
       botRule ?dtn : extrs {(?ps, ?cl |- ?cr)} ; 
       valid s4cns ?dtn ;
      count (mset_map (funpow Circ ?k) ?cr) ?C = 0 ;
      Suc (heightDTs ?list) = heightDT ?dtn + ?k |] 
     ==> sumh_step2_tr (prop2 casdt s4cns) ?C ?sub
                       (Der (seqmap (funpow Circ ?k) 
                            (conclDT ?dtn) + ?flr) ?list,
                        Der ?dtr ?lista)"
\end{verbatim}

It is similar for the parametric case on the right.
The axiom rule is trivial in all cases.

For the $(\vdash \Box)$ rule on the left, where the rule on the right 
is an extension of rule $\rho$ whose principal formula is the ``de-circled''
cut-formula, the only case remaining is where $\rho$ is $(\Box \vdash)$.
\begin{center}
\begin{prooftree}
\AxiomC{$\M \vdash A$}
\RightLabel{$(\vdash \Box)$}
\UnaryInfC{$X, \M \vdash \Box A, Y$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$X', \circ^k X, \circ^k \M \vdash \circ^k \Box A, \circ^k Y, Y'$}
\AxiomC{$\circ^{k''} A, U \vdash V$}
\RightLabel{$(\Box \vdash)$}
\UnaryInfC{$\circ^{k''} \Box A, U \vdash V$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^{k' + k''} \Box A, \circ^{k'} U, U' \vdash \circ^{k'} V, V'$}
\RightLabel{(\textit{cut?})}
\dashedLine
\insertBetweenHyps{\hskip 8pt}
\BinaryInfC{$X', \circ^k X, \circ^k \M, \circ^{k'} U, U' \vdash 
  \circ^k Y, Y', \circ^{k'} V, V'$}
\end{prooftree}
\end{center}

Here $k' + k'' = k$, but since we also have that $k = 0$ or $k' = 0$,
this means that $k' = 0$ and $k'' = k$.  The following diagram omits
a final use of the admissibility of weakening.
\begin{center}
\begin{prooftree}
\AxiomC{$\M \vdash A$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^k \M \vdash \circ^k A$}
\AxiomC{$\M \vdash A$}
\RightLabel{($\vdash \Box$)}
\UnaryInfC{$\M \vdash \Box A$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^k \M \vdash \circ^k \Box A$}
\AxiomC{$\circ^k \Box A, \circ^k A, U \vdash V$}
\RightLabel{(\textit{inductive cut})}
\dashedLine
\insertBetweenHyps{\hskip 8pt}
\BinaryInfC{$\circ^k \M, \circ^k A, U \vdash V$}
\RightLabel{(\textit{inductive cut})}
\dashedLine
\insertBetweenHyps{\hskip 8pt}
\BinaryInfC{$\circ^k \M, \circ^k \M, U \vdash V$}
\RightLabel{(\textit{ctr})}
\UnaryInfC{$\circ^k \M, U \vdash V$}
\end{prooftree}
\end{center}

Next we look at the case of the $(\vdash \Box)$ rule on the right,
but for this, since the cut-formula must be a $\Box$-formula,
all cases have already been dealt with.

Finally, there is the case where the last rules (above the final sequence of
$\circ$-rules) on both sides are extensions of rules in \texttt{s4cnsne}. 
Most of these cases have been covered, ie,
the axiom rules, and 
the ``parametric'' cases, where the ``de-circled'' cut-formula 
is not the principal formula of the rule.

So there remain the cases where the rules on either side are the logical
introduction rules.
For these, the proofs are essentially the same as for other logics generally,
except that we need to allow for a number of circles.
Conceptually it is easiest to imagine that in each case the final $\circ$ rules
are moved upwards to precede the final logical introduction rules,
although we didn't actually prove it this way.

We proved that the usual logical introduction rules,
with $\circ^k$ applied to principal and side formulae (as used in S4C),
satisfy \texttt{c8\_ercas\_prop} (Definition~\ref{d-c8-ercas-prop}).
Recall that this means that assuming cut admissibility on smaller
formulae, us have cut admissibility of a more complex formula where the last
rule on either side is a logical introduction rule.

\begin{lemma}[\texttt{s4cns\_c8\_ercas}] \label{l-s4cns-c8-ercas}
S4C satisfies \texttt{c8\_ercas\_prop} in relation to the 
logical introduction rule skeletons \texttt{lksil} $cup$ \texttt{lksir},
with $\circ^k$ applied to all formulae.
\end{lemma}
\begin{verbatim}
s4cns_c8_ercas: "c8_ercas_prop (circrel ipsubfml) s4cns ?A 
    (nkmap ?k ` (lksil Un lksir))"
\end{verbatim}

The following diagrams show an example.
We let $t = k + k' = l + l'$.
In this case we do not make use of the fact that either $k$ or $l$ must be
zero.
\begin{center}
\begin{prooftree}
\AxiomC{$X \vdash \circ^{k'} A, Y$}
\AxiomC{$X \vdash \circ^{k'} B, Y$}
\RightLabel{($\vdash \land$)}
\BinaryInfC{$X \vdash \circ^{k'} (A \land B), Y$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^k X \vdash \circ^t (A \land B), \circ^k Y$}
\AxiomC{$U, \circ^{l'} A, \circ^{l'} B \vdash V$}
\RightLabel{($\land \vdash$)}
\UnaryInfC{$U, \circ^{l'} (A \land B) \vdash V$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^l U, \circ^t (A \land B) \vdash \circ^l V$}
\RightLabel{(\textit{cut ?})}
\dashedLine
\BinaryInfC{$\circ^k X, \circ^l U \vdash \circ^k Y, \circ^l V$}
\end{prooftree}
\end{center}

The diagram above is simplified by not including the extra context which
may be introduced in the conclusion of the $(\circ)$ rules.
This is replaced by
\begin{center}
\begin{prooftree}
\AxiomC{$X \vdash \circ^{k'} A, Y$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^k X \vdash \circ^t A, \circ^k Y$}
\UnaryInfC{$\vdots$}
\noLine
\UnaryInfC{$\vdots$}
\noLine
\UnaryInfC{$\vdots$}

\AxiomC{$X \vdash \circ^{k'} B, Y$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^k X \vdash \circ^t B, \circ^k Y$}

\AxiomC{$U, \circ^{l'} A, \circ^{l'} B \vdash V$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^l U, \circ^t A, \circ^t B \vdash \circ^l V$}

\RightLabel{(\textit{inductive cut})}
\dashedLine
\BinaryInfC{$\circ^k X, \circ^l U, \circ^t A \vdash \circ^k Y, \circ^l V$}

\RightLabel{(\textit{inductive cut})}
\dashedLine
\insertBetweenHyps{\hskip -1.3cm}
\BinaryInfC{$\circ^k X, \circ^k X, \circ^l U \vdash 
  \circ^k Y, \circ^k Y, \circ^l V$}

\RightLabel{(\textit{contraction})}
\dashedLine
\UnaryInfC{$\circ^k X, \circ^l U \vdash \circ^k Y, \circ^l V$}
\end{prooftree}
\end{center}

Again, we can use weakening admissibility to get the extra context which 
was introduced by the $(\circ)$ rules, but omitted from the first diagram.

Finally we combine these results to get the cut admissibility result,
in terms of explicit derivation trees, and then in terms of derivability.

\begin{theorem}[\texttt{s4cns\_casdt, s4cns\_cas}] \label{t-S4C-ca}
S4C satisfies cut-admissibility.
\end{theorem}

\begin{verbatim}
   s4cns_casdt: "(?dta, ?dtb) : casdt s4cns ?A" 
     s4cns_cas: "(?cl, ?cr) : cas s4cns ?A"
\end{verbatim}

\subsection{Comparing our proofs and the proofs of Mints}

The slides for the presentation of Mints \cite{mints-jaegerfest}
contains a very abbreviated treatment of cut-admissibility for S4C.  
We attempted to follow the proof shown there, but were unable to.
The slides state a lemma (``Substitution Lemma''), that the following rule is
admissible
$$
\frac{\mathcal B \vdash \Box C \quad \Box C, \Gamma \vdash \Delta}
  {\mathcal B, \Gamma \vdash \Delta}
$$
As a lemma it is undoubtedly correct (it is a particular case of
cut admissibility).  However, as part of the proof of cut-admissibility
we were unable to prove it as it stands --- it appears to need (at least) an
assumption that cuts on $C$ are admissible.

\section{Related Work} \label{s-rw}

We may compare this approach with that of Pfenning
\cite{pfenning-structural-cut-elimination}.
Pfenning uses the propositions-as-types paradigm, 
where a type represents (partially) a sequent.
More precisely, for intuitionistic logic, a type
\texttt{hyp A -> hyp B -> conc C} represents a sequent containing
\texttt{A} and \texttt{B} in its antecedent, and 
\texttt{C} in its succedent.
For classical logic, 
\texttt{neg A -> neg B -> pos C -> pos D -> \#} 
represents a sequent containing
\texttt{A} and \texttt{B} in its antecedent, and 
\texttt{C} and \texttt{D} in its succedent.
A term of a given type represents a derivation of the corresponding sequent.

Pfenning's proof of cut-admissibility proceeds by a triple induction,
using structural induction on the formula and 
the two terms representing the derivations.
It therefore most closely resembles our proofs involving explicit derivations,
as described in \S\ref{s-ipedt}.

However in \S\ref{s-ipedt} we go on to measure properties (such as the height)
of an explicit derivation.  It seems as though Pfenning's approach does not
allow the possibility of doing that.  

Tews \cite{tews-coq} describes the use of Coq to prove cut-elimination for
propositional multi-modal logics.  In Coq, types are identified with terms, and
each term has a type: a type has the type \textbf{\textsf{Type}}.
A proposition is a type whose inhabitants are its proofs, so $A \to B$
means both the type of proofs of the proposition $A \to B$ and the type of
functions which take proofs of $A$ to proofs of $B$.
Since types can depend on terms, this gives a dependently typed system,
which can provide a way of capturing side-conditions in the type system.
For example, the type \textsf{counted\_list A n} is the type of lists of
items of type \textsf{A} and whose length is \textsf{n}.

Tews uses a (single) list of formulae as a sequent, where formulae which would
appear on the other side of a two-sided sequent are negated.
He proves that for the rule sets he uses, 
for any reordering $s'$ of the conclusion $s$ of a rule,
there is a corresponding rule whose conclusion is $s'$,
and, assuming sets of rules and hypotheses closed under reordering,
that provability is also closed under reordering. 
He defines an (object-logic) proof as the type \textsf{proof},
similar to our definition of the type \texttt{dertree},
but the type definition also incorporates the requirement 
that each ``node" of the tree must be in the given set of rules.
This is an example of a dependent type, where the type \textsf{proof}
depends on the term \textsf{rules}.

He proves cut-elimination both semantically (by proving soundness and
cut-free completeness) and syntactically (where the proof implements a
cut-elimination procedure). Thus his work includes extensive formalisation of
the semantics of the logics.  His proofs use the modal ranks of formulae,
and involve formalising substitution, which we did not find necessary,
and in some cases require proving depth-preserving admissibility of rules.

\section{Further Work and Conclusion} \label{s-fwc}
We have proved cut-admissibility for several different sequent calculi,
ranging from the well-known logics S4 and S4.3 to GTD and S4C described
recently in \cite{mints-jaegerfest}.
In other work not described here we also proved cut-admissibility for
GTD, for a calculus containing explicit contraction and weakening rules, in 
both the ways described at the start of \S\ref{s-s4c-cut}.

We have shown how the proofs can be split up into
components some of which were expressed in lemmata which
can be reused in similar proofs for other calculi.
This was of significant value, as was the use of the type classes described
in \cite{dawson-gore-generalised}.
It remains to generalise our framework so that these results follow simply by
instantiating these general concepts.
\bibliographystyle{alpha}
\bibliography{dawson-gore-wu}
% \input{refs}

\end{document}


