doc-src/Logics/Sequents.tex
author haftmann
Wed Dec 27 19:10:06 2006 +0100 (2006-12-27)
changeset 21915 4e63c55f4cb4
parent 7160 1135f3f8782c
child 42637 381fdcab0f36
permissions -rw-r--r--
different handling of type variable names
     1 %% $Id$
     2 \chapter{Defining A Sequent-Based 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 higher-order 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 sub-sequences and unspecified or
    31 individual items is written as a comma-separated 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 meta-level 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 higher-order 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 first-order 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 \verb|Seq0'| with type \verb|[o,seq']=>seq'|, and translating a
    73 sequence such as \verb|A, 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 \verb|Seq0'| 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 \verb|A, $B, C|,
    83 we note that \verb|$B| already represents a sequence, so we can use
    84 \verb|B| 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, well-liked {\em
    89 external} representation of sequences, we can represent them {\em
    90 internally} as functions of type \verb|seq'=>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 \verb|prop|, 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 object-level
   107 propositions to meta-level 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 multiple-conclusion 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 low-level parsing
   128 and pretty-printing 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 pretty-printing
   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 object-level sequents and meta-level 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 \verb|single_| and \verb|two_| 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 pretty-printing, 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 \verb|two_seq_tr| and inserting the
   196 constant \verb|Trueprop|.  The pretty-printing translation is applied
   197 analogously; a term that contains \verb|Trueprop| is printed as a
   198 \verb|@Trueprop|.
   199 \end{enumerate}
   200 
   201