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