1.1 --- a/doc-src/IsarRef/intro.tex Tue Apr 22 22:00:31 2008 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,334 +0,0 @@
1.4 -
1.5 -\chapter{Introduction}
1.6 -
1.7 -\section{Overview}
1.8 -
1.9 -The \emph{Isabelle} system essentially provides a generic infrastructure for
1.10 -building deductive systems (programmed in Standard ML), with a special focus
1.11 -on interactive theorem proving in higher-order logics. In the olden days even
1.12 -end-users would refer to certain ML functions (goal commands, tactics,
1.13 -tacticals etc.) to pursue their everyday theorem proving tasks
1.14 -\cite{isabelle-intro,isabelle-ref}.
1.15 -
1.16 -In contrast \emph{Isar} provides an interpreted language environment of its
1.17 -own, which has been specifically tailored for the needs of theory and proof
1.18 -development. Compared to raw ML, the Isabelle/Isar top-level provides a more
1.19 -robust and comfortable development platform, with proper support for theory
1.20 -development graphs, single-step transactions with unlimited undo, etc. The
1.21 -Isabelle/Isar version of the \emph{Proof~General} user interface
1.22 -\cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate front-end for
1.23 -interactive theory and proof development in this advanced theorem proving
1.24 -environment.
1.25 -
1.26 -\medskip Apart from the technical advances over bare-bones ML programming, the
1.27 -main purpose of the Isar language is to provide a conceptually different view
1.28 -on machine-checked proofs \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. ``Isar''
1.29 -stands for ``Intelligible semi-automated reasoning''. Drawing from both the
1.30 -traditions of informal mathematical proof texts and high-level programming
1.31 -languages, Isar offers a versatile environment for structured formal proof
1.32 -documents. Thus properly written Isar proofs become accessible to a broader
1.33 -audience than unstructured tactic scripts (which typically only provide
1.34 -operational information for the machine). Writing human-readable proof texts
1.35 -certainly requires some additional efforts by the writer to achieve a good
1.36 -presentation, both of formal and informal parts of the text. On the other
1.37 -hand, human-readable formal texts gain some value in their own right,
1.38 -independently of the mechanic proof-checking process.
1.39 -
1.40 -Despite its grand design of structured proof texts, Isar is able to assimilate
1.41 -the old tactical style as an ``improper'' sub-language. This provides an easy
1.42 -upgrade path for existing tactic scripts, as well as additional means for
1.43 -interactive experimentation and debugging of structured proofs. Isabelle/Isar
1.44 -supports a broad range of proof styles, both readable and unreadable ones.
1.45 -
1.46 -\medskip The Isabelle/Isar framework is generic and should work reasonably
1.47 -well for any Isabelle object-logic that conforms to the natural deduction view
1.48 -of the Isabelle/Pure framework. Major Isabelle logics like HOL
1.49 -\cite{isabelle-HOL}, HOLCF \cite{MuellerNvOS99}, FOL \cite{isabelle-logics},
1.50 -and ZF \cite{isabelle-ZF} have already been set up for end-users.
1.51 -Nonetheless, much of the existing body of theories still consist of old-style
1.52 -theory files with accompanied ML code for proof scripts; this legacy will be
1.53 -gradually converted in due time.
1.54 -
1.55 -
1.56 -\section{Quick start}
1.57 -
1.58 -\subsection{Terminal sessions}
1.59 -
1.60 -Isar is already part of Isabelle. The low-level \texttt{isabelle} binary
1.61 -provides option \texttt{-I} to run the Isabelle/Isar interaction loop at
1.62 -startup, rather than the raw ML top-level. So the most basic way to do
1.63 -anything with Isabelle/Isar is as follows:
1.64 -\begin{ttbox}
1.65 -isabelle -I HOL\medskip
1.66 -\out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip
1.67 -theory Foo imports Main begin;
1.68 -constdefs foo :: nat "foo == 1";
1.69 -lemma "0 < foo" by (simp add: foo_def);
1.70 -end;
1.71 -\end{ttbox}
1.72 -Note that any Isabelle/Isar command may be retracted by \texttt{undo}. See
1.73 -the Isabelle/Isar Quick Reference (appendix~\ref{ap:refcard}) for a
1.74 -comprehensive overview of available commands and other language elements.
1.75 -
1.76 -
1.77 -\subsection{Proof~General}
1.78 -
1.79 -Plain TTY-based interaction as above used to be quite feasible with
1.80 -traditional tactic based theorem proving, but developing Isar documents really
1.81 -demands some better user-interface support. The Proof~General environment by
1.82 -David Aspinall \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
1.83 -interface for interactive theorem provers that organizes all the cut-and-paste
1.84 -and forward-backward walk through the text in a very neat way. In
1.85 -Isabelle/Isar, the current position within a partial proof document is equally
1.86 -important than the actual proof state. Thus Proof~General provides the
1.87 -canonical working environment for Isabelle/Isar, both for getting acquainted
1.88 -(e.g.\ by replaying existing Isar documents) and for production work.
1.89 -
1.90 -
1.91 -\subsubsection{Proof~General as default Isabelle interface}
1.92 -
1.93 -The Isabelle interface wrapper script provides an easy way to invoke
1.94 -Proof~General (including XEmacs or GNU Emacs). The default
1.95 -configuration of Isabelle is smart enough to detect the Proof~General
1.96 -distribution in several canonical places (e.g.\
1.97 -\texttt{\$ISABELLE_HOME/contrib/ProofGeneral}). Thus the capital
1.98 -\texttt{Isabelle} executable would already refer to the
1.99 -\texttt{ProofGeneral/isar} interface without further ado. The
1.100 -Isabelle interface script provides several options; pass \verb,-?, to
1.101 -see its usage.
1.102 -
1.103 -With the proper Isabelle interface setup, Isar documents may now be edited by
1.104 -visiting appropriate theory files, e.g.\
1.105 -\begin{ttbox}
1.106 -Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
1.107 -\end{ttbox}
1.108 -Beginners may note the tool bar for navigating forward and backward through
1.109 -the text (this depends on the local Emacs installation). Consult the
1.110 -Proof~General documentation \cite{proofgeneral} for further basic command
1.111 -sequences, in particular ``\texttt{C-c C-return}'' and ``\texttt{C-c u}''.
1.112 -
1.113 -\medskip
1.114 -
1.115 -Proof~General may be also configured manually by giving Isabelle settings like
1.116 -this (see also \cite{isabelle-sys}):
1.117 -\begin{ttbox}
1.118 -ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
1.119 -PROOFGENERAL_OPTIONS=""
1.120 -\end{ttbox}
1.121 -You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
1.122 -actual installation directory of Proof~General.
1.123 -
1.124 -\medskip
1.125 -
1.126 -Apart from the Isabelle command line, defaults for interface options may be
1.127 -given by the \texttt{PROOFGENERAL_OPTIONS} setting. For example, the Emacs
1.128 -executable to be used may be configured in Isabelle's settings like this:
1.129 -\begin{ttbox}
1.130 -PROOFGENERAL_OPTIONS="-p xemacs-mule"
1.131 -\end{ttbox}
1.132 -
1.133 -Occasionally, a user's \verb,~/.emacs, file contains code that is incompatible
1.134 -with the (X)Emacs version used by Proof~General, causing the interface startup
1.135 -to fail prematurely. Here the \texttt{-u false} option helps to get the
1.136 -interface process up and running. Note that additional Lisp customization
1.137 -code may reside in \texttt{proofgeneral-settings.el} of
1.138 -\texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc}.
1.139 -
1.140 -
1.141 -\subsubsection{The X-Symbol package}
1.142 -
1.143 -Proof~General provides native support for the Emacs X-Symbol package
1.144 -\cite{x-symbol}, which handles proper mathematical symbols displayed on
1.145 -screen. Pass option \texttt{-x true} to the Isabelle interface script, or
1.146 -check the appropriate Proof~General menu setting by hand. In any case, the
1.147 -X-Symbol package must have been properly installed already.
1.148 -
1.149 -Contrary to what you may expect from the documentation of X-Symbol, the
1.150 -package is very easy to install and configures itself automatically. The
1.151 -default configuration of Isabelle is smart enough to detect the X-Symbol
1.152 -package in several canonical places (e.g.\
1.153 -\texttt{\$ISABELLE_HOME/contrib/x-symbol}).
1.154 -
1.155 -\medskip
1.156 -
1.157 -Using proper mathematical symbols in Isabelle theories can be very convenient
1.158 -for readability of large formulas. On the other hand, the plain ASCII sources
1.159 -easily become somewhat unintelligible. For example, $\Longrightarrow$ would
1.160 -appear as \verb,\<Longrightarrow>, according the default set of Isabelle
1.161 -symbols. Nevertheless, the Isabelle document preparation system (see
1.162 -\S\ref{sec:document-prep}) will be happy to print non-ASCII symbols properly.
1.163 -It is even possible to invent additional notation beyond the display
1.164 -capabilities of Emacs and X-Symbol.
1.165 -
1.166 -
1.167 -\section{Isabelle/Isar theories}
1.168 -
1.169 -Isabelle/Isar offers the following main improvements over classic Isabelle.
1.170 -\begin{enumerate}
1.171 -
1.172 -\item A new \emph{theory format}, occasionally referred to as ``new-style
1.173 - theories'', supporting interactive development and unlimited undo operation.
1.174 -
1.175 -\item A \emph{formal proof document language} designed to support intelligible
1.176 - semi-automated reasoning. Instead of putting together unreadable tactic
1.177 - scripts, the author is enabled to express the reasoning in way that is close
1.178 - to usual mathematical practice. The old tactical style has been assimilated
1.179 - as ``improper'' language elements.
1.180 -
1.181 -\item A simple document preparation system, for typesetting formal
1.182 - developments together with informal text. The resulting hyper-linked PDF
1.183 - documents are equally well suited for WWW presentation and as printed
1.184 - copies.
1.185 -
1.186 -\end{enumerate}
1.187 -
1.188 -The Isar proof language is embedded into the new theory format as a proper
1.189 -sub-language. Proof mode is entered by stating some $\THEOREMNAME$ or
1.190 -$\LEMMANAME$ at the theory level, and left again with the final conclusion
1.191 -(e.g.\ via $\QEDNAME$). A few theory specification mechanisms also require
1.192 -some proof, such as HOL's $\isarkeyword{typedef}$ which demands non-emptiness
1.193 -of the representing sets.
1.194 -
1.195 -New-style theory files may still be associated with separate ML files
1.196 -consisting of plain old tactic scripts. There is no longer any ML binding
1.197 -generated for the theory and theorems, though. ML functions \texttt{theory},
1.198 -\texttt{thm}, and \texttt{thms} retrieve this information from the context
1.199 -\cite{isabelle-ref}. Nevertheless, migration between classic Isabelle and
1.200 -Isabelle/Isar is relatively easy. Thus users may start to benefit from
1.201 -interactive theory development and document preparation, even before they have
1.202 -any idea of the Isar proof language at all.
1.203 -
1.204 -\begin{warn}
1.205 - Proof~General does \emph{not} support mixed interactive development of
1.206 - classic Isabelle theory files or tactic scripts, together with Isar
1.207 - documents. The ``\texttt{isa}'' and ``\texttt{isar}'' versions of
1.208 - Proof~General are handled as two different theorem proving systems, only one
1.209 - of these may be active at the same time.
1.210 -\end{warn}
1.211 -
1.212 -Manual conversion of existing tactic scripts may be done by running two
1.213 -separate Proof~General sessions, one for replaying the old script and the
1.214 -other for the emerging Isabelle/Isar document. Also note that Isar supports
1.215 -emulation commands and methods that support traditional tactic scripts within
1.216 -new-style theories, see appendix~\ref{ap:conv} for more information.
1.217 -
1.218 -
1.219 -\subsection{Document preparation}\label{sec:document-prep}
1.220 -
1.221 -Isabelle/Isar provides a simple document preparation system based on existing
1.222 -{PDF-\LaTeX} technology, with full support of hyper-links (both local
1.223 -references and URLs), bookmarks, and thumbnails. Thus the results are equally
1.224 -well suited for WWW browsing and as printed copies.
1.225 -
1.226 -\medskip
1.227 -
1.228 -Isabelle generates {\LaTeX} output as part of the run of a \emph{logic
1.229 - session} (see also \cite{isabelle-sys}). Getting started with a working
1.230 -configuration for common situations is quite easy by using the Isabelle
1.231 -\texttt{mkdir} and \texttt{make} tools. First invoke
1.232 -\begin{ttbox}
1.233 - isatool mkdir Foo
1.234 -\end{ttbox}
1.235 -to initialize a separate directory for session \texttt{Foo} --- it is safe to
1.236 -experiment, since \texttt{isatool mkdir} never overwrites existing files.
1.237 -Ensure that \texttt{Foo/ROOT.ML} holds ML commands to load all theories
1.238 -required for this session; furthermore \texttt{Foo/document/root.tex} should
1.239 -include any special {\LaTeX} macro packages required for your document (the
1.240 -default is usually sufficient as a start).
1.241 -
1.242 -The session is controlled by a separate \texttt{IsaMakefile} (with crude
1.243 -source dependencies by default). This file is located one level up from the
1.244 -\texttt{Foo} directory location. Now invoke
1.245 -\begin{ttbox}
1.246 - isatool make Foo
1.247 -\end{ttbox}
1.248 -to run the \texttt{Foo} session, with browser information and document
1.249 -preparation enabled. Unless any errors are reported by Isabelle or {\LaTeX},
1.250 -the output will appear inside the directory \texttt{ISABELLE_BROWSER_INFO}, as
1.251 -reported by the batch job in verbose mode.
1.252 -
1.253 -\medskip
1.254 -
1.255 -You may also consider to tune the \texttt{usedir} options in
1.256 -\texttt{IsaMakefile}, for example to change the output format from
1.257 -\texttt{pdf} to \texttt{dvi}, or activate the \texttt{-D} option to retain a
1.258 -second copy of the generated {\LaTeX} sources.
1.259 -
1.260 -\medskip
1.261 -
1.262 -See \emph{The Isabelle System Manual} \cite{isabelle-sys} for further details
1.263 -on Isabelle logic sessions and theory presentation. The Isabelle/HOL tutorial
1.264 -\cite{isabelle-hol-book} also covers theory presentation issues.
1.265 -
1.266 -
1.267 -\subsection{How to write Isar proofs anyway?}\label{sec:isar-howto}
1.268 -
1.269 -This is one of the key questions, of course. First of all, the tactic script
1.270 -emulation of Isabelle/Isar essentially provides a clarified version of the
1.271 -very same unstructured proof style of classic Isabelle. Old-time users should
1.272 -quickly become acquainted with that (slightly degenerative) view of Isar.
1.273 -
1.274 -Writing \emph{proper} Isar proof texts targeted at human readers is quite
1.275 -different, though. Experienced users of the unstructured style may even have
1.276 -to unlearn some of their habits to master proof composition in Isar. In
1.277 -contrast, new users with less experience in old-style tactical proving, but a
1.278 -good understanding of mathematical proof in general, often get started easier.
1.279 -
1.280 -\medskip The present text really is only a reference manual on Isabelle/Isar,
1.281 -not a tutorial. Nevertheless, we will attempt to give some clues of how the
1.282 -concepts introduced here may be put into practice. Appendix~\ref{ap:refcard}
1.283 -provides a quick reference card of the most common Isabelle/Isar language
1.284 -elements. Appendix~\ref{ap:conv} offers some practical hints on converting
1.285 -existing Isabelle theories and proof scripts to the new format (without
1.286 -restructuring proofs).
1.287 -
1.288 -Further issues concerning the Isar concepts are covered in the literature
1.289 -\cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
1.290 -The author's PhD thesis \cite{Wenzel-PhD} presently provides the most complete
1.291 -exposition of Isar foundations, techniques, and applications. A number of
1.292 -example applications are distributed with Isabelle, and available via the
1.293 -Isabelle WWW library (e.g.\ \url{http://isabelle.in.tum.de/library/}). As a
1.294 -general rule of thumb, more recent Isabelle applications that also include a
1.295 -separate ``document'' (in PDF) are more likely to consist of proper
1.296 -Isabelle/Isar theories and proofs.
1.297 -
1.298 -%FIXME
1.299 -% The following examples may be of particular interest. Apart from the plain
1.300 -% sources represented in HTML, these Isabelle sessions also provide actual
1.301 -% documents (in PDF).
1.302 -% \begin{itemize}
1.303 -% \item \url{http://isabelle.in.tum.de/library/HOL/Isar_examples/} is a
1.304 -% collection of introductory examples.
1.305 -% \item \url{http://isabelle.in.tum.de/library/HOL/Lattice/} is an example of
1.306 -% typical mathematics-style reasoning in ``axiomatic'' structures.
1.307 -% \item \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/HahnBanach/} is a
1.308 -% big mathematics application on infinitary vector spaces and functional
1.309 -% analysis.
1.310 -% \item \url{http://isabelle.in.tum.de/library/HOL/Lambda/} develops fundamental
1.311 -% properties of $\lambda$-calculus (Church-Rosser and termination).
1.312 -
1.313 -% This may serve as a realistic example of porting of legacy proof scripts
1.314 -% into Isar tactic emulation scripts.
1.315 -% \item \url{http://isabelle.in.tum.de/library/HOL/Unix/} gives a mathematical
1.316 -% model of the main aspects of the Unix file-system including its security
1.317 -% model, but ignoring processes. A few odd effects caused by the general
1.318 -% ``worse-is-better'' approach followed in Unix are discussed within the
1.319 -% formal model.
1.320 -
1.321 -% This example represents a non-trivial verification task, with all proofs
1.322 -% carefully worked out using the proper part of the Isar proof language;
1.323 -% unstructured scripts are only used for symbolic evaluation.
1.324 -% \item \url{http://isabelle.in.tum.de/library/HOL/MicroJava/} is a
1.325 -% formalization of a fragment of Java, together with a corresponding virtual
1.326 -% machine and a specification of its bytecode verifier and a lightweight
1.327 -% bytecode verifier, including proofs of type-safety.
1.328 -
1.329 -% This represents a very ``realistic'' example of large formalizations
1.330 -% performed in form of tactic emulation scripts and proper Isar proof texts.
1.331 -% \end{itemize}
1.332 -
1.333 -
1.334 -%%% Local Variables:
1.335 -%%% mode: latex
1.336 -%%% TeX-master: "isar-ref"
1.337 -%%% End: