doc-src/Ref/introduction.tex
author wenzelm
Fri Sep 24 12:22:59 1999 +0200 (1999-09-24 ago)
changeset 7592 c29a222cf981
parent 7282 69d601df351c
child 7990 0a604b2fc2b1
permissions -rw-r--r--
tuned;
     1 
     2 %% $Id$
     3 
     4 \chapter{Basic Use of Isabelle}\index{sessions|(} 
     5 The Reference Manual is a comprehensive description of Isabelle
     6 proper, including all \ML{} commands, functions and packages.  It
     7 really is intended for reference, perhaps for browsing, but not for
     8 reading through.  It is not a tutorial, but assumes familiarity with
     9 the basic logical concepts of Isabelle.
    10 
    11 When you are looking for a way of performing some task, scan the Table of
    12 Contents for a relevant heading.  Functions are organized by their purpose,
    13 by their operands (subgoals, tactics, theorems), and by their usefulness.
    14 In each section, basic functions appear first, then advanced functions, and
    15 finally esoteric functions.  Use the Index when you are looking for the
    16 definition of a particular Isabelle function.
    17 
    18 A few examples are presented.  Many example files are distributed with
    19 Isabelle, however; please experiment interactively.
    20 
    21 
    22 \section{Basic interaction with Isabelle}
    23 \index{starting up|bold}\nobreak
    24 %
    25 We assume that your local Isabelle administrator (this might be you!) has
    26 already installed the Isabelle system together with appropriate object-logics
    27 --- otherwise see the \texttt{README} and \texttt{INSTALL} files in the
    28 top-level directory of the distribution on how to do this.
    29 
    30 \medskip Let $\langle isabellehome \rangle$ denote the location where
    31 the distribution has been installed.  To run Isabelle from a the shell
    32 prompt within an ordinary text terminal session, simply type
    33 \begin{ttbox}
    34 \({\langle}isabellehome{\rangle}\)/bin/isabelle
    35 \end{ttbox}
    36 This should start an interactive \ML{} session with the default object-logic
    37 (usually {\HOL}) already pre-loaded.
    38 
    39 Subsequently, we assume that the \texttt{isabelle} executable is determined
    40 automatically by the shell, e.g.\ by adding {\tt \(\langle isabellehome
    41   \rangle\)/bin} to your search path.\footnote{Depending on your installation,
    42   there might be also stand-alone binaries located in some global directory
    43   such as \texttt{/usr/bin}.  Do not attempt to copy {\tt \(\langle
    44     isabellehome \rangle\)/bin/isabelle}, though!  See \texttt{isatool
    45     install} in \emph{The Isabelle System Manual} of how to do this properly.}
    46 
    47 \medskip
    48 
    49 The object-logic image to load may be also specified explicitly as an argument
    50 to the {\tt isabelle} command, e.g.
    51 \begin{ttbox}
    52 isabelle FOL
    53 \end{ttbox}
    54 This should put you into the world of polymorphic first-order logic (assuming
    55 that an image of {\FOL} has been pre-built).
    56 
    57 \index{saving your session|bold} Isabelle provides no means of storing
    58 theorems or internal proof objects on files.  Theorems are simply part of the
    59 \ML{} state.  To save your work between sessions, you may dump the \ML{}
    60 system state to a file.  This is done automatically when ending the session
    61 normally (e.g.\ by typing control-D), provided that the image has been opened
    62 \emph{writable} in the first place.  The standard object-logic images are
    63 usually read-only, so you have to create a private working copy first.  For
    64 example, the following shell command puts you into a writable Isabelle session
    65 of name \texttt{Foo} that initially contains just plain \HOL:
    66 \begin{ttbox}
    67 isabelle HOL Foo
    68 \end{ttbox}
    69 Ending the \texttt{Foo} session with control-D will cause the complete
    70 \ML-world to be saved somewhere in your home directory\footnote{The default
    71   location is in \texttt{\~\relax/isabelle/heaps}, but this depends on your
    72   local configuration.}.  Make sure there is enough space available! Then one
    73 may later continue at exactly the same point by running
    74 \begin{ttbox}
    75 isabelle Foo  
    76 \end{ttbox}
    77 
    78 \medskip Saving the {\ML} state is not enough.  Record, on a file, the
    79 top-level commands that generate your theories and proofs.  Such a record
    80 allows you to replay the proofs whenever required, for instance after making
    81 minor changes to the axioms.  Ideally, these sources will be somewhat
    82 intelligible to others as a formal description of your work.
    83 
    84 It is good practice to put all source files that constitute a separate
    85 Isabelle session into an individual directory, together with an {\ML} file
    86 called \texttt{ROOT.ML} that contains appropriate commands to load all other
    87 files required.  Running \texttt{isabelle} with option \texttt{-u}
    88 automatically loads \texttt{ROOT.ML} on entering the session.  The
    89 \texttt{isatool usedir} utility provides some more options to manage Isabelle
    90 sessions, such as automatic generation of theory browsing information.
    91 
    92 \medskip More details about the \texttt{isabelle} and \texttt{isatool}
    93 commands may be found in \emph{The Isabelle System Manual}.
    94 
    95 \medskip There are more comfortable user interfaces than the bare-bones \ML{}
    96 top-level run from a text terminal.  The \texttt{Isabelle} executable (note
    97 the capital I) runs one such interface, depending on your local configuration.
    98 Again, see \emph{The Isabelle System Manual} for more information.
    99 
   100 
   101 \section{Ending a session}
   102 \begin{ttbox} 
   103 quit    : unit -> unit
   104 exit    : int -> unit
   105 commit  : unit -> bool
   106 \end{ttbox}
   107 \begin{ttdescription}
   108 \item[\ttindexbold{quit}();] ends the Isabelle session, without saving
   109   the state.
   110   
   111 \item[\ttindexbold{exit} \(i\);] similar to {\tt quit}, passing return
   112   code \(i\) to the operating system.
   113 
   114 \item[\ttindexbold{commit}();] saves the current state without ending
   115   the session, provided that the logic image is opened read-write;
   116   return value {\tt false} indicates an error.
   117 \end{ttdescription}
   118 
   119 Typing control-D also finishes the session in essentially the same way
   120 as the sequence {\tt commit(); quit();} would.
   121 
   122 
   123 \section{Reading ML files}
   124 \index{files!reading}
   125 \begin{ttbox} 
   126 cd              : string -> unit
   127 pwd             : unit -> string
   128 use             : string -> unit
   129 time_use        : string -> unit
   130 \end{ttbox}
   131 \begin{ttdescription}
   132 \item[\ttindexbold{cd} "{\it dir}";] changes the current directory to
   133   {\it dir}.  This is the default directory for reading files.
   134   
   135 \item[\ttindexbold{pwd}();] returns the full path of the current
   136   directory.
   137 
   138 \item[\ttindexbold{use} "$file$";]  
   139 reads the given {\it file} as input to the \ML{} session.  Reading a file
   140 of Isabelle commands is the usual way of replaying a proof.
   141 
   142 \item[\ttindexbold{time_use} "$file$";]  
   143 performs {\tt use~"$file$"} and prints the total execution time.
   144 \end{ttdescription}
   145 
   146 The $dir$ and $file$ specifications of the \texttt{cd} and \texttt{use}
   147 commands may contain path variables (e.g.\ \texttt{\$ISABELLE_HOME}) that are
   148 expanded appropriately.  Note that \texttt{\~\relax} abbreviates
   149 \texttt{\$HOME}, and \texttt{\~\relax\~\relax} abbreviates
   150 \texttt{\$ISABELLE_HOME}\index{*\$ISABELLE_HOME}.  The syntax for path
   151 specifications follows Unix conventions.
   152 
   153 
   154 \section{Reading theories}\label{sec:intro-theories}
   155 \index{theories!reading}
   156 
   157 In Isabelle, any kind of declarations, definitions, etc.\ are organized around
   158 named \emph{theory} objects.  Logical reasoning always takes place within a
   159 certain theory context, which may be switched at any time.  Theory $name$ is
   160 defined by a theory file $name$\texttt{.thy}, containing declarations of
   161 \texttt{consts}, \texttt{types}, \texttt{defs}, etc.\ (see
   162 \S\ref{sec:ref-defining-theories} for more details on concrete syntax).
   163 Furthermore, there may be an associated {\ML} file $name$\texttt{.ML} with
   164 proof scripts that are to be run in the context of the theory.
   165 
   166 \begin{ttbox}
   167 context      : theory -> unit
   168 the_context  : unit -> theory
   169 theory       : string -> theory
   170 use_thy      : string -> unit
   171 time_use_thy : string -> unit
   172 update_thy   : string -> unit
   173 \end{ttbox}
   174 
   175 \begin{ttdescription}
   176   
   177 \item[\ttindexbold{context} $thy$;] switches the current theory context.  Any
   178   subsequent command with ``implicit theory argument'' (e.g.\ \texttt{Goal})
   179   will refer to $thy$ as its theory.
   180   
   181 \item[\ttindexbold{the_context}();] obtains the current theory context, or
   182   raises an error if absent.
   183   
   184 \item[\ttindexbold{theory} "$name$";] retrieves the theory called $name$ from
   185   the internal database of loaded theories, raising an error if absent.
   186   
   187 \item[\ttindexbold{use_thy} "$name$";] reads theory $name$ from the file
   188   system, looking for $name$\texttt{.thy} and $name$\texttt{.ML} (the latter
   189   being optional).  It also ensures that all parent theories are loaded as
   190   well.  In case some older versions have already been present,
   191   \texttt{use_thy} only tries to reload $name$ itself, but is content with any
   192   version of its ancestors.
   193   
   194 \item[\ttindexbold{time_use_thy} "$name$";] same as \texttt{use_thy}, but
   195   reports the time taken to process the actual theory parts and {\ML} files
   196   separately.
   197   
   198 \item[\ttindexbold{update_thy} "$name$";] is similar to \texttt{use_thy}, but
   199   ensures that theory $name$ is fully up-to-date with respect to the file
   200   system --- apart from theory $name$ itself, any of its ancestors may be
   201   reloaded as well.
   202   
   203 \end{ttdescription}
   204 
   205 Note that theories of pre-built logic images (e.g.\ {\HOL}) are marked as
   206 \emph{finished} and cannot be updated any more.  See \S\ref{sec:more-theories}
   207 for further information on Isabelle's theory loader.
   208 
   209 
   210 \section{Setting flags}
   211 \begin{ttbox}
   212 set     : bool ref -> bool
   213 reset   : bool ref -> bool
   214 toggle  : bool ref -> bool
   215 \end{ttbox}\index{*set}\index{*reset}\index{*toggle}
   216 These are some shorthands for manipulating boolean references.  The new
   217 value is returned.
   218 
   219 
   220 \section{Printing of terms and theorems}\label{sec:printing-control}
   221 \index{printing control|(}
   222 Isabelle's pretty printer is controlled by a number of parameters.
   223 
   224 \subsection{Printing limits}
   225 \begin{ttbox} 
   226 Pretty.setdepth  : int -> unit
   227 Pretty.setmargin : int -> unit
   228 print_depth      : int -> unit
   229 \end{ttbox}
   230 These set limits for terminal output.  See also {\tt goals_limit},
   231 which limits the number of subgoals printed
   232 (\S\ref{sec:goals-printing}).
   233 
   234 \begin{ttdescription}
   235 \item[\ttindexbold{Pretty.setdepth} \(d\);] tells Isabelle's pretty printer to
   236   limit the printing depth to~$d$.  This affects the display of theorems and
   237   terms.  The default value is~0, which permits printing to an arbitrary
   238   depth.  Useful values for $d$ are~10 and~20.
   239 
   240 \item[\ttindexbold{Pretty.setmargin} \(m\);]  
   241   tells Isabelle's pretty printer to assume a right margin (page width)
   242   of~$m$.  The initial margin is~76.
   243 
   244 \item[\ttindexbold{print_depth} \(n\);]  
   245   limits the printing depth of complex \ML{} values, such as theorems and
   246   terms.  This command affects the \ML{} top level and its effect is
   247   compiler-dependent.  Typically $n$ should be less than~10.
   248 \end{ttdescription}
   249 
   250 
   251 \subsection{Printing of hypotheses, brackets, types etc.}
   252 \index{meta-assumptions!printing of}
   253 \index{types!printing of}\index{sorts!printing of}
   254 \begin{ttbox} 
   255 show_hyps     : bool ref \hfill{\bf initially true}
   256 show_tags     : bool ref \hfill{\bf initially false}
   257 show_brackets : bool ref \hfill{\bf initially false}
   258 show_types    : bool ref \hfill{\bf initially false}
   259 show_sorts    : bool ref \hfill{\bf initially false}
   260 show_consts   : bool ref \hfill{\bf initially false}
   261 long_names    : bool ref \hfill{\bf initially false}
   262 \end{ttbox}
   263 These flags allow you to control how much information is displayed for
   264 types, terms and theorems.  The hypotheses of theorems \emph{are}
   265 normally shown.  Superfluous parentheses of types and terms are not.
   266 Types and sorts of variables are normally hidden.
   267 
   268 Note that displaying types and sorts may explain why a polymorphic
   269 inference rule fails to resolve with some goal, or why a rewrite rule
   270 does not apply as expected.
   271 
   272 \begin{ttdescription}
   273 
   274 \item[reset \ttindexbold{show_hyps};] makes Isabelle show each
   275   meta-level hypothesis as a dot.
   276   
   277 \item[set \ttindexbold{show_tags};] makes Isabelle show tags of theorems
   278   (which are basically just comments that may be attached by some tools).
   279   
   280 \item[set \ttindexbold{show_brackets};] makes Isabelle show full
   281   bracketing.  In particular, this reveals the grouping of infix
   282   operators.
   283   
   284 \item[set \ttindexbold{show_types};] makes Isabelle show types when
   285   printing a term or theorem.
   286   
   287 \item[set \ttindexbold{show_sorts};] makes Isabelle show both types
   288   and the sorts of type variables, independently of the value of
   289   \texttt{show_types}.
   290 
   291 \item[set \ttindexbold{show_consts};] makes Isabelle show types of
   292   constants, provided that showing of types is enabled at all.  This
   293   is supported for printing of proof states only.  Note that the
   294   output can be enormous as polymorphic constants often occur at
   295   several different type instances.
   296 
   297 \item[set \ttindexbold{long_names};] forces names of all objects
   298   (types, constants, theorems, etc.) to be printed in their fully
   299   qualified internal form.
   300 
   301 \end{ttdescription}
   302 
   303 
   304 \subsection{Eta-contraction before printing}
   305 \begin{ttbox} 
   306 eta_contract: bool ref \hfill{\bf initially false}
   307 \end{ttbox}
   308 The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$,
   309 provided $x$ is not free in ~$f$.  It asserts {\bf extensionality} of
   310 functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$.  Higher-order
   311 unification frequently puts terms into a fully $\eta$-expanded form.  For
   312 example, if $F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is
   313 $\lambda h.F(\lambda x.h(x))$.  By default, the user sees this expanded
   314 form.
   315 
   316 \begin{ttdescription}
   317 \item[set \ttindexbold{eta_contract};]
   318 makes Isabelle perform $\eta$-contractions before printing, so that
   319 $\lambda h.F(\lambda x.h(x))$ appears simply as~$F$.  The
   320 distinction between a term and its $\eta$-expanded form occasionally
   321 matters.
   322 \end{ttdescription}
   323 \index{printing control|)}
   324 
   325 \section{Diagnostic messages}
   326 \index{error messages}
   327 \index{warnings}
   328 
   329 Isabelle conceptually provides three output channels for different kinds of
   330 messages: ordinary text, warnings, errors.  Depending on the user interface
   331 involved, these messages may appear in different text styles or colours.
   332 
   333 The default setup of an \texttt{isabelle} terminal session is as
   334 follows: plain output of ordinary text, warnings prefixed by
   335 \texttt{\#\#\#}'s, errors prefixed by \texttt{***}'s.  For example, a
   336 typical warning would look like this:
   337 \begin{ttbox}
   338 \#\#\# Beware the Jabberwock, my son!
   339 \#\#\# The jaws that bite, the claws that catch!
   340 \#\#\# Beware the Jubjub Bird, and shun
   341 \#\#\# The frumious Bandersnatch!
   342 \end{ttbox}
   343 
   344 \texttt{ML} programs may output diagnostic messages using the
   345 following functions:
   346 \begin{ttbox}
   347 writeln : string -> unit
   348 warning : string -> unit
   349 error   : string -> 'a
   350 \end{ttbox}
   351 Note that \ttindex{error} fails by raising exception \ttindex{ERROR}
   352 after having output the text, while \ttindex{writeln} and
   353 \ttindex{warning} resume normal program execution.
   354 
   355 
   356 \section{Displaying exceptions as error messages}
   357 \index{exceptions!printing of}
   358 \begin{ttbox} 
   359 print_exn: exn -> 'a
   360 \end{ttbox}
   361 Certain Isabelle primitives, such as the forward proof functions {\tt RS}
   362 and {\tt RSN}, are called both interactively and from programs.  They
   363 indicate errors not by printing messages, but by raising exceptions.  For
   364 interactive use, \ML's reporting of an uncaught exception may be
   365 uninformative.  The Poly/ML function {\tt exception_trace} can generate a
   366 backtrace.\index{Poly/{\ML} compiler}
   367 
   368 \begin{ttdescription}
   369 \item[\ttindexbold{print_exn} $e$] 
   370 displays the exception~$e$ in a readable manner, and then re-raises~$e$.
   371 Typical usage is~\hbox{\tt $EXP$ handle e => print_exn e;}, where
   372 $EXP$ is an expression that may raise an exception.
   373 
   374 {\tt print_exn} can display the following common exceptions, which concern
   375 types, terms, theorems and theories, respectively.  Each carries a message
   376 and related information.
   377 \begin{ttbox} 
   378 exception TYPE   of string * typ list * term list
   379 exception TERM   of string * term list
   380 exception THM    of string * int * thm list
   381 exception THEORY of string * theory list
   382 \end{ttbox}
   383 \end{ttdescription}
   384 \begin{warn}
   385   {\tt print_exn} prints terms by calling \ttindex{prin}, which obtains
   386   pretty printing information from the proof state last stored in the
   387   subgoal module.  The appearance of the output thus depends upon the
   388   theory used in the last interactive proof.
   389 \end{warn}
   390 
   391 \index{sessions|)}
   392 
   393 
   394 %%% Local Variables: 
   395 %%% mode: latex
   396 %%% TeX-master: "ref"
   397 %%% End: