
diff -r e6d9e46ff7bc -r e7418f8d49fe doc-src/System/Thy/Basics.thy
--- a/doc-src/System/Thy/Basics.thy	Mon Aug 27 16:10:54 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,554 +0,0 @@
-theory Basics
-imports Base
-begin
-
-chapter {* The Isabelle system environment *}
-
-text {* This manual describes Isabelle together with related tools and
-  user interfaces as seen from a system oriented view.  See also the
-  \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} for
-  the actual Isabelle input language and related concepts, and
-  \emph{The Isabelle/Isar Implementation
-  Manual}~\cite{isabelle-implementation} for the main concepts of the
-  underlying implementation in Isabelle/ML.
-
-  \medskip The Isabelle system environment provides the following
-  basic infrastructure to integrate tools smoothly.
-
-  \begin{enumerate}
-
-  \item The \emph{Isabelle settings} mechanism provides process
-  environment variables to all Isabelle executables (including tools
-  and user interfaces).
-
-  \item The raw \emph{Isabelle process} (@{executable_ref
-  "isabelle-process"}) runs logic sessions either interactively or in
-  batch mode.  In particular, this view abstracts over the invocation
-  of the actual ML system to be used.  Regular users rarely need to
-  care about the low-level process.
-
-  \item The main \emph{Isabelle tool wrapper} (@{executable_ref
-  isabelle}) provides a generic startup environment Isabelle related
-  utilities, user interfaces etc.  Such tools automatically benefit
-  from the settings mechanism.
-
-  \end{enumerate}
-*}
-
-
-section {* Isabelle settings \label{sec:settings} *}
-
-text {*
-  The Isabelle system heavily depends on the \emph{settings
-  mechanism}\indexbold{settings}.  Essentially, this is a statically
-  scoped collection of environment variables, such as @{setting
-  ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting ML_HOME}.  These
-  variables are \emph{not} intended to be set directly from the shell,
-  though.  Isabelle employs a somewhat more sophisticated scheme of
-  \emph{settings files} --- one for site-wide defaults, another for
-  additional user-specific modifications.  With all configuration
-  variables in clearly defined places, this scheme is more
-  maintainable and user-friendly than global shell environment
-  variables.
-
-  In particular, we avoid the typical situation where prospective
-  users of a software package are told to put several things into
-  their shell startup scripts, before being able to actually run the
-  program. Isabelle requires none such administrative chores of its
-  end-users --- the executables can be invoked straight away.
-  Occasionally, users would still want to put the @{file
-  "$ISABELLE_HOME/bin"} directory into their shell's search path, but
-  this is not required.
-*}
-
-
-subsection {* Bootstrapping the environment \label{sec:boot} *}
-
-text {* Isabelle executables need to be run within a proper settings
-  environment.  This is bootstrapped as described below, on the first
-  invocation of one of the outer wrapper scripts (such as
-  @{executable_ref isabelle}).  This happens only once for each
-  process tree, i.e.\ the environment is passed to subprocesses
-  according to regular Unix conventions.
-
-  \begin{enumerate}
-
-  \item The special variable @{setting_def ISABELLE_HOME} is
-  determined automatically from the location of the binary that has
-  been run.
-  
-  You should not try to set @{setting ISABELLE_HOME} manually. Also
-  note that the Isabelle executables either have to be run from their
-  original location in the distribution directory, or via the
-  executable objects created by the @{tool install} tool.  Symbolic
-  links are admissible, but a plain copy of the @{file
-  "$ISABELLE_HOME/bin"} files will not work!
-
-  \item The file @{file "$ISABELLE_HOME/etc/settings"} is run as a
-  @{executable_ref bash} shell script with the auto-export option for
-  variables enabled.
-  
-  This file holds a rather long list of shell variable assigments,
-  thus providing the site-wide default settings.  The Isabelle
-  distribution already contains a global settings file with sensible
-  defaults for most variables.  When installing the system, only a few
-  of these may have to be adapted (probably @{setting ML_SYSTEM}
-  etc.).
-  
-  \item The file @{verbatim "$ISABELLE_HOME_USER/etc/settings"} (if it
-  exists) is run in the same way as the site default settings. Note
-  that the variable @{setting ISABELLE_HOME_USER} has already been set
-  before --- usually to something like @{verbatim
-  "$USER_HOME/.isabelle/IsabelleXXXX"}.
-  
-  Thus individual users may override the site-wide defaults.  See also
-  file @{file "$ISABELLE_HOME/etc/user-settings.sample"} in the
-  distribution.  Typically, a user settings file would contain only a
-  few lines, just the assigments that are really changed.  One should
-  definitely \emph{not} start with a full copy the basic @{file
-  "$ISABELLE_HOME/etc/settings"}. This could cause very annoying
-  maintainance problems later, when the Isabelle installation is
-  updated or changed otherwise.
-  
-  \end{enumerate}
-
-  Since settings files are regular GNU @{executable_def bash} scripts,
-  one may use complex shell commands, such as @{verbatim "if"} or
-  @{verbatim "case"} statements to set variables depending on the
-  system architecture or other environment variables.  Such advanced
-  features should be added only with great care, though. In
-  particular, external environment references should be kept at a
-  minimum.
-
-  \medskip A few variables are somewhat special:
-
-  \begin{itemize}
-
-  \item @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set
-  automatically to the absolute path names of the @{executable
-  "isabelle-process"} and @{executable isabelle} executables,
-  respectively.
-  
-  \item @{setting_ref ISABELLE_OUTPUT} will have the identifiers of
-  the Isabelle distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and
-  the ML system (cf.\ @{setting ML_IDENTIFIER}) appended automatically
-  to its value.
-
-  \end{itemize}
-
-  \medskip Note that the settings environment may be inspected with
-  the @{tool getenv} tool.  This might help to figure out the effect
-  of complex settings scripts.  *}
-
-
-subsection {* Common variables *}
-
-text {*
-  This is a reference of common Isabelle settings variables. Note that
-  the list is somewhat open-ended. Third-party utilities or interfaces
-  may add their own selection. Variables that are special in some
-  sense are marked with @{text "\<^sup>*"}.
-
-  \begin{description}
-
-  \item[@{setting_def USER_HOME}@{text "\<^sup>*"}] Is the cross-platform
-  user home directory.  On Unix systems this is usually the same as
-  @{setting HOME}, but on Windows it is the regular home directory of
-  the user, not the one of within the Cygwin root
-  file-system.\footnote{Cygwin itself offers another choice whether
-  its HOME should point to the \texttt{/home} directory tree or the
-  Windows user home.}
-
- \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the location of the
-  top-level Isabelle distribution directory. This is automatically
-  determined from the Isabelle executable that has been invoked.  Do
-  not attempt to set @{setting ISABELLE_HOME} yourself from the shell!
-  
-  \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
-  counterpart of @{setting ISABELLE_HOME}. The default value is
-  relative to @{verbatim "$USER_HOME/.isabelle"}, under rare
-  circumstances this may be changed in the global setting file.
-  Typically, the @{setting ISABELLE_HOME_USER} directory mimics
-  @{setting ISABELLE_HOME} to some extend. In particular, site-wide
-  defaults may be overridden by a private @{verbatim
-  "$ISABELLE_HOME_USER/etc/settings"}.
-  
-  \item[@{setting_def ISABELLE_PLATFORM}@{text "\<^sup>*"}] is automatically
-  set to a symbolic identifier for the underlying hardware and
-  operating system.  The Isabelle platform identification always
-  refers to the 32 bit variant, even this is a 64 bit machine.  Note
-  that the ML or Java runtime may have a different idea, depending on
-  which binaries are actually run.
-
-  \item[@{setting_def ISABELLE_PLATFORM64}@{text "\<^sup>*"}] is similar to
-  @{setting ISABELLE_PLATFORM} but refers to the proper 64 bit variant
-  on a platform that supports this; the value is empty for 32 bit.
-  Note that the following bash expression (including the quotes)
-  prefers the 64 bit platform, if that is available:
-
-  @{verbatim [display] "\"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}\""}
-
-  \item[@{setting_def ISABELLE_PROCESS}@{text "\<^sup>*"}, @{setting
-  ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path
-  names of the @{executable "isabelle-process"} and @{executable
-  isabelle} executables, respectively.  Thus other tools and scripts
-  need not assume that the @{file "$ISABELLE_HOME/bin"} directory is
-  on the current search path of the shell.
-  
-  \item[@{setting_def ISABELLE_IDENTIFIER}@{text "\<^sup>*"}] refers
-  to the name of this Isabelle distribution, e.g.\ ``@{verbatim
-  Isabelle2012}''.
-
-  \item[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME},
-  @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def
-  ML_IDENTIFIER}@{text "\<^sup>*"}] specify the underlying ML system
-  to be used for Isabelle.  There is only a fixed set of admissable
-  @{setting ML_SYSTEM} names (see the @{file
-  "$ISABELLE_HOME/etc/settings"} file of the distribution).
-  
-  The actual compiler binary will be run from the directory @{setting
-  ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the
-  command line.  The optional @{setting ML_PLATFORM} may specify the
-  binary format of ML heap images, which is useful for cross-platform
-  installations.  The value of @{setting ML_IDENTIFIER} is
-  automatically obtained by composing the values of @{setting
-  ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values.
-
-  \item[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK
-  (Java Development Kit) installation with @{verbatim javac} and
-  @{verbatim jar} executables.  This is essential for Isabelle/Scala
-  and other JVM-based tools to work properly.  Note that conventional
-  @{verbatim JAVA_HOME} usually points to the JRE (Java Runtime
-  Environment), not JDK.
-  
-  \item[@{setting_def ISABELLE_PATH}] is a list of directories
-  (separated by colons) where Isabelle logic images may reside.  When
-  looking up heaps files, the value of @{setting ML_IDENTIFIER} is
-  appended to each component internally.
-  
-  \item[@{setting_def ISABELLE_OUTPUT}@{text "\<^sup>*"}] is a
-  directory where output heap files should be stored by default. The
-  ML system and Isabelle version identifier is appended here, too.
-  
-  \item[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where
-  theory browser information (HTML text, graph data, and printable
-  documents) is stored (see also \secref{sec:info}).  The default
-  value is @{verbatim "$ISABELLE_HOME_USER/browser_info"}.
-  
-  \item[@{setting_def ISABELLE_LOGIC}] specifies the default logic to
-  load if none is given explicitely by the user.  The default value is
-  @{verbatim HOL}.
-  
-  \item[@{setting_def ISABELLE_LINE_EDITOR}] specifies the default
-  line editor for the @{tool_ref tty} interface.
-
-  \item[@{setting_def ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed
-  to the command line of any @{tool_ref usedir} invocation. This
-  typically contains compilation options for object-logics --- @{tool
-  usedir} is the basic tool for managing logic sessions (cf.\ the
-  @{verbatim IsaMakefile}s in the distribution).
-
-  \item[@{setting_def ISABELLE_LATEX}, @{setting_def
-  ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}, @{setting_def
-  ISABELLE_DVIPS}] refer to {\LaTeX} related tools for Isabelle
-  document preparation (see also \secref{sec:tool-latex}).
-  
-  \item[@{setting_def ISABELLE_TOOLS}] is a colon separated list of
-  directories that are scanned by @{executable isabelle} for external
-  utility programs (see also \secref{sec:isabelle-tool}).
-  
-  \item[@{setting_def ISABELLE_DOCS}] is a colon separated list of
-  directories with documentation files.
-  
-  \item[@{setting_def ISABELLE_DOC_FORMAT}] specifies the preferred
-  document format, typically @{verbatim dvi} or @{verbatim pdf}.
-  
-  \item[@{setting_def DVI_VIEWER}] specifies the command to be used
-  for displaying @{verbatim dvi} files.
-  
-  \item[@{setting_def PDF_VIEWER}] specifies the command to be used
-  for displaying @{verbatim pdf} files.
-  
-  \item[@{setting_def PRINT_COMMAND}] specifies the standard printer
-  spool command, which is expected to accept @{verbatim ps} files.
-  
-  \item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the
-  prefix from which any running @{executable "isabelle-process"}
-  derives an individual directory for temporary files.  The default is
-  somewhere in @{verbatim "/tmp"}.
-  
-  \end{description}
-*}
-
-
-subsection {* Additional components \label{sec:components} *}
-
-text {* Any directory may be registered as an explicit \emph{Isabelle
-  component}.  The general layout conventions are that of the main
-  Isabelle distribution itself, and the following two files (both
-  optional) have a special meaning:
-
-  \begin{itemize}
-
-  \item @{verbatim "etc/settings"} holds additional settings that are
-  initialized when bootstrapping the overall Isabelle environment,
-  cf.\ \secref{sec:boot}.  As usual, the content is interpreted as a
-  @{verbatim bash} script.  It may refer to the component's enclosing
-  directory via the @{verbatim "COMPONENT"} shell variable.
-
-  For example, the following setting allows to refer to files within
-  the component later on, without having to hardwire absolute paths:
-
-\begin{ttbox}
-MY_COMPONENT_HOME="$COMPONENT"
-\end{ttbox}
-
-  Components can also add to existing Isabelle settings such as
-  @{setting_def ISABELLE_TOOLS}, in order to provide
-  component-specific tools that can be invoked by end-users.  For
-  example:
-
-\begin{ttbox}
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
-\end{ttbox}
-
-  \item @{verbatim "etc/components"} holds a list of further
-  sub-components of the same structure.  The directory specifications
-  given here can be either absolute (with leading @{verbatim "/"}) or
-  relative to the component's main directory.
-
-  \end{itemize}
-
-  The root of component initialization is @{setting ISABELLE_HOME}
-  itself.  After initializing all of its sub-components recursively,
-  @{setting ISABELLE_HOME_USER} is included in the same manner (if
-  that directory exists).  This allows to install private components
-  via @{verbatim "$ISABELLE_HOME_USER/etc/components"}, although it is
-  often more convenient to do that programmatically via the
-  \verb,init_component, shell function in the \verb,etc/settings,
-  script of \verb,$ISABELLE_HOME_USER, (or any other component
-  directory).  For example:
-\begin{ttbox}
-init_component "$HOME/screwdriver-2.0"
-\end{ttbox}
-
-  This is tolerant wrt.\ missing component directories, but might
-  produce a warning.
-
-  \medskip More complex situations may be addressed by initializing
-  components listed in a given catalog file, relatively to some base
-  directory:
-
-\begin{ttbox}
-init_components "$HOME/my_component_store" "some_catalog_file"
-\end{ttbox}
-
-  The component directories listed in the catalog file are treated as
-  relative to the given base directory.
-
-  See also \secref{sec:tool-components} for some tool-support for
-  resolving components that are formally initialized but not installed
-  yet.
-*}
-
-
-section {* The raw Isabelle process *}
-
-text {*
-  The @{executable_def "isabelle-process"} executable runs bare-bones
-  Isabelle logic sessions --- either interactively or in batch mode.
-  It provides an abstraction over the underlying ML system, and over
-  the actual heap file locations.  Its usage is:
-
-\begin{ttbox}
-Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
-
-  Options are:
-    -I           startup Isar interaction mode
-    -P           startup Proof General interaction mode
-    -S           secure mode -- disallow critical operations
-    -T ADDR      startup process wrapper, with socket address
-    -W IN:OUT    startup process wrapper, with input/output fifos
-    -X           startup PGIP interaction mode
-    -e MLTEXT    pass MLTEXT to the ML session
-    -f           pass 'Session.finish();' to the ML session
-    -m MODE      add print mode for output
-    -q           non-interactive session
-    -r           open heap file read-only
-    -u           pass 'use"ROOT.ML";' to the ML session
-    -w           reset write permissions on OUTPUT
-
-  INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
-  These are either names to be searched in the Isabelle path, or
-  actual file names (containing at least one /).
-  If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
-\end{ttbox}
-
-  Input files without path specifications are looked up in the
-  @{setting ISABELLE_PATH} setting, which may consist of multiple
-  components separated by colons --- these are tried in the given
-  order with the value of @{setting ML_IDENTIFIER} appended
-  internally.  In a similar way, base names are relative to the
-  directory specified by @{setting ISABELLE_OUTPUT}.  In any case,
-  actual file locations may also be given by including at least one
-  slash (@{verbatim "/"}) in the name (hint: use @{verbatim "./"} to
-  refer to the current directory).
-*}
-
-
-subsubsection {* Options *}
-
-text {*
-  If the input heap file does not have write permission bits set, or
-  the @{verbatim "-r"} option is given explicitely, then the session
-  started will be read-only.  That is, the ML world cannot be
-  committed back into the image file.  Otherwise, a writable session
-  enables commits into either the input file, or into another output
-  heap file (if that is given as the second argument on the command
-  line).
-
-  The read-write state of sessions is determined at startup only, it
-  cannot be changed intermediately. Also note that heap images may
-  require considerable amounts of disk space (approximately
-  50--200~MB). Users are responsible for themselves to dispose their
-  heap files when they are no longer needed.
-
-  \medskip The @{verbatim "-w"} option makes the output heap file
-  read-only after terminating.  Thus subsequent invocations cause the
-  logic image to be read-only automatically.
-
-  \medskip Using the @{verbatim "-e"} option, arbitrary ML code may be
-  passed to the Isabelle session from the command line. Multiple
-  @{verbatim "-e"}'s are evaluated in the given order. Strange things
-  may happen when errorneous ML code is provided. Also make sure that
-  the ML commands are terminated properly by semicolon.
-
-  \medskip The @{verbatim "-u"} option is a shortcut for @{verbatim
-  "-e"} passing ``@{verbatim "use \"ROOT.ML\";"}'' to the ML session.
-  The @{verbatim "-f"} option passes ``@{verbatim
-  "Session.finish();"}'', which is intended mainly for administrative
-  purposes.
-
-  \medskip The @{verbatim "-m"} option adds identifiers of print modes
-  to be made active for this session. Typically, this is used by some
-  user interface, e.g.\ to enable output of proper mathematical
-  symbols.
-
-  \medskip Isabelle normally enters an interactive top-level loop
-  (after processing the @{verbatim "-e"} texts). The @{verbatim "-q"}
-  option inhibits interaction, thus providing a pure batch mode
-  facility.
-
-  \medskip The @{verbatim "-I"} option makes Isabelle enter Isar
-  interaction mode on startup, instead of the primitive ML top-level.
-  The @{verbatim "-P"} option configures the top-level loop for
-  interaction with the Proof General user interface, and the
-  @{verbatim "-X"} option enables XML-based PGIP communication.
-
-  \medskip The @{verbatim "-T"} or @{verbatim "-W"} option makes
-  Isabelle enter a special process wrapper for interaction via the
-  Isabelle/Scala layer, see also @{file
-  "~~/src/Pure/System/isabelle_process.scala"}.  The protocol between
-  the ML and JVM process is private to the implementation.
-
-  \medskip The @{verbatim "-S"} option makes the Isabelle process more
-  secure by disabling some critical operations, notably runtime
-  compilation and evaluation of ML source code.
-*}
-
-
-subsubsection {* Examples *}
-
-text {*
-  Run an interactive session of the default object-logic (as specified
-  by the @{setting ISABELLE_LOGIC} setting) like this:
-\begin{ttbox}
-isabelle-process
-\end{ttbox}
-
-  Usually @{setting ISABELLE_LOGIC} refers to one of the standard
-  logic images, which are read-only by default.  A writable session
-  --- based on @{verbatim HOL}, but output to @{verbatim Test} (in the
-  directory specified by the @{setting ISABELLE_OUTPUT} setting) ---
-  may be invoked as follows:
-\begin{ttbox}
-isabelle-process HOL Test
-\end{ttbox}
-  Ending this session normally (e.g.\ by typing control-D) dumps the
-  whole ML system state into @{verbatim Test} (be prepared for more
-  than 100\,MB):
-
-  The @{verbatim Test} session may be continued later (still in
-  writable state) by:
-\begin{ttbox}
-isabelle-process Test
-\end{ttbox}
-  A read-only @{verbatim Test} session may be started by:
-\begin{ttbox}
-isabelle-process -r Test
-\end{ttbox}
-
-  \medskip Note that manual session management like this does
-  \emph{not} provide proper setup for theory presentation.  This would
-  require @{tool usedir}.
-
-  \bigskip The next example demonstrates batch execution of Isabelle.
-  We retrieve the @{verbatim Main} theory value from the theory loader
-  within ML (observe the delicate quoting rules for the Bash shell
-  vs.\ ML):
-\begin{ttbox}
-isabelle-process -e 'Thy_Info.get_theory "Main";' -q -r HOL
-\end{ttbox}
-  Note that the output text will be interspersed with additional junk
-  messages by the ML runtime environment.  The @{verbatim "-W"} option
-  allows to communicate with the Isabelle process via an external
-  program in a more robust fashion.
-*}
-
-
-section {* The Isabelle tool wrapper \label{sec:isabelle-tool} *}
-
-text {*
-  All Isabelle related tools and interfaces are called via a common
-  wrapper --- @{executable isabelle}:
-
-\begin{ttbox}
-Usage: isabelle TOOL [ARGS ...]
-
-  Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
-
-Available tools:
-  \dots
-\end{ttbox}
-
-  In principle, Isabelle tools are ordinary executable scripts that
-  are run within the Isabelle settings environment, see
-  \secref{sec:settings}.  The set of available tools is collected by
-  @{executable isabelle} from the directories listed in the @{setting
-  ISABELLE_TOOLS} setting.  Do not try to call the scripts directly
-  from the shell.  Neither should you add the tool directories to your
-  shell's search path!
-*}
-
-
-subsubsection {* Examples *}
-
-text {* Show the list of available documentation of the Isabelle
-  distribution:
-
-\begin{ttbox}
-  isabelle doc
-\end{ttbox}
-
-  View a certain document as follows:
-\begin{ttbox}
-  isabelle doc system
-\end{ttbox}
-
-  Query the Isabelle settings environment:
-\begin{ttbox}
-  isabelle getenv ISABELLE_HOME_USER
-\end{ttbox}
-*}
-
-end
\ No newline at end of file




