doc-src/IsarImplementation/Thy/Integration.thy

replaced Thm.legacy_freezeT by Thm.unvarify_global -- these facts stem from closed definitions, i.e. there are no term Vars;

theory Integration
imports Base
begin

chapter {* System integration *}

section {* Isar toplevel \label{sec:isar-toplevel} *}

text {* 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.  We
  shall even incorporate the existing {\ML} toplevel of the compiler
  and run-time system (cf.\ \secref{sec:ML-toplevel}).

  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 @{text toplevel}, or
  @{text theory}, or @{text proof}.  On entering the main Isar loop we
  start with an empty toplevel.  A theory is commenced by giving a
  @{text \<THEORY>} header; within a theory we may issue theory
  commands such as @{text \<DEFINITION>}, or state a @{text
  \<THEOREM>} 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 @{text \<END>}.  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}).
*}

text %mlref {*
  \begin{mldecls}
  @{index_ML_type Toplevel.state} \\
  @{index_ML Toplevel.UNDEF: "exn"} \\
  @{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.debug: "bool Unsynchronized.ref"} \\
  @{index_ML Toplevel.timing: "bool Unsynchronized.ref"} \\
  @{index_ML Toplevel.profiling: "int Unsynchronized.ref"} \\
  \end{mldecls}

  \begin{description}

  \item @{ML_type 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 @{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.debug := true"} makes the toplevel print further
  details about internal error conditions, exceptions being raised
  etc.

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

  \item @{ML Toplevel.profiling}~@{verbatim ":="}~@{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}
*}


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

text %mlref {*
  \begin{mldecls}
  @{index_ML Toplevel.print: "Toplevel.transition -> Toplevel.transition"} \\
  @{index_ML Toplevel.no_timing: "Toplevel.transition -> Toplevel.transition"} \\
  @{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.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.print}~@{text "tr"} sets the print flag, which
  causes the toplevel loop to echo the result state (in interactive
  mode).

  \item @{ML Toplevel.no_timing}~@{text "tr"} indicates that the
  transition should never show timing information, e.g.\ because it is
  a diagnostic command.

  \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 argument that specifies how to apply the proven
  result to the theory, 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}
*}


subsection {* Toplevel control *}

text {*
  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 Proof~General.

  \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}
*}


section {* ML toplevel \label{sec:ML-toplevel} *}

text {*
  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 loaded from 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 --- while
  observing the usual linearity restrictions
  (cf.~\secref{sec:context-theory}).
*}

text %mlref {*
  \begin{mldecls}
  @{index_ML ML_Context.the_generic_context: "unit -> Context.generic"} \\
  @{index_ML "Context.>> ": "(Context.generic -> Context.generic) -> unit"} \\
  \end{mldecls}

  \begin{description}

  \item @{ML "ML_Context.the_generic_context ()"} refers to the theory
  context of the {\ML} toplevel --- at compile time!  {\ML} code needs
  to take care to refer to @{ML "ML_Context.the_generic_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 @{ML_type theory_ref} (cf.\ \secref{sec:context-theory}).

  \item @{ML "Context.>>"}~@{text f} applies context transformation
  @{text f} to the implicit context of the {\ML} toplevel.

  \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 instead.  Thus it
  may be invoked for an arbitrary context later on, without having to
  worry about any operational details.

  \bigskip

  \begin{mldecls}
  @{index_ML Isar.main: "unit -> unit"} \\
  @{index_ML Isar.loop: "unit -> unit"} \\
  @{index_ML Isar.state: "unit -> Toplevel.state"} \\
  @{index_ML Isar.exn: "unit -> (exn * string) option"} \\
  @{index_ML Isar.context: "unit -> Proof.context"} \\
  @{index_ML Isar.goal: "unit ->
  {context: Proof.context, facts: thm list, goal: thm}"} \\
  \end{mldecls}

  \begin{description}

  \item @{ML "Isar.main ()"} invokes the Isar toplevel from {\ML},
  initializing an empty toplevel state.

  \item @{ML "Isar.loop ()"} continues the Isar toplevel with the
  current state, after having dropped out of the Isar toplevel loop.

  \item @{ML "Isar.state ()"} and @{ML "Isar.exn ()"} get current
  toplevel state and error condition, respectively.  This only works
  after having dropped out of the Isar toplevel loop.

  \item @{ML "Isar.context ()"} produces the proof context from @{ML
  "Isar.state ()"}, analogous to @{ML Context.proof_of}
  (\secref{sec:generic-context}).

  \item @{ML "Isar.goal ()"} produces the full Isar goal state,
  consisting of proof context, facts that have been indicated for
  immediate use, and the tactical goal according to
  \secref{sec:tactical-goals}.

  \end{description}
*}


section {* Theory database \label{sec:theory-database} *}

text {*
  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 @{text A} is associated with the main theory file @{text
  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 @{text \<USES>}, 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 @{text
  "update"}, @{text "outdate"}, and @{text "remove"}:

  \begin{itemize}

  \item @{text "update A"} introduces a link of @{text "A"} with a
  @{text "theory"} value of the same name; it asserts that the theory
  sources are now consistent with that value;

  \item @{text "outdate A"} invalidates the link of a theory database
  entry to its sources, but retains the present theory value;

  \item @{text "remove A"} deletes entry @{text "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: @{text "update"}
  or @{text "outdate"} of an entry will @{text "outdate"} all
  descendants; @{text "remove"} will @{text "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 @{text "\<THEORY> A
  \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"} ensures that the
  sub-graph of the collective imports @{text "B\<^sub>1 \<dots> B\<^sub>n"}
  is up-to-date, too.  Earlier theories are reloaded as required, with
  @{text update} actions proceeding in topological order according to
  theory dependencies.  There may be also a wave of implied @{text
  outdate} actions for derived theory nodes until a stable situation
  is achieved eventually.
*}

text %mlref {*
  \begin{mldecls}
  @{index_ML theory: "string -> theory"} \\
  @{index_ML use_thy: "string -> unit"} \\
  @{index_ML use_thys: "string list -> unit"} \\
  @{index_ML ThyInfo.touch_thy: "string -> unit"} \\
  @{index_ML ThyInfo.remove_thy: "string -> unit"} \\[1ex]
  @{index_ML ThyInfo.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
  @{index_ML ThyInfo.end_theory: "theory -> unit"} \\
  @{index_ML ThyInfo.register_theory: "theory -> unit"} \\[1ex]
  @{verbatim "datatype action = Update | Outdate | Remove"} \\
  @{index_ML ThyInfo.add_hook: "(ThyInfo.action -> string -> unit) -> unit"} \\
  \end{mldecls}

  \begin{description}

  \item @{ML theory}~@{text A} retrieves the theory value presently
  associated with name @{text A}.  Note that the result might be
  outdated.

  \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.  In batch mode, the simultaneous @{ML
  use_thys} should be used exclusively.

  \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 like that, the
  intrinsic parallelism can be exploited by the system, to speedup
  loading.

  \item @{ML ThyInfo.touch_thy}~@{text A} performs and @{text outdate} action
  on theory @{text A} and all descendants.

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

  \item @{ML ThyInfo.begin_theory} is the basic operation behind a
  @{text \<THEORY>} header declaration.  This {\ML} function is
  normally not invoked directly.

  \item @{ML ThyInfo.end_theory} concludes the loading of a theory
  proper and stores the result in the theory database.

  \item @{ML ThyInfo.register_theory}~@{text "text thy"} registers an
  existing theory value with the theory loader database.  There is no
  management of associated sources.

  \item @{ML "ThyInfo.add_hook"}~@{text f} registers function @{text
  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