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: