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

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

\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\derrec{\texttt{derrec}}
\newcommand\rls{\texttt{rls}}
\newcommand\adm{\texttt{adm}}

\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{P}}
\newcommand\wbx{\Box}
\newcommand\wdi{\lozenge}
\newcommand\nxt{\bigcirc}
\newcommand\limp{\rightarrow}

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

\pagestyle{plain}

\begin{document}

\title{Machine-checked Cut-Admissibility for Propositional Modal Logics}

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

\date{}
%% Title 
\maketitle

\begin{abstract}
  We describe how we machine-checked cut-admissibility for
  multiset-based sequent calculi for the unimodal logics K4D, S4 and
  S4.3 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 xx 
\end{abstract}

%% Here begins the main text

\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 containing 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{gr-valentini}. 

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

In Section~\ref{sec:preliminaries}, we briefly describe traditional
sequent calculi, discuss the need for multisets, and describe ???

In Section~\ref{s-deriv} we describe techniques and functions we have
defined for reasoning about derivations, and show how we formalise
formulae, sequents and rules, showing some of the sequent rules
as examples.
%
In Section~\ref{s-caglr} we describe the cut-admissibility proof for
???.

We assume the reader is familiar with basic
proof-theory, ML and Isabelle/HOL.
%
Our Isabelle code can be found at
\url{http://users.rsise.anu.edu.au/~jeremy/isabelle/200x/seqms/}.  
Some of this work was reported informally in \cite{gore-india}.

%TO DO - include explanation of Isabelle notation

\section{Sequents Built From Multisets Verssus 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, to multisets for
linear logic, to ordered lists for substructural logics, to complex
tree structures for display logics.
%
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 formalisation does not
regard the cut (or multicut) 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 \vdash A^{n}, \Delta$}
  \AxiomC{$\Gamma, A^{m} \vdash \Delta$}
  \LeftLabel{(multicut)}
  \BinaryInfC{$\Gamma \vdash \Delta$}
  \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.

\section{Basic Modal Logics}
\label{s-modal}

The sequent calculi we study are designed to reason about the
meta-theory of the basic modal logics K4D, S4, S4.3 and
$\lgp$. Semantically, the first three are mono-modal logics 
characterised by Kripke frames having serial and transitive, reflexive
and transitive, and reflexive, transitive and linear frames
respectively. The logic $\lgp$ is a bimodal logic whose
$\wbx$-modality is characterised by ??? and whose $\nxt$ modality is
characterised by ???.

The Hilbert-calculi for these logics are obtained by extending a
traditional Hilbert-calculus for classical propositional logic with
the following axioms and inference rules:

\begin{tabular}[c]{ll}
  Axiom K$\wbx$
  & $\wbx (\varphi\limp\psi) \limp (\wbx\varphi \limp \wbx\psi)$ 
\\
  Axiom D
  & $\wbx\varphi \limp \wdi\varphi $ 
\\
  Axiom T 
  & $\wbx\varphi \limp \varphi $ 
\\
  Axiom 4
  & $\wbx\varphi \limp \wbx\wbx\varphi $ 
\\
  Axiom .3
  & $\wbx (\wbx\varphi\lor\wbx\psi) \limp (\wbx\varphi \lor \wbx\psi)$ 
\\
  Rule of Necessitation $\wbx$
  & $\varphi$/$\wbx\varphi$
\end{tabular}

The logic $\lgp$ is obtained from S4 by adding the following axioms
and rule:
\begin{tabular}[c]{ll}
  Axiom K$\nxt$
  & $\nxt (\varphi\limp\psi) \limp (\nxt\varphi \limp \nxt\psi)$ 
\\
  Axiom P 
  & $\wbx\nxt\varphi \limp \nxt\wbx\varphi$  
\\
  Rule of Necessitation $\nxt$
  & $\varphi$/$\nxt\varphi$
\end{tabular}

The modal logic $\lgp$ is designed to capture the basic logic for
hybrid systems where ...


\section{Reasoning About Derivations and Derivability}
\label{s-deriv}

% \section{Isabelle} \label{s-isa}
% Isabelle is an automated proof assistant \cite{isabelle-ref}.  Its
% meta-logic is an intuitionistic typed higher-order logic, sufficient
% to support the built-in inference steps of higher-order unification
% and term rewriting.  Isabelle accepts inference rules of the form
% $\alpha_1, \alpha_2, \ldots, \alpha_n, \Longrightarrow \beta$
% where the $\alpha_i$ and $\beta$ are expressions of the Isabelle
% meta-logic, or are expressions using a new syntax, defined by the
% user, for some ``object logic''. Most users build on one of the
% comprehensive ``object logics'' already supplied, like Isabelle/HOL
% \cite{IsLogHOL}, which is an Isabelle theory based on the higher-order
% logic of Church % \cite{church-types}
% and the HOL system of Gordon \cite{HOL-introduction}.  HOL offers
% inductively defined sets, and recursive datatypes, which we use
% extensively.  

In previous work~\cite{dawson-gore-embedding-comparing}, we describe
our initial attempts to formalise display calculi in various logical
frameworks and describe why we selected Isabelle/HOL.  When we model a
derivation tree, explicitly, we do so using the capability in HOL of
defining types like the datatypes of SML, see \S\ref{s-dse}.  
%Here we return to simpler sequents and seek generality.

\subsection{Deep and Shallow Embeddings} \label{s-dse} 

In~\cite{dawson-gore-cut-admissibility}, we modelled a derivation tree
in HOL as a recursive structure which consists of a
root sequent (which should be the conclusion of some rule), and an
associated list of (sub)trees (each of which should derive a premise of
that rule). The type of explicit derivation trees is a recursive
datatype, such as:
\begin{verbatim}
   datatype 'a dertree = Der 'a ('a dertree list)
       | Unf 'a (* unfinished leaf which remains unproved *)
\end{verbatim}
%
We then had to define a predicate on such a tree, saying whether it
was in fact correctly based on the given rules, and so represented a
valid derivation.
%
We modelled a sequent rule as an object in HOL consisting of a list of
premises and a conclusion, each of which was a sequent in the language
of the logic (of relation algebras). Notably, our language of formulae
included ``variables'' which could be instantiated with formulae, 
so we defined functions for such substitutions.
%
Thus it is more accurate to say in
~\cite{dawson-gore-cut-admissibility}, we used a deep embedding for
\emph{derivations}, \emph{rules} and \emph{variables}, since we
modelled each of these features of the proof-theory explicitly rather
than identifying them with the same features of Isabelle.

In alternative approaches to work of this type, the set of derivable
sequents can be modelled as an inductively defined set \texttt{ders}
(say),
% (as we describe in \S\ref{s-dp}). 
where the derivation tree does not exist, but it ``happens'' in the
course of proving that a specific sequent is derivable.  That is,
derivability in the sequent calculus studied equates to derivability
in Isabelle, giving a shallow embedding of {\em derivations}.

In such alternative approaches, the rules of the sequent calculus can
either be encoded explicitly 
%(as assumed in the treatment in \S\ref{s-dp}), 
or they can be encoded in the clauses for the inductive definition of
\texttt{ders}.  In the latter case, the rules of the
sequent calculus under study are encoded as theorems of Isabelle.
Thus, even with a shallow embedding of derivations, we have a choice
of either a deep or a shallow embedding of {\em rules}:
%where \textit{ders} means the set of derivable sequents:
% \begin{gather}
%  (\{P,  Q\},  {P \land Q}) \in \mathit{rules} \tag{deep}
% \qquad
% \frac{ (ps, c) \in \mathit{rules} \quad ps \subseteq \mathtt{ders}}
% {  c \in \mathtt{ders}}
% \\[1ex]
% \frac {P \in \mathtt{ders} \qquad Q \in \mathtt{ders}}
% {P \land Q \in \mathtt{ders}} \tag{shallow}
% \end{gather}
%
\begin{description}
\item[\rm Deep Rules and Shallow Derivation:] \ \\[0.5em]
  \begin{tabular}[c]{l}
   $\mathtt{(\{\Gamma \vdash P, ~~\Gamma \vdash Q\},  
     \;\; \Gamma \vdash P \land Q) \in rules}$
  \\[0.5em]
   $\mathtt{ [|~(ps, c) \in rules ~;~ ps \subseteq \mathtt{ders}~|]
         ==> c \in \mathtt{ders}}$
  \\[0.5em]
  \end{tabular}
\item[\rm Shallow Rules and Shallow Derivations:] \ \\[0.5em]
  \begin{tabular}[c]{l}
   $\mathtt{[|~\Gamma \vdash P \in \mathtt{ders} ~;~ 
          \Gamma \vdash Q \in \mathtt{ders}~|]
        ==> \Gamma \vdash P \land Q \in \mathtt{ders}}$.
  \end{tabular}
\end{description}

Finally, compared to \cite{dawson-gore-cut-admissibility}, it is much
more common to let the variables in a rule be the variables of the
theorem prover, and for the theorem prover to do the substitution. In
general, however, a deep embedding of one feature can be combined with
a shallow embedding of another.

Our experience is that shallow embeddings generally permit easier
proofs, but sometimes they are inadequate to express a desired
concept. For example, with a deep embedding of rules it is easy to
express that one set of rules is a subset of another set.  With a deep
embedding of derivation trees it is easy to express that one property
of derivation trees is the conjunction of two other properties, or
that a derivation tree has a particular height, whereas to express
such things using \derl, \derrec, etc (see \S\ref{s-dp}), one would
have to redefine these predicates incorporating the particular
properties of interest.  Indeed, in this work (see \S\ref{s-caglr}) we
discuss how we found a shallow embedding of derivability inadequate.

We have developed the code on which
\cite{dawson-gore-cut-admissibility} was based to reflect the fact
that Belnap's original proof applied generally to display calculi
satisfying certain conditions.  Some of these conditions required a
deep embedding of variables (and, therefore, of the rules), for
example, that no structure variable appears twice in the conclusion of
the statement of a rule.  For others, a shallow embedding of variables
was adequate, since the condition applied equally to the statement of
the rule and to all its substitution instances, for example that a
premise of a rule contains no variable not contained in the
conclusion.

% In \cite{dawson-gore-machine-checked-strong-normalisation}, we
% considered the individual steps involved in changing a derivation
% containing cuts to a derivation not containing cuts. The explicit
% manipulation of derivation trees, such that each change makes a tree
% ``smaller'' in some sense, made it necessary to have a deep embedding
% of derivation trees.

\subsection{Our General Derivability Predicates} \label{s-dp} 

We now briefly describe the functions we used to describe
derivability.  A fuller account is given in \cite{gore-india}. 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 formulae.

\begin{verbatim}
types 'a psc = "'a list * 'a"       (* single step inference *)
consts
  derl, adm :: "'a psc set => 'a psc set"
  dersl     :: "'a psc set => ('a list * 'a list) 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"
\end{verbatim}

An inference rule \texttt{'a psc} is a list of premises \texttt{ps}
and a conclusion \texttt{c}. Then, \texttt{derl rls} is the set of
rules derivable from the rule set \texttt{rls}, and \texttt{derrec rls
  prems} is the set of formulae derivable using rules \texttt{rls}
from the set \texttt{prems} of premises.  These were defined as
inductive sets, using also the functions \texttt{dersl} and
\texttt{dersrec}. So $\mathtt{(ps, c) \in \derl\rls}$ reflects the
shape of a derivation tree: \texttt{ps} is a list of exactly the
premises used, in the correct order, whereas $\mathtt{c \in \derrec\
  \rls\ prems}$ holds even if the set of premises \texttt{prems}
contains extra formulae.

The auxiliary function \texttt{dersrec} represents several formulae,
all derivable from the premises.  The auxiliary function
\texttt{dersl} represents several derivation trees side by side;
$\mathtt{(ps, cs) \in dersl~rls}$ when \texttt{ps} is the
concatenation of their lists of premises, and \texttt{cs} is the list
of their conclusions.  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}$.  Curiously, we have used this framework for several years, and
only recently we found the need to redefine \derl\ using
\texttt{dercsl} rather than \texttt{dersl} as the auxiliary function.

The key clauses for these functions are shown below:
\begin{verbatim}
  dtderI : "[| (ps, concl) : pscrel ; (pss, ps) : dersl pscrel |] 
              ==> (pss, concl) : derl pscrel"
  derI : "[| (ps, concl) : pscrel ; ps : dersrec pscrel prems |] 
              ==>  concl : derrec pscrel prems"
\end{verbatim}

We obtained the expected results linking \texttt{derl} and \texttt{derrec},
and a number of results expressing transitivity of derivation and the
results of derivation using derived rules, for example:
\begin{verbatim}
derl_trans : "[| (?ps, ?c) : derl ?rls; (?x, ?ps) : dersl ?rls |]
                 ==> (?x, ?c) : derl ?rls" 
derl_deriv_eq : "derl (derl ?rls) = derl ?rls" 
derrec_trans_eq : "derrec ?rls (derrec ?rls ?prems) = derrec ?rls ?prems"
\end{verbatim}

A simplified verson of the induction principle 
generated by the definition of the inductive set \derrec\ is as follows:
$$
\frac {x \in derrec\ rls\ prems \quad
   \forall c \in prems. P\ c \quad 
   \forall (ps, c) \in rls. (\forall p\ in\ ps. P\ p) \Rightarrow P\ c}
   {P\ x}
$$

We may contrast use of this principle 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 above, 
and was not needed for our earlier proofs.

Where we have a property of two derivations, such as cut-admissibility,
we need a more complex induction principle, which we derived
(limited to the case where the set \textit{prems} of ultimate assumptions is
empty) :
$$
 \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}
$$

Finally, $(ps, c)$ is an admissible rule iff: if all premises in $ps$
are derivable, then $c$ is derivable:\\
$(ps, c) \in \adm\ \rls \iff 
(set\ ps \subseteq \derrec\ \rls \ \ \Rightarrow \ \ c \in \derrec\
\rls)
$.

We obtained the following four results, which were surprisingly tricky
since \adm\ is not monotonic:
\begin{verbatim}
"derl ?rls <= adm ?rls"              "adm (adm ?rls) = adm ?rls"
"adm (derl ?rls) = adm ?rls"         "derl (adm ?rls) = adm ?rls"
\end{verbatim}

\subsection{Sequents, Formulae and the \GLS\ rules} \label{s-gls}

We define a language of formulae, with the usual connectives:
\begin{verbatim}
datatype formula = FC string (formula list) (* formula connective *)
                 | FV string                (* formula variable *)
                 | PP string             (* primitive proposition *)
\end{verbatim}
%
The formula connectives are fixed for each logic, 
but we make the datatype as general as possible, 
replacing connectives such as $\land$, $\lor$, etc, with \texttt{FC}
\textit{name}:
\begin{verbatim}
consts
  Btimes :: "formula => formula => formula" ("_ && _" [67,68] 67)
  Bplus  :: "formula => formula => formula" ("_ v _" [63,64] 63)
defs
  Btimes "Btimes f g == FC ''Btimes'' [f, g]"
  Bplus  "Bplus f g == FC ''Bplus'' [f, g]"
\end{verbatim}
%
This permits a single definition of the immediate (proper) subformula
relation, \texttt{ipsubfml}, which will not need to be changed when new
connectives are added.
\begin{verbatim}
consts ipsubfml :: "(formula * formula) set"
inductive "ipsubfml" (* proper immediate subformula relation *)
  intros  ipsI : "P : set Ps ==> (P, FC conn Ps) : ipsubfml"
\end{verbatim}
%
A sequent is a pair of multisets of formulae, written 
$\Gamma \vdash \Delta$ or $\Gamma \Rightarrow \Delta$.
\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
\MR_e = \frac{X \vdash Y, A \quad X \vdash Y, B} {X \vdash Y, A \land B}
$$
we define functions \texttt{extend} and \texttt{pscmap}, such that 
(for example)
\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*}
Then \texttt{extrs} $S$ means the set of all extensions of all rules in the set
$S$.

