updated;

--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Sat Nov 04 19:25:38 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Sat Nov 04 19:25:39 2006 +0100
@@ -5,15 +5,11 @@
 \isadelimtheory
 \isanewline
 \isanewline
-\isanewline
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ Codegen\isanewline
-\isakeyword{imports}\ Main\isanewline
-\isakeyword{begin}%
+%
 \endisatagtheory
 {\isafoldtheory}%
 %
@@ -21,6 +17,19 @@
 %
 \endisadelimtheory
 %
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
 \isamarkupchapter{Code generation from Isabelle theories%
 }
 \isamarkuptrue%
@@ -29,12 +38,124 @@
 }
 \isamarkuptrue%
 %
+\isamarkupsubsection{Motivation%
+}
+\isamarkuptrue%
+%
 \begin{isamarkuptext}%
-\cite{isa-tutorial}%
+Executing formal specifications as programs is a well-established
+  topic in the theorem proving community.  With increasing
+  application of theorem proving systems in the area of
+  software development and verification, its relevance manifests
+  for running test cases and rapid prototyping.  In logical
+  calculi like constructive type theory,
+  a notion of executability is implicit due to the nature
+  of the calculus.  In contrast, specifications in Isabelle/HOL
+  can be highly non-executable.  In order to bridge
+  the gap between logic and executable specifications,
+  an explicit non-trivial transformation has to be applied:
+  code generation.
+
+  This tutorial introduces a generic code generator for the
+  Isabelle system \cite{isa-tutorial}.
+  Generic in the sense that the
+  \qn{target language} for which code shall ultimately be
+  generated is not fixed but may be an arbitrary state-of-the-art
+  functional programming language (currently, the implementation
+  supports SML \cite{web:sml} and Haskell \cite{web:haskell}).
+  We aim to provide a
+  versatile environment
+  suitable for software development and verification,
+  structuring the process
+  of code generation into a small set of orthogonal principles
+  while achieving a big coverage of application areas
+  with maximum flexibility.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Basics%
+\isamarkupsubsection{Overview%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The code generator aims to be usable with no further ado
+  in most cases while allowing for detailed customization.
+  This manifests in the structure of this tutorial: this introduction
+  continues with a short introduction of concepts.  Section
+  \secref{sec:basics} explains how to use the framework naivly,
+  presuming a reasonable default setup.  Then, section
+  \secref{sec:advanced} deals with advanced topics,
+  introducing further aspects of the code generator framework
+  in a motivation-driven manner.  Last, section \secref{sec:ml}
+  introduces the framework's internal programming interfaces.
+
+  \begin{warn}
+    Ultimately, the code generator which this tutorial deals with
+    is supposed to replace the already established code generator
+    by Stefan Berghofer \cite{Berghofer-Nipkow:2002}.
+    So, for the moment, there are two distinct code generators
+    in Isabelle.
+    Also note that while the framework itself is largely
+    object-logic independent, only HOL provides a reasonable
+    framework setup.    
+  \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Code generation process%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The code generator employs a notion of executability
+  for three foundational executable ingredients known
+  from functional programming:
+  \emph{function equations}, \emph{datatypes}, and
+  \emph{type classes}. A function equation as a first approximation
+  is a theorem of the form \isa{f\ t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n\ {\isasymequiv}\ t}
+  (an equation headed by a constant \isa{f} with arguments
+  \isa{t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n} and right hand side \isa{t}.
+  Code generation aims to turn function equations
+  into a functional program by running through
+  a process (see figure \ref{fig:process}):
+
+  \begin{itemize}
+
+    \item Out of the vast collection of theorems proven in a
+      \qn{theory}, a reasonable subset modeling
+      function equations is \qn{selected}.
+
+    \item On those selected theorems, certain
+      transformations are carried out
+      (\qn{preprocessing}).  Their purpose is to turn theorems
+      representing non- or badly executable
+      specifications into equivalent but executable counterparts.
+      The result is a structured collection of \qn{code theorems}.
+
+    \item These \qn{code theorems} then are extracted
+      into an Haskell-like intermediate
+      language.
+
+    \item Finally, out of the intermediate language the final
+      code in the desired \qn{target language} is \qn{serialized}.
+
+  \end{itemize}
+
+  \begin{figure}[h]
+  \centering
+  \includegraphics[width=0.3\textwidth]{codegen_process}
+  \caption{code generator -- processing overview}
+  \label{fig:process}
+  \end{figure}
+
+  From these steps, only the two last are carried out
+  outside the logic; by keeping this layer as
+  thin as possible, the amount of code to trust is
+  kept to a minimum.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Basics \label{sec:basics}%
 }
 \isamarkuptrue%
 %
@@ -42,42 +163,1075 @@
 }
 \isamarkuptrue%
 %
