--- a/doc-src/IsarRef/generic.tex Tue Feb 12 20:32:23 2002 +0100
+++ b/doc-src/IsarRef/generic.tex Tue Feb 12 20:33:03 2002 +0100
@@ -25,9 +25,9 @@
Isabelle documentation.
\begin{rail}
- 'axclass' classdecl (axmdecl prop comment? +)
+ 'axclass' classdecl (axmdecl prop +)
;
- 'instance' (nameref ('<' | subseteq) nameref | nameref '::' simplearity) comment?
+ 'instance' (nameref ('<' | subseteq) nameref | nameref '::' simplearity)
;
\end{rail}
@@ -79,7 +79,7 @@
corresponding parameters do \emph{not} occur in the conclusion.
\begin{rail}
- 'obtain' (vars + 'and') comment? \\ 'where' (props comment? + 'and')
+ 'obtain' (vars + 'and') 'where' (props + 'and')
;
\end{rail}
@@ -163,14 +163,12 @@
\end{matharray}
\begin{rail}
- ('also' | 'finally') transrules? comment?
- ;
- ('moreover' | 'ultimately') comment?
+ ('also' | 'finally') transrules?
;
'trans' (() | 'add' | 'del')
;
- transrules: '(' thmrefs ')' interest?
+ transrules: '(' thmrefs ')'
;
\end{rail}
@@ -193,9 +191,9 @@
\item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$,
but collect results only, without applying rules.
-
-\item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity
- rules declared in the current context.
+
+\item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity (and
+ symmetry) rules declared in the current context.
\item [$trans$] declares theorems as transitivity rules.
--- a/doc-src/IsarRef/intro.tex Tue Feb 12 20:32:23 2002 +0100
+++ b/doc-src/IsarRef/intro.tex Tue Feb 12 20:33:03 2002 +0100
@@ -7,7 +7,7 @@
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 needs
+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
@@ -21,8 +21,8 @@
\medskip Apart from these technical advances over bare-bones ML programming,
the main intention of Isar 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
+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 provides a versatile environment for structured formal proof
documents. Thus properly written Isar proof texts become accessible to a
@@ -34,33 +34,32 @@
own right, independently of the mechanic proof-checking process.
Despite its grand design of structured proof texts, Isar is able to assimilate
-the old-style tactical as an ``improper'' sub-language. This provides an easy
+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
-experimentation and debugging of interactive proofs. Isabelle/Isar freely
-supports a broad range of proof styles, including unreadable ones.
+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 generic and should work for reasonably
-well for any object-logic that directly conforms to the view of natural
-deduction according to the Isabelle/Pure framework. Major Isabelle logics
-(HOL \cite{isabelle-HOL}, HOLCF, FOL \cite{isabelle-logics}, ZF
-\cite{isabelle-ZF}) have already been setup for immediate use by end-users.
-
-Note that much of the existing body of theories still consist of old-style
-theory files with accompanied ML code for proof scripts. This legacy will be
-converted as time goes by.
+\medskip The Isabelle/Isar framework is generic and should work reasonably
+well for any Isabelle object-logic that conforms to the natural deduction view
+of the Isabelle/Pure framework. Major Isabelle logics like HOL
+\cite{isabelle-HOL}, HOLCF \cite{MuellerNvOS99}, FOL \cite{isabelle-logics},
+and ZF \cite{isabelle-ZF} have already been set up for end-users.
+Nonetheless, much of the existing body of theories still consist of old-style
+theory files with accompanied ML code for proof scripts; this legacy will be
+gradually converted in due time.
\section{Quick start}
\subsection{Terminal sessions}
-Isar is already part of Isabelle (as of version Isabelle99, or later). The
-\texttt{isabelle} binary provides option \texttt{-I} to run the Isabelle/Isar
-interaction loop at startup, rather than the raw ML top-level. So the
-quickest way to do anything with Isabelle/Isar is as follows:
+Isar is already part of Isabelle. The low-level \texttt{isabelle} binary
+provides option \texttt{-I} to run the Isabelle/Isar interaction loop at
+startup, rather than the raw ML top-level. So the most basic way to do
+anything with Isabelle/Isar is as follows:
\begin{ttbox}
isabelle -I HOL\medskip
-\out{> Welcome to Isabelle/HOL (Isabelle99-1)}\medskip
+\out{> Welcome to Isabelle/HOL (Isabelle2002)}\medskip
theory Foo = Main:
constdefs foo :: nat "foo == 1";
lemma "0 < foo" by (simp add: foo_def);
@@ -75,38 +74,37 @@
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. David Aspinall's
-\emph{Proof~General}\index{Proof General} environment
-\cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs interface for
-interactive theorem provers that does 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.
+demands some better user-interface support. The Proof~General environment by
+David Aspinall \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
+interface for interactive theorem provers that organizes all the cut-and-paste
+and forward-backward walk through the text in a very neat way. In
+Isabelle/Isar, the current position within a partial proof document is equally
+important than the actual proof state. Thus Proof~General provides the
+canonical working environment for Isabelle/Isar, both for getting acquainted
+(e.g.\ by replaying existing Isar documents) and for production work.
\subsubsection{Proof~General as default Isabelle interface}
-The easiest way to invoke Proof~General is via the Isabelle interface wrapper
-script. The default configuration of Isabelle is smart enough to detect the
-Proof~General distribution in several canonical places (e.g.\
-\texttt{\$ISABELLE_HOME/contrib/ProofGeneral}). Thus the capital
-\texttt{Isabelle} executable would already refer to the
+The Isabelle interface wrapper script provides an easy way to invoke
+Proof~General (and XEmacs or GNU Emacs). The default configuration of
+Isabelle is smart enough to detect the Proof~General distribution in several
+canonical places (e.g.\ \texttt{\$ISABELLE_HOME/contrib/ProofGeneral}). Thus
+the capital \texttt{Isabelle} executable would already refer to the
\texttt{ProofGeneral/isar} interface without further ado.\footnote{There is
also a \texttt{ProofGeneral/isa} interface for old tactic scripts written in
- ML.} The Isabelle interface script provides several options, just pass
-\verb,-?, to see its usage.
+ ML.} 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/BasicLogic.thy
+Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
\end{ttbox}
-Users of XEmacs may note the tool bar for navigating forward and backward
-through the text. Consult the Proof~General documentation \cite{proofgeneral}
-for further basic command sequences, such as ``\texttt{C-c C-return}'' or
-``\texttt{C-c u}''.
+Users may note the tool bar for navigating forward and backward through the
+text (this depends on the local Emacs installation). Consult the
+Proof~General documentation \cite{proofgeneral} for further basic command
+sequences, in particular ``\texttt{C-c C-return}'' and ``\texttt{C-c u}''.
\medskip
@@ -122,27 +120,27 @@
\medskip
Apart from the Isabelle command line, defaults for interface options may be
-given by the \texttt{PROOFGENERAL_OPTIONS} setting as well. For example, the
-Emacs executable to be used may be configured in Isabelle's settings like this:
+given by the \texttt{PROOFGENERAL_OPTIONS} setting. For example, the Emacs
+executable to be used may be configured in Isabelle's settings like this:
\begin{ttbox}
PROOFGENERAL_OPTIONS="-p xemacs-nomule"
\end{ttbox}
-Occasionally, the user's \verb,~/.emacs, file contains material that is
-incompatible with the version of Emacs that Proof~General prefers. Then
-proper startup may be still achieved by using the \texttt{-u false} option.
-Also note that any Emacs lisp file called \texttt{proofgeneral-settings.el}
-occurring in \texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc}
-is automatically loaded by the Proof~General interface script as well.
+Occasionally, a user's \verb,~/.emacs, file contains code that is incompatible
+with the (X)Emacs version used by Proof~General, causing the interface startup
+to fail prematurely. Here the \texttt{-u false} option helps to get the
+interface process up and running. Note that additional Lisp customization
+code may reside in \texttt{proofgeneral-settings.el} of
+\texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc}.
\subsubsection{The X-Symbol package}
-Proof~General also supports the Emacs X-Symbol package \cite{x-symbol}, which
-provides a nice way to get proper mathematical symbols displayed on screen.
-Just pass option \texttt{-x true} to the Isabelle interface script, or check
-the appropriate menu setting by hand. In any case, the X-Symbol package must
-have been properly installed already.
+Proof~General provides native support for the Emacs X-Symbol package
+\cite{x-symbol}, which handles proper mathematical symbols displayed on
+screen. Pass option \texttt{-x true} to the Isabelle interface script, or
+check the appropriate Proof~General menu setting by hand. In any case, the
+X-Symbol package must have been properly installed already.
Contrary to what you may expect from the documentation of X-Symbol, the
package is very easy to install and configures itself automatically. The
@@ -159,7 +157,7 @@
symbols. Nevertheless, the Isabelle document preparation system (see
\S\ref{sec:document-prep}) will be happy to print non-ASCII symbols properly.
It is even possible to invent additional notation beyond the display
-capabilities of XEmacs and X-Symbol.
+capabilities of Emacs and X-Symbol.
\section{Isabelle/Isar theories}
@@ -181,9 +179,9 @@
The Isar proof language is embedded into the new theory format as a proper
sub-language. Proof mode is entered by stating some $\THEOREMNAME$ or
$\LEMMANAME$ at the theory level, and left again with the final conclusion
-(e.g.\ via $\QEDNAME$). A few theory extension mechanisms require proof as
-well, such as HOL's $\isarkeyword{typedef}$ which demands non-emptiness of the
-representing sets.
+(e.g.\ via $\QEDNAME$). A few theory specification mechanisms also require
+some proof, such as HOL's $\isarkeyword{typedef}$ which demands non-emptiness
+of the representing sets.
New-style theory files may still be associated with separate ML files
consisting of plain old tactic scripts. There is no longer any ML binding
@@ -195,138 +193,133 @@
Isar proof language at all.
\begin{warn}
- Currently, Proof~General does \emph{not} support mixed interactive
- development of classic Isabelle theory files or tactic scripts, together
- with Isar documents. The ``\texttt{isa}'' and ``\texttt{isar}'' versions of
+ Proof~General does \emph{not} support mixed interactive development of
+ classic Isabelle theory files or tactic scripts, together with Isar
+ documents. The ``\texttt{isa}'' and ``\texttt{isar}'' versions of
Proof~General are handled as two different theorem proving systems, only one
of these may be active at the same time.
\end{warn}
-Conversion of existing tactic scripts is best done by running two separate
-Proof~General sessions, one for replaying the old script and the other for the
-emerging Isabelle/Isar document. Also note that Isar supports emulation
-commands and methods that support traditional tactic scripts within new-style
-theories, see appendix~\ref{ap:conv} for more information.
+Manual conversion of existing tactic scripts may be done by running two
+separate Proof~General sessions, one for replaying the old script and the
+other for the emerging Isabelle/Isar document. Also note that Isar supports
+emulation commands and methods that support traditional tactic scripts within
+new-style theories, see appendix~\ref{ap:conv} for more information.
\subsection{Document preparation}\label{sec:document-prep}
-Isabelle/Isar provides a simple document preparation system based on current
-(PDF) {\LaTeX} technology, with full support of hyper-links (both local
-references and URLs), bookmarks, thumbnails etc. Thus the results are equally
-well suited for WWW browsing and as printed copies.
+Isabelle/Isar provides a simple document preparation system based on existing
+PDF-\LaTeX technology, with full support of hyper-links (both local references
+and URLs), bookmarks, and thumbnails. Thus the results are equally well
+suited for WWW browsing and as printed copies.
\medskip
Isabelle generates {\LaTeX} output as part of the run of a \emph{logic
session} (see also \cite{isabelle-sys}). Getting started with a working
configuration for common situations is quite easy by using the Isabelle
-\texttt{mkdir} and \texttt{make} tools. Just invoke
+\texttt{mkdir} and \texttt{make} tools. First invoke
\begin{ttbox}
- isatool mkdir -d Foo
+ isatool mkdir Foo
\end{ttbox}
-to setup a separate directory for session \texttt{Foo}.\footnote{It is safe to
- experiment, since \texttt{isatool mkdir} never overwrites existing files.}
-Ensure that \texttt{Foo/ROOT.ML} loads all theories required for this session.
-Furthermore \texttt{Foo/document/root.tex} should include any special {\LaTeX}
-macro packages required for your document (the default is usually sufficient
-as a start).
+to initialize a separate directory for session \texttt{Foo} --- it is safe to
+experiment, since \texttt{isatool mkdir} never overwrites existing files.
+Ensure that \texttt{Foo/ROOT.ML} holds ML commands to load all theories
+required for this session; furthermore \texttt{Foo/document/root.tex} should
+include any special {\LaTeX} macro packages required for your document (the
+default is usually sufficient as a start).
-The session is controlled by a separate \texttt{IsaMakefile} (with very crude
-source dependencies only by default). This file is located one level up from
-the \texttt{Foo} directory location. At that point just invoke
+The session is controlled by a separate \texttt{IsaMakefile} (with crude
+source dependencies by default). This file is located one level up from the
+\texttt{Foo} directory location. Now invoke
\begin{ttbox}
isatool make Foo
\end{ttbox}
to run the \texttt{Foo} session, with browser information and document
preparation enabled. Unless any errors are reported by Isabelle or {\LaTeX},
-the output will appear inside the directory indicated by \texttt{isatool
- getenv ISABELLE_BROWSER_INFO}, with the logical session prefix added (e.g.\
-\texttt{HOL/Foo}). Note that the \texttt{index.html} located there provides a
-link to the finished {\LaTeX} document, too.
-
-Note that this really is batch processing --- better let Isabelle check your
-theory and proof developments beforehand in interactive mode.
+the output will appear inside the directory \texttt{ISABELLE_BROWSER_INFO}, as
+reported by the batch job in verbose mode.
\medskip
You may also consider to tune the \texttt{usedir} options in
\texttt{IsaMakefile}, for example to change the output format from
-\texttt{dvi} to \texttt{pdf}, or activate the \texttt{-D document} option in
-order to preserve a copy of the generated {\LaTeX} sources. The latter
-feature is very useful for debugging {\LaTeX} errors, while avoiding repeated
-runs of Isabelle.
+\texttt{pdf} to \texttt{dvi}, or activate the \texttt{-D generated} option in
+order to keep 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.
+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}
-%FIXME tune
+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 (degenerative) view of Isar at the least.
-This is one of the key questions, of course. Isar offers a rather different
-approach to formal proof documents than plain old tactic scripts. Experienced
-users of existing interactive theorem proving systems may have to learn
-thinking differently in order to make effective use of Isabelle/Isar. On the
-other hand, Isabelle/Isar comes much closer to existing mathematical practice
-of formal proof, so users with less experience in old-style tactical proving,
-but a good understanding of mathematical proof, might cope with Isar even
-better. See also \cite{Wenzel:1999:TPHOL,Bauer-Wenzel:2000:HB} for further
-background information on 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 This really is a reference manual on Isabelle/Isar, not a tutorial.
-Nevertheless, we will also give some clues of how the concepts introduced here
-may be put into practice. Appendix~\ref{ap:refcard} provides a quick
-reference card of the most common Isabelle/Isar language elements.
-Appendix~\ref{ap:conv} offers some practical hints on converting existing
-Isabelle theories and proof scripts to the new format.
+\medskip The present text really is only a reference manual on Isabelle/Isar,
+not a tutorial. Nevertheless, we will attempt to give some clues of how the
+concepts introduced here may be put into practice. Appendix~\ref{ap:refcard}
+provides a quick reference card of the most common Isabelle/Isar language
+elements. Appendix~\ref{ap:conv} offers some practical hints on converting
+existing Isabelle theories and proof scripts to the new format (without
+restructuring proofs).
-Several example applications are distributed with Isabelle, and available via
-the Isabelle WWW library as well as the Isabelle/Isar page:
-\begin{center}\small
- \begin{tabular}{l}
- \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
- \url{http://isabelle.in.tum.de/library/} \\[1ex]
- \url{http://isabelle.in.tum.de/Isar/} \\
- \end{tabular}
-\end{center}
+Further issues concerning the Isar concepts are covered in the literature
+\cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
+The author's PhD thesis \cite{Wenzel-PhD} presently provides the most complete
+exposition of Isar foundations, techniques, and applications. A number of
+example applications are distributed with Isabelle, and available via the
+Isabelle WWW library (e.g.\ \url{http://isabelle.in.tum.de/library/}). As a
+general rule of thumb, more recent Isabelle applications that also include a
+separate ``document'' (in PDF) are more likely to consist of proper
+Isabelle/Isar theories and proofs.
-The following examples may be of particular interest. Apart from the plain
-sources represented in HTML, these Isabelle sessions also provide actual
-documents (in PDF).
-\begin{itemize}
-\item \url{http://isabelle.in.tum.de/library/HOL/Isar_examples/} is a
- collection of introductory examples.
-\item \url{http://isabelle.in.tum.de/library/HOL/Lattice/} is an example of
- typical mathematics-style reasoning in ``axiomatic'' structures.
-\item \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/HahnBanach/} is a
- big mathematics application on infinitary vector spaces and functional
- analysis.
-\item \url{http://isabelle.in.tum.de/library/HOL/Lambda/} develops fundamental
- properties of $\lambda$-calculus (Church-Rosser and termination).
+%FIXME
+% The following examples may be of particular interest. Apart from the plain
+% sources represented in HTML, these Isabelle sessions also provide actual
+% documents (in PDF).
+% \begin{itemize}
+% \item \url{http://isabelle.in.tum.de/library/HOL/Isar_examples/} is a
+% collection of introductory examples.
+% \item \url{http://isabelle.in.tum.de/library/HOL/Lattice/} is an example of
+% typical mathematics-style reasoning in ``axiomatic'' structures.
+% \item \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/HahnBanach/} is a
+% big mathematics application on infinitary vector spaces and functional
+% analysis.
+% \item \url{http://isabelle.in.tum.de/library/HOL/Lambda/} develops fundamental
+% properties of $\lambda$-calculus (Church-Rosser and termination).
- This may serve as a realistic example of porting of legacy proof scripts
- into Isar tactic emulation scripts.
-\item \url{http://isabelle.in.tum.de/library/HOL/Unix/} gives a mathematical
- model of the main aspects of the Unix file-system including its security
- model, but ignoring processes. A few odd effects caused by the general
- ``worse-is-better'' approach followed in Unix are discussed within the
- formal model.
+% This may serve as a realistic example of porting of legacy proof scripts
+% into Isar tactic emulation scripts.
+% \item \url{http://isabelle.in.tum.de/library/HOL/Unix/} gives a mathematical
+% model of the main aspects of the Unix file-system including its security
+% model, but ignoring processes. A few odd effects caused by the general
+% ``worse-is-better'' approach followed in Unix are discussed within the
+% formal model.
- This example represents a non-trivial verification task, with all proofs
- carefully worked out using the proper part of the Isar proof language;
- unstructured scripts are only used for symbolic evaluation.
-\item \url{http://isabelle.in.tum.de/library/HOL/MicroJava/} is a
- formalization of a fragment of Java, together with a corresponding virtual
- machine and a specification of its bytecode verifier and a lightweight
- bytecode verifier, including proofs of type-safety.
+% This example represents a non-trivial verification task, with all proofs
+% carefully worked out using the proper part of the Isar proof language;
+% unstructured scripts are only used for symbolic evaluation.
+% \item \url{http://isabelle.in.tum.de/library/HOL/MicroJava/} is a
+% formalization of a fragment of Java, together with a corresponding virtual
+% machine and a specification of its bytecode verifier and a lightweight
+% bytecode verifier, including proofs of type-safety.
- This represents a very ``realistic'' example of large formalizations
- performed in form of tactic emulation scripts and proper Isar proof texts.
-\end{itemize}
+% This represents a very ``realistic'' example of large formalizations
+% performed in form of tactic emulation scripts and proper Isar proof texts.
+% \end{itemize}
%%% Local Variables:
--- a/doc-src/IsarRef/isar-ref.tex Tue Feb 12 20:32:23 2002 +0100
+++ b/doc-src/IsarRef/isar-ref.tex Tue Feb 12 20:33:03 2002 +0100
@@ -69,21 +69,6 @@
\pagenumbering{roman} \tableofcontents \clearfirst
-%FIXME
-\nocite{Aspinall:2000:eProof}
-\nocite{Bauer-Wenzel:2000:HB}
-\nocite{Harrison:1996:MizarHOL}
-\nocite{Muzalewski:Mizar}
-\nocite{Rudnicki:1992:MizarOverview}
-\nocite{Rudnicki:1992:MizarOverview}
-\nocite{Syme:1997:DECLARE}
-\nocite{Syme:1998:thesis}
-\nocite{Syme:1999:TPHOL}
-\nocite{Trybulec:1993:MizarFeatures}
-\nocite{Wiedijk:1999:Mizar}
-\nocite{Wiedijk:2000:MV}
-\nocite{Zammit:1999:TPHOL}
-
\include{intro}
\include{basics}
\include{syntax}
--- a/doc-src/IsarRef/logics.tex Tue Feb 12 20:32:23 2002 +0100
+++ b/doc-src/IsarRef/logics.tex Tue Feb 12 20:33:03 2002 +0100
@@ -90,9 +90,9 @@
\end{matharray}
\begin{rail}
- 'typedecl' typespec infix? comment?
+ 'typedecl' typespec infix?
;
- 'typedef' parname? typespec infix? \\ '=' term comment?
+ 'typedef' parname? typespec infix? '=' term
;
\end{rail}
@@ -186,7 +186,7 @@
dtspec: parname? typespec infix? '=' (cons + '|')
;
- cons: name (type * ) mixfix? comment?
+ cons: name (type * ) mixfix?
;
dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
\end{rail}
@@ -236,14 +236,12 @@
\begin{rail}
'primrec' parname? (equation + )
;
- 'recdef' ('(' 'permissive' ')')? \\ name term (eqn + ) hints?
+ 'recdef' ('(' 'permissive' ')')? \\ name term (prop + ) hints?
;
- recdeftc thmdecl? tc comment?
+ recdeftc thmdecl? tc
;
- equation: thmdecl? eqn
- ;
- eqn: prop comment?
+ equation: thmdecl? prop
;
hints: '(' 'hints' (recdefmod * ) ')'
;
@@ -329,11 +327,11 @@
'mono' (() | 'add' | 'del')
;
- sets: (term comment? +)
+ sets: (term +)
;
- intros: 'intros' (thmdecl? prop comment? +)
+ intros: 'intros' (thmdecl? prop +)
;
- monos: 'monos' thmrefs comment?
+ monos: 'monos' thmrefs
;
\end{rail}
@@ -404,7 +402,7 @@
;
indcases (prop +)
;
- inductivecases thmdecl? (prop +) comment?
+ inductivecases thmdecl? (prop +)
;
rule: ('rule' ':' thmref)
@@ -468,7 +466,7 @@
dmspec: typespec '=' (cons + '|')
;
- cons: name (type * ) mixfix? comment?
+ cons: name (type * ) mixfix?
;
dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
\end{rail}
--- a/doc-src/IsarRef/pure.tex Tue Feb 12 20:32:23 2002 +0100
+++ b/doc-src/IsarRef/pure.tex Tue Feb 12 20:33:03 2002 +0100
@@ -5,7 +5,7 @@
commands, together with fundamental proof methods and attributes.
Chapter~\ref{ch:gen-tools} describes further Isar elements provided by generic
tools and packages (such as the Simplifier) that are either part of Pure
-Isabelle or pre-installed by most object logics. Chapter~\ref{ch:logics}
+Isabelle or pre-installed in most object logics. Chapter~\ref{ch:logics}
refers to object-logic specific elements (mainly for HOL and ZF).
\medskip
@@ -162,11 +162,11 @@
\end{matharray}
\begin{rail}
- 'classes' (classdecl comment? +)
+ 'classes' (classdecl +)
;
- 'classrel' nameref ('<' | subseteq) nameref comment?
+ 'classrel' nameref ('<' | subseteq) nameref
;
- 'defaultsort' sort comment?
+ 'defaultsort' sort
;
\end{rail}
@@ -195,13 +195,13 @@
\end{matharray}
\begin{rail}
- 'types' (typespec '=' type infix? comment? +)
+ 'types' (typespec '=' type infix? +)
;
- 'typedecl' typespec infix? comment?
+ 'typedecl' typespec infix?
;
- 'nonterminals' (name +) comment?
+ 'nonterminals' (name +)
;
- 'arities' (nameref '::' arity comment? +)
+ 'arities' (nameref '::' arity +)
;
\end{rail}
@@ -236,12 +236,12 @@
\begin{rail}
'consts' (constdecl +)
;
- 'defs' ('(overloaded)')? (axmdecl prop comment? +)
+ 'defs' ('(overloaded)')? (axmdecl prop +)
;
- 'constdefs' (constdecl prop comment? +)
+ 'constdefs' (constdecl prop +)
;
- constdecl: name '::' type mixfix? comment?
+ constdecl: name '::' type mixfix?
;
\end{rail}
@@ -284,7 +284,7 @@
\begin{rail}
'syntax' ('(' ( name | 'output' | name 'output' ) ')')? (constdecl +)
;
- 'translations' (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat comment? +)
+ 'translations' (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
;
transpat: ('(' nameref ')')? string
;
@@ -317,9 +317,9 @@
\end{matharray}
\begin{rail}
- 'axioms' (axmdecl prop comment? +)
+ 'axioms' (axmdecl prop +)
;
- ('lemmas' | 'theorems') (thmdef? thmrefs comment? + 'and')
+ ('lemmas' | 'theorems') (thmdef? thmrefs + 'and')
;
\end{rail}
@@ -349,11 +349,7 @@
\end{matharray}
\begin{rail}
- 'global' comment?
- ;
- 'local' comment?
- ;
- 'hide' name (nameref + ) comment?
+ 'hide' name (nameref + )
;
\end{rail}
@@ -404,11 +400,11 @@
\railterm{MLcommand}
\begin{rail}
- 'use' name comment?
+ 'use' name
;
- ('ML' | MLcommand | MLsetup | 'setup') text comment?
+ ('ML' | MLcommand | MLsetup | 'setup') text
;
- methodsetup name '=' text text comment?
+ methodsetup name '=' text text
;
\end{rail}
@@ -494,7 +490,7 @@
\begin{rail}
( parseasttranslation | parsetranslation | printtranslation | typedprinttranslation |
- printasttranslation | tokentranslation ) text comment?
+ printasttranslation | tokentranslation ) text
\end{rail}
Syntax translation functions written in ML admit almost arbitrary
@@ -527,7 +523,7 @@
oracle invocation. See \cite[\S6]{isabelle-ref} for more information.
\begin{rail}
- 'oracle' name '=' text comment?
+ 'oracle' name '=' text
;
\end{rail}
@@ -629,11 +625,11 @@
\railterm{equiv}
\begin{rail}
- 'fix' (vars comment? + 'and')
+ 'fix' (vars + 'and')
;
- ('assume' | 'presume') (props comment? + 'and')
+ ('assume' | 'presume') (props + 'and')
;
- 'def' thmdecl? \\ name ('==' | equiv) term termpat? comment?
+ 'def' thmdecl? \\ name ('==' | equiv) term termpat?
;
\end{rail}
@@ -677,11 +673,9 @@
$\THEN$ (and variants). Note that the special theorem name
$this$\indexisarthm{this} refers to the most recently established facts.
\begin{rail}
- 'note' (thmdef? thmrefs comment? + 'and')
+ 'note' (thmdef? thmrefs + 'and')
;
- 'then' comment?
- ;
- ('from' | 'with') (thmrefs comment? + 'and')
+ ('from' | 'with') (thmrefs + 'and')
;
\end{rail}
@@ -751,7 +745,7 @@
('have' | 'show' | 'hence' | 'thus') goal
;
- goal: (props comment? + 'and')
+ goal: (props + 'and')
;
goalprefix: thmdecl? locale? context?
@@ -871,16 +865,13 @@
Any remaining goals are always solved by assumption in the very last step.
\begin{rail}
- 'proof' interest? meth? comment?
+ 'proof' method?
;
- 'qed' meth? comment?
+ 'qed' method?
;
- 'by' meth meth? comment?
+ 'by' method method?
;
- ('.' | '..' | 'sorry') comment?
- ;
-
- meth: method interest?
+ ('.' | '..' | 'sorry')
;
\end{rail}
@@ -1030,7 +1021,7 @@
does not support polymorphism.
\begin{rail}
- 'let' ((term + 'and') '=' term comment? + 'and')
+ 'let' ((term + 'and') '=' term + 'and')
;
\end{rail}
@@ -1066,21 +1057,6 @@
\EN & : & \isartrans{proof(state)}{proof(state)} \\
\end{matharray}
-\railalias{lbrace}{\ttlbrace}
-\railterm{lbrace}
-
-\railalias{rbrace}{\ttrbrace}
-\railterm{rbrace}
-
-\begin{rail}
- 'next' comment?
- ;
- lbrace comment?
- ;
- rbrace comment?
- ;
-\end{rail}
-
While Isar is inherently block-structured, opening and closing blocks is
mostly handled rather casually, with little explicit user-intervention. Any
local goal statement automatically opens \emph{two} blocks, which are closed
@@ -1133,17 +1109,13 @@
\railterm{applyend}
\begin{rail}
- ( 'apply' | applyend ) method comment?
+ ( 'apply' | applyend ) method
;
- 'done' comment?
- ;
- 'defer' nat? comment?
+ 'defer' nat?
;
- 'prefer' nat comment?
+ 'prefer' nat
;
- 'back' comment?
- ;
- 'declare' thmrefs comment?
+ 'declare' thmrefs
;
\end{rail}
@@ -1237,13 +1209,13 @@
\begin{rail}
'pr' modes? nat? (',' nat)?
;
- 'thm' modes? thmrefs comment?
+ 'thm' modes? thmrefs
;
- 'term' modes? term comment?
+ 'term' modes? term
;
- 'prop' modes? prop comment?
+ 'prop' modes? prop
;
- 'typ' modes? type comment?
+ 'typ' modes? type
;
modes: '(' (name + ) ')'
--- a/doc-src/IsarRef/syntax.tex Tue Feb 12 20:32:23 2002 +0100
+++ b/doc-src/IsarRef/syntax.tex Tue Feb 12 20:33:03 2002 +0100
@@ -102,7 +102,7 @@
Comments take the form \texttt{(*~\dots~*)} and may in principle be nested,
just as in ML. Note that these are \emph{source} comments only, which are
stripped after lexical analysis of the input. The Isar document syntax also
-provides \emph{formal comments} that are actually part of the text (see
+provides \emph{formal comments} that are considered as part of the text (see
\S\ref{sec:comments}).
\begin{warn}
@@ -165,26 +165,15 @@
Large chunks of plain \railqtoken{text} are usually given
\railtoken{verbatim}, i.e.\ enclosed in \verb|{*|~\dots~\verb|*}|. For
convenience, any of the smaller text units conforming to \railqtoken{nameref}
-are admitted as well. Almost any of the Isar commands may be annotated by a
-marginal \railnonterm{comment} of the form \texttt{--} \railqtoken{text}.
-Note that the latter kind of comment is actually part of the language, while
-source level comments \verb|(*|~\dots~\verb|*)| are stripped at the lexical
-level.
+are admitted as well. A marginal \railnonterm{comment} is of the form
+\texttt{--} \railqtoken{text}. Any number of these may occur within
+Isabelle/Isar commands.
-A few commands such as $\PROOFNAME$ admit additional markup with a ``level of
-interest'': \texttt{\%} followed by an optional number $n$ (default $n = 1$)
-indicates that the respective part of the document becomes $n$ levels more
-obscure; \texttt{\%\%} means that interest drops by $\infty$ --- abandon every
-hope, who enter here. So far the Isabelle tool-chain (for document output
-etc.) does not yet treat interest levels specifically.
-
-\indexoutertoken{text}\indexouternonterm{comment}\indexouternonterm{interest}
+\indexoutertoken{text}\indexouternonterm{comment}
\begin{rail}
text: verbatim | nameref
;
- comment: ('--' text +)
- ;
- interest: percent nat? | ppercent
+ comment: '--' text
;
\end{rail}