author  wenzelm 
Sat, 05 Apr 2014 15:03:40 +0200  
changeset 56421  1ffd7eaa778b 
parent 56265  785569927666 
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 

52788  25 
in batchmode. 
18537  26 

27 
The toplevel state is a disjoint sum of empty @{text toplevel}, or 

28 
@{text theory}, or @{text proof}. On entering the main Isar loop we 

29 
start with an empty toplevel. A theory is commenced by giving a 

30 
@{text \<THEORY>} header; within a theory we may issue theory 

20025  31 
commands such as @{text \<DEFINITION>}, or state a @{text 
32 
\<THEOREM>} to be proven. Now we are within a proof state, with a 

33 
rich collection of Isar proof commands for structured proof 

18537  34 
composition, or unstructured proof scripts. When the proof is 
35 
concluded we get back to the theory, which is then updated by 

36 
storing the resulting fact. Further theory declarations or theorem 

37 
statements with proofs may follow, until we eventually conclude the 

38 
theory development by issuing @{text \<END>}. The resulting theory 

39 
is then stored within the theory database and we are back to the 

40 
empty toplevel. 

41 

42 
In addition to these proper state transformations, there are also 

43 
some diagnostic commands for peeking at the toplevel state without 

44 
modifying it (e.g.\ \isakeyword{thm}, \isakeyword{term}, 

45 
\isakeyword{printcases}). 

46 
*} 

47 

48 
text %mlref {* 

49 
\begin{mldecls} 

50 
@{index_ML_type Toplevel.state} \\ 

55838  51 
@{index_ML_exception Toplevel.UNDEF} \\ 
18537  52 
@{index_ML Toplevel.is_toplevel: "Toplevel.state > bool"} \\ 
53 
@{index_ML Toplevel.theory_of: "Toplevel.state > theory"} \\ 

54 
@{index_ML Toplevel.proof_of: "Toplevel.state > Proof.state"} \\ 

32833  55 
@{index_ML Toplevel.timing: "bool Unsynchronized.ref"} \\ 
56 
@{index_ML Toplevel.profiling: "int Unsynchronized.ref"} \\ 

18537  57 
\end{mldecls} 
58 

59 
\begin{description} 

60 

39864  61 
\item Type @{ML_type Toplevel.state} represents Isar toplevel 
62 
states, which are normally manipulated through the concept of 

63 
toplevel transitions only (\secref{sec:topleveltransition}). Also 

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

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

18537  66 

67 
\item @{ML Toplevel.UNDEF} is raised for undefined toplevel 

20451  68 
operations. Many operations work only partially for certain cases, 
69 
since @{ML_type Toplevel.state} is a sum type. 

18537  70 

20451  71 
\item @{ML Toplevel.is_toplevel}~@{text "state"} checks for an empty 
72 
toplevel state. 

18537  73 

34931  74 
\item @{ML Toplevel.theory_of}~@{text "state"} selects the 
75 
background theory of @{text "state"}, raises @{ML Toplevel.UNDEF} 

76 
for an empty toplevel state. 

18537  77 

20451  78 
\item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof 
79 
state if available, otherwise raises @{ML Toplevel.UNDEF}. 

18537  80 

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

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

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

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

18537  88 

89 
\end{description} 

90 
*} 

91 

39882  92 
text %mlantiq {* 
93 
\begin{matharray}{rcl} 

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

95 
\end{matharray} 

96 

97 
\begin{description} 

98 

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

100 
point  as abstract value. 

101 

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

103 
ML_val} or @{command ML_command}. 

104 

105 
\end{description} 

106 
*} 

107 

18537  108 

20451  109 
subsection {* Toplevel transitions \label{sec:topleveltransition} *} 
18537  110 

20451  111 
text {* 
112 
An Isar toplevel transition consists of a partial function on the 

113 
toplevel state, with additional information for diagnostics and 

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

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

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

117 
etc. 

18537  118 

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

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

18537  125 

126 
Toplevel transitions are composed via transition transformers. 

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

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

130 
suitable transition transformer that adjoins actual operations on a 

131 
theory or proof state etc. 

18537  132 
*} 
133 

134 
text %mlref {* 

135 
\begin{mldecls} 

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

137 
@{index_ML Toplevel.keep: "(Toplevel.state > unit) > 

138 
Toplevel.transition > Toplevel.transition"} \\ 

139 
@{index_ML Toplevel.theory: "(theory > theory) > 

140 
Toplevel.transition > Toplevel.transition"} \\ 

141 
@{index_ML Toplevel.theory_to_proof: "(theory > Proof.state) > 

142 
Toplevel.transition > Toplevel.transition"} \\ 

143 
@{index_ML Toplevel.proof: "(Proof.state > Proof.state) > 

144 
Toplevel.transition > Toplevel.transition"} \\ 

49864  145 
@{index_ML Toplevel.proofs: "(Proof.state > Proof.state Seq.result Seq.seq) > 
18537  146 
Toplevel.transition > Toplevel.transition"} \\ 
21168
0f869edd6cc1
replaced Toplevel.proof_to_theory by Toplevel.end_proof;
wenzelm
parents:
20491
diff
changeset

147 
@{index_ML Toplevel.end_proof: "(bool > Proof.state > Proof.context) > 
18537  148 
Toplevel.transition > Toplevel.transition"} \\ 
149 
\end{mldecls} 

150 

151 
\begin{description} 

152 

20451  153 
\item @{ML Toplevel.print}~@{text "tr"} sets the print flag, which 
154 
causes the toplevel loop to echo the result state (in interactive 

155 
mode). 

18537  156 

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

18537  159 

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

18537  162 

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

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

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

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

18558  168 

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

18537  171 

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

174 
list). 

18537  175 

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

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

177 
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

178 
resulting facts in the context etc. 
18537  179 

180 
\end{description} 

181 
*} 

182 

183 

20451  184 
section {* Theory database \label{sec:theorydatabase} *} 
18537  185 

20451  186 
text {* 
187 
The theory database maintains a collection of theories, together 

188 
with some administrative information about their original sources, 

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

190 
regular file system). 

18537  191 

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

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

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

196 
name space is flat! 

18537  197 

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

199 
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

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

203 
within the theory context. The system keeps track of incoming ML 
34931  204 
sources and associates them with the current theory. 
18537  205 

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

37982  207 
"update"} and @{text "remove"}: 
18537  208 

209 
\begin{itemize} 

210 

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

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

20451  213 
sources are now consistent with that value; 
18537  214 

20451  215 
\item @{text "remove A"} deletes entry @{text "A"} from the theory 
18537  216 
database. 
217 

218 
\end{itemize} 

219 

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

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

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

37982  224 
or @{text "remove"} of an entry will @{text "remove"} all 
225 
descendants. 

18537  226 

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

228 
theory database directly or indirectly. The primitive actions then 

229 
just happen automatically while working with the system. In 

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

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

37982  236 
remove} actions for derived theory nodes until a stable situation 
18537  237 
is achieved eventually. 
238 
*} 

239 

240 
text %mlref {* 

241 
\begin{mldecls} 

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

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

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

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

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

248 
@{index_ML Thy_Info.add_hook: "(Thy_Info.action > string > unit) > unit"} \\ 
18537  249 
\end{mldecls} 
250 

251 
\begin{description} 

252 

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

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

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

18537  257 

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

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

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

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

263 
loading. 

18537  264 

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

267 
might be outdated. 

268 

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

269 
\item @{ML Thy_Info.remove_thy}~@{text A} deletes theory @{text A} and all 
18537  270 
descendants from the theory database. 
271 

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

274 
source version information according to the current filesystem 

275 
state. 

18537  276 

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

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

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

20451  281 
maintaining the state of an editor for the theory sources. 
18537  282 

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

284 
user interactions and the internal process of resolving theory 

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

20451  286 
exceptions raised by the hook are ignored. 
18537  287 

288 
\end{description} 

289 
*} 

30272  290 

18537  291 
end 