author | wenzelm |
Sun, 24 Mar 2019 17:45:00 +0100 | |
changeset 69967 | 8a9d0d894ec0 |
parent 69597 | ff784d5a5bfb |
child 72029 | 83456d9f0ed5 |
permissions | -rw-r--r-- |
61656 | 1 |
(*:maxLineLen=78:*) |
57341 | 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> |
61854 | 12 |
The Isar \<^emph>\<open>toplevel state\<close> represents the outermost configuration that is |
13 |
transformed by a sequence of transitions (commands) within a theory body. |
|
57343 | 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> |
61854 | 26 |
The toplevel state is a disjoint sum of empty \<open>toplevel\<close>, or \<open>theory\<close>, or |
27 |
\<open>proof\<close>. The initial toplevel is empty; a theory is commenced by a @{command |
|
28 |
theory} header; within a theory we may use theory commands such as @{command |
|
29 |
definition}, or state a @{command theorem} to be proven. A proof state |
|
30 |
accepts a rich collection of Isar proof commands for structured proof |
|
31 |
composition, or unstructured proof scripts. When the proof is concluded we |
|
32 |
get back to the (local) theory, which is then updated by defining the |
|
33 |
resulting fact. Further theory declarations or theorem statements with |
|
34 |
proofs may follow, until we eventually conclude the theory development by |
|
35 |
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 |
||
69597 | 47 |
\<^descr> Type \<^ML_type>\<open>Toplevel.state\<close> represents Isar toplevel states, which are |
61854 | 48 |
normally manipulated through the concept of toplevel transitions only |
49 |
(\secref{sec:toplevel-transition}). |
|
18537 | 50 |
|
69597 | 51 |
\<^descr> \<^ML>\<open>Toplevel.UNDEF\<close> is raised for undefined toplevel operations. Many |
52 |
operations work only partially for certain cases, since \<^ML_type>\<open>Toplevel.state\<close> is a sum type. |
|
53 |
||
54 |
\<^descr> \<^ML>\<open>Toplevel.is_toplevel\<close>~\<open>state\<close> checks for an empty toplevel state. |
|
18537 | 55 |
|
69597 | 56 |
\<^descr> \<^ML>\<open>Toplevel.theory_of\<close>~\<open>state\<close> selects the background theory of \<open>state\<close>, |
57 |
it raises \<^ML>\<open>Toplevel.UNDEF\<close> for an empty toplevel state. |
|
18537 | 58 |
|
69597 | 59 |
\<^descr> \<^ML>\<open>Toplevel.proof_of\<close>~\<open>state\<close> selects the Isar proof state if available, |
61854 | 60 |
otherwise it raises an error. |
58618 | 61 |
\<close> |
18537 | 62 |
|
58618 | 63 |
text %mlantiq \<open> |
39882 | 64 |
\begin{matharray}{rcl} |
61493 | 65 |
@{ML_antiquotation_def "Isar.state"} & : & \<open>ML_antiquotation\<close> \\ |
39882 | 66 |
\end{matharray} |
67 |
||
61854 | 68 |
\<^descr> \<open>@{Isar.state}\<close> refers to Isar toplevel state at that point --- as |
69 |
abstract value. |
|
39882 | 70 |
|
61854 | 71 |
This only works for diagnostic ML commands, such as @{command ML_val} or |
72 |
@{command ML_command}. |
|
58618 | 73 |
\<close> |
39882 | 74 |
|
18537 | 75 |
|
58618 | 76 |
subsection \<open>Toplevel transitions \label{sec:toplevel-transition}\<close> |
18537 | 77 |
|
58618 | 78 |
text \<open> |
57421 | 79 |
An Isar toplevel transition consists of a partial function on the toplevel |
80 |
state, with additional information for diagnostics and error reporting: |
|
81 |
there are fields for command name, source position, and other meta-data. |
|
18537 | 82 |
|
61854 | 83 |
The operational part is represented as the sequential union of a list of |
84 |
partial functions, which are tried in turn until the first one succeeds. |
|
85 |
This acts like an outer case-expression for various alternative state |
|
62947 | 86 |
transitions. For example, \<^theory_text>\<open>qed\<close> works differently for a local proofs vs.\ |
87 |
the global ending of an outermost proof. |
|
18537 | 88 |
|
57496 | 89 |
Transitions are composed via transition transformers. Internally, Isar |
90 |
commands are put together from an empty transition extended by name and |
|
91 |
source position. It is then left to the individual command parser to turn |
|
92 |
the given concrete syntax into a suitable transition transformer that |
|
93 |
adjoins actual operations on a theory or proof state. |
|
58618 | 94 |
\<close> |
18537 | 95 |
|
58618 | 96 |
text %mlref \<open> |
18537 | 97 |
\begin{mldecls} |
98 |
@{index_ML Toplevel.keep: "(Toplevel.state -> unit) -> |
|
99 |
Toplevel.transition -> Toplevel.transition"} \\ |
|
100 |
@{index_ML Toplevel.theory: "(theory -> theory) -> |
|
101 |
Toplevel.transition -> Toplevel.transition"} \\ |
|
102 |
@{index_ML Toplevel.theory_to_proof: "(theory -> Proof.state) -> |
|
103 |
Toplevel.transition -> Toplevel.transition"} \\ |
|
104 |
@{index_ML Toplevel.proof: "(Proof.state -> Proof.state) -> |
|
105 |
Toplevel.transition -> Toplevel.transition"} \\ |
|
49864 | 106 |
@{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.result Seq.seq) -> |
18537 | 107 |
Toplevel.transition -> Toplevel.transition"} \\ |
21168
0f869edd6cc1
replaced Toplevel.proof_to_theory by Toplevel.end_proof;
wenzelm
parents:
20491
diff
changeset
|
108 |
@{index_ML Toplevel.end_proof: "(bool -> Proof.state -> Proof.context) -> |
18537 | 109 |
Toplevel.transition -> Toplevel.transition"} \\ |
110 |
\end{mldecls} |
|
111 |
||
69597 | 112 |
\<^descr> \<^ML>\<open>Toplevel.keep\<close>~\<open>tr\<close> adjoins a diagnostic function. |
61854 | 113 |
|
69597 | 114 |
\<^descr> \<^ML>\<open>Toplevel.theory\<close>~\<open>tr\<close> adjoins a theory transformer. |
18537 | 115 |
|
69597 | 116 |
\<^descr> \<^ML>\<open>Toplevel.theory_to_proof\<close>~\<open>tr\<close> adjoins a global goal function, which |
61854 | 117 |
turns a theory into a proof state. The theory may be changed before entering |
118 |
the proof; the generic Isar goal setup includes an \<^verbatim>\<open>after_qed\<close> argument |
|
119 |
that specifies how to apply the proven result to the enclosing context, when |
|
120 |
the proof is finished. |
|
18537 | 121 |
|
69597 | 122 |
\<^descr> \<^ML>\<open>Toplevel.proof\<close>~\<open>tr\<close> adjoins a deterministic proof command, with a |
61854 | 123 |
singleton result. |
18558 | 124 |
|
69597 | 125 |
\<^descr> \<^ML>\<open>Toplevel.proofs\<close>~\<open>tr\<close> adjoins a general proof command, with zero or |
61854 | 126 |
more result states (represented as a lazy list). |
18537 | 127 |
|
69597 | 128 |
\<^descr> \<^ML>\<open>Toplevel.end_proof\<close>~\<open>tr\<close> adjoins a concluding proof command, that |
61854 | 129 |
returns the resulting theory, after applying the resulting facts to the |
130 |
target context. |
|
58618 | 131 |
\<close> |
18537 | 132 |
|
61854 | 133 |
text %mlex \<open> |
63680 | 134 |
The file \<^file>\<open>~~/src/HOL/ex/Commands.thy\<close> shows some example Isar command |
135 |
definitions, with the all-important theory header declarations for outer |
|
136 |
syntax keywords. |
|
61854 | 137 |
\<close> |
59090 | 138 |
|
18537 | 139 |
|
58618 | 140 |
section \<open>Theory loader database\<close> |
18537 | 141 |
|
58618 | 142 |
text \<open> |
57341 | 143 |
In batch mode and within dumped logic images, the theory database maintains |
144 |
a collection of theories as a directed acyclic graph. A theory may refer to |
|
145 |
other theories as @{keyword "imports"}, or to auxiliary files via special |
|
61477 | 146 |
\<^emph>\<open>load commands\<close> (e.g.\ @{command ML_file}). For each theory, the base |
61854 | 147 |
directory of its own theory file is called \<^emph>\<open>master directory\<close>: this is used |
148 |
as the relative location to refer to other files from that theory. |
|
58618 | 149 |
\<close> |
18537 | 150 |
|
58618 | 151 |
text %mlref \<open> |
18537 | 152 |
\begin{mldecls} |
153 |
@{index_ML use_thy: "string -> unit"} \\ |
|
37864 | 154 |
@{index_ML Thy_Info.get_theory: "string -> theory"} \\ |
57341 | 155 |
@{index_ML Thy_Info.remove_thy: "string -> unit"} \\ |
156 |
@{index_ML Thy_Info.register_thy: "theory -> unit"} \\ |
|
18537 | 157 |
\end{mldecls} |
158 |
||
69597 | 159 |
\<^descr> \<^ML>\<open>use_thy\<close>~\<open>A\<close> ensures that theory \<open>A\<close> is fully up-to-date wrt.\ the |
61854 | 160 |
external file store; outdated ancestors are reloaded on demand. |
18537 | 161 |
|
69597 | 162 |
\<^descr> \<^ML>\<open>Thy_Info.get_theory\<close>~\<open>A\<close> retrieves the theory value presently |
61854 | 163 |
associated with name \<open>A\<close>. Note that the result might be outdated wrt.\ the |
164 |
file-system content. |
|
37864 | 165 |
|
69597 | 166 |
\<^descr> \<^ML>\<open>Thy_Info.remove_thy\<close>~\<open>A\<close> deletes theory \<open>A\<close> and all descendants from |
61854 | 167 |
the theory database. |
18537 | 168 |
|
69597 | 169 |
\<^descr> \<^ML>\<open>Thy_Info.register_thy\<close>~\<open>text thy\<close> registers an existing theory value |
61854 | 170 |
with the theory loader database and updates source version information |
171 |
according to the file store. |
|
58618 | 172 |
\<close> |
30272 | 173 |
|
18537 | 174 |
end |