--- 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,\<forall>,).
\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
--- 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 \\
--- 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,\<Longrightarrow>, 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:
--- 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
--- 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}
--- 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,\<forall>,''.
+
\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
--- 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,