+\begin{isamarkuptext}%
+Thanks to a reasonable setup of the HOL theories, in
+  most cases code generation proceeds without further ado:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\isamarkupfalse%
+\isanewline
+\ \ fac\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{primrec}\isamarkupfalse%
+\isanewline
+\ \ {\isachardoublequoteopen}fac\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}fac\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharasterisk}\ fac\ n{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+This executable specification is now turned to SML code:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\ fac\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\begin{isamarkuptext}%
+The \isasymCODEGEN command takes a space-seperated list of
+  constants together with \qn{serialization directives}
+  in parentheses. These start with a \qn{target language}
+  identifer, followed by arguments, their semantics
+  depending on the target. In the SML case, a filename
+  is given where to write the generated code to.
+
+  Internally, the function equations for all selected
+  constants are taken, including any tranitivly required
+  constants, datatypes and classes, resulting in the following
+  code:
+
+  \lstsml{Thy/examples/fac.ML}
+
+  The code generator will complain when a required
+  ingredient does not provide a executable counterpart.
+  This is the case if an involved type is not a datatype:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+\isanewline
+%
+\endisadelimML
+\isacommand{typedecl}\isamarkupfalse%
+\ {\isacharprime}a\ foo\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ bar\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ foo\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}bar\ x\ y\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+\isanewline
+\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\ bar\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fail{\isacharunderscore}type{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent will result in an error. Likewise, generating code
+  for constants not yielding
+  a function equation will fail, e.g.~the Hilbert choice
+  operation \isa{SOME}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+\isanewline
+%
+\endisadelimML
+\isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ pick{\isacharunderscore}some\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}pick{\isacharunderscore}some\ xs\ {\isacharequal}\ {\isacharparenleft}SOME\ x{\isachardot}\ x\ {\isasymin}\ set\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+\isanewline
+\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\ pick{\isacharunderscore}some\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fail{\isacharunderscore}const{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
 \isamarkupsubsection{Theorem selection%
 }
 \isamarkuptrue%
 %
+\begin{isamarkuptext}%
+The list of all function equations in a theory may be inspected
+  using the \isasymPRINTCODETHMS command:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{print{\isacharunderscore}codethms}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\noindent which displays a table of constant with corresponding
+  function equations (the additional stuff displayed
+  shall not bother us for the moment). If this table does
+  not provide at least one function
+  equation, the table of primititve definitions is searched
+  whether it provides one.
+
+  The typical HOL tools are already set up in a way that
+  function definitions introduced by \isasymFUN, \isasymFUNCTION,
+  \isasymPRIMREC, \isasymRECDEF are implicitly propagated
+  to this function equation table. Specific theorems may be
+  selected using an attribute: \emph{code func}. As example,
+  a weight selector function:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\isamarkupfalse%
+\isanewline
+\ \ pick\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ list\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{primrec}\isamarkupfalse%
+\isanewline
+\ \ {\isachardoublequoteopen}pick\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ n\ {\isacharequal}\ {\isacharparenleft}let\ {\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}\ {\isacharequal}\ x\ in\isanewline
+\ \ \ \ if\ n\ {\isacharless}\ k\ then\ v\ else\ pick\ xs\ {\isacharparenleft}n\ {\isacharminus}\ k{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+We want to eliminate the explicit destruction
+  of \isa{x} to \isa{{\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}pick\ {\isacharparenleft}{\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}{\isacharhash}xs{\isacharparenright}\ n\ {\isacharequal}\ {\isacharparenleft}if\ n\ {\isacharless}\ k\ then\ v\ else\ pick\ xs\ {\isacharparenleft}n\ {\isacharminus}\ k{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\ pick\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{1}}{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\begin{isamarkuptext}%
+This theorem is now added to the function equation table:
+
+  \lstsml{Thy/examples/pick1.ML}
+
+  It might be convenient to remove the pointless original
+  equation, using the \emph{nofunc} attribute:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemmas}\isamarkupfalse%
+\ {\isacharbrackleft}code\ nofunc{\isacharbrackright}\ {\isacharequal}\ pick{\isachardot}simps\ \isanewline
+\isanewline
+\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\ pick\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{2}}{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\begin{isamarkuptext}%
+\lstsml{Thy/examples/pick2.ML}
+
+  Syntactic redundancies are implicitly dropped. For example,
+  using a modified version of the \isa{fac} function
+  as function equation, the then redundant (since
+  syntactically subsumed) original function equations
+  are dropped, resulting in a warning:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}fac\ n\ {\isacharequal}\ {\isacharparenleft}case\ n\ of\ {\isadigit{0}}\ {\isasymRightarrow}\ {\isadigit{1}}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ n\ {\isacharasterisk}\ fac\ m{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}cases\ n{\isacharparenright}\ simp{\isacharunderscore}all%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\ fac\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isacharunderscore}case{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\begin{isamarkuptext}%
+\lstsml{Thy/examples/fac_case.ML}
+
+  \begin{warn}
+    Some statements in this section have to be treated with some
+    caution. First, since the HOL function package is still
+    under development, its setup with respect to code generation
+    may differ from what is presumed here.
+    Further, the attributes \emph{code} and \emph{code del}
+    associated with the existing code generator also apply to
+    the new one: \emph{code} implies \emph{code func},
+    and \emph{code del} implies \emph{code nofunc}.
+  \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsubsection{Type classes%
 }
 \isamarkuptrue%
 %
-\isamarkupsubsection{Preprocessing%
-}
+\begin{isamarkuptext}%
+Type classes enter the game via the Isar class package.
+  For a short introduction how to use it, see \cite{isabelle-classes};
+  here we just illustrate its impact on code generation.
+
+  In a target language, type classes may be represented
+  nativly (as in the case of Haskell). For languages
+  like SML, they are implemented using \emph{dictionaries}.
+  Our following example specifiedsa class \qt{null},
+  assigning to each of its inhabitants a \qt{null} value:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{class}\isamarkupfalse%
+\ null\ {\isacharequal}\isanewline
+\ \ \isakeyword{fixes}\ null\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline
+\isanewline
+\isacommand{consts}\isamarkupfalse%
+\isanewline
+\ \ head\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}null\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{primrec}\isamarkupfalse%
+\isanewline
+\ \ {\isachardoublequoteopen}head\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ null{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}head\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+We provide some instances for our \isa{null}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{instance}\isamarkupfalse%
+\ option\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ null\isanewline
+\ \ {\isachardoublequoteopen}null\ {\isasymequiv}\ None{\isachardoublequoteclose}%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{instance}\isamarkupfalse%
+\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ null\isanewline
+\ \ {\isachardoublequoteopen}null\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+Constructing a dummy example:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ {\isachardoublequoteopen}dummy\ {\isacharequal}\ head\ {\isacharbrackleft}Some\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ None{\isacharbrackright}{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+Type classes offer a suitable occassion to introduce
+  the Haskell serializer.  Its usage is almost the same
+  as SML, but, in accordance with conventions
+  some Haskell systems enforce, each module ends
+  up in a single file. The module hierarchy is reflected in
+  the file system, with root given by the user.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\ dummy\ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}examples{\isacharslash}{\isachardoublequoteclose}{\isacharparenright}%
+\begin{isamarkuptext}%
+\lsthaskell{Thy/examples/Codegen.hs}
+
+  (we have left out all other modules).
+
+  The whole code in SML with explicit dictionary passing:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\ dummy\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\begin{isamarkuptext}%
+\lstsml{Thy/examples/class.ML}%
+\end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsubsection{Incremental code generation%
 }
 \isamarkuptrue%
 %
-\isamarkupsection{Customizing serialization%
+\begin{isamarkuptext}%
+Code generation is \emph{incremental}: theorems
+  and abstract intermediate code are cached and extended on demand.
+  The cache may be partially or fully dropped if the underlying
+  executable content of the theory changes.
+  Implementation of caching is supposed to transparently
+  hid away the details from the user.  Anyway, caching
+  reaches the surface by using a slightly more general form
+  of the \isasymCODEGEN: either the list of constants or the
+  list of serialization expressions may be dropped.  If no
+  serialization expressions are given, only abstract code
+  is generated and cached; if no constants are given, the
+  current cache is serialized.
+
+  For explorative reasons, an extended version of the
+  \isasymCODEGEN command may prove useful:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{print{\isacharunderscore}codethms}\isamarkupfalse%
+\ {\isacharparenleft}{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent print all cached function equations (i.e.~\emph{after}
+  any applied transformation. Inside the brackets a
+  list of constants may be given; their function
+  euqations are added to the cache if not already present.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Recipes and advanced topics \label{sec:advanced}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+In this tutorial, we do not attempt to give an exhaustive
+  description of the code generator framework; instead,
+  we cast a light on advanced topics by introducing
+  them together with practically motivated examples.  Concerning
+  further reading, see
+
+  \begin{itemize}
+
+  \item the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}
+    for exhaustive syntax diagrams.
+  \item or \fixme{ref} which deals with foundational issues
+    of the code generator framework.
+
+  \end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Library theories%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The HOL \emph{Main} theory already provides a code generator setup
+  which should be suitable for most applications. Common extensions
+  and modifications are available by certain theories of the HOL
+  library; beside being useful in applications, they may serve
+  as a tutorial for cutomizing the code generator setup.
+
+  \begin{description}
+
+    \item[ExecutableSet] allows to generate code
+       for finite sets using lists.
+    \item[ExecutableRat] implements rational
+       numbers as triples \isa{{\isacharparenleft}sign{\isacharcomma}\ enumerator{\isacharcomma}\ denominator{\isacharparenright}}.
+    \item[EfficientNat] implements natural numbers by integers,
+       which in geneal will result in higher efficency; pattern
+       matching with \isa{{\isadigit{0}}} / \isa{Suc}
+       is eliminated. \label{eff_nat}
+    \item[MLString] provides an additional datatype \isa{mlstring};
+       in the HOL default setup, strings in HOL are mapped to list
+       of chars in SML; values of type \isa{mlstring} are
+       mapped to strings in SML.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Preprocessing%
 }
 \isamarkuptrue%
 %
-\isamarkupsection{Recipes and advanced topics%
+\begin{isamarkuptext}%
+Before selected function theorems are turned into abstract
+  code, a chain of definitional transformation steps is carried
+  out: \emph{preprocessing}. There are three possibilites
+  to customize preprocessing: \emph{inline theorems},
+  \emph{inline procedures} and \emph{generic preprocessors}.
+
+  \emph{Inline theorems} are rewriting rules applied to each
+  function equation.  Due to the interpretation of theorems
+  of function equations, rewrites are applied to the right
+  hand side and the arguments of the left hand side of an
+  equation, but never to the constant heading the left hand side.
+  Inline theorems may be declared an undeclared using the
+  \emph{code inline} or \emph{code noinline} attribute respectivly.
+
+  Some common applications:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{itemize}
+     \item replacing non-executable constructs by executable ones: \\
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\item eliminating superfluous constants: \\
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\item replacing executable but inconvenient constructs: \\
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\end{itemize}
+%
+\begin{isamarkuptext}%
+The current set of inline theorems may be inspected using
+  the \isasymPRINTCODETHMS command.
+
+  \emph{Inline procedures} are a generalized version of inline
+  theorems written in ML -- rewrite rules are generated dependent
+  on the function theorems for a certain function.  One
+  application is the implicit expanding of \isa{nat} numerals
+  to \isa{{\isadigit{0}}} / \isa{Suc} representation.  See further
+  \secref{sec:ml}
+
+  \emph{Generic preprocessors} provide a most general interface,
+  transforming a list of function theorems to another
+  list of function theorems, provided that neither the heading
+  constant nor its type change.  The \isa{{\isadigit{0}}} / \isa{Suc}
+  pattern elimination implemented in \secref{eff_nat} uses this
+  interface.
+
+  \begin{warn}
+    The order in which single preprocessing steps are carried
+    out currently is not specified; in particular, preprocessing
+    is \emph{no} fixpoint process.  Keep this in mind when
+    setting up the preprocessor.
+
+    Further, the attribute \emph{code unfold}
+    associated with the existing code generator also applies to
+    the new one: \emph{code unfold} implies \emph{code inline}.
+  \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Customizing serialization%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Consider the following function and its corresponding
+  SML code:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{fun}\isamarkupfalse%
+\isanewline
+\ \ in{\isacharunderscore}interval\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}\isanewline
+\isacommand{termination}\isamarkupfalse%
+%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}auto{\isacharunderscore}term\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\ in{\isacharunderscore}interval\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isadigit{1}}{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\begin{isamarkuptext}%
+\lstsml{Thy/examples/bool1.ML}
+
+  Though this is correct code, it is a little bit unsatisfactory:
+  boolean values and operators are materialized as distinguished
+  entities with have nothing to do with the SML-builtin notion
+  of \qt{bool}.  This results in less readable code;
+  additionally, eager evaluation may cause programs to
+  loop or break which would perfectly terminate when
+  the existing SML \qt{bool} would be used.  To map
+  the HOL \qt{bool} on SML \qt{bool}, we may use
+  \qn{custom serializations}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
+\ bool\isanewline
+\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}bool{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
+\ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}true{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}false{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharunderscore}\ andalso\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}%
+\begin{isamarkuptext}%
+The \isasymCODETYPE commad takes a type constructor
+  as arguments together with a list of custom serializations.
+  Each custom serialization starts with a target language
+  identifier followed by an expression, which during
+  code serialization is inserted whenever the type constructor
+  would occur.  For constants, \isasymCODECONST implements
+  the corresponding mechanism.  Each \qt{\_} in
+  a serialization expression is treated as a placeholder
+  for the type constructor's (the constant's) arguments.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
+\ SML\isanewline
+\ \ bool\ true\ false%
+\begin{isamarkuptext}%
+To assert that the existing \qt{bool}, \qt{true} and \qt{false}
+  is not used for generated code, we use \isasymCODERESERVED.
+
+  After this setup, code looks quite more readable:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\ in{\isacharunderscore}interval\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isadigit{2}}{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\begin{isamarkuptext}%
+\lstsml{Thy/examples/bool2.ML}
+
+  This still is not perfect: the parentheses
+  around \qt{andalso} are superfluos.  Though the serializer
+  by no means attempts to imitate the rich Isabelle syntax
+  framework, it provides some common idioms, notably
+  associative infixes with precedences which may be used here:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
+\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\isanewline
+\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\ in{\isacharunderscore}interval\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isadigit{3}}{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\begin{isamarkuptext}%
+\lstsml{Thy/examples/bool3.ML}
+
+  Next, we try to map HOL pairs to SML pairs, using the
+  infix \qt{ * } type constructor and parentheses:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isanewline
+\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
+\ {\isacharasterisk}\isanewline
+\ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\isanewline
+\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
+\ Pair\isanewline
+\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
+\begin{isamarkuptext}%
+The initial bang \qt{!} tells the serializer to never put
+  parentheses around the whole expression (they are already present),
+  while the parentheses around argument place holders
+  tell not to put parentheses around the arguments.
+  The slash \qt{/} (followed by arbitrary white space)
+  inserts a space which may be used as a break if necessary
+  during pretty printing.
+
+  So far,%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
+\ int\isanewline
+\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}IntInf{\isachardot}int{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\isanewline
+\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
+\ {\isachardoublequoteopen}op\ {\isacharplus}\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isacharminus}\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isacharasterisk}\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\isanewline
+\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}IntInf{\isachardot}{\isacharplus}\ {\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}IntInf{\isachardot}{\isacharminus}\ {\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}IntInf{\isachardot}{\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{6}}\ {\isachardoublequoteopen}{\isacharplus}{\isachardoublequoteclose}\ \isakeyword{and}\ \isakeyword{infixl}\ {\isadigit{6}}\ {\isachardoublequoteopen}{\isacharminus}{\isachardoublequoteclose}\ \isakeyword{and}\ \isakeyword{infixl}\ {\isadigit{7}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}%
+\isamarkupsubsection{Types matter%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Concerning operational equality%
 }
 \isamarkuptrue%
 %
