1.1 --- a/doc-src/IsarRef/conversion.tex Fri Oct 06 12:31:53 2000 +0200
1.2 +++ b/doc-src/IsarRef/conversion.tex Fri Oct 06 14:19:48 2000 +0200
1.3 @@ -1,15 +1,15 @@
1.4
1.5 -\chapter{The Isabelle/Isar Conversion Guide}
1.6 +\chapter{Isabelle/Isar Conversion Guide}\label{ap:conv}
1.7
1.8 Subsequently, we give a few practical hints on working in a mixed environment
1.9 of old Isabelle ML proof scripts and new Isabelle/Isar theories. There are
1.10 basically three ways to cope with this issue.
1.11 \begin{enumerate}
1.12 \item Do not convert old sources at all, but communicate directly at the level
1.13 - of internal theory and theorem values.
1.14 + of \emph{internal} theory and theorem values.
1.15 \item Port old-style theory files to new-style ones (very easy), and ML proof
1.16 scripts to Isar tactic-emulation scripts (quite easy).
1.17 -\item Actually redo ML proof scripts as human readable Isar proof texts
1.18 +\item Actually redo ML proof scripts as human-readable Isar proof texts
1.19 (probably hard, depending who wrote the original scripts).
1.20 \end{enumerate}
1.21
1.22 @@ -48,8 +48,8 @@
1.23
1.24 Old-style theories often use the ML binding \texttt{thy}, which is
1.25 dynamically created by the ML code generated from old theory source. This
1.26 - is no longer the recommended way in any case! The \texttt{the_context}
1.27 - function should be used for old scripts as well.
1.28 + is no longer the recommended way in any case! Function \texttt{the_context}
1.29 + should be used for old scripts as well.
1.30
1.31 \item [$\mathtt{theory}~name$] retrieves the named theory from the global
1.32 theory-loader database.
1.33 @@ -67,7 +67,7 @@
1.34 bind_thms : string * thm list -> unit
1.35 \end{ttbox}
1.36
1.37 -ML proof scripts have to be well-behaved in storing theorems properly within
1.38 +ML proof scripts have to be well-behaved by storing theorems properly within
1.39 the current theory context, in order to enable new-style theories to retrieve
1.40 these these later.
1.41
1.42 @@ -76,14 +76,15 @@
1.43 ML. This already manages entry in the theorem database of the current
1.44 theory context.
1.45 \item [$\mathtt{bind_thm}~(name, thm)$ and $\mathtt{bind_thms}~(name, thms)$]
1.46 - store (lists of) theorems that have been produced in ML in an ad-hoc manner.
1.47 + store theorems that have been produced in ML in an ad-hoc manner.
1.48 \end{descr}
1.49
1.50 Note that the original ``LCF-system'' approach of binding theorem values on
1.51 -the ML toplevel only has long been given up in Isabelle! Legacy proof scripts
1.52 -occasionally contain code such as \texttt{val foo = result();} which is
1.53 -ill-behaved in several respects. Apart from preventing access from Isar
1.54 -theories, it also omits the result from the WWW presentation, for example.
1.55 +the ML toplevel only has long been given up in Isabelle! Despite of this, old
1.56 +legacy proof scripts occasionally contain code such as \texttt{val foo =
1.57 + result();} which is ill-behaved in several respects. Apart from preventing
1.58 +access from Isar theories, it also omits the result from the WWW presentation,
1.59 +for example.
1.60
1.61
1.62 \subsection{ML declarations in Isar}
1.63 @@ -98,8 +99,8 @@
1.64 \[
1.65 \isarkeyword{ML}~\{*~\mbox{\texttt{val foo = thm "foo"}}~*\}
1.66 \]
1.67 -This command cannot be undone; invalid theorem bindings in ML may persist.
1.68 -Also note that the current theory may not be modified; use
1.69 +Note that this command cannot be undone, so invalid theorem bindings in ML may
1.70 +persist. Also note that the current theory may not be modified; use
1.71 $\isarkeyword{ML_setup}$ for declarations that act on the current context.
1.72
1.73
1.74 @@ -142,14 +143,13 @@
1.75 identifiers $x$, numerals $1$, or symbols $\forall$ (input as
1.76 \verb,\<forall>,).
1.77 \item Theorem declarations require an explicit colon to separate the name from
1.78 - the statement (the name is usually optional). See the syntax of $\DEFS$ in
1.79 - \S\ref{sec:consts}, or $\THEOREMNAME$ in \S\ref{sec:axms-thms}), for
1.80 - example.
1.81 + the statement (the name is usually optional). Cf.\ the syntax of $\DEFS$ in
1.82 + \S\ref{sec:consts}, or $\THEOREMNAME$ in \S\ref{sec:axms-thms}.
1.83 \end{itemize}
1.84
1.85 -Also note that Isabelle/Isar error messages are usually quite explicit about
1.86 -the problem at hand. So in cases of doubt, input syntax may be just as well
1.87 -tried interactively.
1.88 +Note that Isabelle/Isar error messages are usually quite explicit about the
1.89 +problem at hand. So in cases of doubt, input syntax may be just as well tried
1.90 +out interactively.
1.91
1.92
1.93 \subsection{Goal statements}\label{sec:conv-goal}
1.94 @@ -194,33 +194,33 @@
1.95 Isar Proof methods closely resemble traditional tactics, when used in
1.96 unstructured sequences of $\isarkeyword{apply}$ commands (cf.\
1.97 \S\ref{sec:conv-goal}). Isabelle/Isar provides emulations for all major ML
1.98 -tactic of classic Isabelle, mostly for the sake of easy porting of existing
1.99 -developments --- actual Isar proof texts would demand much less diversity of
1.100 -proof methods.
1.101 +tactics of classic Isabelle --- mostly for the sake of easy porting of
1.102 +existing developments, as actual Isar proof texts would demand much less
1.103 +diversity of proof methods.
1.104
1.105 Unlike tactic expressions in ML, Isar proof methods provide proper concrete
1.106 syntax for additional arguments, options, modifiers etc. Thus a typical
1.107 method text is usually more concise than the corresponding ML tactic.
1.108 Furthermore, the Isar versions of classic Isabelle tactics often cover several
1.109 -variant forms into a single method, with separate options to tune the
1.110 -behavior. For example, method $simp$ replaces all of \texttt{simp_tac}~/
1.111 -\texttt{asm_simp_tac}~/ \texttt{full_simp_tac}~/ \texttt{asm_full_simp_tac};
1.112 +variant forms by a single method with separate options to tune the behavior.
1.113 +For example, method $simp$ replaces all of \texttt{simp_tac}~/
1.114 +\texttt{asm_simp_tac}~/ \texttt{full_simp_tac}~/ \texttt{asm_full_simp_tac},
1.115 there is also concrete syntax for augmenting the Simplifier context (the
1.116 -current ``simpset'').
1.117 +current ``simpset'') in a handsome way.
1.118
1.119
1.120 \subsubsection{Resolution tactics}
1.121
1.122 Classic Isabelle provides several variant forms of tactics for single-step
1.123 -rule applications (based on higher-order resolution). The space of possible
1.124 +rule applications (based on higher-order resolution). The space of resolution
1.125 tactics has the following main dimensions.
1.126 \begin{enumerate}
1.127 -\item The ``mode'' of resolution: intro, elim, destruct, forward (e.g.\
1.128 +\item The ``mode'' of resolution: intro, elim, destruct, or forward (e.g.\
1.129 \texttt{resolve_tac}, \texttt{eresolve_tac}, \texttt{dresolve_tac},
1.130 \texttt{forward_tac}).
1.131 -\item Optional explicit instantiation (e.g.\ \texttt{resolve_tac},
1.132 +\item Optional explicit instantiation (e.g.\ \texttt{resolve_tac} vs.\
1.133 \texttt{res_inst_tac}).
1.134 -\item Abbreviations for common arguments (e.g.\ \texttt{resolve_tac},
1.135 +\item Abbreviations for singleton arguments (e.g.\ \texttt{resolve_tac} vs.\
1.136 \texttt{rtac}).
1.137 \end{enumerate}
1.138
1.139 @@ -231,9 +231,9 @@
1.140 use the plain $rule$ method (see \S\ref{sec:pure-meth-att}), or any of its
1.141 ``improper'' variants $erule$, $drule$, $frule$ (see
1.142 \S\ref{sec:misc-methods}). Note that explicit goal addressing is only
1.143 -supported by $rule_tac$ versions.
1.144 +supported by the actual $rule_tac$ version.
1.145
1.146 -\medskip Thus plain resolution tactics may be ported to Isar as follows.
1.147 +With this in mind, plain resolution tactics may be ported as follows.
1.148 \begin{matharray}{lll}
1.149 \texttt{rtac}~a~1 & & rule~a \\
1.150 \texttt{resolve_tac}~[a@1, \dots]~1 & & rule~a@1~\dots \\
1.151 @@ -285,7 +285,7 @@
1.152 The Classical Reasoner provides a rather large number of variations of
1.153 automated tactics, such as \texttt{Blast_tac}, \texttt{Fast_tac},
1.154 \texttt{Clarify_tac} etc.\ (see \cite{isabelle-ref}). The corresponding Isar
1.155 -methods usually have the same base name, such as $blast$, $fast$, $clarify$
1.156 +methods usually share the same base name, such as $blast$, $fast$, $clarify$
1.157 etc.\ (see \S\ref{sec:classical-auto}).
1.158
1.159 Similar to the Simplifier, there is separate method modifier syntax for
1.160 @@ -325,8 +325,8 @@
1.161 modification of existing tactics. This has been greatly reduced in Isar,
1.162 providing the bare minimum of combinators only: ``$,$'' (sequential
1.163 composition), ``$|$'' (alternative choices), ``$?$'' (try), ``$+$'' (repeat at
1.164 -least once). Nevertheless, these are usually sufficient in practice. If all
1.165 -fails, arbitrary ML tactic code may be invoked via the $tactic$ method (see
1.166 +least once). These are usually sufficient in practice; if all fails,
1.167 +arbitrary ML tactic code may be invoked via the $tactic$ method (see
1.168 \S\ref{sec:tactics}).
1.169
1.170 \medskip Common ML tacticals may be expressed directly in Isar as follows:
1.171 @@ -346,12 +346,11 @@
1.172 \emph{unchanged} results as well.
1.173
1.174 \medskip \texttt{ALLGOALS}, \texttt{SOMEGOAL} etc.\ (see \cite{isabelle-ref})
1.175 -are not available in Isar, since there is no direct goal addressing available.
1.176 -Nevertheless, some basic methods (notably $simp_all$, see \S\ref{sec:simp})
1.177 -address all goals internally. Also note that \texttt{ALLGOALS} may be often
1.178 -replaced by ``$+$'' (repeat at least once), although this usually has a
1.179 -slightly different operational behavior, such as solving goals in a different
1.180 -order.
1.181 +are not available in Isar, since there is no direct goal addressing.
1.182 +Nevertheless, some basic methods address all goals internally, notably
1.183 +$simp_all$ (see \S\ref{sec:simp}). Also note that \texttt{ALLGOALS} may be
1.184 +often replaced by ``$+$'' (repeat at least once), although this usually has a
1.185 +different operational behavior, such as solving goals in a different order.
1.186
1.187 \medskip Iterated resolution, such as
1.188 \texttt{REPEAT~(FIRSTGOAL~(resolve_tac~$\dots$))}, is usually better expressed
1.189 @@ -372,18 +371,19 @@
1.190 common ML combinators may be expressed directly in Isar as follows.
1.191 \begin{matharray}{lll}
1.192 thm@1~\texttt{RS}~thm@2 & & thm@1~[THEN~thm@2] \\
1.193 - thm@1~\texttt{RSN}~(i, thm@2) & & thm@1~[THEN~i~thm@2] \\
1.194 + thm@1~\texttt{RSN}~(i, thm@2) & & thm@1~[THEN~[i]~thm@2] \\
1.195 thm@1~\texttt{COMP}~thm@2 & & thm@1~[COMP~thm@2] \\
1.196 \relax[thm@1, \dots]~\texttt{MRS}~thm & & thm~[OF~thm@1~\dots] \\
1.197 \texttt{read_instantiate}~[(x@1, t@1), \dots]~thm & & thm~[where~x@1 = t@1~and~\dots] \\
1.198 \texttt{standard}~thm & & thm~[standard] \\
1.199 \texttt{make_elim}~thm & & thm~[elim_format] \\
1.200 \end{matharray}
1.201 -Note that $OF$ is often more readable then $THEN$; likewise positional
1.202 +
1.203 +Note that $OF$ is often more readable as $THEN$; likewise positional
1.204 instantiation with $of$ is more handsome than $where$.
1.205
1.206 The special ML command \texttt{qed_spec_mp} of Isabelle/HOL and FOL may be
1.207 -replaced by passing the result of a proof through the $rule_format$.
1.208 +replaced by passing the result of a proof through $rule_format$.
1.209
1.210 \medskip Global ML declarations may be expressed using the
1.211 $\isarkeyword{declare}$ command (see \S\ref{sec:tactic-commands}) together
1.212 @@ -415,29 +415,31 @@
1.213 \LEMMA{name~[simp]}{\phi} \\
1.214 \quad\vdots
1.215 \end{matharray}
1.216 +The $name$ may be even omitted, although this would make it difficult to
1.217 +declare the theorem otherwise later (e.g.\ as $[simp~del]$).
1.218
1.219
1.220 \section{Converting to actual Isar proof texts}
1.221
1.222 Porting legacy ML proof scripts into Isar tactic emulation scripts (see
1.223 -\S\ref{sec:port-scripts}) is mainly a purely technical issue, since the basic
1.224 -representation of the formal ``proof'' has been preserved. In contrast,
1.225 -converting existing Isabelle developments into actual human readably Isar
1.226 +\S\ref{sec:port-scripts}) is mainly a technical issue, since the basic
1.227 +representation of formal ``proof script'' is preserved. In contrast,
1.228 +converting existing Isabelle developments into actual human-readably Isar
1.229 proof texts is more involved, due to the fundamental change of the underlying
1.230 paradigm.
1.231
1.232 This issue is comparable to that of converting programs written in a low-level
1.233 -programming languages (say assembly) into higher-level ones (say Haskell). In
1.234 -order to accomplish this, one needs a working knowledge of the target
1.235 +programming languages (say Assembler) into higher-level ones (say Haskell).
1.236 +In order to accomplish this, one needs a working knowledge of the target
1.237 language, as well an understanding of the \emph{original} idea of the piece of
1.238 code expressed in the low-level language.
1.239
1.240 As far as Isar proofs are concerned, it is usually much easier to re-use only
1.241 definitions and the main statements directly, while following the arrangement
1.242 of proof scripts only very loosely. Ideally, one would also have some
1.243 -\emph{informal} proof outlines available as well. In the worst case, obscure
1.244 -proof scripts would have to be re-engineered by tracing forth and backwards,
1.245 -and by educated guessing!
1.246 +\emph{informal} proof outlines available for guidance as well. In the worst
1.247 +case, obscure proof scripts would have to be re-engineered by tracing forth
1.248 +and backwards, and by educated guessing!
1.249
1.250 \medskip This is a possible schedule to embark on actual conversion of legacy
1.251 proof scripts into Isar proof texts.
1.252 @@ -446,16 +448,17 @@
1.253 \S\ref{sec:port-scripts}).
1.254 \item Get sufficiently acquainted with Isabelle/Isar proof
1.255 development.\footnote{As there is still no Isar tutorial around, it is best
1.256 - to look at existing Isar examples.}
1.257 + to look at existing Isar examples, see also \S\ref{sec:isar-howto}.}
1.258 \item Recover the proof structure of a few important theorems.
1.259 \item Rephrase the original intention of the course of reasoning in terms of
1.260 Isar proof language elements.
1.261 \end{enumerate}
1.262
1.263 -Certainly, rewriting formal reasoning in Isar requires additional efforts. On
1.264 -the other hand, one gains a human readable representation of machine-checked
1.265 -formal proof. Depending on the context of application, this might be even
1.266 -indispensable to start with!
1.267 +Certainly, rewriting formal reasoning in Isar requires much additional effort.
1.268 +On the other hand, one gains a human-readable representation of
1.269 +machine-checked formal proof. Depending on the context of application, this
1.270 +might be even indispensable to start with!
1.271 +
1.272
1.273 %%% Local Variables:
1.274 %%% mode: latex
2.1 --- a/doc-src/IsarRef/generic.tex Fri Oct 06 12:31:53 2000 +0200
2.2 +++ b/doc-src/IsarRef/generic.tex Fri Oct 06 14:19:48 2000 +0200
2.3 @@ -238,7 +238,7 @@
2.4 \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex]
2.5 \quad \BG \\
2.6 \qquad \FIX{thesis} \\
2.7 - \qquad \ASSUME{that [simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\
2.8 + \qquad \ASSUME{that~[simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\
2.9 \qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\
2.10 \quad \EN \\
2.11 \quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\
3.1 --- a/doc-src/IsarRef/intro.tex Fri Oct 06 12:31:53 2000 +0200
3.2 +++ b/doc-src/IsarRef/intro.tex Fri Oct 06 14:19:48 2000 +0200
3.3 @@ -18,7 +18,7 @@
3.4 end
3.5 \end{ttbox}
3.6 Note that any Isabelle/Isar command may be retracted by \texttt{undo}. See
3.7 -the Isabelle/Isar Quick Reference (Appendix~\ref{ap:refcard}) for a
3.8 +the Isabelle/Isar Quick Reference (appendix~\ref{ap:refcard}) for a
3.9 comprehensive overview of available commands and other language elements.
3.10
3.11
3.12 @@ -105,7 +105,7 @@
3.13
3.14 Using proper mathematical symbols in Isabelle theories can be very convenient
3.15 for readability of large formulas. On the other hand, the plain ASCII sources
3.16 -easily become somewhat unintelligible. For example, $\Longrightarrow$ will
3.17 +easily become somewhat unintelligible. For example, $\Longrightarrow$ would
3.18 appear as \verb,\<Longrightarrow>, according the default set of Isabelle
3.19 symbols. Nevertheless, the Isabelle document preparation system (see
3.20 \S\ref{sec:document-prep}) will be happy to print non-ASCII symbols properly.
3.21 @@ -153,9 +153,11 @@
3.22 of these may be active at the same time.
3.23 \end{warn}
3.24
3.25 -Porting of existing tactic scripts is best done by running two separate
3.26 +Conversion of existing tactic scripts is best done by running two separate
3.27 Proof~General sessions, one for replaying the old script and the other for the
3.28 -emerging Isabelle/Isar document.
3.29 +emerging Isabelle/Isar document. Also note that Isar supports emulation
3.30 +commands and methods that support traditional tactic scripts within new-style
3.31 +theories, see appendix~\ref{ap:conv} for more information.
3.32
3.33
3.34 \subsection{Document preparation}\label{sec:document-prep}
3.35 @@ -212,7 +214,7 @@
3.36 on Isabelle logic sessions and theory presentation.
3.37
3.38
3.39 -\subsection{How to write Isar proofs anyway?}
3.40 +\subsection{How to write Isar proofs anyway?}\label{sec:isar-howto}
3.41
3.42 This is one of the key questions, of course. Isar offers a rather different
3.43 approach to formal proof documents than plain old tactic scripts. Experienced
3.44 @@ -221,16 +223,18 @@
3.45 other hand, Isabelle/Isar comes much closer to existing mathematical practice
3.46 of formal proof, so users with less experience in old-style tactical proving,
3.47 but a good understanding of mathematical proof, might cope with Isar even
3.48 -better. See also \cite{Wenzel:1999:TPHOL} for further background information
3.49 -on Isar.
3.50 -%FIXME cite [HahnBanach-in-Isar]
3.51 +better. See also \cite{Wenzel:1999:TPHOL,Bauer-Wenzel:2000:HB} for further
3.52 +background information on Isar.
3.53
3.54 -\medskip This really is a \emph{reference manual}. Nevertheless, we will also
3.55 -give some clues of how the concepts introduced here may be put into practice.
3.56 -Appendix~\ref{ap:refcard} provides a quick reference card of the most common
3.57 -Isabelle/Isar language elements. There are several examples distributed with
3.58 -Isabelle, and available via the Isabelle WWW library as well as the
3.59 -Isabelle/Isar page:
3.60 +\medskip This really is a reference manual on Isabelle/Isar, not a tutorial.
3.61 +Nevertheless, we will also give some clues of how the concepts introduced here
3.62 +may be put into practice. Appendix~\ref{ap:refcard} provides a quick
3.63 +reference card of the most common Isabelle/Isar language elements.
3.64 +Appendix~\ref{ap:conv} offers some practical hints on converting existing
3.65 +Isabelle theories and proof scripts to the new format.
3.66 +
3.67 +Several example applications are distributed with Isabelle, and available via
3.68 +the Isabelle WWW library as well as the Isabelle/Isar page:
3.69 \begin{center}\small
3.70 \begin{tabular}{l}
3.71 \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
3.72 @@ -239,10 +243,28 @@
3.73 \end{tabular}
3.74 \end{center}
3.75
3.76 -See \texttt{HOL/Isar_examples} for a collection of introductory examples, and
3.77 -\texttt{HOL/HOL-Real/HahnBanach} for a big mathematics application. Apart
3.78 -from plain HTML sources, these sessions also provide actual documents (in
3.79 -PDF).
3.80 +The following examples may be of particular interest. Apart from the plain
3.81 +sources represented in HTML, these Isabelle sessions also provide actual
3.82 +documents (in PDF).
3.83 +\begin{itemize}
3.84 +\item \url{http://isabelle.in.tum.de/library/HOL/Isar_examples/} is a
3.85 + collection of introductory examples.
3.86 +\item \url{http://isabelle.in.tum.de/library/HOL/Lattice/} is an example of
3.87 + typical mathematics-style reasoning in ``axiomatic'' structures.
3.88 +\item \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/HahnBanach/} is a
3.89 + big mathematics application on infinitary vector spaces and functional
3.90 + analysis.
3.91 +\item \url{http://isabelle.in.tum.de/library/HOL/Lambda/} develops fundamental
3.92 + properties of $\lambda$-calculus (Church-Rosser and termination). This may
3.93 + serve as a realistic example of porting of legacy proof scripts into Isar
3.94 + tactic emulation scripts.
3.95 +\item \url{http://isabelle.in.tum.de/library/HOL/MicroJava/} is a
3.96 + formalization of a fragment of Java, together with a corresponding virtual
3.97 + machine and a specification of its bytecode verifier and a lightweight
3.98 + bytecode verifier, including proofs of type-safety. This represents a very
3.99 + ``realistic'' example of large formalizations performed in either form of
3.100 + legacy scripts, tactic emulation scripts, and proper Isar proof texts.
3.101 +\end{itemize}
3.102
3.103
3.104 %%% Local Variables:
4.1 --- a/doc-src/IsarRef/isar-ref.tex Fri Oct 06 12:31:53 2000 +0200
4.2 +++ b/doc-src/IsarRef/isar-ref.tex Fri Oct 06 14:19:48 2000 +0200
4.3 @@ -1,13 +1,6 @@
4.4
4.5 %% $Id$
4.6
4.7 -% FIXME TODO
4.8 -%
4.9 -% - update Proof General and X-symbol installation notes;
4.10 -% - update tactic emulation (including refcard);
4.11 -% - proof script conversion guide;
4.12 -
4.13 -
4.14 \documentclass[12pt,a4paper,fleqn]{report}
4.15 \usepackage{latexsym,graphicx,../iman,../extra,../ttbox,../proof,../rail,../railsetup,../isar,../pdfsetup}
4.16
4.17 @@ -76,15 +69,14 @@
4.18 satisfy quite contradictory requirements, being both ``declarative'' and
4.19 immediately ``executable'', by virtue of the \emph{Isar/VM} interpreter.
4.20
4.21 - The current version of Isabelle offers Isar as an alternative proof language
4.22 - interface layer. The Isabelle/Isar system provides an interpreter for the
4.23 - Isar formal proof language. The input may consist either of proper document
4.24 - constructors, or improper auxiliary commands (for diagnostics, exploration
4.25 - etc.). Proof texts consisting of proper elements only, admit a purely
4.26 - static reading, thus being intelligible later without requiring dynamic
4.27 - replay that is so typical for traditional proof scripts. Any of the
4.28 - Isabelle/Isar commands may be executed in single-steps, so basically the
4.29 - interpreter has a proof text debugger already built-in.
4.30 + The Isabelle/Isar system provides an interpreter for the Isar formal proof
4.31 + language. The input may consist either of proper document constructors, or
4.32 + improper auxiliary commands (for diagnostics, exploration etc.). Proof
4.33 + texts consisting of proper elements only admit a purely static reading, thus
4.34 + being intelligible later without requiring dynamic replay that is so typical
4.35 + for traditional proof scripts. Any of the Isabelle/Isar commands may be
4.36 + executed in single-steps, so basically the interpreter has a proof text
4.37 + debugger already built-in.
4.38
4.39 Employing the Isar instantiation of \emph{Proof~General}, a generic Emacs
4.40 interface for interactive proof assistants, we arrive at a reasonable
4.41 @@ -96,9 +88,12 @@
4.42 The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic
4.43 implementation. Theories, theorems, proof procedures etc.\ may be used
4.44 interchangeably between classic Isabelle proof scripts and Isabelle/Isar
4.45 - documents. Isar is as generic as Isabelle, able to support a wide range of
4.46 - object-logics. Currently, the end-user working environment is most complete
4.47 - for Isabelle/HOL.
4.48 + documents. Even more, Isar provides a set of emulation commands and methods
4.49 + for simulating traditional tactic scripts within new-style theory documents.
4.50 +
4.51 + The Isar framework is as generic as Isabelle, able to support a wide range
4.52 + of object-logics. Currently, the end-user working environment is most
4.53 + complete for Isabelle/HOL.
4.54 \end{abstract}
4.55
4.56 \pagenumbering{roman} \tableofcontents \clearfirst
5.1 --- a/doc-src/IsarRef/pure.tex Fri Oct 06 12:31:53 2000 +0200
5.2 +++ b/doc-src/IsarRef/pure.tex Fri Oct 06 14:19:48 2000 +0200
5.3 @@ -961,22 +961,35 @@
5.4 but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.).
5.5 \end{descr}
5.6
5.7 -A few \emph{automatic} term abbreviations\index{term abbreviations} for goals
5.8 +Some \emph{automatic} term abbreviations\index{term abbreviations} for goals
5.9 and facts are available as well. For any open goal,
5.10 -$\Var{thesis_prop}$\indexisarvar{thesis-prop} refers to the full proposition
5.11 -(which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its
5.12 -(atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its
5.13 -object-level statement. The latter two abstract over any meta-level
5.14 -parameters.
5.15 +$\Var{thesis}$\indexisarvar{thesis} refers to its object-level statement,
5.16 +abstracted over any meta-level parameters (if present). Likewise,
5.17 +$\Var{this}$\indexisarvar{this} is bound for fact statements resulting from
5.18 +assumptions or finished goals. In case $\Var{this}$ refers to an object-logic
5.19 +statement that is an application $f(t)$, then $t$ is bound to the special text
5.20 +variable ``$\dots$''\indexisarvar{\dots} (three dots). The canonical
5.21 +application of the latter are calculational proofs (see
5.22 +\S\ref{sec:calculation}).
5.23
5.24 -Fact statements resulting from assumptions or finished goals are bound as
5.25 -$\Var{this_prop}$\indexisarvar{this-prop},
5.26 -$\Var{this_concl}$\indexisarvar{this-concl}, and
5.27 -$\Var{this}$\indexisarvar{this}, similar to $\Var{thesis}$ above. In case
5.28 -$\Var{this}$ refers to an object-logic statement that is an application
5.29 -$f(t)$, then $t$ is bound to the special text variable
5.30 -``$\dots$''\indexisarvar{\dots} (three dots). The canonical application of
5.31 -the latter are calculational proofs (see \S\ref{sec:calculation}).
5.32 +%FIXME !?
5.33 +
5.34 +% A few \emph{automatic} term abbreviations\index{term abbreviations} for goals
5.35 +% and facts are available as well. For any open goal,
5.36 +% $\Var{thesis_prop}$\indexisarvar{thesis-prop} refers to the full proposition
5.37 +% (which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its
5.38 +% (atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its
5.39 +% object-level statement. The latter two abstract over any meta-level
5.40 +% parameters.
5.41 +
5.42 +% Fact statements resulting from assumptions or finished goals are bound as
5.43 +% $\Var{this_prop}$\indexisarvar{this-prop},
5.44 +% $\Var{this_concl}$\indexisarvar{this-concl}, and
5.45 +% $\Var{this}$\indexisarvar{this}, similar to $\Var{thesis}$ above. In case
5.46 +% $\Var{this}$ refers to an object-logic statement that is an application
5.47 +% $f(t)$, then $t$ is bound to the special text variable
5.48 +% ``$\dots$''\indexisarvar{\dots} (three dots). The canonical application of
5.49 +% the latter are calculational proofs (see \S\ref{sec:calculation}).
5.50
5.51
5.52 \subsection{Block structure}
6.1 --- a/doc-src/IsarRef/syntax.tex Fri Oct 06 12:31:53 2000 +0200
6.2 +++ b/doc-src/IsarRef/syntax.tex Fri Oct 06 14:19:48 2000 +0200
6.3 @@ -66,9 +66,9 @@
6.4 digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
6.5 quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
6.6 sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~ %$
6.7 - \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \verb,:, ~|~
6.8 - \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~ \\
6.9 - & & \verb,^, ~|~ \verb,_, ~|~ \verb,`, ~|~ \verb,|, ~|~ \verb,~, \\
6.10 + \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \verb,:, ~|~ \\
6.11 + & & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~
6.12 + \verb,^, ~|~ \verb,_, ~|~ \verb,`, ~|~ \verb,|, ~|~ \verb,~, \\
6.13 symbol & = & {\forall} ~|~ {\exists} ~|~ \dots
6.14 \end{matharray}
6.15
6.16 @@ -85,6 +85,9 @@
6.17 syntax also provides \emph{formal comments} that are actually part of the text
6.18 (see \S\ref{sec:comments}).
6.19
6.20 +Mathematical symbols such as ``$\forall$'' are represented in plain ASCII as
6.21 +``\verb,\<forall>,''.
6.22 +
6.23
6.24 \section{Common syntax entities}
6.25
6.26 @@ -340,10 +343,14 @@
6.27 preparation system (see also \S\ref{sec:document-prep}).
6.28
6.29 Thus embedding of
6.30 -\texttt{{\at}{\ttlbrace}term[show_types]~"f(x)~=~a~+~x"{\ttrbrace}} within a
6.31 +\texttt{{\at}{\ttlbrace}term~[show_types]~"f(x)~=~a~+~x"{\ttrbrace}} within a
6.32 text block would cause
6.33 \isa{(f{\isasymColon}'a~{\isasymRightarrow}~'a)~(x{\isasymColon}'a)~=~(a{\isasymColon}'a)~+~x}
6.34 -to appear in the final {\LaTeX} document.
6.35 +to appear in the final {\LaTeX} document. Also note that theorem
6.36 +antiquotations may involve attributes as well. For example,
6.37 +\texttt{{\at}{\ttlbrace}thm~sym~[no_vars]{\ttrbrace}} would print the
6.38 +statement where all schematic variables have been replaced by fixed ones,
6.39 +which are better readable.
6.40
6.41 Antiquotations do not only spare the author from tedious typing, but also
6.42 achieve some degree of consistency-checking of informal explanations with
7.1 --- a/doc-src/manual.bib Fri Oct 06 12:31:53 2000 +0200
7.2 +++ b/doc-src/manual.bib Fri Oct 06 14:19:48 2000 +0200
7.3 @@ -90,10 +90,9 @@
7.4 }
7.5 @InProceedings{Aspinall:TACAS:2000,
7.6 author = {David Aspinall},
7.7 - title = {Proof General: A Generic Tool for Proof Development},
7.8 + title = {{P}roof {G}eneral: A Generic Tool for Proof Development},
7.9 booktitle = {ETAPS / TACAS},
7.10 - year = 2000,
7.11 - note = {To appear}
7.12 + year = 2000
7.13 }
7.14
7.15 @Misc{isamode,