\begin{verbatim}
consts
  extend :: "'a sequent => 'a sequent => 'a sequent"
  extrs  :: "'a sequent psc set => 'a sequent psc set"
defs
  extend_def : "extend fmls seq == seq + fmls"
  pscmap_def : "pscmap f (ps, c) = (map f ps, f c)" 
\end{verbatim}

Then we define \texttt{glss}, the set of rules of \GLS;
we show just a selection. 
Sets \texttt{wkrls} and \texttt{ctrrls} $A$ refer to weakening and contraction
(on $A$) rules.
\begin{verbatim}
inductive "glir" (* right introduction rules *)
intros
 andr : "([{#} |- {#A#}, {#} |- {#B#}], {#} |- {#A && B#}) : glir"
 orr1 : "([{#} |- {#A#}], {#} |- {#A v B#}) : glir"

inductive "glne" (* rules before being extended *)
intros
 wkI  : "(ps, c) : wkrls ==> (ps, c) : glne"
 ctrI : "(ps, c) : ctrrls A ==> (ps, c) : glne"
 ilI  : "(ps, c) : glil ==> (ps, c) : glne"
 irI  : "(ps, c) : glir ==> (ps, c) : glne"

inductive "glr B"
intros
 I : "([mset_map Box X + X + {#Box B#} |- {#B#}],
        mset_map Box X |- {#Box B#}) : glr B"

inductive "glss"
intros
 axiom : "([], {#A#} |- {#A#}) : glss"
 extI : "psc : glne ==> pscmap (extend flr) psc : glss"
 glrI : "psc : glr B ==> psc : glss"
\end{verbatim}
Note that $X$ is a multiset, and $\Box X$ is informal notation for applying 
$\Box$ to each member of $X$; this is formalised as \texttt{mset\_map},
used in the formalised \GLR\ 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\}}.

\section{An Axiomatic Type Class for Multisets and Sequents} \label{s-axtc}

Isabelle provides a theory of finite multisets with an ordering 
based on an underlying ordering on members: given multiset $M$,
we obtain a multiset $N$ less than $M$ by removing an occurrence of some $m$
from $M$, and replacing it with any number of occurrences of elements
smaller than $m$.  We defined a different ordering $\leq$ analogous to
$\subseteq$ for sets: $N \leq M$ if, for all $x$, $N$ contains no more
occurrences of $x$ than does $M$.

An axiomatic type class is characterised by a number of axioms, which hold
for all members of a type in the type class.
The axioms can be used to prove theorems, which then apply
and can be used efficiently for any type which is in the class.
The multiset operators $\leq$, $+$, $-$ and $0$ have several useful properties,
which are described by the following axiomatic type classes
\pmz{} and \pmgez.

\begin{verbatim}
   axclass pm0 < comm_monoid_add, minus
     pm0_plus_minus  : "A + B - A = B"
     pm0_minus_minus : "A - B - C = A - (B + C)"
\end{verbatim}

Thus for any type in class \pmz, the operations
$+$ and $0$ form a commutative monoid, the type allows the $-$ operator, and
the two axioms given hold.

\begin{verbatim}
   axclass pm_ge0 < pm0, ord, leq
     all_ge0        : "0 <= A"
     diff_0_le      : "(m - n = 0) = (m <= n)"
     le_add_diff_eq : "B <= A ==> B + (A - B) = A"
     pm_ge0_less_le : "(x < y) = (x <= y & x ~= y)"
     pg_leq_def     : "a [= b == a <= b"
\end{verbatim}

Class \pmgez\ also has an $\leq$ operator,
$0$ is the smallest element via \texttt{all\_ge0},
and \texttt{le\_add\_diff\_eq} also holds.
For a new type, the other axioms could be made definitions, 
but for natural numbers, $\leq$ and $<$ are already defined.
The naturals obey all these axioms. An explanation of \texttt{[=} is
below.
\begin{lemma}
  Multisets are in \pmz\ and \pmgez\ using our definition of $\leq$.
  Moreover, if $\Gamma$ and $\Delta$ are of any type in the classes
  \pmz\ or \pmgez, then our sequents $\Gamma \vdash \Delta$ are also
  in these classes.
\end{lemma}

Isabelle contains ``simplification procedures'', 
which will simplify $a - b + c + b$ to $a + c$ for integers, 
and which will simplify $a + b + c - b$ to $a + c$ 
for integers \emph{or} naturals.
We have been able to apply almost all of the ones which apply to naturals,
to types of the classes \pmz\ and \pmgez.

It is easy to show that, in the obvious way, multisets form a lattice.
Isabelle's lattice type class is based on using \texttt{[=} as the
order operator. By including the definitional
axiom \texttt{pg\_leq\_def} above, 
we were able to show:
\begin{lemma}
  Any type of class \pmgez\ forms a lattice.
\end{lemma}
\begin{proof}
The definitions of meet and join are shown below:
\begin{verbatim}
"pg_meet ?c ?d == ?c - (?c - ?d)"  "pg_join ?c ?d == ?c + (?d - ?c)" 
\end{verbatim}

From these it is possible to prove
the axioms for a lattice
at some length,
and so any type in the class \pmgez\ is also in Isabelle's class
\texttt{lattice}.
\end{proof}

We produced a number of equivalent definitions characterising atoms of the
lattice, and properties of atomic elements 
(our definition of \texttt{atomic} includes $0$).
Thus we showed that $x$ is atomic is equivalent to each of the following: 

\begin{tabular}[c]{l@{\extracolsep{1cm}}l}
\multicolumn{2}{c}{$\forall y  < x.\ y = 0$}
\\ 
 $\forall z.\ x \leq z \lor (\mathit{pg\_meet}\ x\ z = 0)$ 
& $\forall a b.\ x \leq a + b \Rightarrow x \leq a \lor x \leq b$
\\
 $\forall a b.\  0 < a \land 0 < b \Rightarrow a + b \not= x$
& $\forall a b.\  a < x \land b < x \Rightarrow a + b \not= x$
\end{tabular}
%
The source files for this development are \texttt{pmg*.\{thy,ML\}}.

\section{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.
%
In \S\ref{s-deriv} we mentioned the induction principle used for
deriving cut-admissibility, or indeed any property $P$ of two-premise
subtrees.  In the diagram below, to prove $P (\MR_{l}, \MR_{r})$, the
induction assumption is that $P (\MQ_{li}, \MR_{r})$ and $P (\MR_{l},
\MQ_{rj})$ 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{$\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 ?})}
\dottedLine
\BinaryInfC{?}
\end{prooftree}
\end{center}
A proof of $P (\MR_{l}, \MR_{r})$ 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 $\MQ_{li}$, etc, above are sequents, 
So we actually consider a property $P\ A\  (cl, cr)$
where $psl$ are the premises $\MQ_{l1} \ldots \MQ_{ln}$ of rule
$\rho_l$, and $cl$ is its conclusion $\MR_{l}$, and analogously for
$\rho_r$, and $A$ is the cut-formula.  In proving $P\ A\ (\MR_{l},
\MR_{r})$, in addition to the inductive assumption above, we assume
that $P\ A' \ (da, db)$ holds generally for $A'$ smaller than $A$ and
all sequents $da$ and $db$ which are derivable from the empty set of
premises 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'':
\begin{definition}
 For a formula \texttt{A}, 
 a property \texttt{P},
 a subformula relation \texttt{sub},
 a set of rules \texttt{rls},
 inference rules \texttt{(psl, cl)}, and
 \texttt{(psr, cr)},
 the property \texttt{gen\_step2sr} holds if:
 \texttt{P A (cl, cr)} holds whenever
 \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};
 for each \texttt{pa} in \texttt{psl}, \texttt{pa} is
 \texttt{rls}-derivable and \texttt{P A (pa, cr)} holds;
 for each \texttt{pb} in \texttt{psr},
 \texttt{pb} is \texttt{rls}-derivable and
 \texttt{P A (cl, pb)} holds;
 \texttt{cl} and \texttt{cr} are \texttt{rls}-derivable.
