# HG changeset patch # User wenzelm # Date 1208945588 -7200 # Node ID eb15fd4cd1ad3f253d3c11a88798c6fe1375f90c # Parent 6c8cd101f8753186844a698fc9b36c104bb5c229 converted intro.tex to Thy/intro.thy; diff -r 6c8cd101f875 -r eb15fd4cd1ad doc-src/IsarRef/IsaMakefile --- 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 diff -r 6c8cd101f875 -r eb15fd4cd1ad doc-src/IsarRef/Makefile --- 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 diff -r 6c8cd101f875 -r eb15fd4cd1ad doc-src/IsarRef/Thy/ROOT.ML --- 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"; diff -r 6c8cd101f875 -r eb15fd4cd1ad doc-src/IsarRef/Thy/document/intro.tex --- /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,\, 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: diff -r 6c8cd101f875 -r eb15fd4cd1ad doc-src/IsarRef/Thy/document/session.tex --- 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" diff -r 6c8cd101f875 -r eb15fd4cd1ad doc-src/IsarRef/Thy/intro.thy --- /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,\, 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 diff -r 6c8cd101f875 -r eb15fd4cd1ad doc-src/IsarRef/intro.tex --- 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,\, 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: diff -r 6c8cd101f875 -r eb15fd4cd1ad doc-src/IsarRef/isar-ref.tex --- 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