-\isamarkupsection{ML interfaces%
+\begin{isamarkuptext}%
+Surely you have already noticed how equality is treated
+  by the code generator:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{fun}\isamarkupfalse%
+\isanewline
+\ \ collect{\isacharunderscore}duplicates\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline
+\ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline
+\ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline
+\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline
+\ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isacommand{termination}\isamarkupfalse%
+%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}auto{\isacharunderscore}term\ {\isachardoublequoteopen}measure\ {\isacharparenleft}length\ o\ snd\ o\ snd{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+The membership test during preprocessing is rewritting,
+  resulting in \isa{op\ mem}, which itself
+  performs an explicit equality check.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}collect{\isacharunderscore}duplicates{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\begin{isamarkuptext}%
+\lstsml{Thy/examples/collect_duplicates.ML}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Obviously, polymorphic equality is implemented the Haskell
+  way using a type class.  How is this achieved?  By an
+  almost trivial definition in the HOL setup:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+\isanewline
+%
+\endisadelimML
+\isacommand{class}\isamarkupfalse%
+\ eq\ {\isacharequal}\isanewline
+\ \ \isakeyword{fixes}\ eq\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{defs}\isamarkupfalse%
+\isanewline
+\ \ eq\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}eq\ {\isasymequiv}\ {\isacharparenleft}op\ {\isacharequal}{\isacharparenright}{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+This merely introduces a class \isa{eq} with corresponding
+  operation \isa{eq}, which by definition is isomorphic
+  to \isa{op\ {\isacharequal}}; the preprocessing framework does the rest.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+For datatypes, instances of \isa{eq} are implicitly derived
+  when possible.
+
+  Though this class is designed to get rarely in the way, there
+  are some cases when it suddenly comes to surface:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin {description}
+    \item[code lemmas and customary serializations for equality]
+      Examine the following: \\
+\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
+\ {\isachardoublequoteopen}op\ {\isacharequal}\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharunderscore}\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharequal}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
+\\ What is wrong here? Since \isa{op\ {\isacharequal}} is nothing else then
+  a plain constant, this customary serialization will refer
+  to polymorphic equality \isa{op\ {\isacharequal}}.
+  Instead, we want the specific equality on \isa{int},
+  by using the overloaded constant \isa{Code{\isacharunderscore}Generator{\isachardot}eq}: \\
+\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
+\ {\isachardoublequoteopen}Code{\isacharunderscore}Generator{\isachardot}eq\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharunderscore}\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharequal}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
+\\ \item[typedecls interpretated by customary serializations] A
+  common idiom is to use unspecified types for formalizations
+  and interpret them for a specific target language: \\
+\isacommand{typedecl}\isamarkupfalse%
+\ key\isanewline
+\isanewline
+\isacommand{fun}\isamarkupfalse%
+\isanewline
+\ \ lookup\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}key\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ list\ {\isasymRightarrow}\ key\ {\isasymRightarrow}\ {\isacharprime}a\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}lookup\ {\isacharbrackleft}{\isacharbrackright}\ l\ {\isacharequal}\ None{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}lookup\ {\isacharparenleft}{\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}\ {\isacharhash}\ xs{\isacharparenright}\ l\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isacharequal}\ l\ then\ Some\ v\ else\ lookup\ xs\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isacommand{termination}\isamarkupfalse%
+%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}auto{\isacharunderscore}term\ {\isachardoublequoteopen}measure\ {\isacharparenleft}length\ o\ fst{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
+\ key\isanewline
+\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}string{\isachardoublequoteclose}{\isacharparenright}%
+\\ This, though, is not sufficient: \isa{key} is no instance
+  of \isa{eq} since \isa{key} is no datatype; the instance
+  has to be declared manually, including a serialization
+  for the particular instance of \isa{Code{\isacharunderscore}Generator{\isachardot}eq}: \\
+\isacommand{instance}\isamarkupfalse%
+\ key\ {\isacharcolon}{\isacharcolon}\ eq%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
+\ {\isachardoublequoteopen}Code{\isacharunderscore}Generator{\isachardot}eq\ {\isasymColon}\ key\ {\isasymRightarrow}\ key\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharunderscore}\ {\isacharcolon}\ string\ {\isacharequal}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
+\\ Then everything goes fine: \\
+\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\ lookup\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}lookup{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\begin{isamarkuptext}%
+\lstsml{Thy/examples/lookup.ML}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\item[lexicographic orderings and corregularity] Another sublety
+  enters the stage when definitions of overloaded constants
+  are dependent on operational equality.  For example, let
+  us define a lexicographic ordering on tuples: \\
+\isanewline
+\isanewline
+%
+\\ Then code generation will fail.  Why?  The definition
+  of \isa{op\ {\isasymle}} depends on equality on both arguments,
+  which are polymorhpic and impose an additional \isa{eq}
+  class constraint, thus violating the type discipline
+  for class operations.
+
+  The solution is to add \isa{eq} to both sort arguments: \\
+\isacommand{instance}\isamarkupfalse%
+\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isachardoublequoteopen}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isachardoublequoteclose}{\isacharcomma}\ {\isachardoublequoteopen}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isachardoublequoteclose}{\isacharparenright}\ ord\isanewline
+\ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
+\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymle}\ p{\isadigit{2}}\ {\isasymequiv}\ p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymor}\ p{\isadigit{1}}\ {\isacharequal}\ p{\isadigit{2}}{\isachardoublequoteclose}%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\\ Then code generation succeeds: \\
+\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}lexicographic{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\begin{isamarkuptext}%
+\lstsml{Thy/examples/lexicographic.ML}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\item[Haskell serialization]
+%
+\end {description}
+%
+\isamarkupsubsection{Axiomatic extensions%
 }
 \isamarkuptrue%
 %
-\isamarkupsubsection{codegen\_data.ML%
+\begin{isamarkuptext}%
+\begin{warn}
+    The extensions introduced in this section, though working
+    in practice, are not the cream of the crop.  They will
+    eventually be replaced by more mature approaches.
+  \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{ML interfaces \label{sec:ml}%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Constants with type discipline: codegen\_consts.ML%
+}
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexmltype{CodegenConsts.const}\verb|type CodegenConsts.const| \\
+  \indexml{CodegenConsts.inst-of-typ}\verb|CodegenConsts.inst_of_typ: theory -> string * typ -> CodegenConsts.const| \\
+  \indexml{CodegenConsts.typ-of-inst}\verb|CodegenConsts.typ_of_inst: theory -> CodegenConsts.const -> string * typ| \\
+  \indexml{CodegenConsts.norm}\verb|CodegenConsts.norm: theory -> CodegenConsts.const -> CodegenConsts.const| \\
+  \indexml{CodegenConsts.norm-of-typ}\verb|CodegenConsts.norm_of_typ: theory -> string * typ -> CodegenConsts.const|
+  \end{mldecls}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Executable theory content: codegen\_data.ML%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+This Pure module implements the core notions of
+  executable content of a theory.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Suspended theorems%
+}
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexmltype{CodegenData.lthms}\verb|type CodegenData.lthms| \\
+  \indexml{CodegenData.lazy}\verb|CodegenData.lazy: (unit -> thm list) -> CodegenData.lthms|
+  \end{mldecls}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsubsection{Executable content%
 }
 \isamarkuptrue%
 %
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexml{CodegenData.add-func}\verb|CodegenData.add_func: thm -> theory -> theory| \\
+  \indexml{CodegenData.del-func}\verb|CodegenData.del_func: thm -> theory -> theory| \\
+  \indexml{CodegenData.add-funcl}\verb|CodegenData.add_funcl: CodegenConsts.const * CodegenData.lthms -> theory -> theory| \\
+  \indexml{CodegenData.add-datatype}\verb|CodegenData.add_datatype: string * (((string * sort) list * (string * typ list) list) * CodegenData.lthms) -> theory -> theory| \\
+  \indexml{CodegenData.del-datatype}\verb|CodegenData.del_datatype: string -> theory -> theory| \\
+  \indexml{CodegenData.add-inline}\verb|CodegenData.add_inline: thm -> theory -> theory| \\
+  \indexml{CodegenData.del-inline}\verb|CodegenData.del_inline: thm -> theory -> theory| \\
+  \indexml{CodegenData.add-inline-proc}\verb|CodegenData.add_inline_proc: (theory -> cterm list -> thm list) -> theory -> theory| \\
+  \indexml{CodegenData.add-preproc}\verb|CodegenData.add_preproc: (theory -> thm list -> thm list) -> theory -> theory| \\
+  \indexml{CodegenData.these-funcs}\verb|CodegenData.these_funcs: theory -> CodegenConsts.const -> thm list| \\
+  \indexml{CodegenData.get-datatype}\verb|CodegenData.get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list) option| \\
+  \indexml{CodegenData.get-datatype-of-constr}\verb|CodegenData.get_datatype_of_constr: theory -> CodegenConsts.const -> string option|
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|CodegenData.add_func|~\isa{thm}
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Further auxiliary%
+}
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexml{CodegenConsts.const-ord}\verb|CodegenConsts.const_ord: CodegenConsts.const * CodegenConsts.const -> order| \\
+  \indexml{CodegenConsts.eq-const}\verb|CodegenConsts.eq_const: CodegenConsts.const * CodegenConsts.const -> bool| \\
+  \indexml{CodegenConsts.consts-of}\verb|CodegenConsts.consts_of: theory -> term -> CodegenConsts.const list| \\
+  \indexml{CodegenConsts.read-const}\verb|CodegenConsts.read_const: theory -> string -> CodegenConsts.const| \\
+  \indexmlstructure{CodegenConsts.Consttab}\verb|structure CodegenConsts.Consttab| \\
+  \indexml{CodegenData.typ-func}\verb|CodegenData.typ_func: theory -> thm -> typ| \\
+  \indexml{CodegenData.rewrite-func}\verb|CodegenData.rewrite_func: thm list -> thm -> thm| \\
+  \end{mldecls}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
 \isamarkupsubsection{Implementing code generator applications%
 }
 \isamarkuptrue%
 %
