1.1 --- a/doc-src/IsarRef/IsaMakefile Mon Jun 02 13:21:06 2008 +0200
1.2 +++ b/doc-src/IsarRef/IsaMakefile Mon Jun 02 21:01:42 2008 +0200
1.3 @@ -21,21 +21,24 @@
1.4
1.5 HOL-IsarRef: $(LOG)/HOL-IsarRef.gz
1.6
1.7 -$(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/intro.thy \
1.8 - Thy/syntax.thy Thy/Spec.thy Thy/Proof.thy Thy/pure.thy Thy/Generic.thy \
1.9 - Thy/HOL_Specific.thy Thy/Quick_Reference.thy Thy/ML_Tactic.thy
1.10 +$(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML \
1.11 + Thy/Introduction.thy Thy/syntax.thy Thy/Spec.thy Thy/Proof.thy \
1.12 + Thy/pure.thy Thy/Generic.thy Thy/HOL_Specific.thy \
1.13 + Thy/Quick_Reference.thy Thy/ML_Tactic.thy
1.14 @$(USEDIR) -s IsarRef HOL Thy
1.15
1.16
1.17 HOLCF-IsarRef: $(LOG)/HOLCF-IsarRef.gz
1.18
1.19 -$(LOG)/HOLCF-IsarRef.gz: Thy/ROOT-HOLCF.ML ../antiquote_setup.ML Thy/HOLCF_Specific.thy
1.20 +$(LOG)/HOLCF-IsarRef.gz: Thy/ROOT-HOLCF.ML ../antiquote_setup.ML \
1.21 + Thy/HOLCF_Specific.thy
1.22 @$(USEDIR) -s IsarRef -f ROOT-HOLCF.ML HOLCF Thy
1.23
1.24
1.25 ZF-IsarRef: $(LOG)/ZF-IsarRef.gz
1.26
1.27 -$(LOG)/ZF-IsarRef.gz: Thy/ROOT-ZF.ML ../antiquote_setup.ML Thy/ZF_Specific.thy
1.28 +$(LOG)/ZF-IsarRef.gz: Thy/ROOT-ZF.ML ../antiquote_setup.ML \
1.29 + Thy/ZF_Specific.thy
1.30 @$(USEDIR) -s IsarRef -f ROOT-ZF.ML ZF Thy
1.31
1.32
2.1 --- a/doc-src/IsarRef/Makefile Mon Jun 02 13:21:06 2008 +0200
2.2 +++ b/doc-src/IsarRef/Makefile Mon Jun 02 21:01:42 2008 +0200
2.3 @@ -17,7 +17,7 @@
2.4 Thy/document/HOLCF_Specific.tex Thy/document/HOL_Specific.tex \
2.5 Thy/document/ML_Tactic.tex Thy/document/Proof.tex \
2.6 Thy/document/Quick_Reference.tex Thy/document/Spec.tex \
2.7 - Thy/document/ZF_Specific.tex Thy/document/intro.tex \
2.8 + Thy/document/ZF_Specific.tex Thy/document/Introduction.tex \
2.9 Thy/document/pure.tex Thy/document/syntax.tex ../isar.sty \
2.10 ../rail.sty ../railsetup.sty ../proof.sty ../iman.sty ../extra.sty \
2.11 ../ttbox.sty ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty \
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/doc-src/IsarRef/Thy/Introduction.thy Mon Jun 02 21:01:42 2008 +0200
3.3 @@ -0,0 +1,304 @@
3.4 +(* $Id$ *)
3.5 +
3.6 +theory Introduction
3.7 +imports Pure
3.8 +begin
3.9 +
3.10 +chapter {* Introduction *}
3.11 +
3.12 +section {* Overview *}
3.13 +
3.14 +text {*
3.15 + The \emph{Isabelle} system essentially provides a generic
3.16 + infrastructure for building deductive systems (programmed in
3.17 + Standard ML), with a special focus on interactive theorem proving in
3.18 + higher-order logics. In the olden days even end-users would refer
3.19 + to certain ML functions (goal commands, tactics, tacticals etc.) to
3.20 + pursue their everyday theorem proving tasks
3.21 + \cite{isabelle-intro,isabelle-ref}.
3.22 +
3.23 + In contrast \emph{Isar} provides an interpreted language environment
3.24 + of its own, which has been specifically tailored for the needs of
3.25 + theory and proof development. Compared to raw ML, the Isabelle/Isar
3.26 + top-level provides a more robust and comfortable development
3.27 + platform, with proper support for theory development graphs,
3.28 + single-step transactions with unlimited undo, etc. The
3.29 + Isabelle/Isar version of the \emph{Proof~General} user interface
3.30 + \cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate
3.31 + front-end for interactive theory and proof development in this
3.32 + advanced theorem proving environment.
3.33 +
3.34 + \medskip Apart from the technical advances over bare-bones ML
3.35 + programming, the main purpose of the Isar language is to provide a
3.36 + conceptually different view on machine-checked proofs
3.37 + \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. ``Isar'' stands for
3.38 + ``Intelligible semi-automated reasoning''. Drawing from both the
3.39 + traditions of informal mathematical proof texts and high-level
3.40 + programming languages, Isar offers a versatile environment for
3.41 + structured formal proof documents. Thus properly written Isar
3.42 + proofs become accessible to a broader audience than unstructured
3.43 + tactic scripts (which typically only provide operational information
3.44 + for the machine). Writing human-readable proof texts certainly
3.45 + requires some additional efforts by the writer to achieve a good
3.46 + presentation, both of formal and informal parts of the text. On the
3.47 + other hand, human-readable formal texts gain some value in their own
3.48 + right, independently of the mechanic proof-checking process.
3.49 +
3.50 + Despite its grand design of structured proof texts, Isar is able to
3.51 + assimilate the old tactical style as an ``improper'' sub-language.
3.52 + This provides an easy upgrade path for existing tactic scripts, as
3.53 + well as additional means for interactive experimentation and
3.54 + debugging of structured proofs. Isabelle/Isar supports a broad
3.55 + range of proof styles, both readable and unreadable ones.
3.56 +
3.57 + \medskip The Isabelle/Isar framework is generic and should work
3.58 + reasonably well for any Isabelle object-logic that conforms to the
3.59 + natural deduction view of the Isabelle/Pure framework. Major
3.60 + Isabelle logics like HOL \cite{isabelle-HOL}, HOLCF
3.61 + \cite{MuellerNvOS99}, FOL \cite{isabelle-logics}, and ZF
3.62 + \cite{isabelle-ZF} have already been set up for end-users.
3.63 +*}
3.64 +
3.65 +
3.66 +section {* Quick start *}
3.67 +
3.68 +subsection {* Terminal sessions *}
3.69 +
3.70 +text {*
3.71 + Isar is already part of Isabelle. The low-level @{verbatim
3.72 + isabelle} binary provides option @{verbatim "-I"} to run the
3.73 + Isabelle/Isar interaction loop at startup, rather than the raw ML
3.74 + top-level. So the most basic way to do anything with Isabelle/Isar
3.75 + is as follows: % FIXME update
3.76 +\begin{ttbox}
3.77 +isabelle -I HOL\medskip
3.78 +\out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip
3.79 +theory Foo imports Main begin;
3.80 +definition foo :: nat where "foo == 1";
3.81 +lemma "0 < foo" by (simp add: foo_def);
3.82 +end;
3.83 +\end{ttbox}
3.84 +
3.85 + Note that any Isabelle/Isar command may be retracted by @{command
3.86 + "undo"}. See the Isabelle/Isar Quick Reference
3.87 + (\appref{ap:refcard}) for a comprehensive overview of available
3.88 + commands and other language elements.
3.89 +*}
3.90 +
3.91 +
3.92 +subsection {* Proof General *}
3.93 +
3.94 +text {*
3.95 + Plain TTY-based interaction as above used to be quite feasible with
3.96 + traditional tactic based theorem proving, but developing Isar
3.97 + documents really demands some better user-interface support. The
3.98 + Proof~General environment by David Aspinall
3.99 + \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
3.100 + interface for interactive theorem provers that organizes all the
3.101 + cut-and-paste and forward-backward walk through the text in a very
3.102 + neat way. In Isabelle/Isar, the current position within a partial
3.103 + proof document is equally important than the actual proof state.
3.104 + Thus Proof~General provides the canonical working environment for
3.105 + Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
3.106 + existing Isar documents) and for production work.
3.107 +*}
3.108 +
3.109 +
3.110 +subsubsection{* Proof~General as default Isabelle interface *}
3.111 +
3.112 +text {*
3.113 + The Isabelle interface wrapper script provides an easy way to invoke
3.114 + Proof~General (including XEmacs or GNU Emacs). The default
3.115 + configuration of Isabelle is smart enough to detect the
3.116 + Proof~General distribution in several canonical places (e.g.\
3.117 + @{verbatim "$ISABELLE_HOME/contrib/ProofGeneral"}). Thus the
3.118 + capital @{verbatim Isabelle} executable would already refer to the
3.119 + @{verbatim "ProofGeneral/isar"} interface without further ado. The
3.120 + Isabelle interface script provides several options; pass @{verbatim
3.121 + "-?"} to see its usage.
3.122 +
3.123 + With the proper Isabelle interface setup, Isar documents may now be edited by
3.124 + visiting appropriate theory files, e.g.\
3.125 +\begin{ttbox}
3.126 +Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
3.127 +\end{ttbox}
3.128 + Beginners may note the tool bar for navigating forward and backward
3.129 + through the text (this depends on the local Emacs installation).
3.130 + Consult the Proof~General documentation \cite{proofgeneral} for
3.131 + further basic command sequences, in particular ``@{verbatim "C-c C-return"}''
3.132 + and ``@{verbatim "C-c u"}''.
3.133 +
3.134 + \medskip Proof~General may be also configured manually by giving
3.135 + Isabelle settings like this (see also \cite{isabelle-sys}):
3.136 +
3.137 +\begin{ttbox}
3.138 +ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
3.139 +PROOFGENERAL_OPTIONS=""
3.140 +\end{ttbox}
3.141 + You may have to change @{verbatim
3.142 + "$ISABELLE_HOME/contrib/ProofGeneral"} to the actual installation
3.143 + directory of Proof~General.
3.144 +
3.145 + \medskip Apart from the Isabelle command line, defaults for
3.146 + interface options may be given by the @{verbatim PROOFGENERAL_OPTIONS}
3.147 + setting. For example, the Emacs executable to be used may be
3.148 + configured in Isabelle's settings like this:
3.149 +\begin{ttbox}
3.150 +PROOFGENERAL_OPTIONS="-p xemacs-mule"
3.151 +\end{ttbox}
3.152 +
3.153 + Occasionally, a user's @{verbatim "~/.emacs"} file contains code
3.154 + that is incompatible with the (X)Emacs version used by
3.155 + Proof~General, causing the interface startup to fail prematurely.
3.156 + Here the @{verbatim "-u false"} option helps to get the interface
3.157 + process up and running. Note that additional Lisp customization
3.158 + code may reside in @{verbatim "proofgeneral-settings.el"} of
3.159 + @{verbatim "$ISABELLE_HOME/etc"} or @{verbatim
3.160 + "$ISABELLE_HOME_USER/etc"}.
3.161 +*}
3.162 +
3.163 +
3.164 +subsubsection {* The X-Symbol package *}
3.165 +
3.166 +text {*
3.167 + Proof~General incorporates a version of the Emacs X-Symbol package
3.168 + \cite{x-symbol}, which handles proper mathematical symbols displayed
3.169 + on screen. Pass option @{verbatim "-x true"} to the Isabelle
3.170 + interface script, or check the appropriate Proof~General menu
3.171 + setting by hand. The main challenge of getting X-Symbol to work
3.172 + properly is the underlying (semi-automated) X11 font setup.
3.173 +
3.174 + \medskip Using proper mathematical symbols in Isabelle theories can
3.175 + be very convenient for readability of large formulas. On the other
3.176 + hand, the plain ASCII sources easily become somewhat unintelligible.
3.177 + For example, @{text "\<Longrightarrow>"} would appear as @{verbatim "\<Longrightarrow>"} according
3.178 + the default set of Isabelle symbols. Nevertheless, the Isabelle
3.179 + document preparation system (see \secref{sec:document-prep}) will be
3.180 + happy to print non-ASCII symbols properly. It is even possible to
3.181 + invent additional notation beyond the display capabilities of Emacs
3.182 + and X-Symbol.
3.183 +*}
3.184 +
3.185 +
3.186 +section {* Isabelle/Isar theories *}
3.187 +
3.188 +text {*
3.189 + Isabelle/Isar offers the following main improvements over classic
3.190 + Isabelle.
3.191 +
3.192 + \begin{enumerate}
3.193 +
3.194 + \item A \emph{theory format} that integrates specifications and
3.195 + proofs, supporting interactive development and unlimited undo
3.196 + operation.
3.197 +
3.198 + \item A \emph{formal proof document language} designed to support
3.199 + intelligible semi-automated reasoning. Instead of putting together
3.200 + unreadable tactic scripts, the author is enabled to express the
3.201 + reasoning in way that is close to usual mathematical practice. The
3.202 + old tactical style has been assimilated as ``improper'' language
3.203 + elements.
3.204 +
3.205 + \item A simple document preparation system, for typesetting formal
3.206 + developments together with informal text. The resulting
3.207 + hyper-linked PDF documents are equally well suited for WWW
3.208 + presentation and as printed copies.
3.209 +
3.210 + \end{enumerate}
3.211 +
3.212 + The Isar proof language is embedded into the new theory format as a
3.213 + proper sub-language. Proof mode is entered by stating some
3.214 + @{command "theorem"} or @{command "lemma"} at the theory level, and
3.215 + left again with the final conclusion (e.g.\ via @{command "qed"}).
3.216 + A few theory specification mechanisms also require some proof, such
3.217 + as HOL's @{command "typedef"} which demands non-emptiness of the
3.218 + representing sets.
3.219 +*}
3.220 +
3.221 +
3.222 +subsection {* Document preparation \label{sec:document-prep} *}
3.223 +
3.224 +text {*
3.225 + Isabelle/Isar provides a simple document preparation system based on
3.226 + existing {PDF-\LaTeX} technology, with full support of hyper-links
3.227 + (both local references and URLs) and bookmarks. Thus the results
3.228 + are equally well suited for WWW browsing and as printed copies.
3.229 +
3.230 + \medskip Isabelle generates {\LaTeX} output as part of the run of a
3.231 + \emph{logic session} (see also \cite{isabelle-sys}). Getting
3.232 + started with a working configuration for common situations is quite
3.233 + easy by using the Isabelle @{verbatim mkdir} and @{verbatim make}
3.234 + tools. First invoke
3.235 +\begin{ttbox}
3.236 + isatool mkdir Foo
3.237 +\end{ttbox}
3.238 + to initialize a separate directory for session @{verbatim Foo} ---
3.239 + it is safe to experiment, since @{verbatim "isatool mkdir"} never
3.240 + overwrites existing files. Ensure that @{verbatim "Foo/ROOT.ML"}
3.241 + holds ML commands to load all theories required for this session;
3.242 + furthermore @{verbatim "Foo/document/root.tex"} should include any
3.243 + special {\LaTeX} macro packages required for your document (the
3.244 + default is usually sufficient as a start).
3.245 +
3.246 + The session is controlled by a separate @{verbatim IsaMakefile}
3.247 + (with crude source dependencies by default). This file is located
3.248 + one level up from the @{verbatim Foo} directory location. Now
3.249 + invoke
3.250 +\begin{ttbox}
3.251 + isatool make Foo
3.252 +\end{ttbox}
3.253 + to run the @{verbatim Foo} session, with browser information and
3.254 + document preparation enabled. Unless any errors are reported by
3.255 + Isabelle or {\LaTeX}, the output will appear inside the directory
3.256 + @{verbatim ISABELLE_BROWSER_INFO}, as reported by the batch job in
3.257 + verbose mode.
3.258 +
3.259 + \medskip You may also consider to tune the @{verbatim usedir}
3.260 + options in @{verbatim IsaMakefile}, for example to change the output
3.261 + format from @{verbatim pdf} to @{verbatim dvi}, or activate the
3.262 + @{verbatim "-D"} option to retain a second copy of the generated
3.263 + {\LaTeX} sources.
3.264 +
3.265 + \medskip See \emph{The Isabelle System Manual} \cite{isabelle-sys}
3.266 + for further details on Isabelle logic sessions and theory
3.267 + presentation. The Isabelle/HOL tutorial \cite{isabelle-hol-book}
3.268 + also covers theory presentation issues.
3.269 +*}
3.270 +
3.271 +
3.272 +subsection {* How to write Isar proofs anyway? \label{sec:isar-howto} *}
3.273 +
3.274 +text {*
3.275 + This is one of the key questions, of course. First of all, the
3.276 + tactic script emulation of Isabelle/Isar essentially provides a
3.277 + clarified version of the very same unstructured proof style of
3.278 + classic Isabelle. Old-time users should quickly become acquainted
3.279 + with that (slightly degenerative) view of Isar.
3.280 +
3.281 + Writing \emph{proper} Isar proof texts targeted at human readers is
3.282 + quite different, though. Experienced users of the unstructured
3.283 + style may even have to unlearn some of their habits to master proof
3.284 + composition in Isar. In contrast, new users with less experience in
3.285 + old-style tactical proving, but a good understanding of mathematical
3.286 + proof in general, often get started easier.
3.287 +
3.288 + \medskip The present text really is only a reference manual on
3.289 + Isabelle/Isar, not a tutorial. Nevertheless, we will attempt to
3.290 + give some clues of how the concepts introduced here may be put into
3.291 + practice. Especially note that \appref{ap:refcard} provides a quick
3.292 + reference card of the most common Isabelle/Isar language elements.
3.293 +
3.294 + Further issues concerning the Isar concepts are covered in the
3.295 + literature
3.296 + \cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
3.297 + The author's PhD thesis \cite{Wenzel-PhD} presently provides the
3.298 + most complete exposition of Isar foundations, techniques, and
3.299 + applications. A number of example applications are distributed with
3.300 + Isabelle, and available via the Isabelle WWW library (e.g.\
3.301 + \url{http://isabelle.in.tum.de/library/}). The ``Archive of Formal
3.302 + Proofs'' \url{http://afp.sourceforge.net/} also provides plenty of
3.303 + examples, both in proper Isar proof style and unstructured tactic
3.304 + scripts.
3.305 +*}
3.306 +
3.307 +end
4.1 --- a/doc-src/IsarRef/Thy/ROOT.ML Mon Jun 02 13:21:06 2008 +0200
4.2 +++ b/doc-src/IsarRef/Thy/ROOT.ML Mon Jun 02 21:01:42 2008 +0200
4.3 @@ -4,7 +4,7 @@
4.4 set ThyOutput.source;
4.5 use "../../antiquote_setup.ML";
4.6
4.7 -use_thy "intro";
4.8 +use_thy "Introduction";
4.9 use_thy "syntax";
4.10 use_thy "Spec";
4.11 use_thy "Proof";
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/doc-src/IsarRef/Thy/document/Introduction.tex Mon Jun 02 21:01:42 2008 +0200
5.3 @@ -0,0 +1,354 @@
5.4 +%
5.5 +\begin{isabellebody}%
5.6 +\def\isabellecontext{Introduction}%
5.7 +%
5.8 +\isadelimtheory
5.9 +\isanewline
5.10 +\isanewline
5.11 +%
5.12 +\endisadelimtheory
5.13 +%
5.14 +\isatagtheory
5.15 +\isacommand{theory}\isamarkupfalse%
5.16 +\ Introduction\isanewline
5.17 +\isakeyword{imports}\ Pure\isanewline
5.18 +\isakeyword{begin}%
5.19 +\endisatagtheory
5.20 +{\isafoldtheory}%
5.21 +%
5.22 +\isadelimtheory
5.23 +%
5.24 +\endisadelimtheory
5.25 +%
5.26 +\isamarkupchapter{Introduction%
5.27 +}
5.28 +\isamarkuptrue%
5.29 +%
5.30 +\isamarkupsection{Overview%
5.31 +}
5.32 +\isamarkuptrue%
5.33 +%
5.34 +\begin{isamarkuptext}%
5.35 +The \emph{Isabelle} system essentially provides a generic
5.36 + infrastructure for building deductive systems (programmed in
5.37 + Standard ML), with a special focus on interactive theorem proving in
5.38 + higher-order logics. In the olden days even end-users would refer
5.39 + to certain ML functions (goal commands, tactics, tacticals etc.) to
5.40 + pursue their everyday theorem proving tasks
5.41 + \cite{isabelle-intro,isabelle-ref}.
5.42 +
5.43 + In contrast \emph{Isar} provides an interpreted language environment
5.44 + of its own, which has been specifically tailored for the needs of
5.45 + theory and proof development. Compared to raw ML, the Isabelle/Isar
5.46 + top-level provides a more robust and comfortable development
5.47 + platform, with proper support for theory development graphs,
5.48 + single-step transactions with unlimited undo, etc. The
5.49 + Isabelle/Isar version of the \emph{Proof~General} user interface
5.50 + \cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate
5.51 + front-end for interactive theory and proof development in this
5.52 + advanced theorem proving environment.
5.53 +
5.54 + \medskip Apart from the technical advances over bare-bones ML
5.55 + programming, the main purpose of the Isar language is to provide a
5.56 + conceptually different view on machine-checked proofs
5.57 + \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. ``Isar'' stands for
5.58 + ``Intelligible semi-automated reasoning''. Drawing from both the
5.59 + traditions of informal mathematical proof texts and high-level
5.60 + programming languages, Isar offers a versatile environment for
5.61 + structured formal proof documents. Thus properly written Isar
5.62 + proofs become accessible to a broader audience than unstructured
5.63 + tactic scripts (which typically only provide operational information
5.64 + for the machine). Writing human-readable proof texts certainly
5.65 + requires some additional efforts by the writer to achieve a good
5.66 + presentation, both of formal and informal parts of the text. On the
5.67 + other hand, human-readable formal texts gain some value in their own
5.68 + right, independently of the mechanic proof-checking process.
5.69 +
5.70 + Despite its grand design of structured proof texts, Isar is able to
5.71 + assimilate the old tactical style as an ``improper'' sub-language.
5.72 + This provides an easy upgrade path for existing tactic scripts, as
5.73 + well as additional means for interactive experimentation and
5.74 + debugging of structured proofs. Isabelle/Isar supports a broad
5.75 + range of proof styles, both readable and unreadable ones.
5.76 +
5.77 + \medskip The Isabelle/Isar framework is generic and should work
5.78 + reasonably well for any Isabelle object-logic that conforms to the
5.79 + natural deduction view of the Isabelle/Pure framework. Major
5.80 + Isabelle logics like HOL \cite{isabelle-HOL}, HOLCF
5.81 + \cite{MuellerNvOS99}, FOL \cite{isabelle-logics}, and ZF
5.82 + \cite{isabelle-ZF} have already been set up for end-users.%
5.83 +\end{isamarkuptext}%
5.84 +\isamarkuptrue%
5.85 +%
5.86 +\isamarkupsection{Quick start%
5.87 +}
5.88 +\isamarkuptrue%
5.89 +%
5.90 +\isamarkupsubsection{Terminal sessions%
5.91 +}
5.92 +\isamarkuptrue%
5.93 +%
5.94 +\begin{isamarkuptext}%
5.95 +Isar is already part of Isabelle. The low-level \verb|isabelle| binary provides option \verb|-I| to run the
5.96 + Isabelle/Isar interaction loop at startup, rather than the raw ML
5.97 + top-level. So the most basic way to do anything with Isabelle/Isar
5.98 + is as follows: % FIXME update
5.99 +\begin{ttbox}
5.100 +isabelle -I HOL\medskip
5.101 +\out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip
5.102 +theory Foo imports Main begin;
5.103 +definition foo :: nat where "foo == 1";
5.104 +lemma "0 < foo" by (simp add: foo_def);
5.105 +end;
5.106 +\end{ttbox}
5.107 +
5.108 + Note that any Isabelle/Isar command may be retracted by \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}. See the Isabelle/Isar Quick Reference
5.109 + (\appref{ap:refcard}) for a comprehensive overview of available
5.110 + commands and other language elements.%
5.111 +\end{isamarkuptext}%
5.112 +\isamarkuptrue%
5.113 +%
5.114 +\isamarkupsubsection{Proof General%
5.115 +}
5.116 +\isamarkuptrue%
5.117 +%
5.118 +\begin{isamarkuptext}%
5.119 +Plain TTY-based interaction as above used to be quite feasible with
5.120 + traditional tactic based theorem proving, but developing Isar
5.121 + documents really demands some better user-interface support. The
5.122 + Proof~General environment by David Aspinall
5.123 + \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
5.124 + interface for interactive theorem provers that organizes all the
5.125 + cut-and-paste and forward-backward walk through the text in a very
5.126 + neat way. In Isabelle/Isar, the current position within a partial
5.127 + proof document is equally important than the actual proof state.
5.128 + Thus Proof~General provides the canonical working environment for
5.129 + Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
5.130 + existing Isar documents) and for production work.%
5.131 +\end{isamarkuptext}%
5.132 +\isamarkuptrue%
5.133 +%
5.134 +\isamarkupsubsubsection{Proof~General as default Isabelle interface%
5.135 +}
5.136 +\isamarkuptrue%
5.137 +%
5.138 +\begin{isamarkuptext}%
5.139 +The Isabelle interface wrapper script provides an easy way to invoke
5.140 + Proof~General (including XEmacs or GNU Emacs). The default
5.141 + configuration of Isabelle is smart enough to detect the
5.142 + Proof~General distribution in several canonical places (e.g.\
5.143 + \verb|$ISABELLE_HOME/contrib/ProofGeneral|). Thus the
5.144 + capital \verb|Isabelle| executable would already refer to the
5.145 + \verb|ProofGeneral/isar| interface without further ado. The
5.146 + Isabelle interface script provides several options; pass \verb|-?| to see its usage.
5.147 +
5.148 + With the proper Isabelle interface setup, Isar documents may now be edited by
5.149 + visiting appropriate theory files, e.g.\
5.150 +\begin{ttbox}
5.151 +Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
5.152 +\end{ttbox}
5.153 + Beginners may note the tool bar for navigating forward and backward
5.154 + through the text (this depends on the local Emacs installation).
5.155 + Consult the Proof~General documentation \cite{proofgeneral} for
5.156 + further basic command sequences, in particular ``\verb|C-c C-return|''
5.157 + and ``\verb|C-c u|''.
5.158 +
5.159 + \medskip Proof~General may be also configured manually by giving
5.160 + Isabelle settings like this (see also \cite{isabelle-sys}):
5.161 +
5.162 +\begin{ttbox}
5.163 +ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
5.164 +PROOFGENERAL_OPTIONS=""
5.165 +\end{ttbox}
5.166 + You may have to change \verb|$ISABELLE_HOME/contrib/ProofGeneral| to the actual installation
5.167 + directory of Proof~General.
5.168 +
5.169 + \medskip Apart from the Isabelle command line, defaults for
5.170 + interface options may be given by the \verb|PROOFGENERAL_OPTIONS|
5.171 + setting. For example, the Emacs executable to be used may be
5.172 + configured in Isabelle's settings like this:
5.173 +\begin{ttbox}
5.174 +PROOFGENERAL_OPTIONS="-p xemacs-mule"
5.175 +\end{ttbox}
5.176 +
5.177 + Occasionally, a user's \verb|~/.emacs| file contains code
5.178 + that is incompatible with the (X)Emacs version used by
5.179 + Proof~General, causing the interface startup to fail prematurely.
5.180 + Here the \verb|-u false| option helps to get the interface
5.181 + process up and running. Note that additional Lisp customization
5.182 + code may reside in \verb|proofgeneral-settings.el| of
5.183 + \verb|$ISABELLE_HOME/etc| or \verb|$ISABELLE_HOME_USER/etc|.%
5.184 +\end{isamarkuptext}%
5.185 +\isamarkuptrue%
5.186 +%
5.187 +\isamarkupsubsubsection{The X-Symbol package%
5.188 +}
5.189 +\isamarkuptrue%
5.190 +%
5.191 +\begin{isamarkuptext}%
5.192 +Proof~General incorporates a version of the Emacs X-Symbol package
5.193 + \cite{x-symbol}, which handles proper mathematical symbols displayed
5.194 + on screen. Pass option \verb|-x true| to the Isabelle
5.195 + interface script, or check the appropriate Proof~General menu
5.196 + setting by hand. The main challenge of getting X-Symbol to work
5.197 + properly is the underlying (semi-automated) X11 font setup.
5.198 +
5.199 + \medskip Using proper mathematical symbols in Isabelle theories can
5.200 + be very convenient for readability of large formulas. On the other
5.201 + hand, the plain ASCII sources easily become somewhat unintelligible.
5.202 + For example, \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} would appear as \verb|\<Longrightarrow>| according
5.203 + the default set of Isabelle symbols. Nevertheless, the Isabelle
5.204 + document preparation system (see \secref{sec:document-prep}) will be
5.205 + happy to print non-ASCII symbols properly. It is even possible to
5.206 + invent additional notation beyond the display capabilities of Emacs
5.207 + and X-Symbol.%
5.208 +\end{isamarkuptext}%
5.209 +\isamarkuptrue%
5.210 +%
5.211 +\isamarkupsection{Isabelle/Isar theories%
5.212 +}
5.213 +\isamarkuptrue%
5.214 +%
5.215 +\begin{isamarkuptext}%
5.216 +Isabelle/Isar offers the following main improvements over classic
5.217 + Isabelle.
5.218 +
5.219 + \begin{enumerate}
5.220 +
5.221 + \item A \emph{theory format} that integrates specifications and
5.222 + proofs, supporting interactive development and unlimited undo
5.223 + operation.
5.224 +
5.225 + \item A \emph{formal proof document language} designed to support
5.226 + intelligible semi-automated reasoning. Instead of putting together
5.227 + unreadable tactic scripts, the author is enabled to express the
5.228 + reasoning in way that is close to usual mathematical practice. The
5.229 + old tactical style has been assimilated as ``improper'' language
5.230 + elements.
5.231 +
5.232 + \item A simple document preparation system, for typesetting formal
5.233 + developments together with informal text. The resulting
5.234 + hyper-linked PDF documents are equally well suited for WWW
5.235 + presentation and as printed copies.
5.236 +
5.237 + \end{enumerate}
5.238 +
5.239 + The Isar proof language is embedded into the new theory format as a
5.240 + proper sub-language. Proof mode is entered by stating some
5.241 + \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}} or \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} at the theory level, and
5.242 + left again with the final conclusion (e.g.\ via \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}).
5.243 + A few theory specification mechanisms also require some proof, such
5.244 + as HOL's \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} which demands non-emptiness of the
5.245 + representing sets.%
5.246 +\end{isamarkuptext}%
5.247 +\isamarkuptrue%
5.248 +%
5.249 +\isamarkupsubsection{Document preparation \label{sec:document-prep}%
5.250 +}
5.251 +\isamarkuptrue%
5.252 +%
5.253 +\begin{isamarkuptext}%
5.254 +Isabelle/Isar provides a simple document preparation system based on
5.255 + existing {PDF-\LaTeX} technology, with full support of hyper-links
5.256 + (both local references and URLs) and bookmarks. Thus the results
5.257 + are equally well suited for WWW browsing and as printed copies.
5.258 +
5.259 + \medskip Isabelle generates {\LaTeX} output as part of the run of a
5.260 + \emph{logic session} (see also \cite{isabelle-sys}). Getting
5.261 + started with a working configuration for common situations is quite
5.262 + easy by using the Isabelle \verb|mkdir| and \verb|make|
5.263 + tools. First invoke
5.264 +\begin{ttbox}
5.265 + isatool mkdir Foo
5.266 +\end{ttbox}
5.267 + to initialize a separate directory for session \verb|Foo| ---
5.268 + it is safe to experiment, since \verb|isatool mkdir| never
5.269 + overwrites existing files. Ensure that \verb|Foo/ROOT.ML|
5.270 + holds ML commands to load all theories required for this session;
5.271 + furthermore \verb|Foo/document/root.tex| should include any
5.272 + special {\LaTeX} macro packages required for your document (the
5.273 + default is usually sufficient as a start).
5.274 +
5.275 + The session is controlled by a separate \verb|IsaMakefile|
5.276 + (with crude source dependencies by default). This file is located
5.277 + one level up from the \verb|Foo| directory location. Now
5.278 + invoke
5.279 +\begin{ttbox}
5.280 + isatool make Foo
5.281 +\end{ttbox}
5.282 + to run the \verb|Foo| session, with browser information and
5.283 + document preparation enabled. Unless any errors are reported by
5.284 + Isabelle or {\LaTeX}, the output will appear inside the directory
5.285 + \verb|ISABELLE_BROWSER_INFO|, as reported by the batch job in
5.286 + verbose mode.
5.287 +
5.288 + \medskip You may also consider to tune the \verb|usedir|
5.289 + options in \verb|IsaMakefile|, for example to change the output
5.290 + format from \verb|pdf| to \verb|dvi|, or activate the
5.291 + \verb|-D| option to retain a second copy of the generated
5.292 + {\LaTeX} sources.
5.293 +
5.294 + \medskip See \emph{The Isabelle System Manual} \cite{isabelle-sys}
5.295 + for further details on Isabelle logic sessions and theory
5.296 + presentation. The Isabelle/HOL tutorial \cite{isabelle-hol-book}
5.297 + also covers theory presentation issues.%
5.298 +\end{isamarkuptext}%
5.299 +\isamarkuptrue%
5.300 +%
5.301 +\isamarkupsubsection{How to write Isar proofs anyway? \label{sec:isar-howto}%
5.302 +}
5.303 +\isamarkuptrue%
5.304 +%
5.305 +\begin{isamarkuptext}%
5.306 +This is one of the key questions, of course. First of all, the
5.307 + tactic script emulation of Isabelle/Isar essentially provides a
5.308 + clarified version of the very same unstructured proof style of
5.309 + classic Isabelle. Old-time users should quickly become acquainted
5.310 + with that (slightly degenerative) view of Isar.
5.311 +
5.312 + Writing \emph{proper} Isar proof texts targeted at human readers is
5.313 + quite different, though. Experienced users of the unstructured
5.314 + style may even have to unlearn some of their habits to master proof
5.315 + composition in Isar. In contrast, new users with less experience in
5.316 + old-style tactical proving, but a good understanding of mathematical
5.317 + proof in general, often get started easier.
5.318 +
5.319 + \medskip The present text really is only a reference manual on
5.320 + Isabelle/Isar, not a tutorial. Nevertheless, we will attempt to
5.321 + give some clues of how the concepts introduced here may be put into
5.322 + practice. Especially note that \appref{ap:refcard} provides a quick
5.323 + reference card of the most common Isabelle/Isar language elements.
5.324 +
5.325 + Further issues concerning the Isar concepts are covered in the
5.326 + literature
5.327 + \cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
5.328 + The author's PhD thesis \cite{Wenzel-PhD} presently provides the
5.329 + most complete exposition of Isar foundations, techniques, and
5.330 + applications. A number of example applications are distributed with
5.331 + Isabelle, and available via the Isabelle WWW library (e.g.\
5.332 + \url{http://isabelle.in.tum.de/library/}). The ``Archive of Formal
5.333 + Proofs'' \url{http://afp.sourceforge.net/} also provides plenty of
5.334 + examples, both in proper Isar proof style and unstructured tactic
5.335 + scripts.%
5.336 +\end{isamarkuptext}%
5.337 +\isamarkuptrue%
5.338 +%
5.339 +\isadelimtheory
5.340 +%
5.341 +\endisadelimtheory
5.342 +%
5.343 +\isatagtheory
5.344 +\isacommand{end}\isamarkupfalse%
5.345 +%
5.346 +\endisatagtheory
5.347 +{\isafoldtheory}%
5.348 +%
5.349 +\isadelimtheory
5.350 +%
5.351 +\endisadelimtheory
5.352 +\isanewline
5.353 +\end{isabellebody}%
5.354 +%%% Local Variables:
5.355 +%%% mode: latex
5.356 +%%% TeX-master: "root"
5.357 +%%% End:
6.1 --- a/doc-src/IsarRef/Thy/document/intro.tex Mon Jun 02 13:21:06 2008 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,354 +0,0 @@
6.4 -%
6.5 -\begin{isabellebody}%
6.6 -\def\isabellecontext{intro}%
6.7 -%
6.8 -\isadelimtheory
6.9 -\isanewline
6.10 -\isanewline
6.11 -%
6.12 -\endisadelimtheory
6.13 -%
6.14 -\isatagtheory
6.15 -\isacommand{theory}\isamarkupfalse%
6.16 -\ intro\isanewline
6.17 -\isakeyword{imports}\ Pure\isanewline
6.18 -\isakeyword{begin}%
6.19 -\endisatagtheory
6.20 -{\isafoldtheory}%
6.21 -%
6.22 -\isadelimtheory
6.23 -%
6.24 -\endisadelimtheory
6.25 -%
6.26 -\isamarkupchapter{Introduction%
6.27 -}
6.28 -\isamarkuptrue%
6.29 -%
6.30 -\isamarkupsection{Overview%
6.31 -}
6.32 -\isamarkuptrue%
6.33 -%
6.34 -\begin{isamarkuptext}%
6.35 -The \emph{Isabelle} system essentially provides a generic
6.36 - infrastructure for building deductive systems (programmed in
6.37 - Standard ML), with a special focus on interactive theorem proving in
6.38 - higher-order logics. In the olden days even end-users would refer
6.39 - to certain ML functions (goal commands, tactics, tacticals etc.) to
6.40 - pursue their everyday theorem proving tasks
6.41 - \cite{isabelle-intro,isabelle-ref}.
6.42 -
6.43 - In contrast \emph{Isar} provides an interpreted language environment
6.44 - of its own, which has been specifically tailored for the needs of
6.45 - theory and proof development. Compared to raw ML, the Isabelle/Isar
6.46 - top-level provides a more robust and comfortable development
6.47 - platform, with proper support for theory development graphs,
6.48 - single-step transactions with unlimited undo, etc. The
6.49 - Isabelle/Isar version of the \emph{Proof~General} user interface
6.50 - \cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate
6.51 - front-end for interactive theory and proof development in this
6.52 - advanced theorem proving environment.
6.53 -
6.54 - \medskip Apart from the technical advances over bare-bones ML
6.55 - programming, the main purpose of the Isar language is to provide a
6.56 - conceptually different view on machine-checked proofs
6.57 - \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. ``Isar'' stands for
6.58 - ``Intelligible semi-automated reasoning''. Drawing from both the
6.59 - traditions of informal mathematical proof texts and high-level
6.60 - programming languages, Isar offers a versatile environment for
6.61 - structured formal proof documents. Thus properly written Isar
6.62 - proofs become accessible to a broader audience than unstructured
6.63 - tactic scripts (which typically only provide operational information
6.64 - for the machine). Writing human-readable proof texts certainly
6.65 - requires some additional efforts by the writer to achieve a good
6.66 - presentation, both of formal and informal parts of the text. On the
6.67 - other hand, human-readable formal texts gain some value in their own
6.68 - right, independently of the mechanic proof-checking process.
6.69 -
6.70 - Despite its grand design of structured proof texts, Isar is able to
6.71 - assimilate the old tactical style as an ``improper'' sub-language.
6.72 - This provides an easy upgrade path for existing tactic scripts, as
6.73 - well as additional means for interactive experimentation and
6.74 - debugging of structured proofs. Isabelle/Isar supports a broad
6.75 - range of proof styles, both readable and unreadable ones.
6.76 -
6.77 - \medskip The Isabelle/Isar framework is generic and should work
6.78 - reasonably well for any Isabelle object-logic that conforms to the
6.79 - natural deduction view of the Isabelle/Pure framework. Major
6.80 - Isabelle logics like HOL \cite{isabelle-HOL}, HOLCF
6.81 - \cite{MuellerNvOS99}, FOL \cite{isabelle-logics}, and ZF
6.82 - \cite{isabelle-ZF} have already been set up for end-users.%
6.83 -\end{isamarkuptext}%
6.84 -\isamarkuptrue%
6.85 -%
6.86 -\isamarkupsection{Quick start%
6.87 -}
6.88 -\isamarkuptrue%
6.89 -%
6.90 -\isamarkupsubsection{Terminal sessions%
6.91 -}
6.92 -\isamarkuptrue%
6.93 -%
6.94 -\begin{isamarkuptext}%
6.95 -Isar is already part of Isabelle. The low-level \verb|isabelle| binary provides option \verb|-I| to run the
6.96 - Isabelle/Isar interaction loop at startup, rather than the raw ML
6.97 - top-level. So the most basic way to do anything with Isabelle/Isar
6.98 - is as follows: % FIXME update
6.99 -\begin{ttbox}
6.100 -isabelle -I HOL\medskip
6.101 -\out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip
6.102 -theory Foo imports Main begin;
6.103 -definition foo :: nat where "foo == 1";
6.104 -lemma "0 < foo" by (simp add: foo_def);
6.105 -end;
6.106 -\end{ttbox}
6.107 -
6.108 - Note that any Isabelle/Isar command may be retracted by \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}. See the Isabelle/Isar Quick Reference
6.109 - (\appref{ap:refcard}) for a comprehensive overview of available
6.110 - commands and other language elements.%
6.111 -\end{isamarkuptext}%
6.112 -\isamarkuptrue%
6.113 -%
6.114 -\isamarkupsubsection{Proof General%
6.115 -}
6.116 -\isamarkuptrue%
6.117 -%
6.118 -\begin{isamarkuptext}%
6.119 -Plain TTY-based interaction as above used to be quite feasible with
6.120 - traditional tactic based theorem proving, but developing Isar
6.121 - documents really demands some better user-interface support. The
6.122 - Proof~General environment by David Aspinall
6.123 - \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
6.124 - interface for interactive theorem provers that organizes all the
6.125 - cut-and-paste and forward-backward walk through the text in a very
6.126 - neat way. In Isabelle/Isar, the current position within a partial
6.127 - proof document is equally important than the actual proof state.
6.128 - Thus Proof~General provides the canonical working environment for
6.129 - Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
6.130 - existing Isar documents) and for production work.%
6.131 -\end{isamarkuptext}%
6.132 -\isamarkuptrue%
6.133 -%
6.134 -\isamarkupsubsubsection{Proof~General as default Isabelle interface%
6.135 -}
6.136 -\isamarkuptrue%
6.137 -%
6.138 -\begin{isamarkuptext}%
6.139 -The Isabelle interface wrapper script provides an easy way to invoke
6.140 - Proof~General (including XEmacs or GNU Emacs). The default
6.141 - configuration of Isabelle is smart enough to detect the
6.142 - Proof~General distribution in several canonical places (e.g.\
6.143 - \verb|$ISABELLE_HOME/contrib/ProofGeneral|). Thus the
6.144 - capital \verb|Isabelle| executable would already refer to the
6.145 - \verb|ProofGeneral/isar| interface without further ado. The
6.146 - Isabelle interface script provides several options; pass \verb|-?| to see its usage.
6.147 -
6.148 - With the proper Isabelle interface setup, Isar documents may now be edited by
6.149 - visiting appropriate theory files, e.g.\
6.150 -\begin{ttbox}
6.151 -Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
6.152 -\end{ttbox}
6.153 - Beginners may note the tool bar for navigating forward and backward
6.154 - through the text (this depends on the local Emacs installation).
6.155 - Consult the Proof~General documentation \cite{proofgeneral} for
6.156 - further basic command sequences, in particular ``\verb|C-c C-return|''
6.157 - and ``\verb|C-c u|''.
6.158 -
6.159 - \medskip Proof~General may be also configured manually by giving
6.160 - Isabelle settings like this (see also \cite{isabelle-sys}):
6.161 -
6.162 -\begin{ttbox}
6.163 -ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
6.164 -PROOFGENERAL_OPTIONS=""
6.165 -\end{ttbox}
6.166 - You may have to change \verb|$ISABELLE_HOME/contrib/ProofGeneral| to the actual installation
6.167 - directory of Proof~General.
6.168 -
6.169 - \medskip Apart from the Isabelle command line, defaults for
6.170 - interface options may be given by the \verb|PROOFGENERAL_OPTIONS|
6.171 - setting. For example, the Emacs executable to be used may be
6.172 - configured in Isabelle's settings like this:
6.173 -\begin{ttbox}
6.174 -PROOFGENERAL_OPTIONS="-p xemacs-mule"
6.175 -\end{ttbox}
6.176 -
6.177 - Occasionally, a user's \verb|~/.emacs| file contains code
6.178 - that is incompatible with the (X)Emacs version used by
6.179 - Proof~General, causing the interface startup to fail prematurely.
6.180 - Here the \verb|-u false| option helps to get the interface
6.181 - process up and running. Note that additional Lisp customization
6.182 - code may reside in \verb|proofgeneral-settings.el| of
6.183 - \verb|$ISABELLE_HOME/etc| or \verb|$ISABELLE_HOME_USER/etc|.%
6.184 -\end{isamarkuptext}%
6.185 -\isamarkuptrue%
6.186 -%
6.187 -\isamarkupsubsubsection{The X-Symbol package%
6.188 -}
6.189 -\isamarkuptrue%
6.190 -%
6.191 -\begin{isamarkuptext}%
6.192 -Proof~General incorporates a version of the Emacs X-Symbol package
6.193 - \cite{x-symbol}, which handles proper mathematical symbols displayed
6.194 - on screen. Pass option \verb|-x true| to the Isabelle
6.195 - interface script, or check the appropriate Proof~General menu
6.196 - setting by hand. The main challenge of getting X-Symbol to work
6.197 - properly is the underlying (semi-automated) X11 font setup.
6.198 -
6.199 - \medskip Using proper mathematical symbols in Isabelle theories can
6.200 - be very convenient for readability of large formulas. On the other
6.201 - hand, the plain ASCII sources easily become somewhat unintelligible.
6.202 - For example, \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} would appear as \verb|\<Longrightarrow>| according
6.203 - the default set of Isabelle symbols. Nevertheless, the Isabelle
6.204 - document preparation system (see \secref{sec:document-prep}) will be
6.205 - happy to print non-ASCII symbols properly. It is even possible to
6.206 - invent additional notation beyond the display capabilities of Emacs
6.207 - and X-Symbol.%
6.208 -\end{isamarkuptext}%
6.209 -\isamarkuptrue%
6.210 -%
6.211 -\isamarkupsection{Isabelle/Isar theories%
6.212 -}
6.213 -\isamarkuptrue%
6.214 -%
6.215 -\begin{isamarkuptext}%
6.216 -Isabelle/Isar offers the following main improvements over classic
6.217 - Isabelle.
6.218 -
6.219 - \begin{enumerate}
6.220 -
6.221 - \item A \emph{theory format} that integrates specifications and
6.222 - proofs, supporting interactive development and unlimited undo
6.223 - operation.
6.224 -
6.225 - \item A \emph{formal proof document language} designed to support
6.226 - intelligible semi-automated reasoning. Instead of putting together
6.227 - unreadable tactic scripts, the author is enabled to express the
6.228 - reasoning in way that is close to usual mathematical practice. The
6.229 - old tactical style has been assimilated as ``improper'' language
6.230 - elements.
6.231 -
6.232 - \item A simple document preparation system, for typesetting formal
6.233 - developments together with informal text. The resulting
6.234 - hyper-linked PDF documents are equally well suited for WWW
6.235 - presentation and as printed copies.
6.236 -
6.237 - \end{enumerate}
6.238 -
6.239 - The Isar proof language is embedded into the new theory format as a
6.240 - proper sub-language. Proof mode is entered by stating some
6.241 - \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}} or \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} at the theory level, and
6.242 - left again with the final conclusion (e.g.\ via \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}).
6.243 - A few theory specification mechanisms also require some proof, such
6.244 - as HOL's \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} which demands non-emptiness of the
6.245 - representing sets.%
6.246 -\end{isamarkuptext}%
6.247 -\isamarkuptrue%
6.248 -%
6.249 -\isamarkupsubsection{Document preparation \label{sec:document-prep}%
6.250 -}
6.251 -\isamarkuptrue%
6.252 -%
6.253 -\begin{isamarkuptext}%
6.254 -Isabelle/Isar provides a simple document preparation system based on
6.255 - existing {PDF-\LaTeX} technology, with full support of hyper-links
6.256 - (both local references and URLs) and bookmarks. Thus the results
6.257 - are equally well suited for WWW browsing and as printed copies.
6.258 -
6.259 - \medskip Isabelle generates {\LaTeX} output as part of the run of a
6.260 - \emph{logic session} (see also \cite{isabelle-sys}). Getting
6.261 - started with a working configuration for common situations is quite
6.262 - easy by using the Isabelle \verb|mkdir| and \verb|make|
6.263 - tools. First invoke
6.264 -\begin{ttbox}
6.265 - isatool mkdir Foo
6.266 -\end{ttbox}
6.267 - to initialize a separate directory for session \verb|Foo| ---
6.268 - it is safe to experiment, since \verb|isatool mkdir| never
6.269 - overwrites existing files. Ensure that \verb|Foo/ROOT.ML|
6.270 - holds ML commands to load all theories required for this session;
6.271 - furthermore \verb|Foo/document/root.tex| should include any
6.272 - special {\LaTeX} macro packages required for your document (the
6.273 - default is usually sufficient as a start).
6.274 -
6.275 - The session is controlled by a separate \verb|IsaMakefile|
6.276 - (with crude source dependencies by default). This file is located
6.277 - one level up from the \verb|Foo| directory location. Now
6.278 - invoke
6.279 -\begin{ttbox}
6.280 - isatool make Foo
6.281 -\end{ttbox}
6.282 - to run the \verb|Foo| session, with browser information and
6.283 - document preparation enabled. Unless any errors are reported by
6.284 - Isabelle or {\LaTeX}, the output will appear inside the directory
6.285 - \verb|ISABELLE_BROWSER_INFO|, as reported by the batch job in
6.286 - verbose mode.
6.287 -
6.288 - \medskip You may also consider to tune the \verb|usedir|
6.289 - options in \verb|IsaMakefile|, for example to change the output
6.290 - format from \verb|pdf| to \verb|dvi|, or activate the
6.291 - \verb|-D| option to retain a second copy of the generated
6.292 - {\LaTeX} sources.
6.293 -
6.294 - \medskip See \emph{The Isabelle System Manual} \cite{isabelle-sys}
6.295 - for further details on Isabelle logic sessions and theory
6.296 - presentation. The Isabelle/HOL tutorial \cite{isabelle-hol-book}
6.297 - also covers theory presentation issues.%
6.298 -\end{isamarkuptext}%
6.299 -\isamarkuptrue%
6.300 -%
6.301 -\isamarkupsubsection{How to write Isar proofs anyway? \label{sec:isar-howto}%
6.302 -}
6.303 -\isamarkuptrue%
6.304 -%
6.305 -\begin{isamarkuptext}%
6.306 -This is one of the key questions, of course. First of all, the
6.307 - tactic script emulation of Isabelle/Isar essentially provides a
6.308 - clarified version of the very same unstructured proof style of
6.309 - classic Isabelle. Old-time users should quickly become acquainted
6.310 - with that (slightly degenerative) view of Isar.
6.311 -
6.312 - Writing \emph{proper} Isar proof texts targeted at human readers is
6.313 - quite different, though. Experienced users of the unstructured
6.314 - style may even have to unlearn some of their habits to master proof
6.315 - composition in Isar. In contrast, new users with less experience in
6.316 - old-style tactical proving, but a good understanding of mathematical
6.317 - proof in general, often get started easier.
6.318 -
6.319 - \medskip The present text really is only a reference manual on
6.320 - Isabelle/Isar, not a tutorial. Nevertheless, we will attempt to
6.321 - give some clues of how the concepts introduced here may be put into
6.322 - practice. Especially note that \appref{ap:refcard} provides a quick
6.323 - reference card of the most common Isabelle/Isar language elements.
6.324 -
6.325 - Further issues concerning the Isar concepts are covered in the
6.326 - literature
6.327 - \cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
6.328 - The author's PhD thesis \cite{Wenzel-PhD} presently provides the
6.329 - most complete exposition of Isar foundations, techniques, and
6.330 - applications. A number of example applications are distributed with
6.331 - Isabelle, and available via the Isabelle WWW library (e.g.\
6.332 - \url{http://isabelle.in.tum.de/library/}). The ``Archive of Formal
6.333 - Proofs'' \url{http://afp.sourceforge.net/} also provides plenty of
6.334 - examples, both in proper Isar proof style and unstructured tactic
6.335 - scripts.%
6.336 -\end{isamarkuptext}%
6.337 -\isamarkuptrue%
6.338 -%
6.339 -\isadelimtheory
6.340 -%
6.341 -\endisadelimtheory
6.342 -%
6.343 -\isatagtheory
6.344 -\isacommand{end}\isamarkupfalse%
6.345 -%
6.346 -\endisatagtheory
6.347 -{\isafoldtheory}%
6.348 -%
6.349 -\isadelimtheory
6.350 -%
6.351 -\endisadelimtheory
6.352 -\isanewline
6.353 -\end{isabellebody}%
6.354 -%%% Local Variables:
6.355 -%%% mode: latex
6.356 -%%% TeX-master: "root"
6.357 -%%% End:
7.1 --- a/doc-src/IsarRef/Thy/intro.thy Mon Jun 02 13:21:06 2008 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,304 +0,0 @@
7.4 -(* $Id$ *)
7.5 -
7.6 -theory intro
7.7 -imports Pure
7.8 -begin
7.9 -
7.10 -chapter {* Introduction *}
7.11 -
7.12 -section {* Overview *}
7.13 -
7.14 -text {*
7.15 - The \emph{Isabelle} system essentially provides a generic
7.16 - infrastructure for building deductive systems (programmed in
7.17 - Standard ML), with a special focus on interactive theorem proving in
7.18 - higher-order logics. In the olden days even end-users would refer
7.19 - to certain ML functions (goal commands, tactics, tacticals etc.) to
7.20 - pursue their everyday theorem proving tasks
7.21 - \cite{isabelle-intro,isabelle-ref}.
7.22 -
7.23 - In contrast \emph{Isar} provides an interpreted language environment
7.24 - of its own, which has been specifically tailored for the needs of
7.25 - theory and proof development. Compared to raw ML, the Isabelle/Isar
7.26 - top-level provides a more robust and comfortable development
7.27 - platform, with proper support for theory development graphs,
7.28 - single-step transactions with unlimited undo, etc. The
7.29 - Isabelle/Isar version of the \emph{Proof~General} user interface
7.30 - \cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate
7.31 - front-end for interactive theory and proof development in this
7.32 - advanced theorem proving environment.
7.33 -
7.34 - \medskip Apart from the technical advances over bare-bones ML
7.35 - programming, the main purpose of the Isar language is to provide a
7.36 - conceptually different view on machine-checked proofs
7.37 - \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. ``Isar'' stands for
7.38 - ``Intelligible semi-automated reasoning''. Drawing from both the
7.39 - traditions of informal mathematical proof texts and high-level
7.40 - programming languages, Isar offers a versatile environment for
7.41 - structured formal proof documents. Thus properly written Isar
7.42 - proofs become accessible to a broader audience than unstructured
7.43 - tactic scripts (which typically only provide operational information
7.44 - for the machine). Writing human-readable proof texts certainly
7.45 - requires some additional efforts by the writer to achieve a good
7.46 - presentation, both of formal and informal parts of the text. On the
7.47 - other hand, human-readable formal texts gain some value in their own
7.48 - right, independently of the mechanic proof-checking process.
7.49 -
7.50 - Despite its grand design of structured proof texts, Isar is able to
7.51 - assimilate the old tactical style as an ``improper'' sub-language.
7.52 - This provides an easy upgrade path for existing tactic scripts, as
7.53 - well as additional means for interactive experimentation and
7.54 - debugging of structured proofs. Isabelle/Isar supports a broad
7.55 - range of proof styles, both readable and unreadable ones.
7.56 -
7.57 - \medskip The Isabelle/Isar framework is generic and should work
7.58 - reasonably well for any Isabelle object-logic that conforms to the
7.59 - natural deduction view of the Isabelle/Pure framework. Major
7.60 - Isabelle logics like HOL \cite{isabelle-HOL}, HOLCF
7.61 - \cite{MuellerNvOS99}, FOL \cite{isabelle-logics}, and ZF
7.62 - \cite{isabelle-ZF} have already been set up for end-users.
7.63 -*}
7.64 -
7.65 -
7.66 -section {* Quick start *}
7.67 -
7.68 -subsection {* Terminal sessions *}
7.69 -
7.70 -text {*
7.71 - Isar is already part of Isabelle. The low-level @{verbatim
7.72 - isabelle} binary provides option @{verbatim "-I"} to run the
7.73 - Isabelle/Isar interaction loop at startup, rather than the raw ML
7.74 - top-level. So the most basic way to do anything with Isabelle/Isar
7.75 - is as follows: % FIXME update
7.76 -\begin{ttbox}
7.77 -isabelle -I HOL\medskip
7.78 -\out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip
7.79 -theory Foo imports Main begin;
7.80 -definition foo :: nat where "foo == 1";
7.81 -lemma "0 < foo" by (simp add: foo_def);
7.82 -end;
7.83 -\end{ttbox}
7.84 -
7.85 - Note that any Isabelle/Isar command may be retracted by @{command
7.86 - "undo"}. See the Isabelle/Isar Quick Reference
7.87 - (\appref{ap:refcard}) for a comprehensive overview of available
7.88 - commands and other language elements.
7.89 -*}
7.90 -
7.91 -
7.92 -subsection {* Proof General *}
7.93 -
7.94 -text {*
7.95 - Plain TTY-based interaction as above used to be quite feasible with
7.96 - traditional tactic based theorem proving, but developing Isar
7.97 - documents really demands some better user-interface support. The
7.98 - Proof~General environment by David Aspinall
7.99 - \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
7.100 - interface for interactive theorem provers that organizes all the
7.101 - cut-and-paste and forward-backward walk through the text in a very
7.102 - neat way. In Isabelle/Isar, the current position within a partial
7.103 - proof document is equally important than the actual proof state.
7.104 - Thus Proof~General provides the canonical working environment for
7.105 - Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
7.106 - existing Isar documents) and for production work.
7.107 -*}
7.108 -
7.109 -
7.110 -subsubsection{* Proof~General as default Isabelle interface *}
7.111 -
7.112 -text {*
7.113 - The Isabelle interface wrapper script provides an easy way to invoke
7.114 - Proof~General (including XEmacs or GNU Emacs). The default
7.115 - configuration of Isabelle is smart enough to detect the
7.116 - Proof~General distribution in several canonical places (e.g.\
7.117 - @{verbatim "$ISABELLE_HOME/contrib/ProofGeneral"}). Thus the
7.118 - capital @{verbatim Isabelle} executable would already refer to the
7.119 - @{verbatim "ProofGeneral/isar"} interface without further ado. The
7.120 - Isabelle interface script provides several options; pass @{verbatim
7.121 - "-?"} to see its usage.
7.122 -
7.123 - With the proper Isabelle interface setup, Isar documents may now be edited by
7.124 - visiting appropriate theory files, e.g.\
7.125 -\begin{ttbox}
7.126 -Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
7.127 -\end{ttbox}
7.128 - Beginners may note the tool bar for navigating forward and backward
7.129 - through the text (this depends on the local Emacs installation).
7.130 - Consult the Proof~General documentation \cite{proofgeneral} for
7.131 - further basic command sequences, in particular ``@{verbatim "C-c C-return"}''
7.132 - and ``@{verbatim "C-c u"}''.
7.133 -
7.134 - \medskip Proof~General may be also configured manually by giving
7.135 - Isabelle settings like this (see also \cite{isabelle-sys}):
7.136 -
7.137 -\begin{ttbox}
7.138 -ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
7.139 -PROOFGENERAL_OPTIONS=""
7.140 -\end{ttbox}
7.141 - You may have to change @{verbatim
7.142 - "$ISABELLE_HOME/contrib/ProofGeneral"} to the actual installation
7.143 - directory of Proof~General.
7.144 -
7.145 - \medskip Apart from the Isabelle command line, defaults for
7.146 - interface options may be given by the @{verbatim PROOFGENERAL_OPTIONS}
7.147 - setting. For example, the Emacs executable to be used may be
7.148 - configured in Isabelle's settings like this:
7.149 -\begin{ttbox}
7.150 -PROOFGENERAL_OPTIONS="-p xemacs-mule"
7.151 -\end{ttbox}
7.152 -
7.153 - Occasionally, a user's @{verbatim "~/.emacs"} file contains code
7.154 - that is incompatible with the (X)Emacs version used by
7.155 - Proof~General, causing the interface startup to fail prematurely.
7.156 - Here the @{verbatim "-u false"} option helps to get the interface
7.157 - process up and running. Note that additional Lisp customization
7.158 - code may reside in @{verbatim "proofgeneral-settings.el"} of
7.159 - @{verbatim "$ISABELLE_HOME/etc"} or @{verbatim
7.160 - "$ISABELLE_HOME_USER/etc"}.
7.161 -*}
7.162 -
7.163 -
7.164 -subsubsection {* The X-Symbol package *}
7.165 -
7.166 -text {*
7.167 - Proof~General incorporates a version of the Emacs X-Symbol package
7.168 - \cite{x-symbol}, which handles proper mathematical symbols displayed
7.169 - on screen. Pass option @{verbatim "-x true"} to the Isabelle
7.170 - interface script, or check the appropriate Proof~General menu
7.171 - setting by hand. The main challenge of getting X-Symbol to work
7.172 - properly is the underlying (semi-automated) X11 font setup.
7.173 -
7.174 - \medskip Using proper mathematical symbols in Isabelle theories can
7.175 - be very convenient for readability of large formulas. On the other
7.176 - hand, the plain ASCII sources easily become somewhat unintelligible.
7.177 - For example, @{text "\<Longrightarrow>"} would appear as @{verbatim "\<Longrightarrow>"} according
7.178 - the default set of Isabelle symbols. Nevertheless, the Isabelle
7.179 - document preparation system (see \secref{sec:document-prep}) will be
7.180 - happy to print non-ASCII symbols properly. It is even possible to
7.181 - invent additional notation beyond the display capabilities of Emacs
7.182 - and X-Symbol.
7.183 -*}
7.184 -
7.185 -
7.186 -section {* Isabelle/Isar theories *}
7.187 -
7.188 -text {*
7.189 - Isabelle/Isar offers the following main improvements over classic
7.190 - Isabelle.
7.191 -
7.192 - \begin{enumerate}
7.193 -
7.194 - \item A \emph{theory format} that integrates specifications and
7.195 - proofs, supporting interactive development and unlimited undo
7.196 - operation.
7.197 -
7.198 - \item A \emph{formal proof document language} designed to support
7.199 - intelligible semi-automated reasoning. Instead of putting together
7.200 - unreadable tactic scripts, the author is enabled to express the
7.201 - reasoning in way that is close to usual mathematical practice. The
7.202 - old tactical style has been assimilated as ``improper'' language
7.203 - elements.
7.204 -
7.205 - \item A simple document preparation system, for typesetting formal
7.206 - developments together with informal text. The resulting
7.207 - hyper-linked PDF documents are equally well suited for WWW
7.208 - presentation and as printed copies.
7.209 -
7.210 - \end{enumerate}
7.211 -
7.212 - The Isar proof language is embedded into the new theory format as a
7.213 - proper sub-language. Proof mode is entered by stating some
7.214 - @{command "theorem"} or @{command "lemma"} at the theory level, and
7.215 - left again with the final conclusion (e.g.\ via @{command "qed"}).
7.216 - A few theory specification mechanisms also require some proof, such
7.217 - as HOL's @{command "typedef"} which demands non-emptiness of the
7.218 - representing sets.
7.219 -*}
7.220 -
7.221 -
7.222 -subsection {* Document preparation \label{sec:document-prep} *}
7.223 -
7.224 -text {*
7.225 - Isabelle/Isar provides a simple document preparation system based on
7.226 - existing {PDF-\LaTeX} technology, with full support of hyper-links
7.227 - (both local references and URLs) and bookmarks. Thus the results
7.228 - are equally well suited for WWW browsing and as printed copies.
7.229 -
7.230 - \medskip Isabelle generates {\LaTeX} output as part of the run of a
7.231 - \emph{logic session} (see also \cite{isabelle-sys}). Getting
7.232 - started with a working configuration for common situations is quite
7.233 - easy by using the Isabelle @{verbatim mkdir} and @{verbatim make}
7.234 - tools. First invoke
7.235 -\begin{ttbox}
7.236 - isatool mkdir Foo
7.237 -\end{ttbox}
7.238 - to initialize a separate directory for session @{verbatim Foo} ---
7.239 - it is safe to experiment, since @{verbatim "isatool mkdir"} never
7.240 - overwrites existing files. Ensure that @{verbatim "Foo/ROOT.ML"}
7.241 - holds ML commands to load all theories required for this session;
7.242 - furthermore @{verbatim "Foo/document/root.tex"} should include any
7.243 - special {\LaTeX} macro packages required for your document (the
7.244 - default is usually sufficient as a start).
7.245 -
7.246 - The session is controlled by a separate @{verbatim IsaMakefile}
7.247 - (with crude source dependencies by default). This file is located
7.248 - one level up from the @{verbatim Foo} directory location. Now
7.249 - invoke
7.250 -\begin{ttbox}
7.251 - isatool make Foo
7.252 -\end{ttbox}
7.253 - to run the @{verbatim Foo} session, with browser information and
7.254 - document preparation enabled. Unless any errors are reported by
7.255 - Isabelle or {\LaTeX}, the output will appear inside the directory
7.256 - @{verbatim ISABELLE_BROWSER_INFO}, as reported by the batch job in
7.257 - verbose mode.
7.258 -
7.259 - \medskip You may also consider to tune the @{verbatim usedir}
7.260 - options in @{verbatim IsaMakefile}, for example to change the output
7.261 - format from @{verbatim pdf} to @{verbatim dvi}, or activate the
7.262 - @{verbatim "-D"} option to retain a second copy of the generated
7.263 - {\LaTeX} sources.
7.264 -
7.265 - \medskip See \emph{The Isabelle System Manual} \cite{isabelle-sys}
7.266 - for further details on Isabelle logic sessions and theory
7.267 - presentation. The Isabelle/HOL tutorial \cite{isabelle-hol-book}
7.268 - also covers theory presentation issues.
7.269 -*}
7.270 -
7.271 -
7.272 -subsection {* How to write Isar proofs anyway? \label{sec:isar-howto} *}
7.273 -
7.274 -text {*
7.275 - This is one of the key questions, of course. First of all, the
7.276 - tactic script emulation of Isabelle/Isar essentially provides a
7.277 - clarified version of the very same unstructured proof style of
7.278 - classic Isabelle. Old-time users should quickly become acquainted
7.279 - with that (slightly degenerative) view of Isar.
7.280 -
7.281 - Writing \emph{proper} Isar proof texts targeted at human readers is
7.282 - quite different, though. Experienced users of the unstructured
7.283 - style may even have to unlearn some of their habits to master proof
7.284 - composition in Isar. In contrast, new users with less experience in
7.285 - old-style tactical proving, but a good understanding of mathematical
7.286 - proof in general, often get started easier.
7.287 -
7.288 - \medskip The present text really is only a reference manual on
7.289 - Isabelle/Isar, not a tutorial. Nevertheless, we will attempt to
7.290 - give some clues of how the concepts introduced here may be put into
7.291 - practice. Especially note that \appref{ap:refcard} provides a quick
7.292 - reference card of the most common Isabelle/Isar language elements.
7.293 -
7.294 - Further issues concerning the Isar concepts are covered in the
7.295 - literature
7.296 - \cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
7.297 - The author's PhD thesis \cite{Wenzel-PhD} presently provides the
7.298 - most complete exposition of Isar foundations, techniques, and
7.299 - applications. A number of example applications are distributed with
7.300 - Isabelle, and available via the Isabelle WWW library (e.g.\
7.301 - \url{http://isabelle.in.tum.de/library/}). The ``Archive of Formal
7.302 - Proofs'' \url{http://afp.sourceforge.net/} also provides plenty of
7.303 - examples, both in proper Isar proof style and unstructured tactic
7.304 - scripts.
7.305 -*}
7.306 -
7.307 -end
8.1 --- a/doc-src/IsarRef/isar-ref.tex Mon Jun 02 13:21:06 2008 +0200
8.2 +++ b/doc-src/IsarRef/isar-ref.tex Mon Jun 02 21:01:42 2008 +0200
8.3 @@ -73,7 +73,7 @@
8.4
8.5 \pagenumbering{roman} \tableofcontents \clearfirst
8.6
8.7 -\input{Thy/document/intro.tex}
8.8 +\input{Thy/document/Introduction.tex}
8.9 \input{basics.tex}
8.10 \input{Thy/document/syntax.tex}
8.11 \input{Thy/document/Spec.tex}