3 \def\isabellecontext{Program}%
10 \isacommand{theory}\isamarkupfalse%
12 \isakeyword{imports}\ Introduction\isanewline
21 \isamarkupsection{Turning Theories into Programs \label{sec:program}%
25 \isamarkupsubsection{The \isa{Isabelle{\isacharslash}HOL} default setup%
29 \begin{isamarkuptext}%
30 We have already seen how by default equations stemming from
31 \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}/\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}/\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}}
32 statements are used for code generation. This default behaviour
33 can be changed, e.g. by providing different defining equations.
34 All kinds of customisation shown in this section is \emph{safe}
35 in the sense that the user does not have to worry about
36 correctness -- all programs generatable that way are partially
41 \isamarkupsubsection{Selecting code equations%
45 \begin{isamarkuptext}%
46 Coming back to our introductory example, we
47 could provide an alternative defining equations for \isa{dequeue}
57 \isacommand{lemma}\isamarkupfalse%
58 \ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
59 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
60 \ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
61 \ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
62 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
63 \ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ Queue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
64 \ \ \isacommand{by}\isamarkupfalse%
65 \ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
73 \begin{isamarkuptext}%
74 \noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar}
75 \isa{attribute} which states that the given theorems should be
76 considered as defining equations for a \isa{fun} statement --
77 the corresponding constant is determined syntactically. The resulting code:%
87 \begin{isamarkuptext}%
90 \hspace*{0pt}dequeue ::~forall a. Queue a -> (Maybe a, Queue a);\\
91 \hspace*{0pt}dequeue (Queue xs (y :~ys)) = (Just y, Queue xs ys);\\
92 \hspace*{0pt}dequeue (Queue xs []) =\\
93 \hspace*{0pt} ~(if nulla xs then (Nothing, Queue [] [])\\
94 \hspace*{0pt} ~~~else dequeue (Queue [] (rev xs)));%
105 \begin{isamarkuptext}%
106 \noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has been
107 replaced by the predicate \isa{null\ xs}. This is due to the default
108 setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).
110 Changing the default constructor set of datatypes is also
111 possible but rarely desired in practice. See \secref{sec:datatypes} for an example.
113 As told in \secref{sec:concept}, code generation is based
114 on a structured collection of code theorems.
115 For explorative purpose, this collection
116 may be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:%
125 \isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
134 \begin{isamarkuptext}%
135 \noindent prints a table with \emph{all} defining equations
136 for \isa{dequeue}, including
137 \emph{all} defining equations those equations depend
140 Similarly, the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command shows a graph
141 visualising dependencies between defining equations.%
145 \isamarkupsubsection{\isa{class} and \isa{instantiation}%
149 \begin{isamarkuptext}%
150 Concerning type classes and code generation, let us examine an example
151 from abstract algebra:%
160 \isacommand{class}\isamarkupfalse%
161 \ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline
162 \ \ \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
163 \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
165 \isacommand{class}\isamarkupfalse%
166 \ monoid\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
167 \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
168 \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
169 \ \ \ \ \isakeyword{and}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
171 \isacommand{instantiation}\isamarkupfalse%
172 \ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline
173 \isakeyword{begin}\isanewline
175 \isacommand{primrec}\isamarkupfalse%
176 \ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
177 \ \ \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymotimes}\ n\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
178 \ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m\ {\isasymotimes}\ n{\isachardoublequoteclose}\isanewline
180 \isacommand{definition}\isamarkupfalse%
181 \ neutral{\isacharunderscore}nat\ \isakeyword{where}\isanewline
182 \ \ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
184 \isacommand{lemma}\isamarkupfalse%
185 \ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharcolon}\isanewline
186 \ \ \isakeyword{fixes}\ n\ m\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
187 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ m{\isacharparenright}\ {\isasymotimes}\ q\ {\isacharequal}\ n\ {\isasymotimes}\ q\ {\isacharplus}\ m\ {\isasymotimes}\ q{\isachardoublequoteclose}\isanewline
188 \ \ \isacommand{by}\isamarkupfalse%
189 \ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
191 \isacommand{instance}\isamarkupfalse%
192 \ \isacommand{proof}\isamarkupfalse%
194 \ \ \isacommand{fix}\isamarkupfalse%
195 \ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
196 \ \ \isacommand{show}\isamarkupfalse%
197 \ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
198 \ \ \ \ \isacommand{by}\isamarkupfalse%
199 \ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharparenright}\isanewline
200 \ \ \isacommand{show}\isamarkupfalse%
201 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
202 \ \ \ \ \isacommand{by}\isamarkupfalse%
203 \ {\isacharparenleft}simp\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
204 \ \ \isacommand{show}\isamarkupfalse%
205 \ {\isachardoublequoteopen}m\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
206 \ \ \ \ \isacommand{by}\isamarkupfalse%
207 \ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
208 \isacommand{qed}\isamarkupfalse%
211 \isacommand{end}\isamarkupfalse%
220 \begin{isamarkuptext}%
221 \noindent We define the natural operation of the natural numbers
231 \isacommand{primrec}\isamarkupfalse%
232 \ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
233 \ \ \ \ {\isachardoublequoteopen}pow\ {\isadigit{0}}\ a\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
234 \ \ {\isacharbar}\ {\isachardoublequoteopen}pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ a\ {\isasymotimes}\ pow\ n\ a{\isachardoublequoteclose}%
242 \begin{isamarkuptext}%
243 \noindent This we use to define the discrete exponentiation function:%
252 \isacommand{definition}\isamarkupfalse%
253 \ bexp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
254 \ \ {\isachardoublequoteopen}bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
262 \begin{isamarkuptext}%
263 \noindent The corresponding code:%
273 \begin{isamarkuptext}%
276 \hspace*{0pt}module Example where {\char123}\\
279 \hspace*{0pt}data Nat = Suc Nat | Zero{\char95}nat;\\
281 \hspace*{0pt}class Semigroup a where {\char123}\\
282 \hspace*{0pt} ~mult ::~a -> a -> a;\\
283 \hspace*{0pt}{\char125};\\
285 \hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\
286 \hspace*{0pt} ~neutral ::~a;\\
287 \hspace*{0pt}{\char125};\\
289 \hspace*{0pt}pow ::~forall a. (Monoid a) => Nat -> a -> a;\\
290 \hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
291 \hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
293 \hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\
294 \hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\
295 \hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\
297 \hspace*{0pt}neutral{\char95}nat ::~Nat;\\
298 \hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\
300 \hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\
301 \hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\
302 \hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
304 \hspace*{0pt}instance Semigroup Nat where {\char123}\\
305 \hspace*{0pt} ~mult = mult{\char95}nat;\\
306 \hspace*{0pt}{\char125};\\
308 \hspace*{0pt}instance Monoid Nat where {\char123}\\
309 \hspace*{0pt} ~neutral = neutral{\char95}nat;\\
310 \hspace*{0pt}{\char125};\\
312 \hspace*{0pt}bexp ::~Nat -> Nat;\\
313 \hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
315 \hspace*{0pt}{\char125}%
326 \begin{isamarkuptext}%
327 \noindent This is a convenient place to show how explicit dictionary construction
328 manifests in generated code (here, the same example in \isa{SML}):%
338 \begin{isamarkuptext}%
341 \hspace*{0pt}structure Example = \\
342 \hspace*{0pt}struct\\
344 \hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
346 \hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
347 \hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\
349 \hspace*{0pt}type 'a monoid = {\char123}Program{\char95}{\char95}semigroup{\char95}monoid :~'a semigroup, neutral :~'a{\char125};\\
350 \hspace*{0pt}fun semigroup{\char95}monoid (A{\char95}:'a monoid) = {\char35}Program{\char95}{\char95}semigroup{\char95}monoid A{\char95};\\
351 \hspace*{0pt}fun neutral (A{\char95}:'a monoid) = {\char35}neutral A{\char95};\\
353 \hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\
354 \hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\
356 \hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\
357 \hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
359 \hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\
361 \hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\
362 \hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
364 \hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
366 \hspace*{0pt}val monoid{\char95}nat =\\
367 \hspace*{0pt} ~{\char123}Program{\char95}{\char95}semigroup{\char95}monoid = semigroup{\char95}nat, neutral = neutral{\char95}nat{\char125}~:\\
368 \hspace*{0pt} ~nat monoid;\\
370 \hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
372 \hspace*{0pt}end; (*struct Example*)%
383 \begin{isamarkuptext}%
384 \noindent Note the parameters with trailing underscore (\verb|A_|)
385 which are the dictionary parameters.%
389 \isamarkupsubsection{The preprocessor \label{sec:preproc}%
393 \begin{isamarkuptext}%
394 Before selected function theorems are turned into abstract
395 code, a chain of definitional transformation steps is carried
396 out: \emph{preprocessing}. In essence, the preprocessor
397 consists of two components: a \emph{simpset} and \emph{function transformers}.
399 The \emph{simpset} allows to employ the full generality of the Isabelle
400 simplifier. Due to the interpretation of theorems
401 as defining equations, rewrites are applied to the right
402 hand side and the arguments of the left hand side of an
403 equation, but never to the constant heading the left hand side.
404 An important special case are \emph{inline theorems} which may be
405 declared and undeclared using the
406 \emph{code inline} or \emph{code inline del} attribute respectively.
408 Some common applications:%
414 \begin{isamarkuptext}%
415 \item replacing non-executable constructs by executable ones:%
424 \isacommand{lemma}\isamarkupfalse%
425 \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
426 \ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
427 \ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
435 \begin{isamarkuptext}%
436 \item eliminating superfluous constants:%
445 \isacommand{lemma}\isamarkupfalse%
446 \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
447 \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
456 \begin{isamarkuptext}%
457 \item replacing executable but inconvenient constructs:%
466 \isacommand{lemma}\isamarkupfalse%
467 \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
468 \ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
469 \ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
479 \begin{isamarkuptext}%
480 \noindent \emph{Function transformers} provide a very general interface,
481 transforming a list of function theorems to another
482 list of function theorems, provided that neither the heading
483 constant nor its type change. The \isa{{\isadigit{0}}} / \isa{Suc}
484 pattern elimination implemented in
485 theory \isa{Efficient{\isacharunderscore}Nat} (see \secref{eff_nat}) uses this
488 \noindent The current setup of the preprocessor may be inspected using
489 the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
490 \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient
491 mechanism to inspect the impact of a preprocessor setup
492 on defining equations.
495 The attribute \emph{code unfold}
496 associated with the \isa{SML\ code\ generator} also applies to
497 the \isa{generic\ code\ generator}:
498 \emph{code unfold} implies \emph{code inline}.
503 \isamarkupsubsection{Datatypes \label{sec:datatypes}%
507 \begin{isamarkuptext}%
508 Conceptually, any datatype is spanned by a set of
509 \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n}
510 where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is exactly the set of \emph{all}
511 type variables in \isa{{\isasymtau}}. The HOL datatype package
512 by default registers any new datatype in the table
513 of datatypes, which may be inspected using
514 the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
516 In some cases, it may be convenient to alter or
517 extend this table; as an example, we will develop an alternative
518 representation of natural numbers as binary digits, whose
519 size does increase logarithmically with its value, not linear
520 \footnote{Indeed, the \hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}} theory (see \ref{eff_nat})
521 does something similar}. First, the digit representation:%
530 \isacommand{definition}\isamarkupfalse%
531 \ Dig{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
532 \ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ n\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ n{\isachardoublequoteclose}\isanewline
534 \isacommand{definition}\isamarkupfalse%
535 \ \ Dig{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
536 \ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ n{\isacharparenright}{\isachardoublequoteclose}%
544 \begin{isamarkuptext}%
545 \noindent We will use these two \qt{digits} to represent natural numbers
546 in binary digits, e.g.:%
555 \isacommand{lemma}\isamarkupfalse%
556 \ {\isadigit{4}}{\isadigit{2}}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}Dig{\isadigit{1}}\ {\isacharparenleft}Dig{\isadigit{0}}\ {\isacharparenleft}Dig{\isadigit{1}}\ {\isacharparenleft}Dig{\isadigit{0}}\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
557 \ \ \isacommand{by}\isamarkupfalse%
558 \ {\isacharparenleft}simp\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
566 \begin{isamarkuptext}%
567 \noindent Of course we also have to provide proper code equations for
568 the operations, e.g. \isa{op\ {\isacharplus}}:%
577 \isacommand{lemma}\isamarkupfalse%
578 \ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
579 \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
580 \ \ {\isachardoublequoteopen}m\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
581 \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ n{\isachardoublequoteclose}\isanewline
582 \ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ {\isadigit{1}}\ {\isacharequal}\ Dig{\isadigit{1}}\ m{\isachardoublequoteclose}\isanewline
583 \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
584 \ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ {\isadigit{1}}\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
585 \ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
586 \ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
587 \ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
588 \ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
589 \ \ \isacommand{by}\isamarkupfalse%
590 \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
598 \begin{isamarkuptext}%
599 \noindent We then instruct the code generator to view \isa{{\isadigit{0}}},
600 \isa{{\isadigit{1}}}, \isa{Dig{\isadigit{0}}} and \isa{Dig{\isadigit{1}}} as
601 datatype constructors:%
610 \isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
611 \ {\isachardoublequoteopen}{\isadigit{0}}{\isasymColon}nat{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isadigit{1}}{\isasymColon}nat{\isachardoublequoteclose}\ Dig{\isadigit{0}}\ Dig{\isadigit{1}}%
619 \begin{isamarkuptext}%
620 \noindent For the former constructor \isa{Suc}, we provide a code
621 equation and remove some parts of the default code generator setup
622 which are an obstacle here:%
631 \isacommand{lemma}\isamarkupfalse%
632 \ Suc{\isacharunderscore}Dig\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
633 \ \ {\isachardoublequoteopen}Suc\ n\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
634 \ \ \isacommand{by}\isamarkupfalse%
637 \isacommand{declare}\isamarkupfalse%
638 \ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline\ del{\isacharbrackright}\isanewline
639 \isacommand{declare}\isamarkupfalse%
640 \ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ del{\isacharbrackright}%
648 \begin{isamarkuptext}%
649 \noindent This yields the following code:%
659 \begin{isamarkuptext}%
662 \hspace*{0pt}structure Example = \\
663 \hspace*{0pt}struct\\
665 \hspace*{0pt}datatype nat = Dig1 of nat | Dig0 of nat | One{\char95}nat | Zero{\char95}nat;\\
667 \hspace*{0pt}fun plus{\char95}nat (Dig1 m) (Dig1 n) = Dig0 (plus{\char95}nat (plus{\char95}nat m n) One{\char95}nat)\\
668 \hspace*{0pt} ~| plus{\char95}nat (Dig1 m) (Dig0 n) = Dig1 (plus{\char95}nat m n)\\
669 \hspace*{0pt} ~| plus{\char95}nat (Dig0 m) (Dig1 n) = Dig1 (plus{\char95}nat m n)\\
670 \hspace*{0pt} ~| plus{\char95}nat (Dig0 m) (Dig0 n) = Dig0 (plus{\char95}nat m n)\\
671 \hspace*{0pt} ~| plus{\char95}nat (Dig1 m) One{\char95}nat = Dig0 (plus{\char95}nat m One{\char95}nat)\\
672 \hspace*{0pt} ~| plus{\char95}nat One{\char95}nat (Dig1 n) = Dig0 (plus{\char95}nat n One{\char95}nat)\\
673 \hspace*{0pt} ~| plus{\char95}nat (Dig0 m) One{\char95}nat = Dig1 m\\
674 \hspace*{0pt} ~| plus{\char95}nat One{\char95}nat (Dig0 n) = Dig1 n\\
675 \hspace*{0pt} ~| plus{\char95}nat m Zero{\char95}nat = m\\
676 \hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
678 \hspace*{0pt}end; (*struct Example*)%
689 \begin{isamarkuptext}%
690 \noindent From this example, it can be easily glimpsed that using own constructor sets
691 is a little delicate since it changes the set of valid patterns for values
692 of that type. Without going into much detail, here some practical hints:
695 \item When changing the constructor set for datatypes, take care to
696 provide an alternative for the \isa{case} combinator (e.g.~by replacing
697 it using the preprocessor).
698 \item Values in the target language need not to be normalised -- different
699 values in the target language may represent the same value in the
700 logic (e.g. \isa{Dig{\isadigit{1}}\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}}).
701 \item Usually, a good methodology to deal with the subtleties of pattern
702 matching is to see the type as an abstract type: provide a set
703 of operations which operate on the concrete representation of the type,
704 and derive further operations by combinations of these primitive ones,
705 without relying on a particular representation.
712 \endisadeliminvisible
715 \isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
716 \ {\isachardoublequoteopen}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isachardoublequoteclose}\ Suc\isanewline
717 \isacommand{declare}\isamarkupfalse%
718 \ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ del{\isacharbrackright}\isanewline
719 \isacommand{declare}\isamarkupfalse%
720 \ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline{\isacharbrackright}\isanewline
721 \isacommand{declare}\isamarkupfalse%
722 \ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code{\isacharbrackright}\ \isanewline
723 \isacommand{lemma}\isamarkupfalse%
724 \ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymColon}\ nat{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
731 \endisadeliminvisible
733 \isamarkupsubsection{Equality and wellsortedness%
737 \begin{isamarkuptext}%
738 Surely you have already noticed how equality is treated
739 by the code generator:%
748 \isacommand{primrec}\isamarkupfalse%
749 \ 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
750 \ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
751 \ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline
752 \ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline
753 \ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline
754 \ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline
755 \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}%
763 \begin{isamarkuptext}%
764 \noindent The membership test during preprocessing is rewritten,
765 resulting in \isa{op\ mem}, which itself
766 performs an explicit equality check.%
776 \begin{isamarkuptext}%
779 \hspace*{0pt}structure Example = \\
780 \hspace*{0pt}struct\\
782 \hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
783 \hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\
785 \hspace*{0pt}fun eqop A{\char95}~a b = eq A{\char95}~a b;\\
787 \hspace*{0pt}fun member A{\char95}~x [] = false\\
788 \hspace*{0pt} ~| member A{\char95}~x (y ::~ys) = eqop A{\char95}~x y orelse member A{\char95}~x ys;\\
790 \hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
791 \hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
792 \hspace*{0pt} ~~~(if member A{\char95}~z xs\\
793 \hspace*{0pt} ~~~~~then (if member A{\char95}~z ys then collect{\char95}duplicates A{\char95}~xs ys zs\\
794 \hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
795 \hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
797 \hspace*{0pt}end; (*struct Example*)%
808 \begin{isamarkuptext}%
809 \noindent Obviously, polymorphic equality is implemented the Haskell
810 way using a type class. How is this achieved? HOL introduces
811 an explicit class \isa{eq} with a corresponding operation
812 \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharequal}\ op\ {\isacharequal}}.
813 The preprocessing framework does the rest by propagating the
814 \isa{eq} constraints through all dependent defining equations.
815 For datatypes, instances of \isa{eq} are implicitly derived
816 when possible. For other types, you may instantiate \isa{eq}
817 manually like any other type class.
819 Though this \isa{eq} class is designed to get rarely in
821 enters the stage when definitions of overloaded constants
822 are dependent on operational equality. For example, let
823 us define a lexicographic ordering on tuples
824 (also see theory \hyperlink{theory.Product-ord}{\mbox{\isa{Product{\isacharunderscore}ord}}}):%
833 \isacommand{instantiation}\isamarkupfalse%
834 \ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}order{\isacharcomma}\ order{\isacharparenright}\ order\isanewline
835 \isakeyword{begin}\isanewline
837 \isacommand{definition}\isamarkupfalse%
838 \ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\isanewline
839 \ \ {\isachardoublequoteopen}x\ {\isasymle}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isasymle}\ snd\ y{\isachardoublequoteclose}\isanewline
841 \isacommand{definition}\isamarkupfalse%
842 \ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\isanewline
843 \ \ {\isachardoublequoteopen}x\ {\isacharless}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isacharless}\ snd\ y{\isachardoublequoteclose}\isanewline
845 \isacommand{instance}\isamarkupfalse%
846 \ \isacommand{proof}\isamarkupfalse%
848 \isacommand{qed}\isamarkupfalse%
849 \ {\isacharparenleft}auto\ simp{\isacharcolon}\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}prod{\isacharunderscore}def\ intro{\isacharcolon}\ order{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}\isanewline
851 \isacommand{end}\isamarkupfalse%
854 \isacommand{lemma}\isamarkupfalse%
855 \ order{\isacharunderscore}prod\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
856 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}order{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
857 \ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
858 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}order{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
859 \ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
860 \ \ \isacommand{by}\isamarkupfalse%
861 \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}%
869 \begin{isamarkuptext}%
870 \noindent Then code generation will fail. Why? The definition
871 of \isa{op\ {\isasymle}} depends on equality on both arguments,
872 which are polymorphic and impose an additional \isa{eq}
873 class constraint, which the preprocessor does not propagate
874 (for technical reasons).
876 The solution is to add \isa{eq} explicitly to the first sort arguments in the
886 \isacommand{lemma}\isamarkupfalse%
887 \ order{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
888 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}order{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
889 \ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
890 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}order{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
891 \ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
892 \ \ \isacommand{by}\isamarkupfalse%
893 \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}%
901 \begin{isamarkuptext}%
902 \noindent Then code generation succeeds:%
912 \begin{isamarkuptext}%
915 \hspace*{0pt}structure Example = \\
916 \hspace*{0pt}struct\\
918 \hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
919 \hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\
921 \hspace*{0pt}type 'a ord = {\char123}less{\char95}eq :~'a -> 'a -> bool, less :~'a -> 'a -> bool{\char125};\\
922 \hspace*{0pt}fun less{\char95}eq (A{\char95}:'a ord) = {\char35}less{\char95}eq A{\char95};\\
923 \hspace*{0pt}fun less (A{\char95}:'a ord) = {\char35}less A{\char95};\\
925 \hspace*{0pt}fun eqop A{\char95}~a b = eq A{\char95}~a b;\\
927 \hspace*{0pt}type 'a preorder = {\char123}Orderings{\char95}{\char95}ord{\char95}preorder :~'a ord{\char125};\\
928 \hspace*{0pt}fun ord{\char95}preorder (A{\char95}:'a preorder) = {\char35}Orderings{\char95}{\char95}ord{\char95}preorder A{\char95};\\
930 \hspace*{0pt}type 'a order = {\char123}Orderings{\char95}{\char95}preorder{\char95}order :~'a preorder{\char125};\\
931 \hspace*{0pt}fun preorder{\char95}order (A{\char95}:'a order) = {\char35}Orderings{\char95}{\char95}preorder{\char95}order A{\char95};\\
933 \hspace*{0pt}fun less{\char95}eqa (A1{\char95}, A2{\char95}) B{\char95}~(x1, y1) (x2, y2) =\\
934 \hspace*{0pt} ~less ((ord{\char95}preorder o preorder{\char95}order) A2{\char95}) x1 x2 orelse\\
935 \hspace*{0pt} ~~~eqop A1{\char95}~x1 x2 andalso\\
936 \hspace*{0pt} ~~~~~less{\char95}eq ((ord{\char95}preorder o preorder{\char95}order) B{\char95}) y1 y2\\
937 \hspace*{0pt} ~| less{\char95}eqa (A1{\char95}, A2{\char95}) B{\char95}~(x1, y1) (x2, y2) =\\
938 \hspace*{0pt} ~~~less ((ord{\char95}preorder o preorder{\char95}order) A2{\char95}) x1 x2 orelse\\
939 \hspace*{0pt} ~~~~~eqop A1{\char95}~x1 x2 andalso\\
940 \hspace*{0pt} ~~~~~~~less{\char95}eq ((ord{\char95}preorder o preorder{\char95}order) B{\char95}) y1 y2;\\
942 \hspace*{0pt}end; (*struct Example*)%
953 \begin{isamarkuptext}%
954 In some cases, the automatically derived defining equations
955 for equality on a particular type may not be appropriate.
956 As example, watch the following datatype representing
957 monomorphic parametric types (where type constructors
958 are referred to by natural numbers):%
967 \isacommand{datatype}\isamarkupfalse%
968 \ monotype\ {\isacharequal}\ Mono\ nat\ {\isachardoublequoteopen}monotype\ list{\isachardoublequoteclose}%
989 \begin{isamarkuptext}%
990 \noindent Then code generation for SML would fail with a message
991 that the generated code contains illegal mutual dependencies:
992 the theorem \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymequiv}\ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}} already requires the
993 instance \isa{monotype\ {\isasymColon}\ eq}, which itself requires
994 \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymequiv}\ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}}; Haskell has no problem with mutually
995 recursive \isa{instance} and \isa{function} definitions,
996 but the SML serialiser does not support this.
998 In such cases, you have to provide your own equality equations
999 involving auxiliary constants. In our case,
1000 \isa{list{\isacharunderscore}all{\isadigit{2}}} can do the job:%
1001 \end{isamarkuptext}%
1009 \isacommand{lemma}\isamarkupfalse%
1010 \ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
1011 \ \ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
1012 \ \ \ \ \ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ list{\isacharunderscore}all{\isadigit{2}}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}{\isachardoublequoteclose}\isanewline
1013 \ \ \isacommand{by}\isamarkupfalse%
1014 \ {\isacharparenleft}simp\ add{\isacharcolon}\ eq\ list{\isacharunderscore}all{\isadigit{2}}{\isacharunderscore}eq\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}%
1022 \begin{isamarkuptext}%
1023 \noindent does not depend on instance \isa{monotype\ {\isasymColon}\ eq}:%
1024 \end{isamarkuptext}%
1033 \begin{isamarkuptext}%
1036 \hspace*{0pt}structure Example = \\
1037 \hspace*{0pt}struct\\
1039 \hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
1041 \hspace*{0pt}fun null [] = true\\
1042 \hspace*{0pt} ~| null (x ::~xs) = false;\\
1044 \hspace*{0pt}fun eq{\char95}nat (Suc a) Zero{\char95}nat = false\\
1045 \hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat (Suc a) = false\\
1046 \hspace*{0pt} ~| eq{\char95}nat (Suc nat) (Suc nat') = eq{\char95}nat nat nat'\\
1047 \hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat Zero{\char95}nat = true;\\
1049 \hspace*{0pt}datatype monotype = Mono of nat * monotype list;\\
1051 \hspace*{0pt}fun list{\char95}all2 p (x ::~xs) (y ::~ys) = p x y andalso list{\char95}all2 p xs ys\\
1052 \hspace*{0pt} ~| list{\char95}all2 p xs [] = null xs\\
1053 \hspace*{0pt} ~| list{\char95}all2 p [] ys = null ys;\\
1055 \hspace*{0pt}fun eq{\char95}monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =\\
1056 \hspace*{0pt} ~eq{\char95}nat tyco1 tyco2 andalso list{\char95}all2 eq{\char95}monotype typargs1 typargs2;\\
1058 \hspace*{0pt}end; (*struct Example*)%
1059 \end{isamarkuptext}%
1069 \isamarkupsubsection{Explicit partiality%
1073 \begin{isamarkuptext}%
1074 Partiality usually enters the game by partial patterns, as
1075 in the following example, again for amortised queues:%
1076 \end{isamarkuptext}%
1084 \isacommand{fun}\isamarkupfalse%
1085 \ strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1086 \ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ Queue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
1087 \ \ {\isacharbar}\ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
1088 \ \ \ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
1096 \begin{isamarkuptext}%
1097 \noindent In the corresponding code, there is no equation
1098 for the pattern \isa{Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:%
1099 \end{isamarkuptext}%
1108 \begin{isamarkuptext}%
1111 \hspace*{0pt}strict{\char95}dequeue ::~forall a. Queue a -> (a, Queue a);\\
1112 \hspace*{0pt}strict{\char95}dequeue (Queue xs (y :~ys)) = (y, Queue xs ys);\\
1113 \hspace*{0pt}strict{\char95}dequeue (Queue xs []) =\\
1114 \hspace*{0pt} ~let {\char123}\\
1115 \hspace*{0pt} ~~~(y :~ys) = rev xs;\\
1116 \hspace*{0pt} ~{\char125}~in (y, Queue [] ys);%
1117 \end{isamarkuptext}%
1127 \begin{isamarkuptext}%
1128 \noindent In some cases it is desirable to have this
1129 pseudo-\qt{partiality} more explicitly, e.g.~as follows:%
1130 \end{isamarkuptext}%
1138 \isacommand{axiomatization}\isamarkupfalse%
1139 \ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline
1141 \isacommand{function}\isamarkupfalse%
1142 \ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1143 \ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline
1144 \ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
1145 \ \ {\isacharbar}\ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}Queue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
1146 \ \ \ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ Queue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
1147 \isacommand{by}\isamarkupfalse%
1148 \ pat{\isacharunderscore}completeness\ auto\isanewline
1150 \isacommand{termination}\isamarkupfalse%
1151 \ strict{\isacharunderscore}dequeue{\isacharprime}\isanewline
1152 \isacommand{by}\isamarkupfalse%
1153 \ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}q{\isacharcolon}{\isacharcolon}{\isacharprime}a\ queue{\isachardot}\ case\ q\ of\ Queue\ xs\ ys\ {\isasymRightarrow}\ length\ xs{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\ simp{\isacharunderscore}all%
1161 \begin{isamarkuptext}%
1162 \noindent For technical reasons the definition of
1163 \isa{strict{\isacharunderscore}dequeue{\isacharprime}} is more involved since it requires
1164 a manual termination proof. Apart from that observe that
1165 on the right hand side of its first equation the constant
1166 \isa{empty{\isacharunderscore}queue} occurs which is unspecified.
1168 Normally, if constants without any defining equations occur in
1169 a program, the code generator complains (since in most cases
1170 this is not what the user expects). But such constants can also
1171 be thought of as function definitions with no equations which
1172 always fail, since there is never a successful pattern match
1173 on the left hand side. In order to categorise a constant into
1174 that category explicitly, use \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:%
1175 \end{isamarkuptext}%
1183 \isacommand{code{\isacharunderscore}abort}\isamarkupfalse%
1184 \ empty{\isacharunderscore}queue%
1192 \begin{isamarkuptext}%
1193 \noindent Then the code generator will just insert an error or
1194 exception at the appropriate position:%
1195 \end{isamarkuptext}%
1204 \begin{isamarkuptext}%
1207 \hspace*{0pt}empty{\char95}queue ::~forall a. a;\\
1208 \hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
1210 \hspace*{0pt}strict{\char95}dequeue' ::~forall a. Queue a -> (a, Queue a);\\
1211 \hspace*{0pt}strict{\char95}dequeue' (Queue xs []) =\\
1212 \hspace*{0pt} ~(if nulla xs then empty{\char95}queue else strict{\char95}dequeue' (Queue [] (rev xs)));\\
1213 \hspace*{0pt}strict{\char95}dequeue' (Queue xs (y :~ys)) = (y, Queue xs ys);%
1214 \end{isamarkuptext}%
1224 \begin{isamarkuptext}%
1225 \noindent This feature however is rarely needed in practice.
1226 Note also that the \isa{HOL} default setup already declares
1227 \isa{undefined} as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most
1228 likely to be used in such situations.%
1229 \end{isamarkuptext}%
1237 \isacommand{end}\isamarkupfalse%
1246 \ \end{isabellebody}%
1247 %%% Local Variables:
1249 %%% TeX-master: "root"