diff -r fb7756087101 -r 38b049cd3aad src/Doc/Implementation/Integration.thy --- 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 \Isar toplevel \label{sec:isar-toplevel}\ text \ - The Isar \<^emph>\toplevel state\ represents the outermost configuration that - is transformed by a sequence of transitions (commands) within a theory body. + The Isar \<^emph>\toplevel state\ 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 \Toplevel state\ text \ - The toplevel state is a disjoint sum of empty \toplevel\, or \theory\, or \proof\. 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 \toplevel\, or \theory\, or + \proof\. 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. \ text %mlref \ @@ -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}~\state\ checks for an empty - toplevel state. + \<^descr> @{ML Toplevel.is_toplevel}~\state\ checks for an empty toplevel state. - \<^descr> @{ML Toplevel.theory_of}~\state\ selects the - background theory of \state\, it raises @{ML Toplevel.UNDEF} - for an empty toplevel state. + \<^descr> @{ML Toplevel.theory_of}~\state\ selects the background theory of \state\, + it raises @{ML Toplevel.UNDEF} for an empty toplevel state. - \<^descr> @{ML Toplevel.proof_of}~\state\ selects the Isar proof - state if available, otherwise it raises an error. + \<^descr> @{ML Toplevel.proof_of}~\state\ selects the Isar proof state if available, + otherwise it raises an error. \ text %mlantiq \ @@ -67,11 +66,11 @@ @{ML_antiquotation_def "Isar.state"} & : & \ML_antiquotation\ \\ \end{matharray} - \<^descr> \@{Isar.state}\ refers to Isar toplevel state at that - point --- as abstract value. + \<^descr> \@{Isar.state}\ 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}. \ @@ -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}~\tr\ adjoins a diagnostic - function. + \<^descr> @{ML Toplevel.keep}~\tr\ adjoins a diagnostic function. + + \<^descr> @{ML Toplevel.theory}~\tr\ adjoins a theory transformer. - \<^descr> @{ML Toplevel.theory}~\tr\ adjoins a theory - transformer. + \<^descr> @{ML Toplevel.theory_to_proof}~\tr\ 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>\after_qed\ argument + that specifies how to apply the proven result to the enclosing context, when + the proof is finished. - \<^descr> @{ML Toplevel.theory_to_proof}~\tr\ 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>\after_qed\ argument that specifies how to - apply the proven result to the enclosing context, when the proof - is finished. + \<^descr> @{ML Toplevel.proof}~\tr\ adjoins a deterministic proof command, with a + singleton result. - \<^descr> @{ML Toplevel.proof}~\tr\ adjoins a deterministic - proof command, with a singleton result. + \<^descr> @{ML Toplevel.proofs}~\tr\ adjoins a general proof command, with zero or + more result states (represented as a lazy list). - \<^descr> @{ML Toplevel.proofs}~\tr\ adjoins a general proof - command, with zero or more result states (represented as a lazy - list). - - \<^descr> @{ML Toplevel.end_proof}~\tr\ adjoins a concluding - proof command, that returns the resulting theory, after applying the - resulting facts to the target context. + \<^descr> @{ML Toplevel.end_proof}~\tr\ adjoins a concluding proof command, that + returns the resulting theory, after applying the resulting facts to the + target context. \ -text %mlex \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.\ +text %mlex \ + 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. +\ section \Theory loader database\ @@ -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>\load commands\ (e.g.\ @{command ML_file}). For each theory, the base - directory of its own theory file is called \<^emph>\master directory\: this is - used as the relative location to refer to other files from that theory. + directory of its own theory file is called \<^emph>\master directory\: this is used + as the relative location to refer to other files from that theory. \ text %mlref \ @@ -162,28 +158,27 @@ @{index_ML Thy_Info.register_thy: "theory -> unit"} \\ \end{mldecls} - \<^descr> @{ML use_thy}~\A\ ensures that theory \A\ is fully - up-to-date wrt.\ the external file store; outdated ancestors are reloaded on - demand. + \<^descr> @{ML use_thy}~\A\ ensures that theory \A\ 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}~\A\ retrieves the theory value - presently associated with name \A\. Note that the result might be - outdated wrt.\ the file-system content. + \<^descr> @{ML Thy_Info.get_theory}~\A\ retrieves the theory value presently + associated with name \A\. Note that the result might be outdated wrt.\ the + file-system content. - \<^descr> @{ML Thy_Info.remove_thy}~\A\ deletes theory \A\ and all - descendants from the theory database. + \<^descr> @{ML Thy_Info.remove_thy}~\A\ deletes theory \A\ and all descendants from + the theory database. - \<^descr> @{ML Thy_Info.register_thy}~\text thy\ 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}~\text thy\ registers an existing theory value + with the theory loader database and updates source version information + according to the file store. \ end