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|)}