1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Integration}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 \isacommand{theory}\isamarkupfalse% |
|
11 \ Integration\isanewline |
|
12 \isakeyword{imports}\ Base\isanewline |
|
13 \isakeyword{begin}% |
|
14 \endisatagtheory |
|
15 {\isafoldtheory}% |
|
16 % |
|
17 \isadelimtheory |
|
18 % |
|
19 \endisadelimtheory |
|
20 % |
|
21 \isamarkupchapter{System integration% |
|
22 } |
|
23 \isamarkuptrue% |
|
24 % |
|
25 \isamarkupsection{Isar toplevel \label{sec:isar-toplevel}% |
|
26 } |
|
27 \isamarkuptrue% |
|
28 % |
|
29 \begin{isamarkuptext}% |
|
30 The Isar toplevel may be considered the centeral hub of the |
|
31 Isabelle/Isar system, where all key components and sub-systems are |
|
32 integrated into a single read-eval-print loop of Isar commands, |
|
33 which also incorporates the underlying ML compiler. |
|
34 |
|
35 Isabelle/Isar departs from the original ``LCF system architecture'' |
|
36 where ML was really The Meta Language for defining theories and |
|
37 conducting proofs. Instead, ML now only serves as the |
|
38 implementation language for the system (and user extensions), while |
|
39 the specific Isar toplevel supports the concepts of theory and proof |
|
40 development natively. This includes the graph structure of theories |
|
41 and the block structure of proofs, support for unlimited undo, |
|
42 facilities for tracing, debugging, timing, profiling etc. |
|
43 |
|
44 \medskip The toplevel maintains an implicit state, which is |
|
45 transformed by a sequence of transitions -- either interactively or |
|
46 in batch-mode. In interactive mode, Isar state transitions are |
|
47 encapsulated as safe transactions, such that both failure and undo |
|
48 are handled conveniently without destroying the underlying draft |
|
49 theory (cf.~\secref{sec:context-theory}). In batch mode, |
|
50 transitions operate in a linear (destructive) fashion, such that |
|
51 error conditions abort the present attempt to construct a theory or |
|
52 proof altogether. |
|
53 |
|
54 The toplevel state is a disjoint sum of empty \isa{toplevel}, or |
|
55 \isa{theory}, or \isa{proof}. On entering the main Isar loop we |
|
56 start with an empty toplevel. A theory is commenced by giving a |
|
57 \isa{{\isaliteral{5C3C5448454F52593E}{\isasymTHEORY}}} header; within a theory we may issue theory |
|
58 commands such as \isa{{\isaliteral{5C3C444546494E4954494F4E3E}{\isasymDEFINITION}}}, or state a \isa{{\isaliteral{5C3C5448454F52454D3E}{\isasymTHEOREM}}} to be proven. Now we are within a proof state, with a |
|
59 rich collection of Isar proof commands for structured proof |
|
60 composition, or unstructured proof scripts. When the proof is |
|
61 concluded we get back to the theory, which is then updated by |
|
62 storing the resulting fact. Further theory declarations or theorem |
|
63 statements with proofs may follow, until we eventually conclude the |
|
64 theory development by issuing \isa{{\isaliteral{5C3C454E443E}{\isasymEND}}}. The resulting theory |
|
65 is then stored within the theory database and we are back to the |
|
66 empty toplevel. |
|
67 |
|
68 In addition to these proper state transformations, there are also |
|
69 some diagnostic commands for peeking at the toplevel state without |
|
70 modifying it (e.g.\ \isakeyword{thm}, \isakeyword{term}, |
|
71 \isakeyword{print-cases}).% |
|
72 \end{isamarkuptext}% |
|
73 \isamarkuptrue% |
|
74 % |
|
75 \isadelimmlref |
|
76 % |
|
77 \endisadelimmlref |
|
78 % |
|
79 \isatagmlref |
|
80 % |
|
81 \begin{isamarkuptext}% |
|
82 \begin{mldecls} |
|
83 \indexdef{}{ML type}{Toplevel.state}\verb|type Toplevel.state| \\ |
|
84 \indexdef{}{ML}{Toplevel.UNDEF}\verb|Toplevel.UNDEF: exn| \\ |
|
85 \indexdef{}{ML}{Toplevel.is\_toplevel}\verb|Toplevel.is_toplevel: Toplevel.state -> bool| \\ |
|
86 \indexdef{}{ML}{Toplevel.theory\_of}\verb|Toplevel.theory_of: Toplevel.state -> theory| \\ |
|
87 \indexdef{}{ML}{Toplevel.proof\_of}\verb|Toplevel.proof_of: Toplevel.state -> Proof.state| \\ |
|
88 \indexdef{}{ML}{Toplevel.debug}\verb|Toplevel.debug: bool Unsynchronized.ref| \\ |
|
89 \indexdef{}{ML}{Toplevel.timing}\verb|Toplevel.timing: bool Unsynchronized.ref| \\ |
|
90 \indexdef{}{ML}{Toplevel.profiling}\verb|Toplevel.profiling: int Unsynchronized.ref| \\ |
|
91 \end{mldecls} |
|
92 |
|
93 \begin{description} |
|
94 |
|
95 \item Type \verb|Toplevel.state| represents Isar toplevel |
|
96 states, which are normally manipulated through the concept of |
|
97 toplevel transitions only (\secref{sec:toplevel-transition}). Also |
|
98 note that a raw toplevel state is subject to the same linearity |
|
99 restrictions as a theory context (cf.~\secref{sec:context-theory}). |
|
100 |
|
101 \item \verb|Toplevel.UNDEF| is raised for undefined toplevel |
|
102 operations. Many operations work only partially for certain cases, |
|
103 since \verb|Toplevel.state| is a sum type. |
|
104 |
|
105 \item \verb|Toplevel.is_toplevel|~\isa{state} checks for an empty |
|
106 toplevel state. |
|
107 |
|
108 \item \verb|Toplevel.theory_of|~\isa{state} selects the |
|
109 background theory of \isa{state}, raises \verb|Toplevel.UNDEF| |
|
110 for an empty toplevel state. |
|
111 |
|
112 \item \verb|Toplevel.proof_of|~\isa{state} selects the Isar proof |
|
113 state if available, otherwise raises \verb|Toplevel.UNDEF|. |
|
114 |
|
115 \item \verb|Toplevel.debug := true| makes the toplevel print further |
|
116 details about internal error conditions, exceptions being raised |
|
117 etc. |
|
118 |
|
119 \item \verb|Toplevel.timing := true| makes the toplevel print timing |
|
120 information for each Isar command being executed. |
|
121 |
|
122 \item \verb|Toplevel.profiling|~\verb|:=|~\isa{n} controls |
|
123 low-level profiling of the underlying ML runtime system. For |
|
124 Poly/ML, \isa{n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}} means time and \isa{n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}} space |
|
125 profiling. |
|
126 |
|
127 \end{description}% |
|
128 \end{isamarkuptext}% |
|
129 \isamarkuptrue% |
|
130 % |
|
131 \endisatagmlref |
|
132 {\isafoldmlref}% |
|
133 % |
|
134 \isadelimmlref |
|
135 % |
|
136 \endisadelimmlref |
|
137 % |
|
138 \isadelimmlantiq |
|
139 % |
|
140 \endisadelimmlantiq |
|
141 % |
|
142 \isatagmlantiq |
|
143 % |
|
144 \begin{isamarkuptext}% |
|
145 \begin{matharray}{rcl} |
|
146 \indexdef{}{ML antiquotation}{Isar.state}\hypertarget{ML antiquotation.Isar.state}{\hyperlink{ML antiquotation.Isar.state}{\mbox{\isa{Isar{\isaliteral{2E}{\isachardot}}state}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
|
147 \end{matharray} |
|
148 |
|
149 \begin{description} |
|
150 |
|
151 \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}Isar{\isaliteral{2E}{\isachardot}}state{\isaliteral{7D}{\isacharbraceright}}} refers to Isar toplevel state at that |
|
152 point --- as abstract value. |
|
153 |
|
154 This only works for diagnostic ML commands, such as \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}}}} or \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}command}}}}. |
|
155 |
|
156 \end{description}% |
|
157 \end{isamarkuptext}% |
|
158 \isamarkuptrue% |
|
159 % |
|
160 \endisatagmlantiq |
|
161 {\isafoldmlantiq}% |
|
162 % |
|
163 \isadelimmlantiq |
|
164 % |
|
165 \endisadelimmlantiq |
|
166 % |
|
167 \isamarkupsubsection{Toplevel transitions \label{sec:toplevel-transition}% |
|
168 } |
|
169 \isamarkuptrue% |
|
170 % |
|
171 \begin{isamarkuptext}% |
|
172 An Isar toplevel transition consists of a partial function on the |
|
173 toplevel state, with additional information for diagnostics and |
|
174 error reporting: there are fields for command name, source position, |
|
175 optional source text, as well as flags for interactive-only commands |
|
176 (which issue a warning in batch-mode), printing of result state, |
|
177 etc. |
|
178 |
|
179 The operational part is represented as the sequential union of a |
|
180 list of partial functions, which are tried in turn until the first |
|
181 one succeeds. This acts like an outer case-expression for various |
|
182 alternative state transitions. For example, \isakeyword{qed} works |
|
183 differently for a local proofs vs.\ the global ending of the main |
|
184 proof. |
|
185 |
|
186 Toplevel transitions are composed via transition transformers. |
|
187 Internally, Isar commands are put together from an empty transition |
|
188 extended by name and source position. It is then left to the |
|
189 individual command parser to turn the given concrete syntax into a |
|
190 suitable transition transformer that adjoins actual operations on a |
|
191 theory or proof state etc.% |
|
192 \end{isamarkuptext}% |
|
193 \isamarkuptrue% |
|
194 % |
|
195 \isadelimmlref |
|
196 % |
|
197 \endisadelimmlref |
|
198 % |
|
199 \isatagmlref |
|
200 % |
|
201 \begin{isamarkuptext}% |
|
202 \begin{mldecls} |
|
203 \indexdef{}{ML}{Toplevel.print}\verb|Toplevel.print: Toplevel.transition -> Toplevel.transition| \\ |
|
204 \indexdef{}{ML}{Toplevel.no\_timing}\verb|Toplevel.no_timing: Toplevel.transition -> Toplevel.transition| \\ |
|
205 \indexdef{}{ML}{Toplevel.keep}\verb|Toplevel.keep: (Toplevel.state -> unit) ->|\isasep\isanewline% |
|
206 \verb| Toplevel.transition -> Toplevel.transition| \\ |
|
207 \indexdef{}{ML}{Toplevel.theory}\verb|Toplevel.theory: (theory -> theory) ->|\isasep\isanewline% |
|
208 \verb| Toplevel.transition -> Toplevel.transition| \\ |
|
209 \indexdef{}{ML}{Toplevel.theory\_to\_proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline% |
|
210 \verb| Toplevel.transition -> Toplevel.transition| \\ |
|
211 \indexdef{}{ML}{Toplevel.proof}\verb|Toplevel.proof: (Proof.state -> Proof.state) ->|\isasep\isanewline% |
|
212 \verb| Toplevel.transition -> Toplevel.transition| \\ |
|
213 \indexdef{}{ML}{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline% |
|
214 \verb| Toplevel.transition -> Toplevel.transition| \\ |
|
215 \indexdef{}{ML}{Toplevel.end\_proof}\verb|Toplevel.end_proof: (bool -> Proof.state -> Proof.context) ->|\isasep\isanewline% |
|
216 \verb| Toplevel.transition -> Toplevel.transition| \\ |
|
217 \end{mldecls} |
|
218 |
|
219 \begin{description} |
|
220 |
|
221 \item \verb|Toplevel.print|~\isa{tr} sets the print flag, which |
|
222 causes the toplevel loop to echo the result state (in interactive |
|
223 mode). |
|
224 |
|
225 \item \verb|Toplevel.no_timing|~\isa{tr} indicates that the |
|
226 transition should never show timing information, e.g.\ because it is |
|
227 a diagnostic command. |
|
228 |
|
229 \item \verb|Toplevel.keep|~\isa{tr} adjoins a diagnostic |
|
230 function. |
|
231 |
|
232 \item \verb|Toplevel.theory|~\isa{tr} adjoins a theory |
|
233 transformer. |
|
234 |
|
235 \item \verb|Toplevel.theory_to_proof|~\isa{tr} adjoins a global |
|
236 goal function, which turns a theory into a proof state. The theory |
|
237 may be changed before entering the proof; the generic Isar goal |
|
238 setup includes an argument that specifies how to apply the proven |
|
239 result to the theory, when the proof is finished. |
|
240 |
|
241 \item \verb|Toplevel.proof|~\isa{tr} adjoins a deterministic |
|
242 proof command, with a singleton result. |
|
243 |
|
244 \item \verb|Toplevel.proofs|~\isa{tr} adjoins a general proof |
|
245 command, with zero or more result states (represented as a lazy |
|
246 list). |
|
247 |
|
248 \item \verb|Toplevel.end_proof|~\isa{tr} adjoins a concluding |
|
249 proof command, that returns the resulting theory, after storing the |
|
250 resulting facts in the context etc. |
|
251 |
|
252 \end{description}% |
|
253 \end{isamarkuptext}% |
|
254 \isamarkuptrue% |
|
255 % |
|
256 \endisatagmlref |
|
257 {\isafoldmlref}% |
|
258 % |
|
259 \isadelimmlref |
|
260 % |
|
261 \endisadelimmlref |
|
262 % |
|
263 \isamarkupsection{Theory database \label{sec:theory-database}% |
|
264 } |
|
265 \isamarkuptrue% |
|
266 % |
|
267 \begin{isamarkuptext}% |
|
268 The theory database maintains a collection of theories, together |
|
269 with some administrative information about their original sources, |
|
270 which are held in an external store (i.e.\ some directory within the |
|
271 regular file system). |
|
272 |
|
273 The theory database is organized as a directed acyclic graph; |
|
274 entries are referenced by theory name. Although some additional |
|
275 interfaces allow to include a directory specification as well, this |
|
276 is only a hint to the underlying theory loader. The internal theory |
|
277 name space is flat! |
|
278 |
|
279 Theory \isa{A} is associated with the main theory file \isa{A}\verb,.thy,, which needs to be accessible through the theory |
|
280 loader path. Any number of additional ML source files may be |
|
281 associated with each theory, by declaring these dependencies in the |
|
282 theory header as \isa{{\isaliteral{5C3C555345533E}{\isasymUSES}}}, and loading them consecutively |
|
283 within the theory context. The system keeps track of incoming ML |
|
284 sources and associates them with the current theory. |
|
285 |
|
286 The basic internal actions of the theory database are \isa{update} and \isa{remove}: |
|
287 |
|
288 \begin{itemize} |
|
289 |
|
290 \item \isa{update\ A} introduces a link of \isa{A} with a |
|
291 \isa{theory} value of the same name; it asserts that the theory |
|
292 sources are now consistent with that value; |
|
293 |
|
294 \item \isa{remove\ A} deletes entry \isa{A} from the theory |
|
295 database. |
|
296 |
|
297 \end{itemize} |
|
298 |
|
299 These actions are propagated to sub- or super-graphs of a theory |
|
300 entry as expected, in order to preserve global consistency of the |
|
301 state of all loaded theories with the sources of the external store. |
|
302 This implies certain causalities between actions: \isa{update} |
|
303 or \isa{remove} of an entry will \isa{remove} all |
|
304 descendants. |
|
305 |
|
306 \medskip There are separate user-level interfaces to operate on the |
|
307 theory database directly or indirectly. The primitive actions then |
|
308 just happen automatically while working with the system. In |
|
309 particular, processing a theory header \isa{{\isaliteral{5C3C5448454F52593E}{\isasymTHEORY}}\ A\ {\isaliteral{5C3C494D504F5254533E}{\isasymIMPORTS}}\ B\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C424547494E3E}{\isasymBEGIN}}} ensures that the |
|
310 sub-graph of the collective imports \isa{B\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E7375623E}{}\isactrlsub n} |
|
311 is up-to-date, too. Earlier theories are reloaded as required, with |
|
312 \isa{update} actions proceeding in topological order according to |
|
313 theory dependencies. There may be also a wave of implied \isa{remove} actions for derived theory nodes until a stable situation |
|
314 is achieved eventually.% |
|
315 \end{isamarkuptext}% |
|
316 \isamarkuptrue% |
|
317 % |
|
318 \isadelimmlref |
|
319 % |
|
320 \endisadelimmlref |
|
321 % |
|
322 \isatagmlref |
|
323 % |
|
324 \begin{isamarkuptext}% |
|
325 \begin{mldecls} |
|
326 \indexdef{}{ML}{use\_thy}\verb|use_thy: string -> unit| \\ |
|
327 \indexdef{}{ML}{use\_thys}\verb|use_thys: string list -> unit| \\ |
|
328 \indexdef{}{ML}{Thy\_Info.get\_theory}\verb|Thy_Info.get_theory: string -> theory| \\ |
|
329 \indexdef{}{ML}{Thy\_Info.remove\_thy}\verb|Thy_Info.remove_thy: string -> unit| \\[1ex] |
|
330 \indexdef{}{ML}{Thy\_Info.register\_thy}\verb|Thy_Info.register_thy: theory -> unit| \\[1ex] |
|
331 \verb|datatype action = Update |\verb,|,\verb| Remove| \\ |
|
332 \indexdef{}{ML}{Thy\_Info.add\_hook}\verb|Thy_Info.add_hook: (Thy_Info.action -> string -> unit) -> unit| \\ |
|
333 \end{mldecls} |
|
334 |
|
335 \begin{description} |
|
336 |
|
337 \item \verb|use_thy|~\isa{A} ensures that theory \isa{A} is fully |
|
338 up-to-date wrt.\ the external file store, reloading outdated |
|
339 ancestors as required. In batch mode, the simultaneous \verb|use_thys| should be used exclusively. |
|
340 |
|
341 \item \verb|use_thys| is similar to \verb|use_thy|, but handles |
|
342 several theories simultaneously. Thus it acts like processing the |
|
343 import header of a theory, without performing the merge of the |
|
344 result. By loading a whole sub-graph of theories like that, the |
|
345 intrinsic parallelism can be exploited by the system, to speedup |
|
346 loading. |
|
347 |
|
348 \item \verb|Thy_Info.get_theory|~\isa{A} retrieves the theory value |
|
349 presently associated with name \isa{A}. Note that the result |
|
350 might be outdated. |
|
351 |
|
352 \item \verb|Thy_Info.remove_thy|~\isa{A} deletes theory \isa{A} and all |
|
353 descendants from the theory database. |
|
354 |
|
355 \item \verb|Thy_Info.register_thy|~\isa{text\ thy} registers an |
|
356 existing theory value with the theory loader database and updates |
|
357 source version information according to the current file-system |
|
358 state. |
|
359 |
|
360 \item \verb|Thy_Info.add_hook|~\isa{f} registers function \isa{f} as a hook for theory database actions. The function will be |
|
361 invoked with the action and theory name being involved; thus derived |
|
362 actions may be performed in associated system components, e.g.\ |
|
363 maintaining the state of an editor for the theory sources. |
|
364 |
|
365 The kind and order of actions occurring in practice depends both on |
|
366 user interactions and the internal process of resolving theory |
|
367 imports. Hooks should not rely on a particular policy here! Any |
|
368 exceptions raised by the hook are ignored. |
|
369 |
|
370 \end{description}% |
|
371 \end{isamarkuptext}% |
|
372 \isamarkuptrue% |
|
373 % |
|
374 \endisatagmlref |
|
375 {\isafoldmlref}% |
|
376 % |
|
377 \isadelimmlref |
|
378 % |
|
379 \endisadelimmlref |
|
380 % |
|
381 \isadelimtheory |
|
382 % |
|
383 \endisadelimtheory |
|
384 % |
|
385 \isatagtheory |
|
386 \isacommand{end}\isamarkupfalse% |
|
387 % |
|
388 \endisatagtheory |
|
389 {\isafoldtheory}% |
|
390 % |
|
391 \isadelimtheory |
|
392 % |
|
393 \endisadelimtheory |
|
394 \isanewline |
|
395 \end{isabellebody}% |
|
396 %%% Local Variables: |
|
397 %%% mode: latex |
|
398 %%% TeX-master: "root" |
|
399 %%% End: |
|