doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex

fixed

%
\begin{isabellebody}%
\def\isabellecontext{Program}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Program\isanewline
\isakeyword{imports}\ Introduction\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupsection{Turning Theories into Programs \label{sec:program}%
}
\isamarkuptrue%
%
\isamarkupsubsection{The \isa{Isabelle{\isacharslash}HOL} default setup%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
We have already seen how by default equations stemming from
  \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}/\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}/\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}}
  statements are used for code generation.  This default behaviour
  can be changed, e.g. by providing different defining equations.
  All kinds of customization shown in this section is \emph{safe}
  in the sense that the user does not have to worry about
  correctness -- all programs generatable that way are partially
  correct.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Selecting code equations%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Coming back to our introductory example, we
  could provide an alternative defining equations for \isa{dequeue}
  explicitly:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
\isacommand{lemma}\isamarkupfalse%
\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ else\ dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ Queue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\begin{isamarkuptext}%
\noindent The annotation \isa{{\isacharbrackleft}code\ func{\isacharbrackright}} is an \isa{Isar}
  \isa{attribute} which states that the given theorems should be
  considered as defining equations for a \isa{fun} statement --
  the corresponding constant is determined syntactically.  The resulting code:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
%
\begin{isamarkuptext}%
\isaverbatim%
\noindent%
\verb|module Example where {|\newline%
\newline%
\newline%
\verb|foldla :: forall a b. (a -> b -> a) -> a -> [b] -> a;|\newline%
\verb|foldla f a [] = a;|\newline%
\verb|foldla f a (x : xs) = foldla f (f a x) xs;|\newline%
\newline%
\verb|rev :: forall a. [a] -> [a];|\newline%
\verb|rev xs = foldla (\ xsa x -> x : xsa) [] xs;|\newline%
\newline%
\verb|nulla :: forall a. [a] -> Bool;|\newline%
\verb|nulla (x : xs) = False;|\newline%
\verb|nulla [] = True;|\newline%
\newline%
\verb|data Queue a = Queue [a] [a];|\newline%
\newline%
\verb|empty :: forall a. Queue a;|\newline%
\verb|empty = Queue [] [];|\newline%
\newline%
\verb|dequeue :: forall a. Queue a -> (Maybe a, Queue a);|\newline%
\verb|dequeue (Queue xs (y : ys)) = (Just y, Queue xs ys);|\newline%
\verb|dequeue (Queue xs []) =|\newline%
\verb|  (if nulla xs then (Nothing, Queue [] [])|\newline%
\verb|    else dequeue (Queue [] (rev xs)));|\newline%
\newline%
\verb|enqueue :: forall a. a -> Queue a -> Queue a;|\newline%
\verb|enqueue x (Queue xs ys) = Queue (x : xs) ys;|\newline%
\newline%
\verb|}|%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\begin{isamarkuptext}%
\noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has been
  replaced by the predicate \isa{null\ xs}.  This is due to the default
  setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).

  Changing the default constructor set of datatypes is also
  possible but rarely desired in practice.  See \secref{sec:datatypes} for an example.

  As told in \secref{sec:concept}, code generation is based
  on a structured collection of code theorems.
  For explorative purpose, this collection
  may be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
\ dequeue%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\begin{isamarkuptext}%
\noindent prints a table with \emph{all} defining equations
  for \isa{dequeue}, including
  \emph{all} defining equations those equations depend
  on recursively.
  
  Similarly, the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command shows a graph
  visualising dependencies between defining equations.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{\isa{class} and \isa{instantiation}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Concerning type classes and code generation, let us examine an example
  from abstract algebra:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
\isacommand{class}\isamarkupfalse%
\ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline
\ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{class}\isamarkupfalse%
\ monoid\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \isakeyword{and}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{instantiation}\isamarkupfalse%
\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{primrec}\isamarkupfalse%
\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
\ \ \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymotimes}\ n\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m\ {\isasymotimes}\ n{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ neutral{\isacharunderscore}nat\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ n\ m\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ m{\isacharparenright}\ {\isasymotimes}\ q\ {\isacharequal}\ n\ {\isasymotimes}\ q\ {\isacharplus}\ m\ {\isasymotimes}\ q{\isachardoublequoteclose}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
\ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}m\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\isacommand{end}\isamarkupfalse%
%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\begin{isamarkuptext}%
\noindent We define the natural operation of the natural numbers
  on monoids:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
