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