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