--- a/doc-src/IsarRef/IsaMakefile Mon Jun 02 13:21:06 2008 +0200
+++ b/doc-src/IsarRef/IsaMakefile Mon Jun 02 21:01:42 2008 +0200
@@ -21,21 +21,24 @@
HOL-IsarRef: $(LOG)/HOL-IsarRef.gz
-$(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/intro.thy \
- Thy/syntax.thy Thy/Spec.thy Thy/Proof.thy Thy/pure.thy Thy/Generic.thy \
- Thy/HOL_Specific.thy Thy/Quick_Reference.thy Thy/ML_Tactic.thy
+$(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML \
+ Thy/Introduction.thy Thy/syntax.thy Thy/Spec.thy Thy/Proof.thy \
+ Thy/pure.thy Thy/Generic.thy Thy/HOL_Specific.thy \
+ Thy/Quick_Reference.thy Thy/ML_Tactic.thy
@$(USEDIR) -s IsarRef HOL Thy
HOLCF-IsarRef: $(LOG)/HOLCF-IsarRef.gz
-$(LOG)/HOLCF-IsarRef.gz: Thy/ROOT-HOLCF.ML ../antiquote_setup.ML Thy/HOLCF_Specific.thy
+$(LOG)/HOLCF-IsarRef.gz: Thy/ROOT-HOLCF.ML ../antiquote_setup.ML \
+ Thy/HOLCF_Specific.thy
@$(USEDIR) -s IsarRef -f ROOT-HOLCF.ML HOLCF Thy
ZF-IsarRef: $(LOG)/ZF-IsarRef.gz
-$(LOG)/ZF-IsarRef.gz: Thy/ROOT-ZF.ML ../antiquote_setup.ML Thy/ZF_Specific.thy
+$(LOG)/ZF-IsarRef.gz: Thy/ROOT-ZF.ML ../antiquote_setup.ML \
+ Thy/ZF_Specific.thy
@$(USEDIR) -s IsarRef -f ROOT-ZF.ML ZF Thy
--- a/doc-src/IsarRef/Makefile Mon Jun 02 13:21:06 2008 +0200
+++ b/doc-src/IsarRef/Makefile Mon Jun 02 21:01:42 2008 +0200
@@ -17,7 +17,7 @@
Thy/document/HOLCF_Specific.tex Thy/document/HOL_Specific.tex \
Thy/document/ML_Tactic.tex Thy/document/Proof.tex \
Thy/document/Quick_Reference.tex Thy/document/Spec.tex \
- Thy/document/ZF_Specific.tex Thy/document/intro.tex \
+ Thy/document/ZF_Specific.tex Thy/document/Introduction.tex \
Thy/document/pure.tex Thy/document/syntax.tex ../isar.sty \
../rail.sty ../railsetup.sty ../proof.sty ../iman.sty ../extra.sty \
../ttbox.sty ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/Introduction.thy Mon Jun 02 21:01:42 2008 +0200
@@ -0,0 +1,304 @@
+(* $Id$ *)
+
+theory Introduction
+imports Pure
+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 @{verbatim
+ isabelle} binary provides option @{verbatim "-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: % FIXME update
+\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 @{command
+ "undo"}. See the Isabelle/Isar Quick Reference
+ (\appref{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.\
+ @{verbatim "$ISABELLE_HOME/contrib/ProofGeneral"}). Thus the
+ capital @{verbatim Isabelle} executable would already refer to the
+ @{verbatim "ProofGeneral/isar"} interface without further ado. The
+ Isabelle interface script provides several options; pass @{verbatim
+ "-?"} 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 ``@{verbatim "C-c C-return"}''
+ and ``@{verbatim "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 @{verbatim
+ "$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 @{verbatim 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 @{verbatim "~/.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 @{verbatim "-u false"} option helps to get the interface
+ process up and running. Note that additional Lisp customization
+ code may reside in @{verbatim "proofgeneral-settings.el"} of
+ @{verbatim "$ISABELLE_HOME/etc"} or @{verbatim
+ "$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 @{verbatim "-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, @{text "\<Longrightarrow>"} would appear as @{verbatim "\<Longrightarrow>"} according
+ the default set of Isabelle symbols. Nevertheless, the Isabelle
+ document preparation system (see \secref{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
+ @{command "theorem"} or @{command "lemma"} at the theory level, and
+ left again with the final conclusion (e.g.\ via @{command "qed"}).
+ A few theory specification mechanisms also require some proof, such
+ as HOL's @{command "typedef"} which demands non-emptiness of the
+ representing sets.
+*}
+
+
+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) and bookmarks. 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 @{verbatim mkdir} and @{verbatim make}
+ tools. First invoke
+\begin{ttbox}
+ isatool mkdir Foo
+\end{ttbox}
+ to initialize a separate directory for session @{verbatim Foo} ---
+ it is safe to experiment, since @{verbatim "isatool mkdir"} never
+ overwrites existing files. Ensure that @{verbatim "Foo/ROOT.ML"}
+ holds ML commands to load all theories required for this session;
+ furthermore @{verbatim "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 @{verbatim IsaMakefile}
+ (with crude source dependencies by default). This file is located
+ one level up from the @{verbatim Foo} directory location. Now
+ invoke
+\begin{ttbox}
+ isatool make Foo
+\end{ttbox}
+ to run the @{verbatim 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
+ @{verbatim ISABELLE_BROWSER_INFO}, as reported by the batch job in
+ verbose mode.
+
+ \medskip You may also consider to tune the @{verbatim usedir}
+ options in @{verbatim IsaMakefile}, for example to change the output
+ format from @{verbatim pdf} to @{verbatim dvi}, or activate the
+ @{verbatim "-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. Especially note that \appref{ap:refcard} provides a quick
+ reference card of the most common Isabelle/Isar language elements.
+
+ 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/Thy/ROOT.ML Mon Jun 02 13:21:06 2008 +0200
+++ b/doc-src/IsarRef/Thy/ROOT.ML Mon Jun 02 21:01:42 2008 +0200
@@ -4,7 +4,7 @@
set ThyOutput.source;
use "../../antiquote_setup.ML";
-use_thy "intro";
+use_thy "Introduction";
use_thy "syntax";
use_thy "Spec";
use_thy "Proof";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/document/Introduction.tex Mon Jun 02 21:01:42 2008 +0200
@@ -0,0 +1,354 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Introduction}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Introduction\isanewline
+\isakeyword{imports}\ Pure\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 \verb|isabelle| binary provides option \verb|-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: % FIXME update
+\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 \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}. See the Isabelle/Isar Quick Reference
+ (\appref{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.\
+ \verb|$ISABELLE_HOME/contrib/ProofGeneral|). Thus the
+ capital \verb|Isabelle| executable would already refer to the
+ \verb|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 ``\verb|C-c C-return|''
+ and ``\verb|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 \verb|$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 \verb|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 \verb|-u false| option helps to get the interface
+ process up and running. Note that additional Lisp customization
+ code may reside in \verb|proofgeneral-settings.el| of
+ \verb|$ISABELLE_HOME/etc| or \verb|$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 \verb|-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, \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} would appear as \verb|\<Longrightarrow>| according
+ the default set of Isabelle symbols. Nevertheless, the Isabelle
+ document preparation system (see \secref{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
+ \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}} or \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} at the theory level, and
+ left again with the final conclusion (e.g.\ via \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}).
+ A few theory specification mechanisms also require some proof, such
+ as HOL's \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} which demands non-emptiness of the
+ representing sets.%
+\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) and bookmarks. 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 \verb|mkdir| and \verb|make|
+ tools. First invoke
+\begin{ttbox}
+ isatool mkdir Foo
+\end{ttbox}
+ to initialize a separate directory for session \verb|Foo| ---
+ it is safe to experiment, since \verb|isatool mkdir| never
+ overwrites existing files. Ensure that \verb|Foo/ROOT.ML|
+ holds ML commands to load all theories required for this session;
+ furthermore \verb|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 \verb|IsaMakefile|
+ (with crude source dependencies by default). This file is located
+ one level up from the \verb|Foo| directory location. Now
+ invoke
+\begin{ttbox}
+ isatool make Foo
+\end{ttbox}
+ to run the \verb|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
+ \verb|ISABELLE_BROWSER_INFO|, as reported by the batch job in
+ verbose mode.
+
+ \medskip You may also consider to tune the \verb|usedir|
+ options in \verb|IsaMakefile|, for example to change the output
+ format from \verb|pdf| to \verb|dvi|, or activate the
+ \verb|-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. Especially note that \appref{ap:refcard} provides a quick
+ reference card of the most common Isabelle/Isar language elements.
+
+ 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/intro.tex Mon Jun 02 13:21:06 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,354 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{intro}%
-%
-\isadelimtheory
-\isanewline
-\isanewline
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ intro\isanewline
-\isakeyword{imports}\ Pure\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 \verb|isabelle| binary provides option \verb|-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: % FIXME update
-\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 \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}. See the Isabelle/Isar Quick Reference
- (\appref{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.\
- \verb|$ISABELLE_HOME/contrib/ProofGeneral|). Thus the
- capital \verb|Isabelle| executable would already refer to the
- \verb|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 ``\verb|C-c C-return|''
- and ``\verb|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 \verb|$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 \verb|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 \verb|-u false| option helps to get the interface
- process up and running. Note that additional Lisp customization
- code may reside in \verb|proofgeneral-settings.el| of
- \verb|$ISABELLE_HOME/etc| or \verb|$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 \verb|-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, \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} would appear as \verb|\<Longrightarrow>| according
- the default set of Isabelle symbols. Nevertheless, the Isabelle
- document preparation system (see \secref{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
- \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}} or \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} at the theory level, and
- left again with the final conclusion (e.g.\ via \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}).
- A few theory specification mechanisms also require some proof, such
- as HOL's \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} which demands non-emptiness of the
- representing sets.%
-\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) and bookmarks. 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 \verb|mkdir| and \verb|make|
- tools. First invoke
-\begin{ttbox}
- isatool mkdir Foo
-\end{ttbox}
- to initialize a separate directory for session \verb|Foo| ---
- it is safe to experiment, since \verb|isatool mkdir| never
- overwrites existing files. Ensure that \verb|Foo/ROOT.ML|
- holds ML commands to load all theories required for this session;
- furthermore \verb|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 \verb|IsaMakefile|
- (with crude source dependencies by default). This file is located
- one level up from the \verb|Foo| directory location. Now
- invoke
-\begin{ttbox}
- isatool make Foo
-\end{ttbox}
- to run the \verb|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
- \verb|ISABELLE_BROWSER_INFO|, as reported by the batch job in
- verbose mode.
-
- \medskip You may also consider to tune the \verb|usedir|
- options in \verb|IsaMakefile|, for example to change the output
- format from \verb|pdf| to \verb|dvi|, or activate the
- \verb|-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. Especially note that \appref{ap:refcard} provides a quick
- reference card of the most common Isabelle/Isar language elements.
-
- 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/intro.thy Mon Jun 02 13:21:06 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,304 +0,0 @@
-(* $Id$ *)
-
-theory intro
-imports Pure
-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 @{verbatim
- isabelle} binary provides option @{verbatim "-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: % FIXME update
-\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 @{command
- "undo"}. See the Isabelle/Isar Quick Reference
- (\appref{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.\
- @{verbatim "$ISABELLE_HOME/contrib/ProofGeneral"}). Thus the
- capital @{verbatim Isabelle} executable would already refer to the
- @{verbatim "ProofGeneral/isar"} interface without further ado. The
- Isabelle interface script provides several options; pass @{verbatim
- "-?"} 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 ``@{verbatim "C-c C-return"}''
- and ``@{verbatim "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 @{verbatim
- "$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 @{verbatim 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 @{verbatim "~/.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 @{verbatim "-u false"} option helps to get the interface
- process up and running. Note that additional Lisp customization
- code may reside in @{verbatim "proofgeneral-settings.el"} of
- @{verbatim "$ISABELLE_HOME/etc"} or @{verbatim
- "$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 @{verbatim "-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, @{text "\<Longrightarrow>"} would appear as @{verbatim "\<Longrightarrow>"} according
- the default set of Isabelle symbols. Nevertheless, the Isabelle
- document preparation system (see \secref{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
- @{command "theorem"} or @{command "lemma"} at the theory level, and
- left again with the final conclusion (e.g.\ via @{command "qed"}).
- A few theory specification mechanisms also require some proof, such
- as HOL's @{command "typedef"} which demands non-emptiness of the
- representing sets.
-*}
-
-
-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) and bookmarks. 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 @{verbatim mkdir} and @{verbatim make}
- tools. First invoke
-\begin{ttbox}
- isatool mkdir Foo
-\end{ttbox}
- to initialize a separate directory for session @{verbatim Foo} ---
- it is safe to experiment, since @{verbatim "isatool mkdir"} never
- overwrites existing files. Ensure that @{verbatim "Foo/ROOT.ML"}
- holds ML commands to load all theories required for this session;
- furthermore @{verbatim "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 @{verbatim IsaMakefile}
- (with crude source dependencies by default). This file is located
- one level up from the @{verbatim Foo} directory location. Now
- invoke
-\begin{ttbox}
- isatool make Foo
-\end{ttbox}
- to run the @{verbatim 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
- @{verbatim ISABELLE_BROWSER_INFO}, as reported by the batch job in
- verbose mode.
-
- \medskip You may also consider to tune the @{verbatim usedir}
- options in @{verbatim IsaMakefile}, for example to change the output
- format from @{verbatim pdf} to @{verbatim dvi}, or activate the
- @{verbatim "-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. Especially note that \appref{ap:refcard} provides a quick
- reference card of the most common Isabelle/Isar language elements.
-
- 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/isar-ref.tex Mon Jun 02 13:21:06 2008 +0200
+++ b/doc-src/IsarRef/isar-ref.tex Mon Jun 02 21:01:42 2008 +0200
@@ -73,7 +73,7 @@
\pagenumbering{roman} \tableofcontents \clearfirst
-\input{Thy/document/intro.tex}
+\input{Thy/document/Introduction.tex}
\input{basics.tex}
\input{Thy/document/syntax.tex}
\input{Thy/document/Spec.tex}