%% $Id$

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