doc-src/Codegen/Thy/document/Program.tex
author haftmann
Tue May 26 12:31:01 2009 +0200 (2009-05-26)
changeset 31254 03a35fbc9dc6
parent 31150 03a87478b89e
child 31544 19b77b1de188
permissions -rw-r--r--
documented print_codeproc command
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Program}%
     4 %
     5 \isadelimtheory
     6 %
     7 \endisadelimtheory
     8 %
     9 \isatagtheory
    10 \isacommand{theory}\isamarkupfalse%
    11 \ Program\isanewline
    12 \isakeyword{imports}\ Introduction\isanewline
    13 \isakeyword{begin}%
    14 \endisatagtheory
    15 {\isafoldtheory}%
    16 %
    17 \isadelimtheory
    18 %
    19 \endisadelimtheory
    20 %
    21 \isamarkupsection{Turning Theories into Programs \label{sec:program}%
    22 }
    23 \isamarkuptrue%
    24 %
    25 \isamarkupsubsection{The \isa{Isabelle{\isacharslash}HOL} default setup%
    26 }
    27 \isamarkuptrue%
    28 %
    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 code 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
    37   correct.%
    38 \end{isamarkuptext}%
    39 \isamarkuptrue%
    40 %
    41 \isamarkupsubsection{Selecting code equations%
    42 }
    43 \isamarkuptrue%
    44 %
    45 \begin{isamarkuptext}%
    46 Coming back to our introductory example, we
    47   could provide an alternative code equations for \isa{dequeue}
    48   explicitly:%
    49 \end{isamarkuptext}%
    50 \isamarkuptrue%
    51 %
    52 \isadelimquote
    53 %
    54 \endisadelimquote
    55 %
    56 \isatagquote
    57 \isacommand{lemma}\isamarkupfalse%
    58 \ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
    59 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
    60 \ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
    61 \ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
    62 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
    63 \ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ 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}%
    66 \endisatagquote
    67 {\isafoldquote}%
    68 %
    69 \isadelimquote
    70 %
    71 \endisadelimquote
    72 %
    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 code equations for a \isa{fun} statement --
    77   the corresponding constant is determined syntactically.  The resulting code:%
    78 \end{isamarkuptext}%
    79 \isamarkuptrue%
    80 %
    81 \isadelimquote
    82 %
    83 \endisadelimquote
    84 %
    85 \isatagquote
    86 %
    87 \begin{isamarkuptext}%
    88 \isatypewriter%
    89 \noindent%
    90 \hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
    91 \hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
    92 \hspace*{0pt}dequeue (AQueue xs []) =\\
    93 \hspace*{0pt} ~(if nulla xs then (Nothing,~AQueue [] [])\\
    94 \hspace*{0pt} ~~~else dequeue (AQueue [] (rev xs)));%
    95 \end{isamarkuptext}%
    96 \isamarkuptrue%
    97 %
    98 \endisatagquote
    99 {\isafoldquote}%
   100 %
   101 \isadelimquote
   102 %
   103 \endisadelimquote
   104 %
   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}).
   109 
   110   Changing the default constructor set of datatypes is also
   111   possible.  See \secref{sec:datatypes} for an example.
   112 
   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:%
   117 \end{isamarkuptext}%
   118 \isamarkuptrue%
   119 %
   120 \isadelimquote
   121 %
   122 \endisadelimquote
   123 %
   124 \isatagquote
   125 \isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
   126 \ dequeue%
   127 \endisatagquote
   128 {\isafoldquote}%
   129 %
   130 \isadelimquote
   131 %
   132 \endisadelimquote
   133 %
   134 \begin{isamarkuptext}%
   135 \noindent prints a table with \emph{all} code equations
   136   for \isa{dequeue}, including
   137   \emph{all} code equations those equations depend
   138   on recursively.
   139   
   140   Similarly, the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command shows a graph
   141   visualising dependencies between code equations.%
   142 \end{isamarkuptext}%
   143 \isamarkuptrue%
   144 %
   145 \isamarkupsubsection{\isa{class} and \isa{instantiation}%
   146 }
   147 \isamarkuptrue%
   148 %
   149 \begin{isamarkuptext}%
   150 Concerning type classes and code generation, let us examine an example
   151   from abstract algebra:%
   152 \end{isamarkuptext}%
   153 \isamarkuptrue%
   154 %
   155 \isadelimquote
   156 %
   157 \endisadelimquote
   158 %
   159 \isatagquote
   160 \isacommand{class}\isamarkupfalse%
   161 \ semigroup\ {\isacharequal}\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
   164 \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
   170 \isanewline
   171 \isacommand{instantiation}\isamarkupfalse%
   172 \ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline
   173 \isakeyword{begin}\isanewline
   174 \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
   179 \isanewline
   180 \isacommand{definition}\isamarkupfalse%
   181 \ neutral{\isacharunderscore}nat\ \isakeyword{where}\isanewline
   182 \ \ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
   183 \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
   190 \isanewline
   191 \isacommand{instance}\isamarkupfalse%
   192 \ \isacommand{proof}\isamarkupfalse%
   193 \isanewline
   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%
   209 \isanewline
   210 \isanewline
   211 \isacommand{end}\isamarkupfalse%
   212 %
   213 \endisatagquote
   214 {\isafoldquote}%
   215 %
   216 \isadelimquote
   217 %
   218 \endisadelimquote
   219 %
   220 \begin{isamarkuptext}%
   221 \noindent We define the natural operation of the natural numbers
   222   on monoids:%
   223 \end{isamarkuptext}%
   224 \isamarkuptrue%
   225 %
   226 \isadelimquote
   227 %
   228 \endisadelimquote
   229 %
   230 \isatagquote
   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}%
   235 \endisatagquote
   236 {\isafoldquote}%
   237 %
   238 \isadelimquote
   239 %
   240 \endisadelimquote
   241 %
   242 \begin{isamarkuptext}%
   243 \noindent This we use to define the discrete exponentiation function:%
   244 \end{isamarkuptext}%
   245 \isamarkuptrue%
   246 %
   247 \isadelimquote
   248 %
   249 \endisadelimquote
   250 %
   251 \isatagquote
   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}%
   255 \endisatagquote
   256 {\isafoldquote}%
   257 %
   258 \isadelimquote
   259 %
   260 \endisadelimquote
   261 %
   262 \begin{isamarkuptext}%
   263 \noindent The corresponding code:%
   264 \end{isamarkuptext}%
   265 \isamarkuptrue%
   266 %
   267 \isadelimquote
   268 %
   269 \endisadelimquote
   270 %
   271 \isatagquote
   272 %
   273 \begin{isamarkuptext}%
   274 \isatypewriter%
   275 \noindent%
   276 \hspace*{0pt}module Example where {\char123}\\
   277 \hspace*{0pt}\\
   278 \hspace*{0pt}\\
   279 \hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
   280 \hspace*{0pt}\\
   281 \hspace*{0pt}class Semigroup a where {\char123}\\
   282 \hspace*{0pt} ~mult ::~a -> a -> a;\\
   283 \hspace*{0pt}{\char125};\\
   284 \hspace*{0pt}\\
   285 \hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\
   286 \hspace*{0pt} ~neutral ::~a;\\
   287 \hspace*{0pt}{\char125};\\
   288 \hspace*{0pt}\\
   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);\\
   292 \hspace*{0pt}\\
   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;\\
   296 \hspace*{0pt}\\
   297 \hspace*{0pt}neutral{\char95}nat ::~Nat;\\
   298 \hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\
   299 \hspace*{0pt}\\
   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);\\
   303 \hspace*{0pt}\\
   304 \hspace*{0pt}instance Semigroup Nat where {\char123}\\
   305 \hspace*{0pt} ~mult = mult{\char95}nat;\\
   306 \hspace*{0pt}{\char125};\\
   307 \hspace*{0pt}\\
   308 \hspace*{0pt}instance Monoid Nat where {\char123}\\
   309 \hspace*{0pt} ~neutral = neutral{\char95}nat;\\
   310 \hspace*{0pt}{\char125};\\
   311 \hspace*{0pt}\\
   312 \hspace*{0pt}bexp ::~Nat -> Nat;\\
   313 \hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
   314 \hspace*{0pt}\\
   315 \hspace*{0pt}{\char125}%
   316 \end{isamarkuptext}%
   317 \isamarkuptrue%
   318 %
   319 \endisatagquote
   320 {\isafoldquote}%
   321 %
   322 \isadelimquote
   323 %
   324 \endisadelimquote
   325 %
   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}):%
   329 \end{isamarkuptext}%
   330 \isamarkuptrue%
   331 %
   332 \isadelimquote
   333 %
   334 \endisadelimquote
   335 %
   336 \isatagquote
   337 %
   338 \begin{isamarkuptext}%
   339 \isatypewriter%
   340 \noindent%
   341 \hspace*{0pt}structure Example = \\
   342 \hspace*{0pt}struct\\
   343 \hspace*{0pt}\\
   344 \hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
   345 \hspace*{0pt}\\
   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};\\
   348 \hspace*{0pt}\\
   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};\\
   352 \hspace*{0pt}\\
   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);\\
   355 \hspace*{0pt}\\
   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;\\
   358 \hspace*{0pt}\\
   359 \hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat\\
   360 \hspace*{0pt}\\
   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);\\
   363 \hspace*{0pt}\\
   364 \hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
   365 \hspace*{0pt}\\
   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;\\
   369 \hspace*{0pt}\\
   370 \hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
   371 \hspace*{0pt}\\
   372 \hspace*{0pt}end;~(*struct Example*)%
   373 \end{isamarkuptext}%
   374 \isamarkuptrue%
   375 %
   376 \endisatagquote
   377 {\isafoldquote}%
   378 %
   379 \isadelimquote
   380 %
   381 \endisadelimquote
   382 %
   383 \begin{isamarkuptext}%
   384 \noindent Note the parameters with trailing underscore (\verb|A_|)
   385     which are the dictionary parameters.%
   386 \end{isamarkuptext}%
   387 \isamarkuptrue%
   388 %
   389 \isamarkupsubsection{The preprocessor \label{sec:preproc}%
   390 }
   391 \isamarkuptrue%
   392 %
   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}.
   398 
   399   The \emph{simpset} allows to employ the full generality of the Isabelle
   400   simplifier.  Due to the interpretation of theorems
   401   as code 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.
   407 
   408   Some common applications:%
   409 \end{isamarkuptext}%
   410 \isamarkuptrue%
   411 %
   412 \begin{itemize}
   413 %
   414 \begin{isamarkuptext}%
   415 \item replacing non-executable constructs by executable ones:%
   416 \end{isamarkuptext}%
   417 \isamarkuptrue%
   418 %
   419 \isadelimquote
   420 %
   421 \endisadelimquote
   422 %
   423 \isatagquote
   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%
   428 \endisatagquote
   429 {\isafoldquote}%
   430 %
   431 \isadelimquote
   432 %
   433 \endisadelimquote
   434 %
   435 \begin{isamarkuptext}%
   436 \item eliminating superfluous constants:%
   437 \end{isamarkuptext}%
   438 \isamarkuptrue%
   439 %
   440 \isadelimquote
   441 %
   442 \endisadelimquote
   443 %
   444 \isatagquote
   445 \isacommand{lemma}\isamarkupfalse%
   446 \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
   447 \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
   448 \ simp%
   449 \endisatagquote
   450 {\isafoldquote}%
   451 %
   452 \isadelimquote
   453 %
   454 \endisadelimquote
   455 %
   456 \begin{isamarkuptext}%
   457 \item replacing executable but inconvenient constructs:%
   458 \end{isamarkuptext}%
   459 \isamarkuptrue%
   460 %
   461 \isadelimquote
   462 %
   463 \endisadelimquote
   464 %
   465 \isatagquote
   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%
   470 \endisatagquote
   471 {\isafoldquote}%
   472 %
   473 \isadelimquote
   474 %
   475 \endisadelimquote
   476 %
   477 \end{itemize}
   478 %
   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
   486   interface.
   487 
   488   \noindent The current setup of the preprocessor may be inspected using
   489   the \hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} 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 code equations.
   493 
   494   \begin{warn}
   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}.
   499   \end{warn}%
   500 \end{isamarkuptext}%
   501 \isamarkuptrue%
   502 %
   503 \isamarkupsubsection{Datatypes \label{sec:datatypes}%
   504 }
   505 \isamarkuptrue%
   506 %
   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} where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is exactly the set of \emph{all} type variables in
   510   \isa{{\isasymtau}}.  The HOL datatype package by default registers any new
   511   datatype in the table of datatypes, which may be inspected using the
   512   \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
   513 
   514   In some cases, it is appropriate to alter or extend this table.  As
   515   an example, we will develop an alternative representation of the
   516   queue example given in \secref{sec:intro}.  The amortised
   517   representation is convenient for generating code but exposes its
   518   \qt{implementation} details, which may be cumbersome when proving
   519   theorems about it.  Therefore, here a simple, straightforward
   520   representation of queues:%
   521 \end{isamarkuptext}%
   522 \isamarkuptrue%
   523 %
   524 \isadelimquote
   525 %
   526 \endisadelimquote
   527 %
   528 \isatagquote
   529 \isacommand{datatype}\isamarkupfalse%
   530 \ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
   531 \isanewline
   532 \isacommand{definition}\isamarkupfalse%
   533 \ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   534 \ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
   535 \isanewline
   536 \isacommand{primrec}\isamarkupfalse%
   537 \ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   538 \ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}Queue\ xs{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   539 \isanewline
   540 \isacommand{fun}\isamarkupfalse%
   541 \ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   542 \ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   543 \ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ x{\isacharcomma}\ Queue\ xs{\isacharparenright}{\isachardoublequoteclose}%
   544 \endisatagquote
   545 {\isafoldquote}%
   546 %
   547 \isadelimquote
   548 %
   549 \endisadelimquote
   550 %
   551 \begin{isamarkuptext}%
   552 \noindent This we can use directly for proving;  for executing,
   553   we provide an alternative characterisation:%
   554 \end{isamarkuptext}%
   555 \isamarkuptrue%
   556 %
   557 \isadelimquote
   558 %
   559 \endisadelimquote
   560 %
   561 \isatagquote
   562 \isacommand{definition}\isamarkupfalse%
   563 \ AQueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   564 \ \ {\isachardoublequoteopen}AQueue\ xs\ ys\ {\isacharequal}\ Queue\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
   565 \isanewline
   566 \isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
   567 \ AQueue%
   568 \endisatagquote
   569 {\isafoldquote}%
   570 %
   571 \isadelimquote
   572 %
   573 \endisadelimquote
   574 %
   575 \begin{isamarkuptext}%
   576 \noindent Here we define a \qt{constructor} \isa{AQueue} which
   577   is defined in terms of \isa{Queue} and interprets its arguments
   578   according to what the \emph{content} of an amortised queue is supposed
   579   to be.  Equipped with this, we are able to prove the following equations
   580   for our primitive queue operations which \qt{implement} the simple
   581   queues in an amortised fashion:%
   582 \end{isamarkuptext}%
   583 \isamarkuptrue%
   584 %
   585 \isadelimquote
   586 %
   587 \endisadelimquote
   588 %
   589 \isatagquote
   590 \isacommand{lemma}\isamarkupfalse%
   591 \ empty{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
   592 \ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
   593 \ \ \isacommand{unfolding}\isamarkupfalse%
   594 \ AQueue{\isacharunderscore}def\ empty{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
   595 \ simp\isanewline
   596 \isanewline
   597 \isacommand{lemma}\isamarkupfalse%
   598 \ enqueue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
   599 \ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline
   600 \ \ \isacommand{unfolding}\isamarkupfalse%
   601 \ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
   602 \ simp\isanewline
   603 \isanewline
   604 \isacommand{lemma}\isamarkupfalse%
   605 \ dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
   606 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
   607 \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
   608 \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   609 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
   610 \ \ \isacommand{unfolding}\isamarkupfalse%
   611 \ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
   612 \ simp{\isacharunderscore}all%
   613 \endisatagquote
   614 {\isafoldquote}%
   615 %
   616 \isadelimquote
   617 %
   618 \endisadelimquote
   619 %
   620 \begin{isamarkuptext}%
   621 \noindent For completeness, we provide a substitute for the
   622   \isa{case} combinator on queues:%
   623 \end{isamarkuptext}%
   624 \isamarkuptrue%
   625 %
   626 \isadelimquote
   627 %
   628 \endisadelimquote
   629 %
   630 \isatagquote
   631 \isacommand{lemma}\isamarkupfalse%
   632 \ queue{\isacharunderscore}case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
   633 \ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
   634 \ \ \isacommand{unfolding}\isamarkupfalse%
   635 \ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
   636 \ simp%
   637 \endisatagquote
   638 {\isafoldquote}%
   639 %
   640 \isadelimquote
   641 %
   642 \endisadelimquote
   643 %
   644 \begin{isamarkuptext}%
   645 \noindent The resulting code looks as expected:%
   646 \end{isamarkuptext}%
   647 \isamarkuptrue%
   648 %
   649 \isadelimquote
   650 %
   651 \endisadelimquote
   652 %
   653 \isatagquote
   654 %
   655 \begin{isamarkuptext}%
   656 \isatypewriter%
   657 \noindent%
   658 \hspace*{0pt}structure Example = \\
   659 \hspace*{0pt}struct\\
   660 \hspace*{0pt}\\
   661 \hspace*{0pt}fun foldl f a [] = a\\
   662 \hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
   663 \hspace*{0pt}\\
   664 \hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
   665 \hspace*{0pt}\\
   666 \hspace*{0pt}fun null [] = true\\
   667 \hspace*{0pt} ~| null (x ::~xs) = false;\\
   668 \hspace*{0pt}\\
   669 \hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
   670 \hspace*{0pt}\\
   671 \hspace*{0pt}val empty :~'a queue = AQueue ([],~[])\\
   672 \hspace*{0pt}\\
   673 \hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
   674 \hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\
   675 \hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\
   676 \hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\
   677 \hspace*{0pt}\\
   678 \hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
   679 \hspace*{0pt}\\
   680 \hspace*{0pt}end;~(*struct Example*)%
   681 \end{isamarkuptext}%
   682 \isamarkuptrue%
   683 %
   684 \endisatagquote
   685 {\isafoldquote}%
   686 %
   687 \isadelimquote
   688 %
   689 \endisadelimquote
   690 %
   691 \begin{isamarkuptext}%
   692 \noindent From this example, it can be glimpsed that using own
   693   constructor sets is a little delicate since it changes the set of
   694   valid patterns for values of that type.  Without going into much
   695   detail, here some practical hints:
   696 
   697   \begin{itemize}
   698 
   699     \item When changing the constructor set for datatypes, take care
   700       to provide alternative equations for the \isa{case} combinator.
   701 
   702     \item Values in the target language need not to be normalised --
   703       different values in the target language may represent the same
   704       value in the logic.
   705 
   706     \item Usually, a good methodology to deal with the subtleties of
   707       pattern matching is to see the type as an abstract type: provide
   708       a set of operations which operate on the concrete representation
   709       of the type, and derive further operations by combinations of
   710       these primitive ones, without relying on a particular
   711       representation.
   712 
   713   \end{itemize}%
   714 \end{isamarkuptext}%
   715 \isamarkuptrue%
   716 %
   717 \isamarkupsubsection{Equality%
   718 }
   719 \isamarkuptrue%
   720 %
   721 \begin{isamarkuptext}%
   722 Surely you have already noticed how equality is treated
   723   by the code generator:%
   724 \end{isamarkuptext}%
   725 \isamarkuptrue%
   726 %
   727 \isadelimquote
   728 %
   729 \endisadelimquote
   730 %
   731 \isatagquote
   732 \isacommand{primrec}\isamarkupfalse%
   733 \ 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
   734 \ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
   735 \ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline
   736 \ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline
   737 \ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline
   738 \ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline
   739 \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}%
   740 \endisatagquote
   741 {\isafoldquote}%
   742 %
   743 \isadelimquote
   744 %
   745 \endisadelimquote
   746 %
   747 \begin{isamarkuptext}%
   748 \noindent The membership test during preprocessing is rewritten,
   749   resulting in \isa{op\ mem}, which itself
   750   performs an explicit equality check.%
   751 \end{isamarkuptext}%
   752 \isamarkuptrue%
   753 %
   754 \isadelimquote
   755 %
   756 \endisadelimquote
   757 %
   758 \isatagquote
   759 %
   760 \begin{isamarkuptext}%
   761 \isatypewriter%
   762 \noindent%
   763 \hspace*{0pt}structure Example = \\
   764 \hspace*{0pt}struct\\
   765 \hspace*{0pt}\\
   766 \hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
   767 \hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\
   768 \hspace*{0pt}\\
   769 \hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\
   770 \hspace*{0pt}\\
   771 \hspace*{0pt}fun member A{\char95}~x [] = false\\
   772 \hspace*{0pt} ~| member A{\char95}~x (y ::~ys) = eqa A{\char95}~x y orelse member A{\char95}~x ys;\\
   773 \hspace*{0pt}\\
   774 \hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
   775 \hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
   776 \hspace*{0pt} ~~~(if member A{\char95}~z xs\\
   777 \hspace*{0pt} ~~~~~then (if member A{\char95}~z ys then collect{\char95}duplicates A{\char95}~xs ys zs\\
   778 \hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
   779 \hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
   780 \hspace*{0pt}\\
   781 \hspace*{0pt}end;~(*struct Example*)%
   782 \end{isamarkuptext}%
   783 \isamarkuptrue%
   784 %
   785 \endisatagquote
   786 {\isafoldquote}%
   787 %
   788 \isadelimquote
   789 %
   790 \endisadelimquote
   791 %
   792 \begin{isamarkuptext}%
   793 \noindent Obviously, polymorphic equality is implemented the Haskell
   794   way using a type class.  How is this achieved?  HOL introduces
   795   an explicit class \isa{eq} with a corresponding operation
   796   \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharequal}\ op\ {\isacharequal}}.
   797   The preprocessing framework does the rest by propagating the
   798   \isa{eq} constraints through all dependent code equations.
   799   For datatypes, instances of \isa{eq} are implicitly derived
   800   when possible.  For other types, you may instantiate \isa{eq}
   801   manually like any other type class.
   802 
   803   Though this \isa{eq} class is designed to get rarely in
   804   the way, in some cases the automatically derived code equations
   805   for equality on a particular type may not be appropriate.
   806   As example, watch the following datatype representing
   807   monomorphic parametric types (where type constructors
   808   are referred to by natural numbers):%
   809 \end{isamarkuptext}%
   810 \isamarkuptrue%
   811 %
   812 \isadelimquote
   813 %
   814 \endisadelimquote
   815 %
   816 \isatagquote
   817 \isacommand{datatype}\isamarkupfalse%
   818 \ monotype\ {\isacharequal}\ Mono\ nat\ {\isachardoublequoteopen}monotype\ list{\isachardoublequoteclose}%
   819 \endisatagquote
   820 {\isafoldquote}%
   821 %
   822 \isadelimquote
   823 %
   824 \endisadelimquote
   825 %
   826 \isadelimproof
   827 %
   828 \endisadelimproof
   829 %
   830 \isatagproof
   831 %
   832 \endisatagproof
   833 {\isafoldproof}%
   834 %
   835 \isadelimproof
   836 %
   837 \endisadelimproof
   838 %
   839 \begin{isamarkuptext}%
   840 \noindent Then code generation for SML would fail with a message
   841   that the generated code contains illegal mutual dependencies:
   842   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
   843   instance \isa{monotype\ {\isasymColon}\ eq}, which itself requires
   844   \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
   845   recursive \isa{instance} and \isa{function} definitions,
   846   but the SML serialiser does not support this.
   847 
   848   In such cases, you have to provide your own equality equations
   849   involving auxiliary constants.  In our case,
   850   \isa{list{\isacharunderscore}all{\isadigit{2}}} can do the job:%
   851 \end{isamarkuptext}%
   852 \isamarkuptrue%
   853 %
   854 \isadelimquote
   855 %
   856 \endisadelimquote
   857 %
   858 \isatagquote
   859 \isacommand{lemma}\isamarkupfalse%
   860 \ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
   861 \ \ {\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
   862 \ \ \ \ \ 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
   863 \ \ \isacommand{by}\isamarkupfalse%
   864 \ {\isacharparenleft}simp\ add{\isacharcolon}\ eq\ list{\isacharunderscore}all{\isadigit{2}}{\isacharunderscore}eq\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}%
   865 \endisatagquote
   866 {\isafoldquote}%
   867 %
   868 \isadelimquote
   869 %
   870 \endisadelimquote
   871 %
   872 \begin{isamarkuptext}%
   873 \noindent does not depend on instance \isa{monotype\ {\isasymColon}\ eq}:%
   874 \end{isamarkuptext}%
   875 \isamarkuptrue%
   876 %
   877 \isadelimquote
   878 %
   879 \endisadelimquote
   880 %
   881 \isatagquote
   882 %
   883 \begin{isamarkuptext}%
   884 \isatypewriter%
   885 \noindent%
   886 \hspace*{0pt}structure Example = \\
   887 \hspace*{0pt}struct\\
   888 \hspace*{0pt}\\
   889 \hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
   890 \hspace*{0pt}\\
   891 \hspace*{0pt}fun null [] = true\\
   892 \hspace*{0pt} ~| null (x ::~xs) = false;\\
   893 \hspace*{0pt}\\
   894 \hspace*{0pt}fun eq{\char95}nat (Suc nat') Zero{\char95}nat = false\\
   895 \hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat (Suc nat') = false\\
   896 \hspace*{0pt} ~| eq{\char95}nat (Suc nat) (Suc nat') = eq{\char95}nat nat nat'\\
   897 \hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat Zero{\char95}nat = true;\\
   898 \hspace*{0pt}\\
   899 \hspace*{0pt}datatype monotype = Mono of nat * monotype list;\\
   900 \hspace*{0pt}\\
   901 \hspace*{0pt}fun list{\char95}all2 p (x ::~xs) (y ::~ys) = p x y andalso list{\char95}all2 p xs ys\\
   902 \hspace*{0pt} ~| list{\char95}all2 p xs [] = null xs\\
   903 \hspace*{0pt} ~| list{\char95}all2 p [] ys = null ys;\\
   904 \hspace*{0pt}\\
   905 \hspace*{0pt}fun eq{\char95}monotype (Mono (tyco1,~typargs1)) (Mono (tyco2,~typargs2)) =\\
   906 \hspace*{0pt} ~eq{\char95}nat tyco1 tyco2 andalso list{\char95}all2 eq{\char95}monotype typargs1 typargs2;\\
   907 \hspace*{0pt}\\
   908 \hspace*{0pt}end;~(*struct Example*)%
   909 \end{isamarkuptext}%
   910 \isamarkuptrue%
   911 %
   912 \endisatagquote
   913 {\isafoldquote}%
   914 %
   915 \isadelimquote
   916 %
   917 \endisadelimquote
   918 %
   919 \isamarkupsubsection{Explicit partiality%
   920 }
   921 \isamarkuptrue%
   922 %
   923 \begin{isamarkuptext}%
   924 Partiality usually enters the game by partial patterns, as
   925   in the following example, again for amortised queues:%
   926 \end{isamarkuptext}%
   927 \isamarkuptrue%
   928 %
   929 \isadelimquote
   930 %
   931 \endisadelimquote
   932 %
   933 \isatagquote
   934 \isacommand{definition}\isamarkupfalse%
   935 \ strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   936 \ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\isanewline
   937 \ \ \ \ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   938 \isanewline
   939 \isacommand{lemma}\isamarkupfalse%
   940 \ strict{\isacharunderscore}dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
   941 \ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
   942 \ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
   943 \ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   944 \ \ \isacommand{by}\isamarkupfalse%
   945 \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
   946 \endisatagquote
   947 {\isafoldquote}%
   948 %
   949 \isadelimquote
   950 %
   951 \endisadelimquote
   952 %
   953 \begin{isamarkuptext}%
   954 \noindent In the corresponding code, there is no equation
   955   for the pattern \isa{AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:%
   956 \end{isamarkuptext}%
   957 \isamarkuptrue%
   958 %
   959 \isadelimquote
   960 %
   961 \endisadelimquote
   962 %
   963 \isatagquote
   964 %
   965 \begin{isamarkuptext}%
   966 \isatypewriter%
   967 \noindent%
   968 \hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
   969 \hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
   970 \hspace*{0pt} ~let {\char123}\\
   971 \hspace*{0pt} ~~~(y :~ys) = rev xs;\\
   972 \hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
   973 \hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
   974 \end{isamarkuptext}%
   975 \isamarkuptrue%
   976 %
   977 \endisatagquote
   978 {\isafoldquote}%
   979 %
   980 \isadelimquote
   981 %
   982 \endisadelimquote
   983 %
   984 \begin{isamarkuptext}%
   985 \noindent In some cases it is desirable to have this
   986   pseudo-\qt{partiality} more explicitly, e.g.~as follows:%
   987 \end{isamarkuptext}%
   988 \isamarkuptrue%
   989 %
   990 \isadelimquote
   991 %
   992 \endisadelimquote
   993 %
   994 \isatagquote
   995 \isacommand{axiomatization}\isamarkupfalse%
   996 \ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline
   997 \isanewline
   998 \isacommand{definition}\isamarkupfalse%
   999 \ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
  1000 \ \ {\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
  1001 \isanewline
  1002 \isacommand{lemma}\isamarkupfalse%
  1003 \ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
  1004 \ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline
  1005 \ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
  1006 \ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
  1007 \ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
  1008 \ \ \isacommand{by}\isamarkupfalse%
  1009 \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
  1010 \endisatagquote
  1011 {\isafoldquote}%
  1012 %
  1013 \isadelimquote
  1014 %
  1015 \endisadelimquote
  1016 %
  1017 \begin{isamarkuptext}%
  1018 Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}} the constant \isa{empty{\isacharunderscore}queue} occurs
  1019   which is unspecified.
  1020 
  1021   Normally, if constants without any code equations occur in a
  1022   program, the code generator complains (since in most cases this is
  1023   not what the user expects).  But such constants can also be thought
  1024   of as function definitions with no equations which always fail,
  1025   since there is never a successful pattern match on the left hand
  1026   side.  In order to categorise a constant into that category
  1027   explicitly, use \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:%
  1028 \end{isamarkuptext}%
  1029 \isamarkuptrue%
  1030 %
  1031 \isadelimquote
  1032 %
  1033 \endisadelimquote
  1034 %
  1035 \isatagquote
  1036 \isacommand{code{\isacharunderscore}abort}\isamarkupfalse%
  1037 \ empty{\isacharunderscore}queue%
  1038 \endisatagquote
  1039 {\isafoldquote}%
  1040 %
  1041 \isadelimquote
  1042 %
  1043 \endisadelimquote
  1044 %
  1045 \begin{isamarkuptext}%
  1046 \noindent Then the code generator will just insert an error or
  1047   exception at the appropriate position:%
  1048 \end{isamarkuptext}%
  1049 \isamarkuptrue%
  1050 %
  1051 \isadelimquote
  1052 %
  1053 \endisadelimquote
  1054 %
  1055 \isatagquote
  1056 %
  1057 \begin{isamarkuptext}%
  1058 \isatypewriter%
  1059 \noindent%
  1060 \hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
  1061 \hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
  1062 \hspace*{0pt}\\
  1063 \hspace*{0pt}strict{\char95}dequeue' ::~forall a.~Queue a -> (a,~Queue a);\\
  1064 \hspace*{0pt}strict{\char95}dequeue' (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
  1065 \hspace*{0pt}strict{\char95}dequeue' (AQueue xs []) =\\
  1066 \hspace*{0pt} ~(if nulla xs then empty{\char95}queue\\
  1067 \hspace*{0pt} ~~~else strict{\char95}dequeue' (AQueue [] (rev xs)));%
  1068 \end{isamarkuptext}%
  1069 \isamarkuptrue%
  1070 %
  1071 \endisatagquote
  1072 {\isafoldquote}%
  1073 %
  1074 \isadelimquote
  1075 %
  1076 \endisadelimquote
  1077 %
  1078 \begin{isamarkuptext}%
  1079 \noindent This feature however is rarely needed in practice.
  1080   Note also that the \isa{HOL} default setup already declares
  1081   \isa{undefined} as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most
  1082   likely to be used in such situations.%
  1083 \end{isamarkuptext}%
  1084 \isamarkuptrue%
  1085 %
  1086 \isadelimtheory
  1087 %
  1088 \endisadelimtheory
  1089 %
  1090 \isatagtheory
  1091 \isacommand{end}\isamarkupfalse%
  1092 %
  1093 \endisatagtheory
  1094 {\isafoldtheory}%
  1095 %
  1096 \isadelimtheory
  1097 %
  1098 \endisadelimtheory
  1099 \isanewline
  1100 \ \end{isabellebody}%
  1101 %%% Local Variables:
  1102 %%% mode: latex
  1103 %%% TeX-master: "root"
  1104 %%% End: