
diff -r e7418f8d49fe -r d468d72a458f doc-src/IsarImplementation/Thy/document/Integration.tex
--- a/doc-src/IsarImplementation/Thy/document/Integration.tex	Mon Aug 27 16:48:41 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,399 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Integration}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ Integration\isanewline
-\isakeyword{imports}\ Base\isanewline
-\isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isamarkupchapter{System integration%
-}
-\isamarkuptrue%
-%
-\isamarkupsection{Isar toplevel \label{sec:isar-toplevel}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The Isar toplevel may be considered the centeral hub of the
-  Isabelle/Isar system, where all key components and sub-systems are
-  integrated into a single read-eval-print loop of Isar commands,
-  which also incorporates the underlying ML compiler.
-
-  Isabelle/Isar departs from the original ``LCF system architecture''
-  where ML was really The Meta Language for defining theories and
-  conducting proofs.  Instead, ML now only serves as the
-  implementation language for the system (and user extensions), while
-  the specific Isar toplevel supports the concepts of theory and proof
-  development natively.  This includes the graph structure of theories
-  and the block structure of proofs, support for unlimited undo,
-  facilities for tracing, debugging, timing, profiling etc.
-
-  \medskip The toplevel maintains an implicit state, which is
-  transformed by a sequence of transitions -- either interactively or
-  in batch-mode.  In interactive mode, Isar state transitions are
-  encapsulated as safe transactions, such that both failure and undo
-  are handled conveniently without destroying the underlying draft
-  theory (cf.~\secref{sec:context-theory}).  In batch mode,
-  transitions operate in a linear (destructive) fashion, such that
-  error conditions abort the present attempt to construct a theory or
-  proof altogether.
-
-  The toplevel state is a disjoint sum of empty \isa{toplevel}, or
-  \isa{theory}, or \isa{proof}.  On entering the main Isar loop we
-  start with an empty toplevel.  A theory is commenced by giving a
-  \isa{{\isaliteral{5C3C5448454F52593E}{\isasymTHEORY}}} header; within a theory we may issue theory
-  commands such as \isa{{\isaliteral{5C3C444546494E4954494F4E3E}{\isasymDEFINITION}}}, or state a \isa{{\isaliteral{5C3C5448454F52454D3E}{\isasymTHEOREM}}} to be proven.  Now we are within a proof state, with 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 theory, which is then updated by
-  storing the resulting fact.  Further theory declarations or theorem
-  statements with proofs may follow, until we eventually conclude the
-  theory development by issuing \isa{{\isaliteral{5C3C454E443E}{\isasymEND}}}.  The resulting theory
-  is then stored within the theory database and we are back to the
-  empty toplevel.
-
-  In addition to these proper state transformations, there are also
-  some diagnostic commands for peeking at the toplevel state without
-  modifying it (e.g.\ \isakeyword{thm}, \isakeyword{term},
-  \isakeyword{print-cases}).%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
-  \indexdef{}{ML type}{Toplevel.state}\verb|type Toplevel.state| \\
-  \indexdef{}{ML}{Toplevel.UNDEF}\verb|Toplevel.UNDEF: exn| \\
-  \indexdef{}{ML}{Toplevel.is\_toplevel}\verb|Toplevel.is_toplevel: Toplevel.state -> bool| \\
-  \indexdef{}{ML}{Toplevel.theory\_of}\verb|Toplevel.theory_of: Toplevel.state -> theory| \\
-  \indexdef{}{ML}{Toplevel.proof\_of}\verb|Toplevel.proof_of: Toplevel.state -> Proof.state| \\
-  \indexdef{}{ML}{Toplevel.debug}\verb|Toplevel.debug: bool Unsynchronized.ref| \\
-  \indexdef{}{ML}{Toplevel.timing}\verb|Toplevel.timing: bool Unsynchronized.ref| \\
-  \indexdef{}{ML}{Toplevel.profiling}\verb|Toplevel.profiling: int Unsynchronized.ref| \\
-  \end{mldecls}
-
-  \begin{description}
-
-  \item Type \verb|Toplevel.state| represents Isar toplevel
-  states, which are normally manipulated through the concept of
-  toplevel transitions only (\secref{sec:toplevel-transition}).  Also
-  note that a raw toplevel state is subject to the same linearity
-  restrictions as a theory context (cf.~\secref{sec:context-theory}).
-
-  \item \verb|Toplevel.UNDEF| is raised for undefined toplevel
-  operations.  Many operations work only partially for certain cases,
-  since \verb|Toplevel.state| is a sum type.
-
-  \item \verb|Toplevel.is_toplevel|~\isa{state} checks for an empty
-  toplevel state.
-
-  \item \verb|Toplevel.theory_of|~\isa{state} selects the
-  background theory of \isa{state}, raises \verb|Toplevel.UNDEF|
-  for an empty toplevel state.
-
-  \item \verb|Toplevel.proof_of|~\isa{state} selects the Isar proof
-  state if available, otherwise raises \verb|Toplevel.UNDEF|.
-
-  \item \verb|Toplevel.debug := true| makes the toplevel print further
-  details about internal error conditions, exceptions being raised
-  etc.
-
-  \item \verb|Toplevel.timing := true| makes the toplevel print timing
-  information for each Isar command being executed.
-
-  \item \verb|Toplevel.profiling|~\verb|:=|~\isa{n} controls
-  low-level profiling of the underlying ML runtime system.  For
-  Poly/ML, \isa{n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}} means time and \isa{n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}} space
-  profiling.
-
-  \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isadelimmlantiq
-%
-\endisadelimmlantiq
-%
-\isatagmlantiq
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
-  \indexdef{}{ML antiquotation}{Isar.state}\hypertarget{ML antiquotation.Isar.state}{\hyperlink{ML antiquotation.Isar.state}{\mbox{\isa{Isar{\isaliteral{2E}{\isachardot}}state}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\
-  \end{matharray}
-
-  \begin{description}
-
-  \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}Isar{\isaliteral{2E}{\isachardot}}state{\isaliteral{7D}{\isacharbraceright}}} refers to Isar toplevel state at that
-  point --- as abstract value.
-
-  This only works for diagnostic ML commands, such as \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}}}} or \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}command}}}}.
-
-  \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlantiq
-{\isafoldmlantiq}%
-%
-\isadelimmlantiq
-%
-\endisadelimmlantiq
-%
-\isamarkupsubsection{Toplevel transitions \label{sec:toplevel-transition}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-An Isar toplevel transition consists of a partial function on the
-  toplevel state, with additional information for diagnostics and
-  error reporting: there are fields for command name, source position,
-  optional source text, as well as flags for interactive-only commands
-  (which issue a warning in batch-mode), printing of result state,
-  etc.
-
-  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 the main
-  proof.
-
-  Toplevel transitions are composed via transition transformers.
-  Internally, Isar commands are put together from an empty transition
-  extended by name and source position.  It is then left to the
-  individual command parser to turn the given concrete syntax into a
-  suitable transition transformer that adjoins actual operations on a
-  theory or proof state etc.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
-  \indexdef{}{ML}{Toplevel.print}\verb|Toplevel.print: Toplevel.transition -> Toplevel.transition| \\
-  \indexdef{}{ML}{Toplevel.no\_timing}\verb|Toplevel.no_timing: Toplevel.transition -> Toplevel.transition| \\
-  \indexdef{}{ML}{Toplevel.keep}\verb|Toplevel.keep: (Toplevel.state -> unit) ->|\isasep\isanewline%
-\verb|  Toplevel.transition -> Toplevel.transition| \\
-  \indexdef{}{ML}{Toplevel.theory}\verb|Toplevel.theory: (theory -> theory) ->|\isasep\isanewline%
-\verb|  Toplevel.transition -> Toplevel.transition| \\
-  \indexdef{}{ML}{Toplevel.theory\_to\_proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
-\verb|  Toplevel.transition -> Toplevel.transition| \\
-  \indexdef{}{ML}{Toplevel.proof}\verb|Toplevel.proof: (Proof.state -> Proof.state) ->|\isasep\isanewline%
-\verb|  Toplevel.transition -> Toplevel.transition| \\
-  \indexdef{}{ML}{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline%
-\verb|  Toplevel.transition -> Toplevel.transition| \\
-  \indexdef{}{ML}{Toplevel.end\_proof}\verb|Toplevel.end_proof: (bool -> Proof.state -> Proof.context) ->|\isasep\isanewline%
-\verb|  Toplevel.transition -> Toplevel.transition| \\
-  \end{mldecls}
-
-  \begin{description}
-
-  \item \verb|Toplevel.print|~\isa{tr} sets the print flag, which
-  causes the toplevel loop to echo the result state (in interactive
-  mode).
-
-  \item \verb|Toplevel.no_timing|~\isa{tr} indicates that the
-  transition should never show timing information, e.g.\ because it is
-  a diagnostic command.
-
-  \item \verb|Toplevel.keep|~\isa{tr} adjoins a diagnostic
-  function.
-
-  \item \verb|Toplevel.theory|~\isa{tr} adjoins a theory
-  transformer.
-
-  \item \verb|Toplevel.theory_to_proof|~\isa{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 argument that specifies how to apply the proven
-  result to the theory, when the proof is finished.
-
-  \item \verb|Toplevel.proof|~\isa{tr} adjoins a deterministic
-  proof command, with a singleton result.
-
-  \item \verb|Toplevel.proofs|~\isa{tr} adjoins a general proof
-  command, with zero or more result states (represented as a lazy
-  list).
-
-  \item \verb|Toplevel.end_proof|~\isa{tr} adjoins a concluding
-  proof command, that returns the resulting theory, after storing the
-  resulting facts in the context etc.
-
-  \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isamarkupsection{Theory database \label{sec:theory-database}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The theory database maintains a collection of theories, together
-  with some administrative information about their original sources,
-  which are held in an external store (i.e.\ some directory within the
-  regular file system).
-
-  The theory database is organized as a directed acyclic graph;
-  entries are referenced by theory name.  Although some additional
-  interfaces allow to include a directory specification as well, this
-  is only a hint to the underlying theory loader.  The internal theory
-  name space is flat!
-
-  Theory \isa{A} is associated with the main theory file \isa{A}\verb,.thy,, which needs to be accessible through the theory
-  loader path.  Any number of additional ML source files may be
-  associated with each theory, by declaring these dependencies in the
-  theory header as \isa{{\isaliteral{5C3C555345533E}{\isasymUSES}}}, and loading them consecutively
-  within the theory context.  The system keeps track of incoming ML
-  sources and associates them with the current theory.
-
-  The basic internal actions of the theory database are \isa{update} and \isa{remove}:
-
-  \begin{itemize}
-
-  \item \isa{update\ A} introduces a link of \isa{A} with a
-  \isa{theory} value of the same name; it asserts that the theory
-  sources are now consistent with that value;
-
-  \item \isa{remove\ A} deletes entry \isa{A} from the theory
-  database.
-  
-  \end{itemize}
-
-  These actions are propagated to sub- or super-graphs of a theory
-  entry as expected, in order to preserve global consistency of the
-  state of all loaded theories with the sources of the external store.
-  This implies certain causalities between actions: \isa{update}
-  or \isa{remove} of an entry will \isa{remove} all
-  descendants.
-
-  \medskip There are separate user-level interfaces to operate on the
-  theory database directly or indirectly.  The primitive actions then
-  just happen automatically while working with the system.  In
-  particular, processing a theory header \isa{{\isaliteral{5C3C5448454F52593E}{\isasymTHEORY}}\ A\ {\isaliteral{5C3C494D504F5254533E}{\isasymIMPORTS}}\ B\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C424547494E3E}{\isasymBEGIN}}} ensures that the
-  sub-graph of the collective imports \isa{B\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E7375623E}{}\isactrlsub n}
-  is up-to-date, too.  Earlier theories are reloaded as required, with
-  \isa{update} actions proceeding in topological order according to
-  theory dependencies.  There may be also a wave of implied \isa{remove} actions for derived theory nodes until a stable situation
-  is achieved eventually.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
-  \indexdef{}{ML}{use\_thy}\verb|use_thy: string -> unit| \\
-  \indexdef{}{ML}{use\_thys}\verb|use_thys: string list -> unit| \\
-  \indexdef{}{ML}{Thy\_Info.get\_theory}\verb|Thy_Info.get_theory: string -> theory| \\
-  \indexdef{}{ML}{Thy\_Info.remove\_thy}\verb|Thy_Info.remove_thy: string -> unit| \\[1ex]
-  \indexdef{}{ML}{Thy\_Info.register\_thy}\verb|Thy_Info.register_thy: theory -> unit| \\[1ex]
-  \verb|datatype action = Update |\verb,|,\verb| Remove| \\
-  \indexdef{}{ML}{Thy\_Info.add\_hook}\verb|Thy_Info.add_hook: (Thy_Info.action -> string -> unit) -> unit| \\
-  \end{mldecls}
-
-  \begin{description}
-
-  \item \verb|use_thy|~\isa{A} ensures that theory \isa{A} is fully
-  up-to-date wrt.\ the external file store, reloading outdated
-  ancestors as required.  In batch mode, the simultaneous \verb|use_thys| should be used exclusively.
-
-  \item \verb|use_thys| is similar to \verb|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 like that, the
-  intrinsic parallelism can be exploited by the system, to speedup
-  loading.
-
-  \item \verb|Thy_Info.get_theory|~\isa{A} retrieves the theory value
-  presently associated with name \isa{A}.  Note that the result
-  might be outdated.
-
-  \item \verb|Thy_Info.remove_thy|~\isa{A} deletes theory \isa{A} and all
-  descendants from the theory database.
-
-  \item \verb|Thy_Info.register_thy|~\isa{text\ thy} registers an
-  existing theory value with the theory loader database and updates
-  source version information according to the current file-system
-  state.
-
-  \item \verb|Thy_Info.add_hook|~\isa{f} registers function \isa{f} as a hook for theory database actions.  The function will be
-  invoked with the action and theory name being involved; thus derived
-  actions may be performed in associated system components, e.g.\
-  maintaining the state of an editor for the theory sources.
-
-  The kind and order of actions occurring in practice depends both on
-  user interactions and the internal process of resolving theory
-  imports.  Hooks should not rely on a particular policy here!  Any
-  exceptions raised by the hook are ignored.
-
-  \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:




