doc-src/IsarImplementation/Thy/document/integration.tex

Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure".
This simplifies some proofs.

%
\begin{isabellebody}%
\def\isabellecontext{integration}%
%
\isadelimtheory
\isanewline
\isanewline
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ integration\ \isakeyword{imports}\ base\ \isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupchapter{System integration%
}
\isamarkuptrue%
%
\isamarkupsection{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.
  Here we even incorporate the existing {\ML} toplevel of the compiler
  and run-time system (cf.\ \secref{sec:ML-toplevel}).

  Isabelle/Isar departs from original ``LCF system architecture''
  where {\ML} was really The Meta Language for defining theories and
  conducting proofs.  Instead, {\ML} merely serves as the
  implementation language for the system (and user extensions), while
  our specific Isar toplevel supports particular notions of
  incremental theory and proof development more directly.  This
  includes the graph structure of theories and the block structure of
  proofs, support for unlimited undo, facilities for tracing,
  debugging, timing, profiling.

  \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 strictly linear (destructive) fashion, such
  that error conditions abort the present attempt to construct a
  theory 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{{\isasymTHEORY}} header; within a theory we may issue theory
  commands such as \isa{{\isasymCONSTS}} or \isa{{\isasymDEFS}}, or state a
  \isa{{\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{{\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}
  \indexmltype{Toplevel.state}\verb|type Toplevel.state| \\
  \indexml{Toplevel.UNDEF}\verb|Toplevel.UNDEF: exn| \\
  \indexml{Toplevel.is-toplevel}\verb|Toplevel.is_toplevel: Toplevel.state -> bool| \\
  \indexml{Toplevel.theory-of}\verb|Toplevel.theory_of: Toplevel.state -> theory| \\
  \indexml{Toplevel.proof-of}\verb|Toplevel.proof_of: Toplevel.state -> Proof.state| \\
  \indexml{Toplevel.debug}\verb|Toplevel.debug: bool ref| \\
  \indexml{Toplevel.timing}\verb|Toplevel.timing: bool ref| \\
  \indexml{Toplevel.profiling}\verb|Toplevel.profiling: int ref| \\
  \end{mldecls}

  \begin{description}

  \item \verb|Toplevel.state| represents Isar toplevel states,
  which are normally only manipulated through the toplevel transition
  concept (\secref{sec:toplevel-transition}).  Also note that a
  toplevel state is subject to the same linerarity restrictions as a
  theory context (cf.~\secref{sec:context-theory}).

  \item \verb|Toplevel.UNDEF| is raised for undefined toplevel
  operations: \verb|Toplevel.state| is a sum type, many operations
  work only partially for certain cases.

  \item \verb|Toplevel.is_toplevel| checks for an empty toplevel state.

  \item \verb|Toplevel.theory_of| gets the theory of a theory or proof
  (!), otherwise raises \verb|Toplevel.UNDEF|.

  \item \verb|Toplevel.proof_of| gets the Isar proof state if
  available, otherwise raises \verb|Toplevel.UNDEF|.

  \item \verb|set Toplevel.debug| makes the toplevel print further
  details about internal error conditions, exceptions being raised
  etc.

  \item \verb|set Toplevel.timing| makes the toplevel print timing
  information for each Isar command being executed.

  \item \verb|Toplevel.profiling| controls low-level profiling of the
  underlying {\ML} runtime system.\footnote{For Poly/ML, 1 means time
  and 2 space profiling.}

  \end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsubsection{Toplevel transitions%
}
\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 a sequential union of a list
  of partial functions, which are tried in turn until the first one
  succeeds (i.e.\ does not raise \verb|Toplevel.UNDEF|).  For example,
  a single Isar command like \isacommand{qed} consists of the union of
  some function \verb|Proof.state -> Proof.state| for proofs
  within proofs, plus \verb|Proof.state -> theory| for proofs at
  the outer theory level.

  Toplevel transitions are composed via transition transformers.
  Internally, Isar commands are put together from an empty transition
  extended by name and source position (and optional source text).  It
  is then left to the individual command parser to turn the given
  syntax body into a suitable transition transformer that adjoin
  actual operations on a theory or proof state etc.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
  \indexml{Toplevel.print}\verb|Toplevel.print: Toplevel.transition -> Toplevel.transition| \\
  \indexml{Toplevel.no-timing}\verb|Toplevel.no_timing: Toplevel.transition -> Toplevel.transition| \\
  \indexml{Toplevel.keep}\verb|Toplevel.keep: (Toplevel.state -> unit) ->|\isasep\isanewline%
\verb|  Toplevel.transition -> Toplevel.transition| \\
  \indexml{Toplevel.theory}\verb|Toplevel.theory: (theory -> theory) ->|\isasep\isanewline%
\verb|  Toplevel.transition -> Toplevel.transition| \\
  \indexml{Toplevel.theory-to-proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
\verb|  Toplevel.transition -> Toplevel.transition| \\
  \indexml{Toplevel.proof}\verb|Toplevel.proof: (Proof.state -> Proof.state) ->|\isasep\isanewline%
\verb|  Toplevel.transition -> Toplevel.transition| \\
  \indexml{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline%
\verb|  Toplevel.transition -> Toplevel.transition| \\
  \indexml{Toplevel.proof-to-theory}\verb|Toplevel.proof_to_theory: (Proof.state -> theory) ->|\isasep\isanewline%
\verb|  Toplevel.transition -> Toplevel.transition| \\
  \end{mldecls}

  \begin{description}

  \item \verb|Toplevel.print| sets the print flag, which causes the
  resulting state of the transition to be echoed in interactive mode.

  \item \verb|Toplevel.no_timing| indicates that the transition should
  never show timing information, e.g.\ because it is merely a
  diagnostic command.

  \item \verb|Toplevel.keep| adjoins a diagnostic function.

  \item \verb|Toplevel.theory| adjoins a theory transformer.

  \item \verb|Toplevel.theory_to_proof| 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| adjoins a deterministic proof command,
  with a singleton result state.

  \item \verb|Toplevel.proofs| adjoins a general proof command, with
  zero or more result states (represented as a lazy list).

  \item \verb|Toplevel.proof_to_theory| adjoins a concluding proof
  command, that returns the resulting theory, after storing the
  resulting facts etc.

  \end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsubsection{Toplevel control%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Apart from regular toplevel transactions there are a few
  special control commands that modify the behavior the toplevel
  itself, and only make sense in interactive mode.  Under normal
  circumstances, the user encounters these only implicitly as part of
  the protocol between the Isabelle/Isar system and a user-interface
  such as ProofGeneral.

  \begin{description}

  \item \isacommand{undo} follows the three-level hierarchy of empty
  toplevel vs.\ theory vs.\ proof: undo within a proof reverts to the
  previous proof context, undo after a proof reverts to the theory
  before the initial goal statement, undo of a theory command reverts
  to the previous theory value, undo of a theory header discontinues
  the current theory development and removes it from the theory
  database (\secref{sec:theory-database}).

  \item \isacommand{kill} aborts the current level of development:
  kill in a proof context reverts to the theory before the initial
  goal statement, kill in a theory context aborts the current theory
  development, removing it from the database.

  \item \isacommand{exit} drops out of the Isar toplevel into the
  underlying {\ML} toplevel (\secref{sec:ML-toplevel}).  The Isar
  toplevel state is preserved and may be continued later.

  \item \isacommand{quit} terminates the Isabelle/Isar process without
  saving.

  \end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{ML toplevel \label{sec:ML-toplevel}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The {\ML} toplevel provides a read-compile-eval-print loop for
  {\ML} values, types, structures, and functors.  {\ML} declarations
  operate on the global system state, which consists of the compiler
  environment plus the values of {\ML} reference variables.  There is
  no clean way to undo {\ML} declarations, except for reverting to a
  previously saved state of the whole Isabelle process.  {\ML} input
  is either read interactively from a TTY, or from a string (usually
  within a theory text), or from a source file (usually associated
  with a theory).

  Whenever the {\ML} toplevel is active, the current Isabelle theory
  context is passed as an internal reference variable.  Thus {\ML}
  code may access the theory context during compilation, it may even
  change the value of a theory being under construction --- following
  the usual linearity restrictions (cf.~\secref{sec:context-theory}).%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
  \indexml{context}\verb|context: theory -> unit| \\
  \indexml{the-context}\verb|the_context: unit -> theory| \\
  \indexml{Context.$>$$>$ }\verb|Context.>> : (theory -> theory) -> unit| \\
  \end{mldecls}

  \begin{description}

  \item \verb|context|~\isa{thy} sets the {\ML} theory context to
  \isa{thy}.  This is usually performed automatically by the system,
  when dropping out of the interactive Isar toplevel into {\ML}, or
  when Isar invokes {\ML} to process code from a string or a file.

  \item \verb|the_context ()| refers to the theory context of the
  {\ML} toplevel --- at compile time!  {\ML} code needs to take care
  to refer to \verb|the_context ()| correctly, recall that evaluation
  of a function body is delayed until actual runtime.  Moreover,
  persistent {\ML} toplevel bindings to an unfinished theory should be
  avoided: code should either project out the desired information
  immediately, or produce an explicit \verb|theory_ref| (cf.\
  \secref{sec:context-theory}).

  \item \verb|Context.>>|~\isa{f} applies theory transformation
  \isa{f} to the current theory of the {\ML} toplevel.  In order to
  work as expected, the theory should be still under construction, and
  the Isar language element that invoked the {\ML} compiler in the
  first place shoule be ready to accept the changed theory value
  (e.g.\ \isakeyword{ML-setup}, but not plain \isakeyword{ML}).
  Otherwise the theory may get destroyed!

  \end{description}

  It is very important to note that the above functions are really
  restricted to the compile time, even though the {\ML} compiler is
  invoked at runtime!  The majority of {\ML} code uses explicit
  functional arguments of a theory or proof context, as required.
  Thus it may get run in an arbitrary context later on.

  \bigskip

  \begin{mldecls}
  \indexml{Isar.main}\verb|Isar.main: unit -> unit| \\
  \indexml{Isar.loop}\verb|Isar.loop: unit -> unit| \\
  \indexml{Isar.state}\verb|Isar.state: unit -> Toplevel.state| \\
  \indexml{Isar.exn}\verb|Isar.exn: unit -> (exn * string) option| \\
  \end{mldecls}

  \begin{description}

  \item \verb|Isar.main ()| invokes the Isar toplevel from {\ML},
  initializing the state to empty toplevel state.

  \item \verb|Isar.loop ()| continues the Isar toplevel with the
  current state, after dropping out of the Isar toplevel loop.

  \item \verb|Isar.state ()| and \verb|Isar.exn ()| get current
  toplevel state and optional error condition, respectively.  This
  only works after dropping out of the Isar toplevel loop.

  \end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsection{Theory database%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The theory database maintains a collection of theories,
  together with some administrative information about the original
  sources, which are held in an external store (i.e.\ a collection of
  directories within the regular file system of the underlying
  platform).

  The theory database is organized as a directed acyclic graph, with
  entries referenced by theory name.  Although some external
  interfaces allow to include a directory specification, this is only
  a hint to the underlying theory loader mechanism: 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.  A number of optional {\ML} source files may be
  associated with each theory, by declaring these dependencies in the
  theory header as \isa{{\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 special
  theory {\ML} file \isa{A}\verb,.ML, is loaded after a theory has
  been concluded, in order to support legacy proof {\ML} proof
  scripts.

  The basic internal actions of the theory database are \isa{update}, \isa{outdate}, 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 consistent with that value.

  \item \isa{outdate\ A} invalidates the link of a theory database
  entry to its sources, but retains the present theory value.

  \item \isa{remove\ A} removes entry \isa{A} from the theory
  database.
  
  \end{itemize}

  These actions are propagated to sub- or super-graphs of a theory
  entry in the usual way, in order to preserve global consistency of
  the state of all loaded theories with the sources of the external
  store.  This implies causal dependencies of certain actions: \isa{update} or \isa{outdate} of an entry will \isa{outdate}
  all descendants; \isa{remove} 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{{\isasymTHEORY}\ A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}} ensure that the
  sub-graph of the collective imports \isa{B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n}
  is up-to-date.  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{outdate} actions for derived theory nodes until a stable situation
  is achieved eventually.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
  \indexml{theory}\verb|theory: string -> theory| \\
  \indexml{use-thy}\verb|use_thy: string -> unit| \\
  \indexml{update-thy}\verb|update_thy: string -> unit| \\
  \indexml{use-thy-only}\verb|use_thy_only: string -> unit| \\
  \indexml{update-thy-only}\verb|update_thy_only: string -> unit| \\
  \indexml{touch-thy}\verb|touch_thy: string -> unit| \\
  \indexml{remove-thy}\verb|remove_thy: string -> unit| \\[1ex]
  \indexml{ThyInfo.begin-theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
  \indexml{ThyInfo.end-theory}\verb|ThyInfo.end_theory: theory -> theory| \\
  \indexml{ThyInfo.register-theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]
  \verb|datatype action = Update |\verb,|,\verb| Outdate |\verb,|,\verb| Remove| \\
  \indexml{ThyInfo.add-hook}\verb|ThyInfo.add_hook: (ThyInfo.action -> string -> unit) -> unit| \\
  \end{mldecls}

  \begin{description}

  \item \verb|theory|~\isa{A} retrieves the theory value presently
  associated with \isa{A}.  The result is not necessarily
  up-to-date!

  \item \verb|use_thy|~\isa{A} loads theory \isa{A} if it is absent
  or out-of-date.  It ensures that all parent theories are available
  as well, but does not reload them if older versions are already
  present.

  \item \verb|update_thy| is similar to \verb|use_thy|, but ensures that
  the \isa{A} and all of its ancestors are fully up-to-date.

  \item \verb|use_thy_only|~\isa{A} is like \verb|use_thy|~\isa{A},
  but refrains from loading the attached \isa{A}\verb,.ML, file.
  This is occasionally useful in replaying legacy {\ML} proof scripts
  by hand.
  
  \item \verb|update_thy_only| is analogous to \verb|use_thy_only|, but
  proceeds like \verb|update_thy| for ancestors.

  \item \verb|touch_thy|~\isa{A} performs \isa{outdate} action on
  theory \isa{A} and all of its descendants.

  \item \verb|remove_thy|~\isa{A} removes \isa{A} and all of its
  descendants from the theory database.

  \item \verb|ThyInfo.begin_theory| is the basic operation behind a
  \isa{{\isasymTHEORY}} header declaration.  The boolean argument
  indicates the strictness of treating ancestors: for \verb|true| (as
  in interactive mode) like \verb|update_thy|, and for \verb|false| (as
  in batch mode) like \verb|use_thy|.  This is {\ML} functions is
  normally not invoked directly.

  \item \verb|ThyInfo.end_theory| concludes the loading of a theory
  proper; an attached theory {\ML} file may be still loaded later on.
  This is {\ML} functions is normally not invoked directly.

  \item \verb|ThyInfo.register_theory|~{text thy} registers an existing
  theory value with the theory loader database.  There is no
  management of associated sources; this is mainly for bootstrapping.

  \item \verb|ThyInfo.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 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 by the theory database.

  \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: