# HG changeset patch # User wenzelm # Date 970160829 -7200 # Node ID 78a0397eaec13fa02cc6ca141fc7e46b3809b2c1 # Parent 7d6e03a1f11e80c8dd4a101548c2b257a8a74905 some preliminary stuff on conversion; diff -r 7d6e03a1f11e -r 78a0397eaec1 doc-src/IsarRef/conversion.tex --- a/doc-src/IsarRef/conversion.tex Thu Sep 28 19:06:46 2000 +0200 +++ b/doc-src/IsarRef/conversion.tex Thu Sep 28 19:07:09 2000 +0200 @@ -1,16 +1,221 @@ \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 +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 Actually redo ML proof scripts as human readable Isar proof texts + (probably hard, depending who wrote the original scripts). +\end{enumerate} + + \section{No conversion} -FIXME thm, theory, bind_thm(s); +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. + +\subsection{Referring to theorem and theory values} + +\begin{ttbox} +thm : xstring -> thm +thms : xstring -> thm list +the_context : unit -> theory +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. + +\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 + \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. + +\item [$\mathtt{theory}~name$] retrieves the named theory from the global + theory loader database. + + 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} + +\begin{ttbox} +qed : string -> unit +bind_thm : string * thm -> unit +bind_thms : string * thm list -> unit +\end{ttbox} + +ML proof scripts have to be well-behaved in storing theorems properly within +the current theory context, in order to enable new-style theories to retrieve +these these later. + +\begin{descr} +\item [$\mathtt{qed}~name$] is the canonical way to conclude a proof script in + 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. +\end{descr} + + +\subsection{Providing legacy ML bindings} + +\begin{matharray}{rcl} + \isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\ +\end{matharray} + +New-style theories may provide ML bindings to accommodate legacy ML scripts 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"}. \section{Porting proof scripts} -FIXME +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. + +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. + + +\subsection{Theory syntax} + +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 Types and terms have to be \emph{atomic} as far as the theory syntax is + concerned; this usually requires proper quoting of input strings. + + 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}). +\end{itemize} + +Isabelle/Isar error messages are usually quite explicit about the problem, so +doubtful cases of syntax may as well just tried interactively. + + +\subsection{Basic goal statements}\label{sec:conv-goal} -\subsection{Basic tactics} +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} + +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} \\ +\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. + +\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\) +\end{ttbox} +This may be replaced by an explicit invocation of the $unfold$ proof method. +\begin{matharray}{l} +\LEMMA{name}\texttt"{\phi}\texttt" \\ +\quad \isarkeyword{apply}~(unfold~defs) \\ +\quad \vdots \\ +\end{matharray} + +%FIXME "goal" and higher-order rules; + + +\subsection{Tactics vs.\ proof methods}\label{sec:conv-tac} + +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. + +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''). + +\bigskip + +FIXME \begin{matharray}{llll} \texttt{rtac}~a~1 & & rule~a \\ @@ -27,10 +232,12 @@ \end{matharray} -\section{Performing actual proof} +\subsection{Declarations and ad-hoc operations} + -FIXME +%\section{Performing actual proof} +%FIXME %%% Local Variables: %%% mode: latex