\isacommand{primrec}\isamarkupfalse%
\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ \ \ {\isachardoublequoteopen}pow\ {\isadigit{0}}\ a\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
\ \ {\isacharbar}\ {\isachardoublequoteopen}pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ a\ {\isasymotimes}\ pow\ n\ a{\isachardoublequoteclose}%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\begin{isamarkuptext}%
\noindent This we use to define the discrete exponentiation function:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
\isacommand{definition}\isamarkupfalse%
\ bexp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\begin{isamarkuptext}%
\noindent The corresponding code:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
%
\begin{isamarkuptext}%
\isaverbatim%
\noindent%
\verb|module Example where {|\newline%
\newline%
\newline%
\verb|data Nat = Suc Nat |\verb,|,\verb| Zero_nat;|\newline%
\newline%
\verb|class Semigroup a where {|\newline%
\verb|  mult :: a -> a -> a;|\newline%
\verb|};|\newline%
\newline%
\verb|class (Semigroup a) => Monoid a where {|\newline%
\verb|  neutral :: a;|\newline%
\verb|};|\newline%
\newline%
\verb|pow :: forall a. (Monoid a) => Nat -> a -> a;|\newline%
\verb|pow (Suc n) a = mult a (pow n a);|\newline%
\verb|pow Zero_nat a = neutral;|\newline%
\newline%
\verb|plus_nat :: Nat -> Nat -> Nat;|\newline%
\verb|plus_nat (Suc m) n = plus_nat m (Suc n);|\newline%
\verb|plus_nat Zero_nat n = n;|\newline%
\newline%
\verb|neutral_nat :: Nat;|\newline%
\verb|neutral_nat = Suc Zero_nat;|\newline%
\newline%
\verb|mult_nat :: Nat -> Nat -> Nat;|\newline%
\verb|mult_nat (Suc m) n = plus_nat n (mult_nat m n);|\newline%
\verb|mult_nat Zero_nat n = Zero_nat;|\newline%
\newline%
\verb|instance Semigroup Nat where {|\newline%
\verb|  mult = mult_nat;|\newline%
\verb|};|\newline%
\newline%
\verb|instance Monoid Nat where {|\newline%
\verb|  neutral = neutral_nat;|\newline%
\verb|};|\newline%
\newline%
\verb|bexp :: Nat -> Nat;|\newline%
\verb|bexp n = pow n (Suc (Suc Zero_nat));|\newline%
\newline%
\verb|}|%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\begin{isamarkuptext}%
\noindent This is a convenient place to show how explicit dictionary construction
  manifests in generated code (here, the same example in \isa{SML}):%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
%
\begin{isamarkuptext}%
\isaverbatim%
\noindent%
\verb|structure Example = |\newline%
\verb|struct|\newline%
\newline%
\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
\newline%
\verb|type 'a semigroup = {mult : 'a -> 'a -> 'a};|\newline%
\verb|fun mult (A_:'a semigroup) = #mult A_;|\newline%
\newline%
\verb|type 'a monoid = {Program__semigroup_monoid : 'a semigroup, neutral : 'a};|\newline%
\verb|fun semigroup_monoid (A_:'a monoid) = #Program__semigroup_monoid A_;|\newline%
\verb|fun neutral (A_:'a monoid) = #neutral A_;|\newline%
\newline%
\verb|fun pow A_ (Suc n) a = mult (semigroup_monoid A_) a (pow A_ n a)|\newline%
\verb|  |\verb,|,\verb| pow A_ Zero_nat a = neutral A_;|\newline%
\newline%
\verb|fun plus_nat (Suc m) n = plus_nat m (Suc n)|\newline%
\verb|  |\verb,|,\verb| plus_nat Zero_nat n = n;|\newline%
\newline%
\verb|val neutral_nat : nat = Suc Zero_nat;|\newline%
\newline%
\verb|fun mult_nat (Suc m) n = plus_nat n (mult_nat m n)|\newline%
\verb|  |\verb,|,\verb| mult_nat Zero_nat n = Zero_nat;|\newline%
\newline%
\verb|val semigroup_nat = {mult = mult_nat} : nat semigroup;|\newline%
\newline%
\verb|val monoid_nat =|\newline%
\verb|  {Program__semigroup_monoid = semigroup_nat, neutral = neutral_nat} :|\newline%
\verb|  nat monoid;|\newline%
\newline%
\verb|fun bexp n = pow monoid_nat n (Suc (Suc Zero_nat));|\newline%
\newline%
\verb|end; (*struct Example*)|%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\begin{isamarkuptext}%
\noindent Note the parameters with trailing underscore (\verb|A_|)
    which are the dictionary parameters.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{The preprocessor \label{sec:preproc}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Before selected function theorems are turned into abstract
  code, a chain of definitional transformation steps is carried
  out: \emph{preprocessing}.  In essence, the preprocessor
  consists of two components: a \emph{simpset} and \emph{function transformers}.

  The \emph{simpset} allows to employ the full generality of the Isabelle
  simplifier.  Due to the interpretation of theorems
  as defining 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.
  An important special case are \emph{inline theorems} which may be
  declared and undeclared using the
  \emph{code inline} or \emph{code inline del} attribute respectively.

  Some common applications:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\begin{itemize}
%
\begin{isamarkuptext}%
\item replacing non-executable constructs by executable ones:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
\isacommand{lemma}\isamarkupfalse%
\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\begin{isamarkuptext}%
\item eliminating superfluous constants:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
\isacommand{lemma}\isamarkupfalse%
\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ simp%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\begin{isamarkuptext}%
\item replacing executable but inconvenient constructs:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
\isacommand{lemma}\isamarkupfalse%
\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\end{itemize}
%
\begin{isamarkuptext}%
\noindent \emph{Function transformers} provide a very 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
  theory \isa{Efficient{\isacharunderscore}Nat} (see \secref{eff_nat}) uses this
  interface.

  \noindent The current setup of the preprocessor may be inspected using
  the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
  \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient
  mechanism to inspect the impact of a preprocessor setup
  on defining equations.

  \begin{warn}
    The attribute \emph{code unfold}
    associated with the \isa{SML\ code\ generator} also applies to
    the \isa{generic\ code\ generator}:
    \emph{code unfold} implies \emph{code inline}.
  \end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Datatypes \label{sec:datatypes}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Conceptually, any datatype is spanned by a set of
  \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n}
  where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is excactly the set of \emph{all}
  type variables in \isa{{\isasymtau}}.  The HOL datatype package
  by default registers any new datatype in the table
  of datatypes, which may be inspected using
  the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.

  In some cases, it may be convenient to alter or
  extend this table;  as an example, we will develop an alternative
  representation of natural numbers as binary digits, whose
  size does increase logarithmically with its value, not linear
  \footnote{Indeed, the \hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}} theory (see \ref{eff_nat})
    does something similar}.  First, the digit representation:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
\isacommand{definition}\isamarkupfalse%
\ Dig{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ n\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ n{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ \ Dig{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ n{\isacharparenright}{\isachardoublequoteclose}%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\begin{isamarkuptext}%
\noindent We will use these two \qt{digits} to represent natural numbers
  in binary digits, e.g.:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
\isacommand{lemma}\isamarkupfalse%
\ {\isadigit{4}}{\isadigit{2}}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}Dig{\isadigit{1}}\ {\isacharparenleft}Dig{\isadigit{0}}\ {\isacharparenleft}Dig{\isadigit{1}}\ {\isacharparenleft}Dig{\isadigit{0}}\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\begin{isamarkuptext}%
\noindent Of course we also have to provide proper code equations for
  the operations, e.g. \isa{op\ {\isacharplus}}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
\isacommand{lemma}\isamarkupfalse%
\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}m\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ n{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ {\isadigit{1}}\ {\isacharequal}\ Dig{\isadigit{1}}\ m{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ {\isadigit{1}}\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\begin{isamarkuptext}%
\noindent We then instruct the code generator to view \isa{{\isadigit{0}}},
  \isa{{\isadigit{1}}}, \isa{Dig{\isadigit{0}}} and \isa{Dig{\isadigit{1}}} as
  datatype constructors:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{0}}{\isasymColon}nat{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isadigit{1}}{\isasymColon}nat{\isachardoublequoteclose}\ Dig{\isadigit{0}}\ Dig{\isadigit{1}}%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\begin{isamarkuptext}%
\noindent For the former constructor \isa{Suc}, we provide a code
  equation and remove some parts of the default code generator setup
  which are an obstacle here:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
\isacommand{lemma}\isamarkupfalse%
\ Suc{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}Suc\ n\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isanewline
\isacommand{declare}\isamarkupfalse%
\ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline\ del{\isacharbrackright}\isanewline
\isacommand{declare}\isamarkupfalse%
\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\begin{isamarkuptext}%
\noindent This yields the following code:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
%
\begin{isamarkuptext}%
\isaverbatim%
\noindent%
\verb|structure Example = |\newline%
\verb|struct|\newline%
\newline%
\verb|datatype nat = Dig1 of nat |\verb,|,\verb| Dig0 of nat |\verb,|,\verb| One_nat |\verb,|,\verb| Zero_nat;|\newline%
\newline%
\verb|fun plus_nat (Dig1 m) (Dig1 n) = Dig0 (plus_nat (plus_nat m n) One_nat)|\newline%
\verb|  |\verb,|,\verb| plus_nat (Dig1 m) (Dig0 n) = Dig1 (plus_nat m n)|\newline%
\verb|  |\verb,|,\verb| plus_nat (Dig0 m) (Dig1 n) = Dig1 (plus_nat m n)|\newline%
\verb|  |\verb,|,\verb| plus_nat (Dig0 m) (Dig0 n) = Dig0 (plus_nat m n)|\newline%
\verb|  |\verb,|,\verb| plus_nat (Dig1 m) One_nat = Dig0 (plus_nat m One_nat)|\newline%
\verb|  |\verb,|,\verb| plus_nat One_nat (Dig1 n) = Dig0 (plus_nat n One_nat)|\newline%
\verb|  |\verb,|,\verb| plus_nat (Dig0 m) One_nat = Dig1 m|\newline%
\verb|  |\verb,|,\verb| plus_nat One_nat (Dig0 n) = Dig1 n|\newline%
\verb|  |\verb,|,\verb| plus_nat m Zero_nat = m|\newline%
\verb|  |\verb,|,\verb| plus_nat Zero_nat n = n;|\newline%
\newline%
\verb|end; (*struct Example*)|%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\begin{isamarkuptext}%
\noindent From this example, it can be easily glimpsed that using own constructor sets
  is a little delicate since it changes the set of valid patterns for values
  of that type.  Without going into much detail, here some practical hints:

  \begin{itemize}
    \item When changing the constructor set for datatypes, take care to
      provide an alternative for the \isa{case} combinator (e.g.~by replacing
      it using the preprocessor).
    \item Values in the target language need not to be normalised -- different
      values in the target language may represent the same value in the
      logic (e.g. \isa{Dig{\isadigit{1}}\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}}).
    \item Usually, a good methodology to deal with the subtleties of pattern
      matching is to see the type as an abstract type: provide a set
      of operations which operate on the concrete representation of the type,
      and derive further operations by combinations of these primitive ones,
      without relying on a particular representation.
  \end{itemize}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadeliminvisible
%
\endisadeliminvisible
%
\isataginvisible
\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isachardoublequoteclose}\ Suc\isanewline
\isacommand{declare}\isamarkupfalse%
\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}\isanewline
\isacommand{declare}\isamarkupfalse%
\ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline{\isacharbrackright}\isanewline
\isacommand{declare}\isamarkupfalse%
\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func{\isacharbrackright}\ \isanewline
\isacommand{lemma}\isamarkupfalse%
\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymColon}\ nat{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ simp%
\endisataginvisible
{\isafoldinvisible}%
%
\isadeliminvisible
%
\endisadeliminvisible
%
\isamarkupsubsection{Equality and wellsortedness%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Surely you have already noticed how equality is treated
  by the code generator:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
\isacommand{primrec}\isamarkupfalse%
\ 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
\ \ {\isacharbar}\ {\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}%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\begin{isamarkuptext}%
\noindent The membership test during preprocessing is rewritten,
  resulting in \isa{op\ mem}, which itself
  performs an explicit equality check.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
%
\begin{isamarkuptext}%
\isaverbatim%
\noindent%
\verb|structure Example = |\newline%
\verb|struct|\newline%
\newline%
\verb|type 'a eq = {eq : 'a -> 'a -> bool};|\newline%
\verb|fun eq (A_:'a eq) = #eq A_;|\newline%
\newline%
\verb|fun eqop A_ a b = eq A_ a b;|\newline%
\newline%
\verb|fun member A_ x (y :: ys) = (if eqop A_ y x then true else member A_ x ys)|\newline%
\verb|  |\verb,|,\verb| member A_ x [] = false;|\newline%
\newline%
\verb|fun collect_duplicates A_ xs ys (z :: zs) =|\newline%
\verb|  (if member A_ z xs|\newline%
\verb|    then (if member A_ z ys then collect_duplicates A_ xs ys zs|\newline%
\verb|           else collect_duplicates A_ xs (z :: ys) zs)|\newline%
\verb|    else collect_duplicates A_ (z :: xs) (z :: ys) zs)|\newline%
\verb|  |\verb,|,\verb| collect_duplicates A_ xs ys [] = xs;|\newline%
\newline%
\verb|end; (*struct Example*)|%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\begin{isamarkuptext}%
\noindent Obviously, polymorphic equality is implemented the Haskell
  way using a type class.  How is this achieved?  HOL introduces
  an explicit class \isa{eq} with a corresponding operation
  \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharequal}\ op\ {\isacharequal}}.
  The preprocessing framework does the rest by propagating the
  \isa{eq} constraints through all dependent defining equations.
  For datatypes, instances of \isa{eq} are implicitly derived
  when possible.  For other types, you may instantiate \isa{eq}
  manually like any other type class.

  Though this \isa{eq} class is designed to get rarely in
  the way, a subtlety
  enters the stage when definitions of overloaded constants
  are dependent on operational equality.  For example, let
  us define a lexicographic ordering on tuples
  (also see theory \hyperlink{theory.Product-ord}{\mbox{\isa{Product{\isacharunderscore}ord}}}):%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
\isacommand{instantiation}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}order{\isacharcomma}\ order{\isacharparenright}\ order\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}x\ {\isasymle}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isasymle}\ snd\ y{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}x\ {\isacharless}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isacharless}\ snd\ y{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
\ \isacommand{proof}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp{\isacharcolon}\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}prod{\isacharunderscore}def\ intro{\isacharcolon}\ order{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}\isanewline
\isanewline
\isacommand{end}\isamarkupfalse%
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ order{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}order{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
\ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}order{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
\ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\begin{isamarkuptext}%
\noindent Then code generation will fail.  Why?  The definition
  of \isa{op\ {\isasymle}} depends on equality on both arguments,
  which are polymorphic and impose an additional \isa{eq}
  class constraint, which the preprocessor does not propagate
  (for technical reasons).

  The solution is to add \isa{eq} explicitly to the first sort arguments in the
  code theorems:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
\isacommand{lemma}\isamarkupfalse%
\ order{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}order{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
\ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}order{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
\ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\begin{isamarkuptext}%
\noindent Then code generation succeeds:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
%
\begin{isamarkuptext}%
\isaverbatim%
\noindent%
\verb|structure Example = |\newline%
\verb|struct|\newline%
\newline%
\verb|type 'a eq = {eq : 'a -> 'a -> bool};|\newline%
\verb|fun eq (A_:'a eq) = #eq A_;|\newline%
\newline%
\verb|type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};|\newline%
\verb|fun less_eq (A_:'a ord) = #less_eq A_;|\newline%
\verb|fun less (A_:'a ord) = #less A_;|\newline%
\newline%
\verb|fun eqop A_ a b = eq A_ a b;|\newline%
\newline%
\verb|type 'a preorder = {Orderings__ord_preorder : 'a ord};|\newline%
\verb|fun ord_preorder (A_:'a preorder) = #Orderings__ord_preorder A_;|\newline%
\newline%
\verb|type 'a order = {Orderings__preorder_order : 'a preorder};|\newline%
\verb|fun preorder_order (A_:'a order) = #Orderings__preorder_order A_;|\newline%
\newline%
\verb|fun less_eqa (A1_, A2_) B_ (x1, y1) (x2, y2) =|\newline%
\verb|  less ((ord_preorder o preorder_order) A2_) x1 x2 orelse|\newline%
\verb|    eqop A1_ x1 x2 andalso|\newline%
\verb|      less_eq ((ord_preorder o preorder_order) B_) y1 y2|\newline%
\verb|  |\verb,|,\verb| less_eqa (A1_, A2_) B_ (x1, y1) (x2, y2) =|\newline%
\verb|    less ((ord_preorder o preorder_order) A2_) x1 x2 orelse|\newline%
\verb|      eqop A1_ x1 x2 andalso|\newline%
\verb|        less_eq ((ord_preorder o preorder_order) B_) y1 y2;|\newline%
\newline%
\verb|end; (*struct Example*)|%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\begin{isamarkuptext}%
In some cases, the automatically derived defining equations
  for equality on a particular type may not be appropriate.
  As example, watch the following datatype representing
  monomorphic parametric types (where type constructors
  are referred to by natural numbers):%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
\isacommand{datatype}\isamarkupfalse%
\ monotype\ {\isacharequal}\ Mono\ nat\ {\isachardoublequoteopen}monotype\ list{\isachardoublequoteclose}%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
Then code generation for SML would fail with a message
  that the generated code contains illegal mutual dependencies:
  the theorem \isa{Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}\ {\isacharequal}\ Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}\ {\isasymequiv}\ tyco{\isadigit{1}}\ {\isacharequal}\ tyco{\isadigit{2}}\ {\isasymand}\ typargs{\isadigit{1}}\ {\isacharequal}\ typargs{\isadigit{2}}} already requires the
  instance \isa{monotype\ {\isasymColon}\ eq}, which itself requires
  \isa{Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}\ {\isacharequal}\ Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}\ {\isasymequiv}\ tyco{\isadigit{1}}\ {\isacharequal}\ tyco{\isadigit{2}}\ {\isasymand}\ typargs{\isadigit{1}}\ {\isacharequal}\ typargs{\isadigit{2}}};  Haskell has no problem with mutually
  recursive \isa{inst} and \isa{fun} definitions,
  but the SML serializer does not support this.

  In such cases, you have to provide your own equality equations
  involving auxiliary constants.  In our case,
  \isa{list{\isacharunderscore}all{\isadigit{2}}} can do the job:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
