--- a/doc-src/IsarRef/conversion.tex Wed Oct 04 21:05:10 2000 +0200
+++ b/doc-src/IsarRef/conversion.tex Wed Oct 04 21:05:42 2000 +0200
@@ -2,13 +2,13 @@
\chapter{The Isabelle/Isar Conversion Guide}
Subsequently, we give a few practical hints on working in a mixed environment
-with old Isabelle ML proof scripts and new Isabelle/Isar theories. There are
+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.
-\item Manually port old-style theory files to new-style ones (very easy), and
- ML proof scripts to Isar tactic emulation scripts (quite easy).
+\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
(probably hard, depending who wrote the original scripts).
\end{enumerate}
@@ -16,11 +16,12 @@
\section{No conversion}
-Internally, Isabelle handles both old and new-style theories at the same time;
-the theory loader automatically detects the input format. In any case, this
-results in certain internal ML values of type \texttt{theory} and
-\texttt{thm}. These may be accessed from either the classic or Isar version,
-provided that some minimal care is taken.
+Internally, Isabelle is able to handle both old and new-style theories at the
+same time; the theory loader automatically detects the input format. In any
+case, the results are certain internal ML values of type \texttt{theory} and
+\texttt{thm}. These may be accessed from either classic Isabelle or
+Isabelle/Isar, provided that some minimal precautions are observed.
+
\subsection{Referring to theorem and theory values}
@@ -31,34 +32,34 @@
theory : string -> theory
\end{ttbox}
-These above functions provide general means to refer to logical objects from
-ML. While old-style theories used to emit many ML bindings to theorems (and
-theories), this is no longer done for new-style Isabelle/Isar theories.
-Nevertheless, it is often more appropriate to use these explicit functions in
-any case, even if referring to old theories.
+These functions provide general means to refer to logical objects from ML.
+Old-style theories used to emit many ML bindings of theorems and theories, but
+this is no longer done in new-style Isabelle/Isar theories.
\begin{descr}
\item [$\mathtt{thm}~name$ and $\mathtt{thms}~name$] retrieve theorems stored
in the current theory context, including any ancestor node.
The convention of old-style theories was to bind any theorem as an ML value
- as well. New-style theories no longer do this, so ML code may have to use
+ as well. New-style theories no longer do this, so ML code may require
\texttt{thm~"foo"} rather than just \texttt{foo}.
\item [$\mathtt{the_context()}$] refers to the current theory context.
Old-style theories often use the ML binding \texttt{thy}, which is
- dynamically created as part of producing ML code out of the theory source.
+ 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.
\item [$\mathtt{theory}~name$] retrieves the named theory from the global
- theory loader database.
+ theory-loader database.
- The ML code generated from old style theories would include an ML binding
+ The ML code generated from old-style theories would include an ML binding
$name\mathtt{.thy}$ as part of an ML structure.
\end{descr}
-\subsection{Enabling new-style theories to retrieve theory values}
+\subsection{Storing theorem values}
\begin{ttbox}
qed : string -> unit
@@ -75,169 +76,386 @@
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 theorems that are produced in ML in an ad-hoc manner.
-
- Note that the original ``LCF'' system approach of binding theorem values on
- the ML toplevel only has long been given up in Isabelle. Nevertheless,
- legacy proof scripts may occasionally contain ill-behaved code like this:
- \texttt{val foo = result();} So far, this form did not give any immediate
- feedback that there is something wrong, apart from theorems missing in the
- WWW presentation, for example. Now it prevents such theorems to be referred
- from new-style theories.
+ store (lists of) 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.
-\subsection{Providing legacy ML bindings}
+
+\subsection{ML declarations in Isar}
\begin{matharray}{rcl}
\isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
+ \isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\
\end{matharray}
-New-style theories may provide ML bindings to accommodate legacy ML scripts as
-follows.
+Isabelle/Isar theories may contain ML declarations as well. For example, an
+old-style theorem binding may be mimicked as follows.
\[
\isarkeyword{ML}~\{*~\mbox{\texttt{val foo = thm "foo"}}~*\}
\]
-Note that this command cannot be undone; invalid theorem bindings in ML may
-persist.
-
-By providing an old-style ML binding in the way that legacy proof scripts
-usually expect, one may avoid to change all occurrences of a \texttt{foo}
-reference into \texttt{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
+$\isarkeyword{ML_setup}$ for declarations that act on the current context.
-\section{Porting proof scripts}
+\section{Porting theories and proof scripts}\label{sec:port-scripts}
Porting legacy theory and ML files to proper Isabelle/Isar theories has
several advantages. For example, the Proof~General user interface
-\cite{proofgeneral} for Isabelle/Isar is more robust and more comfortable than
-the classic Isabelle version. This is due to the fact that the generic ML
-toplevel has been replaced by the new Isar interaction loop, with full control
-over input synchronization and errors.
+\cite{proofgeneral} for Isabelle/Isar is more robust and more comfortable to
+use than the version for classic Isabelle. This is due to the fact that the
+generic ML toplevel has been replaced by a separate Isar interaction loop,
+with full control over input synchronization and error conditions.
-Furthermore, the Isabelle document preparation system only properly with
-new-style theories (see also \cite{isabelle-system}). There is only very
-basic document output of the plain sources of legacy theories, lacking
-theorems and proof scripts. Proper document markup is only available for
-Isabelle/Isar theories.
+Furthermore, the Isabelle document preparation system (see also
+\cite{isabelle-sys}) only works properly with new-style theories. Output of
+old-style sources is at the level of individual characters (and symbols),
+without proper document markup as in Isabelle/Isar theories.
-\subsection{Theory syntax}
+\subsection{Theories}
+
+Basically, the Isabelle/Isar theory syntax is a proper superset of the classic
+one. Only a few quirks and legacy problems have been eliminated, resulting in
+simpler rules and less special cases. The main changes of theory syntax are
+as follows.
-Basically, the new-style Isabelle/Isar theory syntax is a proper superset of
-the old one. Only a few quirks and legacy problems have been eliminated,
-resulting in simpler rules with less exceptions.
-
-\medskip The main differences in the new syntax are as follows.
\begin{itemize}
+\item Quoted strings may contain arbitrary white space, and span several lines
+ without requiring \verb,\,\,\dots\verb,\, escapes.
+\item Names may always be quoted.
+
+ The old syntax would occasionally demand plain identifiers vs.\ quoted
+ strings to accommodate certain syntactic features.
\item Types and terms have to be \emph{atomic} as far as the theory syntax is
- concerned; this usually requires proper quoting of input strings.
+ concerned; this typically requires quoting of input strings, e.g.\ ``$x +
+ y$''.
The old theory syntax used to fake part of the syntax of types in order to
- require less quoting. This has caused too many strange effects and is no
- longer supported.
-
- Note that quotes are \emph{not} required for simple atomic terms, such as
- plain identifiers (e.g.\ $x$), numerals (e.g.\ $1$), or non-ASCII symbols
- (e.g.\ $\forall$, which is input as \verb,\<forall>,).
-\item Every name may be quoted, if required. The old syntax would
- occasionally demand plain identifiers vs.\ quoted strings to accommodate
- certain (discontinued) syntactic features.
-\item Theorem declarations now require an explicit colon to separate the name
- and the statement (e.g.\ see the syntax of $\DEFS$ in \S\ref{sec:consts}, or
- $\THEOREMNAME$ in \S\ref{sec:axms-thms}).
+ require less quoting in common cases; this was hard to predict, though. On
+ the other hand, Isar does not require quotes for simple terms, such as plain
+ 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.
\end{itemize}
-Isabelle/Isar error messages are usually quite explicit about the problem, so
-doubtful cases of syntax may as well just tried interactively.
+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.
-\subsection{Basic goal statements}\label{sec:conv-goal}
-
-In ML scripts, the canonical a goal statement with completed proof script is
-as follows.
-\begin{ttbox}
-Goal "\(\phi\)";
- by \(tac@1\);
- \(\vdots\);
- by \(tac@n\);
-qed "\(name\)";
-\end{ttbox}
+\subsection{Goal statements}\label{sec:conv-goal}
-This form may be turned into an Isar tactic emulation script like this:
+In ML the canonical a goal statement together with a complete proof script is
+as follows:
+\begin{ttbox}
+ Goal "\(\phi\)";
+ by \(tac@1\);
+ \(\vdots\)
+ qed "\(name\)";
+\end{ttbox}
+This form may be turned into an Isar tactic-emulation script like this:
\begin{matharray}{l}
-\LEMMA{name}\texttt"{\phi}\texttt" \\
-\quad \isarkeyword{apply}~meth@1 \\
-\quad \vdots \\
-\quad \isarkeyword{apply}~meth@n \\
-\quad \isarkeyword{done} \\
+ \LEMMA{name}\texttt"{\phi}\texttt" \\
+ \quad \isarkeyword{apply}~meth@1 \\
+ \qquad \vdots \\
+ \quad \isarkeyword{done} \\
\end{matharray}
-
-The main statement may be $\THEOREMNAME$ as well. See \S\ref{sec:conv-tac}
-for further details on how to convert actual tactic expressions into proof
-methods.
+Note that the main statement may be $\THEOREMNAME$ as well. See
+\S\ref{sec:conv-tac} for further details on how to convert actual tactic
+expressions into proof methods.
\medskip Classic Isabelle provides many variant forms of goal commands, see
\cite{isabelle-ref} for further details. The second most common one is
\texttt{Goalw}, which expands definitions before commencing the actual proof
script.
\begin{ttbox}
-Goalw [defs] "\(\phi\)";
- \(\vdots\)
+ Goalw [\(def@1\), \(\dots\)] "\(\phi\)";
\end{ttbox}
-This may be replaced by an explicit invocation of the $unfold$ proof method.
+This is replaced by using the $unfold$ proof method explicitly.
\begin{matharray}{l}
\LEMMA{name}\texttt"{\phi}\texttt" \\
-\quad \isarkeyword{apply}~(unfold~defs) \\
-\quad \vdots \\
+\quad \isarkeyword{apply}~(unfold~def@1~\dots) \\
\end{matharray}
%FIXME "goal" and higher-order rules;
-\subsection{Tactics vs.\ proof methods}\label{sec:conv-tac}
+\subsection{Tactics}\label{sec:conv-tac}
+
+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.
+
+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};
+there is also concrete syntax for augmenting the Simplifier context (the
+current ``simpset'').
+
+
+\subsubsection{Resolution tactics}
-Proof methods closely resemble traditional tactics, when used in unstructured
-sequences of $\isarkeyword{apply}$ commands (cf.\ \S\ref{sec:conv-goal}).
-Unlike tactics, proof methods provide proper concrete syntax for additional
-arguments, options, and modifiers. Thus a typical method text is usually more
-concise than the corresponding tactic expression in ML.
+Classic Isabelle provides several variant forms of tactics for single-step
+rule applications (based on higher-order resolution). The space of possible
+tactics has the following main dimensions.
+\begin{enumerate}
+\item The ``mode'' of resolution: intro, elim, destruct, forward (e.g.\
+ \texttt{resolve_tac}, \texttt{eresolve_tac}, \texttt{dresolve_tac},
+ \texttt{forward_tac}).
+\item Optional explicit instantiation (e.g.\ \texttt{resolve_tac},
+ \texttt{res_inst_tac}).
+\item Abbreviations for common arguments (e.g.\ \texttt{resolve_tac},
+ \texttt{rtac}).
+\end{enumerate}
+
+Basically, the set of Isar tactic emulations $rule_tac$, $erule_tac$,
+$drule_tac$, $frule_tac$ (see \S\ref{sec:tactics}) would be sufficient to
+cover the four modes, either with or without instantiation, and either with
+single or multiple arguments. Although it is more convenient in most cases to
+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.
+
+\medskip Thus plain resolution tactics may be ported to Isar as follows.
+\begin{matharray}{lll}
+ \texttt{rtac}~a~1 & & rule~a \\
+ \texttt{resolve_tac}~[a@1, \dots]~1 & & rule~a@1~\dots \\
+ \texttt{res_inst_tac}~[(x@1, t@1), \dots]~a~1 & &
+ rule_tac~x@1 = t@1~and~\dots~in~a \\[0.5ex]
+ \texttt{rtac}~a~i & & rule_tac~[i]~a \\
+ \texttt{resolve_tac}~[a@1, \dots]~i & & rule_tac~[i]~a@1~\dots \\
+ \texttt{res_inst_tac}~[(x@1, t@1), \dots]~a~i & &
+ rule_tac~[i]~x@1 = t@1~and~\dots~in~a \\
+\end{matharray}
+
+Note that explicit goal addressing may be usually avoided by changing the
+order of subgoals with $\isarkeyword{defer}$ or $\isarkeyword{prefer}$ (see
+\S\ref{sec:tactic-commands}).
+
+
+\subsubsection{Simplifier tactics}
-Well-structured Isar proof texts usually demand much less diverse methods than
-traditional proof scripts, so basically a few methods would be sufficient.
-Isabelle/Isar provides emulations for any major ML tactic of classic Isabelle,
-mostly for the sake of easy porting of existing developments. Nevertheless,
-the Isar versions often cover several old-style tactics by a single method.
-For example, $simp$ replaces all of \texttt{simp_tac}~/
-\texttt{asm_simp_tac}~/ \texttt{full_simp_tac}~/ \texttt{asm_full_simp_tac},
-including concrete syntax for augmenting the Simplifier context (the current
-``simpset'').
+The main Simplifier tactics \texttt{Simp_tac}, \texttt{simp_tac} and variants
+(cf.\ \cite{isabelle-ref}) are all covered by the $simp$ and $simp_all$
+methods (see \S\ref{sec:simp}). Note that there is no individual goal
+addressing available, simplification acts either on the first goal ($simp$)
+or all goals ($simp_all$).
+
+\begin{matharray}{lll}
+ \texttt{Asm_full_simp_tac 1} & & simp \\
+ \texttt{ALLGOALS Asm_full_simp_tac} & & simp_all \\[0.5ex]
+ \texttt{Simp_tac 1} & & simp~(no_asm) \\
+ \texttt{Asm_simp_tac 1} & & simp~(no_asm_simp) \\
+ \texttt{Full_simp_tac 1} & & simp~(no_asm_use) \\
+\end{matharray}
-\bigskip
+Isar also provides separate method modifier syntax for augmenting the
+Simplifier context (see \S\ref{sec:simp}), which is known as the ``simpset''
+in ML. A typical ML expression with simpset changes looks like this:
+\begin{ttbox}
+asm_full_simp_tac (simpset () addsimps [\(a@1\), \(\dots\)] delsimps [\(b@1\), \(\dots\)]) 1
+\end{ttbox}
+The corresponding Isar text is as follows:
+\[
+simp~add:~a@1~\dots~del:~b@1~\dots
+\]
+Global declarations of Simplifier rules (e.g.\ \texttt{Addsimps}) are covered
+by application of attributes, see \S\ref{sec:conv-decls} for more information.
+
+
+\subsubsection{Classical Reasoner tactics}
-FIXME
+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$
+etc.\ (see \S\ref{sec:classical-auto}).
-\begin{matharray}{llll}
- \texttt{rtac}~a~1 & & rule~a \\
- \texttt{resolve_tac}~[a@1, \dots, a@n]~1 & & rule~a@1~\dots~a@n \\
- \texttt{res_inst_tac}~[(x@1, t@1), \dots, (x@n, t@n)]~a~1 & &
- rule_tac~x@1 = t@1~\dots~x@n = t@n~\textrm{in}~a \\
-
-% \texttt{} & & \\
+Similar to the Simplifier, there is separate method modifier syntax for
+augmenting the Classical Reasoner context, which is known as the ``claset'' in
+ML. A typical ML expression with claset changes looks like this:
+\begin{ttbox}
+blast_tac (claset () addIs [\(a@1\), \(\dots\)] addSEs [\(b@1\), \(\dots\)]) 1
+\end{ttbox}
+The corresponding Isar text is as follows:
+\[
+blast~intro:~a@1~\dots~elim!:~b@1~\dots
+\]
+Global declarations of Classical Reasoner rules (e.g.\ \texttt{AddIs}) are
+covered by application of attributes, see \S\ref{sec:conv-decls} for more
+information.
+
+
+\subsubsection{Miscellaneous tactics}
+
+There are a few additional tactics defined in various theories of
+Isabelle/HOL, some of these also in Isabelle/FOL or Isabelle/ZF. The most
+common ones of these may be ported to Isar as follows.
+
+\begin{matharray}{lll}
\texttt{stac}~a~1 & & subst~a \\
- \texttt{strip_tac}~1 & & intro~strip & \Text{(HOL)} \\
- \texttt{split_all_tac} & & simp~(no_asm_simp)~only:~split_tupled_all & \Text{(HOL)} \\
- & \approx & simp~only:~split_tupled_all & \Text{(HOL)} \\
- & \ll & clarify & \Text{(HOL)} \\
+ \texttt{hyp_subst_tac}~1 & & hypsubst \\
+ \texttt{strip_tac}~1 & \approx & intro~strip \\
+ \texttt{split_all_tac}~1 & & simp~(no_asm_simp)~only:~split_tupled_all \\
+ & \approx & simp~only:~split_tupled_all \\
+ & \ll & clarify \\
\end{matharray}
-\subsection{Declarations and ad-hoc operations}
+\subsubsection{Tacticals}
+
+Classic Isabelle provides a huge amount of tacticals for combination and
+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
+\S\ref{sec:tactics}).
+
+\medskip Common ML tacticals may be expressed directly in Isar as follows:
+\begin{matharray}{lll}
+tac@1~\texttt{THEN}~tac@2 & & meth@1, meth@2 \\
+tac@1~\texttt{ORELSE}~tac@2 & & meth@1~|~meth@2 \\
+\texttt{TRY}~tac & & meth? \\
+\texttt{REPEAT1}~tac & & meth+ \\
+\texttt{REPEAT}~tac & & (meth+)? \\
+\texttt{EVERY}~[tac@1, \dots] & & meth@1, \dots \\
+\texttt{FIRST}~[tac@1, \dots] & & meth@1~|~\dots \\
+\end{matharray}
+
+\medskip \texttt{CHANGED} (see \cite{isabelle-ref}) is usually not required in
+Isar, since most basic proof methods already fail unless there is an actual
+change in the goal state. Nevertheless, ``$?$'' (try) may be used to accept
+\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.
+
+\medskip Iterated resolution, such as
+\texttt{REPEAT~(FIRSTGOAL~(resolve_tac~$\dots$))}, is usually better expressed
+using the $intro$ and $elim$ methods of Isar (see
+\S\ref{sec:classical-basic}).
+\subsection{Declarations and ad-hoc operations}\label{sec:conv-decls}
-%\section{Performing actual proof}
-%FIXME
+Apart from proof commands and tactic expressions, almost all of the remaining
+ML code occurring in legacy proof scripts are either global context
+declarations (such as \texttt{Addsimps}) or ad-hoc operations on theorems
+(such as \texttt{RS}). In Isar both of these are covered by theorem
+expressions with \emph{attributes}.
+
+\medskip Theorem operations may be attached as attributes in the very place
+where theorems are referenced, say within a method argument. The subsequent
+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{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
+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$.
+
+\medskip Global ML declarations may be expressed using the
+$\isarkeyword{declare}$ command (see \S\ref{sec:tactic-commands}) together
+with appropriate attributes. The most common ones are as follows.
+\begin{matharray}{lll}
+ \texttt{Addsimps}~[thm] & & \isarkeyword{declare}~thm~[simp] \\
+ \texttt{Delsimps}~[thm] & & \isarkeyword{declare}~thm~[simp~del] \\
+ \texttt{Addsplits}~[thm] & & \isarkeyword{declare}~thm~[split] \\
+ \texttt{Delsplits}~[thm] & & \isarkeyword{declare}~thm~[split~del] \\[0.5ex]
+ \texttt{AddIs}~[thm] & & \isarkeyword{declare}~thm~[intro] \\
+ \texttt{AddEs}~[thm] & & \isarkeyword{declare}~thm~[elim] \\
+ \texttt{AddDs}~[thm] & & \isarkeyword{declare}~thm~[dest] \\
+ \texttt{AddSIs}~[thm] & & \isarkeyword{declare}~thm~[intro!] \\
+ \texttt{AddSEs}~[thm] & & \isarkeyword{declare}~thm~[elim!] \\
+ \texttt{AddSDs}~[thm] & & \isarkeyword{declare}~thm~[dest!] \\[0.5ex]
+ \texttt{AddIffs}~[thm] & & \isarkeyword{declare}~thm~[iff] \\
+\end{matharray}
+Note that explicit $\isarkeyword{declare}$ commands are actually needed only
+very rarely; Isar admits to declare theorems on-the-fly wherever they emerge.
+Consider the following ML idiom:
+\begin{ttbox}
+Goal "\(\phi\)";
+ \(\vdots\)
+qed "name";
+Addsimps [name];
+\end{ttbox}
+This may be expressed more concisely in Isar like this:
+\begin{matharray}{l}
+ \LEMMA{name~[simp]}{\phi} \\
+ \quad\vdots
+\end{matharray}
+
+
+\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
+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
+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!
+
+\medskip This is a possible schedule to embark on actual conversion of legacy
+proof scripts into Isar proof texts.
+\begin{enumerate}
+\item Port ML scripts to Isar tactic emulation scripts (see
+ \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.}
+\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!
%%% Local Variables:
%%% mode: latex