+\begin{isamarkuptext}%
+\begin{warn}
+    Some interfaces discussed here have not reached
+    a final state yet.
+    Changes likely to occur in future.
+  \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Data depending on the theory's executable content%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Datatype hooks%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\emph{Happy proving, happy hacking!}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isadelimtheory
 %
 \endisadelimtheory

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool1.ML	Sat Nov 04 19:25:38 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool1.ML	Sat Nov 04 19:25:39 2006 +0100
@@ -11,8 +11,8 @@
 
 fun op_conj y True = y
   | op_conj x False = False
-  | op_conj True ya = ya
-  | op_conj False xa = False;
+  | op_conj True y = y
+  | op_conj False x = False;
 
 end; (*struct HOL*)
 
@@ -22,8 +22,8 @@
 datatype nat = Zero_nat | Succ_nat of nat;
 
 fun less_nat Zero_nat (Succ_nat n) = HOL.True
-  | less_nat na Zero_nat = HOL.False
-  | less_nat (Succ_nat m) (Succ_nat nb) = less_nat m nb;
+  | less_nat n Zero_nat = HOL.False
+  | less_nat (Succ_nat m) (Succ_nat n) = less_nat m n;
 
 fun less_eq_nat m n = HOL.nota (less_nat n m);
 

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool2.ML	Sat Nov 04 19:25:38 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool2.ML	Sat Nov 04 19:25:39 2006 +0100
@@ -15,8 +15,8 @@
 datatype nat = Zero_nat | Succ_nat of nat;
 
 fun less_nat Zero_nat (Succ_nat n) = true
