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