|
1 \chapter{Defining Logics} \label{Defining-Logics} |
|
2 This chapter is intended for Isabelle experts. It explains how to define new |
|
3 logical systems, Isabelle's {\it raison d'\^etre}. Isabelle logics are |
|
4 hierarchies of theories. A number of simple examples are contained in the |
|
5 introductory manual; the full syntax of theory definitions is shown in the |
|
6 {\em Reference Manual}. The purpose of this chapter is to explain the |
|
7 remaining subtleties, especially some context conditions on the class |
|
8 structure and the definition of new mixfix syntax. A full understanding of |
|
9 the material requires knowledge of the internal representation of terms (data |
|
10 type {\tt term}) as detailed in the {\em Reference Manual}. Sections marked |
|
11 with a * can be skipped on first reading. |
|
12 |
|
13 |
|
14 \section{Classes and Types *} |
|
15 \index{*arities!context conditions} |
|
16 |
|
17 Type declarations are subject to the following two well-formedness |
|
18 conditions: |
|
19 \begin{itemize} |
|
20 \item There are no two declarations $ty :: (\vec{r})c$ and $ty :: (\vec{s})c$ |
|
21 with $\vec{r} \neq \vec{s}$. For example |
|
22 \begin{ttbox} |
|
23 types ty 1 |
|
24 arities ty :: (\{logic\}) logic |
|
25 ty :: (\{\})logic |
|
26 \end{ttbox} |
|
27 leads to an error message and fails. |
|
28 \item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty :: |
|
29 (s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold |
|
30 for $i=1,\dots,n$. The relationship $\preceq$, defined as |
|
31 \[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \] |
|
32 expresses that the set of types represented by $s'$ is a subset of the set of |
|
33 types represented by $s$. For example |
|
34 \begin{ttbox} |
|
35 classes term < logic |
|
36 types ty 1 |
|
37 arities ty :: (\{logic\})logic |
|
38 ty :: (\{\})term |
|
39 \end{ttbox} |
|
40 leads to an error message and fails. |
|
41 \end{itemize} |
|
42 These conditions guarantee principal types~\cite{nipkow-prehofer}. |
|
43 |
|
44 \section{Precedence Grammars} |
|
45 \label{PrecedenceGrammars} |
|
46 \index{precedence grammar|(} |
|
47 |
|
48 The precise syntax of a logic is best defined by a context-free grammar. |
|
49 These grammars obey the following conventions: identifiers denote |
|
50 nonterminals, {\tt typewriter} fount denotes terminals, repetition is |
|
51 indicated by \dots, and alternatives are separated by $|$. |
|
52 |
|
53 In order to simplify the description of mathematical languages, we introduce |
|
54 an extended format which permits {\bf precedences}\index{precedence}. This |
|
55 scheme generalizes precedence declarations in \ML\ and {\sc prolog}. In this |
|
56 extended grammar format, nonterminals are decorated by integers, their |
|
57 precedence. In the sequel, precedences are shown as subscripts. A nonterminal |
|
58 $A@p$ on the right-hand side of a production may only be replaced using a |
|
59 production $A@q = \gamma$ where $p \le q$. |
|
60 |
|
61 Formally, a set of context free productions $G$ induces a derivation |
|
62 relation $\rew@G$ on strings as follows: |
|
63 \[ \alpha A@p \beta ~\rew@G~ \alpha\gamma\beta ~~~iff~~~ |
|
64 \exists q \ge p.~(A@q=\gamma) \in G |
|
65 \] |
|
66 Any extended grammar of this kind can be translated into a normal context |
|
67 free grammar. However, this translation may require the introduction of a |
|
68 large number of new nonterminals and productions. |
|
69 |
|
70 \begin{example} |
|
71 \label{PrecedenceEx} |
|
72 The following simple grammar for arithmetic expressions demonstrates how |
|
73 binding power and associativity of operators can be enforced by precedences. |
|
74 \begin{center} |
|
75 \begin{tabular}{rclr} |
|
76 $A@9$ & = & {\tt0} \\ |
|
77 $A@9$ & = & {\tt(} $A@0$ {\tt)} \\ |
|
78 $A@0$ & = & $A@0$ {\tt+} $A@1$ \\ |
|
79 $A@2$ & = & $A@3$ {\tt*} $A@2$ \\ |
|
80 $A@3$ & = & {\tt-} $A@3$ |
|
81 \end{tabular} |
|
82 \end{center} |
|
83 The choice of precedences determines that \verb$-$ binds tighter than |
|
84 \verb$*$ which binds tighter than \verb$+$, and that \verb$+$ and \verb$*$ |
|
85 associate to the left and right, respectively. |
|
86 \end{example} |
|
87 |
|
88 To minimize the number of subscripts, we adopt the following conventions: |
|
89 \begin{itemize} |
|
90 \item all precedences $p$ must be in the range $0 \leq p \leq max_pri$ for |
|
91 some fixed $max_pri$. |
|
92 \item precedence $0$ on the right-hand side and precedence $max_pri$ on the |
|
93 left-hand side may be omitted. |
|
94 \end{itemize} |
|
95 In addition, we write the production $A@p = \alpha$ as $A = \alpha~(p)$. |
|
96 |
|
97 Using these conventions and assuming $max_pri=9$, the grammar in |
|
98 Example~\ref{PrecedenceEx} becomes |
|
99 \begin{center} |
|
100 \begin{tabular}{rclc} |
|
101 $A$ & = & {\tt0} & \hspace*{4em} \\ |
|
102 & $|$ & {\tt(} $A$ {\tt)} \\ |
|
103 & $|$ & $A$ {\tt+} $A@1$ & (0) \\ |
|
104 & $|$ & $A@3$ {\tt*} $A@2$ & (2) \\ |
|
105 & $|$ & {\tt-} $A@3$ & (3) |
|
106 \end{tabular} |
|
107 \end{center} |
|
108 |
|
109 \index{precedence grammar|)} |
|
110 |
|
111 \section{Basic syntax *} |
|
112 |
|
113 An informal account of most of Isabelle's syntax (meta-logic, types etc) is |
|
114 contained in {\em Introduction to Isabelle}. A precise description using a |
|
115 precedence grammar is shown in Figure~\ref{MetaLogicSyntax}. This description |
|
116 is the basis of all extensions by object-logics. |
|
117 \begin{figure}[htb] |
|
118 \begin{center} |
|
119 \begin{tabular}{rclc} |
|
120 $prop$ &=& \ttindex{PROP} $aprop$ ~~$|$~~ {\tt(} $prop$ {\tt)} \\ |
|
121 &$|$& $logic@3$ \ttindex{==} $logic@2$ & (2) \\ |
|
122 &$|$& $prop@2$ \ttindex{==>} $prop@1$ & (1) \\ |
|
123 &$|$& {\tt[|} $prop$ {\tt;} \dots {\tt;} $prop$ {\tt|]} {\tt==>} $prop@1$ & (1) \\ |
|
124 &$|$& {\tt!!} $idts$ {\tt.} $prop$ & (0) \\\\ |
|
125 $logic$ &=& $prop$ ~~$|$~~ $fun$ \\\\ |
|
126 $aprop$ &=& $id$ ~~$|$~~ $var$ |
|
127 ~~$|$~~ $fun@{max_pri}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)} \\\\ |
|
128 $fun$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $fun$ {\tt)} \\ |
|
129 &$|$& \ttindex{\%} $idts$ {\tt.} $logic$ & (0) \\\\ |
|
130 $idts$ &=& $idt$ ~~$|$~~ $idt@1$ $idts$ \\\\ |
|
131 $idt$ &=& $id$ ~~$|$~~ {\tt(} $idt$ {\tt)} \\ |
|
132 &$|$& $id$ \ttindex{::} $type$ & (0) \\\\ |
|
133 $type$ &=& $tfree$ ~~$|$~~ $tvar$ \\ |
|
134 &$|$& $tfree$ {\tt::} $sort$ ~~$|$~~ $tvar$ {\tt::} $sort$ \\ |
|
135 &$|$& $id$ ~~$|$~~ $type@{max_pri}$ $id$ |
|
136 ~~$|$~~ {\tt(} $type$ {\tt,} \dots {\tt,} $type$ {\tt)} $id$ \\ |
|
137 &$|$& $type@1$ \ttindex{=>} $type$ & (0) \\ |
|
138 &$|$& {\tt[} $type$ {\tt,} \dots {\tt,} $type$ {\tt]} {\tt=>} $type$&(0)\\ |
|
139 &$|$& {\tt(} $type$ {\tt)} \\\\ |
|
140 $sort$ &=& $id$ ~~$|$~~ {\tt\{\}} |
|
141 ~~$|$~~ {\tt\{} $id$ {\tt,} \dots {\tt,} $id$ {\tt\}} |
|
142 \end{tabular}\index{*"!"!}\index{*"["|}\index{*"|"]} |
|
143 \indexbold{type@$type$}\indexbold{sort@$sort$}\indexbold{idts@$idts$} |
|
144 \indexbold{logic@$logic$}\indexbold{prop@$prop$}\indexbold{fun@$fun$} |
|
145 \end{center} |
|
146 \caption{Meta-Logic Syntax} |
|
147 \label{MetaLogicSyntax} |
|
148 \end{figure} |
|
149 The following main categories are defined: |
|
150 \begin{description} |
|
151 \item[$prop$] Terms of type $prop$, i.e.\ formulae of the meta-logic. |
|
152 \item[$aprop$] Atomic propositions. |
|
153 \item[$logic$] Terms of types in class $logic$. Initially, $logic$ contains |
|
154 merely $prop$. As the syntax is extended by new object-logics, more |
|
155 productions for $logic$ are added (see below). |
|
156 \item[$fun$] Terms potentially of function type. |
|
157 \item[$type$] Types. |
|
158 \item[$idts$] a list of identifiers, possibly constrained by types. Note |
|
159 that $x::nat~y$ is parsed as $x::(nat~y)$, i.e.\ $y$ is treated like a |
|
160 type constructor applied to $nat$. |
|
161 \end{description} |
|
162 |
|
163 The predefined types $id$, $var$, $tfree$ and $tvar$ represent identifiers |
|
164 ({\tt f}), unknowns ({\tt ?f}), type variables ({\tt 'a}), and type unknowns |
|
165 ({\tt ?'a}) respectively. If we think of them as nonterminals with |
|
166 predefined syntax, we may assume that all their productions have precedence |
|
167 $max_pri$. |
|
168 |
|
169 \subsection{Logical types and default syntax} |
|
170 |
|
171 Isabelle is concerned with mathematical languages which have a certain |
|
172 minimal vocabulary: identifiers, variables, parentheses, and the lambda |
|
173 calculus. Logical types, i.e.\ those of class $logic$, are automatically |
|
174 equipped with this basic syntax. More precisely, for any type constructor |
|
175 $ty$ with arity $(\dots)c$, where $c$ is a subclass of $logic$, the following |
|
176 productions are added: |
|
177 \begin{center} |
|
178 \begin{tabular}{rclc} |
|
179 $ty$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $ty$ {\tt)} \\ |
|
180 &$|$& $fun@{max_pri}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)}\\ |
|
181 &$|$& $ty@{max_pri}$ {\tt::} $type$\\\\ |
|
182 $logic$ &=& $ty$ |
|
183 \end{tabular} |
|
184 \end{center} |
|
185 |
|
186 |
|
187 \section{Mixfix syntax} |
|
188 \index{mixfix|(} |
|
189 |
|
190 We distinguish between abstract and concrete syntax. The {\em abstract} |
|
191 syntax is given by the typed constants of a theory. Abstract syntax trees are |
|
192 well-typed terms, i.e.\ values of \ML\ type {\tt term}. If none of the |
|
193 constants are introduced with mixfix annotations, there is no concrete syntax |
|
194 to speak of: terms can only be abstractions or applications of the form |
|
195 $f(t@1,\dots,t@n)$, where $f$ is a constant or variable. Since this notation |
|
196 quickly becomes unreadable, Isabelle supports syntax definitions in the form |
|
197 of unrestricted context-free grammars using mixfix annotations. |
|
198 |
|
199 Mixfix annotations describe the {\em concrete} syntax, its translation into |
|
200 the abstract syntax, and a pretty-printing scheme, all in one. Isabelle |
|
201 syntax definitions are inspired by \OBJ's~\cite{OBJ} {\em mixfix\/} syntax. |
|
202 Each mixfix annotation defines a precedence grammar production and associates |
|
203 an Isabelle constant with it. |
|
204 |
|
205 A {\em mixfix declaration} {\tt consts $c$ ::\ $\tau$ ($sy$ $ps$ $p$)} is |
|
206 interpreted as a grammar pro\-duction as follows: |
|
207 \begin{itemize} |
|
208 \item $sy$ is the right-hand side of this production, specified as a {\em |
|
209 mixfix annotation}. In general, $sy$ is of the form |
|
210 $\alpha@0\_\alpha@1\dots\alpha@{n-1}\_\alpha@n$, where each occurrence of |
|
211 ``\ttindex{_}'' denotes an argument/nonterminal and the strings |
|
212 $\alpha@i$ do not contain ``{\tt_}''. |
|
213 \item $\tau$ specifies the types of the nonterminals on the left and right |
|
214 hand side. If $sy$ is of the form above, $\tau$ must be of the form |
|
215 $[\tau@1,\dots,\tau@n] \To \tau'$. Then argument $i$ is of type $\tau@i$ |
|
216 and the result, i.e.\ the left-hand side of the production, is of type |
|
217 $\tau'$. Both the $\tau@i$ and $\tau'$ may be function types. |
|
218 \item $c$ is the name of the Isabelle constant associated with this production. |
|
219 Parsing an instance of the phrase $sy$ generates the {\tt term} {\tt |
|
220 Const($c$,dummyT\footnote{Proper types are inserted later on. See |
|
221 \S\ref{Typing}})\$$a@1$\$$\dots$\$$a@n$}\index{*dummyT}, where $a@i$ is |
|
222 the term generated by parsing the $i^{th}$ argument. |
|
223 \item $ps$ must be of the form $[p@1,\dots,p@n]$, where $p@i$ is the |
|
224 minimal precedence\index{precedence} required of any phrase that may appear |
|
225 as the $i^{th}$ argument. The null list is interpreted as a list of 0's of |
|
226 the appropriate length. |
|
227 \item $p$ is the precedence of this production. |
|
228 \end{itemize} |
|
229 Notice that there is a close connection between abstract and concrete syntax: |
|
230 each production has an associated constant, and types act as {\bf syntactic |
|
231 categories} in the concrete syntax. To emphasize this connection, we |
|
232 sometimes refer to the nonterminals on the right-hand side of a production as |
|
233 its arguments and to the nonterminal on the left-hand side as its result. |
|
234 |
|
235 The maximal legal precedence is called \ttindexbold{max_pri}, which is |
|
236 currently 1000. If you want to ignore precedences, the safest way to do so is |
|
237 to use the annotation {\tt($sy$)}: this production puts no precedence |
|
238 constraints on any of its arguments and has maximal precedence itself, i.e.\ |
|
239 it is always applicable and does not exclude any productions of its |
|
240 arguments. |
|
241 |
|
242 \begin{example} |
|
243 In mixfix notation the grammar in Example~\ref{PrecedenceEx} can be written |
|
244 as follows: |
|
245 \begin{ttbox} |
|
246 types exp 0 |
|
247 consts "0" :: "exp" ("0" 9) |
|
248 "+" :: "[exp,exp] => exp" ("_ + _" [0,1] 0) |
|
249 "*" :: "[exp,exp] => exp" ("_ * _" [3,2] 2) |
|
250 "-" :: "exp => exp" ("- _" [3] 3) |
|
251 \end{ttbox} |
|
252 Parsing the string \verb!"0 + - 0 + 0"! produces the term {\tt |
|
253 $p$\$($p$\$($m$\$$z$)\$$z$)\$$z$} where {\tt$p =$ Const("+",dummyT)}, |
|
254 {\tt$m =$ Const("-",dummyT)}, and {\tt$z =$ Const("0",dummyT)}. |
|
255 \end{example} |
|
256 |
|
257 The interpretation of \ttindex{_} in a mixfix annotation is always as a {\bf |
|
258 meta-character}\index{meta-character} which does not represent itself but |
|
259 an argument position. The following characters are also meta-characters: |
|
260 \begin{ttbox} |
|
261 ' ( ) / |
|
262 \end{ttbox} |
|
263 Preceding any character with a quote (\verb$'$) turns it into an ordinary |
|
264 character. Thus you can write \verb!''! if you really want a single quote. |
|
265 The purpose of the other meta-characters is explained in |
|
266 \S\ref{PrettyPrinting}. Remember that in \ML\ strings \verb$\$ is already a |
|
267 (different kind of) meta-character. |
|
268 |
|
269 |
|
270 \subsection{Types and syntactic categories *} |
|
271 |
|
272 The precise mapping from types to syntactic categories is defined by the |
|
273 following function: |
|
274 \begin{eqnarray*} |
|
275 N(\tau@1\To\tau@2) &=& fun \\ |
|
276 N((\tau@1,\dots,\tau@n)ty) &=& ty \\ |
|
277 N(\alpha) &=& logic |
|
278 \end{eqnarray*} |
|
279 Only the outermost type constructor is taken into account and type variables |
|
280 can range over all logical types. This catches some ill-typed terms (like |
|
281 $Cons(x,0)$, where $Cons :: [\alpha,\alpha list] \To \alpha list$ and $0 :: |
|
282 nat$) but leaves the real work to the type checker. |
|
283 |
|
284 In terms of the precedence grammar format introduced in |
|
285 \S\ref{PrecedenceGrammars}, the declaration |
|
286 \begin{ttbox} |
|
287 consts \(c\) :: "[\(\tau@1\),\dots,\(\tau@n\)]\(\To\tau\)" ("\(\alpha@0\_\alpha@1\dots\alpha@{n-1}\_\alpha@n\)") [\(p@1\),\dots,\(p@n\)] \(p\)) |
|
288 \end{ttbox} |
|
289 defines the production |
|
290 \[ N(\tau)@p ~~=~~ \alpha@0 ~N(\tau@1)@{p@1}~ \alpha@1~ \dots |
|
291 ~\alpha@{n-1} ~N(\tau@n)@{p@n}~ \alpha@n |
|
292 \] |
|
293 |
|
294 \subsection{Copy productions *} |
|
295 |
|
296 Productions which do not create a new node in the abstract syntax tree are |
|
297 called {\bf copy productions}. They must have exactly one nonterminal on |
|
298 the right hand side. The term generated when parsing that nonterminal is |
|
299 simply passed up as the result of parsing the whole copy production. In |
|
300 Isabelle a copy production is indicated by an empty constant name, i.e.\ by |
|
301 \begin{ttbox} |
|
302 consts "" :: \(\tau\) (\(sy\) \(ps\) \(p\)) |
|
303 \end{ttbox} |
|
304 |
|
305 A special kind of copy production is one where, modulo white space, $sy$ is |
|
306 {\tt"_"}. It is called a {\bf chain production}. Chain productions should be |
|
307 seen as an abbreviation mechanism. Conceptually, they are removed from the |
|
308 grammar by adding appropriate new rules. Precedence information attached to |
|
309 chain productions is ignored. The following example demonstrates the effect: |
|
310 the grammar defined by |
|
311 \begin{ttbox} |
|
312 types A,B,C 0 |
|
313 consts AB :: "B => A" ("A _" [10] 517) |
|
314 "" :: "C => B" ("_" [0] 100) |
|
315 x :: "C" ("x" 5) |
|
316 y :: "C" ("y" 15) |
|
317 \end{ttbox} |
|
318 admits {\tt"A y"} but not {\tt"A x"}. Had the constant in the second |
|
319 production been some non-empty string, both {\tt"A y"} and {\tt"A x"} would |
|
320 be legal. |
|
321 |
|
322 \index{mixfix|)} |
|
323 |
|
324 \section{Lexical conventions} |
|
325 |
|
326 The lexical analyzer distinguishes the following kinds of tokens: delimiters, |
|
327 identifiers, unknowns, type variables and type unknowns. |
|
328 |
|
329 Delimiters are user-defined, i.e.\ they are extracted from the syntax |
|
330 definition. If $\alpha@0\_\alpha@1\dots\alpha@{n-1}\_\alpha@n$ is a mixfix |
|
331 annotation, each $\alpha@i$ is decomposed into substrings |
|
332 $\beta@1~\dots~\beta@k$ which are separated by and do not contain |
|
333 \bfindex{white space} ( = blanks, tabs, newlines). Each $\beta@j$ becomes a |
|
334 delimiter. Thus a delimiter can be an arbitrary string not containing white |
|
335 space. |
|
336 |
|
337 The lexical syntax of identifiers and variables ( = unknowns) is defined in |
|
338 the introductory manual. Parsing an identifier $f$ generates {\tt |
|
339 Free($f$,dummyT)}\index{*dummyT}. Parsing a variable {\tt?}$v$ generates |
|
340 {\tt Var(($u$,$i$),dummyT)} where $i$ is the integer value of the longest |
|
341 numeric suffix of $v$ (possibly $0$), and $u$ is the remaining prefix. |
|
342 Parsing a variable {\tt?}$v{.}i$ generates {\tt Var(($v$,$i$),dummyT)}. The |
|
343 following table covers the four different cases that can arise: |
|
344 \begin{center}\tt |
|
345 \begin{tabular}{cccc} |
|
346 "?v" & "?v.7" & "?v5" & "?v7.5" \\ |
|
347 Var(("v",0),$d$) & Var(("v",7),$d$) & Var(("v",5),$d$) & Var(("v7",5),$d$) |
|
348 \end{tabular} |
|
349 \end{center} |
|
350 where $d = {\tt dummyT}$. |
|
351 |
|
352 In mixfix annotations, \ttindexbold{id}, \ttindexbold{var}, |
|
353 \ttindexbold{tfree} and \ttindexbold{tvar} are the predefined categories of |
|
354 identifiers, unknowns, type variables and type unknowns, respectively. |
|
355 |
|
356 |
|
357 The lexical analyzer translates input strings to token lists by repeatedly |
|
358 taking the maximal prefix of the input string that forms a valid token. A |
|
359 maximal prefix that is both a delimiter and an identifier or variable (like |
|
360 {\tt ALL}) is treated as a delimiter. White spaces are separators. |
|
361 |
|
362 An important consequence of this translation scheme is that delimiters need |
|
363 not be separated by white space to be recognized as separate. If \verb$"-"$ |
|
364 is a delimiter but \verb$"--"$ is not, the string \verb$"--"$ is treated as |
|
365 two consecutive occurrences of \verb$"-"$. This is in contrast to \ML\ which |
|
366 would treat \verb$"--"$ as a single (undeclared) identifier. The |
|
367 consequence of Isabelle's more liberal scheme is that the same string may be |
|
368 parsed in a different way after extending the syntax: after adding |
|
369 \verb$"--"$ as a delimiter, the input \verb$"--"$ is treated as |
|
370 a single occurrence of \verb$"--"$. |
|
371 |
|
372 \section{Infix operators} |
|
373 |
|
374 {\tt Infixl} and {\tt infixr} declare infix operators which associate to the |
|
375 left and right respectively. As in \ML, prefixing infix operators with |
|
376 \ttindexbold{op} turns them into curried functions. Infix declarations can |
|
377 be reduced to mixfix ones as follows: |
|
378 \begin{center}\tt |
|
379 \begin{tabular}{l@{~~$\Longrightarrow$~~}l} |
|
380 "$c$" ::~$\tau$ (\ttindexbold{infixl} $p$) & |
|
381 "op $c$" ::~$\tau$ ("_ $c$ _" [$p$,$p+1$] $p$) \\ |
|
382 "$c$" ::~$\tau$ (\ttindexbold{infixr} $p$) & |
|
383 "op $c$" ::~$\tau$ ("_ $c$ _" [$p+1$,$p$] $p$) |
|
384 \end{tabular} |
|
385 \end{center} |
|
386 |
|
387 |
|
388 \section{Binders} |
|
389 A {\bf binder} is a variable-binding constant, such as a quantifier. |
|
390 The declaration |
|
391 \begin{ttbox} |
|
392 consts \(c\) :: \(\tau\) (binder \(Q\) \(p\)) |
|
393 \end{ttbox}\indexbold{*binder} |
|
394 introduces a binder $c$ of type $\tau$, |
|
395 which must have the form $(\tau@1\To\tau@2)\To\tau@3$. Its concrete syntax |
|
396 is $Q~x.t$. A binder is like a generalized quantifier where $\tau@1$ is the |
|
397 type of the bound variable $x$, $\tau@2$ the type of the body $t$, and |
|
398 $\tau@3$ the type of the whole term. For example $\forall$ can be declared |
|
399 like this: |
|
400 \begin{ttbox} |
|
401 consts All :: "('a => o) => o" (binder "ALL " 10) |
|
402 \end{ttbox} |
|
403 This allows us to write $\forall x.P$ either as {\tt ALL $x$.$P$} or {\tt |
|
404 All(\%$x$.$P$)}; the latter form is for purists only. |
|
405 |
|
406 In case $\tau@2 = \tau@3$, nested quantifications can be written as $Q~x@1 |
|
407 \dots x@n.t$. From a syntactic point of view, |
|
408 \begin{ttbox} |
|
409 consts \(c\) :: "\((\tau@1\To\tau@2)\To\tau@3\)" (binder "\(Q\)" \(p\)) |
|
410 \end{ttbox} |
|
411 is equivalent to |
|
412 \begin{ttbox} |
|
413 consts \(c\) :: "\((\tau@1\To\tau@2)\To\tau@3\)" |
|
414 "\(Q\)" :: "[idts,\(\tau@2\)] => \(\tau@3\)" ("\(Q\)_. _" \(p\)) |
|
415 \end{ttbox} |
|
416 where {\tt idts} is the syntactic category $idts$ defined in |
|
417 Figure~\ref{MetaLogicSyntax}. |
|
418 |
|
419 However, there is more to binders than concrete syntax: behind the scenes the |
|
420 body of the quantified expression has to be converted into a |
|
421 $\lambda$-abstraction (when parsing) and back again (when printing). This |
|
422 is performed by the translation mechanism, which is discussed below. For |
|
423 binders, the definition of the required translation functions has been |
|
424 automated. Many other syntactic forms, such as set comprehension, require |
|
425 special treatment. |
|
426 |
|
427 |
|
428 \section{Parse translations *} |
|
429 \label{Parse-translations} |
|
430 \index{parse translation|(} |
|
431 |
|
432 So far we have pretended that there is a close enough relationship between |
|
433 concrete and abstract syntax to allow an automatic translation from one to |
|
434 the other using the constant name supplied with each production. In many |
|
435 cases this scheme is not powerful enough, especially for constructs involving |
|
436 variable bindings. Therefore the $ML$-section of a theory definition can |
|
437 associate constant names with user-defined translation functions by including |
|
438 a line |
|
439 \begin{ttbox} |
|
440 val parse_translation = \dots |
|
441 \end{ttbox} |
|
442 where the right-hand side of this binding must be an \ML-expression of type |
|
443 \verb$(string * (term list -> term))list$. |
|
444 |
|
445 After the input string has been translated into a term according to the |
|
446 syntax definition, there is a second phase in which the term is translated |
|
447 using the user-supplied functions in a bottom-up manner. Given a list $tab$ |
|
448 of the above type, a term $t$ is translated as follows. If $t$ is not of the |
|
449 form {\tt Const($c$,$\tau$)\$$t@1$\$\dots\$$t@n$}, then $t$ is returned |
|
450 unchanged. Otherwise all $t@i$ are translated into $t@i'$. Let {\tt $t' =$ |
|
451 Const($c$,$\tau$)\$$t@1'$\$\dots\$$t@n'$}. If there is no pair $(c,f)$ in |
|
452 $tab$, return $t'$. Otherwise apply $f$ to $[t@1',\dots,t@n']$. If that |
|
453 raises an exception, return $t'$, otherwise return the result. |
|
454 \begin{example}\label{list-enum} |
|
455 \ML-lists are constructed by {\tt[]} and {\tt::}. For readability the |
|
456 list \hbox{\tt$x$::$y$::$z$::[]} can be written \hbox{\tt[$x$,$y$,$z$]}. |
|
457 In Isabelle the two forms of lists are declared as follows: |
|
458 \begin{ttbox} |
|
459 types list 1 |
|
460 enum 0 |
|
461 arities list :: (term)term |
|
462 consts "[]" :: "'a list" ("[]") |
|
463 ":" :: "['a, 'a list] => 'a list" (infixr 50) |
|
464 enum :: "enum => 'a list" ("[_]") |
|
465 sing :: "'a => enum" ("_") |
|
466 cons :: "['a,enum] => enum" ("_, _") |
|
467 end |
|
468 \end{ttbox} |
|
469 Because \verb$::$ is already used for type constraints, it is replaced by |
|
470 \verb$:$ as the infix list constructor. |
|
471 |
|
472 In order to allow list enumeration, the new type {\tt enum} is introduced. |
|
473 Its only purpose is syntactic and hence it does not need an arity, in |
|
474 contrast to the logical type {\tt list}. Although \hbox{\tt[$x$,$y$,$z$]} is |
|
475 syntactically legal, it needs to be translated into a term built up from |
|
476 \verb$[]$ and \verb$:$. This is what \verb$make_list$ accomplishes: |
|
477 \begin{ttbox} |
|
478 val cons = Const("op :", dummyT); |
|
479 |
|
480 fun make_list (Const("sing",_)$e) = cons $ e $ Const("[]", dummyT) |
|
481 | make_list (Const("cons",_)$e$es) = cons $ e $ make_list es; |
|
482 \end{ttbox} |
|
483 To hook this translation up to Isabelle's parser, the theory definition needs |
|
484 to contain the following $ML$-section: |
|
485 \begin{ttbox} |
|
486 ML |
|
487 fun enum_tr[enum] = make_list enum; |
|
488 val parse_translation = [("enum",enum_tr)] |
|
489 \end{ttbox} |
|
490 This causes \verb!Const("enum",_)$!$t$ to be replaced by |
|
491 \verb$enum_tr[$$t$\verb$]$. |
|
492 |
|
493 Of course the definition of \verb$make_list$ should be included in the |
|
494 $ML$-section. |
|
495 \end{example} |
|
496 \begin{example}\label{SET} |
|
497 Isabelle represents the set $\{ x \mid P(x) \}$ internally by $Set(\lambda |
|
498 x.P(x))$. The internal and external forms need separate |
|
499 constants:\footnote{In practice, the external form typically has a name |
|
500 beginning with an {\at} sign, such as {\tt {\at}SET}. This emphasizes that |
|
501 the constant should be used only for parsing/printing.} |
|
502 \begin{ttbox} |
|
503 types set 1 |
|
504 arities set :: (term)term |
|
505 consts Set :: "('a => o) => 'a set" |
|
506 SET :: "[id,o] => 'a set" ("\{_ | _\}") |
|
507 \end{ttbox} |
|
508 Parsing {\tt"\{$x$ | $P$\}"} according to this syntax yields the term {\tt |
|
509 Const("SET",dummyT) \$ Free("\(x\)",dummyT) \$ \(p\)}, where $p$ is the |
|
510 result of parsing $P$. What we need is the term {\tt |
|
511 Const("Set",dummyT)\$Abs("$x$",dummyT,$p'$)}, where $p'$ is some |
|
512 ``abstracted'' version of $p$. Therefore we define a function |
|
513 \begin{ttbox} |
|
514 fun set_tr[Free(s,T), p] = Const("Set", dummyT) $ |
|
515 Abs(s, T, abstract_over(Free(s,T), p)); |
|
516 \end{ttbox} |
|
517 where \verb$abstract_over: term*term -> term$ is a predefined function such |
|
518 that {\tt abstract_over($u$,$t$)} replaces every occurrence of $u$ in $t$ by |
|
519 a {\tt Bound} variable of the correct index (i.e.\ 0 at top level). Remember |
|
520 that {\tt dummyT} is replaced by the correct types at a later stage (see |
|
521 \S\ref{Typing}). Function {\tt set_tr} is associated with {\tt SET} by |
|
522 including the \ML-text |
|
523 \begin{ttbox} |
|
524 val parse_translation = [("SET", set_tr)]; |
|
525 \end{ttbox} |
|
526 \end{example} |
|
527 |
|
528 If you want to run the above examples in Isabelle, you should note that an |
|
529 $ML$-section needs to contain not just a definition of |
|
530 \verb$parse_translation$ but also of a variable \verb$print_translation$. The |
|
531 purpose of the latter is to reverse the effect of the former during printing; |
|
532 details are found in \S\ref{Print-translations}. Hence you need to include |
|
533 the line |
|
534 \begin{ttbox} |
|
535 val print_translation = []; |
|
536 \end{ttbox} |
|
537 This is instructive because the terms are then printed out in their internal |
|
538 form. For example the input \hbox{\tt[$x$,$y$,$z$]} is echoed as |
|
539 \hbox{\tt$x$:$y$:$z$:[]}. This helps to check that your parse translation is |
|
540 working correctly. |
|
541 |
|
542 %\begin{warn} |
|
543 %Explicit type constraints disappear with type checking but are still |
|
544 %visible to the parse translation functions. |
|
545 %\end{warn} |
|
546 |
|
547 \index{parse translation|)} |
|
548 |
|
549 \section{Printing} |
|
550 |
|
551 Syntax definitions provide printing information in three distinct ways: |
|
552 through |
|
553 \begin{itemize} |
|
554 \item the syntax of the language (as used for parsing), |
|
555 \item pretty printing information, and |
|
556 \item print translation functions. |
|
557 \end{itemize} |
|
558 The bare mixfix declarations enable Isabelle to print terms, but the result |
|
559 will not necessarily be pretty and may look different from what you expected. |
|
560 To produce a pleasing layout, you need to read the following sections. |
|
561 |
|
562 \subsection{Printing with mixfix declarations} |
|
563 |
|
564 Let {\tt$t =$ Const($c$,_)\$$t@1$\$\dots\$$t@n$} be a term and let |
|
565 \begin{ttbox} |
|
566 consts \(c\) :: \(\tau\) (\(sy\)) |
|
567 \end{ttbox} |
|
568 be a mixfix declaration where $sy$ is of the form |
|
569 $\alpha@0\_\alpha@1\dots\alpha@{n-1}\_\alpha@n$. Printing $t$ according to |
|
570 $sy$ means printing the string |
|
571 $\alpha@0\beta@1\alpha@1\ldots\alpha@{n-1}\beta@n\alpha@n$, where $\beta@i$ |
|
572 is the result of printing $t@i$. |
|
573 |
|
574 Note that the system does {\em not\/} insert blanks. They should be part of |
|
575 the mixfix syntax if they are required to separate tokens or achieve a |
|
576 certain layout. |
|
577 |
|
578 \subsection{Pretty printing} |
|
579 \label{PrettyPrinting} |
|
580 \index{pretty printing} |
|
581 |
|
582 In order to format the output, it is possible to embed pretty printing |
|
583 directives in mixfix annotations. These directives are ignored during parsing |
|
584 and affect only printing. The characters {\tt(}, {\tt)} and {\tt/} are |
|
585 interpreted as meta-characters\index{meta-character} when found in a mixfix |
|
586 annotation. Their meaning is |
|
587 \begin{description} |
|
588 \item[~{\tt(}~] Open a block. A sequence of digits following it is |
|
589 interpreted as the \bfindex{indentation} of this block. It causes the |
|
590 output to be indented by $n$ positions if a line break occurs within the |
|
591 block. If {\tt(} is not followed by a digit, the indentation defaults to |
|
592 $0$. |
|
593 \item[~{\tt)}~] Close a block. |
|
594 \item[~\ttindex{/}~] Allow a \bfindex{line break}. White space immediately |
|
595 following {\tt/} is not printed if the line is broken at this point. |
|
596 \end{description} |
|
597 |
|
598 \subsection{Print translations *} |
|
599 \label{Print-translations} |
|
600 \index{print translation|(} |
|
601 |
|
602 Since terms are translated after parsing (see \S\ref{Parse-translations}), |
|
603 there is a similar mechanism to translate them back before printing. |
|
604 Therefore the $ML$-section of a theory definition can associate constant |
|
605 names with user-defined translation functions by including a line |
|
606 \begin{ttbox} |
|
607 val print_translation = \dots |
|
608 \end{ttbox} |
|
609 where the right-hand side of this binding is again an \ML-expression of type |
|
610 \verb$(string * (term list -> term))list$. |
|
611 Including a pair $(c,f)$ in this list causes the printer to print |
|
612 $f[t@1,\dots,t@n]$ whenever it finds {\tt Const($c$,_)\$$t@1$\$\dots\$$t@n$}. |
|
613 \begin{example} |
|
614 Reversing the effect of the parse translation in Example~\ref{list-enum} is |
|
615 accomplished by the following function: |
|
616 \begin{ttbox} |
|
617 fun make_enum (Const("op :",_) $ e $ es) = case es of |
|
618 Const("[]",_) => Const("sing",dummyT) $ e |
|
619 | _ => Const("enum",dummyT) $ e $ make_enum es; |
|
620 \end{ttbox} |
|
621 It translates \hbox{\tt$x$:$y$:$z$:[]} to \hbox{\tt[$x$,$y$,$z$]}. However, |
|
622 if the input does not terminate with an empty list, e.g.\ \hbox{\tt$x$:$xs$}, |
|
623 \verb$make_enum$ raises exception {\tt Match}. This signals that the |
|
624 attempted translation has failed and the term should be printed as is. |
|
625 The connection with Isabelle's pretty printer is established as follows: |
|
626 \begin{ttbox} |
|
627 fun enum_tr'[x,xs] = Const("enum",dummyT) $ |
|
628 make_enum(Const("op :",dummyT)$x$xs); |
|
629 val print_translation = [("op :", enum_tr')]; |
|
630 \end{ttbox} |
|
631 This declaration causes the printer to print \hbox{\tt enum_tr'[$x$,$y$]} |
|
632 whenever it finds \verb!Const("op :",_)$!$x$\verb!$!$y$. |
|
633 \end{example} |
|
634 \begin{example} |
|
635 In Example~\ref{SET} we showed how to translate the concrete syntax for set |
|
636 comprehension into the proper internal form. The string {\tt"\{$x$ | |
|
637 $P$\}"} now becomes {\tt Const("Set",_)\$Abs("$x$",_,$p$)}. If, however, |
|
638 the latter term were printed without translating it back, it would result |
|
639 in {\tt"Set(\%$x$.$P$)"}. Therefore the abstraction has to be turned back |
|
640 into a term that matches the concrete mixfix syntax: |
|
641 \begin{ttbox} |
|
642 fun set_tr'[Abs(x,T,P)] = |
|
643 let val (x',P') = variant_abs(x,T,P) |
|
644 in Const("SET",dummyT) $ Free(x',T) $ P' end; |
|
645 \end{ttbox} |
|
646 The function \verb$variant_abs$, a basic term manipulation function, replaces |
|
647 the bound variable $x$ by a {\tt Free} variable $x'$ having a unique name. A |
|
648 term produced by {\tt set_tr'} can now be printed according to the concrete |
|
649 syntax defined in Example~\ref{SET} above. |
|
650 |
|
651 Notice that the application of {\tt set_tr'} fails if the second component of |
|
652 the argument is not an abstraction, but for example just a {\tt Free} |
|
653 variable. This is intentional because it signals to the caller that the |
|
654 translation is inapplicable. As a result {\tt Const("Set",_)\$Free("P",_)} |
|
655 prints as {\tt"Set(P)"}. |
|
656 |
|
657 The full theory extension, including concrete syntax and both translation |
|
658 functions, has the following form: |
|
659 \begin{ttbox} |
|
660 types set 1 |
|
661 arities set :: (term)term |
|
662 consts Set :: "('a => o) => 'a set" |
|
663 SET :: "[id,o] => 'a set" ("\{_ | _\}") |
|
664 end |
|
665 ML |
|
666 fun set_tr[Free(s,T), p] = \dots; |
|
667 val parse_translation = [("SET", set_tr)]; |
|
668 fun set_tr'[Abs(x,T,P)] = \dots; |
|
669 val print_translation = [("Set", set_tr')]; |
|
670 \end{ttbox} |
|
671 \end{example} |
|
672 As during the parse translation process, the types attached to constants |
|
673 during print translation are ignored. Thus {\tt Const("SET",dummyT)} in |
|
674 {\tt set_tr'} above is acceptable. The types of {\tt Free}s and {\tt Var}s |
|
675 however must be preserved because they may get printed (see {\tt |
|
676 show_types}). |
|
677 |
|
678 \index{print translation|)} |
|
679 |
|
680 \subsection{Printing a term} |
|
681 |
|
682 Let $tab$ be the set of all string-function pairs of print translations in the |
|
683 current syntax. |
|
684 |
|
685 Terms are printed recursively; print translations are applied top down: |
|
686 \begin{itemize} |
|
687 \item {\tt Free($x$,_)} is printed as $x$. |
|
688 \item {\tt Var(($x$,$i$),_)} is printed as $x$, if $i = 0$ and $x$ does not |
|
689 end with a digit, as $x$ followed by $i$, if $i \neq 0$ and $x$ does not |
|
690 end with a digit, and as {\tt $x$.$i$}, if $x$ ends with a digit. Thus the |
|
691 following cases can arise: |
|
692 \begin{center} |
|
693 {\tt\begin{tabular}{cccc} |
|
694 \verb$Var(("v",0),_)$ & \verb$Var(("v",7),_)$ & \verb$Var(("v5",0),_)$ \\ |
|
695 "?v" & "?v7" & "?v5.0" |
|
696 \end{tabular}} |
|
697 \end{center} |
|
698 \item {\tt Abs($x@1$,_,Abs($x@2$,_,\dots Abs($x@n$,_,$p$)\dots))}, where $p$ |
|
699 is not an abstraction, is printed as {\tt \%$y@1\dots y@n$.$P$}, where $P$ |
|
700 is the result of printing $p$, and the $x@i$ are replaced by $y@i$. The |
|
701 latter are (possibly new) unique names. |
|
702 \item {\tt Bound($i$)} is printed as {\tt B.$i$} \footnote{The occurrence of |
|
703 such ``loose'' bound variables indicates that either you are trying to |
|
704 print a subterm of an abstraction, or there is something wrong with your |
|
705 print translations.}. |
|
706 \item The application {\tt$t =$ Const($c$,_)\$$t@1$\$\dots\$$t@n$} (where |
|
707 $n$ may be $0$!) is printed as follows: |
|
708 |
|
709 If there is a pair $(c,f)$ in $tab$, print $f[t@1,\dots,t@n]$. If this |
|
710 application raises exception {\tt Match} or there is no pair $(c,f)$ in |
|
711 $tab$, let $sy$ be the mixfix annotation associated with $c$. If there is |
|
712 no such $sy$, or if $sy$ does not have exactly $n$ argument positions, $t$ |
|
713 is printed as an application; otherwise $t$ is printed according to $sy$. |
|
714 |
|
715 All other applications are printed as applications. |
|
716 \end{itemize} |
|
717 Printing a term {\tt $c$\$$t@1$\$\dots\$$t@n$} as an application means |
|
718 printing it as {\tt $s$($s@1$,\dots,$s@n$)}, where $s@i$ is the result of |
|
719 printing $t@i$. If $c$ is a {\tt Const}, $s$ is its first argument; |
|
720 otherwise $s$ is the result of printing $c$ as described above. |
|
721 \medskip |
|
722 |
|
723 The printer also inserts parentheses where they are necessary for reasons |
|
724 of precedence. |
|
725 |
|
726 \section{Identifiers, constants, and type inference *} |
|
727 \label{Typing} |
|
728 |
|
729 There is one final step in the translation from strings to terms that we have |
|
730 not covered yet. It explains how constants are distinguished from {\tt Free}s |
|
731 and how {\tt Free}s and {\tt Var}s are typed. Both issues arise because {\tt |
|
732 Free}s and {\tt Var}s are not declared. |
|
733 |
|
734 An identifier $f$ that does not appear as a delimiter in the concrete syntax |
|
735 can be either a free variable or a constant. Since the parser knows only |
|
736 about those constants which appear in mixfix annotations, it parses $f$ as |
|
737 {\tt Free("$f$",dummyT)}, where \ttindex{dummyT} is the predefined dummy {\tt |
|
738 typ}. Although the parser produces these very raw terms, most user |
|
739 interface level functions like {\tt goal} type terms according to the given |
|
740 theory, say $T$. In a first step, every occurrence of {\tt Free($f$,_)} or |
|
741 {\tt Const($f$,_)} is replaced by {\tt Const($f$,$\tau$)}, provided there is |
|
742 a constant $f$ of {\tt typ} $\tau$ in $T$. This means that identifiers are |
|
743 treated as {\tt Free}s iff they are not declared in the theory. The types of |
|
744 the remaining {\tt Free}s (and {\tt Var}s) are inferred as in \ML. Type |
|
745 constraints can be used to remove ambiguities. |
|
746 |
|
747 One peculiarity of the current type inference algorithm is that variables |
|
748 with the same name must have the same type, irrespective of whether they are |
|
749 schematic, free or bound. For example, take the first-order formula $f(x) = x |
|
750 \land (\forall f.~ f=f)$ where ${=} :: [\alpha{::}term,\alpha]\To o$ and |
|
751 $\forall :: (\alpha{::}term\To o)\To o$. The first conjunct forces |
|
752 $x::\alpha{::}term$ and $f::\alpha\To\alpha$, the second one |
|
753 $f::\beta{::}term$. Although the two $f$'s are distinct, they are required to |
|
754 have the same type. Unifying $\alpha\To\alpha$ and $\beta{::}term$ fails |
|
755 because, in first-order logic, function types are not in class $term$. |
|
756 |
|
757 |
|
758 \section{Putting it all together} |
|
759 |
|
760 Having discussed the individual building blocks of a logic definition, it |
|
761 remains to be shown how they fit together. In particular we need to say how |
|
762 an object-logic syntax is hooked up to the meta-logic. Since all theorems |
|
763 must conform to the syntax for $prop$ (see Figure~\ref{MetaLogicSyntax}), |
|
764 that syntax has to be extended with the object-level syntax. Assume that the |
|
765 syntax of your object-logic defines a category $o$ of formulae. These |
|
766 formulae can now appear in axioms and theorems wherever $prop$ does if you |
|
767 add the production |
|
768 \[ prop ~=~ form. \] |
|
769 More precisely, you need a coercion from formulae to propositions: |
|
770 \begin{ttbox} |
|
771 Base = Pure + |
|
772 types o 0 |
|
773 arities o :: logic |
|
774 consts Trueprop :: "o => prop" ("_" 5) |
|
775 end |
|
776 \end{ttbox} |
|
777 The constant {\tt Trueprop} (the name is arbitrary) acts as an invisible |
|
778 coercion function. Assuming this definition resides in a file {\tt base.thy}, |
|
779 you have to load it with the command {\tt use_thy"base"}. |
|
780 |
|
781 One of the simplest nontrivial logics is {\em minimal logic} of |
|
782 implication. Its definition in Isabelle needs no advanced features but |
|
783 illustrates the overall mechanism quite nicely: |
|
784 \begin{ttbox} |
|
785 Hilbert = Base + |
|
786 consts "-->" :: "[o,o] => o" (infixr 10) |
|
787 rules |
|
788 K "P --> Q --> P" |
|
789 S "(P --> Q --> R) --> (P --> Q) --> P --> R" |
|
790 MP "[| P --> Q; P |] ==> Q" |
|
791 end |
|
792 \end{ttbox} |
|
793 After loading this definition you can start to prove theorems in this logic: |
|
794 \begin{ttbox} |
|
795 goal Hilbert.thy "P --> P"; |
|
796 {\out Level 0} |
|
797 {\out P --> P} |
|
798 {\out 1. P --> P} |
|
799 by (resolve_tac [Hilbert.MP] 1); |
|
800 {\out Level 1} |
|
801 {\out P --> P} |
|
802 {\out 1. ?P --> P --> P} |
|
803 {\out 2. ?P} |
|
804 by (resolve_tac [Hilbert.MP] 1); |
|
805 {\out Level 2} |
|
806 {\out P --> P} |
|
807 {\out 1. ?P1 --> ?P --> P --> P} |
|
808 {\out 2. ?P1} |
|
809 {\out 3. ?P} |
|
810 by (resolve_tac [Hilbert.S] 1); |
|
811 {\out Level 3} |
|
812 {\out P --> P} |
|
813 {\out 1. P --> ?Q2 --> P} |
|
814 {\out 2. P --> ?Q2} |
|
815 by (resolve_tac [Hilbert.K] 1); |
|
816 {\out Level 4} |
|
817 {\out P --> P} |
|
818 {\out 1. P --> ?Q2} |
|
819 by (resolve_tac [Hilbert.K] 1); |
|
820 {\out Level 5} |
|
821 {\out P --> P} |
|
822 {\out No subgoals!} |
|
823 \end{ttbox} |
|
824 As you can see, this Hilbert-style formulation of minimal logic is easy to |
|
825 define but difficult to use. The following natural deduction formulation is |
|
826 far preferable: |
|
827 \begin{ttbox} |
|
828 MinI = Base + |
|
829 consts "-->" :: "[o,o] => o" (infixr 10) |
|
830 rules |
|
831 impI "(P ==> Q) ==> P --> Q" |
|
832 impE "[| P --> Q; P |] ==> Q" |
|
833 end |
|
834 \end{ttbox} |
|
835 Note, however, that although the two systems are equivalent, this fact cannot |
|
836 be proved within Isabelle: {\tt S} and {\tt K} can be derived in \verb$MinI$ |
|
837 (exercise!), but {\tt impI} cannot be derived in \verb!Hilbert!. The reason |
|
838 is that {\tt impI} is only an {\em admissible} rule in \verb!Hilbert!, |
|
839 something that can only be shown by induction over all possible proofs in |
|
840 \verb!Hilbert!. |
|
841 |
|
842 It is a very simple matter to extend minimal logic with falsity: |
|
843 \begin{ttbox} |
|
844 MinIF = MinI + |
|
845 consts False :: "o" |
|
846 rules |
|
847 FalseE "False ==> P" |
|
848 end |
|
849 \end{ttbox} |
|
850 On the other hand, we may wish to introduce conjunction only: |
|
851 \begin{ttbox} |
|
852 MinC = Base + |
|
853 consts "&" :: "[o,o] => o" (infixr 30) |
|
854 rules |
|
855 conjI "[| P; Q |] ==> P & Q" |
|
856 conjE1 "P & Q ==> P" |
|
857 conjE2 "P & Q ==> Q" |
|
858 end |
|
859 \end{ttbox} |
|
860 And if we want to have all three connectives together, we define: |
|
861 \begin{ttbox} |
|
862 MinIFC = MinIF + MinC |
|
863 \end{ttbox} |
|
864 Now we can prove mixed theorems like |
|
865 \begin{ttbox} |
|
866 goal MinIFC.thy "P & False --> Q"; |
|
867 by (resolve_tac [MinI.impI] 1); |
|
868 by (dresolve_tac [MinC.conjE2] 1); |
|
869 by (eresolve_tac [MinIF.FalseE] 1); |
|
870 \end{ttbox} |
|
871 Try this as an exercise! |