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: