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