doc-src/IsarRef/intro.tex
 author haftmann Fri Dec 29 12:11:04 2006 +0100 (2006-12-29) changeset 21927 9677abe5d374 parent 21703 a9fdad55a53d permissions -rw-r--r--
added handling for explicit classrel witnesses
     1

     2 \chapter{Introduction}

     3

     4 \section{Overview}

     5

     6 The \emph{Isabelle} system essentially provides a generic infrastructure for

     7 building deductive systems (programmed in Standard ML), with a special focus

     8 on interactive theorem proving in higher-order logics.  In the olden days even

     9 end-users would refer to certain ML functions (goal commands, tactics,

    10 tacticals etc.) to pursue their everyday theorem proving tasks

    11 \cite{isabelle-intro,isabelle-ref}.

    12

    13 In contrast \emph{Isar} provides an interpreted language environment of its

    14 own, which has been specifically tailored for the needs of theory and proof

    15 development.  Compared to raw ML, the Isabelle/Isar top-level provides a more

    16 robust and comfortable development platform, with proper support for theory

    17 development graphs, single-step transactions with unlimited undo, etc.  The

    18 Isabelle/Isar version of the \emph{Proof~General} user interface

    19 \cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate front-end for

    20 interactive theory and proof development in this advanced theorem proving

    21 environment.

    22

    23 \medskip Apart from the technical advances over bare-bones ML programming, the

    24 main purpose of the Isar language is to provide a conceptually different view

    25 on machine-checked proofs \cite{Wenzel:1999:TPHOL,Wenzel-PhD}.  Isar''

    26 stands for Intelligible semi-automated reasoning''.  Drawing from both the

    27 traditions of informal mathematical proof texts and high-level programming

    28 languages, Isar offers a versatile environment for structured formal proof

    29 documents.  Thus properly written Isar proofs become accessible to a broader

    30 audience than unstructured tactic scripts (which typically only provide

    31 operational information for the machine).  Writing human-readable proof texts

    32 certainly requires some additional efforts by the writer to achieve a good

    33 presentation, both of formal and informal parts of the text.  On the other

    34 hand, human-readable formal texts gain some value in their own right,

    35 independently of the mechanic proof-checking process.

    36

    37 Despite its grand design of structured proof texts, Isar is able to assimilate

    38 the old tactical style as an improper'' sub-language.  This provides an easy

    39 upgrade path for existing tactic scripts, as well as additional means for

    40 interactive experimentation and debugging of structured proofs.  Isabelle/Isar

    41 supports a broad range of proof styles, both readable and unreadable ones.

    42

    43 \medskip The Isabelle/Isar framework is generic and should work reasonably

    44 well for any Isabelle object-logic that conforms to the natural deduction view

    45 of the Isabelle/Pure framework.  Major Isabelle logics like HOL

    46 \cite{isabelle-HOL}, HOLCF \cite{MuellerNvOS99}, FOL \cite{isabelle-logics},

    47 and ZF \cite{isabelle-ZF} have already been set up for end-users.

    48 Nonetheless, much of the existing body of theories still consist of old-style

    49 theory files with accompanied ML code for proof scripts; this legacy will be

    50 gradually converted in due time.

    51

    52

    53 \section{Quick start}

    54

    55 \subsection{Terminal sessions}

    56

    57 Isar is already part of Isabelle.  The low-level \texttt{isabelle} binary

    58 provides option \texttt{-I} to run the Isabelle/Isar interaction loop at

    59 startup, rather than the raw ML top-level.  So the most basic way to do

    60 anything with Isabelle/Isar is as follows:

    61 \begin{ttbox}

    62 isabelle -I HOL\medskip

    63 \out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip

    64 theory Foo imports Main begin;

    65 constdefs foo :: nat  "foo == 1";

    66 lemma "0 < foo" by (simp add: foo_def);

    67 end;

    68 \end{ttbox}

    69 Note that any Isabelle/Isar command may be retracted by \texttt{undo}.  See

    70 the Isabelle/Isar Quick Reference (appendix~\ref{ap:refcard}) for a

    71 comprehensive overview of available commands and other language elements.

    72

    73

    74 \subsection{Proof~General}

    75

    76 Plain TTY-based interaction as above used to be quite feasible with

    77 traditional tactic based theorem proving, but developing Isar documents really

    78 demands some better user-interface support.  The Proof~General environment by

    79 David Aspinall \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs

    80 interface for interactive theorem provers that organizes all the cut-and-paste

    81 and forward-backward walk through the text in a very neat way.  In

    82 Isabelle/Isar, the current position within a partial proof document is equally

    83 important than the actual proof state.  Thus Proof~General provides the

    84 canonical working environment for Isabelle/Isar, both for getting acquainted

    85 (e.g.\ by replaying existing Isar documents) and for production work.

    86

    87

    88 \subsubsection{Proof~General as default Isabelle interface}

    89

    90 The Isabelle interface wrapper script provides an easy way to invoke

    91 Proof~General (including XEmacs or GNU Emacs).  The default

    92 configuration of Isabelle is smart enough to detect the Proof~General

    93 distribution in several canonical places (e.g.\

    94 \texttt{\$ISABELLE_HOME/contrib/ProofGeneral}). Thus the capital   95 \texttt{Isabelle} executable would already refer to the   96 \texttt{ProofGeneral/isar} interface without further ado. The   97 Isabelle interface script provides several options; pass \verb,-?, to   98 see its usage.   99   100 With the proper Isabelle interface setup, Isar documents may now be edited by   101 visiting appropriate theory files, e.g.\   102 \begin{ttbox}   103 Isabelle $${\langle}isabellehome{\rangle}$$/src/HOL/Isar_examples/Summation.thy   104 \end{ttbox}   105 Beginners may note the tool bar for navigating forward and backward through   106 the text (this depends on the local Emacs installation). Consult the   107 Proof~General documentation \cite{proofgeneral} for further basic command   108 sequences, in particular \texttt{C-c C-return}'' and \texttt{C-c u}''.   109   110 \medskip   111   112 Proof~General may be also configured manually by giving Isabelle settings like   113 this (see also \cite{isabelle-sys}):   114 \begin{ttbox}   115 ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface

   116 PROOFGENERAL_OPTIONS=""

   117 \end{ttbox}

   118 You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the   119 actual installation directory of Proof~General.   120   121 \medskip   122   123 Apart from the Isabelle command line, defaults for interface options may be   124 given by the \texttt{PROOFGENERAL_OPTIONS} setting. For example, the Emacs   125 executable to be used may be configured in Isabelle's settings like this:   126 \begin{ttbox}   127 PROOFGENERAL_OPTIONS="-p xemacs-mule"   128 \end{ttbox}   129   130 Occasionally, a user's \verb,~/.emacs, file contains code that is incompatible   131 with the (X)Emacs version used by Proof~General, causing the interface startup   132 to fail prematurely. Here the \texttt{-u false} option helps to get the   133 interface process up and running. Note that additional Lisp customization   134 code may reside in \texttt{proofgeneral-settings.el} of   135 \texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc}.   136   137   138 \subsubsection{The X-Symbol package}   139   140 Proof~General provides native support for the Emacs X-Symbol package   141 \cite{x-symbol}, which handles proper mathematical symbols displayed on   142 screen. Pass option \texttt{-x true} to the Isabelle interface script, or   143 check the appropriate Proof~General menu setting by hand. In any case, the   144 X-Symbol package must have been properly installed already.   145   146 Contrary to what you may expect from the documentation of X-Symbol, the   147 package is very easy to install and configures itself automatically. The   148 default configuration of Isabelle is smart enough to detect the X-Symbol   149 package in several canonical places (e.g.\   150 \texttt{\$ISABELLE_HOME/contrib/x-symbol}).

   151

   152 \medskip

   153

   154 Using proper mathematical symbols in Isabelle theories can be very convenient

   155 for readability of large formulas.  On the other hand, the plain ASCII sources

   156 easily become somewhat unintelligible.  For example, $\Longrightarrow$ would

   157 appear as \verb,\<Longrightarrow>, according the default set of Isabelle

   158 symbols.  Nevertheless, the Isabelle document preparation system (see

   159 \S\ref{sec:document-prep}) will be happy to print non-ASCII symbols properly.

   160 It is even possible to invent additional notation beyond the display

   161 capabilities of Emacs and X-Symbol.

   162

   163

   164 \section{Isabelle/Isar theories}

   165

   166 Isabelle/Isar offers the following main improvements over classic Isabelle.

   167 \begin{enumerate}

   168

   169 \item A new \emph{theory format}, occasionally referred to as new-style

   170   theories'', supporting interactive development and unlimited undo operation.

   171

   172 \item A \emph{formal proof document language} designed to support intelligible

   173   semi-automated reasoning.  Instead of putting together unreadable tactic

   174   scripts, the author is enabled to express the reasoning in way that is close

   175   to usual mathematical practice.  The old tactical style has been assimilated

   176   as improper'' language elements.

   177

   178 \item A simple document preparation system, for typesetting formal

   179   developments together with informal text.  The resulting hyper-linked PDF

   180   documents are equally well suited for WWW presentation and as printed

   181   copies.

   182

   183 \end{enumerate}

   184

   185 The Isar proof language is embedded into the new theory format as a proper

   186 sub-language.  Proof mode is entered by stating some $\THEOREMNAME$ or

   187 $\LEMMANAME$ at the theory level, and left again with the final conclusion

   188 (e.g.\ via $\QEDNAME$).  A few theory specification mechanisms also require

   189 some proof, such as HOL's $\isarkeyword{typedef}$ which demands non-emptiness

   190 of the representing sets.

   191

   192 New-style theory files may still be associated with separate ML files

   193 consisting of plain old tactic scripts.  There is no longer any ML binding

   194 generated for the theory and theorems, though.  ML functions \texttt{theory},

   195 \texttt{thm}, and \texttt{thms} retrieve this information from the context

   196 \cite{isabelle-ref}.  Nevertheless, migration between classic Isabelle and

   197 Isabelle/Isar is relatively easy.  Thus users may start to benefit from

   198 interactive theory development and document preparation, even before they have

   199 any idea of the Isar proof language at all.

   200

   201 \begin{warn}

   202   Proof~General does \emph{not} support mixed interactive development of

   203   classic Isabelle theory files or tactic scripts, together with Isar

   204   documents.  The \texttt{isa}'' and \texttt{isar}'' versions of

   205   Proof~General are handled as two different theorem proving systems, only one

   206   of these may be active at the same time.

   207 \end{warn}

   208

   209 Manual conversion of existing tactic scripts may be done by running two

   210 separate Proof~General sessions, one for replaying the old script and the

   211 other for the emerging Isabelle/Isar document.  Also note that Isar supports

   212 emulation commands and methods that support traditional tactic scripts within

   213 new-style theories, see appendix~\ref{ap:conv} for more information.

   214

   215

   216 \subsection{Document preparation}\label{sec:document-prep}

   217

   218 Isabelle/Isar provides a simple document preparation system based on existing

   219 {PDF-\LaTeX} technology, with full support of hyper-links (both local

   220 references and URLs), bookmarks, and thumbnails.  Thus the results are equally

   221 well suited for WWW browsing and as printed copies.

   222

   223 \medskip

   224

   225 Isabelle generates {\LaTeX} output as part of the run of a \emph{logic

   226   session} (see also \cite{isabelle-sys}).  Getting started with a working

   227 configuration for common situations is quite easy by using the Isabelle

   228 \texttt{mkdir} and \texttt{make} tools.  First invoke

   229 \begin{ttbox}

   230   isatool mkdir Foo

   231 \end{ttbox}

   232 to initialize a separate directory for session \texttt{Foo} --- it is safe to

   233 experiment, since \texttt{isatool mkdir} never overwrites existing files.

   234 Ensure that \texttt{Foo/ROOT.ML} holds ML commands to load all theories

   235 required for this session; furthermore \texttt{Foo/document/root.tex} should

   236 include any special {\LaTeX} macro packages required for your document (the

   237 default is usually sufficient as a start).

   238

   239 The session is controlled by a separate \texttt{IsaMakefile} (with crude

   240 source dependencies by default).  This file is located one level up from the

   241 \texttt{Foo} directory location.  Now invoke

   242 \begin{ttbox}

   243   isatool make Foo

   244 \end{ttbox}

   245 to run the \texttt{Foo} session, with browser information and document

   246 preparation enabled.  Unless any errors are reported by Isabelle or {\LaTeX},

   247 the output will appear inside the directory \texttt{ISABELLE_BROWSER_INFO}, as

   248 reported by the batch job in verbose mode.

   249

   250 \medskip

   251

   252 You may also consider to tune the \texttt{usedir} options in

   253 \texttt{IsaMakefile}, for example to change the output format from

   254 \texttt{pdf} to \texttt{dvi}, or activate the \texttt{-D} option to retain a

   255 second copy of the generated {\LaTeX} sources.

   256

   257 \medskip

   258

   259 See \emph{The Isabelle System Manual} \cite{isabelle-sys} for further details

   260 on Isabelle logic sessions and theory presentation.  The Isabelle/HOL tutorial

   261 \cite{isabelle-hol-book} also covers theory presentation issues.

   262

   263

   264 \subsection{How to write Isar proofs anyway?}\label{sec:isar-howto}

   265

   266 This is one of the key questions, of course.  First of all, the tactic script

   267 emulation of Isabelle/Isar essentially provides a clarified version of the

   268 very same unstructured proof style of classic Isabelle.  Old-time users should

   269 quickly become acquainted with that (slightly degenerative) view of Isar.

   270

   271 Writing \emph{proper} Isar proof texts targeted at human readers is quite

   272 different, though.  Experienced users of the unstructured style may even have

   273 to unlearn some of their habits to master proof composition in Isar.  In

   274 contrast, new users with less experience in old-style tactical proving, but a

   275 good understanding of mathematical proof in general, often get started easier.

   276

   277 \medskip The present text really is only a reference manual on Isabelle/Isar,

   278 not a tutorial.  Nevertheless, we will attempt to give some clues of how the

   279 concepts introduced here may be put into practice.  Appendix~\ref{ap:refcard}

   280 provides a quick reference card of the most common Isabelle/Isar language

   281 elements.  Appendix~\ref{ap:conv} offers some practical hints on converting

   282 existing Isabelle theories and proof scripts to the new format (without

   283 restructuring proofs).

   284

   285 Further issues concerning the Isar concepts are covered in the literature

   286 \cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.

   287 The author's PhD thesis \cite{Wenzel-PhD} presently provides the most complete

   288 exposition of Isar foundations, techniques, and applications.  A number of

   289 example applications are distributed with Isabelle, and available via the

   290 Isabelle WWW library (e.g.\ \url{http://isabelle.in.tum.de/library/}).  As a

   291 general rule of thumb, more recent Isabelle applications that also include a

   292 separate document'' (in PDF) are more likely to consist of proper

   293 Isabelle/Isar theories and proofs.

   294

   295 %FIXME

   296 % The following examples may be of particular interest.  Apart from the plain

   297 % sources represented in HTML, these Isabelle sessions also provide actual

   298 % documents (in PDF).

   299 % \begin{itemize}

   300 % \item \url{http://isabelle.in.tum.de/library/HOL/Isar_examples/} is a

   301 %   collection of introductory examples.

   302 % \item \url{http://isabelle.in.tum.de/library/HOL/Lattice/} is an example of

   303 %   typical mathematics-style reasoning in axiomatic'' structures.

   304 % \item \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/HahnBanach/} is a

   305 %   big mathematics application on infinitary vector spaces and functional

   306 %   analysis.

   307 % \item \url{http://isabelle.in.tum.de/library/HOL/Lambda/} develops fundamental

   308 %   properties of $\lambda$-calculus (Church-Rosser and termination).

   309

   310 %   This may serve as a realistic example of porting of legacy proof scripts

   311 %   into Isar tactic emulation scripts.

   312 % \item \url{http://isabelle.in.tum.de/library/HOL/Unix/} gives a mathematical

   313 %   model of the main aspects of the Unix file-system including its security

   314 %   model, but ignoring processes.  A few odd effects caused by the general

   315 %   worse-is-better'' approach followed in Unix are discussed within the

   316 %   formal model.

   317

   318 %   This example represents a non-trivial verification task, with all proofs

   319 %   carefully worked out using the proper part of the Isar proof language;

   320 %   unstructured scripts are only used for symbolic evaluation.

   321 % \item \url{http://isabelle.in.tum.de/library/HOL/MicroJava/} is a

   322 %   formalization of a fragment of Java, together with a corresponding virtual

   323 %   machine and a specification of its bytecode verifier and a lightweight

   324 %   bytecode verifier, including proofs of type-safety.

   325

   326 %   This represents a very realistic'' example of large formalizations

   327 %   performed in form of tactic emulation scripts and proper Isar proof texts.

   328 % \end{itemize}

   329

   330

   331 %%% Local Variables:

   332 %%% mode: latex

   333 %%% TeX-master: "isar-ref"

   334 %%% End: