doc-src/Ref/introduction.tex
author wenzelm
Thu May 15 14:58:51 1997 +0200 (1997-05-15)
changeset 3200 ea2310ba01da
parent 3108 335efc3f5632
child 3485 f27a30a18a17
permissions -rw-r--r--
sysman refs;
removed garbage;
     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 examples 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!)
    26 has already installed the \Pure\ system and several object-logics
    27 properly --- otherwise see the {\tt INSTALL} file in the top-level
    28 directory of the distribution on how to build it.
    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
    37 object-logic already preloaded. All Isabelle commands are bound to
    38 \ML{} identifiers.
    39 
    40 Subsequently we assume that {\tt \(\langle isabellehome \rangle\)/bin}
    41 has been added to your shell's search path, in order to avoid typing
    42 full path specifications of the executable files.
    43 
    44 The object-logic image to load may be also specified explicitly as an
    45 argument to the {\tt isabelle} command, e.g.:
    46 \begin{ttbox}
    47 isabelle FOL
    48 \end{ttbox}
    49 This should put you into the world of polymorphic first-order logic
    50 (assuming that {\FOL} has been pre-built).
    51 
    52 \index{saving your work|bold} Isabelle provides no means of storing
    53 theorems or proofs on files.  Theorems are simply part of the \ML{}
    54 state and are named by \ML{} identifiers.  To save your work between
    55 sessions, you must dump the \ML{} system state to a file. This is done
    56 automatically when ending the session normally (e.g.\ by typing
    57 control-D), provided that the image has been opened \emph{writable} in
    58 the first place. The standard object-logics are usually read-only, so
    59 you probably have to create a private working copy first. For example,
    60 the following shell command puts you into a writable Isabelle session
    61 of name \texttt{Foo} that initially contains just \FOL:
    62 \begin{ttbox}
    63 isabelle FOL Foo
    64 \end{ttbox}
    65 Ending the \texttt{Foo} session with control-D will cause the complete
    66 \ML{} world to be saved somewhere in your home directory\footnote{The
    67   default location is in \texttt{\~\relax/isabelle/heaps}, but this
    68   depends on your local configuration.}. Make sure there is enough
    69 space available! Then one may later continue at exactly the same point
    70 by running
    71 \begin{ttbox}
    72 isabelle Foo  
    73 \end{ttbox}
    74 
    75 More details about \texttt{isabelle} may be found in the \emph{System
    76   Manual}.
    77 
    78 \medskip Saving the state is not enough.  Record, on a file, the
    79 top-level commands that generate your theories and proofs.  Such a
    80 record allows you to replay the proofs whenever required, for instance
    81 after making minor changes to the axioms.  Ideally, your record will
    82 be somewhat intelligible to others as a formal description of your
    83 work.
    84 
    85 \medskip There are more comfortable user interfaces than the
    86 bare-bones \ML{} top-level run from a text terminal. The
    87 \texttt{Isabelle} executable (note the capital I) runs one such
    88 interface, depending on your local configuration.  Furthermore there
    89 are a number of external utilities available. These are started
    90 uniformly via the \texttt{isatool} wrapper.
    91 
    92 Again, see the \emph{System Manual} for more information user
    93 interfaces and utilities.
    94 
    95 
    96 \section{Ending a session}
    97 \begin{ttbox} 
    98 quit    : unit -> unit
    99 exit    : int -> unit
   100 commit  : unit -> unit
   101 \end{ttbox}
   102 \begin{ttdescription}
   103 \item[\ttindexbold{quit}();] ends the Isabelle session, without saving
   104   the state.
   105 
   106 \item[\ttindexbold{exit}();] same as {\tt quit}, passing a return code
   107   to the operating system.
   108 
   109 \item[\ttindexbold{commit}();] saves the current state without ending
   110   the session, provided that the logic image is opened read-write.
   111 \end{ttdescription}
   112 
   113 Typing control-D also finishes the session in essentially the same way
   114 as the sequence {\tt commit(); quit();} would.
   115 
   116 
   117 \section{Reading ML files}
   118 \index{files!reading}
   119 \begin{ttbox} 
   120 cd              : string -> unit
   121 pwd             : unit -> string
   122 use             : string -> unit
   123 time_use        : string -> unit
   124 \end{ttbox}
   125 Section~\ref{LoadingTheories} describes commands for loading theory files.
   126 \begin{ttdescription}
   127 \item[\ttindexbold{cd} "{\it dir}";]
   128   changes the current directory to {\it dir}.  This is the default directory
   129   for reading files and for writing temporary files.
   130 
   131 \item[\ttindexbold{pwd}();] returns the path of the current directory.
   132 
   133 \item[\ttindexbold{use} "$file$";]  
   134 reads the given {\it file} as input to the \ML{} session.  Reading a file
   135 of Isabelle commands is the usual way of replaying a proof.
   136 
   137 \item[\ttindexbold{time_use} "$file$";]  
   138 performs {\tt use~"$file$"} and prints the total execution time.
   139 \end{ttdescription}
   140 
   141 
   142 \section{Setting flags}
   143 \begin{ttbox}
   144 set     : bool ref -> bool
   145 reset   : bool ref -> bool
   146 toggle  : bool ref -> bool
   147 \end{ttbox}\index{*set}\index{*reset}\index{*toggle}
   148 These are some shorthands for manipulating boolean references. The new
   149 value is returned.
   150 
   151 
   152 \section{Printing of terms and theorems}\label{sec:printing-control}
   153 \index{printing control|(}
   154 Isabelle's pretty printer is controlled by a number of parameters.
   155 
   156 \subsection{Printing limits}
   157 \begin{ttbox} 
   158 Pretty.setdepth  : int -> unit
   159 Pretty.setmargin : int -> unit
   160 print_depth      : int -> unit
   161 \end{ttbox}
   162 These set limits for terminal output.  See also {\tt goals_limit}, which
   163 limits the number of subgoals printed (page~\pageref{sec:goals-printing}).
   164 
   165 \begin{ttdescription}
   166 \item[\ttindexbold{Pretty.setdepth} \(d\);]  
   167   tells Isabelle's pretty printer to limit the printing depth to~$d$.  This
   168   affects Isabelle's display of theorems and terms.  The default value
   169   is~0, which permits printing to an arbitrary depth.  Useful values for
   170   $d$ are~10 and~20.
   171 
   172 \item[\ttindexbold{Pretty.setmargin} \(m\);]  
   173   tells Isabelle's pretty printer to assume a right margin (page width)
   174   of~$m$.  The initial margin is~80.
   175 
   176 \item[\ttindexbold{print_depth} \(n\);]  
   177   limits the printing depth of complex \ML{} values, such as theorems and
   178   terms.  This command affects the \ML{} top level and its effect is
   179   compiler-dependent.  Typically $n$ should be less than~10.
   180 \end{ttdescription}
   181 
   182 
   183 \subsection{Printing of hypotheses, brackets, types and sorts}
   184 \index{meta-assumptions!printing of}
   185 \index{types!printing of}\index{sorts!printing of}
   186 \begin{ttbox} 
   187 show_hyps     : bool ref \hfill{\bf initially true}
   188 show_brackets : bool ref \hfill{\bf initially false}
   189 show_types    : bool ref \hfill{\bf initially false}
   190 show_sorts    : bool ref \hfill{\bf initially false}
   191 \end{ttbox}
   192 These flags allow you to control how much information is displayed for
   193 terms and theorems.  The hypotheses are normally shown; superfluous
   194 parentheses are not.  Types and sorts are normally hidden.  Displaying
   195 types and sorts may explain why a polymorphic inference rule fails to
   196 resolve with some goal.
   197 
   198 \begin{ttdescription}
   199 \item[\ttindexbold{show_hyps} := false;]   
   200 makes Isabelle show each meta-level hypothesis as a dot.
   201 
   202 \item[\ttindexbold{show_brackets} := true;] 
   203   makes Isabelle show full bracketing.  This reveals the
   204   grouping of infix operators.
   205 
   206 \item[\ttindexbold{show_types} := true;]
   207 makes Isabelle show types when printing a term or theorem.
   208 
   209 \item[\ttindexbold{show_sorts} := true;]
   210 makes Isabelle show both types and the sorts of type variables.  It does not
   211 matter whether {\tt show_types} is also~{\tt true}. 
   212 \end{ttdescription}
   213 
   214 
   215 \subsection{$\eta$-contraction before printing}
   216 \begin{ttbox} 
   217 eta_contract: bool ref \hfill{\bf initially false}
   218 \end{ttbox}
   219 The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$,
   220 provided $x$ is not free in ~$f$.  It asserts {\bf extensionality} of
   221 functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$.  Higher-order
   222 unification frequently puts terms into a fully $\eta$-expanded form.  For
   223 example, if $F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is
   224 $\lambda h.F(\lambda x.h(x))$.  By default, the user sees this expanded
   225 form.
   226 
   227 \begin{ttdescription}
   228 \item[\ttindexbold{eta_contract} := true;]
   229 makes Isabelle perform $\eta$-contractions before printing, so that
   230 $\lambda h.F(\lambda x.h(x))$ appears simply as~$F$.  The
   231 distinction between a term and its $\eta$-expanded form occasionally
   232 matters.
   233 \end{ttdescription}
   234 \index{printing control|)}
   235 
   236 
   237 \section{Displaying exceptions as error messages}
   238 \index{exceptions!printing of}
   239 \begin{ttbox} 
   240 print_exn: exn -> 'a
   241 \end{ttbox}
   242 Certain Isabelle primitives, such as the forward proof functions {\tt RS}
   243 and {\tt RSN}, are called both interactively and from programs.  They
   244 indicate errors not by printing messages, but by raising exceptions.  For
   245 interactive use, \ML's reporting of an uncaught exception is 
   246 uninformative.  The Poly/ML function {\tt exception_trace} can generate a
   247 backtrace.\index{Poly/{\ML} compiler}
   248 
   249 \begin{ttdescription}
   250 \item[\ttindexbold{print_exn} $e$] 
   251 displays the exception~$e$ in a readable manner, and then re-raises~$e$.
   252 Typical usage is~\hbox{\tt $EXP$ handle e => print_exn e;}, where
   253 $EXP$ is an expression that may raise an exception.
   254 
   255 {\tt print_exn} can display the following common exceptions, which concern
   256 types, terms, theorems and theories, respectively.  Each carries a message
   257 and related information.
   258 \begin{ttbox} 
   259 exception TYPE   of string * typ list * term list
   260 exception TERM   of string * term list
   261 exception THM    of string * int * thm list
   262 exception THEORY of string * theory list
   263 \end{ttbox}
   264 \end{ttdescription}
   265 \begin{warn}
   266   {\tt print_exn} prints terms by calling \ttindex{prin}, which obtains
   267   pretty printing information from the proof state last stored in the
   268   subgoal module.  The appearance of the output thus depends upon the
   269   theory used in the last interactive proof.
   270 \end{warn}
   271 
   272 \index{sessions|)}