\isacommand{lemma}\isamarkupfalse%
\ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
\ \ \ \ \ tyco{\isadigit{1}}\ {\isacharequal}\ tyco{\isadigit{2}}\ {\isasymand}\ list{\isacharunderscore}all{\isadigit{2}}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq\ list{\isacharunderscore}all{\isadigit{2}}{\isacharunderscore}eq\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\begin{isamarkuptext}%
\noindent does not depend on instance \isa{monotype\ {\isasymColon}\ eq}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isatagquoteme
%
\begin{isamarkuptext}%
\isaverbatim%
\noindent%
\verb|structure Example = |\newline%
\verb|struct|\newline%
\newline%
\verb|type 'a eq = {eq : 'a -> 'a -> bool};|\newline%
\verb|fun eq (A_:'a eq) = #eq A_;|\newline%
\newline%
\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
\newline%
\verb|fun eqop A_ a b = eq A_ a b;|\newline%
\newline%
\verb|fun null (x :: xs) = false|\newline%
\verb|  |\verb,|,\verb| null [] = true;|\newline%
\newline%
\verb|fun eq_nat (Suc a) Zero_nat = false|\newline%
\verb|  |\verb,|,\verb| eq_nat Zero_nat (Suc a) = false|\newline%
\verb|  |\verb,|,\verb| eq_nat (Suc nat) (Suc nat') = eq_nat nat nat'|\newline%
\verb|  |\verb,|,\verb| eq_nat Zero_nat Zero_nat = true;|\newline%
\newline%
\verb|val eq_nata = {eq = eq_nat} : nat eq;|\newline%
\newline%
\verb|datatype monotype = Mono of nat * monotype list;|\newline%
\newline%
\verb|fun list_all2 p (x :: xs) (y :: ys) = p x y andalso list_all2 p xs ys|\newline%
\verb|  |\verb,|,\verb| list_all2 p xs [] = null xs|\newline%
\verb|  |\verb,|,\verb| list_all2 p [] ys = null ys;|\newline%
\newline%
\verb|fun eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =|\newline%
\verb|  eqop eq_nata tyco1 tyco2 andalso|\newline%
\verb|    list_all2 eq_monotype typargs1 typargs2;|\newline%
\newline%
\verb|end; (*struct Example*)|%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagquoteme
{\isafoldquoteme}%
%
\isadelimquoteme
%
\endisadelimquoteme
%
\isamarkupsubsection{Partiality%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, examples: maps%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: