src/Doc/Implementation/Integration.thy

clarified "axiomatization" -- minor rewording of this delicate concept;

(*:wrap=hard:maxLineLen=78:*)

theory Integration
imports Base
begin

chapter {* System integration *}

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.
  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 sequentially
  one-by-one. In contemporary Isabelle/Isar, processing toplevel commands
  usually works in parallel in multi-threaded Isabelle/ML.
*}


subsection {* Toplevel state *}

text {*
  The toplevel state is a disjoint sum of empty @{text toplevel}, or @{text
  theory}, or @{text 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 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 {*
  \begin{mldecls}
  @{index_ML_type Toplevel.state} \\
  @{index_ML_exception Toplevel.UNDEF} \\
  @{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\
  @{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\
  @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
  @{index_ML Toplevel.timing: "bool Unsynchronized.ref"} \\
  @{index_ML Toplevel.profiling: "int Unsynchronized.ref"} \\
  \end{mldecls}

  \begin{description}

  \item Type @{ML_type Toplevel.state} represents Isar toplevel
  states, which are normally manipulated through the concept of
  toplevel transitions only (\secref{sec:toplevel-transition}).

  \item @{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.

  \item @{ML Toplevel.is_toplevel}~@{text "state"} checks for an empty
  toplevel state.

  \item @{ML Toplevel.theory_of}~@{text "state"} selects the
  background theory of @{text "state"}, raises @{ML Toplevel.UNDEF}
  for an empty toplevel state.

  \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
  state if available, otherwise raises @{ML Toplevel.UNDEF}.

  \item @{ML "Toplevel.timing := true"} makes the toplevel print timing
  information for each Isar command being executed.

  \item @{ML Toplevel.profiling}~@{ML_text ":="}~@{text "n"} controls
  low-level profiling of the underlying ML runtime system.  For
  Poly/ML, @{text "n = 1"} means time and @{text "n = 2"} space
  profiling.

  \end{description}
*}

text %mlantiq {*
  \begin{matharray}{rcl}
  @{ML_antiquotation_def "Isar.state"} & : & @{text ML_antiquotation} \\
  \end{matharray}

  \begin{description}

  \item @{text "@{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}.

  \end{description}
*}


subsection {* Toplevel transitions \label{sec:toplevel-transition} *}

text {*
  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, 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 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.
*}

text %mlref {*
  \begin{mldecls}
  @{index_ML Toplevel.keep: "(Toplevel.state -> unit) ->
  Toplevel.transition -> Toplevel.transition"} \\
  @{index_ML Toplevel.theory: "(theory -> theory) ->
  Toplevel.transition -> Toplevel.transition"} \\
  @{index_ML Toplevel.theory_to_proof: "(theory -> Proof.state) ->
  Toplevel.transition -> Toplevel.transition"} \\
  @{index_ML Toplevel.proof: "(Proof.state -> Proof.state) ->
  Toplevel.transition -> Toplevel.transition"} \\
  @{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.result Seq.seq) ->
  Toplevel.transition -> Toplevel.transition"} \\
  @{index_ML Toplevel.end_proof: "(bool -> Proof.state -> Proof.context) ->
  Toplevel.transition -> Toplevel.transition"} \\
  \end{mldecls}

  \begin{description}

  \item @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic
  function.

  \item @{ML Toplevel.theory}~@{text "tr"} adjoins a theory
  transformer.

  \item @{ML Toplevel.theory_to_proof}~@{text "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.

  \item @{ML Toplevel.proof}~@{text "tr"} adjoins a deterministic
  proof command, with a singleton result.

  \item @{ML Toplevel.proofs}~@{text "tr"} adjoins a general proof
  command, with zero or more result states (represented as a lazy
  list).

  \item @{ML Toplevel.end_proof}~@{text "tr"} adjoins a concluding
  proof command, that returns the resulting theory, after storing the
  resulting facts in the context etc.

  \end{description}
*}


section {* Theory loader database *}

text {*
  In batch mode and within dumped logic images, the theory database maintains
  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.
*}

text %mlref {*
  \begin{mldecls}
  @{index_ML use_thy: "string -> unit"} \\
  @{index_ML use_thys: "string list -> unit"} \\
  @{index_ML Thy_Info.get_theory: "string -> theory"} \\
  @{index_ML Thy_Info.remove_thy: "string -> unit"} \\
  @{index_ML Thy_Info.register_thy: "theory -> unit"} \\
  \end{mldecls}

  \begin{description}

  \item @{ML use_thy}~@{text A} ensures that theory @{text A} is fully
  up-to-date wrt.\ the external file store, reloading outdated ancestors as
  required.

  \item @{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.

  \item @{ML Thy_Info.get_theory}~@{text A} retrieves the theory value
  presently associated with name @{text A}. Note that the result might be
  outdated wrt.\ the file-system content.

  \item @{ML Thy_Info.remove_thy}~@{text A} deletes theory @{text A} and all
  descendants from the theory database.

  \item @{ML Thy_Info.register_thy}~@{text "text thy"} registers an existing
  theory value with the theory loader database and updates source version
  information according to the current file-system state.

  \end{description}
*}

end