doc-src/Ref/introduction.tex
author wenzelm
Wed Jun 09 14:08:08 2010 +0200 (2010-06-09)
changeset 37368 1c816f2abb0e
parent 30184 37969710e61f
child 39834 b5d688221d1b
permissions -rw-r--r--
removed outdated/confusing INSTALL file;
     1 
     2 \chapter{Basic Use of Isabelle}\index{sessions|(} 
     3 
     4 \section{Basic interaction with Isabelle}
     5 \index{starting up|bold}\nobreak
     6 %
     7 We assume that your local Isabelle administrator (this might be you!) has
     8 already installed the Isabelle system together with appropriate object-logics.
     9 
    10 \medskip Let $\langle isabellehome \rangle$ denote the location where
    11 the distribution has been installed.  To run Isabelle from a the shell
    12 prompt within an ordinary text terminal session, simply type
    13 \begin{ttbox}
    14 \({\langle}isabellehome{\rangle}\)/bin/isabelle
    15 \end{ttbox}
    16 This should start an interactive \ML{} session with the default object-logic
    17 (usually HOL) already pre-loaded.
    18 
    19 Subsequently, we assume that the \texttt{isabelle} executable is determined
    20 automatically by the shell, e.g.\ by adding {\tt \(\langle isabellehome
    21   \rangle\)/bin} to your search path.\footnote{Depending on your installation,
    22   there may be stand-alone binaries located in some global directory such as
    23   \texttt{/usr/bin}.  Do not attempt to copy {\tt \(\langle isabellehome
    24     \rangle\)/bin/isabelle}, though!  See \texttt{isabelle install} in
    25   \emph{The Isabelle System Manual} of how to do this properly.}
    26 
    27 \medskip
    28 
    29 The object-logic image to load may be also specified explicitly as an argument
    30 to the {\tt isabelle} command, e.g.
    31 \begin{ttbox}
    32 isabelle FOL
    33 \end{ttbox}
    34 This should put you into the world of polymorphic first-order logic (assuming
    35 that an image of FOL has been pre-built).
    36 
    37 \index{saving your session|bold} Isabelle provides no means of storing
    38 theorems or internal proof objects on files.  Theorems are simply part of the
    39 \ML{} state.  To save your work between sessions, you may dump the \ML{}
    40 system state to a file.  This is done automatically when ending the session
    41 normally (e.g.\ by typing control-D), provided that the image has been opened
    42 \emph{writable} in the first place.  The standard object-logic images are
    43 usually read-only, so you have to create a private working copy first.  For
    44 example, the following shell command puts you into a writable Isabelle session
    45 of name \texttt{Foo} that initially contains just plain HOL:
    46 \begin{ttbox}
    47 isabelle HOL Foo
    48 \end{ttbox}
    49 Ending the \texttt{Foo} session with control-D will cause the complete
    50 \ML-world to be saved somewhere in your home directory\footnote{The default
    51   location is in \texttt{\~\relax/isabelle/heaps}, but this depends on your
    52   local configuration.}.  Make sure there is enough space available! Then one
    53 may later continue at exactly the same point by running
    54 \begin{ttbox}
    55 isabelle Foo  
    56 \end{ttbox}
    57 
    58 \medskip Saving the {\ML} state is not enough.  Record, on a file, the
    59 top-level commands that generate your theories and proofs.  Such a record
    60 allows you to replay the proofs whenever required, for instance after making
    61 minor changes to the axioms.  Ideally, these sources will be somewhat
    62 intelligible to others as a formal description of your work.
    63 
    64 It is good practice to put all source files that constitute a separate
    65 Isabelle session into an individual directory, together with an {\ML} file
    66 called \texttt{ROOT.ML} that contains appropriate commands to load all other
    67 files required.  Running \texttt{isabelle} with option \texttt{-u}
    68 automatically loads \texttt{ROOT.ML} on entering the session.  The
    69 \texttt{isabelle usedir} utility provides some more options to manage Isabelle
    70 sessions, such as automatic generation of theory browsing information.
    71 
    72 \medskip More details about the \texttt{isabelle} and \texttt{isabelle}
    73 commands may be found in \emph{The Isabelle System Manual}.
    74 
    75 \medskip There are more comfortable user interfaces than the bare-bones \ML{}
    76 top-level run from a text terminal.  The \texttt{Isabelle} executable (note
    77 the capital I) runs one such interface, depending on your local configuration.
    78 Again, see \emph{The Isabelle System Manual} for more information.
    79 
    80 
    81 \section{Ending a session}
    82 \begin{ttbox} 
    83 quit    : unit -> unit
    84 exit    : int -> unit
    85 commit  : unit -> bool
    86 \end{ttbox}
    87 \begin{ttdescription}
    88 \item[\ttindexbold{quit}();] ends the Isabelle session, without saving
    89   the state.
    90   
    91 \item[\ttindexbold{exit} \(i\);] similar to {\tt quit}, passing return
    92   code \(i\) to the operating system.
    93 
    94 \item[\ttindexbold{commit}();] saves the current state without ending
    95   the session, provided that the logic image is opened read-write;
    96   return value {\tt false} indicates an error.
    97 \end{ttdescription}
    98 
    99 Typing control-D also finishes the session in essentially the same way
   100 as the sequence {\tt commit(); quit();} would.
   101 
   102 
   103 \section{Reading ML files}
   104 \index{files!reading}
   105 \begin{ttbox} 
   106 cd              : string -> unit
   107 pwd             : unit -> string
   108 use             : string -> unit
   109 time_use        : string -> unit
   110 \end{ttbox}
   111 \begin{ttdescription}
   112 \item[\ttindexbold{cd} "{\it dir}";] changes the current directory to
   113   {\it dir}.  This is the default directory for reading files.
   114   
   115 \item[\ttindexbold{pwd}();] returns the full path of the current
   116   directory.
   117 
   118 \item[\ttindexbold{use} "$file$";]  
   119 reads the given {\it file} as input to the \ML{} session.  Reading a file
   120 of Isabelle commands is the usual way of replaying a proof.
   121 
   122 \item[\ttindexbold{time_use} "$file$";]  
   123 performs {\tt use~"$file$"} and prints the total execution time.
   124 \end{ttdescription}
   125 
   126 The $dir$ and $file$ specifications of the \texttt{cd} and \texttt{use}
   127 commands may contain path variables (e.g.\ \texttt{\$ISABELLE_HOME}) that are
   128 expanded appropriately.  Note that \texttt{\~\relax} abbreviates
   129 \texttt{\$HOME}, and \texttt{\~\relax\~\relax} abbreviates
   130 \texttt{\$ISABELLE_HOME}\index{*\$ISABELLE_HOME}.  The syntax for path
   131 specifications follows Unix conventions.
   132 
   133 
   134 \section{Reading theories}\label{sec:intro-theories}
   135 \index{theories!reading}
   136 
   137 In Isabelle, any kind of declarations, definitions, etc.\ are organized around
   138 named \emph{theory} objects.  Logical reasoning always takes place within a
   139 certain theory context, which may be switched at any time.  Theory $name$ is
   140 defined by a theory file $name$\texttt{.thy}, containing declarations of
   141 \texttt{consts}, \texttt{types}, \texttt{defs}, etc.\ (see
   142 \S\ref{sec:ref-defining-theories} for more details on concrete syntax).
   143 Furthermore, there may be an associated {\ML} file $name$\texttt{.ML} with
   144 proof scripts that are to be run in the context of the theory.
   145 
   146 \begin{ttbox}
   147 context      : theory -> unit
   148 the_context  : unit -> theory
   149 theory       : string -> theory
   150 use_thy      : string -> unit
   151 time_use_thy : string -> unit
   152 update_thy   : string -> unit
   153 \end{ttbox}
   154 
   155 \begin{ttdescription}
   156   
   157 \item[\ttindexbold{context} $thy$;] switches the current theory context.  Any
   158   subsequent command with ``implicit theory argument'' (e.g.\ \texttt{Goal})
   159   will refer to $thy$ as its theory.
   160   
   161 \item[\ttindexbold{the_context}();] obtains the current theory context, or
   162   raises an error if absent.
   163   
   164 \item[\ttindexbold{theory} "$name$";] retrieves the theory called $name$ from
   165   the internal data\-base of loaded theories, raising an error if absent.
   166   
   167 \item[\ttindexbold{use_thy} "$name$";] reads theory $name$ from the file
   168   system, looking for $name$\texttt{.thy} and $name$\texttt{.ML} (the latter
   169   being optional).  It also ensures that all parent theories are loaded as
   170   well.  In case some older versions have already been present,
   171   \texttt{use_thy} only tries to reload $name$ itself, but is content with any
   172   version of its ancestors.
   173   
   174 \item[\ttindexbold{time_use_thy} "$name$";] same as \texttt{use_thy}, but
   175   reports the time taken to process the actual theory parts and {\ML} files
   176   separately.
   177   
   178 \item[\ttindexbold{update_thy} "$name$";] is similar to \texttt{use_thy}, but
   179   ensures that theory $name$ is fully up-to-date with respect to the file
   180   system --- apart from theory $name$ itself, any of its ancestors may be
   181   reloaded as well.
   182   
   183 \end{ttdescription}
   184 
   185 Note that theories of pre-built logic images (e.g.\ HOL) are marked as
   186 \emph{finished} and cannot be updated any more.  See \S\ref{sec:more-theories}
   187 for further information on Isabelle's theory loader.
   188 
   189 
   190 \section{Setting flags}
   191 \begin{ttbox}
   192 set     : bool ref -> bool
   193 reset   : bool ref -> bool
   194 toggle  : bool ref -> bool
   195 \end{ttbox}\index{*set}\index{*reset}\index{*toggle}
   196 These are some shorthands for manipulating boolean references.  The new
   197 value is returned.
   198 
   199 
   200 \section{Diagnostic messages}
   201 \index{error messages}
   202 \index{warnings}
   203 
   204 Isabelle conceptually provides three output channels for different kinds of
   205 messages: ordinary text, warnings, errors.  Depending on the user interface
   206 involved, these messages may appear in different text styles or colours.
   207 
   208 The default setup of an \texttt{isabelle} terminal session is as
   209 follows: plain output of ordinary text, warnings prefixed by
   210 \texttt{\#\#\#}'s, errors prefixed by \texttt{***}'s.  For example, a
   211 typical warning would look like this:
   212 \begin{ttbox}
   213 \#\#\# Beware the Jabberwock, my son!
   214 \#\#\# The jaws that bite, the claws that catch!
   215 \#\#\# Beware the Jubjub Bird, and shun
   216 \#\#\# The frumious Bandersnatch!
   217 \end{ttbox}
   218 
   219 \texttt{ML} programs may output diagnostic messages using the
   220 following functions:
   221 \begin{ttbox}
   222 writeln : string -> unit
   223 warning : string -> unit
   224 error   : string -> 'a
   225 \end{ttbox}
   226 Note that \ttindex{error} fails by raising exception \ttindex{ERROR}
   227 after having output the text, while \ttindex{writeln} and
   228 \ttindex{warning} resume normal program execution.
   229 
   230 
   231 \section{Timing}
   232 \index{timing statistics}\index{proofs!timing}
   233 \begin{ttbox} 
   234 timing: bool ref \hfill{\bf initially false}
   235 \end{ttbox}
   236 
   237 \begin{ttdescription}
   238 \item[set \ttindexbold{timing};] enables global timing in Isabelle.
   239   This information is compiler-dependent.
   240 \end{ttdescription}
   241 
   242 \index{sessions|)}
   243 
   244 
   245 %%% Local Variables: 
   246 %%% mode: latex
   247 %%% TeX-master: "ref"
   248 %%% End: