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