# HG changeset patch # User wenzelm # Date 1013542383 -3600 # Node ID 8e1cae1de136e87dcc879ebc43f6191efeeb55fe # Parent 2896f88180b9ba5581791b99af9f165a346adb5e tuned; diff -r 2896f88180b9 -r 8e1cae1de136 doc-src/IsarRef/generic.tex --- 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. diff -r 2896f88180b9 -r 8e1cae1de136 doc-src/IsarRef/intro.tex --- 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: diff -r 2896f88180b9 -r 8e1cae1de136 doc-src/IsarRef/isar-ref.tex --- 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} diff -r 2896f88180b9 -r 8e1cae1de136 doc-src/IsarRef/logics.tex --- 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} diff -r 2896f88180b9 -r 8e1cae1de136 doc-src/IsarRef/pure.tex --- 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 + ) ')' diff -r 2896f88180b9 -r 8e1cae1de136 doc-src/IsarRef/syntax.tex --- 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}