--- a/doc-src/IsarRef/IsaMakefile Tue Apr 22 22:00:31 2008 +0200
+++ b/doc-src/IsarRef/IsaMakefile Wed Apr 23 12:13:08 2008 +0200
@@ -21,7 +21,7 @@
Thy: $(LOG)/Pure-Thy.gz
-$(LOG)/Pure-Thy.gz: Thy/ROOT.ML ../antiquote_setup.ML
+$(LOG)/Pure-Thy.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/intro.thy
@$(USEDIR) Pure Thy
--- a/doc-src/IsarRef/Makefile Tue Apr 22 22:00:31 2008 +0200
+++ b/doc-src/IsarRef/Makefile Wed Apr 23 12:13:08 2008 +0200
@@ -13,7 +13,7 @@
NAME = isar-ref
-FILES = isar-ref.tex intro.tex basics.tex syntax.tex pure.tex \
+FILES = isar-ref.tex Thy/document/intro.tex basics.tex syntax.tex pure.tex \
generic.tex logics.tex refcard.tex conversion.tex \
../isar.sty ../rail.sty ../railsetup.sty ../proof.sty \
../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
--- a/doc-src/IsarRef/Thy/ROOT.ML Tue Apr 22 22:00:31 2008 +0200
+++ b/doc-src/IsarRef/Thy/ROOT.ML Wed Apr 23 12:13:08 2008 +0200
@@ -1,2 +1,5 @@
(* $Id$ *)
+
+use "../../antiquote_setup.ML";
+use_thy "intro";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/document/intro.tex Wed Apr 23 12:13:08 2008 +0200
@@ -0,0 +1,376 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{intro}%
+%
+\isadelimtheory
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ intro\isanewline
+\isakeyword{imports}\ CPure\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Introduction%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Overview%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The \emph{Isabelle} system essentially provides a generic
+ infrastructure for building deductive systems (programmed in
+ Standard ML), with a special focus on interactive theorem proving in
+ higher-order logics. In the olden days even end-users would refer
+ to certain ML functions (goal commands, tactics, tacticals etc.) to
+ pursue their everyday theorem proving tasks
+ \cite{isabelle-intro,isabelle-ref}.
+
+ In contrast \emph{Isar} provides an interpreted language environment
+ of its own, which has been specifically tailored for the needs of
+ theory and proof development. Compared to raw ML, the Isabelle/Isar
+ top-level provides a more robust and comfortable development
+ platform, with proper support for theory development graphs,
+ single-step transactions with unlimited undo, etc. The
+ Isabelle/Isar version of the \emph{Proof~General} user interface
+ \cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate
+ front-end for interactive theory and proof development in this
+ advanced theorem proving environment.
+
+ \medskip Apart from the technical advances over bare-bones ML
+ programming, the main purpose of the Isar language is to provide a
+ conceptually different view on machine-checked proofs
+ \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. ``Isar'' stands for
+ ``Intelligible semi-automated reasoning''. Drawing from both the
+ traditions of informal mathematical proof texts and high-level
+ programming languages, Isar offers a versatile environment for
+ structured formal proof documents. Thus properly written Isar
+ proofs become accessible to a broader audience than unstructured
+ tactic scripts (which typically only provide operational information
+ for the machine). Writing human-readable proof texts certainly
+ requires some additional efforts by the writer to achieve a good
+ presentation, both of formal and informal parts of the text. On the
+ other hand, human-readable formal texts gain some value in their own
+ right, independently of the mechanic proof-checking process.
+
+ Despite its grand design of structured proof texts, Isar is able to
+ assimilate the old tactical style as an ``improper'' sub-language.
+ This provides an easy upgrade path for existing tactic scripts, as
+ well as additional means for interactive experimentation and
+ debugging of structured proofs. Isabelle/Isar supports a broad
+ range of proof styles, both readable and unreadable ones.
+
+ \medskip The Isabelle/Isar framework is generic and should work
+ reasonably well for any Isabelle object-logic that conforms to the
+ natural deduction view of the Isabelle/Pure framework. Major
+ Isabelle logics like HOL \cite{isabelle-HOL}, HOLCF
+ \cite{MuellerNvOS99}, FOL \cite{isabelle-logics}, and ZF
+ \cite{isabelle-ZF} have already been set up for end-users.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Quick start%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Terminal sessions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isar is already part of Isabelle. The low-level \texttt{isabelle} binary
+ provides option \texttt{-I} to run the Isabelle/Isar interaction loop at
+ startup, rather than the raw ML top-level. So the most basic way to do
+ anything with Isabelle/Isar is as follows:
+\begin{ttbox}
+isabelle -I HOL\medskip
+\out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip
+theory Foo imports Main begin;
+definition foo :: nat where "foo == 1";
+lemma "0 < foo" by (simp add: foo_def);
+end;
+\end{ttbox}
+
+ Note that any Isabelle/Isar command may be retracted by
+ \texttt{undo}. See the Isabelle/Isar Quick Reference
+ (appendix~\ref{ap:refcard}) for a comprehensive overview of
+ available commands and other language elements.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Proof General%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Plain TTY-based interaction as above used to be quite feasible with
+ traditional tactic based theorem proving, but developing Isar
+ documents really demands some better user-interface support. The
+ Proof~General environment by David Aspinall
+ \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
+ interface for interactive theorem provers that organizes all the
+ cut-and-paste and forward-backward walk through the text in a very
+ neat way. In Isabelle/Isar, the current position within a partial
+ proof document is equally important than the actual proof state.
+ Thus Proof~General provides the canonical working environment for
+ Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
+ existing Isar documents) and for production work.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Proof~General as default Isabelle interface%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The Isabelle interface wrapper script provides an easy way to invoke
+ Proof~General (including XEmacs or GNU Emacs). The default
+ configuration of Isabelle is smart enough to detect the
+ Proof~General distribution in several canonical places (e.g.\
+ \texttt{\$ISABELLE_HOME/contrib/ProofGeneral}). Thus the capital
+ \texttt{Isabelle} executable would already refer to the
+ \texttt{ProofGeneral/isar} interface without further ado. The
+ Isabelle interface script provides several options; pass \verb,-?,
+ to see its usage.
+
+ With the proper Isabelle interface setup, Isar documents may now be edited by
+ visiting appropriate theory files, e.g.\
+\begin{ttbox}
+Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
+\end{ttbox}
+ Beginners may note the tool bar for navigating forward and backward
+ through the text (this depends on the local Emacs installation).
+ Consult the Proof~General documentation \cite{proofgeneral} for
+ further basic command sequences, in particular ``\texttt{C-c
+ C-return}'' and ``\texttt{C-c u}''.
+
+ \medskip Proof~General may be also configured manually by giving
+ Isabelle settings like this (see also \cite{isabelle-sys}):
+
+\begin{ttbox}
+ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
+PROOFGENERAL_OPTIONS=""
+\end{ttbox}
+ You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral}
+ to the actual installation directory of Proof~General.
+
+ \medskip Apart from the Isabelle command line, defaults for
+ interface options may be given by the \texttt{PROOFGENERAL_OPTIONS}
+ setting. For example, the Emacs executable to be used may be
+ configured in Isabelle's settings like this:
+\begin{ttbox}
+PROOFGENERAL_OPTIONS="-p xemacs-mule"
+\end{ttbox}
+
+ Occasionally, a user's \verb,~/.emacs, file contains code that is
+ incompatible with the (X)Emacs version used by Proof~General,
+ causing the interface startup to fail prematurely. Here the
+ \texttt{-u false} option helps to get the interface process up and
+ running. Note that additional Lisp customization code may reside in
+ \texttt{proofgeneral-settings.el} of \texttt{\$ISABELLE_HOME/etc} or
+ \texttt{\$ISABELLE_HOME_USER/etc}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{The X-Symbol package%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Proof~General incorporates a version of the Emacs X-Symbol package
+ \cite{x-symbol}, which handles proper mathematical symbols displayed
+ on screen. Pass option \texttt{-x true} to the Isabelle interface
+ script, or check the appropriate Proof~General menu setting by hand.
+ The main challenge of getting X-Symbol to work properly is the
+ underlying (semi-automated) X11 font setup.
+
+ \medskip Using proper mathematical symbols in Isabelle theories can
+ be very convenient for readability of large formulas. On the other
+ hand, the plain ASCII sources easily become somewhat unintelligible.
+ For example, $\Longrightarrow$ would appear as \verb,\<Longrightarrow>, according
+ the default set of Isabelle symbols. Nevertheless, the Isabelle
+ document preparation system (see \S\ref{sec:document-prep}) will be
+ happy to print non-ASCII symbols properly. It is even possible to
+ invent additional notation beyond the display capabilities of Emacs
+ and X-Symbol.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Isabelle/Isar theories%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle/Isar offers the following main improvements over classic
+ Isabelle.
+
+ \begin{enumerate}
+
+ \item A \emph{theory format} that integrates specifications and
+ proofs, supporting interactive development and unlimited undo
+ operation.
+
+ \item A \emph{formal proof document language} designed to support
+ intelligible semi-automated reasoning. Instead of putting together
+ unreadable tactic scripts, the author is enabled to express the
+ reasoning in way that is close to usual mathematical practice. The
+ old tactical style has been assimilated as ``improper'' language
+ elements.
+
+ \item A simple document preparation system, for typesetting formal
+ developments together with informal text. The resulting
+ hyper-linked PDF documents are equally well suited for WWW
+ presentation and as printed copies.
+
+ \end{enumerate}
+
+ The Isar proof language is embedded into the new theory format as a
+ proper sub-language. Proof mode is entered by stating some
+ $\THEOREMNAME$ or $\LEMMANAME$ at the theory level, and left again
+ with the final conclusion (e.g.\ via $\QEDNAME$). A few theory
+ specification mechanisms also require some proof, such as HOL's
+ $\isarkeyword{typedef}$ which demands non-emptiness of the
+ representing sets.
+
+ New-style theory files may still be associated with separate ML
+ files consisting of plain old tactic scripts. There is no longer
+ any ML binding generated for the theory and theorems, though. ML
+ functions \texttt{theory}, \texttt{thm}, and \texttt{thms} retrieve
+ this information from the context \cite{isabelle-ref}.
+ Nevertheless, migration between classic Isabelle and Isabelle/Isar
+ is relatively easy. Thus users may start to benefit from
+ interactive theory development and document preparation, even before
+ they have any idea of the Isar proof language at all.
+
+ Manual conversion of existing tactic scripts may be done by running
+ two separate Proof~General sessions, one for replaying the old
+ script and the other for the emerging Isabelle/Isar document. Also
+ note that Isar supports emulation commands and methods that support
+ traditional tactic scripts within new-style theories, see
+ appendix~\ref{ap:conv} for more information.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Document preparation \label{sec:document-prep}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle/Isar provides a simple document preparation system based on
+ existing {PDF-\LaTeX} technology, with full support of hyper-links
+ (both local references and URLs), bookmarks, and thumbnails. Thus
+ the results are equally well suited for WWW browsing and as printed
+ copies.
+
+ \medskip
+
+ Isabelle generates {\LaTeX} output as part of the run of a
+ \emph{logic session} (see also \cite{isabelle-sys}). Getting
+ started with a working configuration for common situations is quite
+ easy by using the Isabelle \texttt{mkdir} and \texttt{make} tools.
+ First invoke
+\begin{ttbox}
+ isatool mkdir Foo
+\end{ttbox}
+ to initialize a separate directory for session \texttt{Foo} --- it
+ is safe to experiment, since \texttt{isatool mkdir} never overwrites
+ existing files. Ensure that \texttt{Foo/ROOT.ML} holds ML commands
+ to load all theories required for this session; furthermore
+ \texttt{Foo/document/root.tex} should include any special {\LaTeX}
+ macro packages required for your document (the default is usually
+ sufficient as a start).
+
+ The session is controlled by a separate \texttt{IsaMakefile} (with
+ crude source dependencies by default). This file is located one
+ level up from the \texttt{Foo} directory location. Now invoke
+\begin{ttbox}
+ isatool make Foo
+\end{ttbox}
+ to run the \texttt{Foo} session, with browser information and
+ document preparation enabled. Unless any errors are reported by
+ Isabelle or {\LaTeX}, the output will appear inside the directory
+ \texttt{ISABELLE_BROWSER_INFO}, as reported by the batch job in
+ verbose mode.
+
+ \medskip You may also consider to tune the \texttt{usedir} options
+ in \texttt{IsaMakefile}, for example to change the output format
+ from \texttt{pdf} to \texttt{dvi}, or activate the \texttt{-D}
+ option to retain a second copy of the generated {\LaTeX} sources.
+
+ \medskip See \emph{The Isabelle System Manual} \cite{isabelle-sys}
+ for further details on Isabelle logic sessions and theory
+ presentation. The Isabelle/HOL tutorial \cite{isabelle-hol-book}
+ also covers theory presentation issues.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{How to write Isar proofs anyway? \label{sec:isar-howto}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+This is one of the key questions, of course. First of all, the
+ tactic script emulation of Isabelle/Isar essentially provides a
+ clarified version of the very same unstructured proof style of
+ classic Isabelle. Old-time users should quickly become acquainted
+ with that (slightly degenerative) view of Isar.
+
+ Writing \emph{proper} Isar proof texts targeted at human readers is
+ quite different, though. Experienced users of the unstructured
+ style may even have to unlearn some of their habits to master proof
+ composition in Isar. In contrast, new users with less experience in
+ old-style tactical proving, but a good understanding of mathematical
+ proof in general, often get started easier.
+
+ \medskip The present text really is only a reference manual on
+ Isabelle/Isar, not a tutorial. Nevertheless, we will attempt to
+ give some clues of how the concepts introduced here may be put into
+ practice. Appendix~\ref{ap:refcard} provides a quick reference card
+ of the most common Isabelle/Isar language elements.
+ Appendix~\ref{ap:conv} offers some practical hints on converting
+ existing Isabelle theories and proof scripts to the new format
+ (without restructuring proofs).
+
+ Further issues concerning the Isar concepts are covered in the
+ literature
+ \cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
+ The author's PhD thesis \cite{Wenzel-PhD} presently provides the
+ most complete exposition of Isar foundations, techniques, and
+ applications. A number of example applications are distributed with
+ Isabelle, and available via the Isabelle WWW library (e.g.\
+ \url{http://isabelle.in.tum.de/library/}). The ``Archive of Formal
+ Proofs'' \url{http://afp.sourceforge.net/} also provides plenty of
+ examples, both in proper Isar proof style and unstructured tactic
+ scripts.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- a/doc-src/IsarRef/Thy/document/session.tex Tue Apr 22 22:00:31 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/session.tex Wed Apr 23 12:13:08 2008 +0200
@@ -1,3 +1,5 @@
+\input{intro.tex}
+
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/intro.thy Wed Apr 23 12:13:08 2008 +0200
@@ -0,0 +1,321 @@
+
+theory intro
+imports CPure
+begin
+
+chapter {* Introduction *}
+
+section {* Overview *}
+
+text {*
+ The \emph{Isabelle} system essentially provides a generic
+ infrastructure for building deductive systems (programmed in
+ Standard ML), with a special focus on interactive theorem proving in
+ higher-order logics. In the olden days even end-users would refer
+ to certain ML functions (goal commands, tactics, tacticals etc.) to
+ pursue their everyday theorem proving tasks
+ \cite{isabelle-intro,isabelle-ref}.
+
+ In contrast \emph{Isar} provides an interpreted language environment
+ of its own, which has been specifically tailored for the needs of
+ theory and proof development. Compared to raw ML, the Isabelle/Isar
+ top-level provides a more robust and comfortable development
+ platform, with proper support for theory development graphs,
+ single-step transactions with unlimited undo, etc. The
+ Isabelle/Isar version of the \emph{Proof~General} user interface
+ \cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate
+ front-end for interactive theory and proof development in this
+ advanced theorem proving environment.
+
+ \medskip Apart from the technical advances over bare-bones ML
+ programming, the main purpose of the Isar language is to provide a
+ conceptually different view on machine-checked proofs
+ \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. ``Isar'' stands for
+ ``Intelligible semi-automated reasoning''. Drawing from both the
+ traditions of informal mathematical proof texts and high-level
+ programming languages, Isar offers a versatile environment for
+ structured formal proof documents. Thus properly written Isar
+ proofs become accessible to a broader audience than unstructured
+ tactic scripts (which typically only provide operational information
+ for the machine). Writing human-readable proof texts certainly
+ requires some additional efforts by the writer to achieve a good
+ presentation, both of formal and informal parts of the text. On the
+ other hand, human-readable formal texts gain some value in their own
+ right, independently of the mechanic proof-checking process.
+
+ Despite its grand design of structured proof texts, Isar is able to
+ assimilate the old tactical style as an ``improper'' sub-language.
+ This provides an easy upgrade path for existing tactic scripts, as
+ well as additional means for interactive experimentation and
+ debugging of structured proofs. Isabelle/Isar supports a broad
+ range of proof styles, both readable and unreadable ones.
+
+ \medskip The Isabelle/Isar framework is generic and should work
+ reasonably well for any Isabelle object-logic that conforms to the
+ natural deduction view of the Isabelle/Pure framework. Major
+ Isabelle logics like HOL \cite{isabelle-HOL}, HOLCF
+ \cite{MuellerNvOS99}, FOL \cite{isabelle-logics}, and ZF
+ \cite{isabelle-ZF} have already been set up for end-users.
+*}
+
+
+section {* Quick start *}
+
+subsection {* Terminal sessions *}
+
+text {*
+ Isar is already part of Isabelle. The low-level \texttt{isabelle} binary
+ provides option \texttt{-I} to run the Isabelle/Isar interaction loop at
+ startup, rather than the raw ML top-level. So the most basic way to do
+ anything with Isabelle/Isar is as follows:
+\begin{ttbox}
+isabelle -I HOL\medskip
+\out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip
+theory Foo imports Main begin;
+definition foo :: nat where "foo == 1";
+lemma "0 < foo" by (simp add: foo_def);
+end;
+\end{ttbox}
+
+ Note that any Isabelle/Isar command may be retracted by
+ \texttt{undo}. See the Isabelle/Isar Quick Reference
+ (appendix~\ref{ap:refcard}) for a comprehensive overview of
+ available commands and other language elements.
+*}
+
+
+subsection {* Proof General *}
+
+text {*
+ Plain TTY-based interaction as above used to be quite feasible with
+ traditional tactic based theorem proving, but developing Isar
+ documents really demands some better user-interface support. The
+ Proof~General environment by David Aspinall
+ \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
+ interface for interactive theorem provers that organizes all the
+ cut-and-paste and forward-backward walk through the text in a very
+ neat way. In Isabelle/Isar, the current position within a partial
+ proof document is equally important than the actual proof state.
+ Thus Proof~General provides the canonical working environment for
+ Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
+ existing Isar documents) and for production work.
+*}
+
+
+subsubsection{* Proof~General as default Isabelle interface *}
+
+text {*
+ The Isabelle interface wrapper script provides an easy way to invoke
+ Proof~General (including XEmacs or GNU Emacs). The default
+ configuration of Isabelle is smart enough to detect the
+ Proof~General distribution in several canonical places (e.g.\
+ \texttt{\$ISABELLE_HOME/contrib/ProofGeneral}). Thus the capital
+ \texttt{Isabelle} executable would already refer to the
+ \texttt{ProofGeneral/isar} interface without further ado. The
+ Isabelle interface script provides several options; pass \verb,-?,
+ to see its usage.
+
+ With the proper Isabelle interface setup, Isar documents may now be edited by
+ visiting appropriate theory files, e.g.\
+\begin{ttbox}
+Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
+\end{ttbox}
+ Beginners may note the tool bar for navigating forward and backward
+ through the text (this depends on the local Emacs installation).
+ Consult the Proof~General documentation \cite{proofgeneral} for
+ further basic command sequences, in particular ``\texttt{C-c
+ C-return}'' and ``\texttt{C-c u}''.
+
+ \medskip Proof~General may be also configured manually by giving
+ Isabelle settings like this (see also \cite{isabelle-sys}):
+
+\begin{ttbox}
+ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
+PROOFGENERAL_OPTIONS=""
+\end{ttbox}
+ You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral}
+ to the actual installation directory of Proof~General.
+
+ \medskip Apart from the Isabelle command line, defaults for
+ interface options may be given by the \texttt{PROOFGENERAL_OPTIONS}
+ setting. For example, the Emacs executable to be used may be
+ configured in Isabelle's settings like this:
+\begin{ttbox}
+PROOFGENERAL_OPTIONS="-p xemacs-mule"
+\end{ttbox}
+
+ Occasionally, a user's \verb,~/.emacs, file contains code that is
+ incompatible with the (X)Emacs version used by Proof~General,
+ causing the interface startup to fail prematurely. Here the
+ \texttt{-u false} option helps to get the interface process up and
+ running. Note that additional Lisp customization code may reside in
+ \texttt{proofgeneral-settings.el} of \texttt{\$ISABELLE_HOME/etc} or
+ \texttt{\$ISABELLE_HOME_USER/etc}.
+*}
+
+
+subsubsection {* The X-Symbol package *}
+
+text {*
+ Proof~General incorporates a version of the Emacs X-Symbol package
+ \cite{x-symbol}, which handles proper mathematical symbols displayed
+ on screen. Pass option \texttt{-x true} to the Isabelle interface
+ script, or check the appropriate Proof~General menu setting by hand.
+ The main challenge of getting X-Symbol to work properly is the
+ underlying (semi-automated) X11 font setup.
+
+ \medskip Using proper mathematical symbols in Isabelle theories can
+ be very convenient for readability of large formulas. On the other
+ hand, the plain ASCII sources easily become somewhat unintelligible.
+ For example, $\Longrightarrow$ would appear as \verb,\<Longrightarrow>, according
+ the default set of Isabelle symbols. Nevertheless, the Isabelle
+ document preparation system (see \S\ref{sec:document-prep}) will be
+ happy to print non-ASCII symbols properly. It is even possible to
+ invent additional notation beyond the display capabilities of Emacs
+ and X-Symbol.
+*}
+
+
+section {* Isabelle/Isar theories *}
+
+text {*
+ Isabelle/Isar offers the following main improvements over classic
+ Isabelle.
+
+ \begin{enumerate}
+
+ \item A \emph{theory format} that integrates specifications and
+ proofs, supporting interactive development and unlimited undo
+ operation.
+
+ \item A \emph{formal proof document language} designed to support
+ intelligible semi-automated reasoning. Instead of putting together
+ unreadable tactic scripts, the author is enabled to express the
+ reasoning in way that is close to usual mathematical practice. The
+ old tactical style has been assimilated as ``improper'' language
+ elements.
+
+ \item A simple document preparation system, for typesetting formal
+ developments together with informal text. The resulting
+ hyper-linked PDF documents are equally well suited for WWW
+ presentation and as printed copies.
+
+ \end{enumerate}
+
+ The Isar proof language is embedded into the new theory format as a
+ proper sub-language. Proof mode is entered by stating some
+ $\THEOREMNAME$ or $\LEMMANAME$ at the theory level, and left again
+ with the final conclusion (e.g.\ via $\QEDNAME$). A few theory
+ specification mechanisms also require some proof, such as HOL's
+ $\isarkeyword{typedef}$ which demands non-emptiness of the
+ representing sets.
+
+ New-style theory files may still be associated with separate ML
+ files consisting of plain old tactic scripts. There is no longer
+ any ML binding generated for the theory and theorems, though. ML
+ functions \texttt{theory}, \texttt{thm}, and \texttt{thms} retrieve
+ this information from the context \cite{isabelle-ref}.
+ Nevertheless, migration between classic Isabelle and Isabelle/Isar
+ is relatively easy. Thus users may start to benefit from
+ interactive theory development and document preparation, even before
+ they have any idea of the Isar proof language at all.
+
+ Manual conversion of existing tactic scripts may be done by running
+ two separate Proof~General sessions, one for replaying the old
+ script and the other for the emerging Isabelle/Isar document. Also
+ note that Isar supports emulation commands and methods that support
+ traditional tactic scripts within new-style theories, see
+ appendix~\ref{ap:conv} for more information.
+*}
+
+
+subsection {* Document preparation \label{sec:document-prep} *}
+
+text {*
+ Isabelle/Isar provides a simple document preparation system based on
+ existing {PDF-\LaTeX} technology, with full support of hyper-links
+ (both local references and URLs), bookmarks, and thumbnails. Thus
+ the results are equally well suited for WWW browsing and as printed
+ copies.
+
+ \medskip
+
+ Isabelle generates {\LaTeX} output as part of the run of a
+ \emph{logic session} (see also \cite{isabelle-sys}). Getting
+ started with a working configuration for common situations is quite
+ easy by using the Isabelle \texttt{mkdir} and \texttt{make} tools.
+ First invoke
+\begin{ttbox}
+ isatool mkdir Foo
+\end{ttbox}
+ to initialize a separate directory for session \texttt{Foo} --- it
+ is safe to experiment, since \texttt{isatool mkdir} never overwrites
+ existing files. Ensure that \texttt{Foo/ROOT.ML} holds ML commands
+ to load all theories required for this session; furthermore
+ \texttt{Foo/document/root.tex} should include any special {\LaTeX}
+ macro packages required for your document (the default is usually
+ sufficient as a start).
+
+ The session is controlled by a separate \texttt{IsaMakefile} (with
+ crude source dependencies by default). This file is located one
+ level up from the \texttt{Foo} directory location. Now invoke
+\begin{ttbox}
+ isatool make Foo
+\end{ttbox}
+ to run the \texttt{Foo} session, with browser information and
+ document preparation enabled. Unless any errors are reported by
+ Isabelle or {\LaTeX}, the output will appear inside the directory
+ \texttt{ISABELLE_BROWSER_INFO}, as reported by the batch job in
+ verbose mode.
+
+ \medskip You may also consider to tune the \texttt{usedir} options
+ in \texttt{IsaMakefile}, for example to change the output format
+ from \texttt{pdf} to \texttt{dvi}, or activate the \texttt{-D}
+ option to retain a second copy of the generated {\LaTeX} sources.
+
+ \medskip See \emph{The Isabelle System Manual} \cite{isabelle-sys}
+ for further details on Isabelle logic sessions and theory
+ presentation. The Isabelle/HOL tutorial \cite{isabelle-hol-book}
+ also covers theory presentation issues.
+*}
+
+
+subsection {* How to write Isar proofs anyway? \label{sec:isar-howto} *}
+
+text {*
+ This is one of the key questions, of course. First of all, the
+ tactic script emulation of Isabelle/Isar essentially provides a
+ clarified version of the very same unstructured proof style of
+ classic Isabelle. Old-time users should quickly become acquainted
+ with that (slightly degenerative) view of Isar.
+
+ Writing \emph{proper} Isar proof texts targeted at human readers is
+ quite different, though. Experienced users of the unstructured
+ style may even have to unlearn some of their habits to master proof
+ composition in Isar. In contrast, new users with less experience in
+ old-style tactical proving, but a good understanding of mathematical
+ proof in general, often get started easier.
+
+ \medskip The present text really is only a reference manual on
+ Isabelle/Isar, not a tutorial. Nevertheless, we will attempt to
+ give some clues of how the concepts introduced here may be put into
+ practice. Appendix~\ref{ap:refcard} provides a quick reference card
+ of the most common Isabelle/Isar language elements.
+ Appendix~\ref{ap:conv} offers some practical hints on converting
+ existing Isabelle theories and proof scripts to the new format
+ (without restructuring proofs).
+
+ Further issues concerning the Isar concepts are covered in the
+ literature
+ \cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
+ The author's PhD thesis \cite{Wenzel-PhD} presently provides the
+ most complete exposition of Isar foundations, techniques, and
+ applications. A number of example applications are distributed with
+ Isabelle, and available via the Isabelle WWW library (e.g.\
+ \url{http://isabelle.in.tum.de/library/}). The ``Archive of Formal
+ Proofs'' \url{http://afp.sourceforge.net/} also provides plenty of
+ examples, both in proper Isar proof style and unstructured tactic
+ scripts.
+*}
+
+end
--- a/doc-src/IsarRef/intro.tex Tue Apr 22 22:00:31 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,334 +0,0 @@
-
-\chapter{Introduction}
-
-\section{Overview}
-
-The \emph{Isabelle} system essentially provides a generic infrastructure for
-building deductive systems (programmed in Standard ML), with a special focus
-on interactive theorem proving in higher-order logics. In the olden days even
-end-users would refer to certain ML functions (goal commands, tactics,
-tacticals etc.) to pursue their everyday theorem proving tasks
-\cite{isabelle-intro,isabelle-ref}.
-
-In contrast \emph{Isar} provides an interpreted language environment of its
-own, which has been specifically tailored for the needs of theory and proof
-development. Compared to raw ML, the Isabelle/Isar top-level provides a more
-robust and comfortable development platform, with proper support for theory
-development graphs, single-step transactions with unlimited undo, etc. The
-Isabelle/Isar version of the \emph{Proof~General} user interface
-\cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate front-end for
-interactive theory and proof development in this advanced theorem proving
-environment.
-
-\medskip Apart from the technical advances over bare-bones ML programming, the
-main purpose of the Isar language is to provide a conceptually different view
-on machine-checked proofs \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. ``Isar''
-stands for ``Intelligible semi-automated reasoning''. Drawing from both the
-traditions of informal mathematical proof texts and high-level programming
-languages, Isar offers a versatile environment for structured formal proof
-documents. Thus properly written Isar proofs become accessible to a broader
-audience than unstructured tactic scripts (which typically only provide
-operational information for the machine). Writing human-readable proof texts
-certainly requires some additional efforts by the writer to achieve a good
-presentation, both of formal and informal parts of the text. On the other
-hand, human-readable formal texts gain some value in their own right,
-independently of the mechanic proof-checking process.
-
-Despite its grand design of structured proof texts, Isar is able to assimilate
-the old tactical style as an ``improper'' sub-language. This provides an easy
-upgrade path for existing tactic scripts, as well as additional means for
-interactive experimentation and debugging of structured proofs. Isabelle/Isar
-supports a broad range of proof styles, both readable and unreadable ones.
-
-\medskip The Isabelle/Isar framework is generic and should work reasonably
-well for any Isabelle object-logic that conforms to the natural deduction view
-of the Isabelle/Pure framework. Major Isabelle logics like HOL
-\cite{isabelle-HOL}, HOLCF \cite{MuellerNvOS99}, FOL \cite{isabelle-logics},
-and ZF \cite{isabelle-ZF} have already been set up for end-users.
-Nonetheless, much of the existing body of theories still consist of old-style
-theory files with accompanied ML code for proof scripts; this legacy will be
-gradually converted in due time.
-
-
-\section{Quick start}
-
-\subsection{Terminal sessions}
-
-Isar is already part of Isabelle. The low-level \texttt{isabelle} binary
-provides option \texttt{-I} to run the Isabelle/Isar interaction loop at
-startup, rather than the raw ML top-level. So the most basic way to do
-anything with Isabelle/Isar is as follows:
-\begin{ttbox}
-isabelle -I HOL\medskip
-\out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip
-theory Foo imports Main begin;
-constdefs foo :: nat "foo == 1";
-lemma "0 < foo" by (simp add: foo_def);
-end;
-\end{ttbox}
-Note that any Isabelle/Isar command may be retracted by \texttt{undo}. See
-the Isabelle/Isar Quick Reference (appendix~\ref{ap:refcard}) for a
-comprehensive overview of available commands and other language elements.
-
-
-\subsection{Proof~General}
-
-Plain TTY-based interaction as above used to be quite feasible with
-traditional tactic based theorem proving, but developing Isar documents really
-demands some better user-interface support. The Proof~General environment by
-David Aspinall \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
-interface for interactive theorem provers that organizes all the cut-and-paste
-and forward-backward walk through the text in a very neat way. In
-Isabelle/Isar, the current position within a partial proof document is equally
-important than the actual proof state. Thus Proof~General provides the
-canonical working environment for Isabelle/Isar, both for getting acquainted
-(e.g.\ by replaying existing Isar documents) and for production work.
-
-
-\subsubsection{Proof~General as default Isabelle interface}
-
-The Isabelle interface wrapper script provides an easy way to invoke
-Proof~General (including XEmacs or GNU Emacs). The default
-configuration of Isabelle is smart enough to detect the Proof~General
-distribution in several canonical places (e.g.\
-\texttt{\$ISABELLE_HOME/contrib/ProofGeneral}). Thus the capital
-\texttt{Isabelle} executable would already refer to the
-\texttt{ProofGeneral/isar} interface without further ado. The
-Isabelle interface script provides several options; pass \verb,-?, to
-see its usage.
-
-With the proper Isabelle interface setup, Isar documents may now be edited by
-visiting appropriate theory files, e.g.\
-\begin{ttbox}
-Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
-\end{ttbox}
-Beginners may note the tool bar for navigating forward and backward through
-the text (this depends on the local Emacs installation). Consult the
-Proof~General documentation \cite{proofgeneral} for further basic command
-sequences, in particular ``\texttt{C-c C-return}'' and ``\texttt{C-c u}''.
-
-\medskip
-
-Proof~General may be also configured manually by giving Isabelle settings like
-this (see also \cite{isabelle-sys}):
-\begin{ttbox}
-ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
-PROOFGENERAL_OPTIONS=""
-\end{ttbox}
-You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
-actual installation directory of Proof~General.
-
-\medskip
-
-Apart from the Isabelle command line, defaults for interface options may be
-given by the \texttt{PROOFGENERAL_OPTIONS} setting. For example, the Emacs
-executable to be used may be configured in Isabelle's settings like this:
-\begin{ttbox}
-PROOFGENERAL_OPTIONS="-p xemacs-mule"
-\end{ttbox}
-
-Occasionally, a user's \verb,~/.emacs, file contains code that is incompatible
-with the (X)Emacs version used by Proof~General, causing the interface startup
-to fail prematurely. Here the \texttt{-u false} option helps to get the
-interface process up and running. Note that additional Lisp customization
-code may reside in \texttt{proofgeneral-settings.el} of
-\texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc}.
-
-
-\subsubsection{The X-Symbol package}
-
-Proof~General provides native support for the Emacs X-Symbol package
-\cite{x-symbol}, which handles proper mathematical symbols displayed on
-screen. Pass option \texttt{-x true} to the Isabelle interface script, or
-check the appropriate Proof~General menu setting by hand. In any case, the
-X-Symbol package must have been properly installed already.
-
-Contrary to what you may expect from the documentation of X-Symbol, the
-package is very easy to install and configures itself automatically. The
-default configuration of Isabelle is smart enough to detect the X-Symbol
-package in several canonical places (e.g.\
-\texttt{\$ISABELLE_HOME/contrib/x-symbol}).
-
-\medskip
-
-Using proper mathematical symbols in Isabelle theories can be very convenient
-for readability of large formulas. On the other hand, the plain ASCII sources
-easily become somewhat unintelligible. For example, $\Longrightarrow$ would
-appear as \verb,\<Longrightarrow>, according the default set of Isabelle
-symbols. Nevertheless, the Isabelle document preparation system (see
-\S\ref{sec:document-prep}) will be happy to print non-ASCII symbols properly.
-It is even possible to invent additional notation beyond the display
-capabilities of Emacs and X-Symbol.
-
-
-\section{Isabelle/Isar theories}
-
-Isabelle/Isar offers the following main improvements over classic Isabelle.
-\begin{enumerate}
-
-\item A new \emph{theory format}, occasionally referred to as ``new-style
- theories'', supporting interactive development and unlimited undo operation.
-
-\item A \emph{formal proof document language} designed to support intelligible
- semi-automated reasoning. Instead of putting together unreadable tactic
- scripts, the author is enabled to express the reasoning in way that is close
- to usual mathematical practice. The old tactical style has been assimilated
- as ``improper'' language elements.
-
-\item A simple document preparation system, for typesetting formal
- developments together with informal text. The resulting hyper-linked PDF
- documents are equally well suited for WWW presentation and as printed
- copies.
-
-\end{enumerate}
-
-The Isar proof language is embedded into the new theory format as a proper
-sub-language. Proof mode is entered by stating some $\THEOREMNAME$ or
-$\LEMMANAME$ at the theory level, and left again with the final conclusion
-(e.g.\ via $\QEDNAME$). A few theory specification mechanisms also require
-some proof, such as HOL's $\isarkeyword{typedef}$ which demands non-emptiness
-of the representing sets.
-
-New-style theory files may still be associated with separate ML files
-consisting of plain old tactic scripts. There is no longer any ML binding
-generated for the theory and theorems, though. ML functions \texttt{theory},
-\texttt{thm}, and \texttt{thms} retrieve this information from the context
-\cite{isabelle-ref}. Nevertheless, migration between classic Isabelle and
-Isabelle/Isar is relatively easy. Thus users may start to benefit from
-interactive theory development and document preparation, even before they have
-any idea of the Isar proof language at all.
-
-\begin{warn}
- Proof~General does \emph{not} support mixed interactive development of
- classic Isabelle theory files or tactic scripts, together with Isar
- documents. The ``\texttt{isa}'' and ``\texttt{isar}'' versions of
- Proof~General are handled as two different theorem proving systems, only one
- of these may be active at the same time.
-\end{warn}
-
-Manual conversion of existing tactic scripts may be done by running two
-separate Proof~General sessions, one for replaying the old script and the
-other for the emerging Isabelle/Isar document. Also note that Isar supports
-emulation commands and methods that support traditional tactic scripts within
-new-style theories, see appendix~\ref{ap:conv} for more information.
-
-
-\subsection{Document preparation}\label{sec:document-prep}
-
-Isabelle/Isar provides a simple document preparation system based on existing
-{PDF-\LaTeX} technology, with full support of hyper-links (both local
-references and URLs), bookmarks, and thumbnails. Thus the results are equally
-well suited for WWW browsing and as printed copies.
-
-\medskip
-
-Isabelle generates {\LaTeX} output as part of the run of a \emph{logic
- session} (see also \cite{isabelle-sys}). Getting started with a working
-configuration for common situations is quite easy by using the Isabelle
-\texttt{mkdir} and \texttt{make} tools. First invoke
-\begin{ttbox}
- isatool mkdir Foo
-\end{ttbox}
-to initialize a separate directory for session \texttt{Foo} --- it is safe to
-experiment, since \texttt{isatool mkdir} never overwrites existing files.
-Ensure that \texttt{Foo/ROOT.ML} holds ML commands to load all theories
-required for this session; furthermore \texttt{Foo/document/root.tex} should
-include any special {\LaTeX} macro packages required for your document (the
-default is usually sufficient as a start).
-
-The session is controlled by a separate \texttt{IsaMakefile} (with crude
-source dependencies by default). This file is located one level up from the
-\texttt{Foo} directory location. Now invoke
-\begin{ttbox}
- isatool make Foo
-\end{ttbox}
-to run the \texttt{Foo} session, with browser information and document
-preparation enabled. Unless any errors are reported by Isabelle or {\LaTeX},
-the output will appear inside the directory \texttt{ISABELLE_BROWSER_INFO}, as
-reported by the batch job in verbose mode.
-
-\medskip
-
-You may also consider to tune the \texttt{usedir} options in
-\texttt{IsaMakefile}, for example to change the output format from
-\texttt{pdf} to \texttt{dvi}, or activate the \texttt{-D} option to retain a
-second copy of the generated {\LaTeX} sources.
-
-\medskip
-
-See \emph{The Isabelle System Manual} \cite{isabelle-sys} for further details
-on Isabelle logic sessions and theory presentation. The Isabelle/HOL tutorial
-\cite{isabelle-hol-book} also covers theory presentation issues.
-
-
-\subsection{How to write Isar proofs anyway?}\label{sec:isar-howto}
-
-This is one of the key questions, of course. First of all, the tactic script
-emulation of Isabelle/Isar essentially provides a clarified version of the
-very same unstructured proof style of classic Isabelle. Old-time users should
-quickly become acquainted with that (slightly degenerative) view of Isar.
-
-Writing \emph{proper} Isar proof texts targeted at human readers is quite
-different, though. Experienced users of the unstructured style may even have
-to unlearn some of their habits to master proof composition in Isar. In
-contrast, new users with less experience in old-style tactical proving, but a
-good understanding of mathematical proof in general, often get started easier.
-
-\medskip The present text really is only a reference manual on Isabelle/Isar,
-not a tutorial. Nevertheless, we will attempt to give some clues of how the
-concepts introduced here may be put into practice. Appendix~\ref{ap:refcard}
-provides a quick reference card of the most common Isabelle/Isar language
-elements. Appendix~\ref{ap:conv} offers some practical hints on converting
-existing Isabelle theories and proof scripts to the new format (without
-restructuring proofs).
-
-Further issues concerning the Isar concepts are covered in the literature
-\cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
-The author's PhD thesis \cite{Wenzel-PhD} presently provides the most complete
-exposition of Isar foundations, techniques, and applications. A number of
-example applications are distributed with Isabelle, and available via the
-Isabelle WWW library (e.g.\ \url{http://isabelle.in.tum.de/library/}). As a
-general rule of thumb, more recent Isabelle applications that also include a
-separate ``document'' (in PDF) are more likely to consist of proper
-Isabelle/Isar theories and proofs.
-
-%FIXME
-% The following examples may be of particular interest. Apart from the plain
-% sources represented in HTML, these Isabelle sessions also provide actual
-% documents (in PDF).
-% \begin{itemize}
-% \item \url{http://isabelle.in.tum.de/library/HOL/Isar_examples/} is a
-% collection of introductory examples.
-% \item \url{http://isabelle.in.tum.de/library/HOL/Lattice/} is an example of
-% typical mathematics-style reasoning in ``axiomatic'' structures.
-% \item \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/HahnBanach/} is a
-% big mathematics application on infinitary vector spaces and functional
-% analysis.
-% \item \url{http://isabelle.in.tum.de/library/HOL/Lambda/} develops fundamental
-% properties of $\lambda$-calculus (Church-Rosser and termination).
-
-% This may serve as a realistic example of porting of legacy proof scripts
-% into Isar tactic emulation scripts.
-% \item \url{http://isabelle.in.tum.de/library/HOL/Unix/} gives a mathematical
-% model of the main aspects of the Unix file-system including its security
-% model, but ignoring processes. A few odd effects caused by the general
-% ``worse-is-better'' approach followed in Unix are discussed within the
-% formal model.
-
-% This example represents a non-trivial verification task, with all proofs
-% carefully worked out using the proper part of the Isar proof language;
-% unstructured scripts are only used for symbolic evaluation.
-% \item \url{http://isabelle.in.tum.de/library/HOL/MicroJava/} is a
-% formalization of a fragment of Java, together with a corresponding virtual
-% machine and a specification of its bytecode verifier and a lightweight
-% bytecode verifier, including proofs of type-safety.
-
-% This represents a very ``realistic'' example of large formalizations
-% performed in form of tactic emulation scripts and proper Isar proof texts.
-% \end{itemize}
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "isar-ref"
-%%% End:
--- a/doc-src/IsarRef/isar-ref.tex Tue Apr 22 22:00:31 2008 +0200
+++ b/doc-src/IsarRef/isar-ref.tex Wed Apr 23 12:13:08 2008 +0200
@@ -9,6 +9,10 @@
\usepackage{style}
\usepackage{../pdfsetup}
+\hyphenation{Isabelle}
+\hyphenation{Isar}
+
+\isadroptag{theory}
\title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
\author{\emph{Markus Wenzel} \\ TU M\"unchen}
@@ -64,16 +68,16 @@
\pagenumbering{roman} \tableofcontents \clearfirst
-\include{intro}
-\include{basics}
-\include{syntax}
-\include{pure}
-\include{generic}
-\include{logics}
+\input{Thy/document/intro.tex}
+\input{basics.tex}
+\input{syntax.tex}
+\input{pure.tex}
+\input{generic.tex}
+\input{logics.tex}
\appendix
-\include{refcard}
-\include{conversion}
+\input{refcard.tex}
+\input{conversion.tex}
\begingroup
\bibliographystyle{plain} \small\raggedright\frenchspacing