1.1 --- a/doc-src/Ref/introduction.tex Mon May 03 14:43:52 1999 +0200
1.2 +++ b/doc-src/Ref/introduction.tex Mon May 03 18:35:48 1999 +0200
1.3 @@ -15,17 +15,17 @@
1.4 finally esoteric functions. Use the Index when you are looking for the
1.5 definition of a particular Isabelle function.
1.6
1.7 -A few examples are presented. Many examples files are distributed with
1.8 +A few examples are presented. Many example files are distributed with
1.9 Isabelle, however; please experiment interactively.
1.10
1.11
1.12 \section{Basic interaction with Isabelle}
1.13 \index{starting up|bold}\nobreak
1.14 %
1.15 -We assume that your local Isabelle administrator (this might be you!)
1.16 -has already installed the \Pure\ system and several object-logics
1.17 -properly --- otherwise see the {\tt INSTALL} file in the top-level
1.18 -directory of the distribution on how to build it.
1.19 +We assume that your local Isabelle administrator (this might be you!) has
1.20 +already installed the Isabelle system together with appropriate object-logics
1.21 +--- otherwise see the \texttt{README} and \texttt{INSTALL} files in the
1.22 +top-level directory of the distribution on how to do this.
1.23
1.24 \medskip Let $\langle isabellehome \rangle$ denote the location where
1.25 the distribution has been installed. To run Isabelle from a the shell
1.26 @@ -33,61 +33,67 @@
1.27 \begin{ttbox}
1.28 \({\langle}isabellehome{\rangle}\)/bin/isabelle
1.29 \end{ttbox}
1.30 -This should start an interactive \ML{} session with the default
1.31 -object-logic already preloaded.
1.32 +This should start an interactive \ML{} session with the default object-logic
1.33 +(usually {\HOL}) already pre-loaded.
1.34
1.35 -Subsequently we assume that {\tt \(\langle isabellehome \rangle\)/bin}
1.36 -has been added to your shell's search path, in order to avoid typing
1.37 -full path specifications of the executable files.
1.38 +Subsequently, we assume that the \texttt{isabelle} executable is determined
1.39 +automatically by the shell, e.g.\ by adding {\tt \(\langle isabellehome
1.40 + \rangle\)/bin} to your search path.\footnote{Depending on your installation,
1.41 + there might be also stand-alone binaries located in some global directory
1.42 + such as \texttt{/usr/bin}. Do not attempt to copy {\tt \(\langle
1.43 + isabellehome \rangle\)/bin/isabelle}, though! See \texttt{isatool
1.44 + install} in \emph{The Isabelle System Manual} of how to do this properly.}
1.45
1.46 -The object-logic image to load may be also specified explicitly as an
1.47 -argument to the {\tt isabelle} command, e.g.
1.48 +The object-logic image to load may be also specified explicitly as an argument
1.49 +to the {\tt isabelle} command, e.g.
1.50 \begin{ttbox}
1.51 isabelle FOL
1.52 \end{ttbox}
1.53 -This should put you into the world of polymorphic first-order logic
1.54 -(assuming that {\FOL} has been pre-built).
1.55 +This should put you into the world of polymorphic first-order logic (assuming
1.56 +that an image of {\FOL} has been pre-built).
1.57
1.58 -\index{saving your work|bold} Isabelle provides no means of storing
1.59 -theorems or internal proof objects on files. Theorems are simply part
1.60 -of the \ML{} state. To save your work between sessions, you must dump
1.61 -the \ML{} system state to a file. This is done automatically when
1.62 -ending the session normally (e.g.\ by typing control-D), provided that
1.63 -the image has been opened \emph{writable} in the first place. The
1.64 -standard object-logic images are usually read-only, so you probably
1.65 -have to create a private working copy first. For example, the
1.66 -following shell command puts you into a writable Isabelle session of
1.67 -name \texttt{Foo} that initially contains just \FOL:
1.68 +\index{saving your session|bold} Isabelle provides no means of storing
1.69 +theorems or internal proof objects on files. Theorems are simply part of the
1.70 +\ML{} state. To save your work between sessions, you may dump the \ML{}
1.71 +system state to a file. This is done automatically when ending the session
1.72 +normally (e.g.\ by typing control-D), provided that the image has been opened
1.73 +\emph{writable} in the first place. The standard object-logic images are
1.74 +usually read-only, so you have to create a private working copy first. For
1.75 +example, the following shell command puts you into a writable Isabelle session
1.76 +of name \texttt{Foo} that initially contains just plain \HOL:
1.77 \begin{ttbox}
1.78 -isabelle FOL Foo
1.79 +isabelle HOL Foo
1.80 \end{ttbox}
1.81 Ending the \texttt{Foo} session with control-D will cause the complete
1.82 -\ML{} world to be saved somewhere in your home directory\footnote{The
1.83 - default location is in \texttt{\~\relax/isabelle/heaps}, but this
1.84 - depends on your local configuration.}. Make sure there is enough
1.85 -space available! Then one may later continue at exactly the same point
1.86 -by running
1.87 +\ML-world to be saved somewhere in your home directory\footnote{The default
1.88 + location is in \texttt{\~\relax/isabelle/heaps}, but this depends on your
1.89 + local configuration.}. Make sure there is enough space available! Then one
1.90 +may later continue at exactly the same point by running
1.91 \begin{ttbox}
1.92 isabelle Foo
1.93 \end{ttbox}
1.94
1.95 -More details about the \texttt{isabelle} command may be found in \emph{The
1.96 - Isabelle System Manual}.
1.97 +\medskip Saving the {\ML} state is not enough. Record, on a file, the
1.98 +top-level commands that generate your theories and proofs. Such a record
1.99 +allows you to replay the proofs whenever required, for instance after making
1.100 +minor changes to the axioms. Ideally, your these sources will be somewhat
1.101 +intelligible to others as a formal description of your work.
1.102
1.103 -\medskip Saving the state is not enough. Record, on a file, the
1.104 -top-level commands that generate your theories and proofs. Such a
1.105 -record allows you to replay the proofs whenever required, for instance
1.106 -after making minor changes to the axioms. Ideally, your record will
1.107 -be somewhat intelligible to others as a formal description of your
1.108 -work.
1.109 +It is good practice to put all source files that constitute a separate
1.110 +Isabelle session into an individual directory, together with an {\ML} file
1.111 +called \texttt{ROOT.ML} that contains appropriate commands to load all other
1.112 +files required. Running \texttt{isabelle} with option \texttt{-u}
1.113 +automatically loads \texttt{ROOT.ML} on entering the session. The
1.114 +\texttt{isatool usedir} utility provides some more options to manage your
1.115 +sessions, such as automatic generation of theory browsing information.
1.116
1.117 -\medskip There are more comfortable user interfaces than the
1.118 -bare-bones \ML{} top-level run from a text terminal. The
1.119 -\texttt{Isabelle} executable (note the capital I) runs one such
1.120 -interface, depending on your local configuration. Furthermore there
1.121 -are a number of external utilities available. These are started
1.122 -uniformly via the \texttt{isatool} wrapper. See the \emph{System
1.123 - Manual} for more information user interfaces and utilities.
1.124 +\medskip More details about the \texttt{isabelle} and \texttt{isatool}
1.125 +commands may be found in \emph{The Isabelle System Manual}.
1.126 +
1.127 +\medskip There are more comfortable user interfaces than the bare-bones \ML{}
1.128 +top-level run from a text terminal. The \texttt{Isabelle} executable (note
1.129 +the capital I) runs one such interface, depending on your local configuration.
1.130 +Again, see \emph{The Isabelle System Manual} for more information.
1.131
1.132
1.133 \section{Ending a session}
1.134 @@ -139,8 +145,55 @@
1.135 commands may contain path variables (e.g.\ \texttt{\$ISABELLE_HOME}) that are
1.136 expanded appropriately. Note that \texttt{\~\relax} abbreviates
1.137 \texttt{\$HOME}, and \texttt{\~\relax\~\relax} abbreviates
1.138 -\texttt{\$ISABELLE_HOME}. Section~\ref{LoadingTheories} describes commands
1.139 -for loading theory files.
1.140 +\texttt{\$ISABELLE_HOME}.
1.141 +
1.142 +
1.143 +\section{Reading theories}\label{sec:intro-theories}
1.144 +\index{theories!reading}
1.145 +
1.146 +In Isabelle, any kind of declarations, definitions, etc.\ are organized around
1.147 +named \emph{theory} objects. Logical reasoning always takes place within a
1.148 +certain theory context, which may be switched at any time. Theory $name$ is
1.149 +defined by a theory file $name$\texttt{.thy}, containing declarations of
1.150 +\texttt{consts}, \texttt{types}, \texttt{defs}, etc.\ (see
1.151 +\S\ref{sec:ref-defining-theories} for more details on concrete syntax).
1.152 +Furthermore, there may be an associated {\ML} file $name$\texttt{.ML} with
1.153 +proof scripts that are to be run in the context of the theory.
1.154 +
1.155 +\begin{ttbox}
1.156 +context : theory -> unit
1.157 +the_context : unit -> theory
1.158 +theory : string -> theory
1.159 +use_thy : string -> unit
1.160 +time_use_thy : string -> unit
1.161 +\end{ttbox}
1.162 +
1.163 +\begin{ttdescription}
1.164 +
1.165 +\item[\ttindexbold{context} $thy$;] switches the current theory context. Any
1.166 + subsequent command with ``implicit theory argument'' (e.g.\ \texttt{Goal})
1.167 + will refer to $thy$ as its theory.
1.168 +
1.169 +\item[\ttindexbold{the_context}();] obtains the current theory context, or
1.170 + raises an error if absent.
1.171 +
1.172 +\item[\ttindexbold{theory} $name$;] retrieves the theory called $name$ from
1.173 + the internal database of loaded theories, raising an error if absent.
1.174 +
1.175 +\item[\ttindexbold{use_thy} $name$;] reads theory $name$ from the file system,
1.176 + looking for $name$\texttt{.thy} and (optionally) $name$\texttt{.ML}; also
1.177 + makes sure that all parent theories are loaded as well. In case some older
1.178 + versions have already been present, \texttt{use_thy} only tries to reload
1.179 + $name$ itself, but is content with any version of its parents.
1.180 +
1.181 +\item[\ttindexbold{time_use_thy} $name$;] same as \texttt{use_thy}, but
1.182 + reports the time taken to process the actual theory parts and {\ML} files
1.183 + separately.
1.184 +
1.185 +\end{ttdescription}
1.186 +
1.187 +See \S\ref{sec:more-theories} for further information on Isabelle's theory
1.188 +loader.
1.189
1.190
1.191 \section{Setting flags}
1.192 @@ -263,10 +316,9 @@
1.193 \index{error messages}
1.194 \index{warnings}
1.195
1.196 -Isabelle conceptually provides three output channels for different
1.197 -kinds of messages: ordinary text, warnings, errors. Depending on the
1.198 -user interface involved, these messages may appear in different text
1.199 -styles or colours, even within separate windows.
1.200 +Isabelle conceptually provides three output channels for different kinds of
1.201 +messages: ordinary text, warnings, errors. Depending on the user interface
1.202 +involved, these messages may appear in different text styles or colours.
1.203
1.204 The default setup of an \texttt{isabelle} terminal session is as
1.205 follows: plain output of ordinary text, warnings prefixed by