--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Codegen/Thy/document/Foundations.tex Fri Aug 13 14:41:12 2010 +0200
@@ -0,0 +1,1013 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Foundations}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Foundations\isanewline
+\isakeyword{imports}\ Introduction\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupsection{Code generation foundations \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}}}} and \hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}}
+ statements are used for code generation. This default behaviour
+ can be changed, e.g.\ by providing different code equations.
+ The customisations shown in this section are \emph{safe}
+ as regards correctness: all programs that can be generated are partially
+ correct.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Selecting code equations%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Coming back to our introductory example, we
+ could provide an alternative code equations for \isa{dequeue}
+ explicitly:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
+\ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ 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}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar}
+ \isa{attribute} which states that the given theorems should be
+ considered as code equations for a \isa{fun} statement --
+ the corresponding constant is determined syntactically. The resulting code:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
+\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
+\hspace*{0pt}dequeue (AQueue xs []) =\\
+\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\
+\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\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. See \secref{sec:datatypes} for an example.
+
+ As told in \secref{sec:concept}, code generation is based
+ on a structured collection of code theorems.
+ This collection
+ may be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
+\ dequeue%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent prints a table with \emph{all} code equations
+ for \isa{dequeue}, including
+ \emph{all} code 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 code 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%
+%
+\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%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}module Example where {\char123}\\
+\hspace*{0pt}\\
+\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
+\hspace*{0pt}\\
+\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\
+\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\
+\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\
+\hspace*{0pt}\\
+\hspace*{0pt}class Semigroup a where {\char123}\\
+\hspace*{0pt} ~mult ::~a -> a -> a;\\
+\hspace*{0pt}{\char125};\\
+\hspace*{0pt}\\
+\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\
+\hspace*{0pt} ~neutral ::~a;\\
+\hspace*{0pt}{\char125};\\
+\hspace*{0pt}\\
+\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\
+\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
+\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
+\hspace*{0pt}\\
+\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\
+\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\
+\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
+\hspace*{0pt}\\
+\hspace*{0pt}neutral{\char95}nat ::~Nat;\\
+\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\
+\hspace*{0pt}\\
+\hspace*{0pt}instance Semigroup Nat where {\char123}\\
+\hspace*{0pt} ~mult = mult{\char95}nat;\\
+\hspace*{0pt}{\char125};\\
+\hspace*{0pt}\\
+\hspace*{0pt}instance Monoid Nat where {\char123}\\
+\hspace*{0pt} ~neutral = neutral{\char95}nat;\\
+\hspace*{0pt}{\char125};\\
+\hspace*{0pt}\\
+\hspace*{0pt}bexp ::~Nat -> Nat;\\
+\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
+\hspace*{0pt}\\
+\hspace*{0pt}{\char125}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\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})
+ \cite{Haftmann-Nipkow:2010:code}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}structure Example :~sig\\
+\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
+\hspace*{0pt} ~val plus{\char95}nat :~nat -> nat -> nat\\
+\hspace*{0pt} ~type 'a semigroup\\
+\hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\
+\hspace*{0pt} ~type 'a monoid\\
+\hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid -> 'a semigroup\\
+\hspace*{0pt} ~val neutral :~'a monoid -> 'a\\
+\hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\
+\hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\
+\hspace*{0pt} ~val neutral{\char95}nat :~nat\\
+\hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\
+\hspace*{0pt} ~val monoid{\char95}nat :~nat monoid\\
+\hspace*{0pt} ~val bexp :~nat -> nat\\
+\hspace*{0pt}end = struct\\
+\hspace*{0pt}\\
+\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\
+\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
+\hspace*{0pt}\\
+\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
+\hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\
+\hspace*{0pt}\\
+\hspace*{0pt}type 'a monoid = {\char123}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\
+\hspace*{0pt}val semigroup{\char95}monoid = {\char35}semigroup{\char95}monoid :~'a monoid -> 'a semigroup;\\
+\hspace*{0pt}val neutral = {\char35}neutral :~'a monoid -> 'a;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\
+\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\
+\hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
+\hspace*{0pt}\\
+\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\
+\hspace*{0pt}\\
+\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
+\hspace*{0pt}\\
+\hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\
+\hspace*{0pt} ~:~nat monoid;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
+\hspace*{0pt}\\
+\hspace*{0pt}end;~(*struct Example*)%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\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} can apply the full generality of the
+ Isabelle simplifier. Due to the interpretation of theorems as code
+ 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{unfold theorems}, which may be declared and removed using
+ the \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} or \emph{\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} del}
+ attribute, respectively.
+
+ Some common applications:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{itemize}
+%
+\begin{isamarkuptext}%
+\item replacing non-executable constructs by executable ones:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ List{\isachardot}member\ xs\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}fact\ in{\isacharunderscore}set{\isacharunderscore}member{\isacharparenright}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\item eliminating superfluous constants:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}fact\ One{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\item replacing executable but inconvenient constructs:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}fact\ eq{\isacharunderscore}Nil{\isacharunderscore}null{\isacharparenright}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\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-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} command.
+ \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient
+ mechanism to inspect the impact of a preprocessor setup
+ on code equations.
+
+ \begin{warn}
+
+ Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the
+ preprocessor of the ancient \isa{SML\ code\ generator}; in case
+ this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} instead.
+ \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 exactly 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 is appropriate to alter or extend this table. As
+ an example, we will develop an alternative representation of the
+ queue example given in \secref{sec:intro}. The amortised
+ representation is convenient for generating code but exposes its
+ \qt{implementation} details, which may be cumbersome when proving
+ theorems about it. Therefore, here is a simple, straightforward
+ representation of queues:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{datatype}\isamarkupfalse%
+\ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\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}Queue\ xs{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\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}Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ x{\isacharcomma}\ Queue\ xs{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent This we can use directly for proving; for executing,
+ we provide an alternative characterisation:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{definition}\isamarkupfalse%
+\ AQueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}AQueue\ xs\ ys\ {\isacharequal}\ Queue\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
+\ AQueue%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent Here we define a \qt{constructor} \isa{AQueue} which
+ is defined in terms of \isa{Queue} and interprets its arguments
+ according to what the \emph{content} of an amortised queue is supposed
+ to be. Equipped with this, we are able to prove the following equations
+ for our primitive queue operations which \qt{implement} the simple
+ queues in an amortised fashion:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ empty{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{unfolding}\isamarkupfalse%
+\ AQueue{\isacharunderscore}def\ empty{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ enqueue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{unfolding}\isamarkupfalse%
+\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
+\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{unfolding}\isamarkupfalse%
+\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ simp{\isacharunderscore}all%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent For completeness, we provide a substitute for the
+ \isa{case} combinator on queues:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ queue{\isacharunderscore}case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{unfolding}\isamarkupfalse%
+\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ simp%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent The resulting code looks as expected:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}structure Example :~sig\\
+\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\
+\hspace*{0pt} ~val rev :~'a list -> 'a list\\
+\hspace*{0pt} ~val null :~'a list -> bool\\
+\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
+\hspace*{0pt} ~val empty :~'a queue\\
+\hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\
+\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
+\hspace*{0pt}end = struct\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun foldl f a [] = a\\
+\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun null [] = true\\
+\hspace*{0pt} ~| null (x ::~xs) = false;\\
+\hspace*{0pt}\\
+\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
+\hspace*{0pt}\\
+\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
+\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\
+\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\
+\hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
+\hspace*{0pt}\\
+\hspace*{0pt}end;~(*struct Example*)%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent From this example, it can be 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 alternative equations for the \isa{case} combinator.
+
+ \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.
+
+ \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%
+%
+\isamarkupsubsection{Equality%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Surely you have already noticed how equality is treated
+ by the code generator:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\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}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent During preprocessing, the membership test is rewritten,
+ resulting in \isa{List{\isachardot}member}, which itself
+ performs an explicit equality check.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}structure Example :~sig\\
+\hspace*{0pt} ~type 'a eq\\
+\hspace*{0pt} ~val eq :~'a eq -> 'a -> 'a -> bool\\
+\hspace*{0pt} ~val eqa :~'a eq -> 'a -> 'a -> bool\\
+\hspace*{0pt} ~val member :~'a eq -> 'a list -> 'a -> bool\\
+\hspace*{0pt} ~val collect{\char95}duplicates :\\
+\hspace*{0pt} ~~~'a eq -> 'a list -> 'a list -> 'a list -> 'a list\\
+\hspace*{0pt}end = struct\\
+\hspace*{0pt}\\
+\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
+\hspace*{0pt}val eq = {\char35}eq :~'a eq -> 'a -> 'a -> bool;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun member A{\char95}~[] y = false\\
+\hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eqa A{\char95}~x y orelse member A{\char95}~xs y;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
+\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
+\hspace*{0pt} ~~~(if member A{\char95}~xs z\\
+\hspace*{0pt} ~~~~~then (if member A{\char95}~ys z then collect{\char95}duplicates A{\char95}~xs ys zs\\
+\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
+\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
+\hspace*{0pt}\\
+\hspace*{0pt}end;~(*struct Example*)%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\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 code 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.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Explicit partiality%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Partiality usually enters the game by partial patterns, as
+ in the following example, again for amortised queues:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{definition}\isamarkupfalse%
+\ strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\isanewline
+\ \ \ \ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ strict{\isacharunderscore}dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent In the corresponding code, there is no equation
+ for the pattern \isa{AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
+\hspace*{0pt} ~let {\char123}\\
+\hspace*{0pt} ~~~(y :~ys) = reverse xs;\\
+\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent In some cases it is desirable to have this
+ pseudo-\qt{partiality} more explicitly, e.g.~as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{axiomatization}\isamarkupfalse%
+\ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isacharbar}\ {\isacharunderscore}\ {\isasymRightarrow}\ empty{\isacharunderscore}queue{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline
+\ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}}, the unspecified constant \isa{empty{\isacharunderscore}queue} occurs.
+
+ Normally, if constants without any code equations occur in a
+ program, the code generator complains (since in most cases this is
+ indeed an error). But such constants can also be thought
+ of as function definitions which always fail,
+ since there is never a successful pattern match on the left hand
+ side. In order to categorise a constant into that category
+ explicitly, use \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{code{\isacharunderscore}abort}\isamarkupfalse%
+\ empty{\isacharunderscore}queue%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent Then the code generator will just insert an error or
+ exception at the appropriate position:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
+\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
+\hspace*{0pt}\\
+\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
+\hspace*{0pt} ~(if null xs then empty{\char95}queue\\
+\hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent This feature however is rarely needed in practice.
+ Note also that the \isa{HOL} default setup already declares
+ \isa{undefined} as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most
+ likely to be used in such situations.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- a/doc-src/Codegen/Thy/document/ML.tex Fri Aug 13 14:40:15 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,240 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{ML}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\isanewline
-\isakeyword{imports}\ Setup\isanewline
-\isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isamarkupsection{ML system interfaces \label{sec:ml}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Since the code generator framework not only aims to provide
- a nice Isar interface but also to form a base for
- code-generation-based applications, here a short
- description of the most important ML interfaces.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Executable theory content: \isa{Code}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-This Pure module implements the core notions of
- executable content of a theory.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Managing executable content%
-}
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
- \indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
- \indexdef{}{ML}{Code\_Preproc.map\_pre}\verb|Code_Preproc.map_pre: (simpset -> simpset) -> theory -> theory| \\
- \indexdef{}{ML}{Code\_Preproc.map\_post}\verb|Code_Preproc.map_post: (simpset -> simpset) -> theory -> theory| \\
- \indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
-\verb| -> theory -> theory| \\
- \indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\
- \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
- \indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline%
-\verb| -> (string * sort) list * ((string * string list) * typ list) list| \\
- \indexdef{}{ML}{Code.get\_type\_of\_constr\_or\_abstr}\verb|Code.get_type_of_constr_or_abstr: theory -> string -> (string * bool) option|
- \end{mldecls}
-
- \begin{description}
-
- \item \verb|Code.add_eqn|~\isa{thm}~\isa{thy} adds function
- theorem \isa{thm} to executable content.
-
- \item \verb|Code.del_eqn|~\isa{thm}~\isa{thy} removes function
- theorem \isa{thm} from executable content, if present.
-
- \item \verb|Code_Preproc.map_pre|~\isa{f}~\isa{thy} changes
- the preprocessor simpset.
-
- \item \verb|Code_Preproc.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
- function transformer \isa{f} (named \isa{name}) to executable content;
- \isa{f} is a transformer of the code equations belonging
- to a certain function definition, depending on the
- current theory context. Returning \isa{NONE} indicates that no
- transformation took place; otherwise, the whole process will be iterated
- with the new code equations.
-
- \item \verb|Code_Preproc.del_functrans|~\isa{name}~\isa{thy} removes
- function transformer named \isa{name} from executable content.
-
- \item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds
- a datatype to executable content, with generation
- set \isa{cs}.
-
- \item \verb|Code.get_type_of_constr_or_abstr|~\isa{thy}~\isa{const}
- returns type constructor corresponding to
- constructor \isa{const}; returns \isa{NONE}
- if \isa{const} is no constructor.
-
- \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isamarkupsubsection{Auxiliary%
-}
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string|
- \end{mldecls}
-
- \begin{description}
-
- \item \verb|Code.read_const|~\isa{thy}~\isa{s}
- reads a constant as a concrete term expression \isa{s}.
-
- \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isamarkupsubsection{Implementing code generator applications%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Implementing code generator applications on top
- of the framework set out so far usually not only
- involves using those primitive interfaces
- but also storing code-dependent data and various
- other things.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Data depending on the theory's executable content%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Due to incrementality of code generation, changes in the
- theory's executable content have to be propagated in a
- certain fashion. Additionally, such changes may occur
- not only during theory extension but also during theory
- merge, which is a little bit nasty from an implementation
- point of view. The framework provides a solution
- to this technical challenge by providing a functorial
- data slot \verb|Code_Data|; on instantiation
- of this functor, the following types and operations
- are required:
-
- \medskip
- \begin{tabular}{l}
- \isa{type\ T} \\
- \isa{val\ empty{\isacharcolon}\ T} \\
- \isa{val\ purge{\isacharcolon}\ theory\ {\isasymrightarrow}\ string\ list\ option\ {\isasymrightarrow}\ T\ {\isasymrightarrow}\ T}
- \end{tabular}
-
- \begin{description}
-
- \item \isa{T} the type of data to store.
-
- \item \isa{empty} initial (empty) data.
-
- \item \isa{purge}~\isa{thy}~\isa{consts} propagates changes in executable content;
- \isa{consts} indicates the kind
- of change: \verb|NONE| stands for a fundamental change
- which invalidates any existing code, \isa{SOME\ consts}
- hints that executable content for constants \isa{consts}
- has changed.
-
- \end{description}
-
- \noindent An instance of \verb|Code_Data| provides the following
- interface:
-
- \medskip
- \begin{tabular}{l}
- \isa{get{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} \\
- \isa{change{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ T} \\
- \isa{change{\isacharunderscore}yield{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T{\isacharparenright}\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T}
- \end{tabular}
-
- \begin{description}
-
- \item \isa{get} retrieval of the current data.
-
- \item \isa{change} update of current data (cached!)
- by giving a continuation.
-
- \item \isa{change{\isacharunderscore}yield} update with side result.
-
- \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\bigskip
-
- \emph{Happy proving, happy hacking!}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/Codegen/Thy/document/Program.tex Fri Aug 13 14:40:15 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1013 +0,0 @@
-%
-\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}}}} and \hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}}
- statements are used for code generation. This default behaviour
- can be changed, e.g.\ by providing different code equations.
- The customisations shown in this section are \emph{safe}
- as regards correctness: all programs that can be generated are partially
- correct.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Selecting code equations%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Coming back to our introductory example, we
- could provide an alternative code equations for \isa{dequeue}
- explicitly:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
-\ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ 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}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar}
- \isa{attribute} which states that the given theorems should be
- considered as code equations for a \isa{fun} statement --
- the corresponding constant is determined syntactically. The resulting code:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-%
-\begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
-\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
-\hspace*{0pt}dequeue (AQueue xs []) =\\
-\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\
-\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\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. See \secref{sec:datatypes} for an example.
-
- As told in \secref{sec:concept}, code generation is based
- on a structured collection of code theorems.
- This collection
- may be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
-\ dequeue%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent prints a table with \emph{all} code equations
- for \isa{dequeue}, including
- \emph{all} code 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 code 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%
-%
-\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%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-%
-\begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}module Example where {\char123}\\
-\hspace*{0pt}\\
-\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}class Semigroup a where {\char123}\\
-\hspace*{0pt} ~mult ::~a -> a -> a;\\
-\hspace*{0pt}{\char125};\\
-\hspace*{0pt}\\
-\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\
-\hspace*{0pt} ~neutral ::~a;\\
-\hspace*{0pt}{\char125};\\
-\hspace*{0pt}\\
-\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\
-\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
-\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
-\hspace*{0pt}\\
-\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\
-\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\
-\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\
-\hspace*{0pt}\\
-\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\
-\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\
-\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
-\hspace*{0pt}\\
-\hspace*{0pt}neutral{\char95}nat ::~Nat;\\
-\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}instance Semigroup Nat where {\char123}\\
-\hspace*{0pt} ~mult = mult{\char95}nat;\\
-\hspace*{0pt}{\char125};\\
-\hspace*{0pt}\\
-\hspace*{0pt}instance Monoid Nat where {\char123}\\
-\hspace*{0pt} ~neutral = neutral{\char95}nat;\\
-\hspace*{0pt}{\char125};\\
-\hspace*{0pt}\\
-\hspace*{0pt}bexp ::~Nat -> Nat;\\
-\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
-\hspace*{0pt}\\
-\hspace*{0pt}{\char125}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\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})
- \cite{Haftmann-Nipkow:2010:code}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-%
-\begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
-\hspace*{0pt} ~type 'a semigroup\\
-\hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\
-\hspace*{0pt} ~type 'a monoid\\
-\hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid -> 'a semigroup\\
-\hspace*{0pt} ~val neutral :~'a monoid -> 'a\\
-\hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\
-\hspace*{0pt} ~val plus{\char95}nat :~nat -> nat -> nat\\
-\hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\
-\hspace*{0pt} ~val neutral{\char95}nat :~nat\\
-\hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\
-\hspace*{0pt} ~val monoid{\char95}nat :~nat monoid\\
-\hspace*{0pt} ~val bexp :~nat -> nat\\
-\hspace*{0pt}end = struct\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
-\hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\
-\hspace*{0pt}\\
-\hspace*{0pt}type 'a monoid = {\char123}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\
-\hspace*{0pt}val semigroup{\char95}monoid = {\char35}semigroup{\char95}monoid :~'a monoid -> 'a semigroup;\\
-\hspace*{0pt}val neutral = {\char35}neutral :~'a monoid -> 'a;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\
-\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\
-\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\
-\hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
-\hspace*{0pt}\\
-\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
-\hspace*{0pt}\\
-\hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\
-\hspace*{0pt} ~:~nat monoid;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
-\hspace*{0pt}\\
-\hspace*{0pt}end;~(*struct Example*)%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\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} can apply the full generality of the
- Isabelle simplifier. Due to the interpretation of theorems as code
- 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{unfold theorems}, which may be declared and removed using
- the \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} or \emph{\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} del}
- attribute, respectively.
-
- Some common applications:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{itemize}
-%
-\begin{isamarkuptext}%
-\item replacing non-executable constructs by executable ones:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ List{\isachardot}member\ xs\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}fact\ in{\isacharunderscore}set{\isacharunderscore}member{\isacharparenright}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\item eliminating superfluous constants:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}fact\ One{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\item replacing executable but inconvenient constructs:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}fact\ eq{\isacharunderscore}Nil{\isacharunderscore}null{\isacharparenright}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\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-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} command.
- \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient
- mechanism to inspect the impact of a preprocessor setup
- on code equations.
-
- \begin{warn}
-
- Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the
- preprocessor of the ancient \isa{SML\ code\ generator}; in case
- this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} instead.
- \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 exactly 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 is appropriate to alter or extend this table. As
- an example, we will develop an alternative representation of the
- queue example given in \secref{sec:intro}. The amortised
- representation is convenient for generating code but exposes its
- \qt{implementation} details, which may be cumbersome when proving
- theorems about it. Therefore, here is a simple, straightforward
- representation of queues:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{datatype}\isamarkupfalse%
-\ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\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}Queue\ xs{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\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}Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ x{\isacharcomma}\ Queue\ xs{\isacharparenright}{\isachardoublequoteclose}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent This we can use directly for proving; for executing,
- we provide an alternative characterisation:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{definition}\isamarkupfalse%
-\ AQueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}AQueue\ xs\ ys\ {\isacharequal}\ Queue\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
-\ AQueue%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent Here we define a \qt{constructor} \isa{AQueue} which
- is defined in terms of \isa{Queue} and interprets its arguments
- according to what the \emph{content} of an amortised queue is supposed
- to be. Equipped with this, we are able to prove the following equations
- for our primitive queue operations which \qt{implement} the simple
- queues in an amortised fashion:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{lemma}\isamarkupfalse%
-\ empty{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{unfolding}\isamarkupfalse%
-\ AQueue{\isacharunderscore}def\ empty{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ enqueue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{unfolding}\isamarkupfalse%
-\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
-\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{unfolding}\isamarkupfalse%
-\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
-\ simp{\isacharunderscore}all%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent For completeness, we provide a substitute for the
- \isa{case} combinator on queues:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{lemma}\isamarkupfalse%
-\ queue{\isacharunderscore}case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{unfolding}\isamarkupfalse%
-\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
-\ simp%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent The resulting code looks as expected:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-%
-\begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\
-\hspace*{0pt} ~val rev :~'a list -> 'a list\\
-\hspace*{0pt} ~val null :~'a list -> bool\\
-\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
-\hspace*{0pt} ~val empty :~'a queue\\
-\hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\
-\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
-\hspace*{0pt}end = struct\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun foldl f a [] = a\\
-\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun null [] = true\\
-\hspace*{0pt} ~| null (x ::~xs) = false;\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
-\hspace*{0pt}\\
-\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
-\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\
-\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\
-\hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
-\hspace*{0pt}\\
-\hspace*{0pt}end;~(*struct Example*)%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent From this example, it can be 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 alternative equations for the \isa{case} combinator.
-
- \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.
-
- \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%
-%
-\isamarkupsubsection{Equality%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Surely you have already noticed how equality is treated
- by the code generator:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\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}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent During preprocessing, the membership test is rewritten,
- resulting in \isa{List{\isachardot}member}, which itself
- performs an explicit equality check.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-%
-\begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~type 'a eq\\
-\hspace*{0pt} ~val eq :~'a eq -> 'a -> 'a -> bool\\
-\hspace*{0pt} ~val eqa :~'a eq -> 'a -> 'a -> bool\\
-\hspace*{0pt} ~val member :~'a eq -> 'a list -> 'a -> bool\\
-\hspace*{0pt} ~val collect{\char95}duplicates :\\
-\hspace*{0pt} ~~~'a eq -> 'a list -> 'a list -> 'a list -> 'a list\\
-\hspace*{0pt}end = struct\\
-\hspace*{0pt}\\
-\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
-\hspace*{0pt}val eq = {\char35}eq :~'a eq -> 'a -> 'a -> bool;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun member A{\char95}~[] y = false\\
-\hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eqa A{\char95}~x y orelse member A{\char95}~xs y;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
-\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
-\hspace*{0pt} ~~~(if member A{\char95}~xs z\\
-\hspace*{0pt} ~~~~~then (if member A{\char95}~ys z then collect{\char95}duplicates A{\char95}~xs ys zs\\
-\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
-\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
-\hspace*{0pt}\\
-\hspace*{0pt}end;~(*struct Example*)%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\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 code 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.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Explicit partiality%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Partiality usually enters the game by partial patterns, as
- in the following example, again for amortised queues:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{definition}\isamarkupfalse%
-\ strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\isanewline
-\ \ \ \ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ strict{\isacharunderscore}dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent In the corresponding code, there is no equation
- for the pattern \isa{AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-%
-\begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
-\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
-\hspace*{0pt} ~let {\char123}\\
-\hspace*{0pt} ~~~(y :~ys) = reverse xs;\\
-\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
-\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent In some cases it is desirable to have this
- pseudo-\qt{partiality} more explicitly, e.g.~as follows:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{axiomatization}\isamarkupfalse%
-\ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isacharbar}\ {\isacharunderscore}\ {\isasymRightarrow}\ empty{\isacharunderscore}queue{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline
-\ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}}, the unspecified constant \isa{empty{\isacharunderscore}queue} occurs.
-
- Normally, if constants without any code equations occur in a
- program, the code generator complains (since in most cases this is
- indeed an error). But such constants can also be thought
- of as function definitions which always fail,
- since there is never a successful pattern match on the left hand
- side. In order to categorise a constant into that category
- explicitly, use \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{code{\isacharunderscore}abort}\isamarkupfalse%
-\ empty{\isacharunderscore}queue%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent Then the code generator will just insert an error or
- exception at the appropriate position:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-%
-\begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
-\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
-\hspace*{0pt}\\
-\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
-\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
-\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
-\hspace*{0pt} ~(if null xs then empty{\char95}queue\\
-\hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent This feature however is rarely needed in practice.
- Note also that the \isa{HOL} default setup already declares
- \isa{undefined} as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most
- likely to be used in such situations.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Codegen/Thy/document/Refinement.tex Fri Aug 13 14:41:12 2010 +0200
@@ -0,0 +1,43 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Refinement}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Refinement\isanewline
+\isakeyword{imports}\ Setup\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupsection{Program and datatype refinement \label{sec:refinement}%
+}
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: