3 \def\isabellecontext{integration}%
13 \isacommand{theory}\isamarkupfalse%
14 \ integration\ \isakeyword{imports}\ base\ \isakeyword{begin}%
22 \isamarkupchapter{System integration%
26 \isamarkupsection{Isar toplevel \label{sec:isar-toplevel}%
30 \begin{isamarkuptext}%
31 The Isar toplevel may be considered the centeral hub of the
32 Isabelle/Isar system, where all key components and sub-systems are
33 integrated into a single read-eval-print loop of Isar commands. We
34 shall even incorporate the existing {\ML} toplevel of the compiler
35 and run-time system (cf.\ \secref{sec:ML-toplevel}).
37 Isabelle/Isar departs from the original ``LCF system architecture''
38 where {\ML} was really The Meta Language for defining theories and
39 conducting proofs. Instead, {\ML} now only serves as the
40 implementation language for the system (and user extensions), while
41 the specific Isar toplevel supports the concepts of theory and proof
42 development natively. This includes the graph structure of theories
43 and the block structure of proofs, support for unlimited undo,
44 facilities for tracing, debugging, timing, profiling etc.
46 \medskip The toplevel maintains an implicit state, which is
47 transformed by a sequence of transitions -- either interactively or
48 in batch-mode. In interactive mode, Isar state transitions are
49 encapsulated as safe transactions, such that both failure and undo
50 are handled conveniently without destroying the underlying draft
51 theory (cf.~\secref{sec:context-theory}). In batch mode,
52 transitions operate in a linear (destructive) fashion, such that
53 error conditions abort the present attempt to construct a theory or
56 The toplevel state is a disjoint sum of empty \isa{toplevel}, or
57 \isa{theory}, or \isa{proof}. On entering the main Isar loop we
58 start with an empty toplevel. A theory is commenced by giving a
59 \isa{{\isasymTHEORY}} header; within a theory we may issue theory
60 commands such as \isa{{\isasymDEFINITION}}, or state a \isa{{\isasymTHEOREM}} to be proven. Now we are within a proof state, with a
61 rich collection of Isar proof commands for structured proof
62 composition, or unstructured proof scripts. When the proof is
63 concluded we get back to the theory, which is then updated by
64 storing the resulting fact. Further theory declarations or theorem
65 statements with proofs may follow, until we eventually conclude the
66 theory development by issuing \isa{{\isasymEND}}. The resulting theory
67 is then stored within the theory database and we are back to the
70 In addition to these proper state transformations, there are also
71 some diagnostic commands for peeking at the toplevel state without
72 modifying it (e.g.\ \isakeyword{thm}, \isakeyword{term},
73 \isakeyword{print-cases}).%
83 \begin{isamarkuptext}%
85 \indexmltype{Toplevel.state}\verb|type Toplevel.state| \\
86 \indexml{Toplevel.UNDEF}\verb|Toplevel.UNDEF: exn| \\
87 \indexml{Toplevel.is-toplevel}\verb|Toplevel.is_toplevel: Toplevel.state -> bool| \\
88 \indexml{Toplevel.theory-of}\verb|Toplevel.theory_of: Toplevel.state -> theory| \\
89 \indexml{Toplevel.proof-of}\verb|Toplevel.proof_of: Toplevel.state -> Proof.state| \\
90 \indexml{Toplevel.debug}\verb|Toplevel.debug: bool ref| \\
91 \indexml{Toplevel.timing}\verb|Toplevel.timing: bool ref| \\
92 \indexml{Toplevel.profiling}\verb|Toplevel.profiling: int ref| \\
97 \item \verb|Toplevel.state| represents Isar toplevel states,
98 which are normally manipulated through the concept of toplevel
99 transitions only (\secref{sec:toplevel-transition}). Also note that
100 a raw toplevel state is subject to the same linearity restrictions
101 as a theory context (cf.~\secref{sec:context-theory}).
103 \item \verb|Toplevel.UNDEF| is raised for undefined toplevel
104 operations. Many operations work only partially for certain cases,
105 since \verb|Toplevel.state| is a sum type.
107 \item \verb|Toplevel.is_toplevel|~\isa{state} checks for an empty
110 \item \verb|Toplevel.theory_of|~\isa{state} selects the theory of
111 a theory or proof (!), otherwise raises \verb|Toplevel.UNDEF|.
113 \item \verb|Toplevel.proof_of|~\isa{state} selects the Isar proof
114 state if available, otherwise raises \verb|Toplevel.UNDEF|.
116 \item \verb|set Toplevel.debug| makes the toplevel print further
117 details about internal error conditions, exceptions being raised
120 \item \verb|set Toplevel.timing| makes the toplevel print timing
121 information for each Isar command being executed.
123 \item \verb|Toplevel.profiling|~\verb|:=|~\isa{n} controls
124 low-level profiling of the underlying {\ML} runtime system. For
125 Poly/ML, \isa{n\ {\isacharequal}\ {\isadigit{1}}} means time and \isa{n\ {\isacharequal}\ {\isadigit{2}}} space
139 \isamarkupsubsection{Toplevel transitions \label{sec:toplevel-transition}%
143 \begin{isamarkuptext}%
144 An Isar toplevel transition consists of a partial function on the
145 toplevel state, with additional information for diagnostics and
146 error reporting: there are fields for command name, source position,
147 optional source text, as well as flags for interactive-only commands
148 (which issue a warning in batch-mode), printing of result state,
151 The operational part is represented as the sequential union of a
152 list of partial functions, which are tried in turn until the first
153 one succeeds (i.e.\ does not raise \verb|Toplevel.UNDEF|). This acts
154 like an outer case-expression for various alternative state
155 transitions. For example, \isakeyword{qed} acts differently for a
156 local proofs vs.\ the global ending of the main proof.
158 Toplevel transitions are composed via transition transformers.
159 Internally, Isar commands are put together from an empty transition
160 extended by name and source position (and optional source text). It
161 is then left to the individual command parser to turn the given
162 concrete syntax into a suitable transition transformer that adjoin
163 actual operations on a theory or proof state etc.%
173 \begin{isamarkuptext}%
175 \indexml{Toplevel.print}\verb|Toplevel.print: Toplevel.transition -> Toplevel.transition| \\
176 \indexml{Toplevel.no-timing}\verb|Toplevel.no_timing: Toplevel.transition -> Toplevel.transition| \\
177 \indexml{Toplevel.keep}\verb|Toplevel.keep: (Toplevel.state -> unit) ->|\isasep\isanewline%
178 \verb| Toplevel.transition -> Toplevel.transition| \\
179 \indexml{Toplevel.theory}\verb|Toplevel.theory: (theory -> theory) ->|\isasep\isanewline%
180 \verb| Toplevel.transition -> Toplevel.transition| \\
181 \indexml{Toplevel.theory-to-proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
182 \verb| Toplevel.transition -> Toplevel.transition| \\
183 \indexml{Toplevel.proof}\verb|Toplevel.proof: (Proof.state -> Proof.state) ->|\isasep\isanewline%
184 \verb| Toplevel.transition -> Toplevel.transition| \\
185 \indexml{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline%
186 \verb| Toplevel.transition -> Toplevel.transition| \\
187 \indexml{Toplevel.proof-to-theory}\verb|Toplevel.proof_to_theory: (Proof.state -> theory) ->|\isasep\isanewline%
188 \verb| Toplevel.transition -> Toplevel.transition| \\
193 \item \verb|Toplevel.print|~\isa{tr} sets the print flag, which
194 causes the toplevel loop to echo the result state (in interactive
197 \item \verb|Toplevel.no_timing|~\isa{tr} indicates that the
198 transition should never show timing information, e.g.\ because it is
199 a diagnostic command.
201 \item \verb|Toplevel.keep|~\isa{tr} adjoins a diagnostic
204 \item \verb|Toplevel.theory|~\isa{tr} adjoins a theory
207 \item \verb|Toplevel.theory_to_proof|~\isa{tr} adjoins a global
208 goal function, which turns a theory into a proof state. The theory
209 may be changed before entering the proof; the generic Isar goal
210 setup includes an argument that specifies how to apply the proven
211 result to the theory, when the proof is finished.
213 \item \verb|Toplevel.proof|~\isa{tr} adjoins a deterministic
214 proof command, with a singleton result.
216 \item \verb|Toplevel.proofs|~\isa{tr} adjoins a general proof
217 command, with zero or more result states (represented as a lazy
220 \item \verb|Toplevel.proof_to_theory|~\isa{tr} adjoins a
221 concluding proof command, that returns the resulting theory, after
222 storing the resulting facts etc.
235 \isamarkupsubsection{Toplevel control%
239 \begin{isamarkuptext}%
240 There are a few special control commands that modify the behavior
241 the toplevel itself, and only make sense in interactive mode. Under
242 normal circumstances, the user encounters these only implicitly as
243 part of the protocol between the Isabelle/Isar system and a
244 user-interface such as ProofGeneral.
248 \item \isacommand{undo} follows the three-level hierarchy of empty
249 toplevel vs.\ theory vs.\ proof: undo within a proof reverts to the
250 previous proof context, undo after a proof reverts to the theory
251 before the initial goal statement, undo of a theory command reverts
252 to the previous theory value, undo of a theory header discontinues
253 the current theory development and removes it from the theory
254 database (\secref{sec:theory-database}).
256 \item \isacommand{kill} aborts the current level of development:
257 kill in a proof context reverts to the theory before the initial
258 goal statement, kill in a theory context aborts the current theory
259 development, removing it from the database.
261 \item \isacommand{exit} drops out of the Isar toplevel into the
262 underlying {\ML} toplevel (\secref{sec:ML-toplevel}). The Isar
263 toplevel state is preserved and may be continued later.
265 \item \isacommand{quit} terminates the Isabelle/Isar process without
272 \isamarkupsection{ML toplevel \label{sec:ML-toplevel}%
276 \begin{isamarkuptext}%
277 The {\ML} toplevel provides a read-compile-eval-print loop for
278 {\ML} values, types, structures, and functors. {\ML} declarations
279 operate on the global system state, which consists of the compiler
280 environment plus the values of {\ML} reference variables. There is
281 no clean way to undo {\ML} declarations, except for reverting to a
282 previously saved state of the whole Isabelle process. {\ML} input
283 is either read interactively from a TTY, or from a string (usually
284 within a theory text), or from a source file (usually loaded from a
287 Whenever the {\ML} toplevel is active, the current Isabelle theory
288 context is passed as an internal reference variable. Thus {\ML}
289 code may access the theory context during compilation, it may even
290 change the value of a theory being under construction --- while
291 observing the usual linearity restrictions
292 (cf.~\secref{sec:context-theory}).%
302 \begin{isamarkuptext}%
304 \indexml{context}\verb|context: theory -> unit| \\
305 \indexml{the-context}\verb|the_context: unit -> theory| \\
306 \indexml{Context.$>$$>$ }\verb|Context.>> : (theory -> theory) -> unit| \\
311 \item \verb|context|~\isa{thy} sets the {\ML} theory context to
312 \isa{thy}. This is usually performed automatically by the system,
313 when dropping out of the interactive Isar toplevel into {\ML}, or
314 when Isar invokes {\ML} to process code from a string or a file.
316 \item \verb|the_context ()| refers to the theory context of the
317 {\ML} toplevel --- at compile time! {\ML} code needs to take care
318 to refer to \verb|the_context ()| correctly. Recall that
319 evaluation of a function body is delayed until actual runtime.
320 Moreover, persistent {\ML} toplevel bindings to an unfinished theory
321 should be avoided: code should either project out the desired
322 information immediately, or produce an explicit \verb|theory_ref| (cf.\ \secref{sec:context-theory}).
324 \item \verb|Context.>>|~\isa{f} applies theory transformation
325 \isa{f} to the current theory of the {\ML} toplevel. In order to
326 work as expected, the theory should be still under construction, and
327 the Isar language element that invoked the {\ML} compiler in the
328 first place should be ready to accept the changed theory value
329 (e.g.\ \isakeyword{ML-setup}, but not plain \isakeyword{ML}).
330 Otherwise the theory becomes stale!
334 It is very important to note that the above functions are really
335 restricted to the compile time, even though the {\ML} compiler is
336 invoked at runtime! The majority of {\ML} code uses explicit
337 functional arguments of a theory or proof context instead. Thus it
338 may be invoked for an arbitrary context later on, without having to
339 worry about any operational details.
344 \indexml{Isar.main}\verb|Isar.main: unit -> unit| \\
345 \indexml{Isar.loop}\verb|Isar.loop: unit -> unit| \\
346 \indexml{Isar.state}\verb|Isar.state: unit -> Toplevel.state| \\
347 \indexml{Isar.context}\verb|Isar.context: unit -> Proof.context| \\
348 \indexml{Isar.exn}\verb|Isar.exn: unit -> (exn * string) option| \\
353 \item \verb|Isar.main ()| invokes the Isar toplevel from {\ML},
354 initializing an empty toplevel state.
356 \item \verb|Isar.loop ()| continues the Isar toplevel with the
357 current state, after having dropped out of the Isar toplevel loop.
359 \item \verb|Isar.state ()| and \verb|Isar.exn ()| get current
360 toplevel state and error condition, respectively. This only works
361 after having dropped out of the Isar toplevel loop.
363 \item \verb|Isar.context ()| produces the proof context from \verb|Isar.state ()|, analogous to \verb|Context.proof_of|
364 (\secref{sec:generic-context}).
377 \isamarkupsection{Theory database \label{sec:theory-database}%
381 \begin{isamarkuptext}%
382 The theory database maintains a collection of theories, together
383 with some administrative information about their original sources,
384 which are held in an external store (i.e.\ some directory within the
385 regular file system).
387 The theory database is organized as a directed acyclic graph;
388 entries are referenced by theory name. Although some additional
389 interfaces allow to include a directory specification as well, this
390 is only a hint to the underlying theory loader. The internal theory
393 Theory \isa{A} is associated with the main theory file \isa{A}\verb,.thy,, which needs to be accessible through the theory
394 loader path. Any number of additional {\ML} source files may be
395 associated with each theory, by declaring these dependencies in the
396 theory header as \isa{{\isasymUSES}}, and loading them consecutively
397 within the theory context. The system keeps track of incoming {\ML}
398 sources and associates them with the current theory. The file
399 \isa{A}\verb,.ML, is loaded after a theory has been concluded, in
400 order to support legacy proof {\ML} proof scripts.
402 The basic internal actions of the theory database are \isa{update}, \isa{outdate}, and \isa{remove}:
406 \item \isa{update\ A} introduces a link of \isa{A} with a
407 \isa{theory} value of the same name; it asserts that the theory
408 sources are now consistent with that value;
410 \item \isa{outdate\ A} invalidates the link of a theory database
411 entry to its sources, but retains the present theory value;
413 \item \isa{remove\ A} deletes entry \isa{A} from the theory
418 These actions are propagated to sub- or super-graphs of a theory
419 entry as expected, in order to preserve global consistency of the
420 state of all loaded theories with the sources of the external store.
421 This implies certain causalities between actions: \isa{update}
422 or \isa{outdate} of an entry will \isa{outdate} all
423 descendants; \isa{remove} will \isa{remove} all descendants.
425 \medskip There are separate user-level interfaces to operate on the
426 theory database directly or indirectly. The primitive actions then
427 just happen automatically while working with the system. In
428 particular, processing a theory header \isa{{\isasymTHEORY}\ A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}} ensures that the
429 sub-graph of the collective imports \isa{B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n}
430 is up-to-date, too. Earlier theories are reloaded as required, with
431 \isa{update} actions proceeding in topological order according to
432 theory dependencies. There may be also a wave of implied \isa{outdate} actions for derived theory nodes until a stable situation
433 is achieved eventually.%
443 \begin{isamarkuptext}%
445 \indexml{theory}\verb|theory: string -> theory| \\
446 \indexml{use-thy}\verb|use_thy: string -> unit| \\
447 \indexml{update-thy}\verb|update_thy: string -> unit| \\
448 \indexml{touch-thy}\verb|touch_thy: string -> unit| \\
449 \indexml{remove-thy}\verb|remove_thy: string -> unit| \\[1ex]
450 \indexml{ThyInfo.begin-theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
451 \indexml{ThyInfo.end-theory}\verb|ThyInfo.end_theory: theory -> theory| \\
452 \indexml{ThyInfo.register-theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]
453 \verb|datatype action = Update |\verb,|,\verb| Outdate |\verb,|,\verb| Remove| \\
454 \indexml{ThyInfo.add-hook}\verb|ThyInfo.add_hook: (ThyInfo.action -> string -> unit) -> unit| \\
459 \item \verb|theory|~\isa{A} retrieves the theory value presently
460 associated with name \isa{A}. Note that the result might be
463 \item \verb|use_thy|~\isa{A} loads theory \isa{A} if it is absent
464 or out-of-date. It ensures that all parent theories are available
465 as well, but does not reload them if older versions are already
468 \item \verb|update_thy| is similar to \verb|use_thy|, but ensures that
469 theory \isa{A} and all ancestors are fully up-to-date.
471 \item \verb|touch_thy|~\isa{A} performs and \isa{outdate} action
472 on theory \isa{A} and all descendants.
474 \item \verb|remove_thy|~\isa{A} deletes theory \isa{A} and all
475 descendants from the theory database.
477 \item \verb|ThyInfo.begin_theory| is the basic operation behind a
478 \isa{{\isasymTHEORY}} header declaration. The boolean argument
479 indicates the strictness of treating ancestors: for \verb|true| (as
480 in interactive mode) like \verb|update_thy|, and for \verb|false| (as
481 in batch mode) like \verb|use_thy|. This is {\ML} functions is
482 normally not invoked directly.
484 \item \verb|ThyInfo.end_theory| concludes the loading of a theory
485 proper. An attached theory {\ML} file may be still loaded later on.
486 This is function is normally not invoked directly.
488 \item \verb|ThyInfo.register_theory|~\isa{text\ thy} registers an
489 existing theory value with the theory loader database. There is no
490 management of associated sources.
492 \item \verb|ThyInfo.add_hook|~\isa{f} registers function \isa{f} as a hook for theory database actions. The function will be
493 invoked with the action and theory name being involved; thus derived
494 actions may be performed in associated system components, e.g.\
495 maintaining the state of an editor for the theory sources.
497 The kind and order of actions occurring in practice depends both on
498 user interactions and the internal process of resolving theory
499 imports. Hooks should not rely on a particular policy here! Any
500 exceptions raised by the hook are ignored.
513 \isamarkupsection{Sessions and document preparation%
517 \begin{isamarkuptext}%
527 \isacommand{end}\isamarkupfalse%
539 %%% TeX-master: "root"