77 \end{figure} |
77 \end{figure} |
78 |
78 |
79 The different parts of a theory definition are interpreted as follows: |
79 The different parts of a theory definition are interpreted as follows: |
80 \begin{description} |
80 \begin{description} |
81 \item[$theoryDef$] A theory has a name $id$ and is an |
81 \item[$theoryDef$] A theory has a name $id$ and is an |
82 extension of the union of theories $id@1$ \dots $id@n$ with new |
82 extension of the union of theories $name@1$ \dots $name@n$ with new |
83 classes, types, constants, syntax and axioms. The basic theory, which |
83 classes, types, constants, syntax and axioms. The basic theory, which |
84 contains only the meta-logic, is called {\tt Pure}. |
84 contains only the meta-logic, is called {\tt Pure}. |
85 |
85 |
86 If $name@i$ is a string the theory $name@i$ is {\em not} used in building |
86 If $name@i$ is a string, then theory $name@i$ is {\em not} used in building |
87 the base of theory $id$. The reason for using strings in $theoryDef$ is that |
87 the base of theory $id$. Strings stand for ML-files rather than |
88 many theories use objects created in a \ML-file that does not belong to a |
88 theory-files and document the dependence if $id$ on additional files. This |
89 theory itself. Because $name@1$ \dots $name@n$ are loaded automatically a |
89 is required because $name@1$ \dots $name@n$ are loaded automatically when |
90 string can be used to specify a file that is needed as a series of |
90 theory $id$ is (re)built. See Chapter~\ref{LoadingTheories} for details. |
91 \ML{}-declarations but not as a parent for theory $id$. See |
|
92 Chapter~\ref{LoadingTheories} for details. |
|
93 \item[$class$] The new class $id$ is declared as a subclass of existing |
91 \item[$class$] The new class $id$ is declared as a subclass of existing |
94 classes $id@1$ \dots $id@n$. This rules out cyclic class structures. |
92 classes $id@1$ \dots $id@n$. This rules out cyclic class structures. |
95 Isabelle automatically computes the transitive closure of subclass |
93 Isabelle automatically computes the transitive closure of subclass |
96 hierarchies. Hence it is not necessary to declare $c@1 < c@3$ in addition |
94 hierarchies. Hence it is not necessary to declare $c@1 < c@3$ in addition |
97 to $c@1 < c@2$ and $c@2 < c@3$. |
95 to $c@1 < c@2$ and $c@2 < c@3$. |
138 \subsection{Reading a new theory} |
136 \subsection{Reading a new theory} |
139 |
137 |
140 \begin{ttbox} |
138 \begin{ttbox} |
141 use_thy: string -> unit |
139 use_thy: string -> unit |
142 \end{ttbox} |
140 \end{ttbox} |
143 |
|
144 Each theory definition must reside in a separate file. Let the file {\it |
141 Each theory definition must reside in a separate file. Let the file {\it |
145 tf}{\tt.thy} contain the definition of a theory called $TF$ with parent |
142 tf}{\tt.thy} contain the definition of a theory called $TF$ with parent |
146 theories $TB@1$ \dots $TB@n$. Calling \ttindexbold{use_thy}~{\tt"}{\it |
143 theories $TB@1$ \dots $TB@n$. Calling \ttindexbold{use_thy}~{\tt"}{\it |
147 TF\/}{\tt"} reads file {\it tf}{\tt.thy}, writes an intermediate {\ML}-file |
144 TF\/}{\tt"} reads file {\it tf}{\tt.thy}, writes an intermediate {\ML}-file |
148 {\tt.}{\it tf}{\tt.thy.ML}, and reads the latter file. Any of the parent |
145 {\tt.}{\it tf}{\tt.thy.ML}, and reads the latter file. Any of the parent |
149 theories that have not been loaded yet are read now by recursive {\tt use_thy} |
146 theories that have not been loaded yet are read now by recursive {\tt |
150 calls until either an already loaded theory or {\tt Pure} is reached. |
147 use_thy} calls until either an already loaded theory or {\tt Pure} is |
151 Therefore one can read a complete logic by just one {\tt use_thy} call if all |
148 reached. Therefore one can read a complete logic by just one {\tt use_thy} |
152 theories are linked appropriatly. Afterwards an {\ML} structure~$TF$ |
149 call if all theories are linked appropriatly. Afterwards an {\ML} |
153 containing a component {\tt thy} for the new theory and components $r@1$ \dots |
150 structure~$TF$ containing a component {\tt thy} for the new theory and |
154 $r@n$ for the rules is declared; it also contains the definitions of the {\tt |
151 components $r@1$ \dots $r@n$ for the rules is declared; it also contains the |
155 ML} section if any. (Normally {\tt.}{\it tf}{\tt.thy.ML} is deleted now if |
152 definitions of the {\tt ML} section if any. Unless |
156 there have occured no errors. In case one wants to have a look at it, |
153 \ttindexbold{delete_tmpfiles} is set to {\tt false}, {\tt.}{\it |
157 {\tt delete_tmpfiles := false} can be set before calling {\tt use_thy}.) |
154 tf}{\tt.thy.ML} is deleted if no errors occured. Finally the file {\it |
158 Finally the file {\it tf}{\tt.ML} is read, if it exists; this file normally |
155 tf}{\tt.ML} is read, if it exists; this file normally contains proofs |
159 contains proofs involving the new theory. |
156 involving the new theory. |
160 |
157 |
161 |
158 |
162 \subsection{Filenames and paths} |
159 \subsection{Filenames and paths} |
163 |
160 |
164 The files the theory definition resides in must have the lower case name of |
161 The files the theory definition resides in must have the lower case name of |
165 the theory with ".thy" or ".ML" appended. On the other hand {\tt use_thy}'s |
162 the theory with ".thy" or ".ML" appended. On the other hand {\tt use_thy}'s |
166 parameter has to be the exact theory name. Optionally the name can be |
163 parameter has to be the exact theory name. Optionally the name can be |
167 preceeded by a path to specify the directory where the files can be found. If |
164 preceeded by a path to specify the directory where the files can be found. If |
168 no path is provided the reference variable {\tt loadpath} is used which |
165 no path is provided the reference variable {\tt loadpath} is used which |
169 contains a list of paths that are searched in the given order. After the |
166 contains a list of paths that are searched in the given order. After the |
170 ".thy"-file for a theory has been found the same path is used to locate the |
167 ".thy"-file for a theory has been found, the same path is used to locate the |
171 (optional) ".ML"-file. (You might note that it is also possible to only |
168 (optional) ".ML"-file. (You might note that it is also possible to only |
172 provide a ".ML"- but no ".thy"-file. In this case a \ML{} structure with the |
169 provide a ".ML"- but no ".thy"-file. In this case an \ML{} structure with the |
173 theory's name has to be created in the ".ML" file. If both the ".thy"-file |
170 theory's name has to be created in the ".ML" file. If both the ".thy"-file |
174 and a structure declaration in the ".ML"-file exist the declaration in the |
171 and a structure declaration in the ".ML"-file exist the declaration in the |
175 latter file is used. See {\tt ZF/ex/llist.ML} for an example.) |
172 latter file is used. See {\tt ZF/ex/llist.ML} for an example.) |
176 |
173 |
177 |
174 |
178 \subsection{Reloading a theory} |
175 \subsection{Reloading a theory} |
179 |
176 |
180 {\tt use_thy} keeps track of all loaded theories and stores information about |
177 {\tt use_thy} keeps track of all loaded theories and stores information about |
181 their files. If it finds that the theory to be loaded was already read before |
178 their files. If it finds that the theory to be loaded was already read |
182 the following happens: First the theory's files are searched at the place |
179 before, the following happens: First the theory's files are searched at the |
183 they were located at the last time they were read. If they are found their |
180 place they were located the last time they were read. If they are found, |
184 time of last modification is compared to the internal data and {\tt use_thy} |
181 their time of last modification is compared to the internal data and {\tt |
185 stops if they are equal. In case the files have been moved, {\tt use_thy} |
182 use_thy} stops if they are equal. In case the files have been moved, {\tt |
186 searches them the same way as a new theory would be searched for. After all |
183 use_thy} searches them the same way a new theory would be searched for. |
187 these tests have been passed the theory is reloaded and all theories that |
184 After all these tests have been passed, the theory is reloaded and all |
188 depend on it (i.e. that have its name in their $theoryDef$) are marked as |
185 theories that depend on it (i.e. that have its name in their $theoryDef$) are |
189 out-of-date. |
186 marked as out-of-date. |
190 |
187 |
191 As changing a theory often makes it necessary to reload all theories that |
188 As changing a theory often makes it necessary to reload all theories that |
192 (indirectly) depend on it, {\tt update} should be used instead of {\tt |
189 (indirectly) depend on it, {\tt update} should be used instead of {\tt |
193 use_thy} to read a modified theory. This function reloads all changed |
190 use_thy} to read a modified theory. This function reloads all changed |
194 theories and their descendants in the correct order. |
191 theories and their descendants in the correct order. |
206 \begin{center} \tt |
203 \begin{center} \tt |
207 Attempt to merge different versions of theory: $T$ |
204 Attempt to merge different versions of theory: $T$ |
208 \end{center} |
205 \end{center} |
209 |
206 |
210 Therefore there is a way to link theories and the $orphaned$ \ML-files. The |
207 Therefore there is a way to link theories and the $orphaned$ \ML-files. The |
211 link from a theory to a \ML-file has been mentioned in |
208 link from a theory to an \ML-file has been mentioned in |
212 Chapter~\ref{DefiningTheories} (strings in $theoryDef$). But to make this |
209 Chapter~\ref{DefiningTheories} (strings in $theoryDef$). But to make this |
213 work and to establish a link in the opposite direction we need to create a |
210 work and to establish a link in the opposite direction we need to create a |
214 {\it pseudo theory}. Let's assume we have a \ML-file named {\tt orphan.ML} that |
211 {\it pseudo theory}. Let's assume we have an \ML-file named {\tt orphan.ML} |
215 depends on theory $A$ and itself is used in theory $B$. To link the three we |
212 that depends on theory $A$ and is itself used in theory $B$. To link the |
216 have to create the file {\tt orphan.thy} containing the line |
213 three we have to create the file {\tt orphan.thy} containing the line |
217 \begin{ttbox} |
214 \begin{ttbox} |
218 orphan = A |
215 orphan = A |
219 \end{ttbox} |
216 \end{ttbox} |
220 and add {\tt "orphan"} to theory $B$'s $theoryDef$. Creating {\tt orphan.thy} |
217 and add {\tt "orphan"} to the list of $B$'s parents. Creating {\tt |
221 is necessary because of two reasons: First it enables automatic loading of |
218 orphan.thy} is necessary because of two reasons: First it enables automatic |
222 $orphan$'s parents and second it creates the \ML{}-object {\tt orphan} that |
219 loading of $orphan$'s parents and second it creates the \ML{}-object {\tt |
223 is needed by {\tt use_thy} (though it is not added to the base of theory $B$). |
220 orphan} that is needed by {\tt use_thy} (though it is not added to the base |
224 If {\tt orphan.ML} depended on no theory then {\tt Pure} would have been used |
221 of theory $B$). If {\tt orphan.ML} depended on no theory then {\tt Pure} |
225 instead of {\tt A}. |
222 would have been used instead of {\tt A}. |
226 |
223 |
227 For an extensive example of how this technique can be used to link over 30 |
224 For an extensive example of how this technique can be used to link over 30 |
228 files and read them by just two {\tt use_thy} calls have a look at the ZF logic. |
225 files and read them by just two {\tt use_thy} calls have a look at the ZF |
|
226 logic. |
229 |
227 |
230 |
228 |
231 \subsection{Removing a theory} |
229 \subsection{Removing a theory} |
232 |
230 |
233 If a previously read file is removed the {\tt update} function will keep |
231 If a previously read file is removed the {\tt update} function will keep |