# HG changeset patch # User wenzelm # Date 970834788 -7200 # Node ID bb8f9412fec62e407112120fc35ec1d600a82285 # Parent a72ddfdbfca09c0d8b74a4afa713b42be5967f6e tuned; diff -r a72ddfdbfca0 -r bb8f9412fec6 doc-src/IsarRef/conversion.tex --- a/doc-src/IsarRef/conversion.tex Fri Oct 06 12:31:53 2000 +0200 +++ b/doc-src/IsarRef/conversion.tex Fri Oct 06 14:19:48 2000 +0200 @@ -1,15 +1,15 @@ -\chapter{The Isabelle/Isar Conversion Guide} +\chapter{Isabelle/Isar Conversion Guide}\label{ap:conv} Subsequently, we give a few practical hints on working in a mixed environment of old Isabelle ML proof scripts and new Isabelle/Isar theories. There are basically three ways to cope with this issue. \begin{enumerate} \item Do not convert old sources at all, but communicate directly at the level - of internal theory and theorem values. + of \emph{internal} theory and theorem values. \item Port old-style theory files to new-style ones (very easy), and ML proof scripts to Isar tactic-emulation scripts (quite easy). -\item Actually redo ML proof scripts as human readable Isar proof texts +\item Actually redo ML proof scripts as human-readable Isar proof texts (probably hard, depending who wrote the original scripts). \end{enumerate} @@ -48,8 +48,8 @@ Old-style theories often use the ML binding \texttt{thy}, which is dynamically created by the ML code generated from old theory source. This - is no longer the recommended way in any case! The \texttt{the_context} - function should be used for old scripts as well. + is no longer the recommended way in any case! Function \texttt{the_context} + should be used for old scripts as well. \item [$\mathtt{theory}~name$] retrieves the named theory from the global theory-loader database. @@ -67,7 +67,7 @@ bind_thms : string * thm list -> unit \end{ttbox} -ML proof scripts have to be well-behaved in storing theorems properly within +ML proof scripts have to be well-behaved by storing theorems properly within the current theory context, in order to enable new-style theories to retrieve these these later. @@ -76,14 +76,15 @@ ML. This already manages entry in the theorem database of the current theory context. \item [$\mathtt{bind_thm}~(name, thm)$ and $\mathtt{bind_thms}~(name, thms)$] - store (lists of) theorems that have been produced in ML in an ad-hoc manner. + store theorems that have been produced in ML in an ad-hoc manner. \end{descr} Note that the original ``LCF-system'' approach of binding theorem values on -the ML toplevel only has long been given up in Isabelle! Legacy proof scripts -occasionally contain code such as \texttt{val foo = result();} which is -ill-behaved in several respects. Apart from preventing access from Isar -theories, it also omits the result from the WWW presentation, for example. +the ML toplevel only has long been given up in Isabelle! Despite of this, old +legacy proof scripts occasionally contain code such as \texttt{val foo = + result();} which is ill-behaved in several respects. Apart from preventing +access from Isar theories, it also omits the result from the WWW presentation, +for example. \subsection{ML declarations in Isar} @@ -98,8 +99,8 @@ \[ \isarkeyword{ML}~\{*~\mbox{\texttt{val foo = thm "foo"}}~*\} \] -This command cannot be undone; invalid theorem bindings in ML may persist. -Also note that the current theory may not be modified; use +Note that this command cannot be undone, so invalid theorem bindings in ML may +persist. Also note that the current theory may not be modified; use $\isarkeyword{ML_setup}$ for declarations that act on the current context. @@ -142,14 +143,13 @@ identifiers $x$, numerals $1$, or symbols $\forall$ (input as \verb,\,). \item Theorem declarations require an explicit colon to separate the name from - the statement (the name is usually optional). See the syntax of $\DEFS$ in - \S\ref{sec:consts}, or $\THEOREMNAME$ in \S\ref{sec:axms-thms}), for - example. + the statement (the name is usually optional). Cf.\ the syntax of $\DEFS$ in + \S\ref{sec:consts}, or $\THEOREMNAME$ in \S\ref{sec:axms-thms}. \end{itemize} -Also note that Isabelle/Isar error messages are usually quite explicit about -the problem at hand. So in cases of doubt, input syntax may be just as well -tried interactively. +Note that Isabelle/Isar error messages are usually quite explicit about the +problem at hand. So in cases of doubt, input syntax may be just as well tried +out interactively. \subsection{Goal statements}\label{sec:conv-goal} @@ -194,33 +194,33 @@ Isar Proof methods closely resemble traditional tactics, when used in unstructured sequences of $\isarkeyword{apply}$ commands (cf.\ \S\ref{sec:conv-goal}). Isabelle/Isar provides emulations for all major ML -tactic of classic Isabelle, mostly for the sake of easy porting of existing -developments --- actual Isar proof texts would demand much less diversity of -proof methods. +tactics of classic Isabelle --- mostly for the sake of easy porting of +existing developments, as actual Isar proof texts would demand much less +diversity of proof methods. Unlike tactic expressions in ML, Isar proof methods provide proper concrete syntax for additional arguments, options, modifiers etc. Thus a typical method text is usually more concise than the corresponding ML tactic. Furthermore, the Isar versions of classic Isabelle tactics often cover several -variant forms into a single method, with separate options to tune the -behavior. For example, method $simp$ replaces all of \texttt{simp_tac}~/ -\texttt{asm_simp_tac}~/ \texttt{full_simp_tac}~/ \texttt{asm_full_simp_tac}; +variant forms by a single method with separate options to tune the behavior. +For example, method $simp$ replaces all of \texttt{simp_tac}~/ +\texttt{asm_simp_tac}~/ \texttt{full_simp_tac}~/ \texttt{asm_full_simp_tac}, there is also concrete syntax for augmenting the Simplifier context (the -current ``simpset''). +current ``simpset'') in a handsome way. \subsubsection{Resolution tactics} Classic Isabelle provides several variant forms of tactics for single-step -rule applications (based on higher-order resolution). The space of possible +rule applications (based on higher-order resolution). The space of resolution tactics has the following main dimensions. \begin{enumerate} -\item The ``mode'' of resolution: intro, elim, destruct, forward (e.g.\ +\item The ``mode'' of resolution: intro, elim, destruct, or forward (e.g.\ \texttt{resolve_tac}, \texttt{eresolve_tac}, \texttt{dresolve_tac}, \texttt{forward_tac}). -\item Optional explicit instantiation (e.g.\ \texttt{resolve_tac}, +\item Optional explicit instantiation (e.g.\ \texttt{resolve_tac} vs.\ \texttt{res_inst_tac}). -\item Abbreviations for common arguments (e.g.\ \texttt{resolve_tac}, +\item Abbreviations for singleton arguments (e.g.\ \texttt{resolve_tac} vs.\ \texttt{rtac}). \end{enumerate} @@ -231,9 +231,9 @@ use the plain $rule$ method (see \S\ref{sec:pure-meth-att}), or any of its ``improper'' variants $erule$, $drule$, $frule$ (see \S\ref{sec:misc-methods}). Note that explicit goal addressing is only -supported by $rule_tac$ versions. +supported by the actual $rule_tac$ version. -\medskip Thus plain resolution tactics may be ported to Isar as follows. +With this in mind, plain resolution tactics may be ported as follows. \begin{matharray}{lll} \texttt{rtac}~a~1 & & rule~a \\ \texttt{resolve_tac}~[a@1, \dots]~1 & & rule~a@1~\dots \\ @@ -285,7 +285,7 @@ The Classical Reasoner provides a rather large number of variations of automated tactics, such as \texttt{Blast_tac}, \texttt{Fast_tac}, \texttt{Clarify_tac} etc.\ (see \cite{isabelle-ref}). The corresponding Isar -methods usually have the same base name, such as $blast$, $fast$, $clarify$ +methods usually share the same base name, such as $blast$, $fast$, $clarify$ etc.\ (see \S\ref{sec:classical-auto}). Similar to the Simplifier, there is separate method modifier syntax for @@ -325,8 +325,8 @@ modification of existing tactics. This has been greatly reduced in Isar, providing the bare minimum of combinators only: ``$,$'' (sequential composition), ``$|$'' (alternative choices), ``$?$'' (try), ``$+$'' (repeat at -least once). Nevertheless, these are usually sufficient in practice. If all -fails, arbitrary ML tactic code may be invoked via the $tactic$ method (see +least once). These are usually sufficient in practice; if all fails, +arbitrary ML tactic code may be invoked via the $tactic$ method (see \S\ref{sec:tactics}). \medskip Common ML tacticals may be expressed directly in Isar as follows: @@ -346,12 +346,11 @@ \emph{unchanged} results as well. \medskip \texttt{ALLGOALS}, \texttt{SOMEGOAL} etc.\ (see \cite{isabelle-ref}) -are not available in Isar, since there is no direct goal addressing available. -Nevertheless, some basic methods (notably $simp_all$, see \S\ref{sec:simp}) -address all goals internally. Also note that \texttt{ALLGOALS} may be often -replaced by ``$+$'' (repeat at least once), although this usually has a -slightly different operational behavior, such as solving goals in a different -order. +are not available in Isar, since there is no direct goal addressing. +Nevertheless, some basic methods address all goals internally, notably +$simp_all$ (see \S\ref{sec:simp}). Also note that \texttt{ALLGOALS} may be +often replaced by ``$+$'' (repeat at least once), although this usually has a +different operational behavior, such as solving goals in a different order. \medskip Iterated resolution, such as \texttt{REPEAT~(FIRSTGOAL~(resolve_tac~$\dots$))}, is usually better expressed @@ -372,18 +371,19 @@ common ML combinators may be expressed directly in Isar as follows. \begin{matharray}{lll} thm@1~\texttt{RS}~thm@2 & & thm@1~[THEN~thm@2] \\ - thm@1~\texttt{RSN}~(i, thm@2) & & thm@1~[THEN~i~thm@2] \\ + thm@1~\texttt{RSN}~(i, thm@2) & & thm@1~[THEN~[i]~thm@2] \\ thm@1~\texttt{COMP}~thm@2 & & thm@1~[COMP~thm@2] \\ \relax[thm@1, \dots]~\texttt{MRS}~thm & & thm~[OF~thm@1~\dots] \\ \texttt{read_instantiate}~[(x@1, t@1), \dots]~thm & & thm~[where~x@1 = t@1~and~\dots] \\ \texttt{standard}~thm & & thm~[standard] \\ \texttt{make_elim}~thm & & thm~[elim_format] \\ \end{matharray} -Note that $OF$ is often more readable then $THEN$; likewise positional + +Note that $OF$ is often more readable as $THEN$; likewise positional instantiation with $of$ is more handsome than $where$. The special ML command \texttt{qed_spec_mp} of Isabelle/HOL and FOL may be -replaced by passing the result of a proof through the $rule_format$. +replaced by passing the result of a proof through $rule_format$. \medskip Global ML declarations may be expressed using the $\isarkeyword{declare}$ command (see \S\ref{sec:tactic-commands}) together @@ -415,29 +415,31 @@ \LEMMA{name~[simp]}{\phi} \\ \quad\vdots \end{matharray} +The $name$ may be even omitted, although this would make it difficult to +declare the theorem otherwise later (e.g.\ as $[simp~del]$). \section{Converting to actual Isar proof texts} Porting legacy ML proof scripts into Isar tactic emulation scripts (see -\S\ref{sec:port-scripts}) is mainly a purely technical issue, since the basic -representation of the formal ``proof'' has been preserved. In contrast, -converting existing Isabelle developments into actual human readably Isar +\S\ref{sec:port-scripts}) is mainly a technical issue, since the basic +representation of formal ``proof script'' is preserved. In contrast, +converting existing Isabelle developments into actual human-readably Isar proof texts is more involved, due to the fundamental change of the underlying paradigm. This issue is comparable to that of converting programs written in a low-level -programming languages (say assembly) into higher-level ones (say Haskell). In -order to accomplish this, one needs a working knowledge of the target +programming languages (say Assembler) into higher-level ones (say Haskell). +In order to accomplish this, one needs a working knowledge of the target language, as well an understanding of the \emph{original} idea of the piece of code expressed in the low-level language. As far as Isar proofs are concerned, it is usually much easier to re-use only definitions and the main statements directly, while following the arrangement of proof scripts only very loosely. Ideally, one would also have some -\emph{informal} proof outlines available as well. In the worst case, obscure -proof scripts would have to be re-engineered by tracing forth and backwards, -and by educated guessing! +\emph{informal} proof outlines available for guidance as well. In the worst +case, obscure proof scripts would have to be re-engineered by tracing forth +and backwards, and by educated guessing! \medskip This is a possible schedule to embark on actual conversion of legacy proof scripts into Isar proof texts. @@ -446,16 +448,17 @@ \S\ref{sec:port-scripts}). \item Get sufficiently acquainted with Isabelle/Isar proof development.\footnote{As there is still no Isar tutorial around, it is best - to look at existing Isar examples.} + to look at existing Isar examples, see also \S\ref{sec:isar-howto}.} \item Recover the proof structure of a few important theorems. \item Rephrase the original intention of the course of reasoning in terms of Isar proof language elements. \end{enumerate} -Certainly, rewriting formal reasoning in Isar requires additional efforts. On -the other hand, one gains a human readable representation of machine-checked -formal proof. Depending on the context of application, this might be even -indispensable to start with! +Certainly, rewriting formal reasoning in Isar requires much additional effort. +On the other hand, one gains a human-readable representation of +machine-checked formal proof. Depending on the context of application, this +might be even indispensable to start with! + %%% Local Variables: %%% mode: latex diff -r a72ddfdbfca0 -r bb8f9412fec6 doc-src/IsarRef/generic.tex --- a/doc-src/IsarRef/generic.tex Fri Oct 06 12:31:53 2000 +0200 +++ b/doc-src/IsarRef/generic.tex Fri Oct 06 14:19:48 2000 +0200 @@ -238,7 +238,7 @@ \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex] \quad \BG \\ \qquad \FIX{thesis} \\ - \qquad \ASSUME{that [simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\ + \qquad \ASSUME{that~[simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\ \qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\ \quad \EN \\ \quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\ diff -r a72ddfdbfca0 -r bb8f9412fec6 doc-src/IsarRef/intro.tex --- a/doc-src/IsarRef/intro.tex Fri Oct 06 12:31:53 2000 +0200 +++ b/doc-src/IsarRef/intro.tex Fri Oct 06 14:19:48 2000 +0200 @@ -18,7 +18,7 @@ end \end{ttbox} Note that any Isabelle/Isar command may be retracted by \texttt{undo}. See -the Isabelle/Isar Quick Reference (Appendix~\ref{ap:refcard}) for a +the Isabelle/Isar Quick Reference (appendix~\ref{ap:refcard}) for a comprehensive overview of available commands and other language elements. @@ -105,7 +105,7 @@ Using proper mathematical symbols in Isabelle theories can be very convenient for readability of large formulas. On the other hand, the plain ASCII sources -easily become somewhat unintelligible. For example, $\Longrightarrow$ will +easily become somewhat unintelligible. For example, $\Longrightarrow$ would appear as \verb,\, according the default set of Isabelle symbols. Nevertheless, the Isabelle document preparation system (see \S\ref{sec:document-prep}) will be happy to print non-ASCII symbols properly. @@ -153,9 +153,11 @@ of these may be active at the same time. \end{warn} -Porting of existing tactic scripts is best done by running two separate +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. +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} @@ -212,7 +214,7 @@ on Isabelle logic sessions and theory presentation. -\subsection{How to write Isar proofs anyway?} +\subsection{How to write Isar proofs anyway?}\label{sec:isar-howto} 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 @@ -221,16 +223,18 @@ 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} for further background information -on Isar. -%FIXME cite [HahnBanach-in-Isar] +better. See also \cite{Wenzel:1999:TPHOL,Bauer-Wenzel:2000:HB} for further +background information on Isar. -\medskip This really is a \emph{reference manual}. 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. There are several examples distributed with -Isabelle, and available via the Isabelle WWW library as well as the -Isabelle/Isar page: +\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. + +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/} \\ @@ -239,10 +243,28 @@ \end{tabular} \end{center} -See \texttt{HOL/Isar_examples} for a collection of introductory examples, and -\texttt{HOL/HOL-Real/HahnBanach} for a big mathematics application. Apart -from plain HTML sources, these sessions also provide actual documents (in -PDF). +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/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 either form of + legacy scripts, tactic emulation scripts, and proper Isar proof texts. +\end{itemize} %%% Local Variables: diff -r a72ddfdbfca0 -r bb8f9412fec6 doc-src/IsarRef/isar-ref.tex --- a/doc-src/IsarRef/isar-ref.tex Fri Oct 06 12:31:53 2000 +0200 +++ b/doc-src/IsarRef/isar-ref.tex Fri Oct 06 14:19:48 2000 +0200 @@ -1,13 +1,6 @@ %% $Id$ -% FIXME TODO -% -% - update Proof General and X-symbol installation notes; -% - update tactic emulation (including refcard); -% - proof script conversion guide; - - \documentclass[12pt,a4paper,fleqn]{report} \usepackage{latexsym,graphicx,../iman,../extra,../ttbox,../proof,../rail,../railsetup,../isar,../pdfsetup} @@ -76,15 +69,14 @@ satisfy quite contradictory requirements, being both ``declarative'' and immediately ``executable'', by virtue of the \emph{Isar/VM} interpreter. - The current version of Isabelle offers Isar as an alternative proof language - interface layer. The Isabelle/Isar system provides an interpreter for the - Isar formal proof language. The input may consist either of proper document - constructors, or improper auxiliary commands (for diagnostics, exploration - etc.). Proof texts consisting of proper elements only, admit a purely - static reading, thus being intelligible later without requiring dynamic - replay that is so typical for traditional proof scripts. Any of the - Isabelle/Isar commands may be executed in single-steps, so basically the - interpreter has a proof text debugger already built-in. + The Isabelle/Isar system provides an interpreter for the Isar formal proof + language. The input may consist either of proper document constructors, or + improper auxiliary commands (for diagnostics, exploration etc.). Proof + texts consisting of proper elements only admit a purely static reading, thus + being intelligible later without requiring dynamic replay that is so typical + for traditional proof scripts. Any of the Isabelle/Isar commands may be + executed in single-steps, so basically the interpreter has a proof text + debugger already built-in. Employing the Isar instantiation of \emph{Proof~General}, a generic Emacs interface for interactive proof assistants, we arrive at a reasonable @@ -96,9 +88,12 @@ The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic implementation. Theories, theorems, proof procedures etc.\ may be used interchangeably between classic Isabelle proof scripts and Isabelle/Isar - documents. Isar is as generic as Isabelle, able to support a wide range of - object-logics. Currently, the end-user working environment is most complete - for Isabelle/HOL. + documents. Even more, Isar provides a set of emulation commands and methods + for simulating traditional tactic scripts within new-style theory documents. + + The Isar framework is as generic as Isabelle, able to support a wide range + of object-logics. Currently, the end-user working environment is most + complete for Isabelle/HOL. \end{abstract} \pagenumbering{roman} \tableofcontents \clearfirst diff -r a72ddfdbfca0 -r bb8f9412fec6 doc-src/IsarRef/pure.tex --- a/doc-src/IsarRef/pure.tex Fri Oct 06 12:31:53 2000 +0200 +++ b/doc-src/IsarRef/pure.tex Fri Oct 06 14:19:48 2000 +0200 @@ -961,22 +961,35 @@ but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.). \end{descr} -A few \emph{automatic} term abbreviations\index{term abbreviations} for goals +Some \emph{automatic} term abbreviations\index{term abbreviations} for goals and facts are available as well. For any open goal, -$\Var{thesis_prop}$\indexisarvar{thesis-prop} refers to the full proposition -(which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its -(atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its -object-level statement. The latter two abstract over any meta-level -parameters. +$\Var{thesis}$\indexisarvar{thesis} refers to its object-level statement, +abstracted over any meta-level parameters (if present). Likewise, +$\Var{this}$\indexisarvar{this} is bound for fact statements resulting from +assumptions or finished goals. In case $\Var{this}$ refers to an object-logic +statement that is an application $f(t)$, then $t$ is bound to the special text +variable ``$\dots$''\indexisarvar{\dots} (three dots). The canonical +application of the latter are calculational proofs (see +\S\ref{sec:calculation}). + +%FIXME !? -Fact statements resulting from assumptions or finished goals are bound as -$\Var{this_prop}$\indexisarvar{this-prop}, -$\Var{this_concl}$\indexisarvar{this-concl}, and -$\Var{this}$\indexisarvar{this}, similar to $\Var{thesis}$ above. In case -$\Var{this}$ refers to an object-logic statement that is an application -$f(t)$, then $t$ is bound to the special text variable -``$\dots$''\indexisarvar{\dots} (three dots). The canonical application of -the latter are calculational proofs (see \S\ref{sec:calculation}). +% A few \emph{automatic} term abbreviations\index{term abbreviations} for goals +% and facts are available as well. For any open goal, +% $\Var{thesis_prop}$\indexisarvar{thesis-prop} refers to the full proposition +% (which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its +% (atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its +% object-level statement. The latter two abstract over any meta-level +% parameters. + +% Fact statements resulting from assumptions or finished goals are bound as +% $\Var{this_prop}$\indexisarvar{this-prop}, +% $\Var{this_concl}$\indexisarvar{this-concl}, and +% $\Var{this}$\indexisarvar{this}, similar to $\Var{thesis}$ above. In case +% $\Var{this}$ refers to an object-logic statement that is an application +% $f(t)$, then $t$ is bound to the special text variable +% ``$\dots$''\indexisarvar{\dots} (three dots). The canonical application of +% the latter are calculational proofs (see \S\ref{sec:calculation}). \subsection{Block structure} diff -r a72ddfdbfca0 -r bb8f9412fec6 doc-src/IsarRef/syntax.tex --- a/doc-src/IsarRef/syntax.tex Fri Oct 06 12:31:53 2000 +0200 +++ b/doc-src/IsarRef/syntax.tex Fri Oct 06 14:19:48 2000 +0200 @@ -66,9 +66,9 @@ digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\ quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\ sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~ %$ - \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \verb,:, ~|~ - \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~ \\ - & & \verb,^, ~|~ \verb,_, ~|~ \verb,`, ~|~ \verb,|, ~|~ \verb,~, \\ + \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \verb,:, ~|~ \\ + & & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~ + \verb,^, ~|~ \verb,_, ~|~ \verb,`, ~|~ \verb,|, ~|~ \verb,~, \\ symbol & = & {\forall} ~|~ {\exists} ~|~ \dots \end{matharray} @@ -85,6 +85,9 @@ syntax also provides \emph{formal comments} that are actually part of the text (see \S\ref{sec:comments}). +Mathematical symbols such as ``$\forall$'' are represented in plain ASCII as +``\verb,\,''. + \section{Common syntax entities} @@ -340,10 +343,14 @@ preparation system (see also \S\ref{sec:document-prep}). Thus embedding of -\texttt{{\at}{\ttlbrace}term[show_types]~"f(x)~=~a~+~x"{\ttrbrace}} within a +\texttt{{\at}{\ttlbrace}term~[show_types]~"f(x)~=~a~+~x"{\ttrbrace}} within a text block would cause \isa{(f{\isasymColon}'a~{\isasymRightarrow}~'a)~(x{\isasymColon}'a)~=~(a{\isasymColon}'a)~+~x} -to appear in the final {\LaTeX} document. +to appear in the final {\LaTeX} document. Also note that theorem +antiquotations may involve attributes as well. For example, +\texttt{{\at}{\ttlbrace}thm~sym~[no_vars]{\ttrbrace}} would print the +statement where all schematic variables have been replaced by fixed ones, +which are better readable. Antiquotations do not only spare the author from tedious typing, but also achieve some degree of consistency-checking of informal explanations with diff -r a72ddfdbfca0 -r bb8f9412fec6 doc-src/manual.bib --- a/doc-src/manual.bib Fri Oct 06 12:31:53 2000 +0200 +++ b/doc-src/manual.bib Fri Oct 06 14:19:48 2000 +0200 @@ -90,10 +90,9 @@ } @InProceedings{Aspinall:TACAS:2000, author = {David Aspinall}, - title = {Proof General: A Generic Tool for Proof Development}, + title = {{P}roof {G}eneral: A Generic Tool for Proof Development}, booktitle = {ETAPS / TACAS}, - year = 2000, - note = {To appear} + year = 2000 } @Misc{isamode,