paulson@7160: %% $Id$
paulson@7160: \chapter{Defining A Sequent-Based Logic}
paulson@7160: \label{chap:sequents}
paulson@7160: 
paulson@7160: \underscoreon %this file contains the @ character
paulson@7160: 
paulson@7160: The Isabelle theory \texttt{Sequents.thy} provides facilities for using
paulson@7160: sequent notation in users' object logics. This theory allows users to
paulson@7160: easily interface the surface syntax of sequences with an underlying
paulson@7160: representation suitable for higher-order unification.
paulson@7160: 
paulson@7160: \section{Concrete syntax of sequences}
paulson@7160: 
paulson@7160: Mathematicians and logicians have used sequences in an informal way
paulson@7160: much before proof systems such as Isabelle were created. It seems
paulson@7160: sensible to allow people using Isabelle to express sequents and
paulson@7160: perform proofs in this same informal way, and without requiring the
paulson@7160: theory developer to spend a lot of time in \ML{} programming.
paulson@7160: 
paulson@7160: By using {\tt Sequents.thy}
paulson@7160: appropriately, a logic developer can allow users to refer to sequences
paulson@7160: in several ways:
paulson@7160: %
paulson@7160: \begin{itemize}
paulson@7160: \item A sequence variable is any alphanumeric string with the first
paulson@7160:  character being a \verb%$% sign. 
paulson@7160: So, consider the sequent \verb%$A |- B%, where \verb%$A%
paulson@7160: is intended to match a sequence of zero or more items.
paulson@7160:  
paulson@7160: \item A sequence with unspecified sub-sequences and unspecified or
paulson@7160: individual items is written as a comma-separated list of regular
paulson@7160: variables (representing items), particular items, and
paulson@7160: sequence variables, as in  
paulson@7160: \begin{ttbox}
paulson@7160: $A, B, C, $D(x) |- E
paulson@7160: \end{ttbox}
paulson@7160: Here both \verb%$A% and \verb%$D(x)%
paulson@7160: are allowed to match any subsequences of items on either side of the
paulson@7160: two items that match $B$ and $C$.  Moreover, the sequence matching
paulson@7160: \verb%$D(x)% may contain occurrences of~$x$.
paulson@7160: 
paulson@7160: \item An empty sequence can be represented by a blank space, as in
paulson@7160: \verb? |- true?.
paulson@7160: \end{itemize}
paulson@7160: 
paulson@7160: These syntactic constructs need to be assimilated into the object
paulson@7160: theory being developed. The type that we use for these visible objects
paulson@7160: is given the name {\tt seq}.
paulson@7160: A {\tt seq} is created either by the empty space, a {\tt seqobj} or a
paulson@7160: {\tt seqobj} followed by a {\tt seq}, with a comma between them. A
paulson@7160: {\tt seqobj} is either an item or a variable representing a
paulson@7160: sequence. Thus, a theory designer can specify a function that takes
paulson@7160: two sequences and returns a meta-level proposition by giving it the
paulson@7160: Isabelle type \verb|[seq, seq] => prop|.
paulson@7160: 
paulson@7160: This is all part of the concrete syntax, but one may wish to
paulson@7160: exploit Isabelle's higher-order abstract syntax by actually having a
paulson@7160: different, more powerful {\em internal} syntax.
paulson@7160: 
paulson@7160: 
paulson@7160: 
paulson@7160: \section{ Basis}
paulson@7160: 
paulson@7160: One could opt to represent sequences as first-order objects (such as
paulson@7160: simple lists), but this would not allow us to use many facilities
paulson@7160: Isabelle provides for matching.  By using a slightly more complex
paulson@7160: representation, users of the logic can reap many benefits in
paulson@7160: facilities for proofs and ease of reading logical terms.
paulson@7160: 
paulson@7160: A sequence can be represented as a function --- a constructor for
paulson@7160: further sequences --- by defining a binary {\em abstract} function
paulson@7160: \verb|Seq0'| with type \verb|[o,seq']=>seq'|, and translating a
paulson@7160: sequence such as \verb|A, B, C| into
paulson@7160: \begin{ttbox}
paulson@7160: \%s. Seq0'(A, SeqO'(B, SeqO'(C, s)))  
paulson@7160: \end{ttbox}
paulson@7160: This sequence can therefore be seen as a constructor 
paulson@7160: for further sequences. The constructor \verb|Seq0'| is never given a
paulson@7160: value, and therefore it is not possible to evaluate this expression
paulson@7160: into a basic value.
paulson@7160: 
paulson@7160: Furthermore, if we want to represent the sequence \verb|A, $B, C|,
paulson@7160: we note that \verb|$B| already represents a sequence, so we can use
paulson@7160: \verb|B| itself to refer to the function, and therefore the sequence
paulson@7160: can be mapped to the internal form:
paulson@7160: \verb|%s. SeqO'(A, B(SeqO'(C, s)))|.
paulson@7160: 
paulson@7160: So, while we wish to continue with the standard, well-liked {\em
paulson@7160: external} representation of sequences, we can represent them {\em
paulson@7160: internally} as functions of type \verb|seq'=>seq'|.
paulson@7160: 
paulson@7160: 
paulson@7160: \section{Object logics}
paulson@7160: 
paulson@7160: Recall that object logics are defined by mapping elements of
paulson@7160: particular types to the Isabelle type \verb|prop|, usually with a
paulson@7160: function called {\tt Trueprop}. So, an object
paulson@7160: logic proposition {\tt P} is matched to the Isabelle proposition
paulson@7160: {\tt Trueprop(P)}\@.  The name of the function is often hidden, so the
paulson@7160: user just sees {\tt P}\@. Isabelle is eager to make types match, so it
paulson@7160: inserts {\tt Trueprop} automatically when an object of type {\tt prop}
paulson@7160: is expected. This mechanism can be observed in most of the object
paulson@7160: logics which are direct descendants of {\tt Pure}.
paulson@7160: 
paulson@7160: In order to provide the desired syntactic facilities for sequent
paulson@7160: calculi, rather than use just one function that maps object-level
paulson@7160: propositions to meta-level propositions, we use two functions, and
paulson@7160: separate internal from the external representation. 
paulson@7160: 
paulson@7160: These functions need to be given a type that is appropriate for the particular
paulson@7160: form of sequents required: single or multiple conclusions.  So
paulson@7160: multiple-conclusion sequents (used in the LK logic) can be
paulson@7160: specified by the following two definitions, which are lifted from the inbuilt
paulson@7160: {\tt Sequents/LK.thy}:
paulson@7160: \begin{ttbox}
paulson@7160:  Trueprop       :: two_seqi
paulson@7160:  "@Trueprop"    :: two_seqe   ("((_)/ |- (_))" [6,6] 5)
paulson@7160: \end{ttbox}
paulson@7160: %
paulson@7160: where the types used are defined in {\tt Sequents.thy} as
paulson@7160: abbreviations:
paulson@7160: \begin{ttbox}
paulson@7160:  two_seqi = [seq'=>seq', seq'=>seq'] => prop
paulson@7160:  two_seqe = [seq, seq] => prop
paulson@7160: \end{ttbox}
paulson@7160: 
paulson@7160: The next step is to actually create links into the low-level parsing
paulson@7160: and pretty-printing mechanisms, which map external and internal
paulson@7160: representations. These functions go below the user level and capture
paulson@7160: the underlying structure of Isabelle terms in \ML{}\@.  Fortunately the
paulson@7160: theory developer need not delve in this level; {\tt Sequents.thy}
paulson@7160: provides the necessary facilities. All the theory developer needs to
paulson@7160: add in the \ML{} section is a specification of the two translation
paulson@7160: functions:
paulson@7160: \begin{ttbox}
paulson@7160: ML
paulson@7160: val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")];
paulson@7160: val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];
paulson@7160: \end{ttbox}
paulson@7160: 
paulson@7160: In summary: in the logic theory being developed, the developer needs
paulson@7160: to specify the types for the internal and external representation of
paulson@7160: the sequences, and use the appropriate parsing and pretty-printing
paulson@7160: functions. 
paulson@7160: 
paulson@7160: \section{What's in \texttt{Sequents.thy}}
paulson@7160: 
paulson@7160: Theory \texttt{Sequents.thy} makes many declarations that you need to know
paulson@7160: about: 
paulson@7160: \begin{enumerate}
paulson@7160: \item The Isabelle types given below, which can be used for the
paulson@7160: constants that map object-level sequents and meta-level propositions:
paulson@7160: %
paulson@7160: \begin{ttbox}
paulson@7160:  single_seqe = [seq,seqobj] => prop
paulson@7160:  single_seqi = [seq'=>seq',seq'=>seq'] => prop
paulson@7160:  two_seqi    = [seq'=>seq', seq'=>seq'] => prop
paulson@7160:  two_seqe    = [seq, seq] => prop
paulson@7160:  three_seqi  = [seq'=>seq', seq'=>seq', seq'=>seq'] => prop
paulson@7160:  three_seqe  = [seq, seq, seq] => prop
paulson@7160:  four_seqi   = [seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop
paulson@7160:  four_seqe   = [seq, seq, seq, seq] => prop
paulson@7160: \end{ttbox}
paulson@7160: 
paulson@7160: The \verb|single_| and \verb|two_| sets of mappings for internal and
paulson@7160: external representations are the ones used for, say single and
paulson@7160: multiple conclusion sequents. The other functions are provided to
paulson@7160: allow rules that manipulate more than two functions, as can be seen in
paulson@7160: the inbuilt object logics.
paulson@7160: 
paulson@7160: \item An auxiliary syntactic constant has been
paulson@7160: defined that directly maps a sequence to its internal representation:
paulson@7160: \begin{ttbox}
paulson@7160: "@Side"  :: seq=>(seq'=>seq')     ("<<(_)>>")
paulson@7160: \end{ttbox}
paulson@7160: Whenever a sequence (such as \verb|<< A, $B, $C>>|) is entered using this
paulson@7160: syntax, it is translated into the appropriate internal representation.  This
paulson@7160: form can be used only where a sequence is expected.
paulson@7160: 
paulson@7160: \item The \ML{} functions \texttt{single\_tr}, \texttt{two\_seq\_tr},
paulson@7160:   \texttt{three\_seq\_tr}, \texttt{four\_seq\_tr} for parsing, that is, the
paulson@7160:   translation from external to internal form.  Analogously there are
paulson@7160:   \texttt{single\_tr'}, \texttt{two\_seq\_tr'}, \texttt{three\_seq\_tr'},
paulson@7160:   \texttt{four\_seq\_tr'} for pretty-printing, that is, the translation from
paulson@7160:   internal to external form.  These functions can be used in the \ML{} section
paulson@7160:   of a theory file to specify the translations to be used.  As an example of
paulson@7160:   use, note that in {\tt LK.thy} we declare two identifiers:
paulson@7160: \begin{ttbox}
paulson@7160: val parse_translation =
paulson@7160:     [("@Trueprop",Sequents.two_seq_tr "Trueprop")];
paulson@7160: val print_translation =
paulson@7160:     [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];
paulson@7160: \end{ttbox}
paulson@7160: The given parse translation will be applied whenever a \verb|@Trueprop|
paulson@7160: constant is found, translating using \verb|two_seq_tr| and inserting the
paulson@7160: constant \verb|Trueprop|.  The pretty-printing translation is applied
paulson@7160: analogously; a term that contains \verb|Trueprop| is printed as a
paulson@7160: \verb|@Trueprop|.
paulson@7160: \end{enumerate}
paulson@7160: 
paulson@7160: