author | wenzelm |
Sun, 18 May 2008 15:04:41 +0200 | |
changeset 26948 | efe3e0e235d6 |
parent 20093 | 164a42b7385f |
child 30184 | 37969710e61f |
permissions | -rw-r--r-- |
320 | 1 |
%% $Id$ |
2 |
\chapter{Defining Logics} \label{Defining-Logics} |
|
3 |
This chapter explains how to define new formal systems --- in particular, |
|
4 |
their concrete syntax. While Isabelle can be regarded as a theorem prover |
|
5 |
for set theory, higher-order logic or the sequent calculus, its |
|
6 |
distinguishing feature is support for the definition of new logics. |
|
7 |
||
8 |
Isabelle logics are hierarchies of theories, which are described and |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
9 |
illustrated in |
320 | 10 |
\iflabelundefined{sec:defining-theories}{{\em Introduction to Isabelle}}% |
11 |
{\S\ref{sec:defining-theories}}. That material, together with the theory |
|
12 |
files provided in the examples directories, should suffice for all simple |
|
13 |
applications. The easiest way to define a new theory is by modifying a |
|
14 |
copy of an existing theory. |
|
15 |
||
16 |
This chapter documents the meta-logic syntax, mixfix declarations and |
|
17 |
pretty printing. The extended examples in \S\ref{sec:min_logics} |
|
18 |
demonstrate the logical aspects of the definition of theories. |
|
19 |
||
20 |
||
21 |
\section{Priority grammars} \label{sec:priority_grammars} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
22 |
\index{priority grammars|(} |
320 | 23 |
|
24 |
A context-free grammar contains a set of {\bf nonterminal symbols}, a set of |
|
25 |
{\bf terminal symbols} and a set of {\bf productions}\index{productions}. |
|
26 |
Productions have the form ${A=\gamma}$, where $A$ is a nonterminal and |
|
27 |
$\gamma$ is a string of terminals and nonterminals. One designated |
|
28 |
nonterminal is called the {\bf start symbol}. The language defined by the |
|
29 |
grammar consists of all strings of terminals that can be derived from the |
|
30 |
start symbol by applying productions as rewrite rules. |
|
31 |
||
32 |
The syntax of an Isabelle logic is specified by a {\bf priority |
|
33 |
grammar}.\index{priorities} Each nonterminal is decorated by an integer |
|
34 |
priority, as in~$A^{(p)}$. A nonterminal $A^{(p)}$ in a derivation may be |
|
14231 | 35 |
rewritten using a production $A^{(q)} = \gamma$ only if~$p \leq q$. Any |
320 | 36 |
priority grammar can be translated into a normal context free grammar by |
37 |
introducing new nonterminals and productions. |
|
38 |
||
39 |
Formally, a set of context free productions $G$ induces a derivation |
|
40 |
relation $\longrightarrow@G$. Let $\alpha$ and $\beta$ denote strings of |
|
41 |
terminal or nonterminal symbols. Then |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
42 |
\[ \alpha\, A^{(p)}\, \beta ~\longrightarrow@G~ \alpha\,\gamma\,\beta \] |
14231 | 43 |
if and only if $G$ contains some production $A^{(q)}=\gamma$ for~$p \leq q$. |
320 | 44 |
|
45 |
The following simple grammar for arithmetic expressions demonstrates how |
|
46 |
binding power and associativity of operators can be enforced by priorities. |
|
47 |
\begin{center} |
|
48 |
\begin{tabular}{rclr} |
|
49 |
$A^{(9)}$ & = & {\tt0} \\ |
|
50 |
$A^{(9)}$ & = & {\tt(} $A^{(0)}$ {\tt)} \\ |
|
51 |
$A^{(0)}$ & = & $A^{(0)}$ {\tt+} $A^{(1)}$ \\ |
|
52 |
$A^{(2)}$ & = & $A^{(3)}$ {\tt*} $A^{(2)}$ \\ |
|
53 |
$A^{(3)}$ & = & {\tt-} $A^{(3)}$ |
|
54 |
\end{tabular} |
|
55 |
\end{center} |
|
56 |
The choice of priorities determines that {\tt -} binds tighter than {\tt *}, |
|
57 |
which binds tighter than {\tt +}. Furthermore {\tt +} associates to the |
|
58 |
left and {\tt *} to the right. |
|
59 |
||
60 |
For clarity, grammars obey these conventions: |
|
61 |
\begin{itemize} |
|
62 |
\item All priorities must lie between~0 and \ttindex{max_pri}, which is a |
|
63 |
some fixed integer. Sometimes {\tt max_pri} is written as $\infty$. |
|
64 |
\item Priority 0 on the right-hand side and priority \ttindex{max_pri} on |
|
65 |
the left-hand side may be omitted. |
|
66 |
\item The production $A^{(p)} = \alpha$ is written as $A = \alpha~(p)$; the |
|
67 |
priority of the left-hand side actually appears in a column on the far |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
68 |
right. |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
69 |
\item Alternatives are separated by~$|$. |
320 | 70 |
\item Repetition is indicated by dots~(\dots) in an informal but obvious |
71 |
way. |
|
72 |
\end{itemize} |
|
73 |
||
74 |
Using these conventions and assuming $\infty=9$, the grammar |
|
75 |
takes the form |
|
76 |
\begin{center} |
|
77 |
\begin{tabular}{rclc} |
|
78 |
$A$ & = & {\tt0} & \hspace*{4em} \\ |
|
79 |
& $|$ & {\tt(} $A$ {\tt)} \\ |
|
80 |
& $|$ & $A$ {\tt+} $A^{(1)}$ & (0) \\ |
|
81 |
& $|$ & $A^{(3)}$ {\tt*} $A^{(2)}$ & (2) \\ |
|
82 |
& $|$ & {\tt-} $A^{(3)}$ & (3) |
|
83 |
\end{tabular} |
|
84 |
\end{center} |
|
85 |
\index{priority grammars|)} |
|
86 |
||
87 |
||
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4543
diff
changeset
|
88 |
\begin{figure}\small |
320 | 89 |
\begin{center} |
90 |
\begin{tabular}{rclc} |
|
711
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
91 |
$any$ &=& $prop$ ~~$|$~~ $logic$ \\\\ |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
92 |
$prop$ &=& {\tt(} $prop$ {\tt)} \\ |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
93 |
&$|$& $prop^{(4)}$ {\tt::} $type$ & (3) \\ |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
94 |
&$|$& {\tt PROP} $aprop$ \\ |
711
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
95 |
&$|$& $any^{(3)}$ {\tt ==} $any^{(2)}$ & (2) \\ |
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
96 |
&$|$& $any^{(3)}$ {\tt =?=} $any^{(2)}$ & (2) \\ |
320 | 97 |
&$|$& $prop^{(2)}$ {\tt ==>} $prop^{(1)}$ & (1) \\ |
98 |
&$|$& {\tt[|} $prop$ {\tt;} \dots {\tt;} $prop$ {\tt|]} {\tt==>} $prop^{(1)}$ & (1) \\ |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
99 |
&$|$& {\tt!!} $idts$ {\tt.} $prop$ & (0) \\ |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
100 |
&$|$& {\tt OFCLASS} {\tt(} $type$ {\tt,} $logic$ {\tt)} \\\\ |
4543 | 101 |
$aprop$ &=& $id$ ~~$|$~~ $longid$ ~~$|$~~ $var$ |
711
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
102 |
~~$|$~~ $logic^{(\infty)}$ {\tt(} $any$ {\tt,} \dots {\tt,} $any$ {\tt)} \\\\ |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
103 |
$logic$ &=& {\tt(} $logic$ {\tt)} \\ |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
104 |
&$|$& $logic^{(4)}$ {\tt::} $type$ & (3) \\ |
4543 | 105 |
&$|$& $id$ ~~$|$~~ $longid$ ~~$|$~~ $var$ |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
106 |
~~$|$~~ $logic^{(\infty)}$ {\tt(} $any$ {\tt,} \dots {\tt,} $any$ {\tt)} \\ |
11621 | 107 |
&$|$& {\tt \%} $pttrns$ {\tt.} $any^{(3)}$ & (3) \\ |
108 |
&$|$& {\tt TYPE} {\tt(} $type$ {\tt)} \\\\ |
|
320 | 109 |
$idts$ &=& $idt$ ~~$|$~~ $idt^{(1)}$ $idts$ \\\\ |
110 |
$idt$ &=& $id$ ~~$|$~~ {\tt(} $idt$ {\tt)} \\ |
|
111 |
&$|$& $id$ {\tt ::} $type$ & (0) \\\\ |
|
3694 | 112 |
$pttrns$ &=& $pttrn$ ~~$|$~~ $pttrn^{(1)}$ $pttrns$ \\\\ |
113 |
$pttrn$ &=& $idt$ \\\\ |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
114 |
$type$ &=& {\tt(} $type$ {\tt)} \\ |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
115 |
&$|$& $tid$ ~~$|$~~ $tvar$ ~~$|$~~ $tid$ {\tt::} $sort$ |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
116 |
~~$|$~~ $tvar$ {\tt::} $sort$ \\ |
320 | 117 |
&$|$& $id$ ~~$|$~~ $type^{(\infty)}$ $id$ |
118 |
~~$|$~~ {\tt(} $type$ {\tt,} \dots {\tt,} $type$ {\tt)} $id$ \\ |
|
4543 | 119 |
&$|$& $longid$ ~~$|$~~ $type^{(\infty)}$ $longid$ |
120 |
~~$|$~~ {\tt(} $type$ {\tt,} \dots {\tt,} $type$ {\tt)} $longid$ \\ |
|
320 | 121 |
&$|$& $type^{(1)}$ {\tt =>} $type$ & (0) \\ |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
122 |
&$|$& {\tt[} $type$ {\tt,} \dots {\tt,} $type$ {\tt]} {\tt=>} $type$&(0) \\\\ |
4543 | 123 |
$sort$ &=& $id$ ~~$|$~~ $longid$ ~~$|$~~ {\tt\ttlbrace\ttrbrace} ~~$|$~~ |
8136 | 124 |
{\tt\ttlbrace} $id$ ~$|$~ $longid${\tt,}\dots{\tt,} $id$ ~$|$~$longid$ {\tt\ttrbrace} |
320 | 125 |
\end{tabular} |
126 |
\index{*PROP symbol} |
|
127 |
\index{*== symbol}\index{*=?= symbol}\index{*==> symbol} |
|
128 |
\index{*:: symbol}\index{*=> symbol} |
|
332 | 129 |
\index{sort constraints} |
130 |
%the index command: a percent is permitted, but braces must match! |
|
320 | 131 |
\index{%@{\tt\%} symbol} |
132 |
\index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol} |
|
133 |
\index{*[ symbol}\index{*] symbol} |
|
134 |
\index{*"!"! symbol} |
|
135 |
\index{*"["| symbol} |
|
136 |
\index{*"|"] symbol} |
|
137 |
\end{center} |
|
138 |
\caption{Meta-logic syntax}\label{fig:pure_gram} |
|
139 |
\end{figure} |
|
140 |
||
141 |
||
142 |
\section{The Pure syntax} \label{sec:basic_syntax} |
|
143 |
\index{syntax!Pure|(} |
|
144 |
||
145 |
At the root of all object-logics lies the theory \thydx{Pure}. It |
|
146 |
contains, among many other things, the Pure syntax. An informal account of |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
147 |
this basic syntax (types, terms and formulae) appears in |
320 | 148 |
\iflabelundefined{sec:forward}{{\em Introduction to Isabelle}}% |
149 |
{\S\ref{sec:forward}}. A more precise description using a priority grammar |
|
150 |
appears in Fig.\ts\ref{fig:pure_gram}. It defines the following |
|
151 |
nonterminals: |
|
152 |
\begin{ttdescription} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
153 |
\item[\ndxbold{any}] denotes any term. |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
154 |
|
711
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
155 |
\item[\ndxbold{prop}] denotes terms of type {\tt prop}. These are formulae |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
156 |
of the meta-logic. Note that user constants of result type {\tt prop} |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
157 |
(i.e.\ $c :: \ldots \To prop$) should always provide concrete syntax. |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
158 |
Otherwise atomic propositions with head $c$ may be printed incorrectly. |
320 | 159 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
160 |
\item[\ndxbold{aprop}] denotes atomic propositions. |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
161 |
|
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
162 |
%% FIXME huh!? |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
163 |
% These typically |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
164 |
% include the judgement forms of the object-logic; its definition |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
165 |
% introduces a meta-level predicate for each judgement form. |
320 | 166 |
|
711
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
167 |
\item[\ndxbold{logic}] denotes terms whose type belongs to class |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
168 |
\cldx{logic}, excluding type \tydx{prop}. |
320 | 169 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
170 |
\item[\ndxbold{idts}] denotes a list of identifiers, possibly constrained |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
171 |
by types. |
3694 | 172 |
|
173 |
\item[\ndxbold{pttrn}, \ndxbold{pttrns}] denote patterns for |
|
174 |
abstraction, cases etc. Initially the same as $idt$ and $idts$, |
|
14231 | 175 |
these are intended to be augmented by user extensions. |
320 | 176 |
|
177 |
\item[\ndxbold{type}] denotes types of the meta-logic. |
|
178 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
179 |
\item[\ndxbold{sort}] denotes meta-level sorts. |
320 | 180 |
\end{ttdescription} |
181 |
||
182 |
\begin{warn} |
|
183 |
In {\tt idts}, note that \verb|x::nat y| is parsed as \verb|x::(nat y)|, |
|
184 |
treating {\tt y} like a type constructor applied to {\tt nat}. The |
|
185 |
likely result is an error message. To avoid this interpretation, use |
|
186 |
parentheses and write \verb|(x::nat) y|. |
|
332 | 187 |
\index{type constraints}\index{*:: symbol} |
320 | 188 |
|
189 |
Similarly, \verb|x::nat y::nat| is parsed as \verb|x::(nat y::nat)| and |
|
190 |
yields an error. The correct form is \verb|(x::nat) (y::nat)|. |
|
191 |
\end{warn} |
|
192 |
||
452 | 193 |
\begin{warn} |
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3318
diff
changeset
|
194 |
Type constraints bind very weakly. For example, \verb!x<y::nat! is normally |
711
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
195 |
parsed as \verb!(x<y)::nat!, unless \verb$<$ has priority of 3 or less, in |
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3318
diff
changeset
|
196 |
which case the string is likely to be ambiguous. The correct form is |
452 | 197 |
\verb!x<(y::nat)!. |
198 |
\end{warn} |
|
320 | 199 |
|
867 | 200 |
\subsection{Logical types and default syntax}\label{logical-types} |
201 |
\index{lambda calc@$\lambda$-calculus} |
|
202 |
||
203 |
Isabelle's representation of mathematical languages is based on the |
|
204 |
simply typed $\lambda$-calculus. All logical types, namely those of |
|
205 |
class \cldx{logic}, are automatically equipped with a basic syntax of |
|
206 |
types, identifiers, variables, parentheses, $\lambda$-abstraction and |
|
207 |
application. |
|
208 |
\begin{warn} |
|
209 |
Isabelle combines the syntaxes for all types of class \cldx{logic} by |
|
210 |
mapping all those types to the single nonterminal $logic$. Thus all |
|
211 |
productions of $logic$, in particular $id$, $var$ etc, become available. |
|
212 |
\end{warn} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
213 |
|
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
214 |
|
320 | 215 |
\subsection{Lexical matters} |
216 |
The parser does not process input strings directly. It operates on token |
|
217 |
lists provided by Isabelle's \bfindex{lexer}. There are two kinds of |
|
218 |
tokens: \bfindex{delimiters} and \bfindex{name tokens}. |
|
219 |
||
220 |
\index{reserved words} |
|
221 |
Delimiters can be regarded as reserved words of the syntax. You can |
|
222 |
add new ones when extending theories. In Fig.\ts\ref{fig:pure_gram} they |
|
223 |
appear in typewriter font, for example {\tt ==}, {\tt =?=} and |
|
224 |
{\tt PROP}\@. |
|
225 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
226 |
Name tokens have a predefined syntax. The lexer distinguishes six disjoint |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
227 |
classes of names: \rmindex{identifiers}, \rmindex{unknowns}, type |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
228 |
identifiers\index{type identifiers}, type unknowns\index{type unknowns}, |
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3318
diff
changeset
|
229 |
\rmindex{numerals}, \rmindex{strings}. They are denoted by \ndxbold{id}, |
14948 | 230 |
\ndxbold{var}, \ndxbold{tid}, \ndxbold{tvar}, \ndxbold{num}, \ndxbold{xnum}, |
231 |
\ndxbold{xstr}, respectively. Typical examples are {\tt x}, {\tt ?x7}, {\tt |
|
232 |
'a}, {\tt ?'a3}, {\tt \#42}, {\tt ''foo bar''}. Here is the precise syntax: |
|
320 | 233 |
\begin{eqnarray*} |
14955 | 234 |
id & = & letter\,quasiletter^* \\ |
235 |
longid & = & id (\mbox{\tt .}id)^+ \\ |
|
320 | 236 |
var & = & \mbox{\tt ?}id ~~|~~ \mbox{\tt ?}id\mbox{\tt .}nat \\ |
237 |
tid & = & \mbox{\tt '}id \\ |
|
238 |
tvar & = & \mbox{\tt ?}tid ~~|~~ |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
239 |
\mbox{\tt ?}tid\mbox{\tt .}nat \\ |
20093 | 240 |
num & = & nat ~~|~~ \mbox{\tt-}nat ~~|~~ \verb,0x,\,hex^+ ~~|~~ \verb,0b,\,bin^+ \\ |
241 |
xnum & = & \mbox{\tt \#}num \\ |
|
14955 | 242 |
xstr & = & \mbox{\tt ''~\dots~\tt ''} \\[1ex] |
14960 | 243 |
letter & = & latin ~|~ \verb,\<,latin\verb,>, ~|~ \verb,\<,latin\,latin\verb,>, ~|~ greek ~| \\ |
244 |
& & \verb,\<^isub>, ~|~ \verb,\<^isup>, \\ |
|
245 |
quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\ |
|
14948 | 246 |
latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\ |
247 |
digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\ |
|
248 |
nat & = & digit^+ \\ |
|
20093 | 249 |
bin & = & \verb,0, ~|~ \verb,1, \\ |
250 |
hex & = & digit ~|~ \verb,a, ~|~ \dots ~|~ \verb,f, ~|~ \verb,A, ~|~ \dots ~|~ \verb,F, \\ |
|
14955 | 251 |
greek & = & \verb,\<alpha>, ~|~ \verb,\<beta>, ~|~ \verb,\<gamma>, ~|~ \verb,\<delta>, ~| \\ |
252 |
& & \verb,\<epsilon>, ~|~ \verb,\<zeta>, ~|~ \verb,\<eta>, ~|~ \verb,\<theta>, ~| \\ |
|
253 |
& & \verb,\<iota>, ~|~ \verb,\<kappa>, ~|~ \verb,\<mu>, ~|~ \verb,\<nu>, ~| \\ |
|
254 |
& & \verb,\<xi>, ~|~ \verb,\<pi>, ~|~ \verb,\<rho>, ~|~ \verb,\<sigma>, ~| \\ |
|
255 |
& & \verb,\<tau>, ~|~ \verb,\<upsilon>, ~|~ \verb,\<phi>, ~|~ \verb,\<psi>, ~| \\ |
|
256 |
& & \verb,\<omega>, ~|~ \verb,\<Gamma>, ~|~ \verb,\<Delta>, ~|~ \verb,\<Theta>, ~| \\ |
|
257 |
& & \verb,\<Lambda>, ~|~ \verb,\<Xi>, ~|~ \verb,\<Pi>, ~|~ \verb,\<Sigma>, ~| \\ |
|
258 |
& & \verb,\<Upsilon>, ~|~ \verb,\<Phi>, ~|~ \verb,\<Psi>, ~|~ \verb,\<Omega>, \\ |
|
320 | 259 |
\end{eqnarray*} |
4543 | 260 |
The lexer repeatedly takes the longest prefix of the input string that |
261 |
forms a valid token. A maximal prefix that is both a delimiter and a |
|
262 |
name is treated as a delimiter. Spaces, tabs, newlines and formfeeds |
|
263 |
are separators; they never occur within tokens, except those of class |
|
264 |
$xstr$. |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
265 |
|
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
266 |
\medskip |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
267 |
Delimiters need not be separated by white space. For example, if {\tt -} |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
268 |
is a delimiter but {\tt --} is not, then the string {\tt --} is treated as |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
269 |
two consecutive occurrences of the token~{\tt -}. In contrast, \ML\ |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
270 |
treats {\tt --} as a single symbolic name. The consequence of Isabelle's |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
271 |
more liberal scheme is that the same string may be parsed in different ways |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
272 |
after extending the syntax: after adding {\tt --} as a delimiter, the input |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
273 |
{\tt --} is treated as a single token. |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
274 |
|
320 | 275 |
A \ndxbold{var} or \ndxbold{tvar} describes an unknown, which is internally |
276 |
a pair of base name and index (\ML\ type \mltydx{indexname}). These |
|
277 |
components are either separated by a dot as in {\tt ?x.1} or {\tt ?x7.3} or |
|
278 |
run together as in {\tt ?x1}. The latter form is possible if the base name |
|
279 |
does not end with digits. If the index is 0, it may be dropped altogether: |
|
280 |
{\tt ?x} abbreviates both {\tt ?x0} and {\tt ?x.0}. |
|
281 |
||
14948 | 282 |
Tokens of class $num$, $xnum$ or $xstr$ are not used by the meta-logic. |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
283 |
Object-logics may provide numerals and string constants by adding appropriate |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
284 |
productions and translation functions. |
320 | 285 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
286 |
\medskip |
320 | 287 |
Although name tokens are returned from the lexer rather than the parser, it |
288 |
is more logical to regard them as nonterminals. Delimiters, however, are |
|
289 |
terminals; they are just syntactic sugar and contribute nothing to the |
|
290 |
abstract syntax tree. |
|
291 |
||
292 |
||
3108 | 293 |
\subsection{*Inspecting the syntax} \label{pg:print_syn} |
320 | 294 |
\begin{ttbox} |
295 |
syn_of : theory -> Syntax.syntax |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
296 |
print_syntax : theory -> unit |
320 | 297 |
Syntax.print_syntax : Syntax.syntax -> unit |
298 |
Syntax.print_gram : Syntax.syntax -> unit |
|
299 |
Syntax.print_trans : Syntax.syntax -> unit |
|
300 |
\end{ttbox} |
|
301 |
The abstract type \mltydx{Syntax.syntax} allows manipulation of syntaxes |
|
302 |
in \ML. You can display values of this type by calling the following |
|
303 |
functions: |
|
304 |
\begin{ttdescription} |
|
305 |
\item[\ttindexbold{syn_of} {\it thy}] returns the syntax of the Isabelle |
|
306 |
theory~{\it thy} as an \ML\ value. |
|
307 |
||
8136 | 308 |
\item[\ttindexbold{print_syntax} $thy$] uses {\tt Syntax.print_syntax} |
309 |
to display the syntax part of theory $thy$. |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
310 |
|
320 | 311 |
\item[\ttindexbold{Syntax.print_syntax} {\it syn}] shows virtually all |
312 |
information contained in the syntax {\it syn}. The displayed output can |
|
313 |
be large. The following two functions are more selective. |
|
314 |
||
315 |
\item[\ttindexbold{Syntax.print_gram} {\it syn}] shows the grammar part |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
316 |
of~{\it syn}, namely the lexicon, logical types and productions. These are |
320 | 317 |
discussed below. |
318 |
||
319 |
\item[\ttindexbold{Syntax.print_trans} {\it syn}] shows the translation |
|
320 |
part of~{\it syn}, namely the constants, parse/print macros and |
|
321 |
parse/print translations. |
|
322 |
\end{ttdescription} |
|
323 |
||
12465 | 324 |
The output of the above print functions is divided into labelled sections. |
325 |
The grammar is represented by {\tt lexicon}, {\tt logtypes} and {\tt prods}. |
|
326 |
The rest refers to syntactic translations and macro expansion. Here is an |
|
320 | 327 |
explanation of the various sections. |
328 |
\begin{description} |
|
329 |
\item[{\tt lexicon}] lists the delimiters used for lexical |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
330 |
analysis.\index{delimiters} |
320 | 331 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
332 |
\item[{\tt logtypes}] lists the types that are regarded the same as {\tt |
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3318
diff
changeset
|
333 |
logic} syntactically. Thus types of object-logics (e.g.\ {\tt nat}, say) |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
334 |
will be automatically equipped with the standard syntax of |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
335 |
$\lambda$-calculus. |
320 | 336 |
|
337 |
\item[{\tt prods}] lists the \rmindex{productions} of the priority grammar. |
|
338 |
The nonterminal $A^{(n)}$ is rendered in {\sc ascii} as {\tt $A$[$n$]}. |
|
339 |
Each delimiter is quoted. Some productions are shown with {\tt =>} and |
|
340 |
an attached string. These strings later become the heads of parse |
|
341 |
trees; they also play a vital role when terms are printed (see |
|
342 |
\S\ref{sec:asts}). |
|
343 |
||
344 |
Productions with no strings attached are called {\bf copy |
|
345 |
productions}\indexbold{productions!copy}. Their right-hand side must |
|
346 |
have exactly one nonterminal symbol (or name token). The parser does |
|
347 |
not create a new parse tree node for copy productions, but simply |
|
348 |
returns the parse tree of the right-hand symbol. |
|
349 |
||
350 |
If the right-hand side consists of a single nonterminal with no |
|
351 |
delimiters, then the copy production is called a {\bf chain |
|
352 |
production}. Chain productions act as abbreviations: |
|
353 |
conceptually, they are removed from the grammar by adding new |
|
354 |
productions. Priority information attached to chain productions is |
|
355 |
ignored; only the dummy value $-1$ is displayed. |
|
3108 | 356 |
|
357 |
\item[\ttindex{print_modes}] lists the alternative print modes |
|
358 |
provided by this syntax (see \S\ref{sec:prmodes}). |
|
320 | 359 |
|
360 |
\item[{\tt consts}, {\tt parse_rules}, {\tt print_rules}] |
|
361 |
relate to macros (see \S\ref{sec:macros}). |
|
362 |
||
363 |
\item[{\tt parse_ast_translation}, {\tt print_ast_translation}] |
|
364 |
list sets of constants that invoke translation functions for abstract |
|
365 |
syntax trees. Section \S\ref{sec:asts} below discusses this obscure |
|
366 |
matter.\index{constants!for translations} |
|
367 |
||
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4543
diff
changeset
|
368 |
\item[{\tt parse_translation}, {\tt print_translation}] list the sets |
320 | 369 |
of constants that invoke translation functions for terms (see |
370 |
\S\ref{sec:tr_funs}). |
|
371 |
\end{description} |
|
372 |
\index{syntax!Pure|)} |
|
373 |
||
374 |
||
375 |
\section{Mixfix declarations} \label{sec:mixfix} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
376 |
\index{mixfix declarations|(} |
320 | 377 |
|
378 |
When defining a theory, you declare new constants by giving their names, |
|
379 |
their type, and an optional {\bf mixfix annotation}. Mixfix annotations |
|
380 |
allow you to extend Isabelle's basic $\lambda$-calculus syntax with |
|
381 |
readable notation. They can express any context-free priority grammar. |
|
382 |
Isabelle syntax definitions are inspired by \OBJ~\cite{OBJ}; they are more |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
383 |
general than the priority declarations of \ML\ and Prolog. |
320 | 384 |
|
385 |
A mixfix annotation defines a production of the priority grammar. It |
|
386 |
describes the concrete syntax, the translation to abstract syntax, and the |
|
387 |
pretty printing. Special case annotations provide a simple means of |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
388 |
specifying infix operators and binders. |
320 | 389 |
|
390 |
\subsection{The general mixfix form} |
|
391 |
Here is a detailed account of mixfix declarations. Suppose the following |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
392 |
line occurs within a {\tt consts} or {\tt syntax} section of a {\tt .thy} |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
393 |
file: |
320 | 394 |
\begin{center} |
395 |
{\tt $c$ ::\ "$\sigma$" ("$template$" $ps$ $p$)} |
|
396 |
\end{center} |
|
332 | 397 |
This constant declaration and mixfix annotation are interpreted as follows: |
320 | 398 |
\begin{itemize}\index{productions} |
399 |
\item The string {\tt $c$} is the name of the constant associated with the |
|
400 |
production; unless it is a valid identifier, it must be enclosed in |
|
401 |
quotes. If $c$ is empty (given as~{\tt ""}) then this is a copy |
|
402 |
production.\index{productions!copy} Otherwise, parsing an instance of the |
|
403 |
phrase $template$ generates the \AST{} {\tt ("$c$" $a@1$ $\ldots$ |
|
404 |
$a@n$)}, where $a@i$ is the \AST{} generated by parsing the $i$-th |
|
405 |
argument. |
|
406 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
407 |
\item The constant $c$, if non-empty, is declared to have type $\sigma$ |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
408 |
({\tt consts} section only). |
320 | 409 |
|
410 |
\item The string $template$ specifies the right-hand side of |
|
411 |
the production. It has the form |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
412 |
\[ w@0 \;_\; w@1 \;_\; \ldots \;_\; w@n, \] |
320 | 413 |
where each occurrence of {\tt_} denotes an argument position and |
414 |
the~$w@i$ do not contain~{\tt _}. (If you want a literal~{\tt _} in |
|
415 |
the concrete syntax, you must escape it as described below.) The $w@i$ |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
416 |
may consist of \rmindex{delimiters}, spaces or |
320 | 417 |
\rmindex{pretty printing} annotations (see below). |
418 |
||
419 |
\item The type $\sigma$ specifies the production's nonterminal symbols |
|
420 |
(or name tokens). If $template$ is of the form above then $\sigma$ |
|
421 |
must be a function type with at least~$n$ argument positions, say |
|
422 |
$\sigma = [\tau@1, \dots, \tau@n] \To \tau$. Nonterminal symbols are |
|
423 |
derived from the types $\tau@1$, \ldots,~$\tau@n$, $\tau$ as described |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
424 |
below. Any of these may be function types. |
320 | 425 |
|
426 |
\item The optional list~$ps$ may contain at most $n$ integers, say {\tt |
|
427 |
[$p@1$, $\ldots$, $p@m$]}, where $p@i$ is the minimal |
|
428 |
priority\indexbold{priorities} required of any phrase that may appear |
|
429 |
as the $i$-th argument. Missing priorities default to~0. |
|
4543 | 430 |
|
431 |
\item The integer $p$ is the priority of this production. If |
|
432 |
omitted, it defaults to the maximal priority. Priorities range |
|
433 |
between 0 and \ttindexbold{max_pri} (= 1000). |
|
320 | 434 |
|
435 |
\end{itemize} |
|
436 |
% |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
437 |
The resulting production is \[ A^{(p)}= w@0\, A@1^{(p@1)}\, w@1\, |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
438 |
A@2^{(p@2)}\, \dots\, A@n^{(p@n)}\, w@n \] where $A$ and the $A@i$ are the |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
439 |
nonterminals corresponding to the types $\tau$ and $\tau@i$ respectively. |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
440 |
The nonterminal symbol associated with a type $(\ldots)ty$ is {\tt logic}, if |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
441 |
this is a logical type (namely one of class {\tt logic} excluding {\tt |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
442 |
prop}). Otherwise it is $ty$ (note that only the outermost type constructor |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
443 |
is taken into account). Finally, the nonterminal of a type variable is {\tt |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
444 |
any}. |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
445 |
|
911
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
885
diff
changeset
|
446 |
\begin{warn} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
447 |
Theories must sometimes declare types for purely syntactic purposes --- |
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3318
diff
changeset
|
448 |
merely playing the role of nonterminals. One example is \tydx{type}, the |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
449 |
built-in type of types. This is a `type of all types' in the syntactic |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
450 |
sense only. Do not declare such types under {\tt arities} as belonging to |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
451 |
class {\tt logic}\index{*logic class}, for that would make them useless as |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
452 |
separate nonterminal symbols. |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
453 |
\end{warn} |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
454 |
|
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
455 |
Associating nonterminals with types allows a constant's type to specify |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
456 |
syntax as well. We can declare the function~$f$ to have type $[\tau@1, |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
457 |
\ldots, \tau@n]\To \tau$ and, through a mixfix annotation, specify the layout |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
458 |
of the function's $n$ arguments. The constant's name, in this case~$f$, will |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
459 |
also serve as the label in the abstract syntax tree. |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
460 |
|
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
461 |
You may also declare mixfix syntax without adding constants to the theory's |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
462 |
signature, by using a {\tt syntax} section instead of {\tt consts}. Thus a |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
463 |
production need not map directly to a logical function (this typically |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
464 |
requires additional syntactic translations, see also |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
465 |
Chapter~\ref{chap:syntax}). |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
466 |
|
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
467 |
|
911
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
885
diff
changeset
|
468 |
\medskip |
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
885
diff
changeset
|
469 |
As a special case of the general mixfix declaration, the form |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
470 |
\begin{center} |
911
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
885
diff
changeset
|
471 |
{\tt $c$ ::\ "$\sigma$" ("$template$")} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
472 |
\end{center} |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
473 |
specifies no priorities. The resulting production puts no priority |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
474 |
constraints on any of its arguments and has maximal priority itself. |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
475 |
Omitting priorities in this manner is prone to syntactic ambiguities unless |
3098 | 476 |
the production's right-hand side is fully bracketed, as in |
477 |
\verb|"if _ then _ else _ fi"|. |
|
320 | 478 |
|
479 |
Omitting the mixfix annotation completely, as in {\tt $c$ ::\ "$\sigma$"}, |
|
480 |
is sensible only if~$c$ is an identifier. Otherwise you will be unable to |
|
481 |
write terms involving~$c$. |
|
482 |
||
483 |
||
484 |
\subsection{Example: arithmetic expressions} |
|
485 |
\index{examples!of mixfix declarations} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
486 |
This theory specification contains a {\tt syntax} section with mixfix |
320 | 487 |
declarations encoding the priority grammar from |
488 |
\S\ref{sec:priority_grammars}: |
|
489 |
\begin{ttbox} |
|
3108 | 490 |
ExpSyntax = Pure + |
320 | 491 |
types |
492 |
exp |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
493 |
syntax |
1387 | 494 |
"0" :: exp ("0" 9) |
495 |
"+" :: [exp, exp] => exp ("_ + _" [0, 1] 0) |
|
496 |
"*" :: [exp, exp] => exp ("_ * _" [3, 2] 2) |
|
497 |
"-" :: exp => exp ("- _" [3] 3) |
|
320 | 498 |
end |
499 |
\end{ttbox} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
500 |
Executing {\tt Syntax.print_gram} reveals the productions derived from the |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
501 |
above mixfix declarations (lots of additional information deleted): |
320 | 502 |
\begin{ttbox} |
3108 | 503 |
Syntax.print_gram (syn_of ExpSyntax.thy); |
320 | 504 |
{\out exp = "0" => "0" (9)} |
505 |
{\out exp = exp[0] "+" exp[1] => "+" (0)} |
|
506 |
{\out exp = exp[3] "*" exp[2] => "*" (2)} |
|
507 |
{\out exp = "-" exp[3] => "-" (3)} |
|
508 |
\end{ttbox} |
|
509 |
||
3108 | 510 |
Note that because {\tt exp} is not of class {\tt logic}, it has been |
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3318
diff
changeset
|
511 |
retained as a separate nonterminal. This also entails that the syntax |
3108 | 512 |
does not provide for identifiers or paranthesized expressions. |
513 |
Normally you would also want to add the declaration {\tt arities |
|
514 |
exp::logic} after {\tt types} and use {\tt consts} instead of {\tt |
|
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3318
diff
changeset
|
515 |
syntax}. Try this as an exercise and study the changes in the |
867 | 516 |
grammar. |
320 | 517 |
|
518 |
\subsection{The mixfix template} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
519 |
Let us now take a closer look at the string $template$ appearing in mixfix |
320 | 520 |
annotations. This string specifies a list of parsing and printing |
521 |
directives: delimiters\index{delimiters}, arguments, spaces, blocks of |
|
522 |
indentation and line breaks. These are encoded by the following character |
|
523 |
sequences: |
|
524 |
\index{pretty printing|(} |
|
525 |
\begin{description} |
|
526 |
\item[~$d$~] is a delimiter, namely a non-empty sequence of characters |
|
527 |
other than the special characters {\tt _}, {\tt(}, {\tt)} and~{\tt/}. |
|
528 |
Even these characters may appear if escaped; this means preceding it with |
|
529 |
a~{\tt '} (single quote). Thus you have to write {\tt ''} if you really |
|
911
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
885
diff
changeset
|
530 |
want a single quote. Furthermore, a~{\tt '} followed by a space separates |
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
885
diff
changeset
|
531 |
delimiters without extra white space being added for printing. |
320 | 532 |
|
533 |
\item[~{\tt_}~] is an argument position, which stands for a nonterminal symbol |
|
534 |
or name token. |
|
535 |
||
536 |
\item[~$s$~] is a non-empty sequence of spaces for printing. This and the |
|
537 |
following specifications do not affect parsing at all. |
|
538 |
||
539 |
\item[~{\tt(}$n$~] opens a pretty printing block. The optional number $n$ |
|
540 |
specifies how much indentation to add when a line break occurs within the |
|
541 |
block. If {\tt(} is not followed by digits, the indentation defaults |
|
542 |
to~0. |
|
543 |
||
544 |
\item[~{\tt)}~] closes a pretty printing block. |
|
545 |
||
546 |
\item[~{\tt//}~] forces a line break. |
|
547 |
||
548 |
\item[~{\tt/}$s$~] allows a line break. Here $s$ stands for the string of |
|
549 |
spaces (zero or more) right after the {\tt /} character. These spaces |
|
550 |
are printed if the break is not taken. |
|
551 |
\end{description} |
|
552 |
For example, the template {\tt"(_ +/ _)"} specifies an infix operator. |
|
553 |
There are two argument positions; the delimiter~{\tt+} is preceded by a |
|
554 |
space and followed by a space or line break; the entire phrase is a pretty |
|
555 |
printing block. Other examples appear in Fig.\ts\ref{fig:set_trans} below. |
|
556 |
Isabelle's pretty printer resembles the one described in |
|
6592 | 557 |
Paulson~\cite{paulson-ml2}. |
320 | 558 |
|
559 |
\index{pretty printing|)} |
|
560 |
||
561 |
||
562 |
\subsection{Infixes} |
|
563 |
\indexbold{infixes} |
|
564 |
||
3108 | 565 |
Infix operators associating to the left or right can be declared using |
566 |
{\tt infixl} or {\tt infixr}. Basically, the form {\tt $c$ ::\ |
|
567 |
$\sigma$ (infixl $p$)} abbreviates the mixfix declarations |
|
320 | 568 |
\begin{ttbox} |
1387 | 569 |
"op \(c\)" :: \(\sigma\) ("(_ \(c\)/ _)" [\(p\), \(p+1\)] \(p\)) |
570 |
"op \(c\)" :: \(\sigma\) ("op \(c\)") |
|
320 | 571 |
\end{ttbox} |
1387 | 572 |
and {\tt $c$ ::\ $\sigma$ (infixr $p$)} abbreviates the mixfix declarations |
320 | 573 |
\begin{ttbox} |
1387 | 574 |
"op \(c\)" :: \(\sigma\) ("(_ \(c\)/ _)" [\(p+1\), \(p\)] \(p\)) |
575 |
"op \(c\)" :: \(\sigma\) ("op \(c\)") |
|
320 | 576 |
\end{ttbox} |
577 |
The infix operator is declared as a constant with the prefix {\tt op}. |
|
578 |
Thus, prefixing infixes with \sdx{op} makes them behave like ordinary |
|
579 |
function symbols, as in \ML. Special characters occurring in~$c$ must be |
|
580 |
escaped, as in delimiters, using a single quote. |
|
581 |
||
3108 | 582 |
A slightly more general form of infix declarations allows constant |
583 |
names to be independent from their concrete syntax, namely \texttt{$c$ |
|
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3318
diff
changeset
|
584 |
::\ $\sigma$\ (infixl "$sy$" $p$)}, the same for \texttt{infixr}. As |
3108 | 585 |
an example consider: |
586 |
\begin{ttbox} |
|
587 |
and :: [bool, bool] => bool (infixr "&" 35) |
|
588 |
\end{ttbox} |
|
589 |
The internal constant name will then be just \texttt{and}, without any |
|
590 |
\texttt{op} prefixed. |
|
591 |
||
320 | 592 |
|
593 |
\subsection{Binders} |
|
594 |
\indexbold{binders} |
|
595 |
\begingroup |
|
596 |
\def\Q{{\cal Q}} |
|
597 |
A {\bf binder} is a variable-binding construct such as a quantifier. The |
|
598 |
constant declaration |
|
599 |
\begin{ttbox} |
|
1387 | 600 |
\(c\) :: \(\sigma\) (binder "\(\Q\)" [\(pb\)] \(p\)) |
320 | 601 |
\end{ttbox} |
602 |
introduces a constant~$c$ of type~$\sigma$, which must have the form |
|
603 |
$(\tau@1 \To \tau@2) \To \tau@3$. Its concrete syntax is $\Q~x.P$, where |
|
604 |
$x$ is a bound variable of type~$\tau@1$, the body~$P$ has type $\tau@2$ |
|
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3318
diff
changeset
|
605 |
and the whole term has type~$\tau@3$. The optional integer $pb$ |
1060
a122584b5cc5
In binders, the default body priority is now p instead of 0.
lcp
parents:
911
diff
changeset
|
606 |
specifies the body's priority, by default~$p$. Special characters |
877 | 607 |
in $\Q$ must be escaped using a single quote. |
320 | 608 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
609 |
The declaration is expanded internally to something like |
320 | 610 |
\begin{ttbox} |
3098 | 611 |
\(c\)\hskip3pt :: (\(\tau@1\) => \(\tau@2\)) => \(\tau@3\) |
612 |
"\(\Q\)" :: [idts, \(\tau@2\)] => \(\tau@3\) ("(3\(\Q\)_./ _)" [0, \(pb\)] \(p\)) |
|
320 | 613 |
\end{ttbox} |
614 |
Here \ndx{idts} is the nonterminal symbol for a list of identifiers with |
|
332 | 615 |
\index{type constraints} |
320 | 616 |
optional type constraints (see Fig.\ts\ref{fig:pure_gram}). The |
617 |
declaration also installs a parse translation\index{translations!parse} |
|
618 |
for~$\Q$ and a print translation\index{translations!print} for~$c$ to |
|
619 |
translate between the internal and external forms. |
|
620 |
||
621 |
A binder of type $(\sigma \To \tau) \To \tau$ can be nested by giving a |
|
622 |
list of variables. The external form $\Q~x@1~x@2 \ldots x@n. P$ |
|
623 |
corresponds to the internal form |
|
624 |
\[ c(\lambda x@1. c(\lambda x@2. \ldots c(\lambda x@n. P) \ldots)). \] |
|
625 |
||
626 |
\medskip |
|
627 |
For example, let us declare the quantifier~$\forall$:\index{quantifiers} |
|
628 |
\begin{ttbox} |
|
1387 | 629 |
All :: ('a => o) => o (binder "ALL " 10) |
320 | 630 |
\end{ttbox} |
631 |
This lets us write $\forall x.P$ as either {\tt All(\%$x$.$P$)} or {\tt ALL |
|
632 |
$x$.$P$}. When printing, Isabelle prefers the latter form, but must fall |
|
633 |
back on ${\tt All}(P)$ if $P$ is not an abstraction. Both $P$ and {\tt ALL |
|
634 |
$x$.$P$} have type~$o$, the type of formulae, while the bound variable |
|
635 |
can be polymorphic. |
|
636 |
\endgroup |
|
637 |
||
638 |
\index{mixfix declarations|)} |
|
639 |
||
3108 | 640 |
|
641 |
\section{*Alternative print modes} \label{sec:prmodes} |
|
642 |
\index{print modes|(} |
|
643 |
% |
|
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3318
diff
changeset
|
644 |
Isabelle's pretty printer supports alternative output syntaxes. These |
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3318
diff
changeset
|
645 |
may be used independently or in cooperation. The currently active |
3108 | 646 |
print modes (with precedence from left to right) are determined by a |
647 |
reference variable. |
|
648 |
\begin{ttbox}\index{*print_mode} |
|
649 |
print_mode: string list ref |
|
650 |
\end{ttbox} |
|
651 |
Initially this may already contain some print mode identifiers, |
|
652 |
depending on how Isabelle has been invoked (e.g.\ by some user |
|
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3318
diff
changeset
|
653 |
interface). So changes should be incremental --- adding or deleting |
3108 | 654 |
modes relative to the current value. |
655 |
||
12465 | 656 |
Any \ML{} string is a legal print mode identifier, without any predeclaration |
657 |
required. The following names should be considered reserved, though: |
|
658 |
\texttt{""} (the empty string), \texttt{symbols}, \texttt{xsymbols}, and |
|
659 |
\texttt{latex}. |
|
3108 | 660 |
|
661 |
There is a separate table of mixfix productions for pretty printing |
|
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3318
diff
changeset
|
662 |
associated with each print mode. The currently active ones are |
3108 | 663 |
conceptually just concatenated from left to right, with the standard |
664 |
syntax output table always coming last as default. Thus mixfix |
|
665 |
productions of preceding modes in the list may override those of later |
|
666 |
ones. Also note that token translations are always relative to some |
|
667 |
print mode (see \S\ref{sec:tok_tr}). |
|
668 |
||
669 |
\medskip The canonical application of print modes is optional printing |
|
670 |
of mathematical symbols from a special screen font instead of {\sc |
|
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3318
diff
changeset
|
671 |
ascii}. Another example is to re-use Isabelle's advanced |
3108 | 672 |
$\lambda$-term printing mechanisms to generate completely different |
3228 | 673 |
output, say for interfacing external tools like \rmindex{model |
674 |
checkers} (see also \texttt{HOL/Modelcheck}). |
|
3108 | 675 |
|
676 |
\index{print modes|)} |
|
677 |
||
678 |
||
711
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
679 |
\section{Ambiguity of parsed expressions} \label{sec:ambiguity} |
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
680 |
\index{ambiguity!of parsed expressions} |
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
681 |
|
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
682 |
To keep the grammar small and allow common productions to be shared |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
683 |
all logical types (except {\tt prop}) are internally represented |
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3318
diff
changeset
|
684 |
by one nonterminal, namely {\tt logic}. This and omitted or too freely |
711
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
685 |
chosen priorities may lead to ways of parsing an expression that were |
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3318
diff
changeset
|
686 |
not intended by the theory's maker. In most cases Isabelle is able to |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
687 |
select one of multiple parse trees that an expression has lead |
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3318
diff
changeset
|
688 |
to by checking which of them can be typed correctly. But this may not |
711
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
689 |
work in every case and always slows down parsing. |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
690 |
The warning and error messages that can be produced during this process are |
711
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
691 |
as follows: |
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
692 |
|
880 | 693 |
If an ambiguity can be resolved by type inference the following |
694 |
warning is shown to remind the user that parsing is (unnecessarily) |
|
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3318
diff
changeset
|
695 |
slowed down. In cases where it's not easily possible to eliminate the |
880 | 696 |
ambiguity the frequency of the warning can be controlled by changing |
883
92abd2ad9d08
renamed Sign.ambiguity_level to Syntax.ambiguity_level
clasohm
parents:
880
diff
changeset
|
697 |
the value of {\tt Syntax.ambiguity_level} which has type {\tt int |
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3318
diff
changeset
|
698 |
ref}. Its default value is 1 and by increasing it one can control how |
883
92abd2ad9d08
renamed Sign.ambiguity_level to Syntax.ambiguity_level
clasohm
parents:
880
diff
changeset
|
699 |
many parse trees are necessary to generate the warning. |
711
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
700 |
|
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
701 |
\begin{ttbox} |
3801 | 702 |
{\out Ambiguous input "\dots"} |
711
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
703 |
{\out produces the following parse trees:} |
3801 | 704 |
{\out \dots} |
711
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
705 |
{\out Fortunately, only one parse tree is type correct.} |
3801 | 706 |
{\out You may still want to disambiguate your grammar or your input.} |
711
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
707 |
\end{ttbox} |
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
708 |
|
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
709 |
The following message is normally caused by using the same |
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
710 |
syntax in two different productions: |
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
711 |
|
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
712 |
\begin{ttbox} |
3802 | 713 |
{\out Ambiguous input "..."} |
711
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
714 |
{\out produces the following parse trees:} |
3802 | 715 |
{\out \dots} |
716 |
{\out More than one term is type correct:} |
|
717 |
{\out \dots} |
|
711
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
718 |
\end{ttbox} |
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
719 |
|
866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
864
diff
changeset
|
720 |
Ambiguities occuring in syntax translation rules cannot be resolved by |
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
864
diff
changeset
|
721 |
type inference because it is not necessary for these rules to be type |
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3318
diff
changeset
|
722 |
correct. Therefore Isabelle always generates an error message and the |
866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
864
diff
changeset
|
723 |
ambiguity should be eliminated by changing the grammar or the rule. |
711
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
724 |
|
320 | 725 |
|
726 |
\section{Example: some minimal logics} \label{sec:min_logics} |
|
727 |
\index{examples!of logic definitions} |
|
728 |
||
729 |
This section presents some examples that have a simple syntax. They |
|
730 |
demonstrate how to define new object-logics from scratch. |
|
731 |
||
711
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset
|
732 |
First we must define how an object-logic syntax is embedded into the |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
733 |
meta-logic. Since all theorems must conform to the syntax for~\ndx{prop} |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
734 |
(see Fig.\ts\ref{fig:pure_gram}), that syntax has to be extended with the |
320 | 735 |
object-level syntax. Assume that the syntax of your object-logic defines a |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
736 |
meta-type~\tydx{o} of formulae which refers to the nonterminal {\tt logic}. |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
737 |
These formulae can now appear in axioms and theorems wherever \ndx{prop} does |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
738 |
if you add the production |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
739 |
\[ prop ~=~ logic. \] |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
740 |
This is not supposed to be a copy production but an implicit coercion from |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset
|
741 |
formulae to propositions: |
320 | 742 |
\begin{ttbox} |
743 |
Base = Pure + |
|
744 |
types |
|
745 |
o |
|
746 |
arities |
|
747 |
o :: logic |
|
748 |
consts |
|
1387 | 749 |
Trueprop :: o => prop ("_" 5) |
320 | 750 |
end |
751 |
\end{ttbox} |
|
752 |
The constant \cdx{Trueprop} (the name is arbitrary) acts as an invisible |
|
332 | 753 |
coercion function. Assuming this definition resides in a file {\tt Base.thy}, |
320 | 754 |
you have to load it with the command {\tt use_thy "Base"}. |
755 |
||
756 |
One of the simplest nontrivial logics is {\bf minimal logic} of |
|
757 |
implication. Its definition in Isabelle needs no advanced features but |
|
758 |
illustrates the overall mechanism nicely: |
|
759 |
\begin{ttbox} |
|
760 |
Hilbert = Base + |
|
761 |
consts |
|
1387 | 762 |
"-->" :: [o, o] => o (infixr 10) |
320 | 763 |
rules |
764 |
K "P --> Q --> P" |
|
765 |
S "(P --> Q --> R) --> (P --> Q) --> P --> R" |
|
766 |
MP "[| P --> Q; P |] ==> Q" |
|
767 |
end |
|
768 |
\end{ttbox} |
|
332 | 769 |
After loading this definition from the file {\tt Hilbert.thy}, you can |
320 | 770 |
start to prove theorems in the logic: |
771 |
\begin{ttbox} |
|
5205 | 772 |
Goal "P --> P"; |
320 | 773 |
{\out Level 0} |
774 |
{\out P --> P} |
|
775 |
{\out 1. P --> P} |
|
776 |
\ttbreak |
|
777 |
by (resolve_tac [Hilbert.MP] 1); |
|
778 |
{\out Level 1} |
|
779 |
{\out P --> P} |
|
780 |
{\out 1. ?P --> P --> P} |
|
781 |
{\out 2. ?P} |
|
782 |
\ttbreak |
|
783 |
by (resolve_tac [Hilbert.MP] 1); |
|
784 |
{\out Level 2} |
|
785 |
{\out P --> P} |
|
786 |
{\out 1. ?P1 --> ?P --> P --> P} |
|
787 |
{\out 2. ?P1} |
|
788 |
{\out 3. ?P} |
|
789 |
\ttbreak |
|
790 |
by (resolve_tac [Hilbert.S] 1); |
|
791 |
{\out Level 3} |
|
792 |
{\out P --> P} |
|
793 |
{\out 1. P --> ?Q2 --> P} |
|
794 |
{\out 2. P --> ?Q2} |
|
795 |
\ttbreak |
|
796 |
by (resolve_tac [Hilbert.K] 1); |
|
797 |
{\out Level 4} |
|
798 |
{\out P --> P} |
|
799 |
{\out 1. P --> ?Q2} |
|
800 |
\ttbreak |
|
801 |
by (resolve_tac [Hilbert.K] 1); |
|
802 |
{\out Level 5} |
|
803 |
{\out P --> P} |
|
804 |
{\out No subgoals!} |
|
805 |
\end{ttbox} |
|
806 |
As we can see, this Hilbert-style formulation of minimal logic is easy to |
|
807 |
define but difficult to use. The following natural deduction formulation is |
|
808 |
better: |
|
809 |
\begin{ttbox} |
|
810 |
MinI = Base + |
|
811 |
consts |
|
1387 | 812 |
"-->" :: [o, o] => o (infixr 10) |
320 | 813 |
rules |
814 |
impI "(P ==> Q) ==> P --> Q" |
|
815 |
impE "[| P --> Q; P |] ==> Q" |
|
816 |
end |
|
817 |
\end{ttbox} |
|
818 |
Note, however, that although the two systems are equivalent, this fact |
|
819 |
cannot be proved within Isabelle. Axioms {\tt S} and {\tt K} can be |
|
820 |
derived in {\tt MinI} (exercise!), but {\tt impI} cannot be derived in {\tt |
|
821 |
Hilbert}. The reason is that {\tt impI} is only an {\bf admissible} rule |
|
822 |
in {\tt Hilbert}, something that can only be shown by induction over all |
|
823 |
possible proofs in {\tt Hilbert}. |
|
824 |
||
825 |
We may easily extend minimal logic with falsity: |
|
826 |
\begin{ttbox} |
|
827 |
MinIF = MinI + |
|
828 |
consts |
|
1387 | 829 |
False :: o |
320 | 830 |
rules |
831 |
FalseE "False ==> P" |
|
832 |
end |
|
833 |
\end{ttbox} |
|
834 |
On the other hand, we may wish to introduce conjunction only: |
|
835 |
\begin{ttbox} |
|
836 |
MinC = Base + |
|
837 |
consts |
|
1387 | 838 |
"&" :: [o, o] => o (infixr 30) |
320 | 839 |
\ttbreak |
840 |
rules |
|
841 |
conjI "[| P; Q |] ==> P & Q" |
|
842 |
conjE1 "P & Q ==> P" |
|
843 |
conjE2 "P & Q ==> Q" |
|
844 |
end |
|
845 |
\end{ttbox} |
|
846 |
And if we want to have all three connectives together, we create and load a |
|
3108 | 847 |
theory file consisting of a single line: |
320 | 848 |
\begin{ttbox} |
849 |
MinIFC = MinIF + MinC |
|
850 |
\end{ttbox} |
|
851 |
Now we can prove mixed theorems like |
|
852 |
\begin{ttbox} |
|
5205 | 853 |
Goal "P & False --> Q"; |
320 | 854 |
by (resolve_tac [MinI.impI] 1); |
855 |
by (dresolve_tac [MinC.conjE2] 1); |
|
856 |
by (eresolve_tac [MinIF.FalseE] 1); |
|
857 |
\end{ttbox} |
|
858 |
Try this as an exercise! |
|
5371 | 859 |
|
860 |
||
861 |
%%% Local Variables: |
|
862 |
%%% mode: latex |
|
863 |
%%% TeX-master: "ref" |
|
864 |
%%% End: |