--- a/src/Doc/Implementation/Integration.thy Wed Dec 16 16:31:36 2015 +0100
+++ b/src/Doc/Implementation/Integration.thy Wed Dec 16 17:28:49 2015 +0100
@@ -9,8 +9,8 @@
section \<open>Isar toplevel \label{sec:isar-toplevel}\<close>
text \<open>
- The Isar \<^emph>\<open>toplevel state\<close> represents the outermost configuration that
- is transformed by a sequence of transitions (commands) within a theory body.
+ The Isar \<^emph>\<open>toplevel state\<close> represents the outermost configuration that is
+ transformed by a sequence of transitions (commands) within a theory body.
This is a pure value with pure functions acting on it in a timeless and
stateless manner. Historically, the sequence of transitions was wrapped up
as sequential command loop, such that commands are applied one-by-one. In
@@ -23,15 +23,16 @@
subsection \<open>Toplevel state\<close>
text \<open>
- The toplevel state is a disjoint sum of empty \<open>toplevel\<close>, or \<open>theory\<close>, or \<open>proof\<close>. The initial toplevel is empty; a theory is
- commenced by a @{command theory} header; within a theory we may use theory
- commands such as @{command definition}, or state a @{command theorem} to be
- proven. A proof state accepts a rich collection of Isar proof commands for
- structured proof composition, or unstructured proof scripts. When the proof
- is concluded we get back to the (local) theory, which is then updated by
- defining the resulting fact. Further theory declarations or theorem
- statements with proofs may follow, until we eventually conclude the theory
- development by issuing @{command end} to get back to the empty toplevel.
+ The toplevel state is a disjoint sum of empty \<open>toplevel\<close>, or \<open>theory\<close>, or
+ \<open>proof\<close>. The initial toplevel is empty; a theory is commenced by a @{command
+ theory} header; within a theory we may use theory commands such as @{command
+ definition}, or state a @{command theorem} to be proven. A proof state
+ accepts a rich collection of Isar proof commands for structured proof
+ composition, or unstructured proof scripts. When the proof is concluded we
+ get back to the (local) theory, which is then updated by defining the
+ resulting fact. Further theory declarations or theorem statements with
+ proofs may follow, until we eventually conclude the theory development by
+ issuing @{command end} to get back to the empty toplevel.
\<close>
text %mlref \<open>
@@ -43,23 +44,21 @@
@{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
\end{mldecls}
- \<^descr> Type @{ML_type Toplevel.state} represents Isar toplevel
- states, which are normally manipulated through the concept of
- toplevel transitions only (\secref{sec:toplevel-transition}).
+ \<^descr> Type @{ML_type Toplevel.state} represents Isar toplevel states, which are
+ normally manipulated through the concept of toplevel transitions only
+ (\secref{sec:toplevel-transition}).
- \<^descr> @{ML Toplevel.UNDEF} is raised for undefined toplevel
- operations. Many operations work only partially for certain cases,
- since @{ML_type Toplevel.state} is a sum type.
+ \<^descr> @{ML Toplevel.UNDEF} is raised for undefined toplevel operations. Many
+ operations work only partially for certain cases, since @{ML_type
+ Toplevel.state} is a sum type.
- \<^descr> @{ML Toplevel.is_toplevel}~\<open>state\<close> checks for an empty
- toplevel state.
+ \<^descr> @{ML Toplevel.is_toplevel}~\<open>state\<close> checks for an empty toplevel state.
- \<^descr> @{ML Toplevel.theory_of}~\<open>state\<close> selects the
- background theory of \<open>state\<close>, it raises @{ML Toplevel.UNDEF}
- for an empty toplevel state.
+ \<^descr> @{ML Toplevel.theory_of}~\<open>state\<close> selects the background theory of \<open>state\<close>,
+ it raises @{ML Toplevel.UNDEF} for an empty toplevel state.
- \<^descr> @{ML Toplevel.proof_of}~\<open>state\<close> selects the Isar proof
- state if available, otherwise it raises an error.
+ \<^descr> @{ML Toplevel.proof_of}~\<open>state\<close> selects the Isar proof state if available,
+ otherwise it raises an error.
\<close>
text %mlantiq \<open>
@@ -67,11 +66,11 @@
@{ML_antiquotation_def "Isar.state"} & : & \<open>ML_antiquotation\<close> \\
\end{matharray}
- \<^descr> \<open>@{Isar.state}\<close> refers to Isar toplevel state at that
- point --- as abstract value.
+ \<^descr> \<open>@{Isar.state}\<close> refers to Isar toplevel state at that point --- as
+ abstract value.
- This only works for diagnostic ML commands, such as @{command
- ML_val} or @{command ML_command}.
+ This only works for diagnostic ML commands, such as @{command ML_val} or
+ @{command ML_command}.
\<close>
@@ -82,12 +81,11 @@
state, with additional information for diagnostics and error reporting:
there are fields for command name, source position, and other meta-data.
- The operational part is represented as the sequential union of a
- list of partial functions, which are tried in turn until the first
- one succeeds. This acts like an outer case-expression for various
- alternative state transitions. For example, \isakeyword{qed} works
- differently for a local proofs vs.\ the global ending of an outermost
- proof.
+ The operational part is represented as the sequential union of a list of
+ partial functions, which are tried in turn until the first one succeeds.
+ This acts like an outer case-expression for various alternative state
+ transitions. For example, \isakeyword{qed} works differently for a local
+ proofs vs.\ the global ending of an outermost proof.
Transitions are composed via transition transformers. Internally, Isar
commands are put together from an empty transition extended by name and
@@ -112,34 +110,32 @@
Toplevel.transition -> Toplevel.transition"} \\
\end{mldecls}
- \<^descr> @{ML Toplevel.keep}~\<open>tr\<close> adjoins a diagnostic
- function.
+ \<^descr> @{ML Toplevel.keep}~\<open>tr\<close> adjoins a diagnostic function.
+
+ \<^descr> @{ML Toplevel.theory}~\<open>tr\<close> adjoins a theory transformer.
- \<^descr> @{ML Toplevel.theory}~\<open>tr\<close> adjoins a theory
- transformer.
+ \<^descr> @{ML Toplevel.theory_to_proof}~\<open>tr\<close> adjoins a global goal function, which
+ turns a theory into a proof state. The theory may be changed before entering
+ the proof; the generic Isar goal setup includes an \<^verbatim>\<open>after_qed\<close> argument
+ that specifies how to apply the proven result to the enclosing context, when
+ the proof is finished.
- \<^descr> @{ML Toplevel.theory_to_proof}~\<open>tr\<close> adjoins a global
- goal function, which turns a theory into a proof state. The theory
- may be changed before entering the proof; the generic Isar goal
- setup includes an \<^verbatim>\<open>after_qed\<close> argument that specifies how to
- apply the proven result to the enclosing context, when the proof
- is finished.
+ \<^descr> @{ML Toplevel.proof}~\<open>tr\<close> adjoins a deterministic proof command, with a
+ singleton result.
- \<^descr> @{ML Toplevel.proof}~\<open>tr\<close> adjoins a deterministic
- proof command, with a singleton result.
+ \<^descr> @{ML Toplevel.proofs}~\<open>tr\<close> adjoins a general proof command, with zero or
+ more result states (represented as a lazy list).
- \<^descr> @{ML Toplevel.proofs}~\<open>tr\<close> adjoins a general proof
- command, with zero or more result states (represented as a lazy
- list).
-
- \<^descr> @{ML Toplevel.end_proof}~\<open>tr\<close> adjoins a concluding
- proof command, that returns the resulting theory, after applying the
- resulting facts to the target context.
+ \<^descr> @{ML Toplevel.end_proof}~\<open>tr\<close> adjoins a concluding proof command, that
+ returns the resulting theory, after applying the resulting facts to the
+ target context.
\<close>
-text %mlex \<open>The file @{"file" "~~/src/HOL/ex/Commands.thy"} shows some example
-Isar command definitions, with the all-important theory header declarations
-for outer syntax keywords.\<close>
+text %mlex \<open>
+ The file @{"file" "~~/src/HOL/ex/Commands.thy"} shows some example Isar
+ command definitions, with the all-important theory header declarations for
+ outer syntax keywords.
+\<close>
section \<open>Theory loader database\<close>
@@ -149,8 +145,8 @@
a collection of theories as a directed acyclic graph. A theory may refer to
other theories as @{keyword "imports"}, or to auxiliary files via special
\<^emph>\<open>load commands\<close> (e.g.\ @{command ML_file}). For each theory, the base
- directory of its own theory file is called \<^emph>\<open>master directory\<close>: this is
- used as the relative location to refer to other files from that theory.
+ directory of its own theory file is called \<^emph>\<open>master directory\<close>: this is used
+ as the relative location to refer to other files from that theory.
\<close>
text %mlref \<open>
@@ -162,28 +158,27 @@
@{index_ML Thy_Info.register_thy: "theory -> unit"} \\
\end{mldecls}
- \<^descr> @{ML use_thy}~\<open>A\<close> ensures that theory \<open>A\<close> is fully
- up-to-date wrt.\ the external file store; outdated ancestors are reloaded on
- demand.
+ \<^descr> @{ML use_thy}~\<open>A\<close> ensures that theory \<open>A\<close> is fully up-to-date wrt.\ the
+ external file store; outdated ancestors are reloaded on demand.
- \<^descr> @{ML use_thys} is similar to @{ML use_thy}, but handles several
- theories simultaneously. Thus it acts like processing the import header of a
- theory, without performing the merge of the result. By loading a whole
- sub-graph of theories, the intrinsic parallelism can be exploited by the
- system to speedup loading.
+ \<^descr> @{ML use_thys} is similar to @{ML use_thy}, but handles several theories
+ simultaneously. Thus it acts like processing the import header of a theory,
+ without performing the merge of the result. By loading a whole sub-graph of
+ theories, the intrinsic parallelism can be exploited by the system to
+ speedup loading.
This variant is used by default in @{tool build} @{cite "isabelle-system"}.
- \<^descr> @{ML Thy_Info.get_theory}~\<open>A\<close> retrieves the theory value
- presently associated with name \<open>A\<close>. Note that the result might be
- outdated wrt.\ the file-system content.
+ \<^descr> @{ML Thy_Info.get_theory}~\<open>A\<close> retrieves the theory value presently
+ associated with name \<open>A\<close>. Note that the result might be outdated wrt.\ the
+ file-system content.
- \<^descr> @{ML Thy_Info.remove_thy}~\<open>A\<close> deletes theory \<open>A\<close> and all
- descendants from the theory database.
+ \<^descr> @{ML Thy_Info.remove_thy}~\<open>A\<close> deletes theory \<open>A\<close> and all descendants from
+ the theory database.
- \<^descr> @{ML Thy_Info.register_thy}~\<open>text thy\<close> registers an existing
- theory value with the theory loader database and updates source version
- information according to the file store.
+ \<^descr> @{ML Thy_Info.register_thy}~\<open>text thy\<close> registers an existing theory value
+ with the theory loader database and updates source version information
+ according to the file store.
\<close>
end