7160

1 
%% $Id$


2 
\chapter{Defining A SequentBased Logic}


3 
\label{chap:sequents}


4 


5 
\underscoreon %this file contains the @ character


6 


7 
The Isabelle theory \texttt{Sequents.thy} provides facilities for using


8 
sequent notation in users' object logics. This theory allows users to


9 
easily interface the surface syntax of sequences with an underlying


10 
representation suitable for higherorder unification.


11 


12 
\section{Concrete syntax of sequences}


13 


14 
Mathematicians and logicians have used sequences in an informal way


15 
much before proof systems such as Isabelle were created. It seems


16 
sensible to allow people using Isabelle to express sequents and


17 
perform proofs in this same informal way, and without requiring the


18 
theory developer to spend a lot of time in \ML{} programming.


19 


20 
By using {\tt Sequents.thy}


21 
appropriately, a logic developer can allow users to refer to sequences


22 
in several ways:


23 
%


24 
\begin{itemize}


25 
\item A sequence variable is any alphanumeric string with the first


26 
character being a \verb%$% sign.


27 
So, consider the sequent \verb%$A  B%, where \verb%$A%


28 
is intended to match a sequence of zero or more items.


29 


30 
\item A sequence with unspecified subsequences and unspecified or


31 
individual items is written as a commaseparated list of regular


32 
variables (representing items), particular items, and


33 
sequence variables, as in


34 
\begin{ttbox}


35 
$A, B, C, $D(x)  E


36 
\end{ttbox}


37 
Here both \verb%$A% and \verb%$D(x)%


38 
are allowed to match any subsequences of items on either side of the


39 
two items that match $B$ and $C$. Moreover, the sequence matching


40 
\verb%$D(x)% may contain occurrences of~$x$.


41 


42 
\item An empty sequence can be represented by a blank space, as in


43 
\verb?  true?.


44 
\end{itemize}


45 


46 
These syntactic constructs need to be assimilated into the object


47 
theory being developed. The type that we use for these visible objects


48 
is given the name {\tt seq}.


49 
A {\tt seq} is created either by the empty space, a {\tt seqobj} or a


50 
{\tt seqobj} followed by a {\tt seq}, with a comma between them. A


51 
{\tt seqobj} is either an item or a variable representing a


52 
sequence. Thus, a theory designer can specify a function that takes


53 
two sequences and returns a metalevel proposition by giving it the


54 
Isabelle type \verb[seq, seq] => prop.


55 


56 
This is all part of the concrete syntax, but one may wish to


57 
exploit Isabelle's higherorder abstract syntax by actually having a


58 
different, more powerful {\em internal} syntax.


59 


60 


61 


62 
\section{ Basis}


63 


64 
One could opt to represent sequences as firstorder objects (such as


65 
simple lists), but this would not allow us to use many facilities


66 
Isabelle provides for matching. By using a slightly more complex


67 
representation, users of the logic can reap many benefits in


68 
facilities for proofs and ease of reading logical terms.


69 


70 
A sequence can be represented as a function  a constructor for


71 
further sequences  by defining a binary {\em abstract} function


72 
\verbSeq0' with type \verb[o,seq']=>seq', and translating a


73 
sequence such as \verbA, B, C into


74 
\begin{ttbox}


75 
\%s. Seq0'(A, SeqO'(B, SeqO'(C, s)))


76 
\end{ttbox}


77 
This sequence can therefore be seen as a constructor


78 
for further sequences. The constructor \verbSeq0' is never given a


79 
value, and therefore it is not possible to evaluate this expression


80 
into a basic value.


81 


82 
Furthermore, if we want to represent the sequence \verbA, $B, C,


83 
we note that \verb$B already represents a sequence, so we can use


84 
\verbB itself to refer to the function, and therefore the sequence


85 
can be mapped to the internal form:


86 
\verb%s. SeqO'(A, B(SeqO'(C, s))).


87 


88 
So, while we wish to continue with the standard, wellliked {\em


89 
external} representation of sequences, we can represent them {\em


90 
internally} as functions of type \verbseq'=>seq'.


91 


92 


93 
\section{Object logics}


94 


95 
Recall that object logics are defined by mapping elements of


96 
particular types to the Isabelle type \verbprop, usually with a


97 
function called {\tt Trueprop}. So, an object


98 
logic proposition {\tt P} is matched to the Isabelle proposition


99 
{\tt Trueprop(P)}\@. The name of the function is often hidden, so the


100 
user just sees {\tt P}\@. Isabelle is eager to make types match, so it


101 
inserts {\tt Trueprop} automatically when an object of type {\tt prop}


102 
is expected. This mechanism can be observed in most of the object


103 
logics which are direct descendants of {\tt Pure}.


104 


105 
In order to provide the desired syntactic facilities for sequent


106 
calculi, rather than use just one function that maps objectlevel


107 
propositions to metalevel propositions, we use two functions, and


108 
separate internal from the external representation.


109 


110 
These functions need to be given a type that is appropriate for the particular


111 
form of sequents required: single or multiple conclusions. So


112 
multipleconclusion sequents (used in the LK logic) can be


113 
specified by the following two definitions, which are lifted from the inbuilt


114 
{\tt Sequents/LK.thy}:


115 
\begin{ttbox}


116 
Trueprop :: two_seqi


117 
"@Trueprop" :: two_seqe ("((_)/  (_))" [6,6] 5)


118 
\end{ttbox}


119 
%


120 
where the types used are defined in {\tt Sequents.thy} as


121 
abbreviations:


122 
\begin{ttbox}


123 
two_seqi = [seq'=>seq', seq'=>seq'] => prop


124 
two_seqe = [seq, seq] => prop


125 
\end{ttbox}


126 


127 
The next step is to actually create links into the lowlevel parsing


128 
and prettyprinting mechanisms, which map external and internal


129 
representations. These functions go below the user level and capture


130 
the underlying structure of Isabelle terms in \ML{}\@. Fortunately the


131 
theory developer need not delve in this level; {\tt Sequents.thy}


132 
provides the necessary facilities. All the theory developer needs to


133 
add in the \ML{} section is a specification of the two translation


134 
functions:


135 
\begin{ttbox}


136 
ML


137 
val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")];


138 
val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];


139 
\end{ttbox}


140 


141 
In summary: in the logic theory being developed, the developer needs


142 
to specify the types for the internal and external representation of


143 
the sequences, and use the appropriate parsing and prettyprinting


144 
functions.


145 


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


147 


148 
Theory \texttt{Sequents.thy} makes many declarations that you need to know


149 
about:


150 
\begin{enumerate}


151 
\item The Isabelle types given below, which can be used for the


152 
constants that map objectlevel sequents and metalevel propositions:


153 
%


154 
\begin{ttbox}


155 
single_seqe = [seq,seqobj] => prop


156 
single_seqi = [seq'=>seq',seq'=>seq'] => prop


157 
two_seqi = [seq'=>seq', seq'=>seq'] => prop


158 
two_seqe = [seq, seq] => prop


159 
three_seqi = [seq'=>seq', seq'=>seq', seq'=>seq'] => prop


160 
three_seqe = [seq, seq, seq] => prop


161 
four_seqi = [seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop


162 
four_seqe = [seq, seq, seq, seq] => prop


163 
\end{ttbox}


164 


165 
The \verbsingle_ and \verbtwo_ sets of mappings for internal and


166 
external representations are the ones used for, say single and


167 
multiple conclusion sequents. The other functions are provided to


168 
allow rules that manipulate more than two functions, as can be seen in


169 
the inbuilt object logics.


170 


171 
\item An auxiliary syntactic constant has been


172 
defined that directly maps a sequence to its internal representation:


173 
\begin{ttbox}


174 
"@Side" :: seq=>(seq'=>seq') ("<<(_)>>")


175 
\end{ttbox}


176 
Whenever a sequence (such as \verb<< A, $B, $C>>) is entered using this


177 
syntax, it is translated into the appropriate internal representation. This


178 
form can be used only where a sequence is expected.


179 


180 
\item The \ML{} functions \texttt{single\_tr}, \texttt{two\_seq\_tr},


181 
\texttt{three\_seq\_tr}, \texttt{four\_seq\_tr} for parsing, that is, the


182 
translation from external to internal form. Analogously there are


183 
\texttt{single\_tr'}, \texttt{two\_seq\_tr'}, \texttt{three\_seq\_tr'},


184 
\texttt{four\_seq\_tr'} for prettyprinting, that is, the translation from


185 
internal to external form. These functions can be used in the \ML{} section


186 
of a theory file to specify the translations to be used. As an example of


187 
use, note that in {\tt LK.thy} we declare two identifiers:


188 
\begin{ttbox}


189 
val parse_translation =


190 
[("@Trueprop",Sequents.two_seq_tr "Trueprop")];


191 
val print_translation =


192 
[("Trueprop",Sequents.two_seq_tr' "@Trueprop")];


193 
\end{ttbox}


194 
The given parse translation will be applied whenever a \verb@Trueprop


195 
constant is found, translating using \verbtwo_seq_tr and inserting the


196 
constant \verbTrueprop. The prettyprinting translation is applied


197 
analogously; a term that contains \verbTrueprop is printed as a


198 
\verb@Trueprop.


199 
\end{enumerate}


200 


201 
