1.1 --- a/doc-src/IsarRef/IsaMakefile Tue Apr 22 22:00:31 2008 +0200
1.2 +++ b/doc-src/IsarRef/IsaMakefile Wed Apr 23 12:13:08 2008 +0200
1.3 @@ -21,7 +21,7 @@
1.4
1.5 Thy: $(LOG)/Pure-Thy.gz
1.6
1.7 -$(LOG)/Pure-Thy.gz: Thy/ROOT.ML ../antiquote_setup.ML
1.8 +$(LOG)/Pure-Thy.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/intro.thy
1.9 @$(USEDIR) Pure Thy
1.10
1.11
2.1 --- a/doc-src/IsarRef/Makefile Tue Apr 22 22:00:31 2008 +0200
2.2 +++ b/doc-src/IsarRef/Makefile Wed Apr 23 12:13:08 2008 +0200
2.3 @@ -13,7 +13,7 @@
2.4
2.5 NAME = isar-ref
2.6
2.7 -FILES = isar-ref.tex intro.tex basics.tex syntax.tex pure.tex \
2.8 +FILES = isar-ref.tex Thy/document/intro.tex basics.tex syntax.tex pure.tex \
2.9 generic.tex logics.tex refcard.tex conversion.tex \
2.10 ../isar.sty ../rail.sty ../railsetup.sty ../proof.sty \
2.11 ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
3.1 --- a/doc-src/IsarRef/Thy/ROOT.ML Tue Apr 22 22:00:31 2008 +0200
3.2 +++ b/doc-src/IsarRef/Thy/ROOT.ML Wed Apr 23 12:13:08 2008 +0200
3.3 @@ -1,2 +1,5 @@
3.4
3.5 (* $Id$ *)
3.6 +
3.7 +use "../../antiquote_setup.ML";
3.8 +use_thy "intro";
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/doc-src/IsarRef/Thy/document/intro.tex Wed Apr 23 12:13:08 2008 +0200
4.3 @@ -0,0 +1,376 @@
4.4 +%
4.5 +\begin{isabellebody}%
4.6 +\def\isabellecontext{intro}%
4.7 +%
4.8 +\isadelimtheory
4.9 +\isanewline
4.10 +%
4.11 +\endisadelimtheory
4.12 +%
4.13 +\isatagtheory
4.14 +\isacommand{theory}\isamarkupfalse%
4.15 +\ intro\isanewline
4.16 +\isakeyword{imports}\ CPure\isanewline
4.17 +\isakeyword{begin}%
4.18 +\endisatagtheory
4.19 +{\isafoldtheory}%
4.20 +%
4.21 +\isadelimtheory
4.22 +%
4.23 +\endisadelimtheory
4.24 +%
4.25 +\isamarkupchapter{Introduction%
4.26 +}
4.27 +\isamarkuptrue%
4.28 +%
4.29 +\isamarkupsection{Overview%
4.30 +}
4.31 +\isamarkuptrue%
4.32 +%
4.33 +\begin{isamarkuptext}%
4.34 +The \emph{Isabelle} system essentially provides a generic
4.35 + infrastructure for building deductive systems (programmed in
4.36 + Standard ML), with a special focus on interactive theorem proving in
4.37 + higher-order logics. In the olden days even end-users would refer
4.38 + to certain ML functions (goal commands, tactics, tacticals etc.) to
4.39 + pursue their everyday theorem proving tasks
4.40 + \cite{isabelle-intro,isabelle-ref}.
4.41 +
4.42 + In contrast \emph{Isar} provides an interpreted language environment
4.43 + of its own, which has been specifically tailored for the needs of
4.44 + theory and proof development. Compared to raw ML, the Isabelle/Isar
4.45 + top-level provides a more robust and comfortable development
4.46 + platform, with proper support for theory development graphs,
4.47 + single-step transactions with unlimited undo, etc. The
4.48 + Isabelle/Isar version of the \emph{Proof~General} user interface
4.49 + \cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate
4.50 + front-end for interactive theory and proof development in this
4.51 + advanced theorem proving environment.
4.52 +
4.53 + \medskip Apart from the technical advances over bare-bones ML
4.54 + programming, the main purpose of the Isar language is to provide a
4.55 + conceptually different view on machine-checked proofs
4.56 + \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. ``Isar'' stands for
4.57 + ``Intelligible semi-automated reasoning''. Drawing from both the
4.58 + traditions of informal mathematical proof texts and high-level
4.59 + programming languages, Isar offers a versatile environment for
4.60 + structured formal proof documents. Thus properly written Isar
4.61 + proofs become accessible to a broader audience than unstructured
4.62 + tactic scripts (which typically only provide operational information
4.63 + for the machine). Writing human-readable proof texts certainly
4.64 + requires some additional efforts by the writer to achieve a good
4.65 + presentation, both of formal and informal parts of the text. On the
4.66 + other hand, human-readable formal texts gain some value in their own
4.67 + right, independently of the mechanic proof-checking process.
4.68 +
4.69 + Despite its grand design of structured proof texts, Isar is able to
4.70 + assimilate the old tactical style as an ``improper'' sub-language.
4.71 + This provides an easy upgrade path for existing tactic scripts, as
4.72 + well as additional means for interactive experimentation and
4.73 + debugging of structured proofs. Isabelle/Isar supports a broad
4.74 + range of proof styles, both readable and unreadable ones.
4.75 +
4.76 + \medskip The Isabelle/Isar framework is generic and should work
4.77 + reasonably well for any Isabelle object-logic that conforms to the
4.78 + natural deduction view of the Isabelle/Pure framework. Major
4.79 + Isabelle logics like HOL \cite{isabelle-HOL}, HOLCF
4.80 + \cite{MuellerNvOS99}, FOL \cite{isabelle-logics}, and ZF
4.81 + \cite{isabelle-ZF} have already been set up for end-users.%
4.82 +\end{isamarkuptext}%
4.83 +\isamarkuptrue%
4.84 +%
4.85 +\isamarkupsection{Quick start%
4.86 +}
4.87 +\isamarkuptrue%
4.88 +%
4.89 +\isamarkupsubsection{Terminal sessions%
4.90 +}
4.91 +\isamarkuptrue%
4.92 +%
4.93 +\begin{isamarkuptext}%
4.94 +Isar is already part of Isabelle. The low-level \texttt{isabelle} binary
4.95 + provides option \texttt{-I} to run the Isabelle/Isar interaction loop at
4.96 + startup, rather than the raw ML top-level. So the most basic way to do
4.97 + anything with Isabelle/Isar is as follows:
4.98 +\begin{ttbox}
4.99 +isabelle -I HOL\medskip
4.100 +\out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip
4.101 +theory Foo imports Main begin;
4.102 +definition foo :: nat where "foo == 1";
4.103 +lemma "0 < foo" by (simp add: foo_def);
4.104 +end;
4.105 +\end{ttbox}
4.106 +
4.107 + Note that any Isabelle/Isar command may be retracted by
4.108 + \texttt{undo}. See the Isabelle/Isar Quick Reference
4.109 + (appendix~\ref{ap:refcard}) for a comprehensive overview of
4.110 + available commands and other language elements.%
4.111 +\end{isamarkuptext}%
4.112 +\isamarkuptrue%
4.113 +%
4.114 +\isamarkupsubsection{Proof General%
4.115 +}
4.116 +\isamarkuptrue%
4.117 +%
4.118 +\begin{isamarkuptext}%
4.119 +Plain TTY-based interaction as above used to be quite feasible with
4.120 + traditional tactic based theorem proving, but developing Isar
4.121 + documents really demands some better user-interface support. The
4.122 + Proof~General environment by David Aspinall
4.123 + \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
4.124 + interface for interactive theorem provers that organizes all the
4.125 + cut-and-paste and forward-backward walk through the text in a very
4.126 + neat way. In Isabelle/Isar, the current position within a partial
4.127 + proof document is equally important than the actual proof state.
4.128 + Thus Proof~General provides the canonical working environment for
4.129 + Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
4.130 + existing Isar documents) and for production work.%
4.131 +\end{isamarkuptext}%
4.132 +\isamarkuptrue%
4.133 +%
4.134 +\isamarkupsubsubsection{Proof~General as default Isabelle interface%
4.135 +}
4.136 +\isamarkuptrue%
4.137 +%
4.138 +\begin{isamarkuptext}%
4.139 +The Isabelle interface wrapper script provides an easy way to invoke
4.140 + Proof~General (including XEmacs or GNU Emacs). The default
4.141 + configuration of Isabelle is smart enough to detect the
4.142 + Proof~General distribution in several canonical places (e.g.\
4.143 + \texttt{\$ISABELLE_HOME/contrib/ProofGeneral}). Thus the capital
4.144 + \texttt{Isabelle} executable would already refer to the
4.145 + \texttt{ProofGeneral/isar} interface without further ado. The
4.146 + Isabelle interface script provides several options; pass \verb,-?,
4.147 + to see its usage.
4.148 +
4.149 + With the proper Isabelle interface setup, Isar documents may now be edited by
4.150 + visiting appropriate theory files, e.g.\
4.151 +\begin{ttbox}
4.152 +Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
4.153 +\end{ttbox}
4.154 + Beginners may note the tool bar for navigating forward and backward
4.155 + through the text (this depends on the local Emacs installation).
4.156 + Consult the Proof~General documentation \cite{proofgeneral} for
4.157 + further basic command sequences, in particular ``\texttt{C-c
4.158 + C-return}'' and ``\texttt{C-c u}''.
4.159 +
4.160 + \medskip Proof~General may be also configured manually by giving
4.161 + Isabelle settings like this (see also \cite{isabelle-sys}):
4.162 +
4.163 +\begin{ttbox}
4.164 +ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
4.165 +PROOFGENERAL_OPTIONS=""
4.166 +\end{ttbox}
4.167 + You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral}
4.168 + to the actual installation directory of Proof~General.
4.169 +
4.170 + \medskip Apart from the Isabelle command line, defaults for
4.171 + interface options may be given by the \texttt{PROOFGENERAL_OPTIONS}
4.172 + setting. For example, the Emacs executable to be used may be
4.173 + configured in Isabelle's settings like this:
4.174 +\begin{ttbox}
4.175 +PROOFGENERAL_OPTIONS="-p xemacs-mule"
4.176 +\end{ttbox}
4.177 +
4.178 + Occasionally, a user's \verb,~/.emacs, file contains code that is
4.179 + incompatible with the (X)Emacs version used by Proof~General,
4.180 + causing the interface startup to fail prematurely. Here the
4.181 + \texttt{-u false} option helps to get the interface process up and
4.182 + running. Note that additional Lisp customization code may reside in
4.183 + \texttt{proofgeneral-settings.el} of \texttt{\$ISABELLE_HOME/etc} or
4.184 + \texttt{\$ISABELLE_HOME_USER/etc}.%
4.185 +\end{isamarkuptext}%
4.186 +\isamarkuptrue%
4.187 +%
4.188 +\isamarkupsubsubsection{The X-Symbol package%
4.189 +}
4.190 +\isamarkuptrue%
4.191 +%
4.192 +\begin{isamarkuptext}%
4.193 +Proof~General incorporates a version of the Emacs X-Symbol package
4.194 + \cite{x-symbol}, which handles proper mathematical symbols displayed
4.195 + on screen. Pass option \texttt{-x true} to the Isabelle interface
4.196 + script, or check the appropriate Proof~General menu setting by hand.
4.197 + The main challenge of getting X-Symbol to work properly is the
4.198 + underlying (semi-automated) X11 font setup.
4.199 +
4.200 + \medskip Using proper mathematical symbols in Isabelle theories can
4.201 + be very convenient for readability of large formulas. On the other
4.202 + hand, the plain ASCII sources easily become somewhat unintelligible.
4.203 + For example, $\Longrightarrow$ would appear as \verb,\<Longrightarrow>, according
4.204 + the default set of Isabelle symbols. Nevertheless, the Isabelle
4.205 + document preparation system (see \S\ref{sec:document-prep}) will be
4.206 + happy to print non-ASCII symbols properly. It is even possible to
4.207 + invent additional notation beyond the display capabilities of Emacs
4.208 + and X-Symbol.%
4.209 +\end{isamarkuptext}%
4.210 +\isamarkuptrue%
4.211 +%
4.212 +\isamarkupsection{Isabelle/Isar theories%
4.213 +}
4.214 +\isamarkuptrue%
4.215 +%
4.216 +\begin{isamarkuptext}%
4.217 +Isabelle/Isar offers the following main improvements over classic
4.218 + Isabelle.
4.219 +
4.220 + \begin{enumerate}
4.221 +
4.222 + \item A \emph{theory format} that integrates specifications and
4.223 + proofs, supporting interactive development and unlimited undo
4.224 + operation.
4.225 +
4.226 + \item A \emph{formal proof document language} designed to support
4.227 + intelligible semi-automated reasoning. Instead of putting together
4.228 + unreadable tactic scripts, the author is enabled to express the
4.229 + reasoning in way that is close to usual mathematical practice. The
4.230 + old tactical style has been assimilated as ``improper'' language
4.231 + elements.
4.232 +
4.233 + \item A simple document preparation system, for typesetting formal
4.234 + developments together with informal text. The resulting
4.235 + hyper-linked PDF documents are equally well suited for WWW
4.236 + presentation and as printed copies.
4.237 +
4.238 + \end{enumerate}
4.239 +
4.240 + The Isar proof language is embedded into the new theory format as a
4.241 + proper sub-language. Proof mode is entered by stating some
4.242 + $\THEOREMNAME$ or $\LEMMANAME$ at the theory level, and left again
4.243 + with the final conclusion (e.g.\ via $\QEDNAME$). A few theory
4.244 + specification mechanisms also require some proof, such as HOL's
4.245 + $\isarkeyword{typedef}$ which demands non-emptiness of the
4.246 + representing sets.
4.247 +
4.248 + New-style theory files may still be associated with separate ML
4.249 + files consisting of plain old tactic scripts. There is no longer
4.250 + any ML binding generated for the theory and theorems, though. ML
4.251 + functions \texttt{theory}, \texttt{thm}, and \texttt{thms} retrieve
4.252 + this information from the context \cite{isabelle-ref}.
4.253 + Nevertheless, migration between classic Isabelle and Isabelle/Isar
4.254 + is relatively easy. Thus users may start to benefit from
4.255 + interactive theory development and document preparation, even before
4.256 + they have any idea of the Isar proof language at all.
4.257 +
4.258 + Manual conversion of existing tactic scripts may be done by running
4.259 + two separate Proof~General sessions, one for replaying the old
4.260 + script and the other for the emerging Isabelle/Isar document. Also
4.261 + note that Isar supports emulation commands and methods that support
4.262 + traditional tactic scripts within new-style theories, see
4.263 + appendix~\ref{ap:conv} for more information.%
4.264 +\end{isamarkuptext}%
4.265 +\isamarkuptrue%
4.266 +%
4.267 +\isamarkupsubsection{Document preparation \label{sec:document-prep}%
4.268 +}
4.269 +\isamarkuptrue%
4.270 +%
4.271 +\begin{isamarkuptext}%
4.272 +Isabelle/Isar provides a simple document preparation system based on
4.273 + existing {PDF-\LaTeX} technology, with full support of hyper-links
4.274 + (both local references and URLs), bookmarks, and thumbnails. Thus
4.275 + the results are equally well suited for WWW browsing and as printed
4.276 + copies.
4.277 +
4.278 + \medskip
4.279 +
4.280 + Isabelle generates {\LaTeX} output as part of the run of a
4.281 + \emph{logic session} (see also \cite{isabelle-sys}). Getting
4.282 + started with a working configuration for common situations is quite
4.283 + easy by using the Isabelle \texttt{mkdir} and \texttt{make} tools.
4.284 + First invoke
4.285 +\begin{ttbox}
4.286 + isatool mkdir Foo
4.287 +\end{ttbox}
4.288 + to initialize a separate directory for session \texttt{Foo} --- it
4.289 + is safe to experiment, since \texttt{isatool mkdir} never overwrites
4.290 + existing files. Ensure that \texttt{Foo/ROOT.ML} holds ML commands
4.291 + to load all theories required for this session; furthermore
4.292 + \texttt{Foo/document/root.tex} should include any special {\LaTeX}
4.293 + macro packages required for your document (the default is usually
4.294 + sufficient as a start).
4.295 +
4.296 + The session is controlled by a separate \texttt{IsaMakefile} (with
4.297 + crude source dependencies by default). This file is located one
4.298 + level up from the \texttt{Foo} directory location. Now invoke
4.299 +\begin{ttbox}
4.300 + isatool make Foo
4.301 +\end{ttbox}
4.302 + to run the \texttt{Foo} session, with browser information and
4.303 + document preparation enabled. Unless any errors are reported by
4.304 + Isabelle or {\LaTeX}, the output will appear inside the directory
4.305 + \texttt{ISABELLE_BROWSER_INFO}, as reported by the batch job in
4.306 + verbose mode.
4.307 +
4.308 + \medskip You may also consider to tune the \texttt{usedir} options
4.309 + in \texttt{IsaMakefile}, for example to change the output format
4.310 + from \texttt{pdf} to \texttt{dvi}, or activate the \texttt{-D}
4.311 + option to retain a second copy of the generated {\LaTeX} sources.
4.312 +
4.313 + \medskip See \emph{The Isabelle System Manual} \cite{isabelle-sys}
4.314 + for further details on Isabelle logic sessions and theory
4.315 + presentation. The Isabelle/HOL tutorial \cite{isabelle-hol-book}
4.316 + also covers theory presentation issues.%
4.317 +\end{isamarkuptext}%
4.318 +\isamarkuptrue%
4.319 +%
4.320 +\isamarkupsubsection{How to write Isar proofs anyway? \label{sec:isar-howto}%
4.321 +}
4.322 +\isamarkuptrue%
4.323 +%
4.324 +\begin{isamarkuptext}%
4.325 +This is one of the key questions, of course. First of all, the
4.326 + tactic script emulation of Isabelle/Isar essentially provides a
4.327 + clarified version of the very same unstructured proof style of
4.328 + classic Isabelle. Old-time users should quickly become acquainted
4.329 + with that (slightly degenerative) view of Isar.
4.330 +
4.331 + Writing \emph{proper} Isar proof texts targeted at human readers is
4.332 + quite different, though. Experienced users of the unstructured
4.333 + style may even have to unlearn some of their habits to master proof
4.334 + composition in Isar. In contrast, new users with less experience in
4.335 + old-style tactical proving, but a good understanding of mathematical
4.336 + proof in general, often get started easier.
4.337 +
4.338 + \medskip The present text really is only a reference manual on
4.339 + Isabelle/Isar, not a tutorial. Nevertheless, we will attempt to
4.340 + give some clues of how the concepts introduced here may be put into
4.341 + practice. Appendix~\ref{ap:refcard} provides a quick reference card
4.342 + of the most common Isabelle/Isar language elements.
4.343 + Appendix~\ref{ap:conv} offers some practical hints on converting
4.344 + existing Isabelle theories and proof scripts to the new format
4.345 + (without restructuring proofs).
4.346 +
4.347 + Further issues concerning the Isar concepts are covered in the
4.348 + literature
4.349 + \cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
4.350 + The author's PhD thesis \cite{Wenzel-PhD} presently provides the
4.351 + most complete exposition of Isar foundations, techniques, and
4.352 + applications. A number of example applications are distributed with
4.353 + Isabelle, and available via the Isabelle WWW library (e.g.\
4.354 + \url{http://isabelle.in.tum.de/library/}). The ``Archive of Formal
4.355 + Proofs'' \url{http://afp.sourceforge.net/} also provides plenty of
4.356 + examples, both in proper Isar proof style and unstructured tactic
4.357 + scripts.%
4.358 +\end{isamarkuptext}%
4.359 +\isamarkuptrue%
4.360 +%
4.361 +\isadelimtheory
4.362 +%
4.363 +\endisadelimtheory
4.364 +%
4.365 +\isatagtheory
4.366 +\isacommand{end}\isamarkupfalse%
4.367 +%
4.368 +\endisatagtheory
4.369 +{\isafoldtheory}%
4.370 +%
4.371 +\isadelimtheory
4.372 +%
4.373 +\endisadelimtheory
4.374 +\isanewline
4.375 +\end{isabellebody}%
4.376 +%%% Local Variables:
4.377 +%%% mode: latex
4.378 +%%% TeX-master: "root"
4.379 +%%% End:
5.1 --- a/doc-src/IsarRef/Thy/document/session.tex Tue Apr 22 22:00:31 2008 +0200
5.2 +++ b/doc-src/IsarRef/Thy/document/session.tex Wed Apr 23 12:13:08 2008 +0200
5.3 @@ -1,3 +1,5 @@
5.4 +\input{intro.tex}
5.5 +
5.6 %%% Local Variables:
5.7 %%% mode: latex
5.8 %%% TeX-master: "root"
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/doc-src/IsarRef/Thy/intro.thy Wed Apr 23 12:13:08 2008 +0200
6.3 @@ -0,0 +1,321 @@
6.4 +
6.5 +theory intro
6.6 +imports CPure
6.7 +begin
6.8 +
6.9 +chapter {* Introduction *}
6.10 +
6.11 +section {* Overview *}
6.12 +
6.13 +text {*
6.14 + The \emph{Isabelle} system essentially provides a generic
6.15 + infrastructure for building deductive systems (programmed in
6.16 + Standard ML), with a special focus on interactive theorem proving in
6.17 + higher-order logics. In the olden days even end-users would refer
6.18 + to certain ML functions (goal commands, tactics, tacticals etc.) to
6.19 + pursue their everyday theorem proving tasks
6.20 + \cite{isabelle-intro,isabelle-ref}.
6.21 +
6.22 + In contrast \emph{Isar} provides an interpreted language environment
6.23 + of its own, which has been specifically tailored for the needs of
6.24 + theory and proof development. Compared to raw ML, the Isabelle/Isar
6.25 + top-level provides a more robust and comfortable development
6.26 + platform, with proper support for theory development graphs,
6.27 + single-step transactions with unlimited undo, etc. The
6.28 + Isabelle/Isar version of the \emph{Proof~General} user interface
6.29 + \cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate
6.30 + front-end for interactive theory and proof development in this
6.31 + advanced theorem proving environment.
6.32 +
6.33 + \medskip Apart from the technical advances over bare-bones ML
6.34 + programming, the main purpose of the Isar language is to provide a
6.35 + conceptually different view on machine-checked proofs
6.36 + \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. ``Isar'' stands for
6.37 + ``Intelligible semi-automated reasoning''. Drawing from both the
6.38 + traditions of informal mathematical proof texts and high-level
6.39 + programming languages, Isar offers a versatile environment for
6.40 + structured formal proof documents. Thus properly written Isar
6.41 + proofs become accessible to a broader audience than unstructured
6.42 + tactic scripts (which typically only provide operational information
6.43 + for the machine). Writing human-readable proof texts certainly
6.44 + requires some additional efforts by the writer to achieve a good
6.45 + presentation, both of formal and informal parts of the text. On the
6.46 + other hand, human-readable formal texts gain some value in their own
6.47 + right, independently of the mechanic proof-checking process.
6.48 +
6.49 + Despite its grand design of structured proof texts, Isar is able to
6.50 + assimilate the old tactical style as an ``improper'' sub-language.
6.51 + This provides an easy upgrade path for existing tactic scripts, as
6.52 + well as additional means for interactive experimentation and
6.53 + debugging of structured proofs. Isabelle/Isar supports a broad
6.54 + range of proof styles, both readable and unreadable ones.
6.55 +
6.56 + \medskip The Isabelle/Isar framework is generic and should work
6.57 + reasonably well for any Isabelle object-logic that conforms to the
6.58 + natural deduction view of the Isabelle/Pure framework. Major
6.59 + Isabelle logics like HOL \cite{isabelle-HOL}, HOLCF
6.60 + \cite{MuellerNvOS99}, FOL \cite{isabelle-logics}, and ZF
6.61 + \cite{isabelle-ZF} have already been set up for end-users.
6.62 +*}
6.63 +
6.64 +
6.65 +section {* Quick start *}
6.66 +
6.67 +subsection {* Terminal sessions *}
6.68 +
6.69 +text {*
6.70 + Isar is already part of Isabelle. The low-level \texttt{isabelle} binary
6.71 + provides option \texttt{-I} to run the Isabelle/Isar interaction loop at
6.72 + startup, rather than the raw ML top-level. So the most basic way to do
6.73 + anything with Isabelle/Isar is as follows:
6.74 +\begin{ttbox}
6.75 +isabelle -I HOL\medskip
6.76 +\out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip
6.77 +theory Foo imports Main begin;
6.78 +definition foo :: nat where "foo == 1";
6.79 +lemma "0 < foo" by (simp add: foo_def);
6.80 +end;
6.81 +\end{ttbox}
6.82 +
6.83 + Note that any Isabelle/Isar command may be retracted by
6.84 + \texttt{undo}. See the Isabelle/Isar Quick Reference
6.85 + (appendix~\ref{ap:refcard}) for a comprehensive overview of
6.86 + available commands and other language elements.
6.87 +*}
6.88 +
6.89 +
6.90 +subsection {* Proof General *}
6.91 +
6.92 +text {*
6.93 + Plain TTY-based interaction as above used to be quite feasible with
6.94 + traditional tactic based theorem proving, but developing Isar
6.95 + documents really demands some better user-interface support. The
6.96 + Proof~General environment by David Aspinall
6.97 + \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
6.98 + interface for interactive theorem provers that organizes all the
6.99 + cut-and-paste and forward-backward walk through the text in a very
6.100 + neat way. In Isabelle/Isar, the current position within a partial
6.101 + proof document is equally important than the actual proof state.
6.102 + Thus Proof~General provides the canonical working environment for
6.103 + Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
6.104 + existing Isar documents) and for production work.
6.105 +*}
6.106 +
6.107 +
6.108 +subsubsection{* Proof~General as default Isabelle interface *}
6.109 +
6.110 +text {*
6.111 + The Isabelle interface wrapper script provides an easy way to invoke
6.112 + Proof~General (including XEmacs or GNU Emacs). The default
6.113 + configuration of Isabelle is smart enough to detect the
6.114 + Proof~General distribution in several canonical places (e.g.\
6.115 + \texttt{\$ISABELLE_HOME/contrib/ProofGeneral}). Thus the capital
6.116 + \texttt{Isabelle} executable would already refer to the
6.117 + \texttt{ProofGeneral/isar} interface without further ado. The
6.118 + Isabelle interface script provides several options; pass \verb,-?,
6.119 + to see its usage.
6.120 +
6.121 + With the proper Isabelle interface setup, Isar documents may now be edited by
6.122 + visiting appropriate theory files, e.g.\
6.123 +\begin{ttbox}
6.124 +Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
6.125 +\end{ttbox}
6.126 + Beginners may note the tool bar for navigating forward and backward
6.127 + through the text (this depends on the local Emacs installation).
6.128 + Consult the Proof~General documentation \cite{proofgeneral} for
6.129 + further basic command sequences, in particular ``\texttt{C-c
6.130 + C-return}'' and ``\texttt{C-c u}''.
6.131 +
6.132 + \medskip Proof~General may be also configured manually by giving
6.133 + Isabelle settings like this (see also \cite{isabelle-sys}):
6.134 +
6.135 +\begin{ttbox}
6.136 +ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
6.137 +PROOFGENERAL_OPTIONS=""
6.138 +\end{ttbox}
6.139 + You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral}
6.140 + to the actual installation directory of Proof~General.
6.141 +
6.142 + \medskip Apart from the Isabelle command line, defaults for
6.143 + interface options may be given by the \texttt{PROOFGENERAL_OPTIONS}
6.144 + setting. For example, the Emacs executable to be used may be
6.145 + configured in Isabelle's settings like this:
6.146 +\begin{ttbox}
6.147 +PROOFGENERAL_OPTIONS="-p xemacs-mule"
6.148 +\end{ttbox}
6.149 +
6.150 + Occasionally, a user's \verb,~/.emacs, file contains code that is
6.151 + incompatible with the (X)Emacs version used by Proof~General,
6.152 + causing the interface startup to fail prematurely. Here the
6.153 + \texttt{-u false} option helps to get the interface process up and
6.154 + running. Note that additional Lisp customization code may reside in
6.155 + \texttt{proofgeneral-settings.el} of \texttt{\$ISABELLE_HOME/etc} or
6.156 + \texttt{\$ISABELLE_HOME_USER/etc}.
6.157 +*}
6.158 +
6.159 +
6.160 +subsubsection {* The X-Symbol package *}
6.161 +
6.162 +text {*
6.163 + Proof~General incorporates a version of the Emacs X-Symbol package
6.164 + \cite{x-symbol}, which handles proper mathematical symbols displayed
6.165 + on screen. Pass option \texttt{-x true} to the Isabelle interface
6.166 + script, or check the appropriate Proof~General menu setting by hand.
6.167 + The main challenge of getting X-Symbol to work properly is the
6.168 + underlying (semi-automated) X11 font setup.
6.169 +
6.170 + \medskip Using proper mathematical symbols in Isabelle theories can
6.171 + be very convenient for readability of large formulas. On the other
6.172 + hand, the plain ASCII sources easily become somewhat unintelligible.
6.173 + For example, $\Longrightarrow$ would appear as \verb,\<Longrightarrow>, according
6.174 + the default set of Isabelle symbols. Nevertheless, the Isabelle
6.175 + document preparation system (see \S\ref{sec:document-prep}) will be
6.176 + happy to print non-ASCII symbols properly. It is even possible to
6.177 + invent additional notation beyond the display capabilities of Emacs
6.178 + and X-Symbol.
6.179 +*}
6.180 +
6.181 +
6.182 +section {* Isabelle/Isar theories *}
6.183 +
6.184 +text {*
6.185 + Isabelle/Isar offers the following main improvements over classic
6.186 + Isabelle.
6.187 +
6.188 + \begin{enumerate}
6.189 +
6.190 + \item A \emph{theory format} that integrates specifications and
6.191 + proofs, supporting interactive development and unlimited undo
6.192 + operation.
6.193 +
6.194 + \item A \emph{formal proof document language} designed to support
6.195 + intelligible semi-automated reasoning. Instead of putting together
6.196 + unreadable tactic scripts, the author is enabled to express the
6.197 + reasoning in way that is close to usual mathematical practice. The
6.198 + old tactical style has been assimilated as ``improper'' language
6.199 + elements.
6.200 +
6.201 + \item A simple document preparation system, for typesetting formal
6.202 + developments together with informal text. The resulting
6.203 + hyper-linked PDF documents are equally well suited for WWW
6.204 + presentation and as printed copies.
6.205 +
6.206 + \end{enumerate}
6.207 +
6.208 + The Isar proof language is embedded into the new theory format as a
6.209 + proper sub-language. Proof mode is entered by stating some
6.210 + $\THEOREMNAME$ or $\LEMMANAME$ at the theory level, and left again
6.211 + with the final conclusion (e.g.\ via $\QEDNAME$). A few theory
6.212 + specification mechanisms also require some proof, such as HOL's
6.213 + $\isarkeyword{typedef}$ which demands non-emptiness of the
6.214 + representing sets.
6.215 +
6.216 + New-style theory files may still be associated with separate ML
6.217 + files consisting of plain old tactic scripts. There is no longer
6.218 + any ML binding generated for the theory and theorems, though. ML
6.219 + functions \texttt{theory}, \texttt{thm}, and \texttt{thms} retrieve
6.220 + this information from the context \cite{isabelle-ref}.
6.221 + Nevertheless, migration between classic Isabelle and Isabelle/Isar
6.222 + is relatively easy. Thus users may start to benefit from
6.223 + interactive theory development and document preparation, even before
6.224 + they have any idea of the Isar proof language at all.
6.225 +
6.226 + Manual conversion of existing tactic scripts may be done by running
6.227 + two separate Proof~General sessions, one for replaying the old
6.228 + script and the other for the emerging Isabelle/Isar document. Also
6.229 + note that Isar supports emulation commands and methods that support
6.230 + traditional tactic scripts within new-style theories, see
6.231 + appendix~\ref{ap:conv} for more information.
6.232 +*}
6.233 +
6.234 +
6.235 +subsection {* Document preparation \label{sec:document-prep} *}
6.236 +
6.237 +text {*
6.238 + Isabelle/Isar provides a simple document preparation system based on
6.239 + existing {PDF-\LaTeX} technology, with full support of hyper-links
6.240 + (both local references and URLs), bookmarks, and thumbnails. Thus
6.241 + the results are equally well suited for WWW browsing and as printed
6.242 + copies.
6.243 +
6.244 + \medskip
6.245 +
6.246 + Isabelle generates {\LaTeX} output as part of the run of a
6.247 + \emph{logic session} (see also \cite{isabelle-sys}). Getting
6.248 + started with a working configuration for common situations is quite
6.249 + easy by using the Isabelle \texttt{mkdir} and \texttt{make} tools.
6.250 + First invoke
6.251 +\begin{ttbox}
6.252 + isatool mkdir Foo
6.253 +\end{ttbox}
6.254 + to initialize a separate directory for session \texttt{Foo} --- it
6.255 + is safe to experiment, since \texttt{isatool mkdir} never overwrites
6.256 + existing files. Ensure that \texttt{Foo/ROOT.ML} holds ML commands
6.257 + to load all theories required for this session; furthermore
6.258 + \texttt{Foo/document/root.tex} should include any special {\LaTeX}
6.259 + macro packages required for your document (the default is usually
6.260 + sufficient as a start).
6.261 +
6.262 + The session is controlled by a separate \texttt{IsaMakefile} (with
6.263 + crude source dependencies by default). This file is located one
6.264 + level up from the \texttt{Foo} directory location. Now invoke
6.265 +\begin{ttbox}
6.266 + isatool make Foo
6.267 +\end{ttbox}
6.268 + to run the \texttt{Foo} session, with browser information and
6.269 + document preparation enabled. Unless any errors are reported by
6.270 + Isabelle or {\LaTeX}, the output will appear inside the directory
6.271 + \texttt{ISABELLE_BROWSER_INFO}, as reported by the batch job in
6.272 + verbose mode.
6.273 +
6.274 + \medskip You may also consider to tune the \texttt{usedir} options
6.275 + in \texttt{IsaMakefile}, for example to change the output format
6.276 + from \texttt{pdf} to \texttt{dvi}, or activate the \texttt{-D}
6.277 + option to retain a second copy of the generated {\LaTeX} sources.
6.278 +
6.279 + \medskip See \emph{The Isabelle System Manual} \cite{isabelle-sys}
6.280 + for further details on Isabelle logic sessions and theory
6.281 + presentation. The Isabelle/HOL tutorial \cite{isabelle-hol-book}
6.282 + also covers theory presentation issues.
6.283 +*}
6.284 +
6.285 +
6.286 +subsection {* How to write Isar proofs anyway? \label{sec:isar-howto} *}
6.287 +
6.288 +text {*
6.289 + This is one of the key questions, of course. First of all, the
6.290 + tactic script emulation of Isabelle/Isar essentially provides a
6.291 + clarified version of the very same unstructured proof style of
6.292 + classic Isabelle. Old-time users should quickly become acquainted
6.293 + with that (slightly degenerative) view of Isar.
6.294 +
6.295 + Writing \emph{proper} Isar proof texts targeted at human readers is
6.296 + quite different, though. Experienced users of the unstructured
6.297 + style may even have to unlearn some of their habits to master proof
6.298 + composition in Isar. In contrast, new users with less experience in
6.299 + old-style tactical proving, but a good understanding of mathematical
6.300 + proof in general, often get started easier.
6.301 +
6.302 + \medskip The present text really is only a reference manual on
6.303 + Isabelle/Isar, not a tutorial. Nevertheless, we will attempt to
6.304 + give some clues of how the concepts introduced here may be put into
6.305 + practice. Appendix~\ref{ap:refcard} provides a quick reference card
6.306 + of the most common Isabelle/Isar language elements.
6.307 + Appendix~\ref{ap:conv} offers some practical hints on converting
6.308 + existing Isabelle theories and proof scripts to the new format
6.309 + (without restructuring proofs).
6.310 +
6.311 + Further issues concerning the Isar concepts are covered in the
6.312 + literature
6.313 + \cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
6.314 + The author's PhD thesis \cite{Wenzel-PhD} presently provides the
6.315 + most complete exposition of Isar foundations, techniques, and
6.316 + applications. A number of example applications are distributed with
6.317 + Isabelle, and available via the Isabelle WWW library (e.g.\
6.318 + \url{http://isabelle.in.tum.de/library/}). The ``Archive of Formal
6.319 + Proofs'' \url{http://afp.sourceforge.net/} also provides plenty of
6.320 + examples, both in proper Isar proof style and unstructured tactic
6.321 + scripts.
6.322 +*}
6.323 +
6.324 +end
7.1 --- a/doc-src/IsarRef/intro.tex Tue Apr 22 22:00:31 2008 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,334 +0,0 @@
7.4 -
7.5 -\chapter{Introduction}
7.6 -
7.7 -\section{Overview}
7.8 -
7.9 -The \emph{Isabelle} system essentially provides a generic infrastructure for
7.10 -building deductive systems (programmed in Standard ML), with a special focus
7.11 -on interactive theorem proving in higher-order logics. In the olden days even
7.12 -end-users would refer to certain ML functions (goal commands, tactics,
7.13 -tacticals etc.) to pursue their everyday theorem proving tasks
7.14 -\cite{isabelle-intro,isabelle-ref}.
7.15 -
7.16 -In contrast \emph{Isar} provides an interpreted language environment of its
7.17 -own, which has been specifically tailored for the needs of theory and proof
7.18 -development. Compared to raw ML, the Isabelle/Isar top-level provides a more
7.19 -robust and comfortable development platform, with proper support for theory
7.20 -development graphs, single-step transactions with unlimited undo, etc. The
7.21 -Isabelle/Isar version of the \emph{Proof~General} user interface
7.22 -\cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate front-end for
7.23 -interactive theory and proof development in this advanced theorem proving
7.24 -environment.
7.25 -
7.26 -\medskip Apart from the technical advances over bare-bones ML programming, the
7.27 -main purpose of the Isar language is to provide a conceptually different view
7.28 -on machine-checked proofs \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. ``Isar''
7.29 -stands for ``Intelligible semi-automated reasoning''. Drawing from both the
7.30 -traditions of informal mathematical proof texts and high-level programming
7.31 -languages, Isar offers a versatile environment for structured formal proof
7.32 -documents. Thus properly written Isar proofs become accessible to a broader
7.33 -audience than unstructured tactic scripts (which typically only provide
7.34 -operational information for the machine). Writing human-readable proof texts
7.35 -certainly requires some additional efforts by the writer to achieve a good
7.36 -presentation, both of formal and informal parts of the text. On the other
7.37 -hand, human-readable formal texts gain some value in their own right,
7.38 -independently of the mechanic proof-checking process.
7.39 -
7.40 -Despite its grand design of structured proof texts, Isar is able to assimilate
7.41 -the old tactical style as an ``improper'' sub-language. This provides an easy
7.42 -upgrade path for existing tactic scripts, as well as additional means for
7.43 -interactive experimentation and debugging of structured proofs. Isabelle/Isar
7.44 -supports a broad range of proof styles, both readable and unreadable ones.
7.45 -
7.46 -\medskip The Isabelle/Isar framework is generic and should work reasonably
7.47 -well for any Isabelle object-logic that conforms to the natural deduction view
7.48 -of the Isabelle/Pure framework. Major Isabelle logics like HOL
7.49 -\cite{isabelle-HOL}, HOLCF \cite{MuellerNvOS99}, FOL \cite{isabelle-logics},
7.50 -and ZF \cite{isabelle-ZF} have already been set up for end-users.
7.51 -Nonetheless, much of the existing body of theories still consist of old-style
7.52 -theory files with accompanied ML code for proof scripts; this legacy will be
7.53 -gradually converted in due time.
7.54 -
7.55 -
7.56 -\section{Quick start}
7.57 -
7.58 -\subsection{Terminal sessions}
7.59 -
7.60 -Isar is already part of Isabelle. The low-level \texttt{isabelle} binary
7.61 -provides option \texttt{-I} to run the Isabelle/Isar interaction loop at
7.62 -startup, rather than the raw ML top-level. So the most basic way to do
7.63 -anything with Isabelle/Isar is as follows:
7.64 -\begin{ttbox}
7.65 -isabelle -I HOL\medskip
7.66 -\out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip
7.67 -theory Foo imports Main begin;
7.68 -constdefs foo :: nat "foo == 1";
7.69 -lemma "0 < foo" by (simp add: foo_def);
7.70 -end;
7.71 -\end{ttbox}
7.72 -Note that any Isabelle/Isar command may be retracted by \texttt{undo}. See
7.73 -the Isabelle/Isar Quick Reference (appendix~\ref{ap:refcard}) for a
7.74 -comprehensive overview of available commands and other language elements.
7.75 -
7.76 -
7.77 -\subsection{Proof~General}
7.78 -
7.79 -Plain TTY-based interaction as above used to be quite feasible with
7.80 -traditional tactic based theorem proving, but developing Isar documents really
7.81 -demands some better user-interface support. The Proof~General environment by
7.82 -David Aspinall \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
7.83 -interface for interactive theorem provers that organizes all the cut-and-paste
7.84 -and forward-backward walk through the text in a very neat way. In
7.85 -Isabelle/Isar, the current position within a partial proof document is equally
7.86 -important than the actual proof state. Thus Proof~General provides the
7.87 -canonical working environment for Isabelle/Isar, both for getting acquainted
7.88 -(e.g.\ by replaying existing Isar documents) and for production work.
7.89 -
7.90 -
7.91 -\subsubsection{Proof~General as default Isabelle interface}
7.92 -
7.93 -The Isabelle interface wrapper script provides an easy way to invoke
7.94 -Proof~General (including XEmacs or GNU Emacs). The default
7.95 -configuration of Isabelle is smart enough to detect the Proof~General
7.96 -distribution in several canonical places (e.g.\
7.97 -\texttt{\$ISABELLE_HOME/contrib/ProofGeneral}). Thus the capital
7.98 -\texttt{Isabelle} executable would already refer to the
7.99 -\texttt{ProofGeneral/isar} interface without further ado. The
7.100 -Isabelle interface script provides several options; pass \verb,-?, to
7.101 -see its usage.
7.102 -
7.103 -With the proper Isabelle interface setup, Isar documents may now be edited by
7.104 -visiting appropriate theory files, e.g.\
7.105 -\begin{ttbox}
7.106 -Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
7.107 -\end{ttbox}
7.108 -Beginners may note the tool bar for navigating forward and backward through
7.109 -the text (this depends on the local Emacs installation). Consult the
7.110 -Proof~General documentation \cite{proofgeneral} for further basic command
7.111 -sequences, in particular ``\texttt{C-c C-return}'' and ``\texttt{C-c u}''.
7.112 -
7.113 -\medskip
7.114 -
7.115 -Proof~General may be also configured manually by giving Isabelle settings like
7.116 -this (see also \cite{isabelle-sys}):
7.117 -\begin{ttbox}
7.118 -ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
7.119 -PROOFGENERAL_OPTIONS=""
7.120 -\end{ttbox}
7.121 -You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
7.122 -actual installation directory of Proof~General.
7.123 -
7.124 -\medskip
7.125 -
7.126 -Apart from the Isabelle command line, defaults for interface options may be
7.127 -given by the \texttt{PROOFGENERAL_OPTIONS} setting. For example, the Emacs
7.128 -executable to be used may be configured in Isabelle's settings like this:
7.129 -\begin{ttbox}
7.130 -PROOFGENERAL_OPTIONS="-p xemacs-mule"
7.131 -\end{ttbox}
7.132 -
7.133 -Occasionally, a user's \verb,~/.emacs, file contains code that is incompatible
7.134 -with the (X)Emacs version used by Proof~General, causing the interface startup
7.135 -to fail prematurely. Here the \texttt{-u false} option helps to get the
7.136 -interface process up and running. Note that additional Lisp customization
7.137 -code may reside in \texttt{proofgeneral-settings.el} of
7.138 -\texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc}.
7.139 -
7.140 -
7.141 -\subsubsection{The X-Symbol package}
7.142 -
7.143 -Proof~General provides native support for the Emacs X-Symbol package
7.144 -\cite{x-symbol}, which handles proper mathematical symbols displayed on
7.145 -screen. Pass option \texttt{-x true} to the Isabelle interface script, or
7.146 -check the appropriate Proof~General menu setting by hand. In any case, the
7.147 -X-Symbol package must have been properly installed already.
7.148 -
7.149 -Contrary to what you may expect from the documentation of X-Symbol, the
7.150 -package is very easy to install and configures itself automatically. The
7.151 -default configuration of Isabelle is smart enough to detect the X-Symbol
7.152 -package in several canonical places (e.g.\
7.153 -\texttt{\$ISABELLE_HOME/contrib/x-symbol}).
7.154 -
7.155 -\medskip
7.156 -
7.157 -Using proper mathematical symbols in Isabelle theories can be very convenient
7.158 -for readability of large formulas. On the other hand, the plain ASCII sources
7.159 -easily become somewhat unintelligible. For example, $\Longrightarrow$ would
7.160 -appear as \verb,\<Longrightarrow>, according the default set of Isabelle
7.161 -symbols. Nevertheless, the Isabelle document preparation system (see
7.162 -\S\ref{sec:document-prep}) will be happy to print non-ASCII symbols properly.
7.163 -It is even possible to invent additional notation beyond the display
7.164 -capabilities of Emacs and X-Symbol.
7.165 -
7.166 -
7.167 -\section{Isabelle/Isar theories}
7.168 -
7.169 -Isabelle/Isar offers the following main improvements over classic Isabelle.
7.170 -\begin{enumerate}
7.171 -
7.172 -\item A new \emph{theory format}, occasionally referred to as ``new-style
7.173 - theories'', supporting interactive development and unlimited undo operation.
7.174 -
7.175 -\item A \emph{formal proof document language} designed to support intelligible
7.176 - semi-automated reasoning. Instead of putting together unreadable tactic
7.177 - scripts, the author is enabled to express the reasoning in way that is close
7.178 - to usual mathematical practice. The old tactical style has been assimilated
7.179 - as ``improper'' language elements.
7.180 -
7.181 -\item A simple document preparation system, for typesetting formal
7.182 - developments together with informal text. The resulting hyper-linked PDF
7.183 - documents are equally well suited for WWW presentation and as printed
7.184 - copies.
7.185 -
7.186 -\end{enumerate}
7.187 -
7.188 -The Isar proof language is embedded into the new theory format as a proper
7.189 -sub-language. Proof mode is entered by stating some $\THEOREMNAME$ or
7.190 -$\LEMMANAME$ at the theory level, and left again with the final conclusion
7.191 -(e.g.\ via $\QEDNAME$). A few theory specification mechanisms also require
7.192 -some proof, such as HOL's $\isarkeyword{typedef}$ which demands non-emptiness
7.193 -of the representing sets.
7.194 -
7.195 -New-style theory files may still be associated with separate ML files
7.196 -consisting of plain old tactic scripts. There is no longer any ML binding
7.197 -generated for the theory and theorems, though. ML functions \texttt{theory},
7.198 -\texttt{thm}, and \texttt{thms} retrieve this information from the context
7.199 -\cite{isabelle-ref}. Nevertheless, migration between classic Isabelle and
7.200 -Isabelle/Isar is relatively easy. Thus users may start to benefit from
7.201 -interactive theory development and document preparation, even before they have
7.202 -any idea of the Isar proof language at all.
7.203 -
7.204 -\begin{warn}
7.205 - Proof~General does \emph{not} support mixed interactive development of
7.206 - classic Isabelle theory files or tactic scripts, together with Isar
7.207 - documents. The ``\texttt{isa}'' and ``\texttt{isar}'' versions of
7.208 - Proof~General are handled as two different theorem proving systems, only one
7.209 - of these may be active at the same time.
7.210 -\end{warn}
7.211 -
7.212 -Manual conversion of existing tactic scripts may be done by running two
7.213 -separate Proof~General sessions, one for replaying the old script and the
7.214 -other for the emerging Isabelle/Isar document. Also note that Isar supports
7.215 -emulation commands and methods that support traditional tactic scripts within
7.216 -new-style theories, see appendix~\ref{ap:conv} for more information.
7.217 -
7.218 -
7.219 -\subsection{Document preparation}\label{sec:document-prep}
7.220 -
7.221 -Isabelle/Isar provides a simple document preparation system based on existing
7.222 -{PDF-\LaTeX} technology, with full support of hyper-links (both local
7.223 -references and URLs), bookmarks, and thumbnails. Thus the results are equally
7.224 -well suited for WWW browsing and as printed copies.
7.225 -
7.226 -\medskip
7.227 -
7.228 -Isabelle generates {\LaTeX} output as part of the run of a \emph{logic
7.229 - session} (see also \cite{isabelle-sys}). Getting started with a working
7.230 -configuration for common situations is quite easy by using the Isabelle
7.231 -\texttt{mkdir} and \texttt{make} tools. First invoke
7.232 -\begin{ttbox}
7.233 - isatool mkdir Foo
7.234 -\end{ttbox}
7.235 -to initialize a separate directory for session \texttt{Foo} --- it is safe to
7.236 -experiment, since \texttt{isatool mkdir} never overwrites existing files.
7.237 -Ensure that \texttt{Foo/ROOT.ML} holds ML commands to load all theories
7.238 -required for this session; furthermore \texttt{Foo/document/root.tex} should
7.239 -include any special {\LaTeX} macro packages required for your document (the
7.240 -default is usually sufficient as a start).
7.241 -
7.242 -The session is controlled by a separate \texttt{IsaMakefile} (with crude
7.243 -source dependencies by default). This file is located one level up from the
7.244 -\texttt{Foo} directory location. Now invoke
7.245 -\begin{ttbox}
7.246 - isatool make Foo
7.247 -\end{ttbox}
7.248 -to run the \texttt{Foo} session, with browser information and document
7.249 -preparation enabled. Unless any errors are reported by Isabelle or {\LaTeX},
7.250 -the output will appear inside the directory \texttt{ISABELLE_BROWSER_INFO}, as
7.251 -reported by the batch job in verbose mode.
7.252 -
7.253 -\medskip
7.254 -
7.255 -You may also consider to tune the \texttt{usedir} options in
7.256 -\texttt{IsaMakefile}, for example to change the output format from
7.257 -\texttt{pdf} to \texttt{dvi}, or activate the \texttt{-D} option to retain a
7.258 -second copy of the generated {\LaTeX} sources.
7.259 -
7.260 -\medskip
7.261 -
7.262 -See \emph{The Isabelle System Manual} \cite{isabelle-sys} for further details
7.263 -on Isabelle logic sessions and theory presentation. The Isabelle/HOL tutorial
7.264 -\cite{isabelle-hol-book} also covers theory presentation issues.
7.265 -
7.266 -
7.267 -\subsection{How to write Isar proofs anyway?}\label{sec:isar-howto}
7.268 -
7.269 -This is one of the key questions, of course. First of all, the tactic script
7.270 -emulation of Isabelle/Isar essentially provides a clarified version of the
7.271 -very same unstructured proof style of classic Isabelle. Old-time users should
7.272 -quickly become acquainted with that (slightly degenerative) view of Isar.
7.273 -
7.274 -Writing \emph{proper} Isar proof texts targeted at human readers is quite
7.275 -different, though. Experienced users of the unstructured style may even have
7.276 -to unlearn some of their habits to master proof composition in Isar. In
7.277 -contrast, new users with less experience in old-style tactical proving, but a
7.278 -good understanding of mathematical proof in general, often get started easier.
7.279 -
7.280 -\medskip The present text really is only a reference manual on Isabelle/Isar,
7.281 -not a tutorial. Nevertheless, we will attempt to give some clues of how the
7.282 -concepts introduced here may be put into practice. Appendix~\ref{ap:refcard}
7.283 -provides a quick reference card of the most common Isabelle/Isar language
7.284 -elements. Appendix~\ref{ap:conv} offers some practical hints on converting
7.285 -existing Isabelle theories and proof scripts to the new format (without
7.286 -restructuring proofs).
7.287 -
7.288 -Further issues concerning the Isar concepts are covered in the literature
7.289 -\cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
7.290 -The author's PhD thesis \cite{Wenzel-PhD} presently provides the most complete
7.291 -exposition of Isar foundations, techniques, and applications. A number of
7.292 -example applications are distributed with Isabelle, and available via the
7.293 -Isabelle WWW library (e.g.\ \url{http://isabelle.in.tum.de/library/}). As a
7.294 -general rule of thumb, more recent Isabelle applications that also include a
7.295 -separate ``document'' (in PDF) are more likely to consist of proper
7.296 -Isabelle/Isar theories and proofs.
7.297 -
7.298 -%FIXME
7.299 -% The following examples may be of particular interest. Apart from the plain
7.300 -% sources represented in HTML, these Isabelle sessions also provide actual
7.301 -% documents (in PDF).
7.302 -% \begin{itemize}
7.303 -% \item \url{http://isabelle.in.tum.de/library/HOL/Isar_examples/} is a
7.304 -% collection of introductory examples.
7.305 -% \item \url{http://isabelle.in.tum.de/library/HOL/Lattice/} is an example of
7.306 -% typical mathematics-style reasoning in ``axiomatic'' structures.
7.307 -% \item \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/HahnBanach/} is a
7.308 -% big mathematics application on infinitary vector spaces and functional
7.309 -% analysis.
7.310 -% \item \url{http://isabelle.in.tum.de/library/HOL/Lambda/} develops fundamental
7.311 -% properties of $\lambda$-calculus (Church-Rosser and termination).
7.312 -
7.313 -% This may serve as a realistic example of porting of legacy proof scripts
7.314 -% into Isar tactic emulation scripts.
7.315 -% \item \url{http://isabelle.in.tum.de/library/HOL/Unix/} gives a mathematical
7.316 -% model of the main aspects of the Unix file-system including its security
7.317 -% model, but ignoring processes. A few odd effects caused by the general
7.318 -% ``worse-is-better'' approach followed in Unix are discussed within the
7.319 -% formal model.
7.320 -
7.321 -% This example represents a non-trivial verification task, with all proofs
7.322 -% carefully worked out using the proper part of the Isar proof language;
7.323 -% unstructured scripts are only used for symbolic evaluation.
7.324 -% \item \url{http://isabelle.in.tum.de/library/HOL/MicroJava/} is a
7.325 -% formalization of a fragment of Java, together with a corresponding virtual
7.326 -% machine and a specification of its bytecode verifier and a lightweight
7.327 -% bytecode verifier, including proofs of type-safety.
7.328 -
7.329 -% This represents a very ``realistic'' example of large formalizations
7.330 -% performed in form of tactic emulation scripts and proper Isar proof texts.
7.331 -% \end{itemize}
7.332 -
7.333 -
7.334 -%%% Local Variables:
7.335 -%%% mode: latex
7.336 -%%% TeX-master: "isar-ref"
7.337 -%%% End:
8.1 --- a/doc-src/IsarRef/isar-ref.tex Tue Apr 22 22:00:31 2008 +0200
8.2 +++ b/doc-src/IsarRef/isar-ref.tex Wed Apr 23 12:13:08 2008 +0200
8.3 @@ -9,6 +9,10 @@
8.4 \usepackage{style}
8.5 \usepackage{../pdfsetup}
8.6
8.7 +\hyphenation{Isabelle}
8.8 +\hyphenation{Isar}
8.9 +
8.10 +\isadroptag{theory}
8.11 \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
8.12 \author{\emph{Markus Wenzel} \\ TU M\"unchen}
8.13
8.14 @@ -64,16 +68,16 @@
8.15
8.16 \pagenumbering{roman} \tableofcontents \clearfirst
8.17
8.18 -\include{intro}
8.19 -\include{basics}
8.20 -\include{syntax}
8.21 -\include{pure}
8.22 -\include{generic}
8.23 -\include{logics}
8.24 +\input{Thy/document/intro.tex}
8.25 +\input{basics.tex}
8.26 +\input{syntax.tex}
8.27 +\input{pure.tex}
8.28 +\input{generic.tex}
8.29 +\input{logics.tex}
8.30
8.31 \appendix
8.32 -\include{refcard}
8.33 -\include{conversion}
8.34 +\input{refcard.tex}
8.35 +\input{conversion.tex}
8.36
8.37 \begingroup
8.38 \bibliographystyle{plain} \small\raggedright\frenchspacing