# HG changeset patch # User wenzelm # Date 1212433302 -7200 # Node ID d038a2ba87f64b4a4168daab01b341474f246d5f # Parent 5257bc7e0c068b0bcb9ad1d7972f85f369cc0a95 renamed theory "intro" to "Introduction"; diff -r 5257bc7e0c06 -r d038a2ba87f6 doc-src/IsarRef/IsaMakefile --- 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 diff -r 5257bc7e0c06 -r d038a2ba87f6 doc-src/IsarRef/Makefile --- 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 \ diff -r 5257bc7e0c06 -r d038a2ba87f6 doc-src/IsarRef/Thy/Introduction.thy --- /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 "\"} would appear as @{verbatim "\"} 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 diff -r 5257bc7e0c06 -r d038a2ba87f6 doc-src/IsarRef/Thy/ROOT.ML --- 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"; diff -r 5257bc7e0c06 -r d038a2ba87f6 doc-src/IsarRef/Thy/document/Introduction.tex --- /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|\| 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: diff -r 5257bc7e0c06 -r d038a2ba87f6 doc-src/IsarRef/Thy/document/intro.tex --- 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|\| 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: diff -r 5257bc7e0c06 -r d038a2ba87f6 doc-src/IsarRef/Thy/intro.thy --- 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 "\"} would appear as @{verbatim "\"} 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 diff -r 5257bc7e0c06 -r d038a2ba87f6 doc-src/IsarRef/isar-ref.tex --- 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}