Logics/document/Sequents.tex

\chapter{Defining A Sequent-Based Logic}
\label{chap:sequents}

\underscoreon %this file contains the @ character

The Isabelle theory \texttt{Sequents.thy} provides facilities for using
sequent notation in users' object logics. This theory allows users to
easily interface the surface syntax of sequences with an underlying
representation suitable for higher-order unification.

\section{Concrete syntax of sequences}

Mathematicians and logicians have used sequences in an informal way
much before proof systems such as Isabelle were created. It seems
sensible to allow people using Isabelle to express sequents and
perform proofs in this same informal way, and without requiring the
theory developer to spend a lot of time in \ML{} programming.

By using {\tt Sequents.thy}
appropriately, a logic developer can allow users to refer to sequences
in several ways:
%
\begin{itemize}
\item A sequence variable is any alphanumeric string with the first
 character being a \verb%$% sign.
So, consider the sequent \verb%$A |- B%, where \verb%$A%
is intended to match a sequence of zero or more items.

\item A sequence with unspecified sub-sequences and unspecified or
individual items is written as a comma-separated list of regular
variables (representing items), particular items, and
sequence variables, as in
\begin{ttbox}
$A, B, C, $D(x) |- E
\end{ttbox}
Here both \verb%$A% and \verb%$D(x)%
are allowed to match any subsequences of items on either side of the
two items that match $B$ and $C$.  Moreover, the sequence matching
\verb%$D(x)% may contain occurrences of~$x$.

\item An empty sequence can be represented by a blank space, as in
\verb? |- true?.
\end{itemize}

These syntactic constructs need to be assimilated into the object
theory being developed. The type that we use for these visible objects
is given the name {\tt seq}.
A {\tt seq} is created either by the empty space, a {\tt seqobj} or a
{\tt seqobj} followed by a {\tt seq}, with a comma between them. A
{\tt seqobj} is either an item or a variable representing a
sequence. Thus, a theory designer can specify a function that takes
two sequences and returns a meta-level proposition by giving it the
Isabelle type \verb|[seq, seq] => prop|.

This is all part of the concrete syntax, but one may wish to
exploit Isabelle's higher-order abstract syntax by actually having a
different, more powerful {\em internal} syntax.


\section{ Basis}

One could opt to represent sequences as first-order objects (such as
simple lists), but this would not allow us to use many facilities
Isabelle provides for matching.  By using a slightly more complex
representation, users of the logic can reap many benefits in
facilities for proofs and ease of reading logical terms.

A sequence can be represented as a function --- a constructor for
further sequences --- by defining a binary {\em abstract} function
\verb|Seq0'| with type \verb|[o,seq']=>seq'|, and translating a
sequence such as \verb|A, B, C| into
\begin{ttbox}
\%s. Seq0'(A, SeqO'(B, SeqO'(C, s)))
\end{ttbox}
This sequence can therefore be seen as a constructor
for further sequences. The constructor \verb|Seq0'| is never given a
value, and therefore it is not possible to evaluate this expression
into a basic value.

Furthermore, if we want to represent the sequence \verb|A, $B, C|,
we note that \verb|$B| already represents a sequence, so we can use
\verb|B| itself to refer to the function, and therefore the sequence
can be mapped to the internal form:
\verb|%s. SeqO'(A, B(SeqO'(C, s)))|.

So, while we wish to continue with the standard, well-liked {\em
external} representation of sequences, we can represent them {\em
internally} as functions of type \verb|seq'=>seq'|.


\section{Object logics}

Recall that object logics are defined by mapping elements of
particular types to the Isabelle type \verb|prop|, usually with a
function called {\tt Trueprop}. So, an object
logic proposition {\tt P} is matched to the Isabelle proposition
{\tt Trueprop(P)}\@.  The name of the function is often hidden, so the
user just sees {\tt P}\@. Isabelle is eager to make types match, so it
inserts {\tt Trueprop} automatically when an object of type {\tt prop}
is expected. This mechanism can be observed in most of the object
logics which are direct descendants of {\tt Pure}.

In order to provide the desired syntactic facilities for sequent
calculi, rather than use just one function that maps object-level
propositions to meta-level propositions, we use two functions, and
separate internal from the external representation.

These functions need to be given a type that is appropriate for the particular
form of sequents required: single or multiple conclusions.  So
multiple-conclusion sequents (used in the LK logic) can be
specified by the following two definitions, which are lifted from the inbuilt
{\tt Sequents/LK.thy}:
\begin{ttbox}
 Trueprop       :: two_seqi
 "@Trueprop"    :: two_seqe   ("((_)/ |- (_))" [6,6] 5)
\end{ttbox}
%
where the types used are defined in {\tt Sequents.thy} as
abbreviations:
\begin{ttbox}
 two_seqi = [seq'=>seq', seq'=>seq'] => prop
 two_seqe = [seq, seq] => prop
\end{ttbox}

The next step is to actually create links into the low-level parsing
and pretty-printing mechanisms, which map external and internal
representations. These functions go below the user level and capture
the underlying structure of Isabelle terms in \ML{}\@.  Fortunately the
theory developer need not delve in this level; {\tt Sequents.thy}
provides the necessary facilities. All the theory developer needs to
add in the \ML{} section is a specification of the two translation
functions:
\begin{ttbox}
ML
val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")];
val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];
\end{ttbox}

In summary: in the logic theory being developed, the developer needs
to specify the types for the internal and external representation of
the sequences, and use the appropriate parsing and pretty-printing
functions.

\section{What's in \texttt{Sequents.thy}}

Theory \texttt{Sequents.thy} makes many declarations that you need to know
about:
\begin{enumerate}
\item The Isabelle types given below, which can be used for the
constants that map object-level sequents and meta-level propositions:
%
\begin{ttbox}
 single_seqe = [seq,seqobj] => prop
 single_seqi = [seq'=>seq',seq'=>seq'] => prop
 two_seqi    = [seq'=>seq', seq'=>seq'] => prop
 two_seqe    = [seq, seq] => prop
 three_seqi  = [seq'=>seq', seq'=>seq', seq'=>seq'] => prop
 three_seqe  = [seq, seq, seq] => prop
 four_seqi   = [seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop
 four_seqe   = [seq, seq, seq, seq] => prop
\end{ttbox}

The \verb|single_| and \verb|two_| sets of mappings for internal and
external representations are the ones used for, say single and
multiple conclusion sequents. The other functions are provided to
allow rules that manipulate more than two functions, as can be seen in
the inbuilt object logics.

\item An auxiliary syntactic constant has been
defined that directly maps a sequence to its internal representation:
\begin{ttbox}
"@Side"  :: seq=>(seq'=>seq')     ("<<(_)>>")
\end{ttbox}
Whenever a sequence (such as \verb|<< A, $B, $C>>|) is entered using this
syntax, it is translated into the appropriate internal representation.  This
form can be used only where a sequence is expected.

\item The \ML{} functions \texttt{single\_tr}, \texttt{two\_seq\_tr},
  \texttt{three\_seq\_tr}, \texttt{four\_seq\_tr} for parsing, that is, the
  translation from external to internal form.  Analogously there are
  \texttt{single\_tr'}, \texttt{two\_seq\_tr'}, \texttt{three\_seq\_tr'},
  \texttt{four\_seq\_tr'} for pretty-printing, that is, the translation from
  internal to external form.  These functions can be used in the \ML{} section
  of a theory file to specify the translations to be used.  As an example of
  use, note that in {\tt LK.thy} we declare two identifiers:
\begin{ttbox}
val parse_translation =
    [("@Trueprop",Sequents.two_seq_tr "Trueprop")];
val print_translation =
    [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];
\end{ttbox}
The given parse translation will be applied whenever a \verb|@Trueprop|
constant is found, translating using \verb|two_seq_tr| and inserting the
constant \verb|Trueprop|.  The pretty-printing translation is applied
analogously; a term that contains \verb|Trueprop| is printed as a
\verb|@Trueprop|.
\end{enumerate}