25 |
25 |
26 \section{Defining Theories} |
26 \section{Defining Theories} |
27 \label{DefiningTheories} |
27 \label{DefiningTheories} |
28 |
28 |
29 Theories can be defined either using concrete syntax or by calling certain |
29 Theories can be defined either using concrete syntax or by calling certain |
30 \ML-functions (see \S\ref{BuildingATheory}). Figure~\ref{TheorySyntax} |
30 \ML-functions (see \S\ref{BuildingATheory}). Appendix~\ref{TheorySyntax} |
31 presents the concrete syntax for theories. This grammar employs the |
31 presents the concrete syntax for theories. |
|
32 This grammar employs the |
32 following conventions: |
33 following conventions: |
33 \begin{itemize} |
34 \begin{itemize} |
34 \item Identifiers such as $theoryDef$ denote nonterminal symbols. |
35 \item Identifiers such as {\it theoryDef} denote nonterminal symbols. |
35 \item Text in {\tt typewriter font} denotes terminal symbols. |
36 \item Text in {\tt typewriter font} denotes terminal symbols. |
36 \item \ldots{} indicates repetition of a phrase. |
37 \item $id$ is an Isabelle identifier. |
37 \item A vertical bar~($|$) separates alternative phrases. |
38 \item $string$ is an ML string, with its quotation marks. |
38 \item Square [brackets] enclose optional phrases. |
39 \item $nat$ is for a natural number. |
39 \item $id$ stands for an Isabelle identifier. |
40 \item $tfree$ is an Isabelle type variable, i.e.\ an identifier starting with |
40 \item $string$ stands for an ML string, with its quotation marks. |
41 a prime. |
41 \item $k$ stands for a natural number. |
|
42 \item $text$ stands for arbitrary ML text. |
42 \item $text$ stands for arbitrary ML text. |
43 \end{itemize} |
43 \end{itemize} |
44 |
|
45 \begin{figure}[hp] |
|
46 \begin{center} |
|
47 \begin{tabular}{rclc} |
|
48 $theoryDef$ &=& $id$ {\tt=} $name@1$ {\tt+} \dots {\tt+} $name@n$ |
|
49 [{\tt+} $extension$]\\\\ |
|
50 $extension$ &=& [$classes$] [$default$] [$types$] [$arities$] [$consts$] |
|
51 [$trans$] [$rules$] {\tt end} [$ml$]\\\\ |
|
52 $classes$ &=& \ttindex{classes} $class$ \dots $class$ \\\\ |
|
53 $class$ &=& $id$ [{\tt<} $id@1${\tt,} \dots{\tt,} $id@n$] \\\\ |
|
54 $default$ &=& \ttindex{default} $sort$ \\\\ |
|
55 $sort$ &=& $id$ ~~$|$~~ {\tt\{} $id@1${\tt,} \dots{\tt,} $id@n$ {\tt\}} \\\\ |
|
56 $name$ &=& $id$ ~~$|$~~ $string$ \\\\ |
|
57 $types$ &=& \ttindex{types} $typeDecl$ \dots $typeDecl$ \\\\ |
|
58 $typeDecl$ &=& $name${\tt,} \dots{\tt,} $name$ $k$ |
|
59 [{\tt(} $infix$ {\tt)}] \\\\ |
|
60 $infix$ &=& \ttindex{infixl} $k$ ~~$|$~~ \ttindex{infixr} $k$ \\\\ |
|
61 $arities$ &=& \ttindex{arities} $arityDecl$ \dots $arityDecl$ \\\\ |
|
62 $arityDecl$ &=& $name${\tt,} \dots{\tt,} $name$ {\tt::} $arity$ \\\\ |
|
63 $arity$ &=& [{\tt(} $sort${\tt,} \dots{\tt,} $sort$ {\tt)}] $id$ \\\\ |
|
64 $consts$ &=& \ttindex{consts} $constDecl$ \dots $constDecl$ \\\\ |
|
65 $constDecl$ &=& $name@1${\tt,} \dots{\tt,} $name@n$ {\tt::} $string$ |
|
66 [{\tt(} $mixfix$ {\tt)}] \\\\ |
|
67 $mixfix$ &=& $string$ |
|
68 [ [\quad{\tt[} $k@1${\tt,} \dots{\tt,} $k@n$ {\tt]}\quad] $k$]\\ |
|
69 &$|$& $infix$ \\ |
|
70 &$|$& \ttindex{binder} $string$ $k$\\\\ |
|
71 $trans$ &=& \ttindex{translations} $transDecl$ \dots $transDecl$ \\\\ |
|
72 $transDecl$ &=& [ {\tt(}$string${\tt)} ] $string$ |
|
73 [ {\tt=>} $|$ {\tt<=} $|$ {\tt==} ] [ ($string$) ] $string$ \\\\ |
|
74 $rules$ &=& \ttindex{rules} $rule$ \dots $rule$ \\\\ |
|
75 $rule$ &=& $id$ $string$ \\\\ |
|
76 $ml$ &=& \ttindex{ML} $text$ |
|
77 \end{tabular} |
|
78 \end{center} |
|
79 \caption{Theory Syntax} |
|
80 \label{TheorySyntax} |
|
81 \end{figure} |
|
82 |
|
83 The different parts of a theory definition are interpreted as follows: |
44 The different parts of a theory definition are interpreted as follows: |
84 \begin{description} |
45 \begin{description} |
85 \item[$theoryDef$] A theory has a name $id$ and is an |
46 \item[{\it theoryDef}] A theory has a name $id$ and is an extension of the |
86 extension of the union of theories $name@1$ \dots $name@n$ with new |
47 union of theories {\it name}, the {\em parent theories}, with new classes, |
87 classes, types, constants, syntax and axioms. The basic theory, which |
48 types, constants, syntax and axioms. The basic theory, which contains only |
88 contains only the meta-logic, is called {\tt Pure}. |
49 the meta-logic, is called {\tt Pure}. |
89 |
50 |
90 If $name@i$ is a string, then theory $name@i$ is {\em not} used in building |
51 If {\it name} is a string, then theory {\it name} is {\em not} used in |
91 the base of theory $id$. Strings stand for ML-files rather than |
52 building the base of theory $id$. Strings stand for ML-files rather than |
92 theory-files and document the dependence if $id$ on additional files. This |
53 theory-files and document the dependence of $id$ on additional files. This |
93 is required because $name@1$ \dots $name@n$ are loaded automatically when |
54 enables all required files, namely those corresponding to {\it name}s, to |
94 theory $id$ is (re)built. See Chapter~\ref{LoadingTheories} for details. |
55 be loaded automatically when theory $id$ is (re)built. See |
95 \item[$class$] The new class $id$ is declared as a subclass of existing |
56 Chapter~\ref{LoadingTheories} for details. |
96 classes $id@1$ \dots $id@n$. This rules out cyclic class structures. |
57 \item[$classes$] {\tt$id$ < $id@1$ \dots\ $id@n$} declares $id$ as a subclass |
97 Isabelle automatically computes the transitive closure of subclass |
58 of existing classes $id@1\dots id@n$. This rules out cyclic class |
98 hierarchies. Hence it is not necessary to declare $c@1 < c@3$ in addition |
59 structures. Isabelle automatically computes the transitive closure of |
99 to $c@1 < c@2$ and $c@2 < c@3$. |
60 subclass hierarchies. Hence it is not necessary to declare {\tt c < e} in |
|
61 addition to {\tt c < d} and {\tt d < e}. |
100 \item[$default$] introduces $sort$ as the new default sort for type |
62 \item[$default$] introduces $sort$ as the new default sort for type |
101 variables. Unconstrained type variables in an input string are |
63 variables. Unconstrained type variables in an input string are |
102 automatically constrained by $sort$; this does not apply to type variables |
64 automatically constrained by $sort$; this does not apply to type variables |
103 created internally during type inference. If omitted, |
65 created internally during type inference. If omitted, the default sort is |
104 the default sort is the same as in the parent theory. |
66 the union of the default sorts of the parent theories. |
105 \item[$sort$] is a finite set $id@1$ \dots $id@n$ of classes; a single class |
67 \item[$sort$] is a finite set of classes; a single class $id$ abbreviates the |
106 $id$ abbreviates the singleton set {\tt\{}$id${\tt\}}. |
68 singleton set {\tt\{}$id${\tt\}}. |
107 \item[$name$] is either an alphanumeric identifier or an arbitrary string. |
69 \item[$type$] is either the declaration of a new type (constructor) or type |
108 \item[$typeDecl$] Each $name$ is declared as a new type constructor with |
70 synonym $name$. Only binary type constructors can have infix status and |
109 $k$ arguments. Only binary type constructors can have infix status and |
71 symbolic names, e.g.\ {\tt ('a,'b)"+"}. Type constructors of $n$ arguments |
110 symbolic names ($string$). |
72 are declared by {\tt ($\alpha@1$,\dots,$\alpha@n$)$name$}. Type |
|
73 synonyms\indexbold{type!synonym} are defined as in ML, except that the |
|
74 right-hand side must be enclosed in quotation marks. |
111 \item[$infix$] declares a type or constant to be an infix operator of |
75 \item[$infix$] declares a type or constant to be an infix operator of |
112 precedence $k$ associating to the left ({\tt infixl}) or right ({\tt |
76 precedence $nat$ associating to the left ({\tt infixl}) or right ({\tt |
113 infixr}). |
77 infixr}). |
114 \item[$arityDecl$] Each existing type constructor $name@1$ \dots $name@n$ |
78 \item[$arities$] Each $name$ must be an existing type constructor which is |
115 is given the additional arity $arity$. |
79 given the additional arity $arity$. |
116 \item[$constDecl$] The new constants $name@1$ \dots $name@n$ are declared to |
80 \item[$constDecl$] Each new constant $name$ is declared to be of type |
117 be of type $string$. For display purposes they can be annotated with |
81 $string$. For display purposes they can be annotated with $mixfix$ |
118 $mixfix$ declarations. |
82 declarations. |
119 \item[$mixfix$] $string$ is a mixfix template of the form {\tt"}\dots{\tt\_} |
83 \item[$mixfix$] There are three forms of syntactic annotations: |
120 \dots{\tt\_} \dots{\tt"} where the $i$-th underscore indicates the position |
84 \begin{itemize} |
121 where the $i$-th argument should go, $k@i$ is the minimum precedence of |
85 \item A mixfix template given as a $string$ of the form |
122 the $i$-th argument, and $k$ the precedence of the construct. The list |
86 {\tt"}\dots{\tt\_}\dots{\tt\_}\dots{\tt"} where the $i$-th underscore |
123 \hbox{\tt[$k@1$, \dots, $k@n$]} is optional. |
87 indicates the position where the $i$-th argument should go. The minimal |
124 |
88 precedence of each argument is given by a list of natural numbers, the |
125 Binary constants can be given infix status. |
89 precedence of the construct by the following natural number; precedences |
126 |
90 are optional. |
127 A constant $f$ {\tt::} $(\tau@1\To\tau@2)\To\tau@3$ can be given {\em |
91 |
|
92 \item Binary constants can be given infix status. |
|
93 |
|
94 \item A constant $f$ {\tt::} $(\tau@1\To\tau@2)\To\tau@3$ can be given {\em |
128 binder} status: {\tt binder} $Q$ $p$ causes $Q\,x.F(x)$ to be treated |
95 binder} status: {\tt binder} $Q$ $p$ causes $Q\,x.F(x)$ to be treated |
129 like $f(F)$; $p$ is the precedence of the construct. |
96 like $f(F)$; $p$ is the precedence of the construct. |
130 \item[$transDecl$] Specifies a syntactic translation rule, that is a parse |
97 \end{itemize} |
131 rule ({\tt =>}), a print rule ({\tt <=}), or both ({\tt ==}). |
98 \item[$trans$] Specifies syntactic translation rules, that is parse |
|
99 rules ({\tt =>}), print rules ({\tt <=}), or both ({\tt ==}). |
132 \item[$rule$] A rule consists of a name $id$ and a formula $string$. Rule |
100 \item[$rule$] A rule consists of a name $id$ and a formula $string$. Rule |
133 names must be distinct. |
101 names must be distinct. |
134 \item[$ml$] This final part of a theory consists of ML code, |
102 \item[$ml$] This final part of a theory consists of ML code, |
135 typically for parse and print translations. |
103 typically for parse and print translations. |
136 \end{description} |
104 \end{description} |
137 The $mixfix$, $transDecl$ and $ml$ sections are explained in more detail in |
105 The $mixfix$, $trans$ and $ml$ sections are explained in more detail in |
138 the {\it Defining Logics} chapter of the {\it Logics} manual. |
106 the {\it Defining Logics} chapter of the {\it Logics} manual. |
139 |
107 |
140 |
108 |
141 \subsection{Classes and types} |
109 \subsection{Classes and types} |
142 \index{*arities!context conditions} |
110 \index{*arities!context conditions} |
213 \index{reloading a theory} |
183 \index{reloading a theory} |
214 |
184 |
215 \ttindex{use_thy} keeps track of all loaded theories and stores information |
185 \ttindex{use_thy} keeps track of all loaded theories and stores information |
216 about their files. If it finds that the theory to be loaded was already read |
186 about their files. If it finds that the theory to be loaded was already read |
217 before, the following happens: first the theory's files are searched at the |
187 before, the following happens: first the theory's files are searched at the |
218 place they were located the last time they were read. If they are found, their |
188 place they were located the last time they were read. If they are found, |
219 time of last modification is compared to the internal data and {\tt use_thy} |
189 their time of last modification is compared to the internal data and {\tt |
220 stops if they are equal. In case the files have been moved, {\tt use_thy} |
190 use_thy} stops if they are equal. In case the files have been moved, {\tt |
221 searches them the same way a new theory would be searched for. After all these |
191 use_thy} searches them the same way a new theory would be searched for. |
222 tests have been passed, the theory is reloaded and all theories that depend on |
192 After all these tests have been passed, the theory is reloaded and all |
223 it (those that have its name in their $theoryDef$) are marked as out-of-date. |
193 theories that depend on it (those that have its name in their {\it |
224 |
194 theoryDef}) are marked as out-of-date. |
225 As changing a theory often makes it necessary to reload all theories that |
195 \begin{warn} |
226 (indirectly) depend on it, \ttindexbold{update} should be used instead of {\tt |
196 Changing a theory on disk often makes it necessary to reload all theories |
227 use_thy} to read a modified theory. This function reloads all changed |
197 that (indirectly) depend on it. However, {\tt use_thy} reads only one |
228 theories and their descendants in the correct order. |
198 theory, even if some of the parents are out of date. In this case |
|
199 \ttindexbold{update}{\tt()} should be used. This function reloads {\em all} |
|
200 modified theories and their descendants in the correct order. |
|
201 \end{warn} |
229 |
202 |
230 |
203 |
231 \subsection{Pseudo theories} |
204 \subsection{Pseudo theories} |
232 \indexbold{pseudo theories} |
205 \indexbold{pseudo theories} |
233 |
206 |
234 There is a problem with \ttindex{update}: objects created in \ML-files that do |
207 There is a problem with \ttindex{update}: objects created in \ML-files that |
235 not belong to a theory (see explanation of $theoryDef$ in |
208 do not belong to a theory (see explanation of {\it theoryDef} in |
236 \ref{DefiningTheories}). These files are read manually between {\tt use_thy} |
209 \ref{DefiningTheories}). These files are read manually between {\tt use_thy} |
237 calls and define objects used in different theories. As {\tt update} only |
210 calls and define objects used in different theories. As {\tt update} only |
238 knows about the theories there still exist objects with references to the old |
211 knows about the theories there still exist objects with references to the old |
239 theory version after the new one has been read. This (most probably) will |
212 theory version after the new one has been read. This (most probably) will |
240 produce the fatal error |
213 produce the fatal error |