author  webertj 
Tue, 28 Aug 2012 16:33:06 +0200  
changeset 48974  8882fc8005ad 
parent 48938  d468d72a458f 
permissions  rwrr 
29755  1 
theory Integration 
2 
imports Base 

3 
begin 

18537  4 

5 
chapter {* System integration *} 

6 

20447  7 
section {* Isar toplevel \label{sec:isartoplevel} *} 
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 subsystems 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 readevalprint 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 batchmode. 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:contexttheory}). 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{printcases}). 

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:topleveltransition}). Also 

71 
note that a raw toplevel state is subject to the same linearity 

72 
restrictions as a theory context (cf.~\secref{sec:contexttheory}). 

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 

32833  88 
\item @{ML "Toplevel.debug := true"} makes the toplevel print further 
18537  89 
details about internal error conditions, exceptions being raised 
90 
etc. 

91 

32833  92 
\item @{ML "Toplevel.timing := true"} makes the toplevel print timing 
18537  93 
information for each Isar command being executed. 
94 

40149
4c35be108990
proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents:
39882
diff
changeset

95 
\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

96 
lowlevel profiling of the underlying ML runtime system. For 
20451  97 
Poly/ML, @{text "n = 1"} means time and @{text "n = 2"} space 
98 
profiling. 

18537  99 

100 
\end{description} 

101 
*} 

102 

39882  103 
text %mlantiq {* 
104 
\begin{matharray}{rcl} 

105 
@{ML_antiquotation_def "Isar.state"} & : & @{text ML_antiquotation} \\ 

106 
\end{matharray} 

107 

108 
\begin{description} 

109 

110 
\item @{text "@{Isar.state}"} refers to Isar toplevel state at that 

111 
point  as abstract value. 

112 

113 
This only works for diagnostic ML commands, such as @{command 

114 
ML_val} or @{command ML_command}. 

115 

116 
\end{description} 

117 
*} 

118 

18537  119 

20451  120 
subsection {* Toplevel transitions \label{sec:topleveltransition} *} 
18537  121 

20451  122 
text {* 
123 
An Isar toplevel transition consists of a partial function on the 

124 
toplevel state, with additional information for diagnostics and 

125 
error reporting: there are fields for command name, source position, 

126 
optional source text, as well as flags for interactiveonly commands 

127 
(which issue a warning in batchmode), printing of result state, 

128 
etc. 

18537  129 

20451  130 
The operational part is represented as the sequential union of a 
131 
list of partial functions, which are tried in turn until the first 

20475  132 
one succeeds. This acts like an outer caseexpression for various 
34931  133 
alternative state transitions. For example, \isakeyword{qed} works 
20475  134 
differently for a local proofs vs.\ the global ending of the main 
135 
proof. 

18537  136 

137 
Toplevel transitions are composed via transition transformers. 

138 
Internally, Isar commands are put together from an empty transition 

34931  139 
extended by name and source position. It is then left to the 
140 
individual command parser to turn the given concrete syntax into a 

141 
suitable transition transformer that adjoins actual operations on a 

142 
theory or proof state etc. 

18537  143 
*} 
144 

145 
text %mlref {* 

146 
\begin{mldecls} 

147 
@{index_ML Toplevel.print: "Toplevel.transition > Toplevel.transition"} \\ 

148 
@{index_ML Toplevel.no_timing: "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"} \\ 

157 
@{index_ML Toplevel.proofs: "(Proof.state > Proof.state Seq.seq) > 

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.no_timing}~@{text "tr"} indicates that the 
170 
transition should never show timing information, e.g.\ because it is 

171 
a diagnostic command. 

18537  172 

20451  173 
\item @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic 
174 
function. 

18537  175 

20451  176 
\item @{ML Toplevel.theory}~@{text "tr"} adjoins a theory 
177 
transformer. 

18537  178 

20451  179 
\item @{ML Toplevel.theory_to_proof}~@{text "tr"} adjoins a global 
180 
goal function, which turns a theory into a proof state. The theory 

181 
may be changed before entering the proof; the generic Isar goal 

182 
setup includes an argument that specifies how to apply the proven 

183 
result to the theory, when the proof is finished. 

18558  184 

20451  185 
\item @{ML Toplevel.proof}~@{text "tr"} adjoins a deterministic 
186 
proof command, with a singleton result. 

18537  187 

20451  188 
\item @{ML Toplevel.proofs}~@{text "tr"} adjoins a general proof 
189 
command, with zero or more result states (represented as a lazy 

190 
list). 

18537  191 

21168
0f869edd6cc1
replaced Toplevel.proof_to_theory by Toplevel.end_proof;
wenzelm
parents:
20491
diff
changeset

192 
\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

193 
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

194 
resulting facts in the context etc. 
18537  195 

196 
\end{description} 

197 
*} 

198 

199 

20451  200 
section {* Theory database \label{sec:theorydatabase} *} 
18537  201 

