|
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 |