doc-src/Codegen/Thy/document/Introduction.tex

combine quote and typewriter/tt tag

%
\begin{isabellebody}%
\def\isabellecontext{Introduction}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Introduction\isanewline
\isakeyword{imports}\ Setup\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupsection{Introduction%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
This tutorial introduces the code generator facilities of \isa{Isabelle{\isacharslash}HOL}.  It allows to turn (a certain class of) HOL
  specifications into corresponding executable code in the programming
  languages \isa{SML} \cite{SML}, \isa{OCaml} \cite{OCaml},
  \isa{Haskell} \cite{haskell-revised-report} and \isa{Scala}
  \cite{scala-overview-tech-report}.

  To profit from this tutorial, some familiarity and experience with
  \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \cite{isa-tutorial} and its basic theories is assumed.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Code generation principle: shallow embedding \label{sec:principle}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The key concept for understanding Isabelle's code generation is
  \emph{shallow embedding}: logical entities like constants, types and
  classes are identified with corresponding entities in the target
  language.  In particular, the carrier of a generated program's
  semantics are \emph{equational theorems} from the logic.  If we view
  a generated program as an implementation of a higher-order rewrite
  system, then every rewrite step performed by the program can be
  simulated in the logic, which guarantees partial correctness
  \cite{Haftmann-Nipkow:2010:code}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{A quick start with the Isabelle/HOL toolbox \label{sec:queue_example}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
In a HOL theory, the \indexdef{}{command}{datatype}\hypertarget{command.datatype}{\hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}}} and \indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}}/\indexdef{}{command}{primrec}\hypertarget{command.primrec}{\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}}/\indexdef{}{command}{fun}\hypertarget{command.fun}{\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}}} declarations
  form the core of a functional programming language.  By default
  equational theorems stemming from those are used for generated code,
  therefore \qt{naive} code generation can proceed without further
  ado.

  For example, here a simple \qt{implementation} of amortised queues:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{datatype}\isamarkupfalse%
\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{primrec}\isamarkupfalse%
\ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{fun}\isamarkupfalse%
\ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ %
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\isadeliminvisible
%
\endisadeliminvisible
%
\isataginvisible
%
\endisataginvisible
{\isafoldinvisible}%
%
\isadeliminvisible
%
\endisadeliminvisible
%
\begin{isamarkuptext}%
\noindent Then we can generate code e.g.~for \isa{SML} as follows:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
\ empty\ dequeue\ enqueue\ \isakeyword{in}\ SML\isanewline
\ \ \isakeyword{module{\isacharunderscore}name}\ Example\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}example{\isachardot}ML{\isachardoublequoteclose}%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent resulting in the following code:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquotetypewriter
%
\endisadelimquotetypewriter
%
\isatagquotetypewriter
%
\begin{isamarkuptext}%
structure\ Example\ {\isacharcolon}\ sig\isanewline
\ \ val\ id\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
\ \ val\ fold\ {\isacharcolon}\ {\isacharparenleft}{\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b{\isacharparenright}\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\isanewline
\ \ val\ rev\ {\isacharcolon}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\isanewline
\ \ datatype\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ of\ {\isacharprime}a\ list\ {\isacharasterisk}\ {\isacharprime}a\ list\isanewline
\ \ val\ empty\ {\isacharcolon}\ {\isacharprime}a\ queue\isanewline
\ \ val\ dequeue\ {\isacharcolon}\ {\isacharprime}a\ queue\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ option\ {\isacharasterisk}\ {\isacharprime}a\ queue\isanewline
\ \ val\ enqueue\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ queue\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ queue\isanewline
end\ {\isacharequal}\ struct\isanewline
\isanewline
fun\ id\ x\ {\isacharequal}\ {\isacharparenleft}fn\ xa\ {\isacharequal}{\isachargreater}\ xa{\isacharparenright}\ x{\isacharsemicolon}\isanewline
\isanewline
fun\ fold\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ id\isanewline
\ \ {\isacharbar}\ fold\ f\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharparenright}\ {\isacharequal}\ fold\ f\ xs\ o\ f\ x{\isacharsemicolon}\isanewline
\isanewline
fun\ rev\ xs\ {\isacharequal}\ fold\ {\isacharparenleft}fn\ a\ {\isacharequal}{\isachargreater}\ fn\ b\ {\isacharequal}{\isachargreater}\ a\ {\isacharcolon}{\isacharcolon}\ b{\isacharparenright}\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline
\isanewline
datatype\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ of\ {\isacharprime}a\ list\ {\isacharasterisk}\ {\isacharprime}a\ list{\isacharsemicolon}\isanewline
\isanewline
val\ empty\ {\isacharcolon}\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharsemicolon}\isanewline
\isanewline
fun\ dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}NONE{\isacharcomma}\ AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
\ \ {\isacharbar}\ dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}xs{\isacharcomma}\ y\ {\isacharcolon}{\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}SOME\ y{\isacharcomma}\ AQueue\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isacharparenright}\isanewline
\ \ {\isacharbar}\ dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}v\ {\isacharcolon}{\isacharcolon}\ va{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ let\isanewline
\ \ \ \ \ \ val\ y\ {\isacharcolon}{\isacharcolon}\ ys\ {\isacharequal}\ rev\ {\isacharparenleft}v\ {\isacharcolon}{\isacharcolon}\ va{\isacharparenright}{\isacharsemicolon}\isanewline
\ \ \ \ in\isanewline
\ \ \ \ \ \ {\isacharparenleft}SOME\ y{\isacharcomma}\ AQueue\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ ys{\isacharparenright}{\isacharparenright}\isanewline
\ \ \ \ end{\isacharsemicolon}\isanewline
\isanewline
fun\ enqueue\ x\ {\isacharparenleft}AQueue\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharcomma}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline
\isanewline
end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagquotetypewriter
{\isafoldquotetypewriter}%
%
\isadelimquotetypewriter
%
\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent The \indexdef{}{command}{export\_code}\hypertarget{command.export-code}{\hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}} command takes a
  space-separated list of constants for which code shall be generated;
  anything else needed for those is added implicitly.  Then follows a
  target language identifier and a freely chosen module name.  A file
  name denotes the destination to store the generated code.  Note that
  the semantics of the destination depends on the target language: for
  \isa{SML}, \isa{OCaml} and \isa{Scala} it denotes a \emph{file},
  for \isa{Haskell} it denotes a \emph{directory} where a file named as the
  module name (with extension \isa{{\isachardot}hs}) is written:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
