1.1 --- a/doc-src/IsarRef/generic.tex Tue Feb 12 20:32:23 2002 +0100
1.2 +++ b/doc-src/IsarRef/generic.tex Tue Feb 12 20:33:03 2002 +0100
1.3 @@ -25,9 +25,9 @@
1.4 Isabelle documentation.
1.5
1.6 \begin{rail}
1.7 - 'axclass' classdecl (axmdecl prop comment? +)
1.8 + 'axclass' classdecl (axmdecl prop +)
1.9 ;
1.10 - 'instance' (nameref ('<' | subseteq) nameref | nameref '::' simplearity) comment?
1.11 + 'instance' (nameref ('<' | subseteq) nameref | nameref '::' simplearity)
1.12 ;
1.13 \end{rail}
1.14
1.15 @@ -79,7 +79,7 @@
1.16 corresponding parameters do \emph{not} occur in the conclusion.
1.17
1.18 \begin{rail}
1.19 - 'obtain' (vars + 'and') comment? \\ 'where' (props comment? + 'and')
1.20 + 'obtain' (vars + 'and') 'where' (props + 'and')
1.21 ;
1.22 \end{rail}
1.23
1.24 @@ -163,14 +163,12 @@
1.25 \end{matharray}
1.26
1.27 \begin{rail}
1.28 - ('also' | 'finally') transrules? comment?
1.29 - ;
1.30 - ('moreover' | 'ultimately') comment?
1.31 + ('also' | 'finally') transrules?
1.32 ;
1.33 'trans' (() | 'add' | 'del')
1.34 ;
1.35
1.36 - transrules: '(' thmrefs ')' interest?
1.37 + transrules: '(' thmrefs ')'
1.38 ;
1.39 \end{rail}
1.40
1.41 @@ -193,9 +191,9 @@
1.42
1.43 \item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$,
1.44 but collect results only, without applying rules.
1.45 -
1.46 -\item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity
1.47 - rules declared in the current context.
1.48 +
1.49 +\item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity (and
1.50 + symmetry) rules declared in the current context.
1.51
1.52 \item [$trans$] declares theorems as transitivity rules.
1.53
2.1 --- a/doc-src/IsarRef/intro.tex Tue Feb 12 20:32:23 2002 +0100
2.2 +++ b/doc-src/IsarRef/intro.tex Tue Feb 12 20:33:03 2002 +0100
2.3 @@ -7,7 +7,7 @@
2.4 building deductive systems (programmed in Standard ML), with a special focus
2.5 on interactive theorem proving in higher-order logics. In the olden days even
2.6 end-users would refer to certain ML functions (goal commands, tactics,
2.7 -tacticals etc.) to pursue their everyday theorem proving needs
2.8 +tacticals etc.) to pursue their everyday theorem proving tasks
2.9 \cite{isabelle-intro,isabelle-ref}.
2.10
2.11 In contrast \emph{Isar} provides an interpreted language environment of its
2.12 @@ -21,8 +21,8 @@
2.13
2.14 \medskip Apart from these technical advances over bare-bones ML programming,
2.15 the main intention of Isar is to provide a conceptually different view on
2.16 -machine-checked proofs \cite{Wenzel:1999:TPHOL, Wenzel-PhD} --- ``Isar''
2.17 -stands for ``Intelligible semi-automated reasoning''. Drawing from both the
2.18 +machine-checked proofs \cite{Wenzel:1999:TPHOL,Wenzel-PhD} --- ``Isar'' stands
2.19 +for ``Intelligible semi-automated reasoning''. Drawing from both the
2.20 traditions of informal mathematical proof texts and high-level programming
2.21 languages, Isar provides a versatile environment for structured formal proof
2.22 documents. Thus properly written Isar proof texts become accessible to a
2.23 @@ -34,33 +34,32 @@
2.24 own right, independently of the mechanic proof-checking process.
2.25
2.26 Despite its grand design of structured proof texts, Isar is able to assimilate
2.27 -the old-style tactical as an ``improper'' sub-language. This provides an easy
2.28 +the old tactical style as an ``improper'' sub-language. This provides an easy
2.29 upgrade path for existing tactic scripts, as well as additional means for
2.30 -experimentation and debugging of interactive proofs. Isabelle/Isar freely
2.31 -supports a broad range of proof styles, including unreadable ones.
2.32 +interactive experimentation and debugging of structured proofs. Isabelle/Isar
2.33 +supports a broad range of proof styles, both readable and unreadable ones.
2.34
2.35 -\medskip The Isabelle/Isar framework generic and should work for reasonably
2.36 -well for any object-logic that directly conforms to the view of natural
2.37 -deduction according to the Isabelle/Pure framework. Major Isabelle logics
2.38 -(HOL \cite{isabelle-HOL}, HOLCF, FOL \cite{isabelle-logics}, ZF
2.39 -\cite{isabelle-ZF}) have already been setup for immediate use by end-users.
2.40 -
2.41 -Note that much of the existing body of theories still consist of old-style
2.42 -theory files with accompanied ML code for proof scripts. This legacy will be
2.43 -converted as time goes by.
2.44 +\medskip The Isabelle/Isar framework is generic and should work reasonably
2.45 +well for any Isabelle object-logic that conforms to the natural deduction view
2.46 +of the Isabelle/Pure framework. Major Isabelle logics like HOL
2.47 +\cite{isabelle-HOL}, HOLCF \cite{MuellerNvOS99}, FOL \cite{isabelle-logics},
2.48 +and ZF \cite{isabelle-ZF} have already been set up for end-users.
2.49 +Nonetheless, much of the existing body of theories still consist of old-style
2.50 +theory files with accompanied ML code for proof scripts; this legacy will be
2.51 +gradually converted in due time.
2.52
2.53
2.54 \section{Quick start}
2.55
2.56 \subsection{Terminal sessions}
2.57
2.58 -Isar is already part of Isabelle (as of version Isabelle99, or later). The
2.59 -\texttt{isabelle} binary provides option \texttt{-I} to run the Isabelle/Isar
2.60 -interaction loop at startup, rather than the raw ML top-level. So the
2.61 -quickest way to do anything with Isabelle/Isar is as follows:
2.62 +Isar is already part of Isabelle. The low-level \texttt{isabelle} binary
2.63 +provides option \texttt{-I} to run the Isabelle/Isar interaction loop at
2.64 +startup, rather than the raw ML top-level. So the most basic way to do
2.65 +anything with Isabelle/Isar is as follows:
2.66 \begin{ttbox}
2.67 isabelle -I HOL\medskip
2.68 -\out{> Welcome to Isabelle/HOL (Isabelle99-1)}\medskip
2.69 +\out{> Welcome to Isabelle/HOL (Isabelle2002)}\medskip
2.70 theory Foo = Main:
2.71 constdefs foo :: nat "foo == 1";
2.72 lemma "0 < foo" by (simp add: foo_def);
2.73 @@ -75,38 +74,37 @@
2.74
2.75 Plain TTY-based interaction as above used to be quite feasible with
2.76 traditional tactic based theorem proving, but developing Isar documents really
2.77 -demands some better user-interface support. David Aspinall's
2.78 -\emph{Proof~General}\index{Proof General} environment
2.79 -\cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs interface for
2.80 -interactive theorem provers that does all the cut-and-paste and
2.81 -forward-backward walk through the text in a very neat way. In Isabelle/Isar,
2.82 -the current position within a partial proof document is equally important than
2.83 -the actual proof state. Thus Proof~General provides the canonical working
2.84 -environment for Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
2.85 -existing Isar documents) and for production work.
2.86 +demands some better user-interface support. The Proof~General environment by
2.87 +David Aspinall \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
2.88 +interface for interactive theorem provers that organizes all the cut-and-paste
2.89 +and forward-backward walk through the text in a very neat way. In
2.90 +Isabelle/Isar, the current position within a partial proof document is equally
2.91 +important than the actual proof state. Thus Proof~General provides the
2.92 +canonical working environment for Isabelle/Isar, both for getting acquainted
2.93 +(e.g.\ by replaying existing Isar documents) and for production work.
2.94
2.95
2.96 \subsubsection{Proof~General as default Isabelle interface}
2.97
2.98 -The easiest way to invoke Proof~General is via the Isabelle interface wrapper
2.99 -script. The default configuration of Isabelle is smart enough to detect the
2.100 -Proof~General distribution in several canonical places (e.g.\
2.101 -\texttt{\$ISABELLE_HOME/contrib/ProofGeneral}). Thus the capital
2.102 -\texttt{Isabelle} executable would already refer to the
2.103 +The Isabelle interface wrapper script provides an easy way to invoke
2.104 +Proof~General (and XEmacs or GNU Emacs). The default configuration of
2.105 +Isabelle is smart enough to detect the Proof~General distribution in several
2.106 +canonical places (e.g.\ \texttt{\$ISABELLE_HOME/contrib/ProofGeneral}). Thus
2.107 +the capital \texttt{Isabelle} executable would already refer to the
2.108 \texttt{ProofGeneral/isar} interface without further ado.\footnote{There is
2.109 also a \texttt{ProofGeneral/isa} interface for old tactic scripts written in
2.110 - ML.} The Isabelle interface script provides several options, just pass
2.111 -\verb,-?, to see its usage.
2.112 + ML.} The Isabelle interface script provides several options; pass \verb,-?,
2.113 +to see its usage.
2.114
2.115 With the proper Isabelle interface setup, Isar documents may now be edited by
2.116 visiting appropriate theory files, e.g.\
2.117 \begin{ttbox}
2.118 -Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/BasicLogic.thy
2.119 +Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
2.120 \end{ttbox}
2.121 -Users of XEmacs may note the tool bar for navigating forward and backward
2.122 -through the text. Consult the Proof~General documentation \cite{proofgeneral}
2.123 -for further basic command sequences, such as ``\texttt{C-c C-return}'' or
2.124 -``\texttt{C-c u}''.
2.125 +Users may note the tool bar for navigating forward and backward through the
2.126 +text (this depends on the local Emacs installation). Consult the
2.127 +Proof~General documentation \cite{proofgeneral} for further basic command
2.128 +sequences, in particular ``\texttt{C-c C-return}'' and ``\texttt{C-c u}''.
2.129
2.130 \medskip
2.131
2.132 @@ -122,27 +120,27 @@
2.133 \medskip
2.134
2.135 Apart from the Isabelle command line, defaults for interface options may be
2.136 -given by the \texttt{PROOFGENERAL_OPTIONS} setting as well. For example, the
2.137 -Emacs executable to be used may be configured in Isabelle's settings like this:
2.138 +given by the \texttt{PROOFGENERAL_OPTIONS} setting. For example, the Emacs
2.139 +executable to be used may be configured in Isabelle's settings like this:
2.140 \begin{ttbox}
2.141 PROOFGENERAL_OPTIONS="-p xemacs-nomule"
2.142 \end{ttbox}
2.143
2.144 -Occasionally, the user's \verb,~/.emacs, file contains material that is
2.145 -incompatible with the version of Emacs that Proof~General prefers. Then
2.146 -proper startup may be still achieved by using the \texttt{-u false} option.
2.147 -Also note that any Emacs lisp file called \texttt{proofgeneral-settings.el}
2.148 -occurring in \texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc}
2.149 -is automatically loaded by the Proof~General interface script as well.
2.150 +Occasionally, a user's \verb,~/.emacs, file contains code that is incompatible
2.151 +with the (X)Emacs version used by Proof~General, causing the interface startup
2.152 +to fail prematurely. Here the \texttt{-u false} option helps to get the
2.153 +interface process up and running. Note that additional Lisp customization
2.154 +code may reside in \texttt{proofgeneral-settings.el} of
2.155 +\texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc}.
2.156
2.157
2.158 \subsubsection{The X-Symbol package}
2.159
2.160 -Proof~General also supports the Emacs X-Symbol package \cite{x-symbol}, which
2.161 -provides a nice way to get proper mathematical symbols displayed on screen.
2.162 -Just pass option \texttt{-x true} to the Isabelle interface script, or check
2.163 -the appropriate menu setting by hand. In any case, the X-Symbol package must
2.164 -have been properly installed already.
2.165 +Proof~General provides native support for the Emacs X-Symbol package
2.166 +\cite{x-symbol}, which handles proper mathematical symbols displayed on
2.167 +screen. Pass option \texttt{-x true} to the Isabelle interface script, or
2.168 +check the appropriate Proof~General menu setting by hand. In any case, the
2.169 +X-Symbol package must have been properly installed already.
2.170
2.171 Contrary to what you may expect from the documentation of X-Symbol, the
2.172 package is very easy to install and configures itself automatically. The
2.173 @@ -159,7 +157,7 @@
2.174 symbols. Nevertheless, the Isabelle document preparation system (see
2.175 \S\ref{sec:document-prep}) will be happy to print non-ASCII symbols properly.
2.176 It is even possible to invent additional notation beyond the display
2.177 -capabilities of XEmacs and X-Symbol.
2.178 +capabilities of Emacs and X-Symbol.
2.179
2.180
2.181 \section{Isabelle/Isar theories}
2.182 @@ -181,9 +179,9 @@
2.183 The Isar proof language is embedded into the new theory format as a proper
2.184 sub-language. Proof mode is entered by stating some $\THEOREMNAME$ or
2.185 $\LEMMANAME$ at the theory level, and left again with the final conclusion
2.186 -(e.g.\ via $\QEDNAME$). A few theory extension mechanisms require proof as
2.187 -well, such as HOL's $\isarkeyword{typedef}$ which demands non-emptiness of the
2.188 -representing sets.
2.189 +(e.g.\ via $\QEDNAME$). A few theory specification mechanisms also require
2.190 +some proof, such as HOL's $\isarkeyword{typedef}$ which demands non-emptiness
2.191 +of the representing sets.
2.192
2.193 New-style theory files may still be associated with separate ML files
2.194 consisting of plain old tactic scripts. There is no longer any ML binding
2.195 @@ -195,138 +193,133 @@
2.196 Isar proof language at all.
2.197
2.198 \begin{warn}
2.199 - Currently, Proof~General does \emph{not} support mixed interactive
2.200 - development of classic Isabelle theory files or tactic scripts, together
2.201 - with Isar documents. The ``\texttt{isa}'' and ``\texttt{isar}'' versions of
2.202 + Proof~General does \emph{not} support mixed interactive development of
2.203 + classic Isabelle theory files or tactic scripts, together with Isar
2.204 + documents. The ``\texttt{isa}'' and ``\texttt{isar}'' versions of
2.205 Proof~General are handled as two different theorem proving systems, only one
2.206 of these may be active at the same time.
2.207 \end{warn}
2.208
2.209 -Conversion of existing tactic scripts is best done by running two separate
2.210 -Proof~General sessions, one for replaying the old script and the other for the
2.211 -emerging Isabelle/Isar document. Also note that Isar supports emulation
2.212 -commands and methods that support traditional tactic scripts within new-style
2.213 -theories, see appendix~\ref{ap:conv} for more information.
2.214 +Manual conversion of existing tactic scripts may be done by running two
2.215 +separate Proof~General sessions, one for replaying the old script and the
2.216 +other for the emerging Isabelle/Isar document. Also note that Isar supports
2.217 +emulation commands and methods that support traditional tactic scripts within
2.218 +new-style theories, see appendix~\ref{ap:conv} for more information.
2.219
2.220
2.221 \subsection{Document preparation}\label{sec:document-prep}
2.222
2.223 -Isabelle/Isar provides a simple document preparation system based on current
2.224 -(PDF) {\LaTeX} technology, with full support of hyper-links (both local
2.225 -references and URLs), bookmarks, thumbnails etc. Thus the results are equally
2.226 -well suited for WWW browsing and as printed copies.
2.227 +Isabelle/Isar provides a simple document preparation system based on existing
2.228 +PDF-\LaTeX technology, with full support of hyper-links (both local references
2.229 +and URLs), bookmarks, and thumbnails. Thus the results are equally well
2.230 +suited for WWW browsing and as printed copies.
2.231
2.232 \medskip
2.233
2.234 Isabelle generates {\LaTeX} output as part of the run of a \emph{logic
2.235 session} (see also \cite{isabelle-sys}). Getting started with a working
2.236 configuration for common situations is quite easy by using the Isabelle
2.237 -\texttt{mkdir} and \texttt{make} tools. Just invoke
2.238 +\texttt{mkdir} and \texttt{make} tools. First invoke
2.239 \begin{ttbox}
2.240 - isatool mkdir -d Foo
2.241 + isatool mkdir Foo
2.242 \end{ttbox}
2.243 -to setup a separate directory for session \texttt{Foo}.\footnote{It is safe to
2.244 - experiment, since \texttt{isatool mkdir} never overwrites existing files.}
2.245 -Ensure that \texttt{Foo/ROOT.ML} loads all theories required for this session.
2.246 -Furthermore \texttt{Foo/document/root.tex} should include any special {\LaTeX}
2.247 -macro packages required for your document (the default is usually sufficient
2.248 -as a start).
2.249 +to initialize a separate directory for session \texttt{Foo} --- it is safe to
2.250 +experiment, since \texttt{isatool mkdir} never overwrites existing files.
2.251 +Ensure that \texttt{Foo/ROOT.ML} holds ML commands to load all theories
2.252 +required for this session; furthermore \texttt{Foo/document/root.tex} should
2.253 +include any special {\LaTeX} macro packages required for your document (the
2.254 +default is usually sufficient as a start).
2.255
2.256 -The session is controlled by a separate \texttt{IsaMakefile} (with very crude
2.257 -source dependencies only by default). This file is located one level up from
2.258 -the \texttt{Foo} directory location. At that point just invoke
2.259 +The session is controlled by a separate \texttt{IsaMakefile} (with crude
2.260 +source dependencies by default). This file is located one level up from the
2.261 +\texttt{Foo} directory location. Now invoke
2.262 \begin{ttbox}
2.263 isatool make Foo
2.264 \end{ttbox}
2.265 to run the \texttt{Foo} session, with browser information and document
2.266 preparation enabled. Unless any errors are reported by Isabelle or {\LaTeX},
2.267 -the output will appear inside the directory indicated by \texttt{isatool
2.268 - getenv ISABELLE_BROWSER_INFO}, with the logical session prefix added (e.g.\
2.269 -\texttt{HOL/Foo}). Note that the \texttt{index.html} located there provides a
2.270 -link to the finished {\LaTeX} document, too.
2.271 -
2.272 -Note that this really is batch processing --- better let Isabelle check your
2.273 -theory and proof developments beforehand in interactive mode.
2.274 +the output will appear inside the directory \texttt{ISABELLE_BROWSER_INFO}, as
2.275 +reported by the batch job in verbose mode.
2.276
2.277 \medskip
2.278
2.279 You may also consider to tune the \texttt{usedir} options in
2.280 \texttt{IsaMakefile}, for example to change the output format from
2.281 -\texttt{dvi} to \texttt{pdf}, or activate the \texttt{-D document} option in
2.282 -order to preserve a copy of the generated {\LaTeX} sources. The latter
2.283 -feature is very useful for debugging {\LaTeX} errors, while avoiding repeated
2.284 -runs of Isabelle.
2.285 +\texttt{pdf} to \texttt{dvi}, or activate the \texttt{-D generated} option in
2.286 +order to keep a second copy of the generated {\LaTeX} sources.
2.287
2.288 \medskip
2.289
2.290 See \emph{The Isabelle System Manual} \cite{isabelle-sys} for further details
2.291 -on Isabelle logic sessions and theory presentation.
2.292 +on Isabelle logic sessions and theory presentation. The Isabelle/HOL tutorial
2.293 +\cite{isabelle-hol-book} also covers theory presentation issues.
2.294
2.295
2.296 \subsection{How to write Isar proofs anyway?}\label{sec:isar-howto}
2.297
2.298 -%FIXME tune
2.299 +This is one of the key questions, of course. First of all, the tactic script
2.300 +emulation of Isabelle/Isar essentially provides a clarified version of the
2.301 +very same unstructured proof style of classic Isabelle. Old-time users should
2.302 +quickly become acquainted with that (degenerative) view of Isar at the least.
2.303
2.304 -This is one of the key questions, of course. Isar offers a rather different
2.305 -approach to formal proof documents than plain old tactic scripts. Experienced
2.306 -users of existing interactive theorem proving systems may have to learn
2.307 -thinking differently in order to make effective use of Isabelle/Isar. On the
2.308 -other hand, Isabelle/Isar comes much closer to existing mathematical practice
2.309 -of formal proof, so users with less experience in old-style tactical proving,
2.310 -but a good understanding of mathematical proof, might cope with Isar even
2.311 -better. See also \cite{Wenzel:1999:TPHOL,Bauer-Wenzel:2000:HB} for further
2.312 -background information on Isar.
2.313 +Writing \emph{proper} Isar proof texts targeted at human readers is quite
2.314 +different, though. Experienced users of the unstructured style may even have
2.315 +to unlearn some of their habits to master proof composition in Isar. In
2.316 +contrast, new users with less experience in old-style tactical proving, but a
2.317 +good understanding of mathematical proof in general often get started easier.
2.318
2.319 -\medskip This really is a reference manual on Isabelle/Isar, not a tutorial.
2.320 -Nevertheless, we will also give some clues of how the concepts introduced here
2.321 -may be put into practice. Appendix~\ref{ap:refcard} provides a quick
2.322 -reference card of the most common Isabelle/Isar language elements.
2.323 -Appendix~\ref{ap:conv} offers some practical hints on converting existing
2.324 -Isabelle theories and proof scripts to the new format.
2.325 +\medskip The present text really is only a reference manual on Isabelle/Isar,
2.326 +not a tutorial. Nevertheless, we will attempt to give some clues of how the
2.327 +concepts introduced here may be put into practice. Appendix~\ref{ap:refcard}
2.328 +provides a quick reference card of the most common Isabelle/Isar language
2.329 +elements. Appendix~\ref{ap:conv} offers some practical hints on converting
2.330 +existing Isabelle theories and proof scripts to the new format (without
2.331 +restructuring proofs).
2.332
2.333 -Several example applications are distributed with Isabelle, and available via
2.334 -the Isabelle WWW library as well as the Isabelle/Isar page:
2.335 -\begin{center}\small
2.336 - \begin{tabular}{l}
2.337 - \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
2.338 - \url{http://isabelle.in.tum.de/library/} \\[1ex]
2.339 - \url{http://isabelle.in.tum.de/Isar/} \\
2.340 - \end{tabular}
2.341 -\end{center}
2.342 +Further issues concerning the Isar concepts are covered in the literature
2.343 +\cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
2.344 +The author's PhD thesis \cite{Wenzel-PhD} presently provides the most complete
2.345 +exposition of Isar foundations, techniques, and applications. A number of
2.346 +example applications are distributed with Isabelle, and available via the
2.347 +Isabelle WWW library (e.g.\ \url{http://isabelle.in.tum.de/library/}). As a
2.348 +general rule of thumb, more recent Isabelle applications that also include a
2.349 +separate ``document'' (in PDF) are more likely to consist of proper
2.350 +Isabelle/Isar theories and proofs.
2.351
2.352 -The following examples may be of particular interest. Apart from the plain
2.353 -sources represented in HTML, these Isabelle sessions also provide actual
2.354 -documents (in PDF).
2.355 -\begin{itemize}
2.356 -\item \url{http://isabelle.in.tum.de/library/HOL/Isar_examples/} is a
2.357 - collection of introductory examples.
2.358 -\item \url{http://isabelle.in.tum.de/library/HOL/Lattice/} is an example of
2.359 - typical mathematics-style reasoning in ``axiomatic'' structures.
2.360 -\item \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/HahnBanach/} is a
2.361 - big mathematics application on infinitary vector spaces and functional
2.362 - analysis.
2.363 -\item \url{http://isabelle.in.tum.de/library/HOL/Lambda/} develops fundamental
2.364 - properties of $\lambda$-calculus (Church-Rosser and termination).
2.365 +%FIXME
2.366 +% The following examples may be of particular interest. Apart from the plain
2.367 +% sources represented in HTML, these Isabelle sessions also provide actual
2.368 +% documents (in PDF).
2.369 +% \begin{itemize}
2.370 +% \item \url{http://isabelle.in.tum.de/library/HOL/Isar_examples/} is a
2.371 +% collection of introductory examples.
2.372 +% \item \url{http://isabelle.in.tum.de/library/HOL/Lattice/} is an example of
2.373 +% typical mathematics-style reasoning in ``axiomatic'' structures.
2.374 +% \item \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/HahnBanach/} is a
2.375 +% big mathematics application on infinitary vector spaces and functional
2.376 +% analysis.
2.377 +% \item \url{http://isabelle.in.tum.de/library/HOL/Lambda/} develops fundamental
2.378 +% properties of $\lambda$-calculus (Church-Rosser and termination).
2.379
2.380 - This may serve as a realistic example of porting of legacy proof scripts
2.381 - into Isar tactic emulation scripts.
2.382 -\item \url{http://isabelle.in.tum.de/library/HOL/Unix/} gives a mathematical
2.383 - model of the main aspects of the Unix file-system including its security
2.384 - model, but ignoring processes. A few odd effects caused by the general
2.385 - ``worse-is-better'' approach followed in Unix are discussed within the
2.386 - formal model.
2.387 +% This may serve as a realistic example of porting of legacy proof scripts
2.388 +% into Isar tactic emulation scripts.
2.389 +% \item \url{http://isabelle.in.tum.de/library/HOL/Unix/} gives a mathematical
2.390 +% model of the main aspects of the Unix file-system including its security
2.391 +% model, but ignoring processes. A few odd effects caused by the general
2.392 +% ``worse-is-better'' approach followed in Unix are discussed within the
2.393 +% formal model.
2.394
2.395 - This example represents a non-trivial verification task, with all proofs
2.396 - carefully worked out using the proper part of the Isar proof language;
2.397 - unstructured scripts are only used for symbolic evaluation.
2.398 -\item \url{http://isabelle.in.tum.de/library/HOL/MicroJava/} is a
2.399 - formalization of a fragment of Java, together with a corresponding virtual
2.400 - machine and a specification of its bytecode verifier and a lightweight
2.401 - bytecode verifier, including proofs of type-safety.
2.402 +% This example represents a non-trivial verification task, with all proofs
2.403 +% carefully worked out using the proper part of the Isar proof language;
2.404 +% unstructured scripts are only used for symbolic evaluation.
2.405 +% \item \url{http://isabelle.in.tum.de/library/HOL/MicroJava/} is a
2.406 +% formalization of a fragment of Java, together with a corresponding virtual
2.407 +% machine and a specification of its bytecode verifier and a lightweight
2.408 +% bytecode verifier, including proofs of type-safety.
2.409
2.410 - This represents a very ``realistic'' example of large formalizations
2.411 - performed in form of tactic emulation scripts and proper Isar proof texts.
2.412 -\end{itemize}
2.413 +% This represents a very ``realistic'' example of large formalizations
2.414 +% performed in form of tactic emulation scripts and proper Isar proof texts.
2.415 +% \end{itemize}
2.416
2.417
2.418 %%% Local Variables:
3.1 --- a/doc-src/IsarRef/isar-ref.tex Tue Feb 12 20:32:23 2002 +0100
3.2 +++ b/doc-src/IsarRef/isar-ref.tex Tue Feb 12 20:33:03 2002 +0100
3.3 @@ -69,21 +69,6 @@
3.4
3.5 \pagenumbering{roman} \tableofcontents \clearfirst
3.6
3.7 -%FIXME
3.8 -\nocite{Aspinall:2000:eProof}
3.9 -\nocite{Bauer-Wenzel:2000:HB}
3.10 -\nocite{Harrison:1996:MizarHOL}
3.11 -\nocite{Muzalewski:Mizar}
3.12 -\nocite{Rudnicki:1992:MizarOverview}
3.13 -\nocite{Rudnicki:1992:MizarOverview}
3.14 -\nocite{Syme:1997:DECLARE}
3.15 -\nocite{Syme:1998:thesis}
3.16 -\nocite{Syme:1999:TPHOL}
3.17 -\nocite{Trybulec:1993:MizarFeatures}
3.18 -\nocite{Wiedijk:1999:Mizar}
3.19 -\nocite{Wiedijk:2000:MV}
3.20 -\nocite{Zammit:1999:TPHOL}
3.21 -
3.22 \include{intro}
3.23 \include{basics}
3.24 \include{syntax}
4.1 --- a/doc-src/IsarRef/logics.tex Tue Feb 12 20:32:23 2002 +0100
4.2 +++ b/doc-src/IsarRef/logics.tex Tue Feb 12 20:33:03 2002 +0100
4.3 @@ -90,9 +90,9 @@
4.4 \end{matharray}
4.5
4.6 \begin{rail}
4.7 - 'typedecl' typespec infix? comment?
4.8 + 'typedecl' typespec infix?
4.9 ;
4.10 - 'typedef' parname? typespec infix? \\ '=' term comment?
4.11 + 'typedef' parname? typespec infix? '=' term
4.12 ;
4.13 \end{rail}
4.14
4.15 @@ -186,7 +186,7 @@
4.16
4.17 dtspec: parname? typespec infix? '=' (cons + '|')
4.18 ;
4.19 - cons: name (type * ) mixfix? comment?
4.20 + cons: name (type * ) mixfix?
4.21 ;
4.22 dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
4.23 \end{rail}
4.24 @@ -236,14 +236,12 @@
4.25 \begin{rail}
4.26 'primrec' parname? (equation + )
4.27 ;
4.28 - 'recdef' ('(' 'permissive' ')')? \\ name term (eqn + ) hints?
4.29 + 'recdef' ('(' 'permissive' ')')? \\ name term (prop + ) hints?
4.30 ;
4.31 - recdeftc thmdecl? tc comment?
4.32 + recdeftc thmdecl? tc
4.33 ;
4.34
4.35 - equation: thmdecl? eqn
4.36 - ;
4.37 - eqn: prop comment?
4.38 + equation: thmdecl? prop
4.39 ;
4.40 hints: '(' 'hints' (recdefmod * ) ')'
4.41 ;
4.42 @@ -329,11 +327,11 @@
4.43 'mono' (() | 'add' | 'del')
4.44 ;
4.45
4.46 - sets: (term comment? +)
4.47 + sets: (term +)
4.48 ;
4.49 - intros: 'intros' (thmdecl? prop comment? +)
4.50 + intros: 'intros' (thmdecl? prop +)
4.51 ;
4.52 - monos: 'monos' thmrefs comment?
4.53 + monos: 'monos' thmrefs
4.54 ;
4.55 \end{rail}
4.56
4.57 @@ -404,7 +402,7 @@
4.58 ;
4.59 indcases (prop +)
4.60 ;
4.61 - inductivecases thmdecl? (prop +) comment?
4.62 + inductivecases thmdecl? (prop +)
4.63 ;
4.64
4.65 rule: ('rule' ':' thmref)
4.66 @@ -468,7 +466,7 @@
4.67
4.68 dmspec: typespec '=' (cons + '|')
4.69 ;
4.70 - cons: name (type * ) mixfix? comment?
4.71 + cons: name (type * ) mixfix?
4.72 ;
4.73 dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
4.74 \end{rail}
5.1 --- a/doc-src/IsarRef/pure.tex Tue Feb 12 20:32:23 2002 +0100
5.2 +++ b/doc-src/IsarRef/pure.tex Tue Feb 12 20:33:03 2002 +0100
5.3 @@ -5,7 +5,7 @@
5.4 commands, together with fundamental proof methods and attributes.
5.5 Chapter~\ref{ch:gen-tools} describes further Isar elements provided by generic
5.6 tools and packages (such as the Simplifier) that are either part of Pure
5.7 -Isabelle or pre-installed by most object logics. Chapter~\ref{ch:logics}
5.8 +Isabelle or pre-installed in most object logics. Chapter~\ref{ch:logics}
5.9 refers to object-logic specific elements (mainly for HOL and ZF).
5.10
5.11 \medskip
5.12 @@ -162,11 +162,11 @@
5.13 \end{matharray}
5.14
5.15 \begin{rail}
5.16 - 'classes' (classdecl comment? +)
5.17 + 'classes' (classdecl +)
5.18 ;
5.19 - 'classrel' nameref ('<' | subseteq) nameref comment?
5.20 + 'classrel' nameref ('<' | subseteq) nameref
5.21 ;
5.22 - 'defaultsort' sort comment?
5.23 + 'defaultsort' sort
5.24 ;
5.25 \end{rail}
5.26
5.27 @@ -195,13 +195,13 @@
5.28 \end{matharray}
5.29
5.30 \begin{rail}
5.31 - 'types' (typespec '=' type infix? comment? +)
5.32 + 'types' (typespec '=' type infix? +)
5.33 ;
5.34 - 'typedecl' typespec infix? comment?
5.35 + 'typedecl' typespec infix?
5.36 ;
5.37 - 'nonterminals' (name +) comment?
5.38 + 'nonterminals' (name +)
5.39 ;
5.40 - 'arities' (nameref '::' arity comment? +)
5.41 + 'arities' (nameref '::' arity +)
5.42 ;
5.43 \end{rail}
5.44
5.45 @@ -236,12 +236,12 @@
5.46 \begin{rail}
5.47 'consts' (constdecl +)
5.48 ;
5.49 - 'defs' ('(overloaded)')? (axmdecl prop comment? +)
5.50 + 'defs' ('(overloaded)')? (axmdecl prop +)
5.51 ;
5.52 - 'constdefs' (constdecl prop comment? +)
5.53 + 'constdefs' (constdecl prop +)
5.54 ;
5.55
5.56 - constdecl: name '::' type mixfix? comment?
5.57 + constdecl: name '::' type mixfix?
5.58 ;
5.59 \end{rail}
5.60
5.61 @@ -284,7 +284,7 @@
5.62 \begin{rail}
5.63 'syntax' ('(' ( name | 'output' | name 'output' ) ')')? (constdecl +)
5.64 ;
5.65 - 'translations' (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat comment? +)
5.66 + 'translations' (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
5.67 ;
5.68 transpat: ('(' nameref ')')? string
5.69 ;
5.70 @@ -317,9 +317,9 @@
5.71 \end{matharray}
5.72
5.73 \begin{rail}
5.74 - 'axioms' (axmdecl prop comment? +)
5.75 + 'axioms' (axmdecl prop +)
5.76 ;
5.77 - ('lemmas' | 'theorems') (thmdef? thmrefs comment? + 'and')
5.78 + ('lemmas' | 'theorems') (thmdef? thmrefs + 'and')
5.79 ;
5.80 \end{rail}
5.81
5.82 @@ -349,11 +349,7 @@
5.83 \end{matharray}
5.84
5.85 \begin{rail}
5.86 - 'global' comment?
5.87 - ;
5.88 - 'local' comment?
5.89 - ;
5.90 - 'hide' name (nameref + ) comment?
5.91 + 'hide' name (nameref + )
5.92 ;
5.93 \end{rail}
5.94
5.95 @@ -404,11 +400,11 @@
5.96 \railterm{MLcommand}
5.97
5.98 \begin{rail}
5.99 - 'use' name comment?
5.100 + 'use' name
5.101 ;
5.102 - ('ML' | MLcommand | MLsetup | 'setup') text comment?
5.103 + ('ML' | MLcommand | MLsetup | 'setup') text
5.104 ;
5.105 - methodsetup name '=' text text comment?
5.106 + methodsetup name '=' text text
5.107 ;
5.108 \end{rail}
5.109
5.110 @@ -494,7 +490,7 @@
5.111
5.112 \begin{rail}
5.113 ( parseasttranslation | parsetranslation | printtranslation | typedprinttranslation |
5.114 - printasttranslation | tokentranslation ) text comment?
5.115 + printasttranslation | tokentranslation ) text
5.116 \end{rail}
5.117
5.118 Syntax translation functions written in ML admit almost arbitrary
5.119 @@ -527,7 +523,7 @@
5.120 oracle invocation. See \cite[\S6]{isabelle-ref} for more information.
5.121
5.122 \begin{rail}
5.123 - 'oracle' name '=' text comment?
5.124 + 'oracle' name '=' text
5.125 ;
5.126 \end{rail}
5.127
5.128 @@ -629,11 +625,11 @@
5.129 \railterm{equiv}
5.130
5.131 \begin{rail}
5.132 - 'fix' (vars comment? + 'and')
5.133 + 'fix' (vars + 'and')
5.134 ;
5.135 - ('assume' | 'presume') (props comment? + 'and')
5.136 + ('assume' | 'presume') (props + 'and')
5.137 ;
5.138 - 'def' thmdecl? \\ name ('==' | equiv) term termpat? comment?
5.139 + 'def' thmdecl? \\ name ('==' | equiv) term termpat?
5.140 ;
5.141 \end{rail}
5.142
5.143 @@ -677,11 +673,9 @@
5.144 $\THEN$ (and variants). Note that the special theorem name
5.145 $this$\indexisarthm{this} refers to the most recently established facts.
5.146 \begin{rail}
5.147 - 'note' (thmdef? thmrefs comment? + 'and')
5.148 + 'note' (thmdef? thmrefs + 'and')
5.149 ;
5.150 - 'then' comment?
5.151 - ;
5.152 - ('from' | 'with') (thmrefs comment? + 'and')
5.153 + ('from' | 'with') (thmrefs + 'and')
5.154 ;
5.155 \end{rail}
5.156
5.157 @@ -751,7 +745,7 @@
5.158 ('have' | 'show' | 'hence' | 'thus') goal
5.159 ;
5.160
5.161 - goal: (props comment? + 'and')
5.162 + goal: (props + 'and')
5.163 ;
5.164
5.165 goalprefix: thmdecl? locale? context?
5.166 @@ -871,16 +865,13 @@
5.167 Any remaining goals are always solved by assumption in the very last step.
5.168
5.169 \begin{rail}
5.170 - 'proof' interest? meth? comment?
5.171 + 'proof' method?
5.172 ;
5.173 - 'qed' meth? comment?
5.174 + 'qed' method?
5.175 ;
5.176 - 'by' meth meth? comment?
5.177 + 'by' method method?
5.178 ;
5.179 - ('.' | '..' | 'sorry') comment?
5.180 - ;
5.181 -
5.182 - meth: method interest?
5.183 + ('.' | '..' | 'sorry')
5.184 ;
5.185 \end{rail}
5.186
5.187 @@ -1030,7 +1021,7 @@
5.188 does not support polymorphism.
5.189
5.190 \begin{rail}
5.191 - 'let' ((term + 'and') '=' term comment? + 'and')
5.192 + 'let' ((term + 'and') '=' term + 'and')
5.193 ;
5.194 \end{rail}
5.195
5.196 @@ -1066,21 +1057,6 @@
5.197 \EN & : & \isartrans{proof(state)}{proof(state)} \\
5.198 \end{matharray}
5.199
5.200 -\railalias{lbrace}{\ttlbrace}
5.201 -\railterm{lbrace}
5.202 -
5.203 -\railalias{rbrace}{\ttrbrace}
5.204 -\railterm{rbrace}
5.205 -
5.206 -\begin{rail}
5.207 - 'next' comment?
5.208 - ;
5.209 - lbrace comment?
5.210 - ;
5.211 - rbrace comment?
5.212 - ;
5.213 -\end{rail}
5.214 -
5.215 While Isar is inherently block-structured, opening and closing blocks is
5.216 mostly handled rather casually, with little explicit user-intervention. Any
5.217 local goal statement automatically opens \emph{two} blocks, which are closed
5.218 @@ -1133,17 +1109,13 @@
5.219 \railterm{applyend}
5.220
5.221 \begin{rail}
5.222 - ( 'apply' | applyend ) method comment?
5.223 + ( 'apply' | applyend ) method
5.224 ;
5.225 - 'done' comment?
5.226 + 'defer' nat?
5.227 ;
5.228 - 'defer' nat? comment?
5.229 + 'prefer' nat
5.230 ;
5.231 - 'prefer' nat comment?
5.232 - ;
5.233 - 'back' comment?
5.234 - ;
5.235 - 'declare' thmrefs comment?
5.236 + 'declare' thmrefs
5.237 ;
5.238 \end{rail}
5.239
5.240 @@ -1237,13 +1209,13 @@
5.241 \begin{rail}
5.242 'pr' modes? nat? (',' nat)?
5.243 ;
5.244 - 'thm' modes? thmrefs comment?
5.245 + 'thm' modes? thmrefs
5.246 ;
5.247 - 'term' modes? term comment?
5.248 + 'term' modes? term
5.249 ;
5.250 - 'prop' modes? prop comment?
5.251 + 'prop' modes? prop
5.252 ;
5.253 - 'typ' modes? type comment?
5.254 + 'typ' modes? type
5.255 ;
5.256
5.257 modes: '(' (name + ) ')'
6.1 --- a/doc-src/IsarRef/syntax.tex Tue Feb 12 20:32:23 2002 +0100
6.2 +++ b/doc-src/IsarRef/syntax.tex Tue Feb 12 20:33:03 2002 +0100
6.3 @@ -102,7 +102,7 @@
6.4 Comments take the form \texttt{(*~\dots~*)} and may in principle be nested,
6.5 just as in ML. Note that these are \emph{source} comments only, which are
6.6 stripped after lexical analysis of the input. The Isar document syntax also
6.7 -provides \emph{formal comments} that are actually part of the text (see
6.8 +provides \emph{formal comments} that are considered as part of the text (see
6.9 \S\ref{sec:comments}).
6.10
6.11 \begin{warn}
6.12 @@ -165,26 +165,15 @@
6.13 Large chunks of plain \railqtoken{text} are usually given
6.14 \railtoken{verbatim}, i.e.\ enclosed in \verb|{*|~\dots~\verb|*}|. For
6.15 convenience, any of the smaller text units conforming to \railqtoken{nameref}
6.16 -are admitted as well. Almost any of the Isar commands may be annotated by a
6.17 -marginal \railnonterm{comment} of the form \texttt{--} \railqtoken{text}.
6.18 -Note that the latter kind of comment is actually part of the language, while
6.19 -source level comments \verb|(*|~\dots~\verb|*)| are stripped at the lexical
6.20 -level.
6.21 +are admitted as well. A marginal \railnonterm{comment} is of the form
6.22 +\texttt{--} \railqtoken{text}. Any number of these may occur within
6.23 +Isabelle/Isar commands.
6.24
6.25 -A few commands such as $\PROOFNAME$ admit additional markup with a ``level of
6.26 -interest'': \texttt{\%} followed by an optional number $n$ (default $n = 1$)
6.27 -indicates that the respective part of the document becomes $n$ levels more
6.28 -obscure; \texttt{\%\%} means that interest drops by $\infty$ --- abandon every
6.29 -hope, who enter here. So far the Isabelle tool-chain (for document output
6.30 -etc.) does not yet treat interest levels specifically.
6.31 -
6.32 -\indexoutertoken{text}\indexouternonterm{comment}\indexouternonterm{interest}
6.33 +\indexoutertoken{text}\indexouternonterm{comment}
6.34 \begin{rail}
6.35 text: verbatim | nameref
6.36 ;
6.37 - comment: ('--' text +)
6.38 - ;
6.39 - interest: percent nat? | ppercent
6.40 + comment: '--' text
6.41 ;
6.42 \end{rail}
6.43