1\chapter{Defining A Sequent-Based Logic} 2\label{chap:sequents} 3 4\underscoreon %this file contains the @ character 5 6The Isabelle theory \texttt{Sequents.thy} provides facilities for using 7sequent notation in users' object logics. This theory allows users to 8easily interface the surface syntax of sequences with an underlying 9representation suitable for higher-order unification. 10 11\section{Concrete syntax of sequences} 12 13Mathematicians and logicians have used sequences in an informal way 14much before proof systems such as Isabelle were created. It seems 15sensible to allow people using Isabelle to express sequents and 16perform proofs in this same informal way, and without requiring the 17theory developer to spend a lot of time in \ML{} programming. 18 19By using {\tt Sequents.thy} 20appropriately, a logic developer can allow users to refer to sequences 21in several ways: 22% 23\begin{itemize} 24\item A sequence variable is any alphanumeric string with the first 25 character being a \verb%$% sign. 26So, consider the sequent \verb%$A |- B%, where \verb%$A% 27is intended to match a sequence of zero or more items. 28 29\item A sequence with unspecified sub-sequences and unspecified or 30individual items is written as a comma-separated list of regular 31variables (representing items), particular items, and 32sequence variables, as in 33\begin{ttbox} 34$A, B, C, $D(x) |- E 35\end{ttbox} 36Here both \verb%$A% and \verb%$D(x)% 37are allowed to match any subsequences of items on either side of the 38two items that match $B$ and $C$. Moreover, the sequence matching 39\verb%$D(x)% may contain occurrences of~$x$. 40 41\item An empty sequence can be represented by a blank space, as in 42\verb? |- true?. 43\end{itemize} 44 45These syntactic constructs need to be assimilated into the object 46theory being developed. The type that we use for these visible objects 47is given the name {\tt seq}. 48A {\tt seq} is created either by the empty space, a {\tt seqobj} or a 49{\tt seqobj} followed by a {\tt seq}, with a comma between them. A 50{\tt seqobj} is either an item or a variable representing a 51sequence. Thus, a theory designer can specify a function that takes 52two sequences and returns a meta-level proposition by giving it the 53Isabelle type \verb|[seq, seq] => prop|. 54 55This is all part of the concrete syntax, but one may wish to 56exploit Isabelle's higher-order abstract syntax by actually having a 57different, more powerful {\em internal} syntax. 58 59 60 61\section{ Basis} 62 63One could opt to represent sequences as first-order objects (such as 64simple lists), but this would not allow us to use many facilities 65Isabelle provides for matching. By using a slightly more complex 66representation, users of the logic can reap many benefits in 67facilities for proofs and ease of reading logical terms. 68 69A sequence can be represented as a function --- a constructor for 70further sequences --- by defining a binary {\em abstract} function 71\verb|Seq0'| with type \verb|[o,seq']=>seq'|, and translating a 72sequence such as \verb|A, B, C| into 73\begin{ttbox} 74\%s. Seq0'(A, SeqO'(B, SeqO'(C, s))) 75\end{ttbox} 76This sequence can therefore be seen as a constructor 77for further sequences. The constructor \verb|Seq0'| is never given a 78value, and therefore it is not possible to evaluate this expression 79into a basic value. 80 81Furthermore, if we want to represent the sequence \verb|A, $B, C|, 82we note that \verb|$B| already represents a sequence, so we can use 83\verb|B| itself to refer to the function, and therefore the sequence 84can be mapped to the internal form: 85\verb|%s. SeqO'(A, B(SeqO'(C, s)))|. 86 87So, while we wish to continue with the standard, well-liked {\em 88external} representation of sequences, we can represent them {\em 89internally} as functions of type \verb|seq'=>seq'|. 90 91 92\section{Object logics} 93 94Recall that object logics are defined by mapping elements of 95particular types to the Isabelle type \verb|prop|, usually with a 96function called {\tt Trueprop}. So, an object 97logic proposition {\tt P} is matched to the Isabelle proposition 98{\tt Trueprop(P)}\@. The name of the function is often hidden, so the 99user just sees {\tt P}\@. Isabelle is eager to make types match, so it 100inserts {\tt Trueprop} automatically when an object of type {\tt prop} 101is expected. This mechanism can be observed in most of the object 102logics which are direct descendants of {\tt Pure}. 103 104In order to provide the desired syntactic facilities for sequent 105calculi, rather than use just one function that maps object-level 106propositions to meta-level propositions, we use two functions, and 107separate internal from the external representation. 108 109These functions need to be given a type that is appropriate for the particular 110form of sequents required: single or multiple conclusions. So 111multiple-conclusion sequents (used in the LK logic) can be 112specified by the following two definitions, which are lifted from the inbuilt 113{\tt Sequents/LK.thy}: 114\begin{ttbox} 115 Trueprop :: two_seqi 116 "@Trueprop" :: two_seqe ("((_)/ |- (_))" [6,6] 5) 117\end{ttbox} 118% 119where the types used are defined in {\tt Sequents.thy} as 120abbreviations: 121\begin{ttbox} 122 two_seqi = [seq'=>seq', seq'=>seq'] => prop 123 two_seqe = [seq, seq] => prop 124\end{ttbox} 125 126The next step is to actually create links into the low-level parsing 127and pretty-printing mechanisms, which map external and internal 128representations. These functions go below the user level and capture 129the underlying structure of Isabelle terms in \ML{}\@. Fortunately the 130theory developer need not delve in this level; {\tt Sequents.thy} 131provides the necessary facilities. All the theory developer needs to 132add in the \ML{} section is a specification of the two translation 133functions: 134\begin{ttbox} 135ML 136val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")]; 137val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")]; 138\end{ttbox} 139 140In summary: in the logic theory being developed, the developer needs 141to specify the types for the internal and external representation of 142the sequences, and use the appropriate parsing and pretty-printing 143functions. 144 145\section{What's in \texttt{Sequents.thy}} 146 147Theory \texttt{Sequents.thy} makes many declarations that you need to know 148about: 149\begin{enumerate} 150\item The Isabelle types given below, which can be used for the 151constants that map object-level sequents and meta-level propositions: 152% 153\begin{ttbox} 154 single_seqe = [seq,seqobj] => prop 155 single_seqi = [seq'=>seq',seq'=>seq'] => prop 156 two_seqi = [seq'=>seq', seq'=>seq'] => prop 157 two_seqe = [seq, seq] => prop 158 three_seqi = [seq'=>seq', seq'=>seq', seq'=>seq'] => prop 159 three_seqe = [seq, seq, seq] => prop 160 four_seqi = [seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop 161 four_seqe = [seq, seq, seq, seq] => prop 162\end{ttbox} 163 164The \verb|single_| and \verb|two_| sets of mappings for internal and 165external representations are the ones used for, say single and 166multiple conclusion sequents. The other functions are provided to 167allow rules that manipulate more than two functions, as can be seen in 168the inbuilt object logics. 169 170\item An auxiliary syntactic constant has been 171defined that directly maps a sequence to its internal representation: 172\begin{ttbox} 173"@Side" :: seq=>(seq'=>seq') ("<<(_)>>") 174\end{ttbox} 175Whenever a sequence (such as \verb|<< A, $B, $C>>|) is entered using this 176syntax, it is translated into the appropriate internal representation. This 177form can be used only where a sequence is expected. 178 179\item The \ML{} functions \texttt{single\_tr}, \texttt{two\_seq\_tr}, 180 \texttt{three\_seq\_tr}, \texttt{four\_seq\_tr} for parsing, that is, the 181 translation from external to internal form. Analogously there are 182 \texttt{single\_tr'}, \texttt{two\_seq\_tr'}, \texttt{three\_seq\_tr'}, 183 \texttt{four\_seq\_tr'} for pretty-printing, that is, the translation from 184 internal to external form. These functions can be used in the \ML{} section 185 of a theory file to specify the translations to be used. As an example of 186 use, note that in {\tt LK.thy} we declare two identifiers: 187\begin{ttbox} 188val parse_translation = 189 [("@Trueprop",Sequents.two_seq_tr "Trueprop")]; 190val print_translation = 191 [("Trueprop",Sequents.two_seq_tr' "@Trueprop")]; 192\end{ttbox} 193The given parse translation will be applied whenever a \verb|@Trueprop| 194constant is found, translating using \verb|two_seq_tr| and inserting the 195constant \verb|Trueprop|. The pretty-printing translation is applied 196analogously; a term that contains \verb|Trueprop| is printed as a 197\verb|@Trueprop|. 198\end{enumerate} 199 200 201