\ empty\ dequeue\ enqueue\ \isakeyword{in}\ Haskell\isanewline
\ \ \isakeyword{module{\isacharunderscore}name}\ Example\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}{\isachardoublequoteclose}%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent This is the corresponding code:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquotetypewriter
%
\endisadelimquotetypewriter
%
\isatagquotetypewriter
%
\begin{isamarkuptext}%
module\ Example\ where\ {\isacharbraceleft}\isanewline
\isanewline
data\ Queue\ a\ {\isacharequal}\ AQueue\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharbrackleft}a{\isacharbrackright}{\isacharsemicolon}\isanewline
\isanewline
empty\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a{\isacharsemicolon}\isanewline
empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline
\isanewline
dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Maybe\ a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline
dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Nothing{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharsemicolon}\isanewline
dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Just\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon}\isanewline
dequeue\ {\isacharparenleft}AQueue\ {\isacharparenleft}v\ {\isacharcolon}\ va{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
\ \ let\ {\isacharbraceleft}\isanewline
\ \ \ \ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}\ {\isacharequal}\ reverse\ {\isacharparenleft}v\ {\isacharcolon}\ va{\isacharparenright}{\isacharsemicolon}\isanewline
\ \ {\isacharbraceright}\ in\ {\isacharparenleft}Just\ y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline
\isanewline
enqueue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ a\ {\isacharminus}{\isachargreater}\ Queue\ a\ {\isacharminus}{\isachargreater}\ Queue\ a{\isacharsemicolon}\isanewline
enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharcolon}\ xs{\isacharparenright}\ ys{\isacharsemicolon}\isanewline
\isanewline
{\isacharbraceright}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagquotetypewriter
{\isafoldquotetypewriter}%
%
\isadelimquotetypewriter
%
\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent For more details about \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} see
  \secref{sec:further}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Type classes%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Code can also be generated from type classes in a Haskell-like
  manner.  For illustration here an example from abstract algebra:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{class}\isamarkupfalse%
\ semigroup\ {\isacharequal}\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%
%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent We define the natural operation of the natural numbers
  on monoids:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\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}%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent This we use to define the discrete exponentiation
  function:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\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}%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent The corresponding code in Haskell uses that language's
  native classes:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquotetypewriter
%
\endisadelimquotetypewriter
%
\isatagquotetypewriter
%
\begin{isamarkuptext}%
module\ Example\ where\ {\isacharbraceleft}\isanewline
\isanewline
data\ Nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ Nat{\isacharsemicolon}\isanewline
\isanewline
plus{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
plus{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ plus{\isacharunderscore}nat\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharsemicolon}\isanewline
plus{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ n{\isacharsemicolon}\isanewline
\isanewline
class\ Semigroup\ a\ where\ {\isacharbraceleft}\isanewline
\ \ mult\ {\isacharcolon}{\isacharcolon}\ a\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
{\isacharbraceright}{\isacharsemicolon}\isanewline
\isanewline
class\ {\isacharparenleft}Semigroup\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Monoid\ a\ where\ {\isacharbraceleft}\isanewline
\ \ neutral\ {\isacharcolon}{\isacharcolon}\ a{\isacharsemicolon}\isanewline
{\isacharbraceright}{\isacharsemicolon}\isanewline
\isanewline
pow\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Monoid\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Nat\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
pow\ Zero{\isacharunderscore}nat\ a\ {\isacharequal}\ neutral{\isacharsemicolon}\isanewline
pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ mult\ a\ {\isacharparenleft}pow\ n\ a{\isacharparenright}{\isacharsemicolon}\isanewline
\isanewline
mult{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
mult{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline
mult{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ plus{\isacharunderscore}nat\ n\ {\isacharparenleft}mult{\isacharunderscore}nat\ m\ n{\isacharparenright}{\isacharsemicolon}\isanewline
\isanewline
instance\ Semigroup\ Nat\ where\ {\isacharbraceleft}\isanewline
\ \ mult\ {\isacharequal}\ mult{\isacharunderscore}nat{\isacharsemicolon}\isanewline
{\isacharbraceright}{\isacharsemicolon}\isanewline
\isanewline
neutral{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ Nat{\isacharsemicolon}\isanewline
neutral{\isacharunderscore}nat\ {\isacharequal}\ Suc\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline
\isanewline
instance\ Monoid\ Nat\ where\ {\isacharbraceleft}\isanewline
\ \ neutral\ {\isacharequal}\ neutral{\isacharunderscore}nat{\isacharsemicolon}\isanewline
{\isacharbraceright}{\isacharsemicolon}\isanewline
\isanewline
bexp\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
\isanewline
{\isacharbraceright}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagquotetypewriter
{\isafoldquotetypewriter}%
%
\isadelimquotetypewriter
%
\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent This is a convenient place to show how explicit dictionary
  construction manifests in generated code -- the same example in
  \isa{SML}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquotetypewriter
%
\endisadelimquotetypewriter
%
\isatagquotetypewriter
%
\begin{isamarkuptext}%
structure\ Example\ {\isacharcolon}\ sig\isanewline
\ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline
\ \ val\ plus{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ nat\isanewline
\ \ type\ {\isacharprime}a\ semigroup\isanewline
\ \ val\ mult\ {\isacharcolon}\ {\isacharprime}a\ semigroup\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
\ \ type\ {\isacharprime}a\ monoid\isanewline
\ \ val\ semigroup{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ semigroup\isanewline
\ \ val\ neutral\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
\ \ val\ pow\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
\ \ val\ mult{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ nat\isanewline
\ \ val\ semigroup{\isacharunderscore}nat\ {\isacharcolon}\ nat\ semigroup\isanewline
\ \ val\ neutral{\isacharunderscore}nat\ {\isacharcolon}\ nat\isanewline
\ \ val\ monoid{\isacharunderscore}nat\ {\isacharcolon}\ nat\ monoid\isanewline
\ \ val\ bexp\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\isanewline
end\ {\isacharequal}\ struct\isanewline
\isanewline
datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat{\isacharsemicolon}\isanewline
\isanewline
fun\ plus{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ plus{\isacharunderscore}nat\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\isanewline
\ \ {\isacharbar}\ plus{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ n{\isacharsemicolon}\isanewline
\isanewline
type\ {\isacharprime}a\ semigroup\ {\isacharequal}\ {\isacharbraceleft}mult\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharbraceright}{\isacharsemicolon}\isanewline
val\ mult\ {\isacharequal}\ {\isacharhash}mult\ {\isacharcolon}\ {\isacharprime}a\ semigroup\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharsemicolon}\isanewline
\isanewline
type\ {\isacharprime}a\ monoid\ {\isacharequal}\ {\isacharbraceleft}semigroup{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ semigroup{\isacharcomma}\ neutral\ {\isacharcolon}\ {\isacharprime}a{\isacharbraceright}{\isacharsemicolon}\isanewline
val\ semigroup{\isacharunderscore}monoid\ {\isacharequal}\ {\isacharhash}semigroup{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ semigroup{\isacharsemicolon}\isanewline
val\ neutral\ {\isacharequal}\ {\isacharhash}neutral\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharsemicolon}\isanewline
\isanewline
fun\ pow\ A{\isacharunderscore}\ Zero{\isacharunderscore}nat\ a\ {\isacharequal}\ neutral\ A{\isacharunderscore}\isanewline
\ \ {\isacharbar}\ pow\ A{\isacharunderscore}\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ mult\ {\isacharparenleft}semigroup{\isacharunderscore}monoid\ A{\isacharunderscore}{\isacharparenright}\ a\ {\isacharparenleft}pow\ A{\isacharunderscore}\ n\ a{\isacharparenright}{\isacharsemicolon}\isanewline
\isanewline
fun\ mult{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ n\ {\isacharequal}\ Zero{\isacharunderscore}nat\isanewline
\ \ {\isacharbar}\ mult{\isacharunderscore}nat\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n\ {\isacharequal}\ plus{\isacharunderscore}nat\ n\ {\isacharparenleft}mult{\isacharunderscore}nat\ m\ n{\isacharparenright}{\isacharsemicolon}\isanewline
\isanewline
val\ semigroup{\isacharunderscore}nat\ {\isacharequal}\ {\isacharbraceleft}mult\ {\isacharequal}\ mult{\isacharunderscore}nat{\isacharbraceright}\ {\isacharcolon}\ nat\ semigroup{\isacharsemicolon}\isanewline
\isanewline
val\ neutral{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharequal}\ Suc\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline
\isanewline
val\ monoid{\isacharunderscore}nat\ {\isacharequal}\ {\isacharbraceleft}semigroup{\isacharunderscore}monoid\ {\isacharequal}\ semigroup{\isacharunderscore}nat{\isacharcomma}\ neutral\ {\isacharequal}\ neutral{\isacharunderscore}nat{\isacharbraceright}\isanewline
\ \ {\isacharcolon}\ nat\ monoid{\isacharsemicolon}\isanewline
\isanewline
fun\ bexp\ n\ {\isacharequal}\ pow\ monoid{\isacharunderscore}nat\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
\isanewline
end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagquotetypewriter
{\isafoldquotetypewriter}%
%
\isadelimquotetypewriter
%
\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent Note the parameters with trailing underscore (\verb|A_|), which are the dictionary parameters.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{How to continue from here%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
What you have seen so far should be already enough in a lot of
  cases.  If you are content with this, you can quit reading here.

  Anyway, to understand situations where problems occur or to increase
  the scope of code generation beyond default, it is necessary to gain
  some understanding how the code generator actually works:

  \begin{itemize}

    \item The foundations of the code generator are described in
      \secref{sec:foundations}.

    \item In particular \secref{sec:utterly_wrong} gives hints how to
      debug situations where code generation does not succeed as
      expected.

    \item The scope and quality of generated code can be increased
      dramatically by applying refinement techniques, which are
      introduced in \secref{sec:refinement}.

    \item Inductive predicates can be turned executable using an
      extension of the code generator \secref{sec:inductive}.

    \item You may want to skim over the more technical sections
      \secref{sec:adaptation} and \secref{sec:further}.

    \item For exhaustive syntax diagrams etc. you should visit the
      Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}.

  \end{itemize}

  \bigskip

  \begin{center}\fbox{\fbox{\begin{minipage}{8cm}

    \begin{center}\textit{Happy proving, happy hacking!}\end{center}

  \end{minipage}}}\end{center}

  \begin{warn}
    There is also a more ancient code generator in Isabelle by Stefan
    Berghofer \cite{Berghofer-Nipkow:2002}.  Although its
    functionality is covered by the code generator presented here, it
    will sometimes show up as an artifact.  In case of ambiguity, we
    will refer to the framework described here as \isa{generic\ code\ generator}, to the other as \isa{SML\ code\ generator}.
  \end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: