\chapter{Basic Use of Isabelle}\index{sessions|(} \section{Basic interaction with Isabelle}\index{starting up|bold}\nobreak%We assume that your local Isabelle administrator (this might be you!) hasalready installed the Isabelle system together with appropriate object-logics--- otherwise see the \texttt{README} and \texttt{INSTALL} files in thetop-level directory of the distribution on how to do this.\medskip Let $\langle isabellehome \rangle$ denote the location wherethe distribution has been installed. To run Isabelle from a the shellprompt within an ordinary text terminal session, simply type\begin{ttbox}\({\langle}isabellehome{\rangle}\)/bin/isabelle\end{ttbox}This should start an interactive \ML{} session with the default object-logic(usually HOL) already pre-loaded.Subsequently, we assume that the \texttt{isabelle} executable is determinedautomatically by the shell, e.g.\ by adding {\tt \(\langle isabellehome \rangle\)/bin} to your search path.\footnote{Depending on your installation, there may be stand-alone binaries located in some global directory such as \texttt{/usr/bin}. Do not attempt to copy {\tt \(\langle isabellehome \rangle\)/bin/isabelle}, though! See \texttt{isabelle install} in \emph{The Isabelle System Manual} of how to do this properly.}\medskipThe object-logic image to load may be also specified explicitly as an argumentto the {\tt isabelle} command, e.g.\begin{ttbox}isabelle FOL\end{ttbox}This should put you into the world of polymorphic first-order logic (assumingthat an image of FOL has been pre-built).\index{saving your session|bold} Isabelle provides no means of storingtheorems or internal proof objects on files. Theorems are simply part of the\ML{} state. To save your work between sessions, you may dump the \ML{}system state to a file. This is done automatically when ending the sessionnormally (e.g.\ by typing control-D), provided that the image has been opened\emph{writable} in the first place. The standard object-logic images areusually read-only, so you have to create a private working copy first. Forexample, the following shell command puts you into a writable Isabelle sessionof name \texttt{Foo} that initially contains just plain HOL:\begin{ttbox}isabelle HOL Foo\end{ttbox}Ending the \texttt{Foo} session with control-D will cause the complete\ML-world to be saved somewhere in your home directory\footnote{The default location is in \texttt{\~\relax/isabelle/heaps}, but this depends on your local configuration.}. Make sure there is enough space available! Then onemay later continue at exactly the same point by running\begin{ttbox}isabelle Foo \end{ttbox}\medskip Saving the {\ML} state is not enough. Record, on a file, thetop-level commands that generate your theories and proofs. Such a recordallows you to replay the proofs whenever required, for instance after makingminor changes to the axioms. Ideally, these sources will be somewhatintelligible to others as a formal description of your work.It is good practice to put all source files that constitute a separateIsabelle session into an individual directory, together with an {\ML} filecalled \texttt{ROOT.ML} that contains appropriate commands to load all otherfiles required. Running \texttt{isabelle} with option \texttt{-u}automatically loads \texttt{ROOT.ML} on entering the session. The\texttt{isabelle usedir} utility provides some more options to manage Isabellesessions, such as automatic generation of theory browsing information.\medskip More details about the \texttt{isabelle} and \texttt{isabelle}commands may be found in \emph{The Isabelle System Manual}.\medskip There are more comfortable user interfaces than the bare-bones \ML{}top-level run from a text terminal. The \texttt{Isabelle} executable (notethe capital I) runs one such interface, depending on your local configuration.Again, see \emph{The Isabelle System Manual} for more information.\section{Ending a session}\begin{ttbox} quit : unit -> unitexit : int -> unitcommit : unit -> bool\end{ttbox}\begin{ttdescription}\item[\ttindexbold{quit}();] ends the Isabelle session, without saving the state.\item[\ttindexbold{exit} \(i\);] similar to {\tt quit}, passing return code \(i\) to the operating system.\item[\ttindexbold{commit}();] saves the current state without ending the session, provided that the logic image is opened read-write; return value {\tt false} indicates an error.\end{ttdescription}Typing control-D also finishes the session in essentially the same wayas the sequence {\tt commit(); quit();} would.\section{Reading ML files}\index{files!reading}\begin{ttbox} cd : string -> unitpwd : unit -> stringuse : string -> unittime_use : string -> unit\end{ttbox}\begin{ttdescription}\item[\ttindexbold{cd} "{\it dir}";] changes the current directory to {\it dir}. This is the default directory for reading files.\item[\ttindexbold{pwd}();] returns the full path of the current directory.\item[\ttindexbold{use} "$file$";] reads the given {\it file} as input to the \ML{} session. Reading a fileof Isabelle commands is the usual way of replaying a proof.\item[\ttindexbold{time_use} "$file$";] performs {\tt use~"$file$"} and prints the total execution time.\end{ttdescription}The $dir$ and $file$ specifications of the \texttt{cd} and \texttt{use}commands may contain path variables (e.g.\ \texttt{\$ISABELLE_HOME}) that areexpanded appropriately. Note that \texttt{\~\relax} abbreviates\texttt{\$HOME}, and \texttt{\~\relax\~\relax} abbreviates\texttt{\$ISABELLE_HOME}\index{*\$ISABELLE_HOME}. The syntax for pathspecifications follows Unix conventions.\section{Reading theories}\label{sec:intro-theories}\index{theories!reading}In Isabelle, any kind of declarations, definitions, etc.\ are organized aroundnamed \emph{theory} objects. Logical reasoning always takes place within acertain theory context, which may be switched at any time. Theory $name$ isdefined by a theory file $name$\texttt{.thy}, containing declarations of\texttt{consts}, \texttt{types}, \texttt{defs}, etc.\ (see\S\ref{sec:ref-defining-theories} for more details on concrete syntax).Furthermore, there may be an associated {\ML} file $name$\texttt{.ML} withproof scripts that are to be run in the context of the theory.\begin{ttbox}context : theory -> unitthe_context : unit -> theorytheory : string -> theoryuse_thy : string -> unittime_use_thy : string -> unitupdate_thy : string -> unit\end{ttbox}\begin{ttdescription}\item[\ttindexbold{context} $thy$;] switches the current theory context. Any subsequent command with ``implicit theory argument'' (e.g.\ \texttt{Goal}) will refer to $thy$ as its theory.\item[\ttindexbold{the_context}();] obtains the current theory context, or raises an error if absent.\item[\ttindexbold{theory} "$name$";] retrieves the theory called $name$ from the internal data\-base of loaded theories, raising an error if absent.\item[\ttindexbold{use_thy} "$name$";] reads theory $name$ from the file system, looking for $name$\texttt{.thy} and $name$\texttt{.ML} (the latter being optional). It also ensures that all parent theories are loaded as well. In case some older versions have already been present, \texttt{use_thy} only tries to reload $name$ itself, but is content with any version of its ancestors.\item[\ttindexbold{time_use_thy} "$name$";] same as \texttt{use_thy}, but reports the time taken to process the actual theory parts and {\ML} files separately.\item[\ttindexbold{update_thy} "$name$";] is similar to \texttt{use_thy}, but ensures that theory $name$ is fully up-to-date with respect to the file system --- apart from theory $name$ itself, any of its ancestors may be reloaded as well.\end{ttdescription}Note that theories of pre-built logic images (e.g.\ HOL) are marked as\emph{finished} and cannot be updated any more. See \S\ref{sec:more-theories}for further information on Isabelle's theory loader.\section{Setting flags}\begin{ttbox}set : bool ref -> boolreset : bool ref -> booltoggle : bool ref -> bool\end{ttbox}\index{*set}\index{*reset}\index{*toggle}These are some shorthands for manipulating boolean references. The newvalue is returned.\section{Diagnostic messages}\index{error messages}\index{warnings}Isabelle conceptually provides three output channels for different kinds ofmessages: ordinary text, warnings, errors. Depending on the user interfaceinvolved, these messages may appear in different text styles or colours.The default setup of an \texttt{isabelle} terminal session is asfollows: plain output of ordinary text, warnings prefixed by\texttt{\#\#\#}'s, errors prefixed by \texttt{***}'s. For example, atypical warning would look like this:\begin{ttbox}\#\#\# Beware the Jabberwock, my son!\#\#\# The jaws that bite, the claws that catch!\#\#\# Beware the Jubjub Bird, and shun\#\#\# The frumious Bandersnatch!\end{ttbox}\texttt{ML} programs may output diagnostic messages using thefollowing functions:\begin{ttbox}writeln : string -> unitwarning : string -> uniterror : string -> 'a\end{ttbox}Note that \ttindex{error} fails by raising exception \ttindex{ERROR}after having output the text, while \ttindex{writeln} and\ttindex{warning} resume normal program execution.\section{Timing}\index{timing statistics}\index{proofs!timing}\begin{ttbox} timing: bool ref \hfill{\bf initially false}\end{ttbox}\begin{ttdescription}\item[set \ttindexbold{timing};] enables global timing in Isabelle. This information is compiler-dependent.\end{ttdescription}\index{sessions|)}%%% Local Variables: %%% mode: latex%%% TeX-master: "ref"%%% End: