author | wenzelm |
Sun, 18 Oct 2015 22:57:09 +0200 | |
changeset 61477 | e467ae7aa808 |
parent 61458 | 987533262fc2 |
child 61493 | 0debd22f0c0e |
permissions | -rw-r--r-- |
57341 | 1 |
(*:wrap=hard:maxLineLen=78:*) |
2 |
||
29755 | 3 |
theory Integration |
4 |
imports Base |
|
5 |
begin |
|
18537 | 6 |
|
58618 | 7 |
chapter \<open>System integration\<close> |
18537 | 8 |
|
58618 | 9 |
section \<open>Isar toplevel \label{sec:isar-toplevel}\<close> |
18537 | 10 |
|
58618 | 11 |
text \<open> |
61477 | 12 |
The Isar \<^emph>\<open>toplevel state\<close> represents the outermost configuration that |
57343 | 13 |
is transformed by a sequence of transitions (commands) within a theory body. |
14 |
This is a pure value with pure functions acting on it in a timeless and |
|
15 |
stateless manner. Historically, the sequence of transitions was wrapped up |
|
57496 | 16 |
as sequential command loop, such that commands are applied one-by-one. In |
17 |
contemporary Isabelle/Isar, processing toplevel commands usually works in |
|
58555 | 18 |
parallel in multi-threaded Isabelle/ML @{cite "Wenzel:2009" and |
19 |
"Wenzel:2013:ITP"}. |
|
58618 | 20 |
\<close> |
18537 | 21 |
|
22 |
||
58618 | 23 |
subsection \<open>Toplevel state\<close> |
18537 | 24 |
|
58618 | 25 |
text \<open> |
57343 | 26 |
The toplevel state is a disjoint sum of empty @{text toplevel}, or @{text |
27 |
theory}, or @{text proof}. The initial toplevel is empty; a theory is |
|
28 |
commenced by a @{command theory} header; within a theory we may use theory |
|
29 |
commands such as @{command definition}, or state a @{command theorem} to be |
|
30 |
proven. A proof state accepts a rich collection of Isar proof commands for |
|
31 |
structured proof composition, or unstructured proof scripts. When the proof |
|
57496 | 32 |
is concluded we get back to the (local) theory, which is then updated by |
33 |
defining the resulting fact. Further theory declarations or theorem |
|
34 |
statements with proofs may follow, until we eventually conclude the theory |
|
35 |
development by issuing @{command end} to get back to the empty toplevel. |
|
58618 | 36 |
\<close> |
18537 | 37 |
|
58618 | 38 |
text %mlref \<open> |
18537 | 39 |
\begin{mldecls} |
40 |
@{index_ML_type Toplevel.state} \\ |
|
55838 | 41 |
@{index_ML_exception Toplevel.UNDEF} \\ |
18537 | 42 |
@{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\ |
43 |
@{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\ |
|
44 |
@{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\ |
|
45 |
\end{mldecls} |
|
46 |
||
61439 | 47 |
\<^descr> Type @{ML_type Toplevel.state} represents Isar toplevel |
39864 | 48 |
states, which are normally manipulated through the concept of |
57343 | 49 |
toplevel transitions only (\secref{sec:toplevel-transition}). |
18537 | 50 |
|
61439 | 51 |
\<^descr> @{ML Toplevel.UNDEF} is raised for undefined toplevel |
20451 | 52 |
operations. Many operations work only partially for certain cases, |
53 |
since @{ML_type Toplevel.state} is a sum type. |
|
18537 | 54 |
|
61439 | 55 |
\<^descr> @{ML Toplevel.is_toplevel}~@{text "state"} checks for an empty |
20451 | 56 |
toplevel state. |
18537 | 57 |
|
61439 | 58 |
\<^descr> @{ML Toplevel.theory_of}~@{text "state"} selects the |
57496 | 59 |
background theory of @{text "state"}, it raises @{ML Toplevel.UNDEF} |
34931 | 60 |
for an empty toplevel state. |
18537 | 61 |
|
61439 | 62 |
\<^descr> @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof |
60094 | 63 |
state if available, otherwise it raises an error. |
58618 | 64 |
\<close> |
18537 | 65 |
|
58618 | 66 |
text %mlantiq \<open> |
39882 | 67 |
\begin{matharray}{rcl} |
68 |
@{ML_antiquotation_def "Isar.state"} & : & @{text ML_antiquotation} \\ |
|
69 |
\end{matharray} |
|
70 |
||
61439 | 71 |
\<^descr> @{text "@{Isar.state}"} refers to Isar toplevel state at that |
39882 | 72 |
point --- as abstract value. |
73 |
||
74 |
This only works for diagnostic ML commands, such as @{command |
|
75 |
ML_val} or @{command ML_command}. |
|
58618 | 76 |
\<close> |
39882 | 77 |
|
18537 | 78 |
|
58618 | 79 |
subsection \<open>Toplevel transitions \label{sec:toplevel-transition}\<close> |
18537 | 80 |
|
58618 | 81 |
text \<open> |
57421 | 82 |
An Isar toplevel transition consists of a partial function on the toplevel |
83 |
state, with additional information for diagnostics and error reporting: |
|
84 |
there are fields for command name, source position, and other meta-data. |
|
18537 | 85 |
|
20451 | 86 |
The operational part is represented as the sequential union of a |
87 |
list of partial functions, which are tried in turn until the first |
|
20475 | 88 |
one succeeds. This acts like an outer case-expression for various |
34931 | 89 |
alternative state transitions. For example, \isakeyword{qed} works |
57496 | 90 |
differently for a local proofs vs.\ the global ending of an outermost |
20475 | 91 |
proof. |
18537 | 92 |
|
57496 | 93 |
Transitions are composed via transition transformers. Internally, Isar |
94 |
commands are put together from an empty transition extended by name and |
|
95 |
source position. It is then left to the individual command parser to turn |
|
96 |
the given concrete syntax into a suitable transition transformer that |
|
97 |
adjoins actual operations on a theory or proof state. |
|
58618 | 98 |
\<close> |
18537 | 99 |
|
58618 | 100 |
text %mlref \<open> |
18537 | 101 |
\begin{mldecls} |
102 |
@{index_ML Toplevel.keep: "(Toplevel.state -> unit) -> |
|
103 |
Toplevel.transition -> Toplevel.transition"} \\ |
|
104 |
@{index_ML Toplevel.theory: "(theory -> theory) -> |
|
105 |
Toplevel.transition -> Toplevel.transition"} \\ |
|
106 |
@{index_ML Toplevel.theory_to_proof: "(theory -> Proof.state) -> |
|
107 |
Toplevel.transition -> Toplevel.transition"} \\ |
|
108 |
@{index_ML Toplevel.proof: "(Proof.state -> Proof.state) -> |
|
109 |
Toplevel.transition -> Toplevel.transition"} \\ |
|
49864 | 110 |
@{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.result Seq.seq) -> |
18537 | 111 |
Toplevel.transition -> Toplevel.transition"} \\ |
21168
0f869edd6cc1
replaced Toplevel.proof_to_theory by Toplevel.end_proof;
wenzelm
parents:
20491
diff
changeset
|
112 |
@{index_ML Toplevel.end_proof: "(bool -> Proof.state -> Proof.context) -> |
18537 | 113 |
Toplevel.transition -> Toplevel.transition"} \\ |
114 |
\end{mldecls} |
|
115 |
||
61439 | 116 |
\<^descr> @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic |
20451 | 117 |
function. |
18537 | 118 |
|
61439 | 119 |
\<^descr> @{ML Toplevel.theory}~@{text "tr"} adjoins a theory |
20451 | 120 |
transformer. |
18537 | 121 |
|
61439 | 122 |
\<^descr> @{ML Toplevel.theory_to_proof}~@{text "tr"} adjoins a global |
20451 | 123 |
goal function, which turns a theory into a proof state. The theory |
124 |
may be changed before entering the proof; the generic Isar goal |
|
57421 | 125 |
setup includes an @{verbatim after_qed} argument that specifies how to |
126 |
apply the proven result to the enclosing context, when the proof |
|
127 |
is finished. |
|
18558 | 128 |
|
61439 | 129 |
\<^descr> @{ML Toplevel.proof}~@{text "tr"} adjoins a deterministic |
20451 | 130 |
proof command, with a singleton result. |
18537 | 131 |
|
61439 | 132 |
\<^descr> @{ML Toplevel.proofs}~@{text "tr"} adjoins a general proof |
20451 | 133 |
command, with zero or more result states (represented as a lazy |
134 |
list). |
|
18537 | 135 |
|
61439 | 136 |
\<^descr> @{ML Toplevel.end_proof}~@{text "tr"} adjoins a concluding |
57496 | 137 |
proof command, that returns the resulting theory, after applying the |
138 |
resulting facts to the target context. |
|
58618 | 139 |
\<close> |
18537 | 140 |
|
59090 | 141 |
text %mlex \<open>The file @{"file" "~~/src/HOL/ex/Commands.thy"} shows some example |
142 |
Isar command definitions, with the all-important theory header declarations |
|
143 |
for outer syntax keywords.\<close> |
|
144 |
||
18537 | 145 |
|
58618 | 146 |
section \<open>Theory loader database\<close> |
18537 | 147 |
|
58618 | 148 |
text \<open> |
57341 | 149 |
In batch mode and within dumped logic images, the theory database maintains |
150 |
a collection of theories as a directed acyclic graph. A theory may refer to |
|
151 |
other theories as @{keyword "imports"}, or to auxiliary files via special |
|
61477 | 152 |
\<^emph>\<open>load commands\<close> (e.g.\ @{command ML_file}). For each theory, the base |
153 |
directory of its own theory file is called \<^emph>\<open>master directory\<close>: this is |
|
57341 | 154 |
used as the relative location to refer to other files from that theory. |
58618 | 155 |
\<close> |
18537 | 156 |
|
58618 | 157 |
text %mlref \<open> |
18537 | 158 |
\begin{mldecls} |
159 |
@{index_ML use_thy: "string -> unit"} \\ |
|
57496 | 160 |
@{index_ML use_thys: "string list -> unit"} \\[0.5ex] |
37864 | 161 |
@{index_ML Thy_Info.get_theory: "string -> theory"} \\ |
57341 | 162 |
@{index_ML Thy_Info.remove_thy: "string -> unit"} \\ |
163 |
@{index_ML Thy_Info.register_thy: "theory -> unit"} \\ |
|
18537 | 164 |
\end{mldecls} |
165 |
||
61439 | 166 |
\<^descr> @{ML use_thy}~@{text A} ensures that theory @{text A} is fully |
57496 | 167 |
up-to-date wrt.\ the external file store; outdated ancestors are reloaded on |
168 |
demand. |
|
18537 | 169 |
|
61439 | 170 |
\<^descr> @{ML use_thys} is similar to @{ML use_thy}, but handles several |
57341 | 171 |
theories simultaneously. Thus it acts like processing the import header of a |
172 |
theory, without performing the merge of the result. By loading a whole |
|
173 |
sub-graph of theories, the intrinsic parallelism can be exploited by the |
|
174 |
system to speedup loading. |
|
18537 | 175 |
|
60270 | 176 |
This variant is used by default in @{tool build} @{cite "isabelle-system"}. |
57496 | 177 |
|
61439 | 178 |
\<^descr> @{ML Thy_Info.get_theory}~@{text A} retrieves the theory value |
57341 | 179 |
presently associated with name @{text A}. Note that the result might be |
180 |
outdated wrt.\ the file-system content. |
|
37864 | 181 |
|
61439 | 182 |
\<^descr> @{ML Thy_Info.remove_thy}~@{text A} deletes theory @{text A} and all |
18537 | 183 |
descendants from the theory database. |
184 |
||
61439 | 185 |
\<^descr> @{ML Thy_Info.register_thy}~@{text "text thy"} registers an existing |
57341 | 186 |
theory value with the theory loader database and updates source version |
57496 | 187 |
information according to the file store. |
58618 | 188 |
\<close> |
30272 | 189 |
|
18537 | 190 |
end |