20451  202 
text {* 
203 
The theory database maintains a collection of theories, together 

204 
with some administrative information about their original sources, 

205 
which are held in an external store (i.e.\ some directory within the 

206 
regular file system). 

18537  207 

20451  208 
The theory database is organized as a directed acyclic graph; 
209 
entries are referenced by theory name. Although some additional 

210 
interfaces allow to include a directory specification as well, this 

211 
is only a hint to the underlying theory loader. The internal theory 

212 
name space is flat! 

18537  213 

214 
Theory @{text A} is associated with the main theory file @{text 

215 
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

216 
loader path. Any number of additional ML source files may be 
18537  217 
associated with each theory, by declaring these dependencies in the 
218 
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

219 
within the theory context. The system keeps track of incoming ML 
34931  220 
sources and associates them with the current theory. 
18537  221 

222 
The basic internal actions of the theory database are @{text 

37982  223 
"update"} and @{text "remove"}: 
18537  224 

225 
\begin{itemize} 

226 

227 
\item @{text "update A"} introduces a link of @{text "A"} with a 

228 
@{text "theory"} value of the same name; it asserts that the theory 

20451  229 
sources are now consistent with that value; 
18537  230 

20451  231 
\item @{text "remove A"} deletes entry @{text "A"} from the theory 
18537  232 
database. 
233 

234 
\end{itemize} 

235 

236 
These actions are propagated to sub or supergraphs of a theory 

20451  237 
entry as expected, in order to preserve global consistency of the 
238 
state of all loaded theories with the sources of the external store. 

239 
This implies certain causalities between actions: @{text "update"} 

37982  240 
or @{text "remove"} of an entry will @{text "remove"} all 
241 
descendants. 

18537  242 

243 
\medskip There are separate userlevel interfaces to operate on the 

244 
theory database directly or indirectly. The primitive actions then 

245 
just happen automatically while working with the system. In 

246 
particular, processing a theory header @{text "\<THEORY> A 

20451  247 
\<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"} ensures that the 
18537  248 
subgraph of the collective imports @{text "B\<^sub>1 \<dots> B\<^sub>n"} 
20451  249 
is uptodate, too. Earlier theories are reloaded as required, with 
18537  250 
@{text update} actions proceeding in topological order according to 
251 
theory dependencies. There may be also a wave of implied @{text 

37982  252 
remove} actions for derived theory nodes until a stable situation 
18537  253 
is achieved eventually. 
254 
*} 

255 

256 
text %mlref {* 

257 
\begin{mldecls} 

258 
@{index_ML use_thy: "string > unit"} \\ 

24173
4ba00a972eb8
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
22095
diff
changeset

259 
@{index_ML use_thys: "string list > unit"} \\ 
37864  260 
@{index_ML Thy_Info.get_theory: "string > theory"} \\ 
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
34931
diff
changeset

261 
@{index_ML Thy_Info.remove_thy: "string > unit"} \\[1ex] 
37982  262 
@{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

263 
@{ML_text "datatype action = Update  Remove"} \\ 
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
34931
diff
changeset

264 
@{index_ML Thy_Info.add_hook: "(Thy_Info.action > string > unit) > unit"} \\ 
18537  265 
\end{mldecls} 
266 

267 
\begin{description} 

268 

24173
4ba00a972eb8
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
22095
diff
changeset

269 
\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

270 
uptodate wrt.\ the external file store, reloading outdated 
34931  271 
ancestors as required. In batch mode, the simultaneous @{ML 
272 
use_thys} should be used exclusively. 

18537  273 

24173
4ba00a972eb8
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
22095
diff
changeset

274 
\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

275 
several theories simultaneously. Thus it acts like processing the 
4ba00a972eb8
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
22095
diff
changeset

276 
import header of a theory, without performing the merge of the 
34931  277 
result. By loading a whole subgraph of theories like that, the 
278 
intrinsic parallelism can be exploited by the system, to speedup 

279 
loading. 

18537  280 

37864  281 
\item @{ML Thy_Info.get_theory}~@{text A} retrieves the theory value 
282 
presently associated with name @{text A}. Note that the result 

283 
might be outdated. 

284 

37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
34931
diff
changeset

285 
\item @{ML Thy_Info.remove_thy}~@{text A} deletes theory @{text A} and all 
18537  286 
descendants from the theory database. 
287 

37982  288 
\item @{ML Thy_Info.register_thy}~@{text "text thy"} registers an 
289 
existing theory value with the theory loader database and updates 

290 
source version information according to the current filesystem 

291 
state. 

18537  292 

37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
34931
diff
changeset

293 
\item @{ML "Thy_Info.add_hook"}~@{text f} registers function @{text 
18537  294 
f} as a hook for theory database actions. The function will be 
295 
invoked with the action and theory name being involved; thus derived 

296 
actions may be performed in associated system components, e.g.\ 

20451  297 
maintaining the state of an editor for the theory sources. 
18537  298 

299 
The kind and order of actions occurring in practice depends both on 

300 
user interactions and the internal process of resolving theory 

301 
imports. Hooks should not rely on a particular policy here! Any 

20451  302 
exceptions raised by the hook are ignored. 
18537  303 

304 
\end{description} 

305 
*} 

30272  306 

18537  307 
end 