doc-src/Ref/introduction.tex
author wenzelm
Mon Aug 28 13:52:38 2000 +0200 (2000-08-28)
changeset 9695 ec7d7f877712
parent 9231 8812a07d52ee
child 12831 a2a3896f9c48
permissions -rw-r--r--
proper setup of iman.sty/extra.sty/ttbox.sty;
     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 may be stand-alone binaries located in some global directory such as
    43   \texttt{/usr/bin}.  Do not attempt to copy {\tt \(\langle isabellehome
    44     \rangle\)/bin/isabelle}, though!  See \texttt{isatool install} in
    45   \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 data\-base 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 constants
   292   when printing proof states.  Note that the output can be enormous as
   293   polymorphic constants often occur at several different type instances.
   294 
   295 \item[set \ttindexbold{long_names};] forces names of all objects
   296   (types, constants, theorems, etc.) to be printed in their fully
   297   qualified internal form.
   298 
   299 \end{ttdescription}
   300 
   301 
   302 \subsection{Eta-contraction before printing}
   303 \begin{ttbox} 
   304 eta_contract: bool ref
   305 \end{ttbox}
   306 The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$,
   307 provided $x$ is not free in ~$f$.  It asserts {\bf extensionality} of
   308 functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$.  Higher-order
   309 unification frequently puts terms into a fully $\eta$-expanded form.  For
   310 example, if $F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is
   311 $\lambda h.F(\lambda x.h(x))$.  By default, the user sees this expanded
   312 form.
   313 
   314 \begin{ttdescription}
   315 \item[set \ttindexbold{eta_contract};]
   316 makes Isabelle perform $\eta$-contractions before printing, so that
   317 $\lambda h.F(\lambda x.h(x))$ appears simply as~$F$.  The
   318 distinction between a term and its $\eta$-expanded form occasionally
   319 matters.
   320 \end{ttdescription}
   321 \index{printing control|)}
   322 
   323 \section{Diagnostic messages}
   324 \index{error messages}
   325 \index{warnings}
   326 
   327 Isabelle conceptually provides three output channels for different kinds of
   328 messages: ordinary text, warnings, errors.  Depending on the user interface
   329 involved, these messages may appear in different text styles or colours.
   330 
   331 The default setup of an \texttt{isabelle} terminal session is as
   332 follows: plain output of ordinary text, warnings prefixed by
   333 \texttt{\#\#\#}'s, errors prefixed by \texttt{***}'s.  For example, a
   334 typical warning would look like this:
   335 \begin{ttbox}
   336 \#\#\# Beware the Jabberwock, my son!
   337 \#\#\# The jaws that bite, the claws that catch!
   338 \#\#\# Beware the Jubjub Bird, and shun
   339 \#\#\# The frumious Bandersnatch!
   340 \end{ttbox}
   341 
   342 \texttt{ML} programs may output diagnostic messages using the
   343 following functions:
   344 \begin{ttbox}
   345 writeln : string -> unit
   346 warning : string -> unit
   347 error   : string -> 'a
   348 \end{ttbox}
   349 Note that \ttindex{error} fails by raising exception \ttindex{ERROR}
   350 after having output the text, while \ttindex{writeln} and
   351 \ttindex{warning} resume normal program execution.
   352 
   353 
   354 \section{Displaying exceptions as error messages}
   355 \index{exceptions!printing of}
   356 \begin{ttbox} 
   357 print_exn: exn -> 'a
   358 \end{ttbox}
   359 Certain Isabelle primitives, such as the forward proof functions {\tt RS}
   360 and {\tt RSN}, are called both interactively and from programs.  They
   361 indicate errors not by printing messages, but by raising exceptions.  For
   362 interactive use, \ML's reporting of an uncaught exception may be
   363 uninformative.  The Poly/ML function {\tt exception_trace} can generate a
   364 backtrace.\index{Poly/{\ML} compiler}
   365 
   366 \begin{ttdescription}
   367 \item[\ttindexbold{print_exn} $e$] 
   368 displays the exception~$e$ in a readable manner, and then re-raises~$e$.
   369 Typical usage is~\hbox{\tt $EXP$ handle e => print_exn e;}, where
   370 $EXP$ is an expression that may raise an exception.
   371 
   372 {\tt print_exn} can display the following common exceptions, which concern
   373 types, terms, theorems and theories, respectively.  Each carries a message
   374 and related information.
   375 \begin{ttbox} 
   376 exception TYPE   of string * typ list * term list
   377 exception TERM   of string * term list
   378 exception THM    of string * int * thm list
   379 exception THEORY of string * theory list
   380 \end{ttbox}
   381 \end{ttdescription}
   382 \begin{warn}
   383   {\tt print_exn} prints terms by calling \ttindex{prin}, which obtains
   384   pretty printing information from the proof state last stored in the
   385   subgoal module.  The appearance of the output thus depends upon the
   386   theory used in the last interactive proof.
   387 \end{warn}
   388 
   389 \index{sessions|)}
   390 
   391 
   392 %%% Local Variables: 
   393 %%% mode: latex
   394 %%% TeX-master: "ref"
   395 %%% End: