\message{ !name(ce.tex)}%%
%%
\documentclass{llncs}
%\usepackage{makeidx}
%\usepackage{acmnew-xref}

% \usepackage[scrtime]{prelim2e}
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{exptrees}

%\RequirePackage{mathptm}
%\RequirePackage{times}
%\RequirePackage{palatino}

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

%\setlength \parskip {1.0ex}
\setcounter{secnumdepth}2
\setcounter{tocdepth}2

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Preamble

\newcommand{\mcyl}{\raisebox{0.2ex}{\bf c}}
\newcommand{\mor}{+}
\newcommand{\mand}{\circ}
\newcommand{\mnot}{\sim}
\newcommand{\mimp}{\rightarrow}
\newcommand{\mif}{\leftarrow}
\newcommand{\mtop}{\mbox{\bf 1}}
\newcommand{\mbot}{\mbox{\bf 0}}
%\newcommand{\myzero}{\mbox{\bf 0}}
\newcommand{\mstar}{\bigstar}

%\newcommand{\fiss}{+}

\newcommand{\mcal}[1]{\mbox{$\cal #1$}}

\newcommand{\btop}{\top}
\newcommand{\bbot}{\bot}
\newcommand{\bor}{\vee}
\newcommand{\band}{\wedge}
\newcommand{\bnot}{\neg}
\newcommand{\bimp}{\supset}

\newcommand{\conv}{\smallsmile}
\newcommand{\semic}{\mbox{ ; }}
\newcommand{\comma}{\raisebox{0.5ex}{ , }}
%\newcommand{\colon}{\mbox{ : }}
\newcommand{\myE}{ E }

\newcommand\cfile{}
%\renewcommand{\thepage}{\roman{page}}
\newcommand\shrinklist[1]{
\setlength\parskip{#1\parskip}
\setlength\itemsep{#1\itemsep}
\setlength\itemindent{#1\itemindent}
\setlength\topsep{#1\topsep}
}

\newcommand\comment[1]{} 
% \newcommand\cc[1]{} % for label names 
\newcommand\cc[1]{#1} % for label names 
% \renewcommand\footnote[1]{} % for footnotes
% \pagestyle{myheadings}

\newcommand\url[1]{\texttt{#1}} % in Raj's bibliography

\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\proof{\noindent\textbf{Proof.}}
\newcommand\src[1]{source file \texttt{#1}}
\newcommand\apsrc[1]{Appendix \ref{app:code}}
%\newcommand\seesrc[1]{(see source file \texttt{#1}, \apsrc{#1})}
\newcommand\seesrc[1]{(see source file \texttt{#1})}
%\newcommand\insrc[1]{in source file \texttt{#1} (see \apsrc{#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\M{\ensuremath{\mathcal M}}
\newcommand\Mp{$\mathcal M'$}
\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\pt{\texttt{pt}}
\newcommand\ptn{\texttt{ptn}}

\newcommand{\blob}{\bullet}

% automatically defined in LLNCS style
%\newtheorem{thm}{Theorem}%[chapter]
%\newtheorem{lemma}[thm]{Lemma}
%\newtheorem{defn}[thm]{Definition}
%\newtheorem{cor}{Corollary}[thm]
%\renewcommand\thecor{\thethm(\arabic{cor})}

\pagestyle{plain}

\begin{document}
{\makeatletter\gdef\AucTeX@cite#1[#2]#3{[#3#1#2]}\gdef\cite{\@ifnextchar[{\AucTeX@cite{, }}{\AucTeX@cite{}[]}}}

\message{ !name(pt.tex) !offset(-139) }
\section{A Deep Embedding of \dRA\ in Isabelle/HOL}

In \cite{dawson-gore-embedding-comparing}, we describe our initial
attempts to formalise display calculi in various logical frameworks,
and describe why we chose Isabelle/HOL for this work. In this section,
we describe the Isabelle/HOL data structures used to represent
formulae, structures, sequents and derivations.

\subsection{Representing Formulae, Structures, Sequents and Rules}
\cc{pt.tex}

\begin{figure}[t]
  \centering
\begin{verbatim}
datatype formula = Btimes formula formula ("_ && _" [68,68] 67)
                 | Rtimes formula formula ("_ oo _" [68,68] 67)
                 | Bplus formula formula ("_ v _" [64,64] 63)
                 | Rplus formula formula ("_ ++ _" [64,64] 63)
                 | Bneg formula ("--_" [70] 70)
                 | Rneg formula ("_^" [75] 75)
                 | Btrue ("T")
                 | Bfalse("F")
                 | Rtrue ("r1")
                 | Rfalse("r0")
                 | FV string 
                 | PP string 
\end{verbatim}
  \caption{Isabelle/HOL Representation of Formulae of \dRA.}
  \label{fig:isabelle-formulae}
\end{figure}

Formulae of \dRA\ are represented by the datatype declaration shown in
Figure~\ref{fig:isabelle-formulae}. The constructors \texttt{FV} and
\texttt{SV} represent formula and structure variables which appear in
the statement of a rule or theorem, and which are instantiated to
actual formulae of \dRA\ when constructing derivations.  The
constructor \texttt{PP} represents a primitive proposition $p_i$,
which is not amenable to substitution.  When we reason about
substitution of arbitrary structures or formulae for variables (for
example, in a rule), we use these variables.  Thus we find these
variables in the statements of the rules of the object logic.
Accordingly, it is an axiom of our meta-logic that a derivation in the
object logic may use substitutions (instantiations) of the object
logic rules, obtained by substituting for these variables.

\begin{figure}[t]
  \centering
\begin{verbatim}
datatype structr = Comma structr structr 
                 | SemiC structr structr 
                 | Star structr  
                 | Blob structr  
                 | I 
                 | E 
                 | Structform formula 
                 | SV string   
\end{verbatim}
  \caption{Isabelle/HOL Representation of Structures of \dRA.}
  \label{fig:isabelle-formulae}
\end{figure}

The operator \texttt{Structform} causes a formula to be ``cast'' into 
a structure.
We describe a structure expression as being \emph{formula-free} if 
it does not contain any formula as a sub-structure, that is, if it does
not contain any occurrence of the operator \texttt{Structform}.
A formula-free sequent is defined similarly.

\begin{verbatim}
datatype sequent = Sequent structr structr 

datatype rule = Rule (sequent list) sequent 
              | Bidi sequent sequent
              | InvBidi sequent sequent 
\end{verbatim}

In contrast to the variables modelled explicitly by \texttt{FV} and
\texttt{SV},
Isabelle has ``scheme variables'', identified by a preceding 
`\texttt{?}'.
When a scheme variable appears in an Isabelle theorem,
it means that the statement
is true when anything (of the appropriate type) is substituted for it.

The standard formulation of formulae in 
a display logic involves formula variables ($A, B, \ldots$)
and primitive propositions ($p, q, \ldots$), with the identity axiom 
$p \vdash p$, using primitive propositions only.
It is then proved that the sequent $A \vdash A$ is derivable
for all formulae $A$,
where $A$ \emph{stands for} a formula composed of 
primitive propositions and logical connectives.
We proved this, as the theorem \texttt{idfpp}.

However we also need to reason about the derivation trees of derived
rules; such trees may contain formula and structure variables as
well as primitive propositions, and may use the (derived) rule
$A \vdash A$, for arbitrary formula $A$.
Therefore we consider formula variables
as formulae in their own right, and treat $A \vdash A$ 
(where $A$ is a formula variable) as an axiom.

The notations in parentheses describe the syntax used.
Some complex manipulation of the syntax, available through Isabelle's
``parse translations'' and ``print translations'', allows structure variables
and constants to be prefixed by `\$', and the notations \texttt{FV},
\texttt{SV} and \texttt{Structform}
to be omitted.
For technical reasons related to this
the syntax for structures and sequents is given separately;
note that a sequent \texttt{(Sequent X Y)}
can also be represented as \texttt{\$X |- \$Y}.

Thus the term \texttt{Sequent (SV ''X'') (Structform (FV ''A''))}
is printed (and may be entered) as \texttt{(\$''X'' |- ''A'')}.

\texttt{Rule prems concl} means a rule with 
premises \texttt{prems} and conclusion \texttt{concl}.
\texttt{Bidi prem concl} means an invertible, or ``bi-directional'' rule
(such as the display postulates) and 
\texttt{InvBidi prem concl} means the rule 
\texttt{Bidi prem concl} used in the inverted sense.
There are also functions \texttt{premsRule} and \texttt{conclRule}
which return the list of premises, or the conclusion, of a rule.

\subsection{Handling Substitutions Explicitly}

We now consider the definitions relating to substitution for structure and
formula variables.
We first define some type abbreviations, and then give the types of some of
the functions.

\begin{verbatim}
types 

  fSubst = "(string * formula) list"
  sSubst = "(string * structr) list"
  fsSubst = "fSubst * sSubst"

consts

  fFind         :: "fSubst => string => formula"
  sFind         :: "sSubst => string => structr"

  subPT         :: "fsSubst => pftree => pftree"
  ruleSubst     :: "fsSubst => rule => rule"
  seqSubst      :: "fsSubst => sequent => sequent"
  strSubst      :: "fsSubst => structr => structr"
  fmlSubst      :: "fSubst => formula => formula"
\end{verbatim}

This means, for example, that \texttt{sFind} is a function of two
curried arguments, of types \texttt{sSubst} and \texttt{string},
and result type \texttt{structr}, and that \texttt{sSubst} is the
type of lists of (\texttt{string}, \texttt{structr}) pairs.
In fact, to substitute for a variable, for example \texttt{SV ''X''},
in some object, using the substitution \texttt{(fsubs, ssubs)}, 
we use \texttt{sFind} to obtain the first pair in 
\texttt{ssubs} whose first component is \texttt{''X''}.
If that pair is \texttt{(''X''}, $X$\texttt{)},
then \texttt{sFind} returns $X$, and each occurrence of 
\texttt{SV ''X''} in the given object is replaced by $X$.
The functions given substitute for every formula or structure variable in 
the derivation tree (see below), rule, sequent, structure or formula. 

\subsection{Representing Derivations as Trees}

We use the term ``derivation'' to refer to a proof \emph{within} the
sequent calculus, reserving the term ``proof'' for a metatheoretic
proof of a theorem \emph{about} the sequent calculus.

We model a derivation tree (type \texttt{pftree}) using the following datatype:

\begin{verbatim}
datatype pftree = Pr sequent rule (pftree list) 
                | Unf sequent 
\end{verbatim}

In a term \texttt{Pr seq rule pts},
the subterm \texttt{seq} is the sequent at the root (bottom) of the tree,
and \texttt{rule} is the rule used in the last (bottom) step.
Thus (if the tree represents a real derivation)
\texttt{seq} will be an instantiation of the conclusion of \texttt{rule},
and the corresponding instantiations of the premises of \texttt{rule}
will be the roots of the trees in the list \texttt{pts}.
The trees in \texttt{pts} will be called the \emph{immediate}
subtees of \texttt{Pr seq rule pts}.

The leaves of a derivation tree may be axioms or sequents which are 
left unproved. 
The derivation tree for a theorem will have no unproved leaves;
we will call such a derivation tree \emph{complete}.
The derivation tree for a derived rule will have, as its unproved leaf
sequents, the premises of the rule.
% For a derivation tree which is incomplete, an unproved leaf is modelled
An unproved leaf sequent is modelled
by the tree \texttt{Unf seq}.
%Thus the tree for a derived rule has leaves \texttt{Unf seq}
%for each \texttt{seq}
%in the set of premises of the derived rule.

For example, the derivation tree shown below at left is represented
as the Isabelle/HOL term shown below at right where \texttt{cA} and
\texttt{ands} are the contraction and ($\vdash \land $) rules, and
\texttt{idf} is the rule $A \vdash A$:\\[1em]
\begin{tabular}[c]{rr}
  \begin{minipage}[c]{0.3\linewidth}
    {\vpf
     \bpf
     \A "$A \vdash p$"
     \A "$A \vdash A$"
     \B [1em] "$A, A \vdash p \land A$" "($\vdash \land $)"
     \U "$A \vdash p \land A$" "(\textsl{ctr})"
     \epf
    }
  \end{minipage}
&
\begin{minipage}[c]{0.5\textwidth}
\begin{verbatim}
  Pr (A |- PP p && A) cA
     [Pr (A, A |- PP p && A) ands 
      [Unf (A |- PP p), Pr (A |- A) idf []]]
\end{verbatim}
\end{minipage}
\end{tabular}


\subsection{Various Properties of Derivation Trees}

In this section we describe various functions which allow us to reason
about derivations in \dRA. The types for these functions are shown in
Figure~\ref{fig:functions-reasoning-about-derivations}.

\begin{figure}[t]
  \centering
\begin{verbatim}
  allPT         :: "(pftree => bool) => pftree => bool"
  allNextPTs    :: "(pftree => bool) => pftree => bool"
  wfb           :: "pftree => bool"
  frb           :: "rule set => pftree => bool"
  premsPT       :: "pftree => sequent list"
  IsDerivable   :: "rule set => rule => bool" 
  IsDerivableR  :: "rule set => sequent set => sequent => bool" 
  IsDerivableB  :: "rule set => sequent => sequent => bool" 
\end{verbatim}
  \caption{Functions for reasoning about derivations}
  \label{fig:functions-reasoning-about-derivations}
\end{figure}


\begin{description}
  
\item[\texttt{allPT f pt}] holds if property \texttt{f} holds for
  every sub-tree in the derivation tree \texttt{pt}.
  
\item[\texttt{allNextPTs f pt}] holds if property \texttt{f} holds for
  every proper sub-tree of \texttt{pt}.

\item[\texttt{wfb (Pr concl rule pts)}] holds if sequent rule
  \texttt{rule} has an instantiation with conclusion instance
  \texttt{concl} and premise instances which are the conclusions of the
  derivation trees in the list \texttt{pts}. Such a node is said to be
  \emph{well-formed}.
  
\item[\texttt{allPT wfb pt}] holds if every sub-tree of the derivation
  tree \texttt{pt} is \emph{well-formed}.  That is, if every node in
  \texttt{pt} is well-formed.  Such a derivation is said to be
  \emph{well-formed}.
  
\item[\texttt{frb rules (Pr concl rule pts)}] holds when the lowest
  rule \texttt{rule} used in a derivation tree \texttt{Pr concl rule
    pts} belongs to the set \texttt{rules}.
  
\item[\texttt{allPT (frb rules) pt}] holds when every rule used in
  a derivation tree \texttt{pt} belongs to the set \texttt{rules}.
  
\item[\texttt{premsPT pt}] returns a list of all ``premises''
  (unproved leaves) of the derivation tree \texttt{pt}. That is, the
  sequents found in nodes of \texttt{pt} of the form \texttt{Unf seq}.

\end{description}

We call a node of a derivation tree \texttt{Pr seq rule pts}
\emph{well-formed} if the subterm \texttt{rule} can be instantiated so
that the instantiated conclusion is \texttt{seq} and the instantiated
premises are the conclusions of the trees in the list \texttt{pts}.
This property is expressed as \texttt{wfb (Pr seq rule pts)}.  We call
a derivation tree \texttt{pt} \emph{well-formed} if every node in it
is well-formed.  This is expressed as \texttt{allPT wfb pt}, as
\texttt{allPT f pt} means that property \texttt{f} holds for every
sub-tree in the derivation tree \texttt{pt}.  Also, \texttt{allNextPTs
  f pt} means that \texttt{f} holds for every proper sub-tree of
\texttt{pt}.

The property \texttt{allPT (frb rules)} holds when every rule
used in a derivation tree belongs to the set \texttt{rules}.
The function \texttt{premsPT} returns a list of all 
``premises'' (unproved assumptions) of the derivation
tree, that is, the sequents found in nodes of the form \texttt{Unf seq}.

A tree representing a real derivation in a display calculus naturally
is well-formed and uses the rules of the calculus.  Further, a tree
which derives a sequent (rather than a derived rule) is complete, that
is, it has no premises.

The cut-elimination procedure involves transformations
of derivation trees; 
in discussing these we will only be interested in 
derivation trees which actually derive a sequent, so we make the following
definition.

\begin{definition}
A derivation tree is \emph{valid} if
\begin{itemize}
\item it is well-formed,
\item it uses rules in the set of rules of the calculus, and
\item it has no premises (ie, unproved leaves).
\end{itemize}
\end{definition}

Finally, \texttt{IsDerivable rules rule} denotes that 
\texttt{rule} may be obtained as a derived rule, from the 
(unordered) set \texttt{rules}.
Thus, for example, if 
\texttt{rule} is of the form \texttt{Rule prems concl},
then \texttt{IsDerivable rules rule} is equivalent to 
\texttt{IsDerivableR rules (set prems) concl}, as defined below
(where \texttt{set prems} is the set of the members of
the list \texttt{prems}).

\begin{definition}[\texttt{IsDerivableR}]
\texttt{IsDerivableR rules prems' concl} holds iff
there exists a well-formed derivation tree \texttt{pftr}
whose premises are among 
\texttt{prems'}, whose conclusion is \texttt{concl},
and which uses only rules contained in \texttt{rules}.
\end{definition}

\begin{verbatim}
  "IsDerivableR rules prems' concl == (EX pftr.
      allPT (frb rules) pftr & allPT wfb pftr &
      conclPT pftr = concl & set (premsPT pftr) <= prems')"
\end{verbatim}

If \texttt{rule} is a bi-directional rule, say
\texttt{Bidi prem concl}, 
then \texttt{IsDerivable rules rule} is equivalent to 
\texttt{IsDerivableB rules prem concl}.

\begin{verbatim}
 "IsDerivableB rules prem concl ==
     IsDerivableR rules {prem} concl &
     IsDerivableR rules {concl} prem"
\end{verbatim}


\subsection{Theorems about Derivability}

Among the results we have proved about the provability relation  
are the following theorems.
\comment{
Note that 
\texttt{IsDerivableR rules prems concl}
means that 
conclusion \texttt{concl} is derivable from
premises \texttt{prems} using
rules \texttt{rules}
(ie, except for the type of \texttt{prems},
the same as
\texttt{IsDerivable rules (Rule prems concl)}).
}

The first is a transitivity result,
relating to a derivation of a conclusion from premises which are themselves
derived.
\begin{theorem}[\texttt{IsDerivableR\_trans}]
If \texttt{concl} is derivable from
\texttt{prems'}, and each sequent \texttt{p} in \texttt{prems'}
is derivable from \texttt{prems}, then
\texttt{concl} is derivable from \texttt{prems}. 
\end{theorem}

\begin{verbatim}
IsDerivableR_trans = 
  "[| IsDerivableR ?rules ?prems' ?concl ;  
     ALL p:?prems'. IsDerivableR ?rules ?prems p |] ==>  
     IsDerivableR ?rules ?prems ?concl" 
\end{verbatim}

The second is a a different sort of transitivity result,
relating to a derivation using rules which are themselves derived.
\begin{theorem}[\texttt{IsDerivableR\_deriv}]
If \texttt{concl} is derivable from \texttt{prems} using 
the set \texttt{rules'},
and each \texttt{rule} in \texttt{rules'}
is derivable using \texttt{rules}, then
\texttt{concl} is derivable from \texttt{prems} using \texttt{rules}.
\end{theorem}

\begin{verbatim}
IsDerivableR_deriv = 
  "[| ALL rule:?rules'. IsDerivable ?rules rule ;  
      IsDerivableR ?rules' ?prems ?concl |] ==>  
      IsDerivableR ?rules ?prems ?concl"
\end{verbatim}

We note that in another reported formalization of the notion of
derivations in a logical calculus \cite{mikhajlova-vonwright-isomorphism},
these two properties were, in effect, stated rather than proved.
The disadvantage of proceeding that way is the possiblity of stating 
them incorrectly.
For example, in the paper cited, on p.~302,
a relation \texttt{IsDerivable} is defined
inductively to be a relation which is transitive in both the senses 
of the results above (see the second and third clauses of the definition).
However in the third clause, which deals with the case of a result being
provable using derived rules, inappropriate use
of an existential quantifier leads to the result that $P \to Q$
could be used as a derived rule on the grounds that one
instance of it, say $\textsl{True} \to \textsl{True}$, is provable.

Finally we have a recursive characterization of derivability.
Here, 
\texttt{ruleFromSet rule rules} means that \texttt{rule}
is an instantiation of a rule in \texttt{rules}
(which may be the inverse sense of a bi-directional rule).

\begin{theorem}[\texttt{IsDerivableR\_recur}]
A conclusion \texttt{concl} is derivable from premises \texttt{prems}
using rules \texttt{rules} if and only if either \texttt{concl} is one of
\texttt{prems} or there is an instantiated rule \texttt{rule}
obtained from \texttt{rules}
and the conclusion of \texttt{rule} is \texttt{concl} 
and the premises of \texttt{rule} are themselves
derivable from \texttt{prems} using \texttt{rules}.
\end{theorem}

\begin{verbatim}
IsDerivableR_recur = 
  "IsDerivableR ?rules ?prems ?concl =
      (?concl : ?prems 
    | (EX rule. ruleFromSet rule ?rules & conclRule rule = ?concl
      & (ALL p : set (premsRule rule). IsDerivableR ?rules ?prems p)))"
\end{verbatim}


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

\message{ !name(ce.tex) !offset(-364) }

\end{document}