# HG changeset patch # User wenzelm # Date 970686342 -7200 # Node ID 482899aff303f16767c419e04c8976bba0768d02 # Parent 473807a5a43659bd7415cd5d07d6d8a50119e9be added more stuff; diff -r 473807a5a436 -r 482899aff303 doc-src/IsarRef/conversion.tex --- 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,\,). -\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,\,). +\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