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: