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