-  | less_nat na Zero_nat = false
-  | less_nat (Succ_nat m) (Succ_nat nb) = less_nat m nb;
+  | less_nat n Zero_nat = false
+  | less_nat (Succ_nat m) (Succ_nat n) = less_nat m n;
 
 fun less_eq_nat m n = HOL.nota (less_nat n m);
 

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool3.ML	Sat Nov 04 19:25:38 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool3.ML	Sat Nov 04 19:25:39 2006 +0100
@@ -15,8 +15,8 @@
 datatype nat = Zero_nat | Succ_nat of nat;
 
 fun less_nat Zero_nat (Succ_nat n) = true
-  | less_nat na Zero_nat = false
-  | less_nat (Succ_nat m) (Succ_nat nb) = less_nat m nb;
+  | less_nat n Zero_nat = false
+  | less_nat (Succ_nat m) (Succ_nat n) = less_nat m n;
 
 fun less_eq_nat m n = HOL.nota (less_nat n m);
 

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Sat Nov 04 19:25:38 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Sat Nov 04 19:25:39 2006 +0100
@@ -21,7 +21,7 @@
 
 fun memberl (A_1_:'a_1 Code_Generator.eq) x (y :: ys) =
   HOL.op_eq A_1_ x y orelse memberl A_1_ x ys
-  | memberl (A_1_:'a_1 Code_Generator.eq) xa [] = false;
+  | memberl (A_1_:'a_1 Code_Generator.eq) x [] = false;
 
 end; (*struct List*)
 
@@ -33,7 +33,7 @@
     then (if List.memberl A_ z ys then collect_duplicates A_ xs ys zs
            else collect_duplicates A_ xs (z :: ys) zs)
     else collect_duplicates A_ (z :: xs) (z :: ys) zs)
-  | collect_duplicates (A_:'a Code_Generator.eq) y ysa [] = y;
+  | collect_duplicates (A_:'a Code_Generator.eq) y ys [] = y;
 
 end; (*struct Codegen*)
 

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Sat Nov 04 19:25:38 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Sat Nov 04 19:25:39 2006 +0100
@@ -10,7 +10,7 @@
   | plus_nat Zero_nat y = y;
 
 fun times_nat (Succ_nat m) n = plus_nat n (times_nat m n)
-  | times_nat Zero_nat na = Zero_nat;
+  | times_nat Zero_nat n = Zero_nat;
 
 end; (*struct IntDef*)
 

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Sat Nov 04 19:25:38 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Sat Nov 04 19:25:39 2006 +0100
@@ -10,7 +10,7 @@
   | plus_nat Zero_nat y = y;
 
 fun times_nat (Succ_nat m) n = plus_nat n (times_nat m n)
-  | times_nat Zero_nat na = Zero_nat;
+  | times_nat Zero_nat n = Zero_nat;
 
 end; (*struct IntDef*)
 

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML	Sat Nov 04 19:25:38 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML	Sat Nov 04 19:25:39 2006 +0100
@@ -6,7 +6,7 @@
 
 fun lookup ((k, v) :: xs) l =
   (if (k : string = l) then SOME v else lookup xs l)
-  | lookup [] la = NONE;
+  | lookup [] l = NONE;
 
 end; (*struct Codegen*)
 

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Sat Nov 04 19:25:38 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Sat Nov 04 19:25:39 2006 +0100
@@ -7,11 +7,11 @@
 datatype nat = Zero_nat | Succ_nat of nat;
 
 fun less_nat Zero_nat (Succ_nat n) = true
-  | less_nat na Zero_nat = false
-  | less_nat (Succ_nat m) (Succ_nat nb) = less_nat m nb;
+  | less_nat n Zero_nat = false
+  | less_nat (Succ_nat m) (Succ_nat n) = less_nat m n;
 
 fun minus_nat (Succ_nat m) (Succ_nat n) = minus_nat m n
-  | minus_nat Zero_nat na = Zero_nat
+  | minus_nat Zero_nat n = Zero_nat
   | minus_nat y Zero_nat = y;
 
 end; (*struct IntDef*)
@@ -21,12 +21,11 @@
 
 fun pick ((k, v) :: xs) n =
   (if IntDef.less_nat n k then v else pick xs (IntDef.minus_nat n k))
-  | pick (x :: xsa) na =
+  | pick (x :: xs) n =
     let
       val (ka, va) = x;
     in
-      (if IntDef.less_nat na ka then va
-        else pick xsa (IntDef.minus_nat na ka))
+      (if IntDef.less_nat n ka then va else pick xs (IntDef.minus_nat n ka))
     end;
 
 end; (*struct Codegen*)

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Sat Nov 04 19:25:38 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Sat Nov 04 19:25:39 2006 +0100
@@ -7,11 +7,11 @@
 datatype nat = Zero_nat | Succ_nat of nat;
 
 fun less_nat Zero_nat (Succ_nat n) = true
-  | less_nat na Zero_nat = false
-  | less_nat (Succ_nat m) (Succ_nat nb) = less_nat m nb;
+  | less_nat n Zero_nat = false
+  | less_nat (Succ_nat m) (Succ_nat n) = less_nat m n;
 
 fun minus_nat (Succ_nat m) (Succ_nat n) = minus_nat m n
-  | minus_nat Zero_nat na = Zero_nat
+  | minus_nat Zero_nat n = Zero_nat
   | minus_nat y Zero_nat = y;
 
 end; (*struct IntDef*)

--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Sat Nov 04 19:25:38 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Sat Nov 04 19:25:39 2006 +0100
@@ -41,7 +41,7 @@
       written once, modified ten times, and read
       100 times.  So simplify its writing,
       always keep future modifications in mind,
-      and never jeopardize readability. Every second you hesitate
+      and never jeopardize readability.  Every second you hesitate
       to spend on making your code more clear you will
       have to spend ten times understanding what you have
       written later on.

--- a/doc-src/IsarImplementation/Thy/document/integration.tex	Sat Nov 04 19:25:38 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex	Sat Nov 04 19:25:39 2006 +0100
@@ -184,7 +184,7 @@
 \verb|  Toplevel.transition -> Toplevel.transition| \\
   \indexml{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline%
 \verb|  Toplevel.transition -> Toplevel.transition| \\
-  \indexml{Toplevel.proof-to-theory}\verb|Toplevel.proof_to_theory: (Proof.state -> theory) ->|\isasep\isanewline%
+  \indexml{Toplevel.end-proof}\verb|Toplevel.end_proof: (bool -> Proof.state -> Proof.context) ->|\isasep\isanewline%
 \verb|  Toplevel.transition -> Toplevel.transition| \\
   \end{mldecls}
 
@@ -217,9 +217,9 @@
   command, with zero or more result states (represented as a lazy
   list).
 
-  \item \verb|Toplevel.proof_to_theory|~\isa{tr} adjoins a
-  concluding proof command, that returns the resulting theory, after
-  storing the resulting facts etc.
+  \item \verb|Toplevel.end_proof|~\isa{tr} adjoins a concluding
+  proof command, that returns the resulting theory, after storing the
+  resulting facts in the context etc.
 
   \end{description}%
 \end{isamarkuptext}%