\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
is possible for all cases of final rule instances $(psl, cl)$ and
$(psr, cr)$ on each side, then $P$ holds in all cases.

\begin{theorem}
 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)} holds.
\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}

\end{theorem}

This enables us to split up an inductive proof, by showing,
separately, that \texttt{gen\_step2sr} holds for particular cases of
the final rules $(psl, cl)$ and $(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 mar ?erls ?A (?cl, ?cr)} means
that the conclusion of a multicut on \texttt{A} with premises
\texttt{cl} and \texttt{cr} is derivable using rules \texttt{erls}.

\begin{theorem}
  If weakening is admissible for the rule set \texttt{erls}, all
  extensions of some rule \texttt{(ps, c)} are in the rule set
  \texttt{erls}, and the final rule instance of the left hand subtree
  is an extension of \texttt{(ps, c)} where the cut-formula \texttt{A}
  is not in the succedent of \texttt{c} (meaning that \texttt{A} is
  parametric on the left), then
  \verb!gen_step2sr (prop2 mar ?erls) ?A ?sub ?rls (?pscl, ?pscr)!
  holds.
\begin{verbatim}
mk_sr1 lmg_gen_step' :
   "[| wk_adm ?erls; extrs {(?ps, ?c)} <= ?erls; ~ ?A :# succ ?c;
         ?pscl = pscmap (extend ?flr) (?ps, ?c) |]
      ==> gen_step2sr (prop2 mar ?erls) ?A ?sub ?rls (?pscl, ?pscr)"
\end{verbatim}
\end{theorem}

Of course, for a system containing explicit weakening rules, such as
\GLS{}, weakening is {\it a fortiori} admissible. But as noted
earlier, we have tried to make our results as general as possible.

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 all of this section has used a shallow embedding of
derivations since no explicit derivation trees were required.

\input{gls}
\input{refs}

\end{document}

