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