# HG changeset patch # User paulson # Date 933678376 -7200 # Node ID 1135f3f8782c7d4a3243c93f687c3a82311091fd # Parent b009afd1ace55a38aebe4d8eeb4eb3238a2c19c1 new chapter on Sequents diff -r b009afd1ace5 -r 1135f3f8782c doc-src/Logics/Makefile --- a/doc-src/Logics/Makefile Tue Aug 03 13:05:54 1999 +0200 +++ b/doc-src/Logics/Makefile Tue Aug 03 13:06:16 1999 +0200 @@ -12,7 +12,7 @@ include ../Makefile.in NAME = logics -FILES = logics.tex preface.tex syntax.tex LK.tex CTT.tex \ +FILES = logics.tex preface.tex syntax.tex LK.tex Sequents.tex CTT.tex \ ../proof.sty ../iman.sty ../extra.sty ../manual.bib dvi: $(NAME).dvi diff -r b009afd1ace5 -r 1135f3f8782c doc-src/Logics/Sequents.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Logics/Sequents.tex Tue Aug 03 13:06:16 1999 +0200 @@ -0,0 +1,201 @@ +%% $Id$ +\chapter{Defining A Sequent-Based Logic} +\label{chap:sequents} + +\underscoreon %this file contains the @ character + +The Isabelle theory \texttt{Sequents.thy} provides facilities for using +sequent notation in users' object logics. This theory allows users to +easily interface the surface syntax of sequences with an underlying +representation suitable for higher-order unification. + +\section{Concrete syntax of sequences} + +Mathematicians and logicians have used sequences in an informal way +much before proof systems such as Isabelle were created. It seems +sensible to allow people using Isabelle to express sequents and +perform proofs in this same informal way, and without requiring the +theory developer to spend a lot of time in \ML{} programming. + +By using {\tt Sequents.thy} +appropriately, a logic developer can allow users to refer to sequences +in several ways: +% +\begin{itemize} +\item A sequence variable is any alphanumeric string with the first + character being a \verb%$% sign. +So, consider the sequent \verb%$A |- B%, where \verb%$A% +is intended to match a sequence of zero or more items. + +\item A sequence with unspecified sub-sequences and unspecified or +individual items is written as a comma-separated list of regular +variables (representing items), particular items, and +sequence variables, as in +\begin{ttbox} +$A, B, C, $D(x) |- E +\end{ttbox} +Here both \verb%$A% and \verb%$D(x)% +are allowed to match any subsequences of items on either side of the +two items that match $B$ and $C$. Moreover, the sequence matching +\verb%$D(x)% may contain occurrences of~$x$. + +\item An empty sequence can be represented by a blank space, as in +\verb? |- true?. +\end{itemize} + +These syntactic constructs need to be assimilated into the object +theory being developed. The type that we use for these visible objects +is given the name {\tt seq}. +A {\tt seq} is created either by the empty space, a {\tt seqobj} or a +{\tt seqobj} followed by a {\tt seq}, with a comma between them. A +{\tt seqobj} is either an item or a variable representing a +sequence. Thus, a theory designer can specify a function that takes +two sequences and returns a meta-level proposition by giving it the +Isabelle type \verb|[seq, seq] => prop|. + +This is all part of the concrete syntax, but one may wish to +exploit Isabelle's higher-order abstract syntax by actually having a +different, more powerful {\em internal} syntax. + + + +\section{ Basis} + +One could opt to represent sequences as first-order objects (such as +simple lists), but this would not allow us to use many facilities +Isabelle provides for matching. By using a slightly more complex +representation, users of the logic can reap many benefits in +facilities for proofs and ease of reading logical terms. + +A sequence can be represented as a function --- a constructor for +further sequences --- by defining a binary {\em abstract} function +\verb|Seq0'| with type \verb|[o,seq']=>seq'|, and translating a +sequence such as \verb|A, B, C| into +\begin{ttbox} +\%s. Seq0'(A, SeqO'(B, SeqO'(C, s))) +\end{ttbox} +This sequence can therefore be seen as a constructor +for further sequences. The constructor \verb|Seq0'| is never given a +value, and therefore it is not possible to evaluate this expression +into a basic value. + +Furthermore, if we want to represent the sequence \verb|A, $B, C|, +we note that \verb|$B| already represents a sequence, so we can use +\verb|B| itself to refer to the function, and therefore the sequence +can be mapped to the internal form: +\verb|%s. SeqO'(A, B(SeqO'(C, s)))|. + +So, while we wish to continue with the standard, well-liked {\em +external} representation of sequences, we can represent them {\em +internally} as functions of type \verb|seq'=>seq'|. + + +\section{Object logics} + +Recall that object logics are defined by mapping elements of +particular types to the Isabelle type \verb|prop|, usually with a +function called {\tt Trueprop}. So, an object +logic proposition {\tt P} is matched to the Isabelle proposition +{\tt Trueprop(P)}\@. The name of the function is often hidden, so the +user just sees {\tt P}\@. Isabelle is eager to make types match, so it +inserts {\tt Trueprop} automatically when an object of type {\tt prop} +is expected. This mechanism can be observed in most of the object +logics which are direct descendants of {\tt Pure}. + +In order to provide the desired syntactic facilities for sequent +calculi, rather than use just one function that maps object-level +propositions to meta-level propositions, we use two functions, and +separate internal from the external representation. + +These functions need to be given a type that is appropriate for the particular +form of sequents required: single or multiple conclusions. So +multiple-conclusion sequents (used in the LK logic) can be +specified by the following two definitions, which are lifted from the inbuilt +{\tt Sequents/LK.thy}: +\begin{ttbox} + Trueprop :: two_seqi + "@Trueprop" :: two_seqe ("((_)/ |- (_))" [6,6] 5) +\end{ttbox} +% +where the types used are defined in {\tt Sequents.thy} as +abbreviations: +\begin{ttbox} + two_seqi = [seq'=>seq', seq'=>seq'] => prop + two_seqe = [seq, seq] => prop +\end{ttbox} + +The next step is to actually create links into the low-level parsing +and pretty-printing mechanisms, which map external and internal +representations. These functions go below the user level and capture +the underlying structure of Isabelle terms in \ML{}\@. Fortunately the +theory developer need not delve in this level; {\tt Sequents.thy} +provides the necessary facilities. All the theory developer needs to +add in the \ML{} section is a specification of the two translation +functions: +\begin{ttbox} +ML +val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")]; +val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")]; +\end{ttbox} + +In summary: in the logic theory being developed, the developer needs +to specify the types for the internal and external representation of +the sequences, and use the appropriate parsing and pretty-printing +functions. + +\section{What's in \texttt{Sequents.thy}} + +Theory \texttt{Sequents.thy} makes many declarations that you need to know +about: +\begin{enumerate} +\item The Isabelle types given below, which can be used for the +constants that map object-level sequents and meta-level propositions: +% +\begin{ttbox} + single_seqe = [seq,seqobj] => prop + single_seqi = [seq'=>seq',seq'=>seq'] => prop + two_seqi = [seq'=>seq', seq'=>seq'] => prop + two_seqe = [seq, seq] => prop + three_seqi = [seq'=>seq', seq'=>seq', seq'=>seq'] => prop + three_seqe = [seq, seq, seq] => prop + four_seqi = [seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop + four_seqe = [seq, seq, seq, seq] => prop +\end{ttbox} + +The \verb|single_| and \verb|two_| sets of mappings for internal and +external representations are the ones used for, say single and +multiple conclusion sequents. The other functions are provided to +allow rules that manipulate more than two functions, as can be seen in +the inbuilt object logics. + +\item An auxiliary syntactic constant has been +defined that directly maps a sequence to its internal representation: +\begin{ttbox} +"@Side" :: seq=>(seq'=>seq') ("<<(_)>>") +\end{ttbox} +Whenever a sequence (such as \verb|<< A, $B, $C>>|) is entered using this +syntax, it is translated into the appropriate internal representation. This +form can be used only where a sequence is expected. + +\item The \ML{} functions \texttt{single\_tr}, \texttt{two\_seq\_tr}, + \texttt{three\_seq\_tr}, \texttt{four\_seq\_tr} for parsing, that is, the + translation from external to internal form. Analogously there are + \texttt{single\_tr'}, \texttt{two\_seq\_tr'}, \texttt{three\_seq\_tr'}, + \texttt{four\_seq\_tr'} for pretty-printing, that is, the translation from + internal to external form. These functions can be used in the \ML{} section + of a theory file to specify the translations to be used. As an example of + use, note that in {\tt LK.thy} we declare two identifiers: +\begin{ttbox} +val parse_translation = + [("@Trueprop",Sequents.two_seq_tr "Trueprop")]; +val print_translation = + [("Trueprop",Sequents.two_seq_tr' "@Trueprop")]; +\end{ttbox} +The given parse translation will be applied whenever a \verb|@Trueprop| +constant is found, translating using \verb|two_seq_tr| and inserting the +constant \verb|Trueprop|. The pretty-printing translation is applied +analogously; a term that contains \verb|Trueprop| is printed as a +\verb|@Trueprop|. +\end{enumerate} + + diff -r b009afd1ace5 -r 1135f3f8782c doc-src/Logics/logics.tex --- a/doc-src/Logics/logics.tex Tue Aug 03 13:05:54 1999 +0200 +++ b/doc-src/Logics/logics.tex Tue Aug 03 13:06:16 1999 +0200 @@ -20,12 +20,13 @@ Computer Laboratory \\ University of Cambridge \\ \texttt{lcp@cl.cam.ac.uk}\\[3ex] With Contributions by Tobias Nipkow and Markus Wenzel% - \thanks{Markus Wenzel made numerous improvements. Philippe de Groote - wrote the first version of the logic~\LK{}. Tobias Nipkow developed - \LCF{} and~\Cube{}. Martin Coen developed~\Modal{} with assistance - from Rajeev Gor\'e. The research has been funded by the EPSRC - (grants GR/G53279, GR/H40570, GR/K57381, GR/K77051) and by ESPRIT - project 6453: Types.} } + \thanks{Markus Wenzel made numerous improvements. Sara Kalvala + contributed Chap.\ts\ref{chap:sequents}. Philippe de Groote + wrote the first version of the logic~\LK{}. Tobias Nipkow developed + \LCF{} and~\Cube{}. Martin Coen developed~\Modal{} with assistance + from Rajeev Gor\'e. The research has been funded by the EPSRC + (grants GR/G53279, GR/H40570, GR/K57381, GR/K77051) and by ESPRIT + project 6453: Types.} } \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip \hrule\bigskip} @@ -47,10 +48,9 @@ \include{preface} \include{syntax} \include{LK} +\include{Sequents} %%\include{Modal} \include{CTT} -%%\include{Cube} -%%\include{LCF} \bibliographystyle{plain} \bibliography{../manual} \input{logics.ind}