285
|
1 |
%% $Id$
|
|
2 |
|
|
3 |
\appendix
|
|
4 |
\newlinechar=-1 %mathsing.sty sets \newlinechar=`\|, which would cause mayhem
|
|
5 |
|
|
6 |
\chapter{Syntax of Isabelle Theories}\label{app:TheorySyntax}
|
325
|
7 |
Chapter~\ref{sec:ref-defining-theories} explains the meanings of these
|
|
8 |
constructs. The syntax obeys the following conventions:
|
285
|
9 |
\begin{itemize}
|
|
10 |
\item {\tt Typewriter font} denotes terminal symbols.
|
|
11 |
\item $id$, $tid$, $nat$, $string$ and $text$ are the lexical classes of
|
|
12 |
identifiers, type identifiers, natural numbers, \ML\ strings (with their
|
|
13 |
quotation marks) and arbitrary \ML\ text. The first three are fully defined
|
325
|
14 |
in
|
|
15 |
\iflabelundefined{Defining-Logics}%
|
|
16 |
{{\it The Isabelle Reference Manual}, chapter `Defining Logics'}%
|
|
17 |
{Chap.\ts\ref{Defining-Logics}}.
|
285
|
18 |
\end{itemize}
|
325
|
19 |
Comments in theories take the form {\tt (*} {\it text\/} {\tt*)}, where
|
|
20 |
{\it text\/} should not contain the character sequence {\tt*)}.
|
285
|
21 |
|
|
22 |
\begin{rail}
|
|
23 |
|
|
24 |
theoryDef : id '=' (name + '+') ('+' extension | ());
|
|
25 |
|
|
26 |
name: id | string;
|
|
27 |
|
295
|
28 |
extension : classes default types arities consts trans rules \\ 'end' ml
|
285
|
29 |
;
|
|
30 |
|
|
31 |
classes : ()
|
|
32 |
| 'classes' ( ( id ( ()
|
|
33 |
| '<' (id + ',')
|
|
34 |
)
|
|
35 |
) + )
|
|
36 |
;
|
|
37 |
|
|
38 |
default : ()
|
|
39 |
| 'default' sort
|
|
40 |
;
|
|
41 |
|
|
42 |
sort : id
|
|
43 |
| '\{' (id * ',') '\}'
|
|
44 |
;
|
|
45 |
|
|
46 |
types : ()
|
325
|
47 |
| 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + )
|
285
|
48 |
;
|
|
49 |
|
325
|
50 |
typeDecl : ( () | tid | '(' ( tid + ',' ) ')') name ( () | '=' string );
|
285
|
51 |
|
|
52 |
infix : ( 'infixr' | 'infixl' ) nat;
|
|
53 |
|
|
54 |
|
|
55 |
arities : ()
|
|
56 |
| 'arities' ((( name + ',' ) '::' arity ) + )
|
|
57 |
;
|
|
58 |
|
|
59 |
arity : ( ()
|
|
60 |
| '(' (sort + ',') ')'
|
|
61 |
) id
|
|
62 |
;
|
|
63 |
|
|
64 |
|
|
65 |
consts : ()
|
|
66 |
| 'consts' ( ( constDecl ( () | ( '(' mixfix ')' ) ) ) + )
|
|
67 |
;
|
|
68 |
|
|
69 |
constDecl : ( name + ',') '::' string ;
|
|
70 |
|
|
71 |
|
|
72 |
mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat )
|
|
73 |
| infix
|
|
74 |
| 'binder' string nat ;
|
|
75 |
|
|
76 |
trans : ()
|
|
77 |
| 'translations' ( pat ( '==' | '=>' | '<=' ) pat + )
|
|
78 |
;
|
|
79 |
|
|
80 |
pat : ( () | ( '(' id ')' ) ) string;
|
|
81 |
|
|
82 |
rules : ()
|
|
83 |
| 'rules' (( id string ) + )
|
|
84 |
;
|
|
85 |
|
|
86 |
ml : ()
|
|
87 |
| 'ML' text
|
|
88 |
;
|
|
89 |
|
|
90 |
\end{rail}
|