
\section{Isabelle Framework}
COMBINE THIS SECTION WITH JEREMY'S STUFF

TODO: perhaps begin with shallow stuff below, then bring in Jeremy's section 2.
or start with Jeremy's section 2, cover mix for GTD, then move to S4, and then introduce shallow stuff for weak/inv/ctr proofs.\\
not sure how to organise this.

\medskip


Meta-level proofs generally follow an inductive procedure on derivations. However, many transformations do not actually require use of the height of an original derivation $\Pi$ in creating some new derivation, they only refer to the endsequents derived by $\Pi$. In particular, an induction on height can often be mimicked by an induction on rule applications. Rather than using an actual derivation tree, where the induction hypothesis is applied on a sub-tree of height $n$, it is normally simpler in a formal proof to deal only with the last rule, where the induction hypothesis is applied on the premises of that rule.

This leads to a shallow embedding of derivations, as inductively defined sets:
\begin{lstlisting}
consts derrec :: "'a psc set => 'a set => 'a set"
\end{lstlisting}
where \texttt{derrec rls prems} is the set of sequents derivable using the rules \texttt{rls} from a set \texttt{prems} of premises. Formally this is encoded as:\\[4px]
\begin{tabular}[c]{l}
 $ ~c \in \mathtt{prems} \Longrightarrow c \in \mathtt{derrec~rules~prems}$ \\
 $ [|~(ps, c) \in \mathtt{rules} ~;~ 
    ps \subseteq \mathtt{derrec~rules~prems}~|]
       \Longrightarrow c \in \mathtt{derrec~rules~prems}$
\end{tabular}

\smallskip

%Note that in Isabelle syntax, $[| X ~;~ Y ~;~ Z |] \Longrightarrow P$, states that given $X, Y, Z$ it follows that $P$ holds. The brackets are omitted if there is only one assumption.

Shallow embeddings will be used for many of the formalised proofs in this work. These have the advantage of simplifying representations of derivations and also the proofs themselves.

As the shallow embedding of derivations uses inductively defined sets, Isabelle provides an induction principle for proving properties for such derivations. A slightly simplified version is used as a basis for proving results about \weaka{} and invertibility.

\begin{lemma}[\texttt{drs.inductr}]\label{inductr:lem}~\\
For a derivable sequent \texttt{$x \in$ derrec rls prems}, if property $P$ holds for all initial sequents \texttt{prems} (such initial assumptions are always empty for this work), and also for all \texttt{$(ps, c) \in$ rls} it can be shown that $\forall p \in ps.\ P\ p$ implies $P\ c$, then $P\ x$ also holds.
\end{lemma}

Lemma~\ref{inductr:lem} essentially replaces the standard pen and paper induction on height, with an induction on rule applications -- if every rule preserves a property $P$ from premises to conclusion, then so does the whole derivation. The downside of this principle is that there is never an explicit derivation tree, only the exact premises of a rule application are accessible, so transforming sub-trees in some height-preserving way is impossible. Nevertheless, this principle is sufficient to prove \weaka{} for the class of sequent calculi which allow arbitrary contexts in the conclusion of all rules.





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:

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

\smallskip

\texttt{gen\_step $P\ A$ sub rls derivs r} means:
\begin{description}
 \item[if] forall $A'$ such that \texttt{$(A', A) \in$ sub}\\
   and all \texttt{rls}-derivable sequents $D$ the property
   $P\ A'\ D$ holds\\
   and for every premise $p \in ps$ both \texttt{$p \in$ derivs} and $P\ A\ p$ holds
 \item[then] $P\ A\ c$ holds.
\end{description}
\end{definition}

In English, this step condition states that if a property $P$ is true 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.

\pagebreak

\begin{theorem}[\texttt{gen\_step\_lem}]\label{genstep:lem}~
\begin{description}
\item[if]
item $A$ is in the well-founded part of the subformula relation \texttt{sub}\\
and sequent \texttt{S} is \texttt{rls}-derivable\\
and for all formulae $A'$, 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
\item[then]
\texttt{P\ A\ S} holds.
\end{description}
\end{theorem}




\subsection{Weakening, Invertibility and Contraction}
Weakening admissibility, invertibility, and \ctra{} are stated using \texttt{wk\_adm}, \texttt{inv\_rl} and \texttt{ctr\_adm} respectively:

\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$.

\subsection{Cut}
NEED JEREMY'S STUFF FOR CUT BASED ON DEEP TREES HERE

...

TODO:
could introduce the following in the proof for Cut for S4, if we want to intertwine the formalisation and pen and paper stuff more.

\medskip

For a cut-formula $A$, \cuta{} is expressed as:
\begin{description}
\item[\texttt{(Xl |- mins A Yl, mins A Xr |- Yr) : cas rls A)}]~\\
The property name is \texttt{cas}, and \texttt{rls} once again represents a calculus (set of rules).
\texttt{mins} is multiset insertion, while \texttt{X} and \texttt{Y} for both the left and right represent arbitrary multisets. The pair of sequents in the \cuta{} statement then simply correspond to two potential premises for an application of the Cut rule.
The definition of \texttt{cas} states that if both these left and right sequents are \texttt{rls}-derivable, then so is the sequent, \texttt{(Xl + Xr |- Yl + Yr)}, which would result from applying Cut on $A$.
\end{description}

In addition to the height\_step2\_tr\_eq lemma, we also use the following induction principle, named 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 prems}),
and explicit derivation trees \texttt{dta} and \texttt{dtb},

\smallskip

\texttt{sum\_step2\_tr $P\ A$ sub gsl gsr (dta, dtb)} means:
\begin{description}
 \item[if] forall $A'$ such that \texttt{$(A', A) \in$ sub}\\
   the property $P\ A'\ (a, b)$ holds for all derivation trees \texttt{a} and \texttt{b}\\
   and for all derivation trees \texttt{dta'} and \texttt{dtb'} where\\
   \texttt{gsl dta' + gsr dtb' < gsl dta + gsr dtb}\\
   the property $P\ A (dta', dtb')$ holds
 \item[then] $P\ A\ (dta, dtb)$ holds.
\end{description}
\end{definition}

Instantiating the measures in \texttt{sum\_step2\_tr} with measures of derivation height results in the final principle used to prove \cuta{}:
\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{A'}, and derivation trees \texttt{dta} and \texttt{dtb}\\
the induction step condition \texttt{sum\_step2\_tr P A' sub heightDT heightDT (dta, dtb)} holds
\item[then]
\texttt{P A (dta, dtb)} holds
\end{description}
\end{theorem}

