author | wenzelm |
Tue, 09 Apr 2013 15:37:23 +0200 | |
changeset 51659 | 5151706dc9a6 |
parent 51658 | 21c10672633b |
child 52788 | da1fdbfebd39 |
permissions | -rw-r--r-- |
29755 | 1 |
theory Integration |
2 |
imports Base |
|
3 |
begin |
|
18537 | 4 |
|
5 |
chapter {* System integration *} |
|
6 |
||
20447 | 7 |
section {* Isar toplevel \label{sec:isar-toplevel} *} |
18537 | 8 |
|
48974 | 9 |
text {* The Isar toplevel may be considered the central hub of the |
18537 | 10 |
Isabelle/Isar system, where all key components and sub-systems are |
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
37982
diff
changeset
|
11 |
integrated into a single read-eval-print loop of Isar commands, |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
37982
diff
changeset
|
12 |
which also incorporates the underlying ML compiler. |
18537 | 13 |
|
20451 | 14 |
Isabelle/Isar departs from the original ``LCF system architecture'' |
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
37982
diff
changeset
|
15 |
where ML was really The Meta Language for defining theories and |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
37982
diff
changeset
|
16 |
conducting proofs. Instead, ML now only serves as the |
18537 | 17 |
implementation language for the system (and user extensions), while |
20451 | 18 |
the specific Isar toplevel supports the concepts of theory and proof |
19 |
development natively. This includes the graph structure of theories |
|
20 |
and the block structure of proofs, support for unlimited undo, |
|
21 |
facilities for tracing, debugging, timing, profiling etc. |
|
18537 | 22 |
|
23 |
\medskip The toplevel maintains an implicit state, which is |
|
24 |
transformed by a sequence of transitions -- either interactively or |
|
25 |
in batch-mode. In interactive mode, Isar state transitions are |
|
26 |
encapsulated as safe transactions, such that both failure and undo |
|
27 |
are handled conveniently without destroying the underlying draft |
|
28 |
theory (cf.~\secref{sec:context-theory}). In batch mode, |
|
20451 | 29 |
transitions operate in a linear (destructive) fashion, such that |
30 |
error conditions abort the present attempt to construct a theory or |
|
31 |
proof altogether. |
|
18537 | 32 |
|
33 |
The toplevel state is a disjoint sum of empty @{text toplevel}, or |
|
34 |
@{text theory}, or @{text proof}. On entering the main Isar loop we |
|
35 |
start with an empty toplevel. A theory is commenced by giving a |
|
36 |
@{text \<THEORY>} header; within a theory we may issue theory |
|
20025 | 37 |
commands such as @{text \<DEFINITION>}, or state a @{text |
38 |
\<THEOREM>} to be proven. Now we are within a proof state, with a |
|
39 |
rich collection of Isar proof commands for structured proof |
|
18537 | 40 |
composition, or unstructured proof scripts. When the proof is |
41 |
concluded we get back to the theory, which is then updated by |
|
42 |
storing the resulting fact. Further theory declarations or theorem |
|
43 |
statements with proofs may follow, until we eventually conclude the |
|
44 |
theory development by issuing @{text \<END>}. The resulting theory |
|
45 |
is then stored within the theory database and we are back to the |
|
46 |
empty toplevel. |
|
47 |
||
48 |
In addition to these proper state transformations, there are also |
|
49 |
some diagnostic commands for peeking at the toplevel state without |
|
50 |
modifying it (e.g.\ \isakeyword{thm}, \isakeyword{term}, |
|
51 |
\isakeyword{print-cases}). |
|
52 |
*} |
|
53 |
||
54 |
text %mlref {* |
|
55 |
\begin{mldecls} |
|
56 |
@{index_ML_type Toplevel.state} \\ |
|
57 |
@{index_ML Toplevel.UNDEF: "exn"} \\ |
|
58 |
@{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\ |
|
59 |
@{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\ |
|
60 |
@{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\ |
|
32833 | 61 |
@{index_ML Toplevel.debug: "bool Unsynchronized.ref"} \\ |
62 |
@{index_ML Toplevel.timing: "bool Unsynchronized.ref"} \\ |
|
63 |
@{index_ML Toplevel.profiling: "int Unsynchronized.ref"} \\ |
|
18537 | 64 |
\end{mldecls} |
65 |
||
66 |
\begin{description} |
|
67 |
||
39864 | 68 |
\item Type @{ML_type Toplevel.state} represents Isar toplevel |
69 |
states, which are normally manipulated through the concept of |
|
70 |
toplevel transitions only (\secref{sec:toplevel-transition}). Also |
|
71 |
note that a raw toplevel state is subject to the same linearity |
|
72 |
restrictions as a theory context (cf.~\secref{sec:context-theory}). |
|
18537 | 73 |
|
74 |
\item @{ML Toplevel.UNDEF} is raised for undefined toplevel |
|
20451 | 75 |
operations. Many operations work only partially for certain cases, |
76 |
since @{ML_type Toplevel.state} is a sum type. |
|
18537 | 77 |
|
20451 | 78 |
\item @{ML Toplevel.is_toplevel}~@{text "state"} checks for an empty |
79 |
toplevel state. |
|
18537 | 80 |
|
34931 | 81 |
\item @{ML Toplevel.theory_of}~@{text "state"} selects the |
82 |
background theory of @{text "state"}, raises @{ML Toplevel.UNDEF} |
|
83 |
for an empty toplevel state. |
|
18537 | 84 |
|
20451 | 85 |
\item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof |
86 |
state if available, otherwise raises @{ML Toplevel.UNDEF}. |
|
18537 | 87 |
|
51659 | 88 |
\item @{ML "Toplevel.debug := true"} enables low-level exception |
89 |
trace of the ML runtime system. Note that the result might appear |
|
90 |
on some raw output window only, outside the formal context of the |
|
91 |
source text. |
|
18537 | 92 |
|
32833 | 93 |
\item @{ML "Toplevel.timing := true"} makes the toplevel print timing |
18537 | 94 |
information for each Isar command being executed. |
95 |
||
40149
4c35be108990
proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents:
39882
diff
changeset
|
96 |
\item @{ML Toplevel.profiling}~@{ML_text ":="}~@{text "n"} controls |
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
37982
diff
changeset
|
97 |
low-level profiling of the underlying ML runtime system. For |
20451 | 98 |
Poly/ML, @{text "n = 1"} means time and @{text "n = 2"} space |
99 |
profiling. |
|
18537 | 100 |
|
101 |
\end{description} |
|
102 |
*} |
|
103 |
||
39882 | 104 |
text %mlantiq {* |
105 |
\begin{matharray}{rcl} |
|
106 |
@{ML_antiquotation_def "Isar.state"} & : & @{text ML_antiquotation} \\ |
|
107 |
\end{matharray} |
|
108 |
||
109 |
\begin{description} |
|
110 |
||
111 |
\item @{text "@{Isar.state}"} refers to Isar toplevel state at that |
|
112 |
point --- as abstract value. |
|
113 |
||
114 |
This only works for diagnostic ML commands, such as @{command |
|
115 |
ML_val} or @{command ML_command}. |
|
116 |
||
117 |
\end{description} |
|
118 |
*} |
|
119 |
||
18537 | 120 |
|
20451 | 121 |
subsection {* Toplevel transitions \label{sec:toplevel-transition} *} |
18537 | 122 |
|
20451 | 123 |
text {* |
124 |
An Isar toplevel transition consists of a partial function on the |
|
125 |
toplevel state, with additional information for diagnostics and |
|
126 |
error reporting: there are fields for command name, source position, |
|
127 |
optional source text, as well as flags for interactive-only commands |
|
128 |
(which issue a warning in batch-mode), printing of result state, |
|
129 |
etc. |
|
18537 | 130 |
|
20451 | 131 |
The operational part is represented as the sequential union of a |
132 |
list of partial functions, which are tried in turn until the first |
|
20475 | 133 |
one succeeds. This acts like an outer case-expression for various |
34931 | 134 |
alternative state transitions. For example, \isakeyword{qed} works |
20475 | 135 |
differently for a local proofs vs.\ the global ending of the main |
136 |
proof. |
|
18537 | 137 |
|
138 |
Toplevel transitions are composed via transition transformers. |
|
139 |
Internally, Isar commands are put together from an empty transition |
|
34931 | 140 |
extended by name and source position. It is then left to the |
141 |
individual command parser to turn the given concrete syntax into a |
|
142 |
suitable transition transformer that adjoins actual operations on a |
|
143 |
theory or proof state etc. |
|
18537 | 144 |
*} |
145 |
||
146 |
text %mlref {* |
|
147 |
\begin{mldecls} |
|
148 |
@{index_ML Toplevel.print: "Toplevel.transition -> Toplevel.transition"} \\ |
|
149 |
@{index_ML Toplevel.keep: "(Toplevel.state -> unit) -> |
|
150 |
Toplevel.transition -> Toplevel.transition"} \\ |
|
151 |
@{index_ML Toplevel.theory: "(theory -> theory) -> |
|
152 |
Toplevel.transition -> Toplevel.transition"} \\ |
|
153 |
@{index_ML Toplevel.theory_to_proof: "(theory -> Proof.state) -> |
|
154 |
Toplevel.transition -> Toplevel.transition"} \\ |
|
155 |
@{index_ML Toplevel.proof: "(Proof.state -> Proof.state) -> |
|
156 |
Toplevel.transition -> Toplevel.transition"} \\ |
|
49864 | 157 |
@{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.result Seq.seq) -> |
18537 | 158 |
Toplevel.transition -> Toplevel.transition"} \\ |
21168
0f869edd6cc1
replaced Toplevel.proof_to_theory by Toplevel.end_proof;
wenzelm
parents:
20491
diff
changeset
|
159 |
@{index_ML Toplevel.end_proof: "(bool -> Proof.state -> Proof.context) -> |
18537 | 160 |
Toplevel.transition -> Toplevel.transition"} \\ |
161 |
\end{mldecls} |
|
162 |
||
163 |
\begin{description} |
|
164 |
||
20451 | 165 |
\item @{ML Toplevel.print}~@{text "tr"} sets the print flag, which |
166 |
causes the toplevel loop to echo the result state (in interactive |
|
167 |
mode). |
|
18537 | 168 |
|
20451 | 169 |
\item @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic |
170 |
function. |
|
18537 | 171 |
|
20451 | 172 |
\item @{ML Toplevel.theory}~@{text "tr"} adjoins a theory |
173 |
transformer. |
|
18537 | 174 |
|
20451 | 175 |
\item @{ML Toplevel.theory_to_proof}~@{text "tr"} adjoins a global |
176 |
goal function, which turns a theory into a proof state. The theory |
|
177 |
may be changed before entering the proof; the generic Isar goal |
|
178 |
setup includes an argument that specifies how to apply the proven |
|
179 |
result to the theory, when the proof is finished. |
|
18558 | 180 |
|
20451 | 181 |
\item @{ML Toplevel.proof}~@{text "tr"} adjoins a deterministic |
182 |
proof command, with a singleton result. |
|
18537 | 183 |
|
20451 | 184 |
\item @{ML Toplevel.proofs}~@{text "tr"} adjoins a general proof |
185 |
command, with zero or more result states (represented as a lazy |
|
186 |
list). |
|
18537 | 187 |
|
21168
0f869edd6cc1
replaced Toplevel.proof_to_theory by Toplevel.end_proof;
wenzelm
parents:
20491
diff
changeset
|
188 |
\item @{ML Toplevel.end_proof}~@{text "tr"} adjoins a concluding |
0f869edd6cc1
replaced Toplevel.proof_to_theory by Toplevel.end_proof;
wenzelm
parents:
20491
diff
changeset
|
189 |
proof command, that returns the resulting theory, after storing the |
0f869edd6cc1
replaced Toplevel.proof_to_theory by Toplevel.end_proof;
wenzelm
parents:
20491
diff
changeset
|
190 |
resulting facts in the context etc. |
18537 | 191 |
|
192 |
\end{description} |
|
193 |
*} |
|
194 |
||
195 |
||
20451 | 196 |
section {* Theory database \label{sec:theory-database} *} |
18537 | 197 |
|
20451 | 198 |
text {* |
199 |
The theory database maintains a collection of theories, together |
|
200 |
with some administrative information about their original sources, |
|
201 |
which are held in an external store (i.e.\ some directory within the |
|
202 |
regular file system). |
|
18537 | 203 |
|
20451 | 204 |
The theory database is organized as a directed acyclic graph; |
205 |
entries are referenced by theory name. Although some additional |
|
206 |
interfaces allow to include a directory specification as well, this |
|
207 |
is only a hint to the underlying theory loader. The internal theory |
|
208 |
name space is flat! |
|
18537 | 209 |
|
210 |
Theory @{text A} is associated with the main theory file @{text |
|
211 |
A}\verb,.thy,, which needs to be accessible through the theory |
|
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
37982
diff
changeset
|
212 |
loader path. Any number of additional ML source files may be |
18537 | 213 |
associated with each theory, by declaring these dependencies in the |
214 |
theory header as @{text \<USES>}, and loading them consecutively |
|
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
37982
diff
changeset
|
215 |
within the theory context. The system keeps track of incoming ML |
34931 | 216 |
sources and associates them with the current theory. |
18537 | 217 |
|
218 |
The basic internal actions of the theory database are @{text |
|
37982 | 219 |
"update"} and @{text "remove"}: |
18537 | 220 |
|
221 |
\begin{itemize} |
|
222 |
||
223 |
\item @{text "update A"} introduces a link of @{text "A"} with a |
|
224 |
@{text "theory"} value of the same name; it asserts that the theory |
|
20451 | 225 |
sources are now consistent with that value; |
18537 | 226 |
|
20451 | 227 |
\item @{text "remove A"} deletes entry @{text "A"} from the theory |
18537 | 228 |
database. |
229 |
||
230 |
\end{itemize} |
|
231 |
||
232 |
These actions are propagated to sub- or super-graphs of a theory |
|
20451 | 233 |
entry as expected, in order to preserve global consistency of the |
234 |
state of all loaded theories with the sources of the external store. |
|
235 |
This implies certain causalities between actions: @{text "update"} |
|
37982 | 236 |
or @{text "remove"} of an entry will @{text "remove"} all |
237 |
descendants. |
|
18537 | 238 |
|
239 |
\medskip There are separate user-level interfaces to operate on the |
|
240 |
theory database directly or indirectly. The primitive actions then |
|
241 |
just happen automatically while working with the system. In |
|
242 |
particular, processing a theory header @{text "\<THEORY> A |
|
20451 | 243 |
\<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"} ensures that the |
18537 | 244 |
sub-graph of the collective imports @{text "B\<^sub>1 \<dots> B\<^sub>n"} |
20451 | 245 |
is up-to-date, too. Earlier theories are reloaded as required, with |
18537 | 246 |
@{text update} actions proceeding in topological order according to |
247 |
theory dependencies. There may be also a wave of implied @{text |
|
37982 | 248 |
remove} actions for derived theory nodes until a stable situation |
18537 | 249 |
is achieved eventually. |
250 |
*} |
|
251 |
||
252 |
text %mlref {* |
|
253 |
\begin{mldecls} |
|
254 |
@{index_ML use_thy: "string -> unit"} \\ |
|
24173
4ba00a972eb8
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
22095
diff
changeset
|
255 |
@{index_ML use_thys: "string list -> unit"} \\ |
37864 | 256 |
@{index_ML Thy_Info.get_theory: "string -> theory"} \\ |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
34931
diff
changeset
|
257 |
@{index_ML Thy_Info.remove_thy: "string -> unit"} \\[1ex] |
37982 | 258 |
@{index_ML Thy_Info.register_thy: "theory -> unit"} \\[1ex] |
40149
4c35be108990
proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents:
39882
diff
changeset
|
259 |
@{ML_text "datatype action = Update | Remove"} \\ |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
34931
diff
changeset
|
260 |
@{index_ML Thy_Info.add_hook: "(Thy_Info.action -> string -> unit) -> unit"} \\ |
18537 | 261 |
\end{mldecls} |
262 |
||
263 |
\begin{description} |
|
264 |
||
24173
4ba00a972eb8
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
22095
diff
changeset
|
265 |
\item @{ML use_thy}~@{text A} ensures that theory @{text A} is fully |
4ba00a972eb8
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
22095
diff
changeset
|
266 |
up-to-date wrt.\ the external file store, reloading outdated |
34931 | 267 |
ancestors as required. In batch mode, the simultaneous @{ML |
268 |
use_thys} should be used exclusively. |
|
18537 | 269 |
|
24173
4ba00a972eb8
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
22095
diff
changeset
|
270 |
\item @{ML use_thys} is similar to @{ML use_thy}, but handles |
4ba00a972eb8
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
22095
diff
changeset
|
271 |
several theories simultaneously. Thus it acts like processing the |
4ba00a972eb8
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
22095
diff
changeset
|
272 |
import header of a theory, without performing the merge of the |
34931 | 273 |
result. By loading a whole sub-graph of theories like that, the |
274 |
intrinsic parallelism can be exploited by the system, to speedup |
|
275 |
loading. |
|
18537 | 276 |
|
37864 | 277 |
\item @{ML Thy_Info.get_theory}~@{text A} retrieves the theory value |
278 |
presently associated with name @{text A}. Note that the result |
|
279 |
might be outdated. |
|
280 |
||
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
34931
diff
changeset
|
281 |
\item @{ML Thy_Info.remove_thy}~@{text A} deletes theory @{text A} and all |
18537 | 282 |
descendants from the theory database. |
283 |
||
37982 | 284 |
\item @{ML Thy_Info.register_thy}~@{text "text thy"} registers an |
285 |
existing theory value with the theory loader database and updates |
|
286 |
source version information according to the current file-system |
|
287 |
state. |
|
18537 | 288 |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
34931
diff
changeset
|
289 |
\item @{ML "Thy_Info.add_hook"}~@{text f} registers function @{text |
18537 | 290 |
f} as a hook for theory database actions. The function will be |
291 |
invoked with the action and theory name being involved; thus derived |
|
292 |
actions may be performed in associated system components, e.g.\ |
|
20451 | 293 |
maintaining the state of an editor for the theory sources. |
18537 | 294 |
|
295 |
The kind and order of actions occurring in practice depends both on |
|
296 |
user interactions and the internal process of resolving theory |
|
297 |
imports. Hooks should not rely on a particular policy here! Any |
|
20451 | 298 |
exceptions raised by the hook are ignored. |
18537 | 299 |
|
300 |
\end{description} |
|
301 |
*} |
|
30272 | 302 |
|
18537 | 303 |
end |