%

\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}\isanewline

\ \ \ \ \ \ \ 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|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)));|%

\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) = eqop A_ x y orelse 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}%

\noindent Then code generation for SML would fail with a message

  that the generated code contains illegal mutual dependencies:

  the theorem \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymequiv}\ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}} already requires the

  instance \isa{monotype\ {\isasymColon}\ eq}, which itself requires